The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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

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