Unification constraint handling (#4763, #5149)

Refine fix for bug #4763, fixing #5149

Tactic [Refine.solve_constraints] and global option

Adds a new multi-goal tactic [Refine.solve_constraints] that forces solving of
unification constraints and evar candidates to be solved. run_tactic now calls
[solve_constraints] at every [.], preserving (mostly) the 8.4/8.5 behavior of tactics.
The option allows to unset the forced solving unification constraints at
each ".", letting the user control the places where the use of
heuristics is done.

Fix test-suite files too.

12 files changed, 98 insertions, 21 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 855235d2b..c01879765 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1157,10 +1157,6 @@ let tclLIFT = Proof.lift
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
 
-
-
-
-
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 725445251..90be2f90a 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -373,7 +373,6 @@ val mark_as_unsafe : unit tactic
     with given up goals cannot be closed. *)
 val give_up : unit tactic
 
-
 (** {7 Control primitives} *)
 
 (** [tclPROGRESS t] checks the state of the proof after [t]. It it is
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d0318fb5f..e6498e02b 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -370,6 +370,11 @@ TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ]
 END
 
+(* Solve unification constraints using heuristics or fail if any remain *)
+TACTIC EXTEND solve_constraints
+[ "solve_constraints" ] -> [ Refine.solve_constraints ]
+END
+
 (**********************************************************************)
 (* Inversion lemmas (Leminv)                                          *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index cec9f700a..fc63015a8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1301,7 +1301,6 @@ let w_merge env with_types flags (evd,metas,evars) =
 	      if is_mimick_head flags.modulo_delta f then
 		let evd' =
 		  mimick_undefined_evar evd flags f (Array.length cl) evk in
-		(* let evd' = Evarconv.consider_remaining_unif_problems env evd' in *)
 		  w_merge_rec evd' metas evars eqns
 	      else
 		let evd' = 
@@ -1397,8 +1396,7 @@ let w_merge env with_types flags (evd,metas,evars) =
                 (* Assign evars in the order of assignments during unification *)
                 (List.rev evars) []
   in
-    if with_types then check_types res
-    else res
+  if with_types then check_types res else res
 
 let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
   let metas,evd = retract_coercible_metas evd in
@@ -1456,7 +1454,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 =
   let subst = Array.fold_left2 fold_subst subst l1 l2 in
   let evd = w_merge env true flags.merge_unify_flags subst in
   try_resolve_typeclasses env evd flags.resolve_evars
-    (mkApp(f1,l1)) (mkApp(f2,l2))
+                          (mkApp(f1,l1)) (mkApp(f2,l2))
 
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
@@ -1885,21 +1883,14 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
     error_wrong_abstraction_type env evd'
       (Evd.meta_name evd p) pred typp predtyp;
   w_merge env false flags.merge_unify_flags
-    (evd',[p,pred,(Conv,TypeProcessed)],[])
-
-  (* let evd',metas,evars =  *)
-  (*   try unify_0 env evd' CUMUL flags predtyp typp  *)
-  (*   with NotConvertible -> *)
-  (*     error_wrong_abstraction_type env evd *)
-  (*       (Evd.meta_name evd p) pred typp predtyp *)
-  (* in *)
-  (*   w_merge env false flags (evd',(p,pred,(Conv,TypeProcessed))::metas,evars) *)
+          (evd',[p,pred,(Conv,TypeProcessed)],[])
 
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
   w_merge env false flags.merge_unify_flags
-    (evd,[p,pred,(Conv,TypeProcessed)],[])
+          (evd,[p,pred,(Conv,TypeProcessed)],[])
+
 
 let secondOrderAbstractionAlgo dep =
   if dep then secondOrderDependentAbstraction else secondOrderAbstraction
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a3ece1913..9c71e107c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -13,6 +13,17 @@ open Entries
 open Environ
 open Evd
 
+let use_unification_heuristics_ref = ref true
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname = "Unification heuristics are applied at every .";
+  Goptions.optkey = ["Use";"Unification";"Heuristics"];
+  Goptions.optread = (fun () -> !use_unification_heuristics_ref);
+  Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a);
+}
+
+let use_unification_heuristics () = !use_unification_heuristics_ref
+
 let refining = Proof_global.there_are_pending_proofs
 let check_no_pending_proofs = Proof_global.check_no_pending_proof
 
@@ -119,6 +130,11 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
       | Vernacexpr.SelectAll -> tac
     in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
+    in
     let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
     let () =
       match info_lvl with
diff --git a/proofs/refine.ml b/proofs/refine.ml
index e5114a2ec..2f2142890 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -149,3 +149,14 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   } in
   refine ?unsafe f
 end }
+
+(** {7 solve_constraints}
+
+  Ensure no remaining unification problems are left. Run at every "." by default. *)
+
+let solve_constraints =
+  let open Proofview in
+  tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
+   try let sigma = Evarconv.consider_remaining_unif_problems env sigma in
+       Unsafe.tclEVARSADVANCE sigma
+   with e -> tclZERO e
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3d140f036..a44632eff 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -43,3 +43,8 @@ val with_type : Environ.env -> Evd.evar_map ->
 val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)
+
+(** {7 Unification constraint handling} *)
+
+val solve_constraints : unit tactic
+(** Solve any remaining unification problems, applying heuristics. *)
diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 0be859edd..9fddede7e 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
    leave P as subgoal or choose itself one solution *)
 
-intros. refine (Cons (cast H _ y)).
\ No newline at end of file
+  intros. Fail refine (Cons (cast H _ y)).
+  Unset Use Unification Heuristics. (* Keep the unification constraint around *)
+  refine (Cons (cast H _ y)).
+  intros.
+  refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index 495e67e09..f2cd41203 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -650,4 +650,5 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
 
   Grab Existential Variables.
   subst_body; simpl.
-  refine (all_behead (projT2 _)).
+  Fail refine (all_behead (projT2 _)).
+  Unset Use Unification Heuristics. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce64..afe8c62ed 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
 Goal exists x, x.
+Unset Use Unification Heuristics.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 000000000..01b9d158f
--- /dev/null
+++ b/test-suite/bugs/closed/5149.v
@@ -0,0 +1,47 @@
+Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x.
+intros.
+eexists.
+rewrite <- H.
+eassumption.
+Qed.
+
+Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) 
+            (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : 
+flat_type -> Type)
+            (v v' : interp_flat_type1 t'),
+    v = v' ->
+    forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0)
+           (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> 
+interp_flat_type0 t0)
+           (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t))
+           (x' : interp_flat_type1 (Tbase t)) (T : Type)
+           (flatten_binding_list : forall t0 : flat_type,
+               interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T)
+           (P : T -> list T -> Prop) (prod : Type -> Type -> Type)
+           (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) 
+(interp_flat_type1 (Tbase x0)) -> T)
+           (pair : forall A B : Type, A -> B -> prod A B),
+      P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x'))
+        (flatten_binding_list t' (SmartVarVar t' v') v) ->
+      (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 
+t'0)
+              (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)),
+          P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 
+x'0))
+            (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf 
+(Tbase t0) x0 = x'0) ->
+      interpf (Tbase t) x = x'.
+Proof.
+  intros ?????????????????????? interpf_SmartVarVar.
+  solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail 
+"too early".
+  Undo.
+  (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
+  Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
+  solve [eapply interpf_SmartVarVar; subst; eassumption].
+  Undo.
+  Unset Use Unification Heuristics.
+  (* User control of when constraints are solved *)
+  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
+Qed.
+
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0..c7fb82ada 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
 (* Set Printing Existential Instances. *)
+Unset Use Unification Heuristics.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =