refold before evar instantiation

Until now, the algorithm unfolded terms blindly and instantiated an evar with whatever term was on the other side. Now, we remember the terms from the initial unification problem, and whenever we reach a problem of the form `?e = t`, we replace `t` with its initial version.

Author: Tragicus

pretyping/evarconv.ml

@@ -704,10 +704,11 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
         let term1 = apprec_nohdbeta flags env evd term1 in
         let term2 = apprec_nohdbeta flags env evd term2 in
         let default () =
+          let hd1 = (whd_nored_state env evd (term1,Stack.empty)) in
+          let hd2 = (whd_nored_state env evd (term2,Stack.empty)) in
         match
           evar_eqappr_x flags env evd pbty (Cs_keys_cache.empty ()) None
-            (whd_nored_state env evd (term1,Stack.empty))
-            (whd_nored_state env evd (term2,Stack.empty))
+            (hd1, hd2) hd1 hd2
         with
         | UnifFailure _ as x ->
            if Retyping.is_term_irrelevant env evd term1 ||
@@ -743,8 +744,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     keys (* canonical structure keys cache *)
-    lastUnfolded (* tells which side was last unfolded, if any *)
-    (term1, sk1 as appr1) (term2, sk2 as appr2) =
+    lastUnfolded (* tells which side was last unfolded, if any, where `true` means RHS. *)
+    hds (term1, sk1 as appr1) (term2, sk2 as appr2) =
   let quick_fail i = (* not costly, loses info *)
     UnifFailure (i, NotSameHead)
   in
@@ -781,8 +782,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
       flags.open_ts env' evd (c'1, Stack.empty) in
     let out2 = whd_nored_state env' evd
       (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty) in
-    if onleft then evar_eqappr_x flags env' evd CONV keys None out1 out2
-    else evar_eqappr_x flags env' evd CONV (Cs_keys_cache.flip keys) None out2 out1
+    if onleft then evar_eqappr_x flags env' evd CONV keys None (out1, out2) out1 out2
+    else evar_eqappr_x flags env' evd CONV (Cs_keys_cache.flip keys) None (out2, out1) out2 out1
   in
   let rigids env evd sk term sk' term' =
     let nargs = Stack.args_size sk in
@@ -822,8 +823,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
        3.  reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *)
     let switch f a b = if l2r then f a b else f b a in
     let delta i =
-      switch (evar_eqappr_x flags env i pbty keys None) apprF
-        (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vskM)
+      let vskM = Option.get (eval_flexible_term flags.open_ts env evd (fst vskM) (snd vskM)) in
+      let apprM' = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vskM in
+      (* We cheat here. Unfolding here means that we should not go back to the heads
+        when rediscovering the problem ?e=t, so we put the unfolded term in place of the
+        head. *)
+      let hds = (apprM', apprM') in
+      switch (evar_eqappr_x flags env i pbty keys None hds) apprF apprM'
     in
     let default i = ise_try i [miller l2r ev apprF apprM;
                                consume l2r apprF apprM;
@@ -844,8 +850,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                   let apprM' =
                     whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (termM',skM)
                   in
+                  (* We cheat here. Unfolding here means that we should not go back to the heads
+                     when rediscovering the problem ?e=t, so we put the unfolded term in place of the
+                     head. *)
+                  let hds = if l2r then (fst hds, apprM') else (apprM', snd hds) in
                   let delta' i =
-                    switch (evar_eqappr_x flags env i pbty keys None) apprF apprM'
+                    switch (evar_eqappr_x flags env i pbty keys None hds) apprF apprM'
                   in
                   fun i -> ise_try i [miller l2r ev apprF apprM';
                                    consume l2r apprF apprM'; delta']
@@ -900,7 +910,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                      UnifFailure (evd,OccurCheck (fst ev,tR)))])
             ev lF tR evd
   in
-  let first_order env i t1 t2 sk1 sk2 =
+  let first_order env i t1 t2 sk1 sk2 hds =
     (* Try first-order unification *)
     match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
     | None, Success i' ->
@@ -912,7 +922,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                           (position_problem true pbty,destEvar i' ev1',term2)
        else
          (* HH: Why not to drop sk1 and sk2 since they unified *)
