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

Author: herbelin

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))

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.