Replace `frozen` by `allowed` evars in evarconv, and delay them

This is a follow-up of #9062, which introduced a discrenpancy between
the two unification engines.

11 files changed, 70 insertions, 62 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fb149071c9..a8a3a21f4a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -546,7 +546,7 @@ let rewrite_core_unif_flags = {
   Unification.check_applied_meta_types = true;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
-  Unification.allowed_evars = Unification.AllowAll;
+  Unification.allowed_evars = Evarsolve.AllowAll;
   Unification.restrict_conv_on_strict_subterms = false;
   Unification.modulo_betaiota = false;
   Unification.modulo_eta = true;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 489e8de602..3dc00d195e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full
 let default_flags_of ?(subterm_ts=TransparentState.empty) ts =
   { modulo_betaiota = true;
     open_ts = ts; closed_ts = ts; subterm_ts;
-    frozen_evars = Evar.Set.empty; with_cs = true;
+    allowed_evars = AllowAll; with_cs = true;
     allow_K_at_toplevel = true }
 
 let default_flags env =
@@ -118,8 +118,6 @@ type flex_kind_of_term =
   | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *)
   | Flexible of EConstr.existential
 
-let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars
-
 let flex_kind_of_term flags env evd c sk =
   match EConstr.kind evd c with
     | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
@@ -128,8 +126,7 @@ let flex_kind_of_term flags env evd c sk =
        if flags.modulo_betaiota then MaybeFlexible c
        else Rigid
     | Evar ev ->
-       if is_frozen flags ev then Rigid
-       else Flexible ev
+       if is_evar_allowed flags (fst ev) then Flexible ev else Rigid
     | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid
     | Meta _ -> Rigid
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
@@ -192,11 +189,11 @@ let occur_rigidly flags env evd (evk,_) t =
           | Rigid _ as res -> res
           | Normal b -> Reducible
           | Reducible -> Reducible)
-    | Evar (evk',l as ev) ->
+    | Evar (evk',l) ->
       if Evar.equal evk evk' then Rigid true
-      else if is_frozen flags ev then
-        Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
-      else Reducible
+      else if is_evar_allowed flags evk' then
+        Reducible
+        else Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
     | Cast (p, _, _) -> aux p
     | Lambda (na, t, b) -> aux b
     | LetIn (na, _, _, b) -> aux b
@@ -458,7 +455,7 @@ let conv_fun f flags on_types =
   let typefn env evd pbty term1 term2 =
     let flags = { (default_flags env) with
       with_cs = flags.with_cs;
-      frozen_evars = flags.frozen_evars }
+      allowed_evars = flags.allowed_evars }
     in f flags env evd pbty term1 term2
   in
   let termfn env evd pbty term1 term2 =
@@ -500,7 +497,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
             (whd_nored_state env evd (term2,Stack.empty))
         in
           begin match EConstr.kind evd term1, EConstr.kind evd term2 with
-          | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+          | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
             (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
               (position_problem true pbty,ev,term2) with
               | UnifFailure (_,(OccurCheck _ | NotClean _)) ->
@@ -511,7 +508,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
                      Miller patterns *)
                 default ()
               | x -> x)
-          | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+          | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
             (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
               (position_problem false pbty,ev,term1) with
               | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
@@ -1206,14 +1203,14 @@ type occurrences_selection =
 
 let default_occurrence_selection = Unspecified Abstraction.Imitate
 
-let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat =
-  let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in
+let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat =
+  let flags = { (default_flags_of ~subterm_ts:ts ts) with allowed_evars } in
   match evar_conv_x flags env sigma CONV c pat with
   | Success sigma -> true, sigma
   | UnifFailure _ -> false, sigma
 
-let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n =
-  (default_occurrence_test ~frozen_evars ts,
+let default_occurrences_selection ?(allowed_evars=AllowAll) ts n =
+  (default_occurrence_test ~allowed_evars ts,
    List.init n (fun _ -> default_occurrence_selection))
 
 let apply_on_subterm env evd fixedref f test c t =
@@ -1554,7 +1551,7 @@ let second_order_matching_with_args flags env evd with_ho pbty ev l t =
   if with_ho then
     let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in
     let argoccs = default_evar_selection flags evd ev in
-    let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in
+    let test = default_occurrence_test ~allowed_evars:flags.allowed_evars flags.subterm_ts in
     let evd, b =
       try second_order_matching flags env evd ev (test,argoccs) t
       with PretypeError (_, _, NoOccurrenceFound _) -> evd, false
@@ -1582,8 +1579,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 as ev1), (Rel _|Var _) when app_empty
-      && not (is_frozen flags ev1)
+  | Evar (evk1,args1), (Rel _|Var _) when app_empty
+      && is_evar_allowed flags evk1
       && 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
@@ -1593,8 +1590,8 @@ 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 as ev2) when app_empty
-    && not (is_frozen flags ev2)
+  | (Rel _|Var _), Evar (evk2,args2) when app_empty
+    && is_evar_allowed flags evk2
     && 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
