Skip to content

fix: instantiate and normalize level metavariables in getLevel #13343

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
sgraf812 wants to merge 2 commits into from
+37 −8
Closed

fix: instantiate and normalize level metavariables in getLevel #13343

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
514d850
fix: universe normalization in getLevel
sgraf812 Apr 9, 2026
104a473
test: add direct `getDecLevel` reproducer for sort-polymorphic types
sgraf812 Apr 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Lean/Meta/InferType.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Copy Markdown
Collaborator

@kmill kmill Apr 9, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Usually we leave instantiation and other such operations to whoever needs it. Can you comment on why it's better to change getLevel instead of fixing decLevel??

Copy link
Copy Markdown
Contributor Author

@sgraf812 sgraf812 Apr 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, that's exactly my backup plan!

Copy link
Copy Markdown
Collaborator

@kmill kmill Apr 9, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that decLevel itself is able to instantiate metavariables already. The actual issue isn't about instantiation, but that processMax should skip arguments where decrementing fails, so long as at least one succeeds, if I'm understanding it correctly. In your example, decrementing max (u + 1) 0 should be u, even though you can't decrement 0.

For imax though, decrementing the second argument must succeed. The first argument's success is optional.

Copy link
Copy Markdown
Contributor Author

@sgraf812 sgraf812 Apr 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, but what about max (?u+1) ?v? If this returns just ?u then we are losing information because ?v could be larger than ?u+1, no? Maybe the correct thing is to filter out max components that can't be decremented? That works as long as decLevel? l = none iff l = 0... Not sure whether this is true.

Copy link
Copy Markdown
Contributor Author

@sgraf812 sgraf812 Apr 9, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At any rate, all I need right now is to instantiate and then normalize the resulting constant Level expression. I think I'm going to do just that in getDecLevel and getDecLevel?.

I don't want to touch decLevel? directly, because it has many transitive call sites; it's called from the main def eq solving function, for example.

Copy link
Copy Markdown
Collaborator

@kmill kmill Apr 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, yeah, my approach would need can/can't/unknown.

How about this: give decLevel? the ability to simplify max expressions? Here's a possibility:

  | u => do
    let isAlwaysZero (u : Level) : MetaM Bool := do
      if u.isAlwaysZero then
        return true
      else if u.isNeverZero then
        return false
      else
        let u ← instantiateLevelMVars u
        return u.isAlwaysZero
    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  =>
      if ← isAlwaysZero u then
        decAux? v
      else if ← isAlwaysZero v then
        decAux? u
      else
        processMax u v
    | Level.imax u v =>
      if ← isAlwaysZero v then
        return none
      else if ← isAlwaysZero u then
        decAux? v
      else
        /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/
        processMax u v

Copy link
Copy Markdown
Collaborator

@kmill kmill Apr 9, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

all I need right now is to instantiate and then normalize the resulting constant Level expression

I'm worried about the unknown impact of normalizing the expressions. I don't have any specific concerns though, just the fact that it will result in significantly reordered level expressions. Giving decAux? the ability to more precisely decrement max expressions seems like a smaller change to me, despite the fact it has a bigger impact — and I do worry about decLevel? and getDecLevel? having subtly different behavior.

Copy link
Copy Markdown
Collaborator

@kmill kmill Apr 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I take it back — after having looked at how isLevelDefEq works, I think you're perfectly justified in using normalize. Having decAux? do any simplification just makes it more complicated, and it's an imperfect simplification anyway.

(I want to see the performance impact of some changes to decAux? so I made #13352, but I don't intend to merge it. Feel free to take the extra test file for this PR.)

| Expr.mvar mvarId =>
if (← mvarId.isReadOnlyOrSyntheticOpaque) then
throwTypeExpected type
Expand Down
29 changes: 29 additions & 0 deletions tests/elab/doForMutSortPoly.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
8 changes: 4 additions & 4 deletions tests/elab/nestedInductiveConstructions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
6 changes: 3 additions & 3 deletions tests/elab_fail/doNotation1.lean.out.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Loading