rm problematic variables under evars for evar instantiation + shelve new variable when instantiating old shelved variable with the new one in evarsolve/instantiate_evar

Author: Tragicus

dev/ci/user-overlays/19822-Tragicus-evd-inst.sh

@@ -0,0 +1 @@
+overlay hott https://github.com/Tragicus/Coq-HoTT rocq19822 19822

pretyping/evarsolve.ml

@@ -1586,6 +1586,10 @@ let instantiate_evar unify flags env evd evk body =
   let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in
   let flags = { flags with allowed_evars } in
   let evd' = check_evar_instance unify flags env evd evk body in
+  let evd' = try
+      let evk' = fst (EConstr.destEvar evd' (fst (EConstr.decompose_app evd' body))) in
+      if List.mem evk (Evd.shelf evd') then Evd.shelve evd' [evk'] else evd'
+    with DestKO -> evd' in
   Evd.define evk body evd'
 
 (* We try to instantiate the evar assuming the body won't depend
@@ -1760,6 +1764,20 @@ let rec invert_definition unify flags choose imitate_defs
           map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1)
                                         imitate envk t
         with _ -> progress := p; imitate envk (whd_beta env' !evdref t))
+    | App (f, args) when EConstr.isEvar !evdref f ->
+        progress := true;
+        (* Tries to imitate the arguments. If this fails, i is Some i' with i' the index of the last argument we fail to imitate *)
+        let i, args' = Array.fold_left_map_i (fun i k a ->
+          try let a' = imitate envk a in (k, a')
+          with ex -> (Some i, a)) None args in
+        (match i with
+        | None ->
+          let f' = imitate envk f in
+          if f' == f && Array.for_all2 (==) args args' then t else EConstr.mkApp (f', args')
+        | Some i ->
+          let args, args' = Array.chop (i+1) args in
+          let evd, e = Evardefine.evar_absorb_arguments env !evdref (EConstr.destEvar !evdref f) (Array.to_list args) in
+          evdref := evd; imitate envk (EConstr.mkApp (EConstr.mkEvar e, args')))
     | _ ->
         progress := true;
         match

test-suite/bugs/bug_3209.v

@@ -27,9 +27,11 @@ Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop.
 
 (* This used to fail with a Not_found, we fail more graciously but a
    heuristic could be implemented, e.g. in some smart occur-check
-   function, to find a solution of then form ?P := fun _ => ?P' *)
+   function, to find a solution of then form ?P := fun _ => ?P'
 
-Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)).
+   Well, now we do.*)
+
+Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)).
 
 (* This works and tells which solution we could have inferred *)