The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/29/2016 01:05 PM, Jonathan Leivent wrote:
> On 06/29/2016 12:38 PM, Matthieu Sozeau wrote:
> > Hi Jonathan,
> >
> >    short answer is not currently. I would advise to make an abbreviation
> > class eqC instead. The fact that local hypotheses of
> > typeclass type are automatically considered for resolution is a 
> > feature. It
> > could be an option of individual class declarations
> > to not do that: only explicit Instances/Existing Instances for that 
> > class
> > would be considered. We'd certainly need to devise a
> > way to declare when a local binder (in fun (x : C foo) y => t) or a goal
> > hypothesis (e.g. after intro H) should be considered though.
> > Best,
> > -- Matthieu
>
> Thanks, Matthieu.
>
> What do you mean by an "abbreviation class eqC"?

Here's a guess - instead of "Existing Class eq", I tried this:

Class eqC {T}(a b : T) := equals : eq a b.
Hint Resolve equals : typeclass_instances.

with some specific Instances of eqC.

However, this seems to require the explicit use of "typeclass eauto" - a 
hole of eq type won't get filled automatically, unlike what was 
happening in the Existing Class eq case (and happening too often). I 
would like to have the holes corresponding to the instances of eqC 
automatically filled in.  Is there some other way to do this?

-- Jonathan