The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Is there a way to forbid typeclass resolution from applying a particular instance to a goal with evars in it?  For example, if I have the typeclass [Foo : nat -> Type -> Type], and I have an instance [forall `{Foo (S n) T} (x y : T), Foo n (x = y)], and I want to prevent Coq from running off into the woods by trying to solve the goal [Foo 1 ?1] by instantiating [?1] with [@eq ?2 ?3 ?4] and trying to find [Foo 2 ?2], and repeating the process forever.

Thanks,

Jason