The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Guillaume,

thanks a lot for the detailed explanation! To double check if I got it now, 
let me describe it with my own words:

When typing individual cases, the "in" clause (eq _ t) is unified with the 
type of the unification result of the match argument (H) and the pattern for 
this case (eq_refl).
The unification of (H : @eq Set nat bool) and (@eq_refl x : @eq Set x x) 
gives (@eq_refl nat : @eq Set nat nat).
Unification of (@eq Set nat nat) with the in clause (eq _ t) gives t=nat, so 
the return type must be nat, which is the case for the term "1".

The type of the match statement is obtained by unifying the type of the match 
argument (@eq Set nat bool) with the in clause (eq _ t) which gives t=bool, 
so the match statement has type bool.

If I got this right, the unification of (H : @eq Set nat bool) and (@eq_refl 
x : @eq Set x x) works, because the last argument of eq is a (forall _ : A) 
and not a type family parameter, but I must admit I don't fully understand 
what  (@eq Set x x) and (@eq Set x) are then (as yet).

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928