fix: decLevel? should normalize

src/Lean/Elab/Do/Basic.lean

@@ -606,8 +606,8 @@ private partial def extractMonadInfo (expectedType? : Option Expr) : Term.TermEl
     unless ← isType resultType do return none
     let u ← getDecLevel resultType
     let v ← getDecLevel type
-    let u := u.normalize
-    let v := v.normalize
+    let u := (← instantiateLevelMVars u).normalize
+    let v := (← instantiateLevelMVars v).normalize
     return some ({ m, u, v }, resultType)
   let rec extract? (type : Expr) : Term.TermElabM (Option (MonadInfo × Expr)) := do
     match (← extractStep? type) with

src/Lean/Meta/DecLevel.lean

@@ -12,67 +12,110 @@ public section
 
 namespace Lean.Meta
 
-structure DecLevelContext where
-  /--
-   If `true`, then `decAux? ?m` returns a fresh metavariable `?n` s.t.
-   `?m := ?n+1`.
-   -/
-  canAssignMVars : Bool := true
-
-private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Level)
-  | Level.zero        => return none
-  | Level.param _     => return none
+private inductive DecResult where
+  /-- The level can be decremented. -/
+  | succ (u : Level)
+  /-- The level cannot be decremented since it is always zero. -/
+  | zero
+  /-- The level `u` cannot be decremented due to a metavariable `?v`, and `?v` is the only metavariable
+  such that `1 ≤ u` implies `1 ≤ ?v`. Hence, assigning `?v := ?v'+1` where `?v'` is a fresh metavariable
+  will make it possible to decrement `u`. -/
+  | mvar (mvarId : LMVarId)
+  /-- The expression cannot be decremented due to a parameter or metavariable. -/
+  | none
+
+private def DecResult.isSucc (r? : DecResult) : Bool := r? matches .succ _
+
+/--
+`decAux? u` checks whether `1 ≤ u` by finding a level `u'` such that `u = u'+1`, if possible.
+-/
+private partial def decAux? : Level → MetaM DecResult
+  | Level.zero        => return .zero
+  | Level.succ u      => return .succ u
+  | Level.param _     => return .none
   | Level.mvar mvarId => do
     match (← getLevelMVarAssignment? mvarId) with