@@ -1620,24 +1617,24 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
                  (evar_define evar_unify flags ~choose:true)
                  evar_unify flags env evd
                  (position_problem true pbty) ev1 ev2)
-  | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 ->
+  | Evar ev1,_ when is_evar_allowed flags (fst 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 not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 ->
+  | _,Evar ev2 when is_evar_allowed flags (fst 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,_ when not (is_frozen flags ev1) ->
+  | Evar ev1,_ when is_evar_allowed flags (fst ev1) ->
       (* Try second-order pattern-matching *)
       second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2
-  | _,Evar ev2 when not (is_frozen flags ev2) ->
+  | _,Evar ev2 when is_evar_allowed flags (fst ev2) ->
       (* Try second-order pattern-matching *)
       second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1
   | _ ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 767a173131..9343be6484 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -105,11 +105,11 @@ val default_occurrence_selection : occurrence_selection
 type occurrences_selection =
   occurrence_match_test * occurrence_selection list
 
-val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test
+val default_occurrence_test : allowed_evars:Evarsolve.allowed_evars -> TransparentState.t -> occurrence_match_test
 
 (** [default_occurrence_selection n]
     Gives the default test and occurrences for [n] arguments *)
-val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) ->
+val default_occurrences_selection : ?allowed_evars:Evarsolve.allowed_evars (* By default, all *) ->
   TransparentState.t -> int -> occurrences_selection
 
 val second_order_matching : unify_flags -> env -> evar_map ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 989fb05c3d..9cf1e6fd6f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -25,14 +25,23 @@ open Reductionops
 open Evarutil
 open Pretype_errors
 
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
 type unify_flags = {
   modulo_betaiota: bool;
   open_ts : TransparentState.t;
   closed_ts : TransparentState.t;
   subterm_ts : TransparentState.t;
-  frozen_evars : Evar.Set.t;
+  allowed_evars : allowed_evars;
   allow_K_at_toplevel : bool;
-  with_cs : bool }
+  with_cs : bool
+}
+
+let is_evar_allowed flags evk = match flags.allowed_evars with
+| AllowAll -> true
+| AllowFun f -> f evk
 
 type unification_kind =
   | TypeUnification
@@ -1307,24 +1316,24 @@ let preferred_orientation evd evk1 evk2 =
 
 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
+  let allowed_ev1 = is_evar_allowed flags evk1 in
+  let allowed_ev2 = is_evar_allowed flags evk2 in
   if preferred_orientation evd evk1 evk2 then
-    try if not frozen_ev1 then
+    try if allowed_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
+      try if allowed_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
+    try if allowed_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 if not frozen_ev1 then
+    try if allowed_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) ->
@@ -1390,15 +1399,15 @@ 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
-  let frozen = Evar.Set.mem evk flags.frozen_evars in
-  if Evar.equal (fst ev1) evk && (frozen || can_drop) then
+  let allowed = is_evar_allowed flags evk in
+  if Evar.equal (fst ev1) evk && (not allowed || 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 *)
-  if frozen then
+  if not allowed then
     (* We cannot prune a frozen evar *)
     add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd
   else
@@ -1455,7 +1464,11 @@ let occur_evar_upto_types sigma n c =
 let instantiate_evar unify flags env evd evk body =
   (* Check instance freezing the evar to be defined, as
      checking could involve the same evar definition problem again otherwise *)
