The inferred level for structures doesn't always work

Prerequisites

• 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

The inferred level for structures can cause universe level comparison failures when imax is involved and sometimes it's quite hard to find a working level.

Context

Figuring out dependent mutual wellfounded recursion.

Steps to Reproduce

/--
error: Invalid universe level for field `MyType`: Field has type
  Sort (imax u v)
at universe level
  (imax u v) + 1
which is not less than or equal to the structure's resulting universe level
  max (u + 1) (v + 1)
-/
#guard_msgs in
structure Test where
  MyType : Sort (imax u v)
  thing : MyType

Expected behavior:
The inferred level works for any non-recursive structures.

Actual behavior:
Test fails with an error at the field MyType. Specifying Type (imax u v) manually produces the error [...] imax u v [...] is not less than or equal to [...] (imax u v) + 1 at thing. Another option, Sort (max (imax u v + 1) (imax 2 (imax u v))), instead produces a kernel error. Sort (max (imax u v + 1) u v) works but it should not be so hard to find a working level.

Versions

Lean 4.31.0-nightly-2026-04-17

Impact

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

Start by running the minimal structure example against the latest Lean nightly or on live.lean-lang.org and inspect the structure universe-level inference path, focusing on the imax case. Done means the reproducible non-recursive structure is accepted without manually specifying a level, with a regression test covering the example.