Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_eqn).

The bug was that an assumption could be interpreted as a local
definition and wrongly expanded.

It triggered rarely because it involved mixing let-ins and
local assumptions + imitation under binders.

2 files changed, 12 insertions, 1 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de41c8f22f..c58ebe1bbd 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1576,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs
     match EConstr.kind !evdref t with
     | Rel i when i>k ->
         let open Context.Rel.Declaration in
-        (match Environ.lookup_rel (i-k) env' with
+        (match Environ.lookup_rel i env' with
         | LocalAssum _ -> project_variable (RelAlias (i-k))
         | LocalDef (_,b,_) ->
           try project_variable (RelAlias (i-k))
diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v
new file mode 100644
index 0000000000..93ba6f17e0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12348.v
@@ -0,0 +1,11 @@
+(* Was raising an anomaly before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := _ in
+      (fun n : nat => 0 : X) : _.
+
+(* Was raising an ill-typed instance error before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := true in
+      (fun n : nat => 0 : X) : _.