Universe approximation creates a cyclic level metavariable assignment and stack overflow #16125

With Meta.Context.univApprox := true, isLevelDefEq can assign a universe metavariable to its own successor. Subsequent universe instantiation overflows the stack.

This reproduces using only import Lean and public APIs; the example does not call the unchecked assignLevelMVar API.

import Lean

open Lean Meta in
run_meta do
  let m ← mkFreshLevelMVar
  let a := Level.param `a
  withReader (fun ctx : Meta.Context => { ctx with univApprox := true }) do
    discard <| isLevelDefEq (mkLevelMax a (mkLevelSucc m)) (mkLevelMax a m)
    discard <| instantiateLevelMVars m

Running lean UniverseCycle.lean prints:

Stack overflow detected. Aborting.

Observed on Linux x86_64 with the official Lean 4.36.0-rc2 toolchain, commit b35cb10cf2ced51a2fd1880cfdbf75c71ab7a35a (Release); exit status 134.

The cyclic assignment can also be checked without crashing. Replace the final two lines with:

    let ok ← isLevelDefEq (mkLevelMax a (mkLevelSucc m)) (mkLevelMax a m)
    assert! ok
    let assignment ← getLevelMVarAssignment? m.mvarId!
    assert! assignment == some (mkLevelSucc m)

Those assertions pass: unification has produced ?m := succ ?m.

The apparent cause is the missing occurs check in tryApproxMaxMax.solve. For max a (succ ?m) =?= max a ?m, the first branch directly assigns ?m := succ ?m. The symmetric branch also directly assigns without checking occurrence. The same code is present on current master; I have not executed the reproducer on that commit.

Expected behavior: approximate universe unification should preserve an acyclic metavariable context, rejecting or postponing a constraint when an assignment would introduce a cycle.

I encountered this while prototyping a Mathlib linter that re-elaborates a theorem after dropping one parameter. Dropping a section parameter while retaining explicitly dependent section binders triggered the overflow in both Mathlib/CategoryTheory/Limits/Types/End.lean (coendRel_iff) and Mathlib/CategoryTheory/Topos/Sheaf.lean (Sheaf.isPullback_χ_truth). Both debugger backtraces repeatedly recurse through lean::instantiate_lmvars_all_fn::visit. The prototype now skips those invalid section-context trials, which avoids both crashes, but the Lean-only reproducer above still demonstrates the underlying issue.

🤖 Prepared with Codex.