fix: expose LCNF of private inline decl referenced by implemented_by (#9514)

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
 }
 

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

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