The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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"?

Also - my particular issue was with an Axiom - shouldn't that be a very 
distinct case from a local hypothesis?

-- Jonathan

> On Wed, Jun 29, 2016 at 6:09 PM Jonathan Leivent 
> <jonikelee AT gmail.com>
> wrote:
>
> > On 06/29/2016 11:33 AM, Jonathan Leivent wrote:
> > > I just debugged an infinite loop in typeclass eauto that was
> > > apparently due to Existing Class causing instances created afterwards
> > > to become Existing Instances, even if not explicitly declared as
> > > such.  I had declared "Existing Class eq", and really only wanted a
> > > very few cases of eq to be considered instances, but some later
> > > equalities automagically became instances (I can see them via Print
> > > Hints in the typeclass_instances db).
> > >
> > > First of all - is this a feature or a bug?  Secondly, if a feature, is
> > > there a way to turn it off, at least for particular Classes?
> > >
> > > -- Jonathan
> > Hmmm... maybe it only happens with Axioms, Variables, Hypotheses, etc.?:
> >
> > Existing Class eq.
> >
> > Variable T : Type.
> >
> > Variable eqT : forall a b : T, a = b.
> >
> > Print HintDb typeclass_instances.
> >
> > (* prints:
> > Discriminated database
> > Unfoldable variable definitions: all
> > Unfoldable constant definitions: all
> > Cut: emp
> > For any goal ->
> > For eq ->   apply eqT(level 0, id 0)
> > *)
> >
> > But - still - is there a way to turn this off?
> >
> > -- Jonathan