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

@@ -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

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
+