The Coq mailing list

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

Tom Prince 
<tom.prince AT ualberta.net>
 writes:
>>   (* even though [m] is reported as implicit, Coq still will not accept 
>> this: *)
>>   (*Context `(t2:class2 t).*)

> In `{} and `() binders, implicit arguments are ignored,

Hrm, I wasn't able to find any mention of this in the manual
(particularly not in section 2.7.17).  Is this an undocumented behavior?


> also works, (the ! turning off some of the magical properties of `().

I noticed the very brief mention of the bang (!) in section 18.5.1 a
while back, but wasn't able to figure out what it did.  It also doesn't
seem to be in the manual's BNF.


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

I see.

In retrospect, perhaps it would have been better to make implicit
generalization a property of *identifiers* being bound rather than
entire *binders*.  For example, instead of:

  Definition Param2 := True.
  Context `(MyClass Param1 Param2 Param3).
  (* Param1 and Param3 are generalized but Param2 is not *)

Putting the annotation mark directly on the identifier(s) the user wants
generalized:

  Context (MyClass `Param1 Param2 `Param3).
  (* Param1 and Param3 are generalized but Param2 is not *)

This leaves the case where a class has a huge number of implicit
arguments and the user wants all of them generalized -- in that case the
user would have to explicitly list them all and put the annotation mark
on each of them.  But perhaps that isn't a bad thing.

  - a