The Coq mailing list

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

Erik Ernst wrote:
> 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.
>    

Sorry!  I didn't read carefully enough.

Now I think I see what you're saying, and it puzzles me, too!  What 
puzzles me in particular is why the rebound [P] would have its type 
changed.  I don't expect that behavior from dependent pattern-matching.  
I think you've convinced me that this is worth looking into as a bug!

I generally suggest avoiding parallel pattern-matching for tracking 
dependencies across patterns; I don't think it's meant to support that.  
But perhaps some (recently added?) feature is trying to allow this but 
doing it wrong.  All parallel matching is compiled to nested single 
matches, so it's at least clear that the parallel form can't enhance 
expressivity.