From a92890ec84380bbba6981152ef585f6dff1dca3c Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Tue, 10 Jun 2025 22:46:39 -0700 Subject: [PATCH] fix: use the fvar subst for erased code in LCNF simp (#8717) This PR uses the fvar substitution mechanism to replace erased code. This isn't entirely satisfactory, since LCNF's `.return` doesn't support a general `Arg` (which has a `.erased` constructor), it only supports an `FVarId`. This is in contrast to the IR `.ret`, which does support a general `Arg`. --- src/Lean/Compiler/LCNF/Simp/Main.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index 3e8e2f8d34..649d6dbd1d 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -224,13 +224,17 @@ 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 - if let some decls ← ConstantFold.foldConstants decl then + -- This `decl.value != .erased` check is required because `.return` takes + -- and `FVarId` rather than `Arg`, and the substitution will end up + -- creating a new erased let decl in that case. + if decl.type.isErased && decl.value != .erased then + modifySubst fun s => s.insert decl.fvarId (.const ``lcErased []) + eraseLetDecl decl + simp k + else if let some decls ← ConstantFold.foldConstants decl then markSimplified let k ← simp k attachCodeDecls decls k