The Coq mailing list

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

I suggest that it is appropriate to elaborate the following code:
    Definition foo (n : nat) : T n := match n with ... end.
into:
    Definition foo (n : nat) : T n := match n return T n with ... end.
but that further cleverness does more harm than good.

On 05/13/2014 10:19 AM, Cedric Auger wrote:

What do you mean by "that isn't at the top level of a definition"?

2014-05-13 16:07 GMT+02:00 Adam Chlipala <adamc AT csail.mit.edu>:

Thanks for a good example that I hope contributes further to convincing the Coq team to remove this confusing flavor of type inference for dependent [match]. :)  I don't think there is a simple explanation of the behavior you see, and IMO it would be better to require a [return] annotation on every [match] (that isn't at the top level of a definition) giving the dependent typing scheme explicitly.