Require Import String.
Require Import Ascii.
Require Import List.

Inductive optionE (X:Type) : Type :=
  | SomeE : X -> optionE X
  | NoneE : string -> optionE X.
Implicit Arguments SomeE [[X]].
Implicit Arguments NoneE [[X]].

Inductive sublist {A : Set} : list A -> list A -> Prop :=
| sl_tail : forall (c : A) l, sublist l (c::l)
| sl_cons : forall (c : A) l' l, sublist l' l -> sublist l' (c::l).

Definition parser (T : Type) :=
  forall l : list ascii, optionE (T * {l' : list ascii | sublist l' l}).

(* This works. And I don't understand why. The type checker seems to be able to figure out that xs = c::t. *)
Definition foo {T : Type} (f : T) : parser T :=
  fun xs => match xs with
    | nil    => NoneE "End of token stream"
    | (c::t) => SomeE (f, exist _ t (sl_tail c t))
    end.

(* And this one doesn't.  And given that the above works, I don't understand why this doesn't. *)
Definition bar (f : T) : parser T :=
  fun xs => match xs with
    | nil    => NoneE "End of token stream"
    | (c::t) => SomeE (f, exist _ t (sl_tail c t))
    end.

(* And this is how I would like to actually write this code: create a placeholder at the point of
   proof, and use the tactic language to write down the proof. Explicitly constructing a proof
   is tedious, but there seems to be no way around it when using dependent types. *) 
Definition baz (f : T) : parser T :=
  fun xs => match xs with
    | nil    => NoneE "End of token stream"
    | (c::t) => SomeE (f, exist _ t _)
    end.
Proof
  apply sl_tail. (* or whatever *)
Qed.