While resolving typeclass evars in clenv, touch only the ones that appear in the

clenv's value and type, ensuring we don't try to solve unrelated
goals (fixes bug#3633).

2 files changed, 29 insertions, 2 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 99ea2300c..bbf7c27fd 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -59,15 +59,21 @@ let clenv_pose_dependent_evars with_evars clenv =
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
+let clenv_evars clenv value =
+  let templset = Evar.Set.union (Evarutil.evars_of_term value)
+    (Evarutil.evars_of_term (clenv_type clenv))
+  in fun ev _ -> Evar.Set.mem ev templset
+
 let clenv_refine with_evars ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
   let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let value = clenv_value clenv in
   let evd' =
     if with_classes then
-      let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
+      let evd' = Typeclasses.resolve_typeclasses ~filter:(clenv_evars clenv value)
         ~fail:(not with_evars) clenv.env clenv.evd
       in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
     else clenv.evd
@@ -75,7 +81,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
   let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS (Evd.clear_metas evd'))
-    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+    (refine_no_check (clenv_cast_meta clenv value)) gl
   end
 
 open Unification
diff --git a/test-suite/bugs/closed/3633.v b/test-suite/bugs/closed/3633.v
new file mode 100644
index 000000000..6f89ef6db
--- /dev/null
+++ b/test-suite/bugs/closed/3633.v
@@ -0,0 +1,21 @@
+Set Typeclasses Strict Resolution.
+Class Contr (A : Type) := { center : A }.
+Definition foo {A} `{Contr A} : A.
+Proof.
+  apply center.
+  Undo.
+  (* Ensure the constraints are solved indepentently, otherwise a frozen ?A 
+  makes a search for Contr ?A fail when finishing to apply (fun x => x) *)
+  apply (fun x => x), center. 
+
+(* Toplevel input, characters 7-17:
+Error:
+Unable to satisfy the following constraints:
+In environment:
+A : Type
+H : Contr A
+
+?A : "Type"
+?Contr : "Contr ?X8"
+
+ *)
\ No newline at end of file