diff --git a/src/Lean/Compiler/LCNF/PullLetDecls.lean b/src/Lean/Compiler/LCNF/PullLetDecls.lean
index ec48511a69..27e7ec117a 100644
--- a/src/Lean/Compiler/LCNF/PullLetDecls.lean
+++ b/src/Lean/Compiler/LCNF/PullLetDecls.lean
@@ -107,6 +107,11 @@ def Decl.pullLetDecls (decl : Decl) (isCandidateFn : LetDecl → FVarIdSet → C
 
 def Decl.pullInstances (decl : Decl) : CompilerM Decl :=
   decl.pullLetDecls fun letDecl candidates => do
+    -- TODO: Correctly represent these dependencies so this check isn't required.
+    if let .const _ _ args := letDecl.value then
+      if args.any (· == .erased) then return false
+    if let .fvar _ args := letDecl.value then
+      if args.any (· == .erased) then return false
     if (← isClass? letDecl.type).isSome then
       return true
     else if let .proj _ _ fvarId := letDecl.value then
diff --git a/tests/lean/run/instanceUsingFalse.lean b/tests/lean/run/instanceUsingFalse.lean
new file mode 100644
index 0000000000..b5f7439940
--- /dev/null
+++ b/tests/lean/run/instanceUsingFalse.lean
@@ -0,0 +1,14 @@
+class WrappedNat (α : Type) where
+  n : Nat
+
+inductive FalseContainer where
+  | nat (n : Nat)
+  | oops (f : Prop → False)
+
+def f (x : FalseContainer) : WrappedNat FalseContainer :=
+  match x with
+  | .nat n => { n }
+  | .oops f => (f (0 == 0)).rec
+
+#eval f (.nat 1) |>.n
+