From 0b2884bfa3b19ae35f73958864c74cecb92011b6 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Tue, 10 Jun 2025 17:58:55 -0700 Subject: [PATCH] fix: erase code of an erased type in LCNF simp (#8712) This PR optimizes let decls of an erased type to an erased value. Specialization can create local functions that produce a Prop, and there's no point in keeping them around. --- src/Lean/Compiler/LCNF/Simp/Main.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index 8c0ba865be..3e8e2f8d34 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -224,6 +224,9 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do let mut decl ← normLetDecl baseDecl if baseDecl != decl then markSimplified + if decl.type.isErased && decl.value != .erased then + markSimplified + decl ← decl.updateValue .erased if let some value ← simpValue? decl.value then markSimplified decl ← decl.updateValue value