What is Coq's type system doing in this example? -

i'm confused behavior of coq's type system on match portion of proof term in definition of h below:

set implicit arguments. definition h := fun (a b : nat) (e : = b) => (fun (x y : nat)(hc : b = y)(h : x = y) => (match h in (_ = y0) return (b = y0 -> b = x) | @eq_refl _ _ => fun hc0 : b = x => hc0 end hc)) b (eq_refl b) e. 

check h tells overall type "forall b : nat, = b -> b = a".

since type of h x = y, looks match return term of type b = y -> b = x due return clause. after applying various terms follow, expected type h.

however, fun hc0 : b = x => hc0 identity function of type b = x -> b = x. don't believe there coercion force b = x -> b = x recognized type b = y -> b = x.

my best guess constructor h, being @eq_refl nat x of type x = x, unique. since h of type x = y, names x , y bind same term. thus, type system decides b = x -> b = x of type b = y -> b = x. close? kind of behavior explained or documented somewhere? looked @ iota reduction, don't think correct.

that pretty it. behavior documented (look "the match...with...end construction" in this manual chapter), although understanding going on there can bit daunting.

first, recall how typical match checked in coq:

inductive list (t : type) := | nil : list t | cons : t -> list t -> list t.  definition tail (t : type) (l : list t) : list t :=   match l    | nil       => nil   | cons x l' => l'   end. 

coq checks (1) every constructor of list type has corresponding branch in match, , (2) each branch has same type (in case, list t) assuming constructor arguments introduced in each branch have appropriate types (here, assuming x has type t , l' has type list t in second branch).

in such simple cases, type used check each branch same type of whole match expression. however, not true: sometimes, coq uses more specialized type based on information extracts branch checking. happens when doing case analysis on indexed inductive types, eq:

inductive eq (t : type) (x : t) : t -> prop := | eq_refl : eq t x x. 

(the = notation infix syntax sugar eq.)

the arguments of inductive type given right of colon special in coq: known indices. appearing left (in case, t , x) known parameters. parameters must different in declaration of inductive type, , must match ones used in result of constructors. instance, consider following illegal snippet:

inductive eq' (t : type) (x : t) : t -> type := | eq_refl' : eq nat 4 3. 

coq rejects example because finds nat instead of t in result of eq_refl' constructor.

indices, on other hand, not have restriction: indices appearing on return type of constructors can expression of appropriate type. furthermore, expression may differ depending on constructor at. because of this, coq allows return type of each branch vary depending on choice of index of each branch. consider following simplified version of original example.

definition h (a b : nat) (e : = b) : b = :=   match e in _ = x return x =   | eq_refl => eq_refl : =   end. 

since second argument eq index, in principle vary depending on constructor used. since find out index when constructor used, coq allows return type of match depend on index: in clause of match gives names indices of inductive type, , these names become bound variables can used in return clause.

when typing branch, coq finds out values of indices were, , substitutes values variables declared in in clause. match has 1 branch, , branch forces index equal second argument in type of e (in case, a). thus, coq tries make sure type of branch a = a (that is, x = a a substituted x). can provide eq_refl : = a , done.

now coq checked branches correct, assigns entire match expression type of return clause index of type of e substituted x. variable e has type a = b, index b, , resulting type b = a (that is, x = a b substituted x).

this answer provides more explanations on difference between parameters , indices, if helps.