The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Sorry for the confusion caused by my use of "have".  Indeed, I was speaking meta theoretically, and meant types for which decide equality is provable.

On Thu, Aug 18, 2016, 7:51 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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