The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 07/09/2016 18:52, Soegtrop, Michael wrote:
> 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".

That is right. But my explanation might have wrongly given the
impression that types flow from the thing being matched to the branches,
but you can also do it the other way around (though it is a bit more
contrived):

1 is of type nat, so t (from "return t") is nat in the branch. Since
eq_refl is both of type ?x=?x (by definition) and of type _=t (from "in
_=t"), it is of type nat=nat. So H is of type nat=?u (from "in _=t") and
the type of the "match" is ?u (from "return t").

> I don't fully understand what  (@eq Set x x) and (@eq Set x) are then (as 
> yet).

Basically, you have a family of types "@eq Set x y". Some of these types
are empty (when y != x) while some others contain a unique element
eq_refl (when y == x). Where the match construct shines is that it makes
it possible for you to deal only with those types which are potentially
inhabited.

Best regards,

Guillaume