-         evar_eqappr_x flags env evd pbty keys None
+         evar_eqappr_x flags env evd pbty keys None hds
                        (ev1', sk1) (term2, sk2)
     | Some (r,[]), Success i' ->
        (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
@@ -922,7 +932,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
          solve_simple_eqn (conv_fun evar_conv_x) flags env i'
                           (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r))
        else
-         evar_eqappr_x flags env evd pbty keys None
+         evar_eqappr_x flags env evd pbty keys None hds
                        (ev2', sk1) (term2, sk2)
     | Some ([],r), Success i' ->
        (* Symmetrically *)
@@ -934,7 +944,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                           (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r))
        else
          (* HH: Why not to drop sk1 and sk2 since they unified *)
-         evar_eqappr_x flags env evd pbty keys None
+         evar_eqappr_x flags env evd pbty keys None hds
                           (ev1', sk1) (term2, sk2)
     | None, (UnifFailure _ as x) ->
        (* sk1 and sk2 have no common outer part *)
@@ -1007,6 +1017,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
   match (flex_kind_of_term flags env evd term1 sk1,
          flex_kind_of_term flags env evd term2 sk2) with
     | Flexible (sp1,al1), Flexible (sp2,al2) ->
+        let k1 = if lastUnfolded = Some true then let (t, sk) = fst hds in flex_kind_of_term flags env evd t sk else Flexible (sp1, al1) in
+        let k2 = if lastUnfolded = Some false then let (t, sk) = snd hds in flex_kind_of_term flags env evd t sk else Flexible (sp2, al2) in
+        begin match (k1, k2) with
+        | Flexible ev1, MaybeFlexible v2 -> flex_maybeflex true ev1 appr1 (snd hds) (snd hds)
+        | MaybeFlexible v1, Flexible ev2 -> flex_maybeflex false ev2 appr2 (fst hds) (fst hds)
+        | _, Rigid | Rigid, _ -> anomaly (Pp.str "flexible terms cannot fold to rigid ones")
+        | _ ->
       (* Notations:
          - "sk" is a stack (or, more abstractly, an evaluation context, written E)
          - "ev" is an evar "?ev", more precisely an evar ?n with an instance inst
@@ -1018,7 +1035,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
            1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂]
              recursively solve E2[?n[inst]] = E'2[redex]
            2. fails if neither E₁ nor E₂ is a prefix of the other *)
-        let f1 i = first_order env i term1 term2 sk1 sk2
+        let f1 i = first_order env i term1 term2 sk1 sk2 hds
         and f2 i =
           if Evar.equal sp1 sp2 then
             match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with
@@ -1046,12 +1063,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           | UnifFailure _ -> quick_fail i
         in
         ise_try evd [f1; f2; f3; f4; f5]
+        end
 
     | Flexible ev1, MaybeFlexible v2 ->
-      flex_maybeflex true ev1 appr1 appr2 v2
+      flex_maybeflex true ev1 appr1 appr2 (snd hds)
 
     | MaybeFlexible vsk1, Flexible ev2 ->
-      flex_maybeflex false ev2 appr2 appr1 vsk1
+      flex_maybeflex false ev2 appr2 appr1 (fst hds)
 
     | MaybeFlexible (v1', sk1' as vsk1'), MaybeFlexible (v2', sk2' as vsk2') -> begin
         match EConstr.kind evd term1, EConstr.kind evd term2 with
@@ -1071,7 +1089,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         and f2 i =
           let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1'
           and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2'
-          in evar_eqappr_x flags env i pbty keys None out1 out2
+          in evar_eqappr_x flags env i pbty keys None hds out1 out2
         in
         ise_try evd [f1; f2]
 
@@ -1083,7 +1101,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           and f2 i =
             let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk1'
             and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i vsk2'
-            in evar_eqappr_x flags env i pbty keys None out1 out2
+            in evar_eqappr_x flags env i pbty keys None hds out1 out2
           in
             ise_try evd [f1; f2]
 
@@ -1095,7 +1113,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           in
             (match res with
             | Some (f1,args1) ->
-              evar_eqappr_x flags env evd pbty keys None (f1,Stack.append_app args1 sk1)
+              evar_eqappr_x flags env evd pbty keys None hds (f1,Stack.append_app args1 sk1)
                 appr2
             | None -> UnifFailure (evd,NotSameHead))
 
@@ -1106,7 +1124,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           in
             (match res with
             | Some (f2,args2) ->
-              evar_eqappr_x flags env evd pbty keys None appr1 (f2,Stack.append_app args2 sk2)
+              evar_eqappr_x flags env evd pbty keys None hds appr1 (f2,Stack.append_app args2 sk2)
             | None -> UnifFailure (evd,NotSameHead))
 
         | _, _ ->
@@ -1169,14 +1187,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
           ise_try i [
             (fun i ->
               if b || !no_cs1 then
-                evar_eqappr_x flags env i pbty keys (Some false)
+                evar_eqappr_x flags env i pbty keys (Some false) hds
                   (whd_betaiota_deltazeta_for_iota_state
                      flags.open_ts env i vsk1')
                   appr2
               else quick_fail i);
             fun i ->
               if b then quick_fail i else
-              evar_eqappr_x flags env i pbty keys (Some true) appr1
+              evar_eqappr_x flags env i pbty keys (Some true) hds appr1
                 (whd_betaiota_deltazeta_for_iota_state
                    flags.open_ts env i vsk2')]
         in
@@ -1195,8 +1213,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
            (* When in modulo_betaiota = false case, lambda's are not reduced *)
            (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
 
-    | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
-    | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
+    | Flexible ev1, Rigid ->
+        let (t2, sk2) as appr2 = snd hds in
+        begin match flex_kind_of_term flags env evd t2 sk2 with
+        | Flexible ev2 -> anomaly (Pp.str "rigid terms can not fold to flexible ones")
+        | MaybeFlexible v2 -> flex_maybeflex true ev1 appr1 appr2 appr2
+        | Rigid -> flex_rigid true ev1 appr1 appr2
+        end
+    | Rigid, Flexible ev2 ->
+        let (t1, sk1) as appr1 = fst hds in
+        begin match flex_kind_of_term flags env evd t1 sk1 with
+        | Flexible ev1 -> anomaly (Pp.str "rigid terms can not fold to flexible ones")
+        | MaybeFlexible v1 -> flex_maybeflex false ev2 appr2 appr1 appr1
+        | Rigid -> flex_rigid false ev2 appr2 appr1
+        end
 
     | MaybeFlexible vsk1', Rigid ->
         let f3 i =
@@ -1206,7 +1236,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              | Inl x -> x
              | Inr _ -> UnifFailure (i,NoCanonicalStructure)
         and f4 i =
-          evar_eqappr_x flags env i pbty keys (Some false)
+          evar_eqappr_x flags env i pbty keys (Some false) hds
             (whd_betaiota_deltazeta_for_iota_state
                flags.open_ts env i vsk1')
             appr2
@@ -1221,7 +1251,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
              | Inl x -> x
              | Inr _ -> UnifFailure (i,NoCanonicalStructure)
         and f4 i =
-          evar_eqappr_x flags env i pbty keys (Some true) appr1
+          evar_eqappr_x flags env i pbty keys (Some true) hds appr1
             (whd_betaiota_deltazeta_for_iota_state
                flags.open_ts env i vsk2')
         in

pretyping/evarconv.mli

@@ -159,7 +159,7 @@ module Cs_keys_cache : sig type t end
 val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
   env -> evar_map -> conv_pb ->
   Cs_keys_cache.t ->
-  bool option -> state -> state ->
+  bool option -> (state * state) -> state -> state ->
       Evarsolve.unification_result
 
 val occur_rigidly : Evarsolve.unify_flags ->

test-suite/success/evars.v

@@ -433,3 +433,11 @@ Fail Type let x := _ in
        let t := type of x in
        unify x (abs t);
      exact 0).
+
+(* Check that evars are instantiated with least unfolded terms *)
+Module TestFold.
+Structure S := {T : Type}.
+Definition nat' : Type := nat.
+Canonical nat'_S := {| T := nat' |}.
+Check (eq_refl : (fun x => (id x, x)) _ = (nat', T _)).
+End TestFold.