The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/29/2016 10:06 PM, Jonathan Leivent wrote:
> 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

I found an ugly workaround: use Existing Class eq, and wrap any 
subsequent hypothesis-like declaration that one does not want to be 
considered an instance, then unwrap it in a definition.  This works 
because complete definitions are not automatically considered instances 
of the Existing Class - although, is that a bug?  Why aren't definitions 
considered just declarations with proofs? Anyway, that's how it works 
(though none of this is in the refman or typeclassestut, or anywhere I 
googled) - so the workaround is:

Existing Class eq.

Variable T : Type.

Structure NonInstance X := { unwrap_noninstance : X }.

Axiom eqT_ : NonInstance (forall a b : T, a = b).
Definition eqT := unwrap_noninstance _ eqT_.

Print HintDb typeclass_instances.

(* neither eqT_ nor eqT appear:
Discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Cut: emp
For any goal ->
*)

For Axioms, the NonInstance wrapper seems like a somewhat plausible 
workaround, but it is probably too ugly for section Variables or module 
Parameters, as one would have to wrap the corresponding actual parameters.

I think I am stuck using "Existing Class eq" if the objective is to have 
at least some eq holes automatically filled.  I tried limiting the scope 
of Existing Class eq by wrapping it in a section or module - but that 
doesn't limit it.  And "Local Existing Class" is not legal.  This makes 
"Existing Class" a dangerous thing to use in a shared module, especially 
on ubiquitous types like eq.

How about this for an enhancement: allow the "Instance foo ... : T ... 
:= ..." syntax for T even when it is not previously declared a class.  
Currently, this produces the error "T is not a declared type class".  
This would make T into an existing class in a limited capacity, so that 
it only accepts such explicitly declared instances.

Although I also think "Local Existing Class" is worth adding as well.

-- Jonathan