From 738688efeed68cd70c7ae8a51e07d63e0095b73e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 26 Feb 2026 23:33:08 +0100
Subject: [PATCH] chore: cleanup after closed term extraction by removing dead
 values (#12717)

---
 src/Lean/Compiler/LCNF/ExtractClosed.lean   |  6 +++-
 tests/elab/unhygienicCode.lean.out.expected | 32 +++++++--------------
 2 files changed, 15 insertions(+), 23 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ExtractClosed.lean b/src/Lean/Compiler/LCNF/ExtractClosed.lean
index 3aa07df7c6..5d29d5d50c 100644
--- a/src/Lean/Compiler/LCNF/ExtractClosed.lean
+++ b/src/Lean/Compiler/LCNF/ExtractClosed.lean
@@ -10,6 +10,7 @@ public import Lean.Compiler.ClosedTermCache
 public import Lean.Compiler.NeverExtractAttr
 public import Lean.Compiler.LCNF.Internalize
 public import Lean.Compiler.LCNF.ToExpr
+import Lean.Compiler.LCNF.ElimDead
 
 public section
 
@@ -159,7 +160,10 @@ end ExtractClosed
 
 partial def Decl.extractClosed (decl : Decl .pure) (sccDecls : Array (Decl .pure)) :
     CompilerM (Array (Decl .pure)) := do
-  let ⟨decl, s⟩ ← ExtractClosed.visitDecl decl |>.run { baseName := decl.name, sccDecls } |>.run {}
+  let mut ⟨decl, s⟩ ← ExtractClosed.visitDecl decl |>.run { baseName := decl.name, sccDecls } |>.run {}
+  if !s.decls.isEmpty then
+    -- Closed term extraction might have left behind dead values.
+    decl ← decl.elimDeadVars
   return s.decls.push decl
 
 def extractClosed : Pass where
diff --git a/tests/elab/unhygienicCode.lean.out.expected b/tests/elab/unhygienicCode.lean.out.expected
index 54c46639c4..caa9f3814b 100644
--- a/tests/elab/unhygienicCode.lean.out.expected
+++ b/tests/elab/unhygienicCode.lean.out.expected
@@ -61,26 +61,14 @@
       let _x.2 := foo._closed_0;
       let _x.3 := Syntax.atom _x.2 _x.1;
       return _x.3
-[Compiler.extractClosed] size: 20
+[Compiler.extractClosed] size: 8
     def foo n : Syntax :=
-      let _x.1 := Syntax.missing;
-      let _x.2 := 1;
-      let _x.3 := false;
-      let _x.4 := foo._closed_0;
-      let _x.5 := foo._closed_1;
-      let _x.6 := foo._closed_2;
-      let _x.7 := foo._closed_3;
-      let _x.8 := foo._closed_4;
-      let _x.9 := foo._closed_5;
-      let _x.10 := foo._closed_6;
-      let _x.11 := foo._closed_7;
-      let _x.12 := foo._closed_8;
-      let _x.13 := [] ◾;
-      let _x.14 := foo._closed_9;
-      let _x.15 := foo._closed_10;
-      let _x.16 := foo._closed_11;
-      let _x.17 := Nat.reprFast n;
-      let _x.18 := SourceInfo.none;
-      let _x.19 := @Syntax.mkNumLit _x.17 _x.18;
-      let _x.20 := Syntax.node3 _x.4 _x.8 _x.14 _x.16 _x.19;
-      return _x.20
+      let _x.1 := foo._closed_0;
+      let _x.2 := foo._closed_4;
+      let _x.3 := foo._closed_9;
+      let _x.4 := foo._closed_11;
+      let _x.5 := Nat.reprFast n;
+      let _x.6 := SourceInfo.none;
+      let _x.7 := @Syntax.mkNumLit _x.5 _x.6;
+      let _x.8 := Syntax.node3 _x.1 _x.2 _x.3 _x.4 _x.7;
+      return _x.8