From aa769e7677e517f679265016dfb64de65ccffc1a Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Fri, 25 Jul 2025 17:49:52 -0700
Subject: [PATCH] chore: make inferVisibility LCNF pass style match others
 (#9558)

---
 src/Lean/Compiler/LCNF/Passes.lean     | 12 ++----------
 src/Lean/Compiler/LCNF/Visibility.lean | 18 +++++++++++-------
 2 files changed, 13 insertions(+), 17 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index 2f8b2444e6..278dbb0c17 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -64,14 +64,6 @@ def saveMono : Pass where
     return decl
   shouldAlwaysRunCheck := true
 
-def inferVisibility (phase : Phase) : Pass where
-  occurrence := 0
-  phase
-  name := `inferVisibility
-  run decls := do
-    LCNF.inferVisibility phase decls
-    return decls
-
 end Pass
 
 open Pass
@@ -99,7 +91,7 @@ def builtinPassManager : PassManager := {
     saveBase, -- End of base phase
     -- should come last so it can see all created decls
     -- pass must be run for each phase; see `base/monoTransparentDeclsExt`
-    Pass.inferVisibility .base,
+    inferVisibility (phase := .base),
     toMono,
     simp (occurrence := 3) (phase := .mono),
     reduceJpArity (phase := .mono),
@@ -116,7 +108,7 @@ def builtinPassManager : PassManager := {
     simp (occurrence := 5) (phase := .mono),
     cse (occurrence := 2) (phase := .mono),
     saveMono,  -- End of mono phase
-    Pass.inferVisibility .mono,
+    inferVisibility (phase := .mono),
     extractClosed,
   ]
 }
diff --git a/src/Lean/Compiler/LCNF/Visibility.lean b/src/Lean/Compiler/LCNF/Visibility.lean
index 7f7e5a27c8..f3723f6942 100644
--- a/src/Lean/Compiler/LCNF/Visibility.lean
+++ b/src/Lean/Compiler/LCNF/Visibility.lean
@@ -51,13 +51,17 @@ partial def markDeclPublicRec (phase : Phase) (decl : Decl) : CompilerM Unit :=
             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"
-      markDeclPublicRec phase decl
+def inferVisibility (phase : Phase) : Pass where
+  occurrence := 0
+  phase
+  name := `inferVisibility
+  run decls := do
+    if (← getEnv).header.isModule then
+      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"
+          markDeclPublicRec phase decl
+    return decls
 
 builtin_initialize
   registerTraceClass `Compiler.inferVisibility