Merge PR coq#19769: Fixes coq#17314: Tactic unification may leave unb…

…ound de Bruijn indices when unifying holes under a "fun"

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

doc/changelog/04-tactics/19769-master+fix17314-wrong-env-unif-meta-under-lambda.rst

@@ -0,0 +1,7 @@
+- **Fixed:**
+  Unbound variables were sometimes generated when a metavariable of a
+  theorem given to :tacn:`apply` occurred in the type of the theorem
+  under a :n:`fun`
+  (`#19769 <https://github.com/coq/coq/pull/19769>`_,
+  fixes `#17314 <https://github.com/coq/coq/issues/17314>`_,
+  by Hugo Herbelin).

pretyping/unification.ml

@@ -1846,7 +1846,7 @@ let w_merge env with_types flags (substn : subst0) =
                 in
                 w_merge_rec metas0 evd' metas evars' eqns
           | _ ->
-              let evd', metas0, rhs'' = pose_all_metas_as_evars ~metas:metas0 curenv evd rhs' in
+              let evd', metas0, rhs'' = pose_all_metas_as_evars ~metas:metas0 env evd rhs' in
               let evd' =
                 try solve_simple_evar_eqn eflags curenv evd' ev rhs''
                 with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'')

test-suite/bugs/bug_17314.v

@@ -0,0 +1,13 @@
+Definition arrow_apply (f : Prop -> Prop) := True -> f True. (* We need True-> to trigger a unification in an extended context *)
+
+Definition something (x : Prop) := arrow_apply (fun _ => x).
+
+Axiom trivial: forall l1: Prop, something l1 -> something l1.
+
+Lemma t : exists f, arrow_apply f.
+eexists.
+unshelve apply trivial.
+(* was giving "something ?l1@{t:=_UNBOUND_REL_1}" while the evar is not supposed to depend on t *)
+(* so, we check that, indeed, t is not here *)
+match goal with [ H : True |- _ ] => fail 1 | _ => idtac end.
+Abort.