Universe inference infers `max u_1 u_2` with otherwise unused `u_1`, `u_2`

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

While inferring universe levels, Lean sometimes creates two universes u_1 and u_2 that only appear in max u_1 u_2.

Context

This occurred in an earlier version of the iterator library. In the meantime, I have gotten rid of max universe levels in most of the code base, so that this is no longer an issue for iterators, but it was still an annoying situation. The problem is that as soon as Lean infers universes as above noted, universe unification can easily get stuck because it needs to satisfy constraints x = max u_1 u_2 but there is no unique way to assign u_1 and u_2.

Steps to Reproduce

Try this in Lean Web:

structure ListIterator (α : Type u) (m : Type u → Type u) where
  list : List α

structure Iter (α : Type u) (m : Type max u v → Type max u v) (β : Type v) : Type u where
  inner : α

def List.iter (l : List α) (m) : Iter (α := ListIterator α m) m α :=
  ⟨{ list := l }⟩

set_option pp.universes true in
/--
info: List.iter.{u_1, u_2} {α : Type (max u_1 u_2)} (l : List.{max u_1 u_2} α) (m : Type (max u_1 u_2) → Type (max u_1 u_2)) :
  Iter.{max u_1 u_2, max u_1 u_2} (ListIterator.{max u_1 u_2} α m) m α
-/
#guard_msgs in
#check List.iter

Expected behavior:

Lean should never infer universe levels u_1 and u_2 such that the whole expression can be described without mentioning u_1 and u_2 individually, only max u_1 u_2. Instead, it should infer only a single universe level u_1 and use it whenver max u_1 u_2 occurs.

There are variants of this situation that might also be desirable to cover, such as only max u_1 (u_2 + 1) or imax u_1 u_2 occurring in the expression.

Actual behavior: [Clear and concise description of what actually happens]

See the #guard_msgs above -- Lean assigns max u_1 u_2 to every single universe level parameter.

Versions

Reproducible in Lean Web with these versions:

Lean 4.19.0-rc3
Target: x86_64-unknown-linux-gnu

Lean 4.20.0-nightly-2025-04-14
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal reproducer in the issue and inspect the universe-inference path exercised by #check List.iter and #guard_msgs. Compare the inferred universe parameters with the expected single-level form, then add or update a focused regression test covering the max case and verify the guard output no longer exposes independent unused universes.