Fixes #7780 (missing lift in expanding alias under a binder in unification).

2 files changed, 17 insertions, 1 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aefae1ecc2..8afb9b9421 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -929,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
     with Not_found ->
       match expand_alias_once evd aliases t with
       | None -> raise Not_found
-      | Some c -> aux k c in
+      | Some c -> aux k (lift k c) in
   try
     let c = aux 0 c_in_env_extended_with_k_binders in
     Invertible (UniqueProjection (c,!effects))
diff --git a/test-suite/bugs/closed/7780.v b/test-suite/bugs/closed/7780.v
new file mode 100644
index 0000000000..2318f4d6ec
--- /dev/null
+++ b/test-suite/bugs/closed/7780.v
@@ -0,0 +1,16 @@
+(* A lift was missing in expanding aliases under binders for unification *)
+
+(* Below, the lift was missing while expanding the reference to
+   [mkcons] in [?N] which was under binder [arg] *)
+
+Goal forall T (t : T) (P P0 : T -> Set), option (option (list (P0 t)) -> option (list (P t))).
+  intros ????.
+  refine (Some
+            (fun rls
+             => let mkcons := ?[M] in
+                let default arg := ?[N] in
+                match rls as rls (* 2 *) return option (list (P ?[O])) with
+                | Some _ => None
+                | None => None
+                end)).
+Abort.