The Coq mailing list

[<valentin.robert.42 AT gmail.com>]

(Trying again, I might have been posting the previous one wrong, sorry if this
ends up being a double-post...)

---

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 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