Abstracting leads to a term ill-typed... yet well-typed

Question

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.
forall (n : nat) (e : n = n) (x : f n),
match e in (_ = _n) return (f _n -> Prop) with
| eq_refl => fun v : f n => v = x
end x

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

The command has indeed failed with message:
Cannot instantiate metavariable P of type
"forall a : nat, n = a -> Prop" with abstraction
"fun (n : nat) (e : n = n) =>
 forall x : f n,
 match e in (_ = _n) return (f _n -> Prop) with
 | eq_refl => fun v : f n => v = x
 end x"
of incompatible type "forall n : nat, n = n -> Prop".

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

illt
     : forall n : nat, n = n -> Prop

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

EDIT: To address Robin Green's comment, here is the Set Printing All versions of the error message:

The command has indeed failed with message:
Cannot instantiate metavariable P of type
"forall (a : nat) (_ : @eq nat n a), Prop" with
abstraction
"fun (n : nat) (e : @eq nat n n) =>
 forall x : f n,
 match
   e in (eq _ _n) return (forall _ : f _n, Prop)
 with
 | eq_refl => fun v : f n => @eq (f n) v x
 end x"
of incompatible type
"forall (n : nat) (_ : @eq nat n n), Prop".

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

Answer

Here is a possible explanation of the problem. What happens when constructing a pattern-matching construct can also be described using a theorem. Here is my view of the theorem that is being used in your case.

Check eq_rect.
eq_rect
     : forall (A : Type) (x : A) (P : A -> Type),
       P x -> forall y : A, x = y -> P y

So when pattern matching on an equality, you have to provide a formula P parametrized on any value y that happens to be provably equal to x. Intuitively, you should be able to replace your pattern-matching expression by apply eq_rect, but the property P that should come up there is beyond the reach of what Coq can guess, because every occurrence of x in your formula is bound to be in type f n and cannot just be in type f m where m = n. The error message does not say that, it is probably a mistake.

To perform your proof, I suggest rather to use the fact that proofs of equality are unique in certain classes of types, and nat belongs to such a class. This is treated in the file Eqdep_dec.

Require Eqdep_dec Arith.

Now your proof goes through quite easily.

Goal forall n (x : f n) (e : n = n),
    match e in _ = _n return f _n -> Prop with
    | Logic.eq_refl => fun v : f n => v = x
    end x.
forall (n : nat) (x : f n) (e : n = n),
match e in (_ = _n) return (f _n -> Prop) with
| eq_refl => fun v : f n => v = x
end x
  intros n x e.
n: nat
x: f n
e: n = n
match e in (_ = _n) return (f _n -> Prop) with
| eq_refl => fun v : f n => v = x
end x replace e with (eq_refl n).
n: nat
x: f n
e: n = n
x = x
n: nat
x: f n
e: n = n
eq_refl = e
  -
n: nat
x: f n
e: n = n
x = x reflexivity.
  -
n: nat
x: f n
e: n = n
eq_refl = e apply Eqdep_dec.UIP_dec, PeanoNat.Nat.eq_dec.
Qed.

Now, this solution may feel unsatisfactory. Where does this UIP_dec come from? UIP stands for uniqueness of identity proofs and unfortunately, this property is not guaranteed for all arbitrary types. It is guaranteed for all types where equality is decidable (as expressed by UIP_dec), for instance nat.