The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here's a proposal: if we can fully infer the type of the [match] without inspecting it, and [pattern <match discriminee> in <type of match>] succeeds (and a further patterning on the indices/parameters, if necessary), then the resulting function should be tried as a the motive of the match.

-Jason

On Tue, May 13, 2014 at 5:29 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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