The Coq mailing list

[Valentin ROBERT <vrobert AT cs.ucsd.edu>]

Hello Coq-club,

I posted this on StackOverflow but it seems to reach only a very limited audience, so this might be a better place.

cf. http://stackoverflow.com/questions/14867685/abstracting-leads-to-a-term-ill-typed-yet-well-typed

--- (I hope this renders well...)

I was stuck on a problem for a while, for which I derived a smaller standalone example:

Axiom f : nat -> Set.

Goal forall (n : nat) (e : n = n) (x : f n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

Now, if you try to destruct e, you get the following error message:

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : n0 = n0) =>
 forall x : f n0,
 match e in (_ = _n) return (f _n -> Prop) with
 | Logic.eq_refl => fun v : f n0 => v = x
 end x" which is ill-typed.

After scratching my head for a while, I couldn't figure out what was ill-typed in that term... So I tried this:

Definition illt :=
  fun (n : nat) (e : n = n) =>
  forall x : f n,
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.

And Coq accepts it, at type forall n : nat, n = n -> Prop.

So, what is wrong with this error message, and how could I solve/tweak my initial goal?

Here is the Set Printing All versions of the error message:

Error: Abstracting over the terms "n0" and "e" leads to a term
"fun (n0 : nat) (e : @eq nat n0 n0) =>
 forall x : f n0,
 match e in (@eq _ _ _n) return (f _n -> Prop) with
 | eq_refl => fun v : f n0 => @eq (f n0) v x
 end x" which is ill-typed.

It seems to be a well-typed term, and nothing is implicit.

Thank you,

- Valentin