The Coq mailing list

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

On 07/09/2016 16:13, Soegtrop, Michael wrote:
> Dear Guillaume,
> 
>> Coq just checks that this is true for all the branches  of the "match"; if 
>> so, it assumes that it is also true for the "match" itself.
> 
> Sorry, I don't get it. That is what I assumed Coq does until I saw your 
> example, but how does Coq check that (in my example below ) the branch term 
> "1" has type "bool"?

Coq does not check that 1 is of type bool; it checks that 1 is of type
nat. It is "match H ..." that is of type bool. Let me state it again.

1. "match H with" is matching a term H whose type is in the inductive
type family "eq nat", since H has type "eq nat bool".

2. The match signature is "in (eq _ t) return t", so Coq checks that 1
(which is returned in the branch matching "@eq_refl nat" of type "eq nat
nat") has type nat.

3. All the branches are well-typed, so "match H with ..." is of type
bool since H is of type "eq nat bool" and the signature is "in (eq _ t)
return t".

Best regards,

Guillaume