chore: make checkUnivs linter into Lean.Linter (#13832)

This PR makes `checkUnivs` linter into `Lean.Linter`.

Stacked on top of #13803.

Author: wkrozowski

src/Lean/Linter.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Linter.Util
 public import Lean.Linter.Builtin
+public import Lean.Linter.CheckUnivs
 public import Lean.Linter.ConstructorAsVariable
 public import Lean.Linter.DefProp
 public import Lean.Linter.Deprecated

src/Lean/Linter/CheckUnivs.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Linter.Basic
+public import Lean.Linter.Util
+public import Lean.Util.CollectLevelParams
+public import Lean.Util.ForEachExpr
+
+public section
+
+namespace Lean.Linter
+open Elab Command Meta
+
+/--
+Enables the `checkUnivs` linter, which warns when a declaration has a universe parameter
+that only ever occurs in a `max u v` together with another parameter, never on its own.
+This usually means that the type contains a `max u v` where neither `u` nor `v` occur by
+themselves; the fix is to provide the universe level explicitly.
+-/
+register_builtin_option linter.checkUnivs : Bool := {
+  defValue := false
+  descr := "enable the `checkUnivs` linter, which warns when a declaration has a universe \
+    parameter that only ever occurs in a `max u v` together with another parameter, never \
+    on its own."
+}
+
+namespace CheckUnivs
+
+/--
+`univParamsGrouped e nm₀` computes for each `Level` occurring in `e` the set of level parameters
+that appear in it, returning the collection of such parameter sets.
+In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : level) ∈ e}`.
+Ignores `nm₀.proof_*` sub-constants.
+-/
+private def univParamsGrouped (e : Expr) (nm₀ : Name) : Std.HashSet (Array Name) :=
+  runST fun _ =>
+    let go : StateRefT (Std.HashSet (Array Name)) (ST _) Unit := e.forEach fun
+      | .sort u =>
+        modify (·.insert (CollectLevelParams.visitLevel u {}).params)
+      | .const n us => do
+        if let .str n s := n then
+          if n == nm₀ && s.startsWith "proof_" then return
+        modify (us.foldl (·.insert <| CollectLevelParams.visitLevel · {} |>.params))
+      | _ => pure ()
+    Prod.snd <$> go.run {}
+
+/--
+The good parameters are the parameters that occur somewhere in the set as a singleton or
+(recursively) with only other good parameters.
+All other parameters in the set are bad.
+-/
+private partial def badParams (l : Array (Array Name)) : Array Name :=
+  let goodLevels := l.filterMap fun
+    | #[u] => some u
+    | _ => none
+  if goodLevels.isEmpty then
+    l.flatten.foldl (init := #[]) fun acc x => if acc.contains x then acc else acc.push x
+  else
+    badParams <| l.map (·.filter (!goodLevels.contains ·))
+
+@[inherit_doc linter.checkUnivs]
+def checkUnivsLinter : Linter where run := withSetOptionIn fun _ => do
+  unless getLinterValue linter.checkUnivs (← getLinterOptions) do return
+  if (← get).messages.hasErrors then return
+  let env ← getEnv
+  let mut seen : NameSet := {}
+  for t in ← getInfoTrees do
+    for declName in getNewDecls t do
+      if seen.contains declName then continue
+      seen := seen.insert declName
+      let some info := env.find? declName | continue
+      let bad := badParams (univParamsGrouped info.type declName).toArray
+      unless bad.isEmpty do
+        let univs := MessageData.joinSep (bad.toList.map fun u => m!"`{u}`") ", "
+        logLintIf linter.checkUnivs (← getRef)
+          m!"`{.ofConstName declName}`: universes {univs} only occur together. \
+            This usually means there is a `max` expression in the type where none of these \
+            universes appear on their own."
+
+builtin_initialize addLinter checkUnivsLinter
+
+end CheckUnivs
+end Lean.Linter

src/Lean/Linter/EnvLinter.lean

@@ -8,4 +8,3 @@ module
 prelude
 public import Lean.Linter.EnvLinter.Basic
 public import Lean.Linter.EnvLinter.Frontend
-public import Lean.Linter.EnvLinter.Builtin

src/Lean/Linter/EnvLinter/Builtin.lean

@@ -57,3 +57,20 @@ def getDeclsByBody (t : InfoTree) : List Name :=
         else decls
       else decls
     | _ => decls
+
+/-- Get the names of declarations introduced by elaborating `t`.
+
+A declaration introduces a `TermInfo` with `isBinder := true` whose `expr` is the constant
+being declared. This covers `def`/`theorem`/`axiom`, inductive types and their constructors,
+and structure fields and parent projections — including mutual blocks where each member
+emits its own binder.
+-/
+def getNewDecls (t : InfoTree) : List Name :=
+  t.collectNodesBottomUp fun _ i _ acc =>
+    match i with
+    | .ofTermInfo ti =>
+      if ti.isBinder && ti.expr.isConst then
+        ti.expr.constName! :: acc
+      else
+        acc
+    | _ => acc

src/Lean/Linter/Util.lean

@@ -130,8 +130,8 @@ def testGetChecksDefault : CoreM (Array Name) := do
   let checks ← getChecks (scope := .default) (runOnly := none)
   return checks.map (·.name)
 
--- dummyBadName and checkUnivs are default, dummyExtraLinter is not
-/-- info: #[`checkUnivs, `dummyBadName] -/
+-- dummyBadName is default, dummyExtraLinter is not
+/-- info: #[`dummyBadName] -/
 #guard_msgs in
 #eval testGetChecksDefault
 
