fix: decLevel? should normalize

src/Lean/Meta/DecLevel.lean

@@ -21,6 +21,7 @@ structure DecLevelContext where
 
 private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Level)
   | Level.zero        => return none
+  | Level.succ u      => return u
   | Level.param _     => return none
   | Level.mvar mvarId => do
     match (← getLevelMVarAssignment? mvarId) with
@@ -33,28 +34,35 @@ private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Le
         trace[Meta.isLevelDefEq.step] "decAux?, {mkLevelMVar mvarId} := {mkLevelSucc u}"
         assignLevelMVar mvarId (mkLevelSucc u)
         return u
-  | Level.succ u  => return u
-  | u =>
-    let processMax (u v : Level) : ReaderT DecLevelContext MetaM (Option Level) := do
-      /- Remark: this code uses the fact that `max (u+1) (v+1) = (max u v)+1`.
-         `decAux? (max (u+1) (v+1)) := max (decAux? (u+1)) (decAux? (v+1))`
-         However, we must *not* assign metavariables in the recursive calls since
-         `max ?u 1` is not equivalent to `max ?v 0` where `?v` is a fresh metavariable, and `?u := ?v+1`
+  | Level.max u v     => do
+    /- Remark: this code uses the fact that `max (u+1) (v+1) = (max u v)+1`.
+       `decAux? (max (u+1) (v+1)) := max (decAux? (u+1)) (decAux? (v+1))`
+       However, we must *not* assign metavariables in the recursive calls since the equation
+       `max ?u 1 = (max ?v 0) + 1`, where `?v` is a fresh metavariable, does *not* force `?u := ?v+1`.
+     -/
+    withReader (fun _ => { canAssignMVars := false }) do
+      match (← decAux? u) with
+      | none    => return none
+      | some u' => do
+        match (← decAux? v) with
+        | none    => return none
+        | some v' => return mkLevelMax' u' v'
+  | Level.imax u v    => do
+    /- Remark: for `imax u v` to be nonzero, `v` *must* be nonzero, so assigning metavariables in `v` is permissible. -/
+    match (← decAux? v) with
+    | none    => return none
+    | some v' =>
+      /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`.
+         Like for `max`, the equation `imax ?u 1 = (max ?v 0) + 1` does *not* force `?u := ?v + 1`.
        -/
       withReader (fun _ => { canAssignMVars := false }) do
         match (← decAux? u) with
-        | none   => return none
-        | some u => do
-          match (← decAux? v) with
-          | none   => return none
-          | some v => return mkLevelMax' u v
-    match u with
-    | Level.max u v  => processMax u v
-    /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/
-    | Level.imax u v => processMax u v
-    | _              => unreachable!
+        | none => return none
+        | some u' => return mkLevelMax' u' v'
 
 def decLevel? (u : Level) : MetaM (Option Level) := do
+  /- Normalize so that levels such as `max (u + 1) 0` can be decremented. -/
+  let u := (← instantiateLevelMVars u).normalize
   let mctx ← getMCtx
   match (← decAux? u |>.run {}) with
   | some v => return some v

tests/elab/decLevel.lean

@@ -0,0 +1,69 @@
+import Lean
+/-!
+# Tests of `Meta.decLevel?`
+-/
+
+open Lean Elab Term Command
+
+elab "#dec_level " u:level : command => runTermElabM fun _ => do
+  let u ← elabLevel u
+  let u' ← Meta.decLevel u
+  let u ← instantiateLevelMVars u
+  let u' ← instantiateLevelMVars u'
+  logInfo m!"({u'}) + 1 = {u}"
+
+/-!
+Decrementing constant.
+-/
+/-- info: (1) + 1 = 2 -/
+#guard_msgs in #dec_level 2
+
+/-!
+Decrement can assign.
+-/
+/-- info: (?u.2) + 1 = ?u.2 + 1 -/
+#guard_msgs in #dec_level _
+
+/-!
+Cannot assign inside `max`.
+-/
+/-- error: invalid universe level, max ?u.2 ?u.1 is not greater than 0 -/
+#guard_msgs in #dec_level max _ _
+
+/-!
+Simplifies `max`, allowing assignment.
+-/
+/-- info: (?u.2) + 1 = ?u.2 + 1 -/
+#guard_msgs in #dec_level max 0 _
+/-- info: (?u.2) + 1 = ?u.2 + 1 -/
+#guard_msgs in #dec_level max _ 0
+
+/-!
+Simplifies `imax` if first argument is `0`.
+-/
+/-- info: (?u.2) + 1 = ?u.2 + 1 -/
+#guard_msgs in #dec_level imax 0 _
+/-!
+Can't decrement `imax _ 0`.
+-/
+/-- error: invalid universe level, 0 is not greater than 0 -/
+#guard_msgs in #dec_level imax 5 0
+/-!
+Second argument of `imax` is always assignable.
+-/
+/-- info: (max 4 ?u.2) + 1 = max 5 (?u.2 + 1) -/
+#guard_msgs in #dec_level imax 5 _
+
+/-!
+Tests of `max` decrementing both arguments.
+-/
+/-- info: (u) + 1 = u + 1 -/
+#guard_msgs in universe u in #dec_level max 1 (u + 1)
+/-- info: (max 1 u) + 1 = max 2 (u + 1) -/
+#guard_msgs in universe u in #dec_level max 2 (u + 1)
+
+/-!
+Failure, since `u` cannot be decremented.
+-/
+/-- error: invalid universe level, max 1 u is not greater than 0 -/
+#guard_msgs in universe u in #dec_level max 1 u

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)