I'm confused about the behavior of Coq's type system on the match portion of the proof term in the definition of h below:
Set Implicit Arguments.
Definition h := fun (a b : nat) (e : a = b) =>
(fun (x y : nat)(HC : b = y)(H : x = y) =>
(match H in (_ = y0) return (b = y0 -> b = x) with
| @eq_refl _ _ => fun HC0 : b = x => HC0
end HC)) a b (eq_refl b) e.
Check h tells us the overall type is "forall a b : nat, a = b -> b = a".
Since the type of H is x = y, it looks like the match will return a term of type b = y -> b = x due to the return clause. After applying the various terms that follow, we get the expected type for h.
However, fun HC0 : b = x => HC0 is the identity function of type b = x -> b = x. I don't believe there is any coercion that would force b = x -> b = x to be recognized as type b = y -> b = x.
My best guess is that the constructor for H, being @eq_refl nat x of type x = x, is unique. Since H is also of type x = y, the names x and y bind to the same term. Thus, the type system decides b = x -> b = x is of type b = y -> b = x. Is this close? Is this kind of behavior explained or documented somewhere? I looked at iota reduction, but I don't think that is correct.