The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2010-10-22, Adam Megacz wrote:
> 
> (*
>  * 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 is (somewhat) expected, although I am not sure if it is the most
useful behaviour. In `{} and `() binders, implicit arguments are
ignored, and all unamed arguments of Class type are automatically generalized.
But 
Context `(t2: class2 _ (t:=t)).
does work.
> 
>   (* this works *)
>   Context `(t2:@class2 _ t).

I suspect this works because @class2 isn't treated as a class for the
purposes of `(). 
Context `(t2:!class2 t)
also works, (the ! turning off some of the magical properties of `().

I am not very familiar with the coq code, but I ran into this, and did
some digging. As far as I can tell, the tricky bit is that the `{} and
`() binders need to insert extra bindings before themselves, and so have
to run when the syntax is being check, before Coq starts typechecking.
But coq only does the normal implicit argument checks and typclass
resolution at typecheck time.

As an experiment, I created an ugly hack, to play around with different
semantics in generalized binders. Right now, it keys of the second letter
of the argument name of arguments of class type. With 'z', it treats the
argument as implicit, and 'Z' as explicit.

http://codepad.org/dnChPbgM

But I suspect that it is broken in weird and wonderous ways.


  Tom