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/Init/Grind/Order.lean

@@ -75,6 +75,9 @@ theorem nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCa
 theorem of_nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by
   intro _ _; subst x y; intro; simp [*]
 
+theorem of_natCast_eq {α : Type u} [NatCast α] (a b : Nat) (x y : α) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by
+  intro h₁ h₂ h; subst h; exact h₁.symm.trans h₂
+
 theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α]
     {a b : α} : ¬ a ≤ b → b ≤ a := by
   intro h

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

src/Lean/Meta/Tactic/Grind/Order/Assert.lean

@@ -148,11 +148,14 @@ def propagatePending : OrderM Unit := do
         - `h₁ : ↑ue' = ue`
         - `h₂ : ↑ve' = ve`
         - `h : ue = ve`
-        **Note**: We currently only support `Nat`. Thus `↑a` is actually
-        `NatCast.natCast a`. If we decide to support arbitrary semirings
-        in this module, we must adjust this code.
+        **Note**: We currently only support `Nat` originals. Thus `↑a` is actually
+        `NatCast.natCast a`. The lemma `nat_eq` is specialized to `Int`, so we
+        only invoke it when the cast destination is `Int`. For other types (e.g.
+        `Rat`), `pushEq ue ve h` above is sufficient and `grind` core can derive
+        the `Nat` equality via `norm_cast`/cast injectivity if needed.
         -/
-        pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h
+        if (← inferType ue) == Int.mkType then
+          pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h
 where
   /--
   If `e` is an auxiliary term used to represent some term `a`, returns
