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