@@ -140,7 +140,7 @@ def testGetChecksExtra : CoreM (Array Name) := do
   let checks ← getChecks (scope := .extra) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`checkUnivs, `dummyBadName, `dummyExtraLinter] -/
+/-- info: #[`dummyBadName, `dummyExtraLinter] -/
 #guard_msgs in
 #eval testGetChecksExtra
 
@@ -149,7 +149,7 @@ def testGetChecksAll : CoreM (Array Name) := do
   let checks ← getChecks (scope := .all) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`checkUnivs, `dummyBadName, `dummyExtraLinter] -/
+/-- info: #[`dummyBadName, `dummyExtraLinter] -/
 #guard_msgs in
 #eval testGetChecksAll
 
@@ -181,7 +181,7 @@ def testLintCore : CoreM (Array (Name × Nat)) := do
   let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
   return results.map fun (linter, msgs) => (linter.name, msgs.size)
 
-/-- info: #[(`checkUnivs, 0), (`dummyBadName, 1)] -/
+/-- info: #[(`dummyBadName, 1)] -/
 #guard_msgs in
 #eval testLintCore
 
@@ -210,7 +210,7 @@ def testFormatResults : CoreM Format := do
   return (← msg.format)
 
 /--
-info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 2 linters
+info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 1 linters
 
 /- The `dummyBadName` linter reports:
 found bad names -/
@@ -229,39 +229,7 @@ def testFormatResultsClean : CoreM Format := do
   return (← msg.format)
 
 /--
-info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 2 linters
+info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 1 linters
 -/
 #guard_msgs in
 #eval testFormatResultsClean
-
-/-! ## Test: checkUnivs -/
-
--- Good: each universe parameter occurs alone somewhere
-universe u v in
-def goodUnivs (α : Type u) (β : Type v) : Type (max u v) := α × β
-
--- Good: one universe dominates the other (max u v where u occurs alone)
-universe u v in
-def goodUnivsDominated (α : Type u) (β : Type (max u v)) : Type (max u v) := α × β
-
--- Bad: neither u nor v occur alone
-universe u v in
-def badUnivs (α : Type (max u v)) : Type (max u v) := α
-
-def testCheckUnivs (declName : Name) : MetaM Bool := do
-  let some (linterDeclName, _) := (envLinterExt.getState (← getEnv)).find? `checkUnivs
-    | throwError "not found"
-  let linter ← getEnvLinter `checkUnivs linterDeclName
-  return (← linter.test declName).isSome
-
-/-- info: false -/
-#guard_msgs in
-#eval testCheckUnivs `goodUnivs
-
-/-- info: false -/
-#guard_msgs in
-#eval testCheckUnivs `goodUnivsDominated
-
-/-- info: true -/
-#guard_msgs in
-#eval testCheckUnivs `badUnivs

