The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Pierre,

> OK but pattern matching cannot currently use such information to infer
> return clause. I think this is what Michael had in mind IIUC and it makes 
> sense
> indeed.

actually my idea was to use "apply UIP_dec_typeclass" to solve "proof 
irrelevance for equalities" goals rather than return clause inference. I 
would prefer this because I think it is easier to understand.

I can imagine that extending return clause inference with type classes would 
solve many of the "ill typed term" issues I ran into since I am experimenting 
with dependent types. But I don't know how understandable this would be. It 
is already quite complicated and hard to predict as is.
 
Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928