From 592eb02bb2d2191ddd728165129ae9e52a880daf Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 17 Apr 2026 18:07:22 -0700
Subject: [PATCH] feat: have level metavariable pretty printer instantiate
 level metavariables (#13438)

This PR makes the universe level pretty printer instantiate level
metavariables when `pp.instantiateMVars` is true.

Previously level metavariables were not instantiated.

The PR adjusts the tracing in the LevelDefEq module to create the trace
message using the original MetavarContext. It also adds
`Meta.isLevelDefEq.step` traces for when level metavariables are
assigned.
---
 src/Lean/Meta/LevelDefEq.lean                 | 22 ++++++++++++++-----
 src/Lean/PrettyPrinter/Delaborator/Basic.lean |  1 +
 tests/elab/343.lean                           |  2 +-
 tests/elab/456.lean                           |  2 +-
 4 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index eaed3886b7..637f855c5e 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -38,7 +38,9 @@ and assigning `?m := max ?n v`
 private def solveSelfMax (mvarId : LMVarId) (v : Level) : MetaM Unit := do
   assert! v.isMax
   let n ← mkFreshLevelMVar
-  assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
+  let v' := mkMaxArgsDiff mvarId v n
+  trace[Meta.isLevelDefEq.step] "solveSelfMax: {mkLevelMVar mvarId} := {v'}"
+  assignLevelMVar mvarId v'
 
 /--
 Returns true if `v` is `max u ?m` (or variant). That is, we solve `u =?= max u ?m` as `?m := u`.
@@ -53,6 +55,7 @@ private def tryApproxSelfMax (u v : Level) : MetaM Bool := do
 where
   solve (v' : Level) (mvarId : LMVarId) : MetaM Bool := do
     if u == v' then
+      trace[Meta.isLevelDefEq.step] "tryApproxSelfMax {mkLevelMVar mvarId} := {u}"
       assignLevelMVar mvarId u
       return true
     else
@@ -71,8 +74,14 @@ private def tryApproxMaxMax (u v : Level) : MetaM Bool := do
   | _, _ => return false
 where
   solve (u₁ u₂ v' : Level) (mvarId : LMVarId) : MetaM Bool := do
-    if u₁ == v' then assignLevelMVar mvarId u₂; return true
-    else if u₂ == v' then assignLevelMVar mvarId u₁; return true
+    if u₁ == v' then
+      trace[Meta.isLevelDefEq.step] "tryApproxMaxMax {mkLevelMVar mvarId} := {u₂}"
+      assignLevelMVar mvarId u₂
+      return true
+    else if u₂ == v' then
+      trace[Meta.isLevelDefEq.step] "tryApproxMaxMax {mkLevelMVar mvarId} := {u₁}"
+      assignLevelMVar mvarId u₁
+      return true
     else return false
 
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
@@ -97,9 +106,11 @@ mutual
       else if (← isMVarWithGreaterDepth v mvarId) then
         -- If both `u` and `v` are both metavariables, but depth of v is greater, then we assign `v := u`.
         -- This can only happen when levelAssignDepth is set to a smaller value than depth (e.g. during TC synthesis)
+        trace[Meta.isLevelDefEq.step] "{v} := {u}"
         assignLevelMVar v.mvarId! u
         return LBool.true
       else if !u.occurs v then
+        trace[Meta.isLevelDefEq.step] "{u} := {v}"
         assignLevelMVar u.mvarId! v
         return LBool.true
       else if v.isMax && !strictOccursMax u v then
@@ -133,8 +144,9 @@ mutual
   @[export lean_is_level_def_eq]
   partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool
     | Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs
-    | lhs, rhs =>
-      withTraceNode `Meta.isLevelDefEq (fun _ => return m!"{lhs} =?= {rhs}") do
+    | lhs, rhs => do
+      withTraceNodeBefore `Meta.isLevelDefEq (fun _ =>
+          withOptions (·.set `pp.instantiateMVars false) do addMessageContext m!"{lhs} =?= {rhs}") do
       if lhs.getLevelOffset == rhs.getLevelOffset then
         return lhs.getOffset == rhs.getOffset
       else
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index ba94431601..c7e254bf95 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -484,6 +484,7 @@ open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze DelabM getPPOption)
 
 def delabLevel (l : Level) (prec : Nat) : MetaM Syntax.Level := do
+  let l ← if getPPInstantiateMVars (← getOptions) then instantiateLevelMVars l else pure l
   let mvars := getPPMVarsLevels (← getOptions)
   return Level.quote l prec (mvars := mvars) (lIndex? := (← getMCtx).findLevelIndex?)
 
diff --git a/tests/elab/343.lean b/tests/elab/343.lean
index d0646901ee..9fc33c92bc 100644
--- a/tests/elab/343.lean
+++ b/tests/elab/343.lean
@@ -41,7 +41,7 @@ with
   CatIsh.{max _ _, max (_ + 1) (_ + 1)} : Type (max ((max _ _) + 1) ((max (_ + 1) (_ + 1)) + 1))
 ---
 error: failed to solve universe constraint
-  max (_ + 1) (_ + 1) =?= max (_ + 1) (_ + 1)
+  max (u_1 + 1) (u_2 + 1) =?= max (u_3 + 1) (u_4 + 1)
 while trying to unify
   Catish.Obj : Type (max ((max (u_1 + 1) (u_2 + 1)) + 1) ((max u_3 u_4) + 1))
 with
diff --git a/tests/elab/456.lean b/tests/elab/456.lean
index 4bd91ca0a5..42edd90eb2 100644
--- a/tests/elab/456.lean
+++ b/tests/elab/456.lean
@@ -2,7 +2,7 @@ set_option pp.mvars false
 
 /--
 error: failed to solve universe constraint
-  u =?= max 1 _
+  u =?= 1
 while trying to unify
   Sort u : Type u
 with