-  let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in
+  let allowed = match flags.allowed_evars with
+    | AllowAll -> fun evk' -> not (Evar.equal evk evk')
+    | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk'
+  in
+  let flags = { flags with allowed_evars = AllowFun allowed } in
   let evd' = check_evar_instance unify flags env evd evk body in
   Evd.define evk body evd'
 
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3fb80432ad..89e162937d 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,6 +16,10 @@ type alias
 
 val of_alias : alias -> EConstr.t
 
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
 type unify_flags = {
   modulo_betaiota : bool;
   (* Enable beta-iota reductions during unification *)
@@ -26,8 +30,8 @@ type unify_flags = {
   subterm_ts : TransparentState.t;
   (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
      unifications. *)
-  frozen_evars : Evar.Set.t;
-  (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *)
+  allowed_evars : allowed_evars;
+  (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *)
   allow_K_at_toplevel : bool;
   (* During higher-order unifications, allow to produce K-redexes: i.e. to produce
      an abstraction for an unused argument *)
@@ -41,6 +45,8 @@ type unification_result =
 
 val is_success : unification_result -> bool
 
+val is_evar_allowed : unify_flags -> Evar.t -> bool
+
 (** Replace the vars and rels that are aliases to other vars and rels by
    their representative that is most ancient in the context *)
 val expand_vars_in_term : env -> evar_map -> constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a26c981cb9..d63d367a84 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -252,10 +252,6 @@ let unify_r2l x = x
 let sort_eqns = unify_r2l
 *)
 
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
-
 type core_unify_flags = {
   modulo_conv_on_closed_terms : TransparentState.t option;
     (* What this flag controls was activated with all constants transparent, *)
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index f9a969a253..e3750f7d97 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -13,10 +13,6 @@ open EConstr
 open Environ
 open Evd
 
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
-
 type core_unify_flags = {
   modulo_conv_on_closed_terms : TransparentState.t option;
   use_metas_eagerly_in_conv_on_closed_terms : bool;
@@ -26,7 +22,7 @@ type core_unify_flags = {
   check_applied_meta_types : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
-  allowed_evars : allowed_evars;
+  allowed_evars : Evarsolve.allowed_evars;
   restrict_conv_on_strict_subterms : bool;
   modulo_betaiota : bool;
   modulo_eta : bool;
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index db76d08736..65a7a6c711 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -673,7 +673,7 @@ let fail_quick_core_unif_flags = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  allowed_evars = AllowAll;
+  allowed_evars = Evarsolve.AllowAll;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 784322679f..4cec72597a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = {
   check_applied_meta_types = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true;
-  allowed_evars = AllowAll;
+  allowed_evars = Evarsolve.AllowAll;
   restrict_conv_on_strict_subterms = false; (* Compat *)
   modulo_betaiota = false;
   modulo_eta = true;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d969dea19e..39589b2d11 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = {
   modulo_eta = false;
 }
 
-let auto_unif_flags ?(allowed_evars = AllowAll) st =
+let auto_unif_flags ?(allowed_evars = Evarsolve.AllowAll) st =
   let fl = auto_core_unif_flags st allowed_evars in
   { core_unify_flags = fl;
     merge_unify_flags = fl;
@@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
          if cl.cl_strict then
           let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in
           let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in
-          AllowFun allowed
-         else AllowAll
-      | _ -> AllowAll
-    with e when CErrors.noncritical e -> AllowAll
+          Evarsolve.AllowFun allowed
+         else Evarsolve.AllowAll
+      | _ -> Evarsolve.AllowAll
+    with e when CErrors.noncritical e -> Evarsolve.AllowAll
   in
   let tac_of_hint =
     fun (flags, h) ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b4def7bb51..cecb2df8e0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -105,7 +105,7 @@ let rewrite_core_unif_flags = {
   check_applied_meta_types = true;
   use_pattern_unification = true;
   use_meta_bound_pattern_unification = true;
-  allowed_evars = AllowAll;
+  allowed_evars = Evarsolve.AllowAll;
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = true;
@@ -130,7 +130,7 @@ let freeze_initial_evars sigma flags clause =
     if Evar.Map.mem evk initial then false
     else Evar.Set.mem evk (Lazy.force newevars)
   in
-  let allowed_evars = AllowFun allowed in
+  let allowed_evars = Evarsolve.AllowFun allowed in
   {flags with
     core_unify_flags = {flags.core_unify_flags with allowed_evars};
     merge_unify_flags = {flags.merge_unify_flags with allowed_evars};
@@ -187,7 +187,7 @@ let rewrite_conv_closed_core_unif_flags = {
 
   use_meta_bound_pattern_unification = true;
 
-  allowed_evars = AllowAll;
+  allowed_evars = Evarsolve.AllowAll;
 
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
@@ -221,7 +221,7 @@ let rewrite_keyed_core_unif_flags = {
 
   use_meta_bound_pattern_unification = true;
 
-  allowed_evars = AllowAll;
+  allowed_evars = Evarsolve.AllowAll;
 
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = true;