-    | some u => decAux? u
-    | none   =>
-      if (← mvarId.isReadOnly) || !(← read).canAssignMVars then
-        return none
-      else
-        let u ← mkFreshLevelMVar
-        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`
-       -/
-      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!
+    | some u          => decAux? u
+    | none            => return .mvar mvarId
+  | Level.max u v     => processMax u v false
+  | Level.imax u v    => processMax u v true
+where
+  /--
+  Decrements `max` or `imax` using the rules
+  - `max (u+1) (v+1) = (max u v) + 1`
+  - `max (u+1) 0 = u+1`
+  - `max 0 (v+1) = v+1`
+  - `imax (u+1) (v+1) = (max u v) + 1`
+  - `imax 0 (v+1) = v+1`
+
+  In general, `1 ≤ max u v` iff `1 ≤ u` or `1 ≤ v`.
+  If neither `u` nor `v` is zero, then we need both `1 ≤ u` and `1 ≤ v` to be true to decrement `max u v`.
+  If `1 ≤ u` or `1 ≤ v` can be made to be true by metavariable assignments, then we want to determine
+  the unique solution, if one exists. This is only possible if both `1 ≤ u` and `1 ≤ v` are obstructed by the same metavariable.
+
+  There is also a special rule for `imax (u+1) ?v`, since `1 ≤ imax (u+1) ?v` is only satisfiable if `1 ≤ ?v`.
+  We let `imax ?u ?v` fail since after a `?v := ?v'+1` assignment, `imax ?u (?v'+1) = max ?u (?v'+1)`,
+  and `1 ≤ max ?u (?v'+1)` is true even if `?u = 0`.
+  -/
+  processMax (u v : Level) (imax : Bool) : MetaM DecResult := do
+    match (← decAux? u), (← decAux? v) with
+    | .succ u',      .succ v'      => return .succ <| mkLevelMax' u' v'
+    | u'?,           .zero         => return if imax then .zero else u'?
+    | .zero,         v'?           => return v'?
+    | .mvar uMVarId, .mvar vMVarId => return if uMVarId == vMVarId then .mvar uMVarId else .none
+    | .mvar _,       _             => return .none
+    | u'?,           .mvar vMVarId => return if imax && u'?.isSucc then .mvar vMVarId else .none
+    | .none,         _             => return .none
+    | _,             .none         => return .none
+
+/--
+Returns a level `u'` such that `u = u'+1`, if such a level exists.
 
+If there's a metavariable `?v` that obstructs decrementing the level, then it assigns `?v := ?v'+1`
+where `?v'` is a fresh metavariable, but only if the inequality `1 ≤ u` implies `1 ≤ ?v`.
+-/
 def decLevel? (u : Level) : MetaM (Option Level) := do
-  let mctx ← getMCtx
-  match (← decAux? u |>.run {}) with
-  | some v => return some v
-  | none   => do
-    modify fun s => { s with mctx := mctx }
-    return none
+  match (← decAux? u) with
+  | .zero | .none => return none
+  | .succ u'      => return u'
+  | .mvar mvarId  =>
+    if (← mvarId.isReadOnly) then
+      return none
+    else
+      let v ← mkFreshLevelMVar
+      trace[Meta.isLevelDefEq.step] "decAux?, {mkLevelMVar mvarId} := {mkLevelSucc v}"
+      assignLevelMVar mvarId (mkLevelSucc v)
+      match (← decAux? u) with
+      | .succ u' => return u'
+      | _        => unreachable!
+
+/--
+Returns a level `u'` such that `u = u'+1`. Throws an error if no such level exist.
 
+Assigns metavariables to make this possible. See `decLevel?` for details.
+-/
 def decLevel (u : Level) : MetaM Level := do
   match (← decLevel? u) with
   | some u => return u
   | none   => throwError "invalid universe level, {u} is not greater than 0"
 
-/-- 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`. -/
+/--
+Given a type `α`, infers the universe level `u` such that `α : Type u`. Throws an error if no such level exists.
+
+Assigns metavariables to make this possible. See `decLevel?` for details.
+
+This method is useful for inferring universe level parameters for functions 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 by one to obtain `u`.
+-/
 def getDecLevel (type : Expr) : MetaM Level := do
   decLevel (← getLevel type)
 
+/--
+Given a type `α`, infers the universe level `u` such that `α : Type u`, if such a level exists.
+
+See `getDecLevel` for details.
+-/
 def getDecLevel? (type : Expr) : MetaM (Option Level) := do
   decLevel? (← getLevel type)
 

tests/elab/decLevel.lean

@@ -0,0 +1,103 @@
+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}"
+
+/-!
+Cannot decrement zero.
+-/
+/-- error: invalid universe level, 0 is not greater than 0 -/
+#guard_msgs in #dec_level 0
+
+/-!
+Decrementing positive constant.
+-/
+/-- info: (2) + 1 = 3 -/
+#guard_msgs in #dec_level 3
+
+/-!
+Cannot decrement universe parameter.
+-/
+/-- error: invalid universe level, u is not greater than 0 -/
+#guard_msgs in universe u in #dec_level u
+
+/-!
+Decrementing offset universe parameter
+-/
+/-- info: (u + 2) + 1 = u + 3 -/
+#guard_msgs in universe u in #dec_level u+3
+
+/-!
+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 _ _
+/-- error: invalid universe level, max ?u.1 3 is not greater than 0 -/
+#guard_msgs in #dec_level max _ 3
+/-- error: invalid universe level, max 3 ?u.1 is not greater than 0 -/
+#guard_msgs in #dec_level max 3 _
+
+/-!
+Can assign inside `max` if one side is zero.
+-/
+/-- 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
+/-- info: (?u.2) + 1 = ?u.2 + 1 -/
+#guard_msgs in #dec_level max (imax 2 (max 0 0)) _
+
+/-!
+Can assign inside `imax` if first argument is zero
+-/
+/-- 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 assignable, if the first argument is zero or decrementable.
+-/
+/-- info: (max 4 ?u.2) + 1 = max 5 (?u.2 + 1) -/
+#guard_msgs in #dec_level imax 5 _
+/-- info: (?u.2) + 1 = ?u.2 + 1 -/
+#guard_msgs in #dec_level imax 0 _
+/-- error: invalid universe level, imax u ?u.1 is not greater than 0 -/
+#guard_msgs in universe u in #dec_level imax u _
+
+/-!
+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
+/-- error: invalid universe level, max u 1 is not greater than 0 -/
+#guard_msgs in universe u in #dec_level max u 1
+/-- error: invalid universe level, imax 1 u is not greater than 0 -/
+#guard_msgs in universe u in #dec_level imax 1 u
+/-- error: invalid universe level, max u 1 is not greater than 0 -/
+#guard_msgs in universe u in #dec_level imax u 1

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)