The Coq mailing list

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

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

> 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.

Exactly.

>  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!

Cool!

> 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.

The convoy pattern is a much better and more general solution, so that's an 
easy choice.  ;-)

  best regards,

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