The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  This is just a case of misleading diagnostic. Indeed, the term is 
well-typed -- but it does have the type expected by the 'eq' eliminator.
That would start with fun (n0 : nat) (e : n = n0) => ... where the n is the 
variable introduced implicitly by your destruct e.
So what Coq is really saying is that the 'match' proof term it is trying to 
build to implement the destruct is ill-typed, but the diagnostic assumes the 
error is yours rather than the system's. The problem is that the Coq code for 
destruct tries to build dynamically the lambda-abstraction prefix from the 
current goal, by successively replacing the inductive family instance (e 
here) and its indices (n here) by variables. When this fails it is usually 
because some typing constraint of the original goal has been violated, hence 
the diagnostic. Here the error is somewhat silly because the tactic code just 
failed to generate the lambda abstraction it knew (from the declaration of 
eq) it had to come up with. If this annoys you, you can try using the 
ssreflect case: tactic, which will handle your example successfully.
  Cheers,
Georges

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of 
valentin.robert.42 AT gmail.com
Sent: 17 February 2013 18:40
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Abstracting leads to a term ill-typed… yet well-typed

(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