Strange error "invalid reassignment, value has type ?m.926 : Type u but is expected to have type Nat : Type"

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

All mutable variables in do blocks seem to be required to have the same universe as the containing Monad (unless unused). Some strange errors may be reported (not sure if they will in all cases), which are neither very helpful nor clear, in cases where this is not true.

Steps to Reproduce

Here is a MWE:

def test.{u, v} {m : Type u → Type v} [Monad m] : m PUnit.{u + 1} := do
  let mut i : Nat := 0
  while true do i := i + 1

Expected behavior: Either of the following:

• The mutable variable i could be (automatically) boxed into a ULift.{u} that gives it the correct universe (perhaps hard to achieve?), or
• A clearer error should be printed, hinting at the fact that i has a type that isn't a Type u (required by forIn and bind) therefore is "incompatible" with the containing Monad.

Actual behavior: The following error is reported on the while loop, which isn't clear or helpful unless you know the cause (although it seems to hint at a universe problem)

invalid reassignment, value has type
  ?m.369 : Type u
but is expected to have type
  Nat : Type

Versions

Tested on https://live.lean-lang.org/#project=lean-nightly at version 4.20.0-nightly-2025-04-26 as well as locally at version 4.18.0.

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 run it against the listed Lean nightly and local versions. Investigate mutable variables in do blocks and the while/forIn/bind universe handling; done means either the value is accepted through boxing or the compiler reports a clear universe-related error.