From 332c1ec46a86b363b8fa0c027dfe9efeb1baeae0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 30 Jan 2026 09:23:15 +0100
Subject: [PATCH] perf: specializer a little more courageously (#12239)

This PR reverts a lot of the changes done in #8308. We practically
encountered situations such as:
```
fun y (z) :=
  let x := inst
  mkInst x z
f y
```
Where the instance puller turns it into:
```
let x := inst
fun y (z) :=
  mkInst x z
f y
```
The current heuristic now discovers `x` being in scope at the call site
of `f` and being used under a binder in `y` and thus blocks pulling in
`x` to the specialization, abstracting over an instance.

According to @zwarich this was done at the time either due to observed
stack overflows or pulling in computation into loops. With the current
configuration for abstraction in specialization it seems rather unlikely
that we pull in a non trivial computation into a loop with this. We also
practically didn't observe stack overflows in our tests or benchmarks.
Cameron speculates that the issues he observed might've been fixed
otherwise by now.

Crucial note: Deciding not to abstract over ground terms *might* cause
us to pull in computationally intensive ground terms into a loop. We
could decide to weaken this to just instance terms though of course even
computing instances might end up being non-trivial.
---
 src/Lean/Compiler/LCNF/Closure.lean           |  14 +-
 stage0/src/stdlib_flags.h                     |   2 +
 tests/lean/run/do_for_loop_compiler_test.lean | 160 +++++++--------
 .../do_for_loop_levenstein_compiler_test.lean | 190 +++++++++---------
 4 files changed, 183 insertions(+), 183 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean
index de77803a2c..e13b88d2af 100644
--- a/src/Lean/Compiler/LCNF/Closure.lean
+++ b/src/Lean/Compiler/LCNF/Closure.lean
@@ -33,10 +33,6 @@ structure Context where
   Remark: the lambda lifting pass abstracts all `let`/`fun`-declarations.
   -/
   abstract : FVarId → Bool
-  /--
-  Indicates whether we are processing terms beneath a binder.
-  -/
-  isUnderBinder : Bool
 
 /--
 State for the `ClosureM` monad.
@@ -103,8 +99,7 @@ mutual
     match c with
     | .let decl k =>
       collectType decl.type
-      withReader (fun ctx => { ctx with isUnderBinder := ctx.isUnderBinder || decl.type.isForall })
-        do collectLetValue decl.value
+      collectLetValue decl.value
       collectCode k
     | .fun decl k | .jp decl k => collectFunDecl decl; collectCode k
     | .cases c =>
@@ -122,8 +117,7 @@ mutual
   partial def collectFunDecl (decl : FunDecl) : ClosureM Unit := do
     collectType decl.type
     collectParams decl.params
-    withReader (fun ctx => { ctx with isUnderBinder := true }) do
-      collectCode decl.value
+    collectCode decl.value
 
   /--
   Process the given free variable.
@@ -146,7 +140,7 @@ mutual
           modify fun s => { s with params := s.params.push param }
         else if let some letDecl ← findLetDecl? fvarId then
           collectType letDecl.type
-          if ctx.isUnderBinder || ctx.abstract letDecl.fvarId then
+          if ctx.abstract letDecl.fvarId then
             modify fun s => { s with params := s.params.push <| { letDecl with borrow := false } }
           else
             collectLetValue letDecl.value
@@ -162,7 +156,7 @@ mutual
 end
 
 def run (x : ClosureM α) (inScope : FVarId → Bool) (abstract : FVarId → Bool := fun _ => true) : CompilerM (α × Array Param × Array CodeDecl) := do
-  let (a, s) ← x { inScope, abstract, isUnderBinder := false } |>.run {}
+  let (a, s) ← x { inScope, abstract } |>.run {}
   -- If we've abstracted an fvar into a param, exclude its definition. Note that this still allows
   -- for other decls the removed decl depends upon to be included, but they will be removed later
   -- for having no users.
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..6c6b3bee8f 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update thy
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/do_for_loop_compiler_test.lean b/tests/lean/run/do_for_loop_compiler_test.lean
index 8b2117be83..08d4080e54 100644
--- a/tests/lean/run/do_for_loop_compiler_test.lean
+++ b/tests/lean/run/do_for_loop_compiler_test.lean
@@ -8,43 +8,43 @@ def List.newForIn (l : List α) (b : β) (kcons : α → (β → γ) → β →
 
 /--
 trace: [Compiler.saveMono] size: 7
-    def List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 l b : Nat :=
+    def List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b i;
-        let x := Nat.add _x.6 head.4;
-        let _x.7 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 tail.5 x;
-        return _x.7
+        let _x.2 := List.newForIn._at_.testing.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b i;
+        let x := Nat.add _x.5 head.3;
+        let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 tail.4 x;
+        return _x.6
 [Compiler.saveMono] size: 7
-    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.2 i l b : Nat :=
+    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 tail.1 i l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b i;
-        let x := Nat.add _x.6 head.4;
-        let _x.7 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i _x.1 tail.2 tail.5 x;
-        return _x.7
+        let _x.2 := List.newForIn._at_.testing.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b i;
+        let x := Nat.add _x.5 head.3;
+        let _x.6 := List.newForIn._at_.List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2.spec_2 i tail.1 tail.4 x;
+        return _x.6
 [Compiler.saveMono] size: 12
-    def List.newForIn._at_.testing.spec_1 _x.1 l b : Nat :=
+    def List.newForIn._at_.testing.spec_1 l b : Nat :=
       cases l : Nat
       | List.nil =>
         return b
-      | List.cons head.2 tail.3 =>
+      | List.cons head.1 tail.2 =>
+        let _x.3 := 1;
         let _x.4 := 10;
-        let _x.5 := Nat.sub _x.4 head.2;
-        let _x.6 := Nat.add _x.5 _x.1;
-        let _x.7 := 1;
-        let _x.8 := Nat.sub _x.6 _x.7;
-        let _x.9 := Nat.add head.2 _x.8;
-        let _x.10 := [] ◾;
-        let _x.11 := List.range'TR.go _x.1 _x.8 _x.9 _x.10;
-        let _x.12 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 _x.1 tail.3 head.2 _x.11 b;
-        return _x.12
+        let _x.5 := Nat.sub _x.4 head.1;
+        let _x.6 := Nat.add _x.5 _x.3;
+        let _x.7 := Nat.sub _x.6 _x.3;
+        let _x.8 := Nat.add head.1 _x.7;
+        let _x.9 := [] ◾;
+        let _x.10 := List.range'TR.go _x.3 _x.7 _x.8 _x.9;
+        let _x.11 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing.spec_1.spec_2 tail.2 head.1 _x.10 b;
+        return _x.11
 [Compiler.saveMono] size: 9
     def testing : Nat :=
       let x := 42;
@@ -55,7 +55,7 @@ trace: [Compiler.saveMono] size: 7
       let _x.5 := List.cons ◾ _x.3 _x.4;
       let _x.6 := List.cons ◾ _x.2 _x.5;
       let _x.7 := List.cons ◾ _x.1 _x.6;
-      let _x.8 := List.newForIn._at_.testing.spec_1 _x.1 _x.7 x;
+      let _x.8 := List.newForIn._at_.testing.spec_1 _x.7 x;
       return _x.8
 [Compiler.saveMono] size: 7
     def List.newForIn._at_.testing.spec_0 i kcontinue l b : Nat :=
@@ -90,34 +90,34 @@ def testing :=
 
 /--
 trace: [Compiler.saveMono] size: 7
-    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.2 i l b : Nat :=
+    def List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.1 i l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing2.spec_0 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b i;
-        let x := Nat.add _x.6 head.4;
-        let _x.7 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.2 i tail.5 x;
-        return _x.7
+        let _x.2 := List.newForIn._at_.testing2.spec_0 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b i;
+        let x := Nat.add _x.5 head.3;
+        let _x.6 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.1 i tail.4 x;
+        return _x.6
 [Compiler.saveMono] size: 14
-    def List.newForIn._at_.testing2.spec_0 _x.1 l b : Nat :=
+    def List.newForIn._at_.testing2.spec_0 l b : Nat :=
       cases l : Nat
       | List.nil =>
         return b
-      | List.cons head.2 tail.3 =>
+      | List.cons head.1 tail.2 =>
+        let _x.3 := 1;
         let _x.4 := 37;
         let x := Nat.add b _x.4;
         let _x.5 := 10;
-        let _x.6 := Nat.sub _x.5 head.2;
-        let _x.7 := Nat.add _x.6 _x.1;
-        let _x.8 := 1;
-        let _x.9 := Nat.sub _x.7 _x.8;
-        let _x.10 := Nat.add head.2 _x.9;
-        let _x.11 := [] ◾;
-        let _x.12 := List.range'TR.go _x.1 _x.9 _x.10 _x.11;
-        let _x.13 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 _x.1 tail.3 head.2 _x.12 x;
-        return _x.13
+        let _x.6 := Nat.sub _x.5 head.1;
+        let _x.7 := Nat.add _x.6 _x.3;
+        let _x.8 := Nat.sub _x.7 _x.3;
+        let _x.9 := Nat.add head.1 _x.8;
+        let _x.10 := [] ◾;
+        let _x.11 := List.range'TR.go _x.3 _x.8 _x.9 _x.10;
+        let _x.12 := List.newForIn._at_.testing.spec_0._at_.List.newForIn._at_.testing2.spec_0.spec_1 tail.2 head.1 _x.11 x;
+        return _x.12
 [Compiler.saveMono] size: 9
     def testing2 : Nat :=
       let x := 42;
@@ -128,7 +128,7 @@ trace: [Compiler.saveMono] size: 7
       let _x.5 := List.cons ◾ _x.3 _x.4;
       let _x.6 := List.cons ◾ _x.2 _x.5;
       let _x.7 := List.cons ◾ _x.1 _x.6;
-      let _x.8 := List.newForIn._at_.testing2.spec_0 _x.1 _x.7 x;
+      let _x.8 := List.newForIn._at_.testing2.spec_0 _x.7 x;
       return _x.8
 -/
 #guard_msgs in
@@ -152,47 +152,47 @@ def testing2 :=
 
 /--
 trace: [Compiler.saveMono] size: 9
-    def List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 l b : Nat :=
+    def List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing3.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b b;
-        let x := Nat.add _x.6 s;
-        let _x.7 := Nat.add x i;
-        let x := Nat.add _x.7 head.4;
-        let _x.8 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 tail.5 x;
-        return _x.8
+        let _x.2 := List.newForIn._at_.testing3.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b b;
+        let x := Nat.add _x.5 s;
+        let _x.6 := Nat.add x i;
+        let x := Nat.add _x.6 head.3;
+        let _x.7 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 tail.4 x;
+        return _x.7
 [Compiler.saveMono] size: 9
-    def List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.2 s i l b : Nat :=
+    def List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 tail.1 s i l b : Nat :=
       cases l : Nat
       | List.nil =>
-        let _x.3 := List.newForIn._at_.testing3.spec_1 _x.1 tail.2 b;
-        return _x.3
-      | List.cons head.4 tail.5 =>
-        let _x.6 := Nat.add b b;
-        let x := Nat.add _x.6 s;
-        let _x.7 := Nat.add x i;
-        let x := Nat.add _x.7 head.4;
-        let _x.8 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i _x.1 tail.2 tail.5 x;
-        return _x.8
+        let _x.2 := List.newForIn._at_.testing3.spec_1 tail.1 b;
+        return _x.2
+      | List.cons head.3 tail.4 =>
+        let _x.5 := Nat.add b b;
+        let x := Nat.add _x.5 s;
+        let _x.6 := Nat.add x i;
+        let x := Nat.add _x.6 head.3;
+        let _x.7 := List.newForIn._at_.List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2.spec_2 s i tail.1 tail.4 x;
+        return _x.7
 [Compiler.saveMono] size: 12
-    def List.newForIn._at_.testing3.spec_1 _x.1 l b : Nat :=
+    def List.newForIn._at_.testing3.spec_1 l b : Nat :=
       cases l : Nat
       | List.nil =>
         return b
-      | List.cons head.2 tail.3 =>
+      | List.cons head.1 tail.2 =>
+        let _x.3 := 1;
         let _x.4 := 10;
-        let _x.5 := Nat.sub _x.4 head.2;
-        let _x.6 := Nat.add _x.5 _x.1;
-        let _x.7 := 1;
-        let _x.8 := Nat.sub _x.6 _x.7;
-        let _x.9 := Nat.add head.2 _x.8;
-        let _x.10 := [] ◾;
-        let _x.11 := List.range'TR.go _x.1 _x.8 _x.9 _x.10;
-        let _x.12 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 _x.1 tail.3 b head.2 _x.11 b;
-        return _x.12
+        let _x.5 := Nat.sub _x.4 head.1;
+        let _x.6 := Nat.add _x.5 _x.3;
+        let _x.7 := Nat.sub _x.6 _x.3;
+        let _x.8 := Nat.add head.1 _x.7;
+        let _x.9 := [] ◾;
+        let _x.10 := List.range'TR.go _x.3 _x.7 _x.8 _x.9;
+        let _x.11 := List.newForIn._at_.testing3.spec_0._at_.List.newForIn._at_.testing3.spec_1.spec_2 tail.2 b head.1 _x.10 b;
+        return _x.11
 [Compiler.saveMono] size: 9
     def testing3 : Nat :=
       let x := 42;
@@ -203,7 +203,7 @@ trace: [Compiler.saveMono] size: 9
       let _x.5 := List.cons ◾ _x.3 _x.4;
       let _x.6 := List.cons ◾ _x.2 _x.5;
       let _x.7 := List.cons ◾ _x.1 _x.6;
-      let _x.8 := List.newForIn._at_.testing3.spec_1 _x.1 _x.7 x;
+      let _x.8 := List.newForIn._at_.testing3.spec_1 _x.7 x;
       return _x.8
 [Compiler.saveMono] size: 9
     def List.newForIn._at_.testing3.spec_0 s i kcontinue l b : Nat :=
diff --git a/tests/lean/run/do_for_loop_levenstein_compiler_test.lean b/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
index 7be10d86e6..0cefd9f4ce 100644
--- a/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
+++ b/tests/lean/run/do_for_loop_levenstein_compiler_test.lean
@@ -75,83 +75,87 @@ trace: [Compiler.saveMono] size: 13
           let _x.8 := String.length a;
           let _x.9 := 1;
           let _x.10 := Std.Legacy.Range.mk _x.4 _x.8 _x.9 ◾;
-          let _x.11 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.7 a _x.9 _x.5 _x.10 _x.4 s;
+          let _x.11 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.7 a _x.3 _x.10 _x.4 s;
           return _x.11
         | Bool.true =>
           let _x.12 := Array.reverse._redArg s;
           return _x.12
-[Compiler.saveMono] size: 29
-    def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range i a.4 : Array
+[Compiler.saveMono] size: 31
+    def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 as sz _x.2 range i a.3 : Array
       String :=
       cases range : Array String
       | Std.Legacy.Range.mk start stop step step_pos =>
-        let _x.5 := Nat.decLt i stop;
-        cases _x.5 : Array String
+        let _x.4 := Nat.decLt i stop;
+        cases _x.4 : Array String
         | Bool.false =>
-          let _x.6 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.3 a.4;
-          return _x.6
+          let _x.5 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.2 a.3;
+          return _x.5
         | Bool.true =>
-          let _x.7 := Nat.add i step;
-          let _x.8 := 0;
-          let _x.9 := String.utf8ByteSize s';
-          let _x.10 := String.Slice.mk s' _x.8 _x.9 ◾;
-          let _x.11 := @String.Slice.Pos.nextn _x.10 _x.8 i;
-          let _x.12 := @String.extract s' _x.8 _x.11;
-          let _x.13 := Nat.add i _x.1;
-          let _x.14 := @String.Slice.Pos.nextn _x.10 _x.8 _x.13;
-          let _x.15 := @String.extract s' _x.14 _x.9;
-          let d := String.append _x.12 _x.15;
-          jp _jp.16 : Array String :=
-            let out := Array.push ◾ a.4 d;
-            let _x.17 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range _x.7 out;
-            return _x.17;
-          let _x.18 := Array.contains._at_.deletions.spec_0 a.4 d;
-          cases _x.18 : Array String
+          let _x.6 := 1;
+          let _x.7 := 0;
+          let _x.8 := Nat.decEq _x.1 _x.7;
+          let _x.9 := Nat.add i step;
+          let _x.10 := String.utf8ByteSize s';
+          let _x.11 := String.Slice.mk s' _x.7 _x.10 ◾;
+          let _x.12 := @String.Slice.Pos.nextn _x.11 _x.7 i;
+          let _x.13 := @String.extract s' _x.7 _x.12;
+          let _x.14 := Nat.add i _x.6;
+          let _x.15 := @String.Slice.Pos.nextn _x.11 _x.7 _x.14;
+          let _x.16 := @String.extract s' _x.15 _x.10;
+          let d := String.append _x.13 _x.16;
+          jp _jp.17 : Array String :=
+            let out := Array.push ◾ a.3 d;
+            let _x.18 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 as sz _x.2 range _x.9 out;
+            return _x.18;
+          let _x.19 := Array.contains._at_.deletions.spec_0 a.3 d;
+          cases _x.19 : Array String
           | Bool.false =>
-            goto _jp.16
+            goto _jp.17
           | Bool.true =>
-            cases _x.2 : Array String
+            cases _x.8 : Array String
             | Bool.false =>
-              let _x.19 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range _x.7 a.4;
-              return _x.19
+              let _x.20 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 as sz _x.2 range _x.9 a.3;
+              return _x.20
             | Bool.true =>
-              goto _jp.16
-[Compiler.saveMono] size: 29
-    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 _x.3 range i a.4 : Array
+              goto _jp.17
+[Compiler.saveMono] size: 31
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 range i a.3 : Array
       String :=
       cases range : Array String
       | Std.Legacy.Range.mk start stop step step_pos =>
-        let _x.5 := Nat.decLt i stop;
-        cases _x.5 : Array String
+        let _x.4 := Nat.decLt i stop;
+        cases _x.4 : Array String
         | Bool.false =>
-          let _x.6 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.1 a.4;
-          return _x.6
+          let _x.5 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 as sz _x.1 a.3;
+          return _x.5
         | Bool.true =>
-          let _x.7 := Nat.add i step;
-          let _x.8 := 0;
-          let _x.9 := String.utf8ByteSize s';
-          let _x.10 := String.Slice.mk s' _x.8 _x.9 ◾;
-          let _x.11 := @String.Slice.Pos.nextn _x.10 _x.8 i;
-          let _x.12 := @String.extract s' _x.8 _x.11;
-          let _x.13 := Nat.add i _x.2;
-          let _x.14 := @String.Slice.Pos.nextn _x.10 _x.8 _x.13;
-          let _x.15 := @String.extract s' _x.14 _x.9;
-          let d := String.append _x.12 _x.15;
-          jp _jp.16 : Array String :=
-            let out := Array.push ◾ a.4 d;
-            let _x.17 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.2 _x.3 as sz _x.1 range _x.7 out;
-            return _x.17;
-          let _x.18 := Array.contains._at_.deletions.spec_0 a.4 d;
-          cases _x.18 : Array String
+          let _x.6 := 1;
+          let _x.7 := 0;
+          let _x.8 := Nat.decEq _x.2 _x.7;
+          let _x.9 := Nat.add i step;
+          let _x.10 := String.utf8ByteSize s';
+          let _x.11 := String.Slice.mk s' _x.7 _x.10 ◾;
+          let _x.12 := @String.Slice.Pos.nextn _x.11 _x.7 i;
+          let _x.13 := @String.extract s' _x.7 _x.12;
+          let _x.14 := Nat.add i _x.6;
+          let _x.15 := @String.Slice.Pos.nextn _x.11 _x.7 _x.14;
+          let _x.16 := @String.extract s' _x.15 _x.10;
+          let d := String.append _x.13 _x.16;
+          jp _jp.17 : Array String :=
+            let out := Array.push ◾ a.3 d;
+            let _x.18 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.2 as sz _x.1 range _x.9 out;
+            return _x.18;
+          let _x.19 := Array.contains._at_.deletions.spec_0 a.3 d;
+          cases _x.19 : Array String
           | Bool.false =>
-            goto _jp.16
+            goto _jp.17
           | Bool.true =>
-            cases _x.3 : Array String
+            cases _x.8 : Array String
             | Bool.false =>
-              let _x.19 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.2 _x.3 as sz _x.1 range _x.7 a.4;
-              return _x.19
+              let _x.20 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.2 as sz _x.1 range _x.9 a.3;
+              return _x.20
             | Bool.true =>
-              goto _jp.16
+              goto _jp.17
 [Compiler.saveMono] size: 15
     def deletions n s : Array String :=
       let zero := 0;
@@ -171,57 +175,57 @@ trace: [Compiler.saveMono] size: 13
         let _x.6 := 0;
         let _x.7 := Array.forInNew'Unsafe.loop._at_.deletions.spec_2 _x.5 sz _x.6 out;
         return _x.7
-[Compiler.saveMono] size: 29
-    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3 : Array
-      String :=
+[Compiler.saveMono] size: 31
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range i a.2 : Array String :=
       cases range : Array String
       | Std.Legacy.Range.mk start stop step step_pos =>
-        let _x.4 := Nat.decLt i stop;
-        cases _x.4 : Array String
+        let _x.3 := Nat.decLt i stop;
+        cases _x.3 : Array String
         | Bool.false =>
-          let _x.5 := kcontinue a.3;
-          return _x.5
+          let _x.4 := kcontinue a.2;
+          return _x.4
         | Bool.true =>
-          let _x.6 := Nat.add i step;
-          let _x.7 := 0;
-          let _x.8 := String.utf8ByteSize s';
-          let _x.9 := String.Slice.mk s' _x.7 _x.8 ◾;
-          let _x.10 := @String.Slice.Pos.nextn _x.9 _x.7 i;
-          let _x.11 := @String.extract s' _x.7 _x.10;
-          let _x.12 := Nat.add i _x.1;
-          let _x.13 := @String.Slice.Pos.nextn _x.9 _x.7 _x.12;
-          let _x.14 := @String.extract s' _x.13 _x.8;
-          let d := String.append _x.11 _x.14;
-          jp _jp.15 : Array String :=
-            let out := Array.push ◾ a.3 d;
-            let _x.16 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range _x.6 out;
-            return _x.16;
-          let _x.17 := Array.contains._at_.deletions.spec_0 a.3 d;
-          cases _x.17 : Array String
+          let _x.5 := 1;
+          let _x.6 := 0;
+          let _x.7 := Nat.decEq _x.1 _x.6;
+          let _x.8 := Nat.add i step;
+          let _x.9 := String.utf8ByteSize s';
+          let _x.10 := String.Slice.mk s' _x.6 _x.9 ◾;
+          let _x.11 := @String.Slice.Pos.nextn _x.10 _x.6 i;
+          let _x.12 := @String.extract s' _x.6 _x.11;
+          let _x.13 := Nat.add i _x.5;
+          let _x.14 := @String.Slice.Pos.nextn _x.10 _x.6 _x.13;
+          let _x.15 := @String.extract s' _x.14 _x.9;
+          let d := String.append _x.12 _x.15;
+          jp _jp.16 : Array String :=
+            let out := Array.push ◾ a.2 d;
+            let _x.17 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range _x.8 out;
+            return _x.17;
+          let _x.18 := Array.contains._at_.deletions.spec_0 a.2 d;
+          cases _x.18 : Array String
           | Bool.false =>
-            goto _jp.15
+            goto _jp.16
           | Bool.true =>
-            cases _x.2 : Array String
+            cases _x.7 : Array String
             | Bool.false =>
-              let _x.18 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range _x.6 a.3;
-              return _x.18
+              let _x.19 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range _x.8 a.2;
+              return _x.19
             | Bool.true =>
-              goto _jp.15
+              goto _jp.16
 [Compiler.saveMono] size: 1
-    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 _x.2 kcontinue range this i hs hl a.3 : Array
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1 s' _x.1 kcontinue range this i hs hl a.2 : Array String :=
+      let _x.3 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 kcontinue range i a.2;
+      return _x.3
+[Compiler.saveMono] size: 1
+    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4 as sz _x.1 s' _x.2 range this i hs hl a.3 : Array
       String :=
-      let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._redArg s' _x.1 _x.2 kcontinue range i a.3;
+      let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 range i a.3;
       return _x.4
 [Compiler.saveMono] size: 1
-    def Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4 as sz _x.1 s' _x.2 _x.3 range this i hs hl a.4 : Array
+    def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4 s' _x.1 as sz _x.2 range this i hs hl a.3 : Array
       String :=
-      let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4._redArg as sz _x.1 s' _x.2 _x.3 range i a.4;
-      return _x.5
-[Compiler.saveMono] size: 1
-    def Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4 s' _x.1 _x.2 as sz _x.3 range this i hs hl a.4 : Array
-      String :=
-      let _x.5 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 _x.2 as sz _x.3 range i a.4;
-      return _x.5
+      let _x.4 := Std.Legacy.Range.forInNew'.loop._at_.Std.Legacy.Range.forInNew'.loop._at_.deletions.spec_1._at_.Array.forInNew'Unsafe.loop._at_.deletions.spec_2.spec_4.spec_4._redArg s' _x.1 as sz _x.2 range i a.3;
+      return _x.4
 -/
 #guard_msgs in
 set_option trace.Compiler.saveMono true in