The Coq mailing list

[Erik Ernst <eernst AT cs.au.dk>]

Den 23/09/2011 kl. 13.39 skrev Adam Chlipala:

> Erik Ernst wrote:
>>   "here are two definitions that contain type incorrect expressions 
>> demonstrating the following:
>> 
>>       - in 'match N1,N2 return ..', the Coq type checker tells me that P 
>> has type (R N1 N2)
>> 
>>       - in 'match N1,N2,P return ..' the Coq type checker tells me that P 
>> has type (R (natS N1') (natS N2'))
>> [...]
>> 
>>   - if we use e1[P], Coq claims that P has type (R (natS N1') (natS N2')) 
>> but it must have type (R N1 N2)
>>   - if we use e2[P], Coq claims that P has type (R N1 N2) but it must have 
>> type (R (natS N1') (natS N2'))
>> 
>> Isn't that a bug?  Shouldn't P have one specific type T in both cases?
> 
> No, because the second pattern-matching form is shadowing the old binding 
> of [P] with a new one.  They are two different variables that happen to 
> share a name.


In fact, the first quote above is about the two error messages, which used 
both forms of matching.

The second quote is about the first message I sent to [Coq-Club] about this 
issue (subject 'Type A or B?'), and here both situations arise with the 
'match N1,N2,P return ..' form.  There was no occurrence of 'match N1,N2 
return' in that message, and P is the same variable in both cases.

  best regards,

-- 
Erik Ernst - 
eernst AT cs.au.dk
Department of Computer Science, Aarhus University
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark