The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think that non-dependent matches (where the type of every branch is unifiable), at least, shouldn't require [return] annotations.  I also think that there should be some type inference in the return annotation; I want to be able to leave underscores for things that don't depend on the variables bound in [as] and [in].

-Jason

On Tue, May 13, 2014 at 4:23 PM, Beta Ziliani <beta AT mpi-sws.org> wrote:

On Tue, May 13, 2014 at 4:07 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:
> 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.

+1

I also think cleverness can sometimes obfuscate instead of help.

>
> On 05/10/2014 04:29 PM, Jack Kolb wrote:
>
> In this case, I get the helpful error message: "Non exhaustive
> pattern-matching: no clause found for pattern 1." However, something strange
> happens when I make a similar mistake in the second of the two definitions
> given above:
>
> Definition nat_ind3: forall (P : nat -> Prop),
>   P 0 -> P 1 -> P 2 ->
>   (forall n : nat, P n -> P (S (S (S n)))) ->
>   forall n : nat, P n :=
>     fun P => fun P0 => fun P1 => fun P2 => fun PSSS =>
>       fix f (n:nat) := match n with
>          0 => P0
>        | 1 => P1
>        | (S (S (S n'))) => PSSS n' (f n')
>      end.
>
> In this case, I get the following error message:
>
> In environment
> P : nat -> Prop
> P0 : P 0
> P1 : P 1
> P2 : P 2
> PSSS : forall n : nat, P n -> P (S (S (S n)))
> f : nat -> P 0
> n : nat
> n0 : nat
> The term "P1" has type "P 1" while it is expected to have type "P 0".
>
>