fix: universe normalization in getDecLevel

src/Lean/Meta/DecLevel.lean

@@ -69,12 +69,16 @@ def decLevel (u : Level) : MetaM Level := do
 
 /-- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
    Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
-   and then decrement 1 to obtain `u`. -/
+   instantiate and normalize it, and then decrement 1 to obtain `u`. -/
 def getDecLevel (type : Expr) : MetaM Level := do
-  decLevel (← getLevel type)
+  let l ← getLevel type
+  let l ← normalizeLevel l
+  decLevel l
 
 def getDecLevel? (type : Expr) : MetaM (Option Level) := do
-  decLevel? (← getLevel type)
+  let l ← getLevel type
+  let l ← normalizeLevel l
+  decLevel? l
 
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.step

tests/elab/doForMutSortPoly.lean

@@ -0,0 +1,11 @@
+/-!
+Test that `for` loops with `mut` variables of sort-polymorphic type (e.g. `PProd`) work correctly.
+`PProd Nat True : Sort (max 1 0)` has a `Prop` component, so `getDecLevel` must see the fully
+instantiated and normalized level `1` rather than `max ?u ?v` with unresolved metavariables.
+-/
+
+def foo : Unit := Id.run do
+  let mut x : PProd Nat True := ⟨0, trivial⟩
+  for _ in [true] do
+    x := ⟨0, trivial⟩
+    break

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)