fix: add checkSystem calls to hasAssignableMVar (#13219)

This PR moves `hasAssignableMVar`, `hasAssignableLevelMVar`, and
`isLevelMVarAssignable` from `MetavarContext.lean` to a new
`Lean.Meta.HasAssignableMVar` module, changing them from generic `[Monad
m] [MonadMCtx m]` functions to `MetaM` functions. This enables adding
`checkSystem` calls in the recursive traversal, which ensures
cancellation and heartbeat checks happen during what can be a very
expensive computation.

All callers of these functions were already in `MetaM`, so this change
is safe. The motivating case is the `4595_slowdown.lean` test, where
`hasAssignableMVar` (with `PersistentHashMap.find?` lookups on
`mctx.lDepth`) was the dominant CPU cost during elaboration of category
theory definitions. Without `checkSystem` calls, cancellation requests
could be delayed by over 2 seconds.

The test file `4595_slowdown.lean` gets a slightly increased
`maxHeartbeats` limit because `checkSystem` now detects heartbeat
exhaustion mid-traversal rather than after the function returns.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Basic
+public import Lean.Meta.HasAssignableMVar
 public import Lean.Meta.LevelDefEq
 public import Lean.Meta.WHNF
 public import Lean.Meta.InferType

src/Lean/Meta/AppBuilder.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.DecLevel
 import Lean.Meta.CtorRecognizer
+public import Lean.Meta.HasAssignableMVar
 import Lean.Structure
 import Init.Omega
 public section

src/Lean/Meta/HasAssignableMVar.lean

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Meta.Basic
+
+public section
+
+open Lean
+
+namespace Lean.Meta
+
+def isLevelMVarAssignable (mvarId : LMVarId) : MetaM Bool := do
+  let mctx ← getMCtx
+  match mctx.lDepth.find? mvarId with
+  | some d => return d >= mctx.levelAssignDepth
+  | _      => panic! s!"unknown universe metavariable {mvarId.name}"
+
+def hasAssignableLevelMVar : Level → MetaM Bool
+  | .succ lvl       => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl
+  | .max lvl₁ lvl₂  => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
+  | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
+  | .mvar mvarId    => isLevelMVarAssignable mvarId
+  | .zero           => return false
+  | .param _        => return false
+
+/-- Return `true` iff expression contains a metavariable that can be assigned. -/
+partial def hasAssignableMVar (e : Expr) : MetaM Bool :=
+  if !e.hasMVar then
+    return false
+  else
+    go e |>.run' {}
+where
+  go (e : Expr) : StateRefT ExprSet MetaM Bool :=
+    match e with
+    | .const _ lvls    => lvls.anyM (liftM <| hasAssignableLevelMVar ·)
+    | .sort lvl        => liftM <| hasAssignableLevelMVar lvl
+    | .app f a         => do checkSystem "hasAssignableMVar"; visit f <||> visit a
+    | .letE _ t v b _  => do checkSystem "hasAssignableMVar"; visit t <||> visit v <||> visit b
+    | .forallE _ d b _ => do checkSystem "hasAssignableMVar"; visit d <||> visit b
+    | .lam _ d b _     => do checkSystem "hasAssignableMVar"; visit d <||> visit b
+    | .fvar _          => return false
+    | .bvar _          => return false
+    | .lit _           => return false
+    | .mdata _ e       => visit e
+    | .proj _ _ e      => visit e
+    | .mvar mvarId     => mvarId.isAssignable
+  visit (e : Expr) : StateRefT ExprSet MetaM Bool := do
+    if !e.hasMVar then return false
+    if (← get).contains e then return false
+    modify fun s => s.insert e
+    go e
+
+end Lean.Meta
+
+end

src/Lean/Meta/LevelDefEq.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Util.CollectMVars
 public import Lean.Meta.DecLevel
+public import Lean.Meta.HasAssignableMVar
 
 public section
 

src/Lean/Meta/Sym/Pattern.lean

@@ -18,6 +18,7 @@ import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
 import Lean.Meta.Sym.Util
+import Lean.Meta.HasAssignableMVar
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
 import Std.Do.Triple.Basic

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Simp
 import Init.Grind.Util
 import Init.Omega
+public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Simp.Arith
 public import Lean.Meta.Tactic.Simp.Attr
 public import Lean.Meta.BinderNameHint
 import Lean.Meta.WHNF
+public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Simp
 /--

src/Lean/MetavarContext.lean

@@ -444,12 +444,6 @@ def _root_.Lean.MVarId.isAssignedOrDelayedAssigned [Monad m] [MonadMCtx m] (mvar
   let mctx ← getMCtx
   return mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId
 
-def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do
-  let mctx ← getMCtx
-  match mctx.lDepth.find? mvarId with
-  | some d => return d >= mctx.levelAssignDepth
-  | _      => panic! s!"unknown universe metavariable {mvarId.name}"
-
 def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
   match mctx.decls.find? mvarId with
   | some decl => decl
@@ -484,30 +478,6 @@ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool
   | .proj _ _ e      => pure e.hasMVar <&&> hasAssignedMVar e
   | .mvar mvarId     => mvarId.isAssigned <||> mvarId.isDelayedAssigned
 
-/-- Return true iff the given level contains a metavariable that can be assigned. -/
-def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool
-  | .succ lvl       => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl
-  | .max lvl₁ lvl₂  => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
-  | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
-  | .mvar mvarId    => isLevelMVarAssignable mvarId
-  | .zero           => return false
-  | .param _        => return false
-
-/-- Return `true` iff expression contains a metavariable that can be assigned. -/
-def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool
-  | .const _ lvls    => lvls.anyM hasAssignableLevelMVar
-  | .sort lvl        => hasAssignableLevelMVar lvl
-  | .app f a         => (pure f.hasMVar <&&> hasAssignableMVar f) <||> (pure a.hasMVar <&&> hasAssignableMVar a)
-  | .letE _ t v b _  => (pure t.hasMVar <&&> hasAssignableMVar t) <||> (pure v.hasMVar <&&> hasAssignableMVar v) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
-  | .forallE _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
-  | .lam _ d b _     => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
-  | .fvar _          => return false
-  | .bvar _          => return false
-  | .lit _           => return false
-  | .mdata _ e       => pure e.hasMVar <&&> hasAssignableMVar e
-  | .proj _ _ e      => pure e.hasMVar <&&> hasAssignableMVar e
-  | .mvar mvarId     => mvarId.isAssignable
-
 /--
   Add `mvarId := u` to the universe metavariable assignment.
   This method does not check whether `mvarId` is already assigned, nor does it check whether

tests/elab/4595_slowdown.lean

@@ -1,6 +1,8 @@
 -- The final declaration blew up by a factor of about 40x heartbeats on an earlier draft of
 -- https://github.com/leanprover/lean4/pull/4595, so this is here as a regression test.
 
+set_option maxHeartbeats 400000
+
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 section Mathlib.Combinatorics.Quiver.Basic

tests/elab/4595_slowdown.lean.out.expected

@@ -1,12 +1,12 @@
-4595_slowdown.lean:104:14-104:25: warning: declaration uses `sorry`
-4595_slowdown.lean:136:9-136:17: warning: declaration uses `sorry`
-4595_slowdown.lean:154:8-154:16: warning: declaration uses `sorry`
-4595_slowdown.lean:181:8-181:14: warning: declaration uses `sorry`
+4595_slowdown.lean:106:14-106:25: warning: declaration uses `sorry`
+4595_slowdown.lean:138:9-138:17: warning: declaration uses `sorry`
+4595_slowdown.lean:156:8-156:16: warning: declaration uses `sorry`
 4595_slowdown.lean:183:8-183:14: warning: declaration uses `sorry`
-4595_slowdown.lean:186:0-186:8: warning: declaration uses `sorry`
-4595_slowdown.lean:194:8-194:19: warning: declaration uses `sorry`
-4595_slowdown.lean:197:8-197:15: warning: declaration uses `sorry`
-4595_slowdown.lean:207:4-207:13: warning: declaration uses `sorry`
-4595_slowdown.lean:229:8-229:14: warning: declaration uses `sorry`
-4595_slowdown.lean:231:8-231:16: warning: declaration uses `sorry`
-4595_slowdown.lean:233:4-233:11: warning: declaration uses `sorry`
+4595_slowdown.lean:185:8-185:14: warning: declaration uses `sorry`
+4595_slowdown.lean:188:0-188:8: warning: declaration uses `sorry`
+4595_slowdown.lean:196:8-196:19: warning: declaration uses `sorry`
+4595_slowdown.lean:199:8-199:15: warning: declaration uses `sorry`
+4595_slowdown.lean:209:4-209:13: warning: declaration uses `sorry`
+4595_slowdown.lean:231:8-231:14: warning: declaration uses `sorry`
+4595_slowdown.lean:233:8-233:16: warning: declaration uses `sorry`
+4595_slowdown.lean:235:4-235:11: warning: declaration uses `sorry`