The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Does anybody know how to make this pattern matching be compiled correctly, without explicit annotations? I'm testing this on 8.4pl3, couldn't compile trunk to see whether it's been fixed there or not. Thanks!

Inductive foo : nat -> Type :=

| F0 : foo 0

| F1 (n : nat) (f : foo n) : foo n

| F2 (n : nat) (f : foo n) : foo (S n).

Inductive bar : forall n, foo n -> Type :=

| B0 (n : nat) (f : foo n) : bar n (F1 n f)

| B1 (n : nat) (f : foo n) : bar (S n) (F2 n f). (* NB: the nat index starts with a constructor *)

(* First match is compiled correctly. Coq is able to figure out all annotations by itself. 

   It also works if I add a branch for B1 returning tt, but with no annotations *)

Definition case1 n (f : foo n)

                 (b : bar n (F1 n f)) :

  forall (P : bar n (F1 n f) -> Type)

         (H : P (B0 n f)), P b :=

  match b with

  | B0 n f => fun P H => H

  end.

Definition case1' n (f : foo n)

                 (b : bar n (F1 n f)) :

  forall (P : bar n (F1 n f) -> Type)

         (H : P (B0 n f)), P b :=

  match b with

  | B0 n f => fun P H => H

  | B1 _ _ => tt

  end.

(* Here it doesn't work anymore. *)

Fail Definition case2 n (f : foo n)

                 (b : bar (S n) (F2 n f)) :

  forall (P : bar (S n) (F2 n f) -> Type)

         (H : P (B1 n f)), P b :=

  match b with

  | B1 n f => fun P H => H

  end.

(* If I add a branch for B0 returning tt,

  Coq prints an error message showing the type that it's trying to unify it with.

  It seems to try to do pattern matching on the nat before doing it on the foo (S n),

  and then it gets confused *)

Fail Definition case2' n (f : foo n)

                 (b : bar (S n) (F2 n f)) :

  forall (P : bar (S n) (F2 n f) -> Type)

         (H : P (B1 n f)), P b :=

  match b with

  | B0 _ _ => tt

  | B1 n f => fun P H => H

  end.

(* Adding an explicit annotation solves the problem *)

Definition case2 n (f : foo n)

                 (b : bar (S n) (F2 n f)) :

  forall (P : bar (S n) (F2 n f) -> Type)

         (H : P (B1 n f)), P b :=

  match b in bar n' f'

          return match f' in foo n'

                          return bar n' f' -> Type

                 with

                 | F0 => fun _ => False

                 | F1 n f => fun _ => unit

                 | F2 n f => fun b =>

                               forall (P : bar (S n) (F2 n f) -> Type)

                                      (H : P (B1 n f)), P b

                 end b

  with

  | B0 _ _ => tt

  | B1 n f => fun P H => H

  end.

--
Arthur Azevedo de Amorim