The Coq mailing list

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

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