The Coq mailing list

[Erik Ernst <eernst AT cs.au.dk>]

Dear all,

I've encountered a puzzling problem in connection with typing of expressions 
in the context of a dependent match.  Try this:

------------------------------------------------------------------------------------------------------------
(*
   This specification below is currently accepted by Coq 8.2pl1, where the 
'let .. in' that
   contains the lines (* 1 *) and (* 2 *) is commented out.  Now try to 
"comment
   it in" again, and comment out one of the two marked lines:


   Comment out line (* 1 *) and keep (* 2 *), and you get this error message:
   
--------------------------------------------------------------------------------
   The term "P" has type "R (natS N1') (natS N2')" while it is expected to 
have type "R N1 N2".
   
--------------------------------------------------------------------------------


   Comment out line (* 2 *) and keep (* 1 *), and you get this error message:
   
--------------------------------------------------------------------------------
    ...
    "P" : "R N1 N2"      <-- [this is the 6th term]
    ...
   The 6th term has type "R N1 N2" which should be coercible to "R (natS N1') 
(natS N2')".
   
--------------------------------------------------------------------------------

   So, essentially, we can get two error messages on the form 

     P has type A which should be B
     P has type B which should be A

   in a context where the definition of P is unchanged.  What's a guy gotta 
do? ;-)
 *)

Set Implicit Arguments.

CoInductive Nat: Set :=
| natO: Nat
| natS: Nat -> Nat.

CoInductive Nat_lt: Nat -> Nat -> Prop :=
| Nat_lt_O: forall N, Nat_lt natO (natS N)
| Nat_lt_S: forall N1 N2, Nat_lt N1 N2 -> Nat_lt (natS N1) (natS N2).

Parameter R: Nat -> Nat -> Prop.

Hypothesis Hyp: forall N1' N2' N1 N2,
  natS N1' = N1 -> natS N2' = N2 -> R N1 N2 -> R N1' N2'.

Definition cast:
  forall (R': Nat->Nat->Prop) (N1' N2' N1 N2: Nat) (P: R' N1' N2'),
    N1 = N1' -> N2 = N2' -> R' N1 N2.
Proof.
  intros. subst N1' N2'. assumption.
Defined.
Implicit Arguments cast [R' N1' N2' N1 N2].

Parameter magic: forall N1 N2, Nat_lt N1 N2.
Parameter eq_magic: forall n1 n1' : Nat, n1 = n1'.

Definition F: forall (N1 N2: Nat) (P: R N1 N2), Nat_lt N1 N2 :=
  fun (N1 N2: Nat) (P: R N1 N2) =>
    match N1,N2,P return Nat_lt N1 N2 with
      | natO     , natO     , P => magic natO natO
      | natO     , natS N2' , P => magic natO (natS N2')
      | natS N1' , natO     , P => magic (natS N1') natO
      | natS N1' , natS N2' , P =>
        let Hyp' := Hyp (eq_magic (natS N1') N1) (eq_magic (natS N2') N2) in
(*
          let P' := Hyp'
            (cast P (eq_magic N1 (natS N1')) (eq_magic N2 (natS N2')))       
(* 1 *)
            P                                                                
(* 2 *)
          in
*)
            magic (natS N1') (natS N2')
    end.
------------------------------------------------------------------------------------------------------------

-- 
Erik Ernst - 
eernst AT cs.au.dk
Department of Computer Science, Aarhus University
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark