The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

On Tue, Dec 13, 2011 at 17:44, Tom Prince 
<tom.prince AT ualberta.net>
 wrote:
>> Is it possible to declare a typeclass method as a hint?  When I say
>>
>> Hint Resolve some_method.
>>
>> if no instances have yet been declared, I get a "cannot infer implicit
>> parameter" error.  If some instances have been declared, then
>> apparently only the method applied to the first such instance is
>> declared as a hint.  I can specify which instance I want with
>>
>> Hint Resolve (@some_method some_instance).
>>
>> but I want the hint to apply to *all* instances.  However, if I write
>>
>> Hint Resolve @some_method.
>
> You probably want to add ': typeclass_instances' here.

Why?

>> I am told "some_method cannot be used as a hint".  Is there a way to
>> do this?
>
> Is is that some_method cannot be used as a hint by *auto*?

I'm not sure -- are you asking me?  This shouldn't cause the "Hint
Resolve" command to fail, should it?  The manual says that if a hint
will only be used by eauto, then "Hint Resolve" just prints a warning.

> There are a number of other things one can do. The simplest method is to use
> ':>' instead of ':' when declaring the projection ... this automatically
> declares a hint for the projection.

The method in question isn't a projection declared as part of the
typeclass definition, but a function defined later which happens to
take an argument belonging to a typeclass.  (Is the word "method"
wrong in this context?)

> You can also add arbitrary tactics as hints like
> Hint Extern 4 (<some-optional-patern>) => <some-tactic> : 
> typeclass_instances.

Hmm, I'll try that.  Thanks!

Mike