Fixing #4256 and #4484 (changes in evar-evar resolution made that new

evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.

See comments on #4484 for details.

4 files changed, 71 insertions, 12 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index faba5c7563..521fa2247b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -183,22 +183,26 @@ type inference_flags = {
   expand_evars : bool
 }
 
+let frozen_holes (sigma, sigma') =
+  let fold evk _ accu = Evar.Set.add evk accu in
+  Evd.fold_undefined fold sigma Evar.Set.empty
+
 let pending_holes (sigma, sigma') =
   let fold evk _ accu =
     if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu
   in
   Evd.fold_undefined fold sigma' Evar.Set.empty
 
-let apply_typeclasses env evdref pending fail_evar =
-  let filter_pending evk = Evar.Set.mem evk pending in
+let apply_typeclasses env evdref frozen fail_evar =
+  let filter_frozen evk = Evar.Set.mem evk frozen in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
-	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && filter_pending evk)
-              else (fun evk evi -> Typeclasses.no_goals evk evi && filter_pending evk))
+	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
+              else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
      ~split:true ~fail:fail_evar env !evdref;
   if Flags.is_program_mode () then (* Try optionally solving the obligations *)
     evdref := Typeclasses.resolve_typeclasses
-      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && filter_pending evk) ~split:true ~fail:false env !evdref
+      ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
 
 let apply_inference_hook hook evdref pending =
   evdref := Evar.Set.fold (fun evk sigma ->
@@ -219,9 +223,9 @@ let apply_heuristics env evdref fail_evar =
   with e when Errors.noncritical e ->
     let e = Errors.push e in if fail_evar then iraise e
 
-let check_typeclasses_instances_are_solved env current_sigma pending =
+let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env (ref current_sigma) pending true
+  apply_typeclasses env (ref current_sigma) frozen true
 
 let check_extra_evars_are_solved env current_sigma pending =
   Evar.Set.iter
@@ -233,26 +237,28 @@ let check_extra_evars_are_solved env current_sigma pending =
 	| _ ->
 	    error_unsolvable_implicit loc env current_sigma evk None) pending
 
-let check_evars_are_solved env current_sigma pending =
-  check_typeclasses_instances_are_solved env current_sigma pending;
+let check_evars_are_solved env current_sigma frozen pending =
+  check_typeclasses_instances_are_solved env current_sigma frozen;
   check_problems_are_solved env current_sigma;
   check_extra_evars_are_solved env current_sigma pending
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars flags env current_sigma pending =
+  let frozen = frozen_holes pending in
   let pending = pending_holes pending in
   let evdref = ref current_sigma in
-  if flags.use_typeclasses then apply_typeclasses env evdref pending false;
+  if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
     apply_inference_hook (Option.get flags.use_hook env) evdref pending;
   if flags.use_unif_heuristics then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env !evdref pending;
+  if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
   !evdref
 
 let check_evars_are_solved env current_sigma pending =
+  let frozen = frozen_holes pending in
   let pending = pending_holes pending in
-  check_evars_are_solved env current_sigma pending
+  check_evars_are_solved env current_sigma frozen pending
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
   let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/closed/3848.v
index a03e8ffdab..a03e8ffdab 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/closed/3848.v
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v
new file mode 100644
index 0000000000..3cdc4ada02
--- /dev/null
+++ b/test-suite/bugs/closed/4256.v
@@ -0,0 +1,43 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Global Set Universe Polymorphism.
+Monomorphic Universe i.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+Notation "-1" := (trunc_S minus_two) (at level 0).
+
+Class IsPointed (A : Type) := point : A.
+Arguments point A {_}.
+
+Record pType :=
+  { pointed_type : Type ;
+    ispointed_type : IsPointed pointed_type }.
+Coercion pointed_type : pType >-> Sortclass.
+Existing Instance ispointed_type.
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+
+
+Record ooGroup :=
+  { classifying_space : pType@{i} }.
+
+Definition group_loops (X : pType)
+: ooGroup.
+Proof.
+  (** This works: *)
+  pose (x0 := point X).
+  pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)).
+  clear H x0.
+  (** But this doesn't: *)
+  pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v
new file mode 100644
index 0000000000..f988539d62
--- /dev/null
+++ b/test-suite/bugs/closed/4484.v
@@ -0,0 +1,10 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Class A := {}.
+Axiom foo : forall {ac : A}, bool.
+Lemma bar (ac : A) : True.
+Check (match foo as k return foo = k -> True with
+       | true => _
+       | false => _
+       end eq_refl).