The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 9 juil. 2013 à 03:19, Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> 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.

There is a way, using:
[Hint Extern (Foo _ (_ = _)) => apply inst : typeclass_instances]
It's a bit hackish but the pattern must match precisely, and (_ = _) 
does not pattern-match against ?1. Another way is to use the [not_evar t] 
tactic that succeeds iff [t] is not an evar.
-- Matthieu