The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.