The Coq mailing list

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

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

2014-05-13 16:20 GMT+02:00 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.

Well, don’t you rather want to allow that when the overall type of the match is provided?

Well, in short, no. :-)  It's hard for me to see a simple, elegant rule that covers your examples.

I mean a:

Definition foo … := … ((fun x : <some explicit type> => …) match … end) …

or a

Definition foo … := … (match … end : <some explicit type>) …

would be allowed, but not

Definition foo (n : nat) := match n with … end.

(This is your example, but this time the ": T n" is not provided.)