tests/elab/env_linter.lean

@@ -0,0 +1,41 @@
+module
+
+/-!
+Tests for the `linter.checkUnivs` linter, which warns when a declaration has a universe
+parameter that only ever occurs in a `max u v` together with another parameter, never
+on its own.
+-/
+
+set_option linter.checkUnivs true
+
+universe u v
+
+-- Good: each universe parameter occurs alone somewhere.
+def goodUnivs (α : Type u) (β : Type v) : Type (max u v) := α × β
+
+-- Good: `u` occurs alone in `α`, so the `max u v` is fine.
+def goodUnivsDominated (α : Type u) (β : Type (max u v)) : Type (max u v) := α × β
+
+-- Bad: neither `u` nor `v` occur alone in `badUnivs`'s type.
+/--
+warning: `badUnivs`: universes `u`, `v` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.
+
+Note: This linter can be disabled with `set_option linter.checkUnivs false`
+-/
+#guard_msgs in
+def badUnivs (α : Type (max u v)) : Type (max u v) := α
+
+-- `set_option ... false in` suppresses the warning locally.
+#guard_msgs in
+set_option linter.checkUnivs false in
+def badUnivsSuppressed (α : Type (max u v)) : Type (max u v) := α
+
+-- Inductives are also checked.
+/--
+warning: `BadInd`: universes `u`, `v` only occur together. This usually means there is a `max` expression in the type where none of these universes appear on their own.
+
+Note: This linter can be disabled with `set_option linter.checkUnivs false`
+-/
+#guard_msgs in
+inductive BadInd : Type (max u v) where
+  | mk

tests/elab/linterCheckUnivs.lean

@@ -1,9 +1,8 @@
 module
 
-public import Lean.Linter.EnvLinter
-public import Lean.Elab.Command
+public meta import Lean.Linter.EnvLinter
 
-open Lean Meta Lean.Linter Lean.Elab.Command
+open Lean Meta Lean.Linter
 
 /-- Dummy env linter for the `lake lint --builtin-lint` module-system test.
 Default scope (no `extra`), and the test reads only the declaration name so

tests/lake/tests/builtin-lint-module/Linters.lean

@@ -1,8 +1,10 @@
 import Main.Sub
 
--- `linter.defProp` is off by default for bootstrapping reasons; enable it
--- here so the test scenarios that exercise default lint mode still trigger it.
+-- `linter.defProp` and `linter.checkUnivs` are off by default for bootstrapping
+-- reasons; enable them here so the test scenarios that exercise default lint
+-- mode still trigger them.
 set_option linter.defProp true
+set_option linter.checkUnivs true
 
 -- This uses `def` for a Prop — the `defProp` linter should flag this.
 def shouldBeTheorem : 1 = 1 := rfl
@@ -24,7 +26,7 @@ instance plainInstIsOk : Nonempty String := ⟨""⟩
 universe u v in
 def badUnivDecl (α : Type (max u v)) : Type (max u v) := α
 
--- Annotated to be skipped by `checkUnivs`.
+-- `set_option` disables `checkUnivs` locally so this violation is not flagged.
+set_option linter.checkUnivs false in
 universe u v in
-@[builtin_nolint checkUnivs]
 def badUnivSkipped (α : Type (max u v)) : Type (max u v) := α

tests/lake/tests/builtin-lint/Main.lean

@@ -217,9 +217,11 @@ match_pat 'shouldBeTheorem' produced.out
 
 # --- builtinLint = true with a lint driver ---
 
-# builtinLint = true + lint driver + clean module: both builtin lints and driver run
+# builtinLint = true + lint driver + clean module: both builtin lints and driver run.
+# With no default env linters registered in core, the builtin-lint pass reports
+# "No environment linters registered" rather than "Linting passed".
 lake_out lint -f with-driver.lean Clean || true
-match_pat 'Linting passed for Clean' produced.out
+match_pat 'No environment linters registered for Clean' produced.out
 match_pat 'lint-driver:' produced.out
 
 # builtinLint = true + lint driver + violations: both run, exit code is nonzero