From 4177f123bc4c17148ff7b8d98a13b1868208d860 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 24 Jul 2025 15:05:21 +0200
Subject: [PATCH] fix: expose LCNF of private inline decl referenced by
 `implemented_by` (#9514)

---
 src/Lean/Compiler/ImplementedByAttr.lean |  2 --
 src/Lean/Compiler/LCNF/Main.lean         |  7 ++++++
 src/Lean/Compiler/LCNF/Visibility.lean   | 32 +++++++++++++-----------
 3 files changed, 25 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index e1a6234b72..3e486629c3 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -61,8 +61,6 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara
         throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has type{indentExpr fnType}\nbut '{declName}' has type{indentExpr declType}"
       if decl.name == fnDecl.name then
         throwError "invalid 'implemented_by' argument '{fnName}', function cannot be implemented by itself"
-      trace[Compiler.inferVisibility] m!"Marking {fnName} as opaque because it implements {decl.name}"
-      modifyEnv (LCNF.setDeclPublic · fnName)
       return fnName
 }
 
diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 650d41a4b0..49aed61b62 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -18,6 +18,7 @@ import Lean.Compiler.LCNF.Check
 import Lean.Compiler.LCNF.PullLetDecls
 import Lean.Compiler.LCNF.PhaseExt
 import Lean.Compiler.LCNF.CSE
+public import Lean.Compiler.LCNF.Visibility
 
 namespace Lean.Compiler.LCNF
 /--
@@ -88,6 +89,12 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
   and it often creates a very deep recursion.
   Moreover, some declarations get very big during simplification.
   -/
+  for declName in declNames do
+    if let some fnName := Compiler.getImplementedBy? (← getEnv) declName then
+      if !isDeclPublic (← getEnv) fnName then
+        if let some decl ← getLocalDecl? fnName then
+          trace[Compiler.inferVisibility] m!"Marking {fnName} as opaque because it implements {declName}"
+          LCNF.markDeclPublicRec .base decl
   let declNames ← declNames.filterM (shouldGenerateCode ·)
   if declNames.isEmpty then return #[]
   for declName in declNames do
diff --git a/src/Lean/Compiler/LCNF/Visibility.lean b/src/Lean/Compiler/LCNF/Visibility.lean
index 5713bc0526..ded86f4da4 100644
--- a/src/Lean/Compiler/LCNF/Visibility.lean
+++ b/src/Lean/Compiler/LCNF/Visibility.lean
@@ -32,25 +32,29 @@ private def isBodyRelevant (decl : Decl) : CompilerM Bool := do
   decl.isTemplateLike
     -- <||> decl.value.isCodeAndM (pure <| ·.sizeLe (compiler.small.get opts))
 
-partial def inferVisibility (phase : Phase) (decls : Array Decl) : CompilerM Unit := do
+/--
+Marks the given declaration as to be exported and recursively infers the correct visibility of its
+body and referenced declarations based on that.
+-/
+partial def markDeclPublicRec (phase : Phase) (decl : Decl) : CompilerM Unit := do
+  modifyEnv (setDeclPublic · decl.name)
+  if (← isBodyRelevant decl) && !isDeclTransparent (← getEnv) phase decl.name then
+    trace[Compiler.inferVisibility] m!"Marking {decl.name} as transparent because it is opaque and its body looks relevant"
+    modifyEnv (setDeclTransparent · phase decl.name)
+    decl.value.forCodeM fun code =>
+      for ref in collectUsedDecls code do
+        if let some refDecl ← getLocalDecl? ref then
+          if !isDeclPublic (← getEnv) ref then
+            trace[Compiler.inferVisibility] m!"Marking {ref} as opaque because it is used by transparent {decl.name}"
+            markDeclPublicRec phase refDecl
+
+def inferVisibility (phase : Phase) (decls : Array Decl) : CompilerM Unit := do
   if !(← getEnv).header.isModule then
     return
   for decl in decls do
     if (← getEnv).setExporting true |>.contains decl.name then
       trace[Compiler.inferVisibility] m!"Marking {decl.name} as opaque because it is a public def"
-      markPublic decl
-where
-  markPublic (decl : Decl) : CompilerM Unit := do
-    modifyEnv (setDeclPublic · decl.name)
-    if (← isBodyRelevant decl) && !isDeclTransparent (← getEnv) phase decl.name then
-      trace[Compiler.inferVisibility] m!"Marking {decl.name} as transparent because it is opaque and its body looks relevant"
-      modifyEnv (setDeclTransparent · phase decl.name)
-      decl.value.forCodeM fun code =>
-        for ref in collectUsedDecls code do
-          if let some refDecl ← getLocalDecl? ref then
-            if !isDeclPublic (← getEnv) ref then
-              trace[Compiler.inferVisibility] m!"Marking {ref} as opaque because it is used by transparent {decl.name}"
-              markPublic refDecl
+      markDeclPublicRec phase decl
 
 builtin_initialize
   registerTraceClass `Compiler.inferVisibility