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