From d88e417cda0f7afb1e15c806c6bfdbbb09ba7eef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 30 Sep 2025 21:51:16 +0200
Subject: [PATCH] refactor: tame down dead let eliminator in lambda RC (#10626)

This PR reduces the aggressiveness of the dead let eliminator from
lambda RC.

The motivation for this is that all other passes in lambda RC respect
impurity but the dead let eliminator still operates under the assumption
of purity. There is a couple of motivations for the elim dead let
elaborator:
- unused projections introduced by the ToIR translation
- the elim dead branch pass introducing new opportunities
- closed term extraction introducing new opportunities
---
 src/Lean/Compiler/IR/ElimDeadVars.lean | 29 +++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Compiler/IR/ElimDeadVars.lean b/src/Lean/Compiler/IR/ElimDeadVars.lean
index d8be5dff9c..4679348fd1 100644
--- a/src/Lean/Compiler/IR/ElimDeadVars.lean
+++ b/src/Lean/Compiler/IR/ElimDeadVars.lean
@@ -13,6 +13,18 @@ public section
 
 namespace Lean.IR
 
+/--
+This function implements a simple heuristic for let values that we know may be dropped because they
+are pure.
+-/
+private def safeToElim (e : Expr) : Bool :=
+  match e with
+  | .ctor .. | .reset .. | .reuse .. | .proj .. | .uproj .. | .sproj .. | .box .. | .unbox ..
+  | .lit .. | .isShared .. | .pap .. => true
+  -- 0-ary full applications are considered constants
+  | .fap _ args => args.isEmpty
+  | .ap .. => false
+
 partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
   let rec reshape (bs : Array FnBody) (b : FnBody) (used : IndexSet) :=
     if bs.isEmpty then b
@@ -23,13 +35,20 @@ partial def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody :=
         let used := curr.collectFreeIndices used
         let b    := curr.setBody b
         reshape bs b used
-      let keepIfUsed (vidx : Index) :=
-        if used.contains vidx then keep ()
-        else reshape bs b used
+      let keepIfUsedJp (vidx : Index) :=
+        if used.contains vidx then
+          keep ()
+        else
+          reshape bs b used
+      let keepIfUsedLet (vidx : Index) (val : Expr) :=
+        if used.contains vidx || !safeToElim val then
+          keep ()
+        else
+          reshape bs b used
       match curr with
-      | FnBody.vdecl x _ _ _  => keepIfUsed x.idx
+      | FnBody.vdecl x _ e _  => keepIfUsedLet x.idx e
       -- TODO: we should keep all struct/union projections because they are used to ensure struct/union values are fully consumed.
-      | FnBody.jdecl j _ _ _  => keepIfUsed j.idx
+      | FnBody.jdecl j _ _ _  => keepIfUsedJp j.idx
       | _                     => keep ()
   reshape bs term term.freeIndices