diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 3f8c4a081ca9..e2135250ee1d 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -140,7 +140,7 @@ def getLevel (type : Expr) : MetaM Level := do
   let typeType ← inferType type
   let typeType ← whnfD typeType
   match typeType with
-  | Expr.sort lvl     => return lvl
+  | Expr.sort lvl     => return (← instantiateLevelMVars lvl).normalize
   | Expr.mvar mvarId  =>
     if (← mvarId.isReadOnlyOrSyntheticOpaque) then
       throwTypeExpected type
diff --git a/tests/elab/doForMutSortPoly.lean b/tests/elab/doForMutSortPoly.lean
new file mode 100644
index 000000000000..b1c2b6652649
--- /dev/null
+++ b/tests/elab/doForMutSortPoly.lean
@@ -0,0 +1,29 @@
+import Lean
+
+/-!
+Test that `getLevel` instantiates and normalizes level metavariables.
+
+Without this, `getDecLevel` fails on sort-polymorphic types with `Prop` components:
+`PProd.{?u, ?v} Nat True` has sort `max ?u ?v`. After `?u := 1`, `?v := 0`, this should
+normalize to `1` (decrementable to `0`), but without instantiation `decLevel` sees
+`max ?u ?v`, tries to decrement each arm independently inside the `max`, follows
+`?v → 0`, and fails because `dec 0 = none`.
+-/
+
+-- Direct reproducer: getDecLevel on PProd with assigned-but-uninstantiated level mvars
+open Lean Meta in
+#eval show MetaM _ from do
+  let u ← mkFreshLevelMVar
+  let v ← mkFreshLevelMVar
+  let ty := mkApp2 (mkConst ``PProd [u, v]) (mkConst ``Nat) (mkConst ``True)
+  assignLevelMVar u.mvarId! (.succ .zero)
+  assignLevelMVar v.mvarId! .zero
+  let lvl ← getDecLevel ty
+  assert! lvl == .zero
+
+-- End-to-end: for loop with sort-polymorphic mut var
+def foo : Unit := Id.run do
+  let mut x : PProd Nat True := ⟨0, trivial⟩
+  for _ in [true] do
+    x := ⟨0, trivial⟩
+    break
diff --git a/tests/elab/nestedInductiveConstructions.lean b/tests/elab/nestedInductiveConstructions.lean
index 70171c0cf93a..61be1aba03f2 100644
--- a/tests/elab/nestedInductiveConstructions.lean
+++ b/tests/elab/nestedInductiveConstructions.lean
@@ -140,8 +140,8 @@ fun {motive_1} {motive_2} t =>
   Tree.rec.{(max (u + 1) u_1) + 1, u} (fun a a_ih => PProd.{u_1, max (u + 1) u_1} (motive_2 a) a_ih)
     PUnit.{max (u + 1) u_1}
     (fun head tail head_ih tail_ih =>
-      PProd.{max (max 1 u_1) (u + 1) u_1, max (max 1 u_1) (u + 1) u_1}
-        (PProd.{u_1, max (u + 1) u_1} (motive_1 head) head_ih) (PProd.{u_1, max (u + 1) u_1} (motive_2 tail) tail_ih))
+      PProd.{max (u + 1) u_1, max (u + 1) u_1} (PProd.{u_1, max (u + 1) u_1} (motive_1 head) head_ih)
+        (PProd.{u_1, max (u + 1) u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -154,8 +154,8 @@ fun {motive_1} {motive_2} t =>
   Tree.rec_1.{(max (u + 1) u_1) + 1, u} (fun a a_ih => PProd.{u_1, max (u + 1) u_1} (motive_2 a) a_ih)
     PUnit.{max (u + 1) u_1}
     (fun head tail head_ih tail_ih =>
-      PProd.{max (max 1 u_1) (u + 1) u_1, max (max 1 u_1) (u + 1) u_1}
-        (PProd.{u_1, max (u + 1) u_1} (motive_1 head) head_ih) (PProd.{u_1, max (u + 1) u_1} (motive_2 tail) tail_ih))
+      PProd.{max (u + 1) u_1, max (u + 1) u_1} (PProd.{u_1, max (u + 1) u_1} (motive_1 head) head_ih)
+        (PProd.{u_1, max (u + 1) u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
diff --git a/tests/elab_fail/doNotation1.lean.out.expected b/tests/elab_fail/doNotation1.lean.out.expected
index 6435ba43cf92..926ae71df9c8 100644
--- a/tests/elab_fail/doNotation1.lean.out.expected
+++ b/tests/elab_fail/doNotation1.lean.out.expected
@@ -49,7 +49,7 @@ doNotation1.lean:78:21-78:31: error: typeclass instance problem is stuck
 Note: Lean will not try to resolve this typeclass instance problem because the type argument to `ToString` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
 
 Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-doNotation1.lean:82:0-83:9: error: Type mismatch. `for` loops have result type PUnit, but the rest of the `do` sequence expected List (Nat × Nat).
+doNotation1.lean:82:0-83:9: error: Type mismatch. `for` loops have result type Unit, but the rest of the `do` sequence expected List (Nat × Nat).
 doNotation1.lean:83:7-83:9: error: Application type mismatch: The argument
   ()
 has type
@@ -59,8 +59,8 @@ but is expected to have type
 in the application
   pure ()
 doNotation1.lean:82:0-83:9: error: Type mismatch
-  PUnit.unit
+  ()
 has type
-  PUnit
+  Unit
 but is expected to have type
   List (Nat × Nat)