From 501993eb7f19860101ddf1dc9ec2a06ab3ce5e15 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Thu, 3 Jul 2025 12:17:25 -0700
Subject: [PATCH] fix: don't pull instances depending on erased propositions
 (#9177)

This PR makes the `pullInstances` pass avoid pulling any instance
expressions containing erased propositions, because we don't correctly
represent the dependencies that remain after erasure.
---
 src/Lean/Compiler/LCNF/PullLetDecls.lean |  5 +++++
 tests/lean/run/instanceUsingFalse.lean   | 14 ++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/lean/run/instanceUsingFalse.lean

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
+