@@ -343,7 +346,7 @@ def getStructIdOf? (e : Expr) : GoalM (Option Nat) := do
   return (← get').exprToStructId.find? { expr := e }
 
 def propagateIneq (e : Expr) : GoalM Unit := do
-  if let some (e', he) := (← get').termMap.find? { expr := e } then
+  if let some { e := e', h := he, .. } := (← get').termMap.find? { expr := e } then
     go e' (some he)
   else
     go e none
@@ -369,20 +372,27 @@ builtin_grind_propagator propagateLT ↓LT.lt := propagateIneq
 public def processNewEq (a b : Expr) : GoalM Unit := do
   unless isSameExpr a b do
     let h ← mkEqProof a b
-    if let some (a', h₁) ← getAuxTerm? a then
-      let some (b', h₂) ← getAuxTerm? b | return ()
+    if let some { e := a', h := h₁, α } ← getAuxTerm? a then
+      let some { e := b', h := h₂, .. } ← getAuxTerm? b | return ()
       /-
       We have
       - `h  : a = b`
       - `h₁ : ↑a = a'`
       - `h₂ : ↑b = b'`
+      where `a'` and `b'` are `NatCast.natCast α inst _` for some type `α`.
       -/
-      let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h
-      go a' b' h
+      if α == Int.mkType then
+        let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h
+        go a' b' h
+      else
+        let u ← getDecLevel α
+        let inst ← synthInstance (mkApp (mkConst ``NatCast [u]) α)
+        let h := mkApp9 (mkConst ``Grind.Order.of_natCast_eq [u]) α inst a b a' b' h₁ h₂ h
+        go a' b' h
     else
       go a b h
 where
-  getAuxTerm? (e : Expr) : GoalM (Option (Expr × Expr)) := do
+  getAuxTerm? (e : Expr) : GoalM (Option TermMapEntry) := do
     return (← get').termMap.find? { expr := e }
 
   go (a b h : Expr) : GoalM Unit := do

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -166,9 +166,9 @@ def setStructId (e : Expr) : OrderM Unit := do
     exprToStructId := s.exprToStructId.insert { expr := e } structId
   }
 
-def updateTermMap (e eNew h : Expr) : GoalM Unit := do
+def updateTermMap (e eNew h α : Expr) : GoalM Unit := do
   modify' fun s => { s with
-    termMap    := s.termMap.insert { expr := e } (eNew, h)
+    termMap    := s.termMap.insert { expr := e } { e := eNew, h, α }
     termMapInv := s.termMapInv.insert { expr := eNew } (e, h)
   }
 
@@ -198,9 +198,9 @@ where
   getOriginal? (e : Expr) : GoalM (Option Expr) := do
     if let some (e', _) := (← get').termMapInv.find? { expr := e } then
       return some e'
-    let_expr NatCast.natCast _ _ a := e | return none
+    let_expr NatCast.natCast α _ a := e | return none
     if (← alreadyInternalized a) then
-      updateTermMap a e (← mkEqRefl e)
+      updateTermMap a e (← mkEqRefl e) α
       return some a
     else
       return none
@@ -290,7 +290,7 @@ def internalizeTerm (e : Expr) : OrderM Unit := do
 
 open Arith.Cutsat in
 def adaptNat (e : Expr) : GoalM Expr := do
-  if let some (eNew, _) := (← get').termMap.find? { expr := e } then
+  if let some { e := eNew, .. } := (← get').termMap.find? { expr := e } then
     return eNew
   else match_expr e with
     | LE.le _ _ lhs rhs => adaptCnstr lhs rhs (isLT := false)
@@ -307,12 +307,12 @@ where
     let h := mkApp6
         (mkConst (if isLT then ``Nat.ToInt.lt_eq else ``Nat.ToInt.le_eq))
         lhs rhs lhs' rhs' h₁ h₂
-    updateTermMap e eNew h
+    updateTermMap e eNew h (← getIntExpr)
     return eNew
 
   adaptTerm : GoalM Expr := do
     let (eNew, h) ← natToInt e
-    updateTermMap e eNew h
+    updateTermMap e eNew h (← getIntExpr)
     return eNew
 
 def adapt (α : Expr) (e : Expr) : GoalM (Expr × Expr) := do

src/Lean/Meta/Tactic/Grind/Order/Types.lean

@@ -128,6 +128,13 @@ structure Struct where
   propagate          : List ToPropagate := []
   deriving Inhabited
 
+/-- Entry/Value for the map `termMap` in `State` -/
+structure TermMapEntry where
+  e : Expr
+  h : Expr
+  α : Expr
+deriving Inhabited
+
 /-- State for all order types detected by `grind`. -/
 structure State where
   /-- Order structures detected. -/
@@ -143,7 +150,7 @@ structure State where
   Example: given `x y : Nat`, `x ≤ y + 1` is mapped to `Int.ofNat x ≤ Int.ofNat y + 1`, and proof
   of equivalence.
   -/
-  termMap    : PHashMap ExprPtr (Expr × Expr) := {}
+  termMap    : PHashMap ExprPtr TermMapEntry := {}
   /-- `termMap` inverse -/
   termMapInv : PHashMap ExprPtr (Expr × Expr) := {}
   deriving Inhabited

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?)
 

src/lake/Lake/Build/Common.lean

@@ -235,7 +235,7 @@ public def checkHashUpToDate
 : JobM Bool := (·.isUpToDate) <$> checkHashUpToDate' info depTrace depHash oldTrace
 
 /--
-**Ror internal use only.**
+**For internal use only.**
 Checks whether `info` is up-to-date with the trace.
 If so, replays the log of the trace if available.
 -/
@@ -271,20 +271,24 @@ Returns `true` if the saved trace exists and its hash matches `inputHash`.
 
 If up-to-date, replays the saved log from the trace and sets the current
 build action to `replay`. Otherwise, if the log is empty and trace is synthetic,
-or if the trace is not up-to-date, the build action will be set to `fetch`.
+or if the trace is not up-to-date, the build action will be set to `reuse`.
 -/
-public def SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
+public def SavedTrace.replayCachedIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
   if let .ok data := self then
     if data.depHash == inputHash then
       if data.synthetic && data.log.isEmpty then
-        updateAction .fetch
+        updateAction .reuse
       else
         updateAction .replay
         data.log.replay
       return true
-  updateAction .fetch
+  updateAction .reuse
   return false
 
+@[deprecated replayCachedIfUpToDate (since := "2026-04-15")]
+public abbrev SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
+  self.replayCachedIfUpToDate inputHash
+
 /-- **For internal use only.** -/
 public class ToOutputJson (α : Type u) where
   toOutputJson (arts : α) : Json
@@ -684,7 +688,7 @@ public def buildArtifactUnlessUpToDate
     let fetchArt? restore := do
       let some (art : XArtifact exe) ← getArtifacts? inputHash savedTrace pkg
         | return none
-      unless (← savedTrace.replayOrFetchIfUpToDate inputHash) do
+      unless (← savedTrace.replayCachedIfUpToDate inputHash) do
         removeFileIfExists file
         writeFetchTrace traceFile inputHash (toJson art.descr)
       if restore then

src/lake/Lake/Build/Job/Basic.lean

@@ -29,11 +29,18 @@ namespace Lake
 public inductive JobAction
 /-- No information about this job's action is available. -/
 | unknown
-/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
+/-- Tried to reuse a cached build (e.g., can be set by `replayCachedIfUpToDate`). -/
+| reuse
+/-- Tried to replay a completed build action (e.g., can be set by `replayIfUpToDate`). -/
 | replay
-/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
+/-- Tried to unpack a build from an archive (e.g., unpacking a module `ltar`). -/
+| unpack
+/--
+Tried to fetch a build from a remote store (e.g., set when downloading an artifact
+on-demand from a cache service in `buildArtifactUnlessUpToDate`).
+-/
 | fetch
-/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
+/-- Tried to perform a build action (e.g., set by `buildAction`). -/
 | build
 deriving Inhabited, Repr, DecidableEq, Ord
 
@@ -45,11 +52,13 @@ public instance : Min JobAction := minOfLe
 public instance : Max JobAction := maxOfLe
 
 public def merge (a b : JobAction) : JobAction :=
-  max a b
+  max a b -- inlines `max`
 
-public def verb (failed : Bool) : JobAction → String
+public def verb (failed : Bool) : (self : JobAction) → String
 | .unknown => if failed then "Running" else "Ran"
+| .reuse => if failed then "Reusing" else "Reused"
 | .replay => if failed then "Replaying" else "Replayed"
+| .unpack => if failed then "Unpacking" else "Unpacked"
 | .fetch => if failed then "Fetching" else "Fetched"
 | .build => if failed then "Building" else "Built"
 

src/lake/Lake/Build/Module.lean

@@ -900,8 +900,9 @@ where
     let inputHash := (← getTrace).hash
     let some ltarOrArts ← getArtifacts? inputHash savedTrace mod.pkg
       | return .inr savedTrace
-    match (ltarOrArts : ModuleOutputs)  with
+    match (ltarOrArts : ModuleOutputs) with
     | .ltar ltar =>
+      updateAction .unpack
       mod.clearOutputArtifacts
       mod.unpackLtar ltar.path
       -- Note: This branch implies that only the ltar output is (validly) cached.
@@ -919,7 +920,7 @@ where
       else
         return .inr savedTrace
     | .arts arts =>
-      unless (← savedTrace.replayOrFetchIfUpToDate inputHash) do
+      unless (← savedTrace.replayCachedIfUpToDate inputHash) do
         mod.clearOutputArtifacts
         writeFetchTrace mod.traceFile inputHash (toJson arts.descrs)
       let arts ←

src/lake/Lake/Build/Package.lean

@@ -153,7 +153,7 @@ def Package.fetchBuildArchive
   let upToDate ← buildUnlessUpToDate? (action := .fetch) archiveFile depTrace traceFile do
     download url archiveFile headers
   unless upToDate && (← self.buildDir.pathExists) do
-    updateAction .fetch
+    updateAction .unpack
     untar archiveFile self.buildDir
 
 @[inline]

src/lake/Lake/Build/Run.lean

@@ -210,7 +210,7 @@ def mkMonitorContext (cfg : BuildConfig) (jobs : JobQueue) : BaseIO MonitorConte
   let failLv := cfg.failLv
   let isVerbose := cfg.verbosity = .verbose
   let showProgress := cfg.showProgress
-  let minAction := if isVerbose then .unknown else .fetch
+  let minAction := if isVerbose then .unknown else .unpack
   let showOptional := isVerbose
   let showTime := isVerbose || !useAnsi
   let updateFrequency := 100

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

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

tests/elab/grind_order_eq.lean

@@ -30,3 +30,6 @@ example
 example
     : a = b + 1 → a ≤ b + 2 := by
   grind -lia -linarith -ring (splits := 0) only
+
+-- Issue #13265: kernel error from `of_nat_eq` when the cast is to a non-`Int` type.
+example (j k : Nat) (h : j = k) : (j + 1 : Rat) = (k + 1 : Rat) := by grind

tests/lake/tests/cache/test.sh

@@ -102,16 +102,16 @@ test_run exe test
 touch Ignored.lean
 test_run -v build +Ignored
 
-# Verify that fetching from the cache can be disabled
+# Verify that using the cache can be disabled
 test_cmd rm -f .lake/build/lib/lean/Ignored.trace
 test_status $NO_BUILD_CODE -v -f disabled.toml build +Ignored --no-build
 LAKE_ARTIFACT_CACHE=false test_status $NO_BUILD_CODE -v \
   -f unset.toml build +Ignored --no-build
 
-# Verify that fetching from the cache creates a trace file that does not replay
-test_out "Fetched Ignored" -v build +Ignored
+# Verify that using the cache creates a trace file that does not replay
+test_out "Reused Ignored" -v build +Ignored
 test_exp -f .lake/build/lib/lean/Ignored.trace
-test_out "Fetched Ignored" -v build +Ignored
+test_out "Reused Ignored" -v build +Ignored
 
 # Verify that modifications invalidate the cache
 echo "def foo := ()" > Ignored.lean
@@ -162,7 +162,7 @@ check_diff .lake/backup-outputs.txt <(ls "$CACHE_DIR/outputs")
 test_cmd rm -f "$local_art"
 test_out "Replayed Test:c.o" build +Test:o -v --no-build
 test_cmd rm -f "$local_art.trace"
-test_out "Fetched Test:c.o" build +Test:o -v --no-build
+test_out "Reused Test:c.o" build +Test:o -v --no-build
 
 # Verify that if the input cache is missing,
 # the cached artifact is still used via the output hash in the trace