[evarconv] Handle frozen evars in solve_unif_constraints_with_heuristics

2 files changed, 39 insertions, 24 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 65ccfc641f..748143cad5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1545,7 +1545,6 @@ let is_beyond_capabilities = function
   | CannotSolveConstraint (pb,ProblemBeyondCapabilities) -> true
   | _ -> false
 
-(* TODO frozen *)
 let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   let t1 = apprec_nohdbeta flags env evd (whd_head_evar evd t1) in
   let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
@@ -1558,7 +1557,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
                                 Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match EConstr.kind evd term1, EConstr.kind evd term2 with
-  | Evar (evk1,args1), (Rel _|Var _) when app_empty
+  | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty
+      && not (is_frozen flags ev1)
       && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a)
         (remove_instance_local_defs evd evk1 args1) ->
       (* The typical kind of constraint coming from pattern-matching return
@@ -1568,8 +1568,9 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
       | None ->
          let reason = ProblemBeyondCapabilities in
          UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
-  | (Rel _|Var _), Evar (evk2,args2) when app_empty
-      && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
+  | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty
+    && not (is_frozen flags ev2)
+    && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
         (remove_instance_local_defs evd evk2 args2) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
@@ -1589,28 +1590,29 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
       Success (solve_refl ~can_drop:true f flags env evd
                  (position_problem true pbty) evk1 args1 args2)
   | Evar ev1, Evar ev2 when app_empty ->
+    (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *)
       Success (solve_evar_evar ~force:true
                  (evar_define evar_unify flags ~choose:true)
                  evar_unify flags env evd
                  (position_problem true pbty) ev1 ev2)
-  | Evar ev1,_ when Array.length l1 <= Array.length l2 ->
+  | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
       (* and otherwise second-order matching *)
       ise_try evd
         [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2);
          (fun evd ->
            second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)]
-  | _,Evar ev2 when Array.length l2 <= Array.length l1 ->
+  | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 ->
       (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
       (* and otherwise second-order matching *)
       ise_try evd
         [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1);
          (fun evd ->
            second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)]
-  | Evar ev1,_ ->
+  | Evar ev1,_ when not (is_frozen flags ev1) ->
       (* Try second-order pattern-matching *)
       second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2
-  | _,Evar ev2 ->
+  | _,Evar ev2 when not (is_frozen flags ev2) ->
       (* Try second-order pattern-matching *)
       second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1
   | _ ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ffb083e768..cdaf66f119 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1294,24 +1294,30 @@ let preferred_orientation evd evk1 evk2 =
   else if is_obligation_evar evd evk2 then false
   else true
 
-(** Precondition evk1 is not frozen, evk2 might be. *)
 let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env evd in
+  let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in
   let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in
   if preferred_orientation evd evk1 evk2 then
-    try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
-    with CannotProject (evd,ev2) when not frozen_ev2 ->
-    try solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
-    with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
-  else
-    try if not frozen_ev2 then
+    try if not frozen_ev1 then
+        solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
+      else raise (CannotProject (evd,ev2))
+    with CannotProject (evd,ev2) ->
+      try if not frozen_ev2 then
           solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
         else raise (CannotProject (evd,ev1))
+      with CannotProject (evd,ev1) ->
+        add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
+  else
+    try if not frozen_ev2 then
+        solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
+      else raise (CannotProject (evd,ev1))
     with CannotProject (evd,ev1) ->
-    try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
+    try if not frozen_ev1 then
+        solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
+      else raise (CannotProject (evd,ev2))
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
+      add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 (** Precondition: evk1 is not frozen *)
 let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
@@ -1361,7 +1367,7 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
   let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
   | None -> false
   | Some cstr ->
-    try ignore (Evd.add_universe_constraints !evdref cstr); true
+    try evdref := Evd.add_universe_constraints !evdref cstr; true
     with UniversesDiffer -> false
   in
   if Array.equal eq_constr argsv1 argsv2 then !evdref else
@@ -1373,15 +1379,22 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
   let candidates = filter_candidates evd evk untypedfilter NoUpdate in
   let filter = closure_of_filter evd evk untypedfilter in
   let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
-  if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd' else
+  let frozen = Evar.Set.mem evk flags.frozen_evars in
+  if Evar.equal (fst ev1) evk && (frozen || can_drop) then
+    (* No refinement needed *) evd'
+  else
     (* either progress, or not allowed to drop, e.g. to preserve possibly *)
     (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
     (* if e can depend on x until ?y is not resolved, or, conversely, we *)
     (* don't know if ?y has to be unified with ?y, until e is resolved *)
-  let argsv2 = restrict_instance evd' evk filter argsv2 in
-  let ev2 = (fst ev1,argsv2) in
-  (* Leave a unification problem *)
-  add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd'
+  if frozen then
+    (* We cannot prune a frozen evar *)
+    add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd
+  else
+    let argsv2 = restrict_instance evd' evk filter argsv2 in
+    let ev2 = (fst ev1,argsv2) in
+    (* Leave a unification problem *)
+    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd'
 
 (* If the evar can be instantiated by a finite set of candidates known
    in advance, we check which of them apply *)