The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

(*
 * In the script below, Coq's responses are shown in comments with a ">".
 * Commands which produce an error are commented out.  This was attempted
 * with SVN trunk r13458
 *)
Generalizable All Variables.

Section test.

  Class class1  {m:nat}    := { blah  : nat }.
  Context `(t:class1).

  Class class2 `(t:class1) := { blah2 : nat }.
  Print class2.
    (*
     *> Record class2 (m : nat) (t : class1 m) : Type := Build_class2 { blah2 
: nat }
     *> For class2: Argument m is implicit and maximally inserted
     *> For class2: Argument scopes are [nat_scope _]
     *> For Build_class2: Argument scopes are [nat_scope _ nat_scope]
     *)

  (* even though [m] is reported as implicit, Coq still will not accept this: 
*)
  (*Context `(t2:class2 t).*)
     (*> The term "t" has type "class1" while it is expected to have type 
      *> "nat". *)
  (* yet this doesn't work either *)
  (*Context `(t2:class2 _ t).*)
     (*> Error: Typeclass does not expect more arguments *)
  
  (* moreover, the following attempt also will not work; Coq
   * synthesizes a new free variable [m0] and tries to unify it with
   * the [m] synthesized when declaring [t], which, of course, fails.
   * Is this the expected behavior?  It would be better if Coq only
   * generalized variables which it has no plans to try unifying later
   * on, although perhaps that isn't easy to implement. *)
  Set Printing Implicit.
  (*Context `(t2:class2(t:=t)).*)
  (*> The term "t" has type "@class1 m" while it is expected to have type
   *> "@class1 m0". *)

  (* this works *)
  Context `(t2:@class2 _ t).
End test.