The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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