From 2e5bbf459640ea38ab61bf22dd895daeeffa78ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 24 Sep 2025 09:38:10 +0200
Subject: [PATCH] fix: #guard should work with the module system (#10535)

This PR ensures that `#guard` can be called under the module system
without issues.
---
 src/Lean/Elab/Tactic/Guard.lean |  2 +-
 src/Lean/Meta/Eval.lean         | 15 +++++++++------
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Guard.lean b/src/Lean/Elab/Tactic/Guard.lean
index 1f52015cac..4ca6c5b5d7 100644
--- a/src/Lean/Elab/Tactic/Guard.lean
+++ b/src/Lean/Elab/Tactic/Guard.lean
@@ -160,7 +160,7 @@ def evalGuardCmd : Lean.Elab.Command.CommandElab
     let e ← instantiateMVars e
     let mvars ← getMVars e
     if mvars.isEmpty then
-      let v ← unsafe evalExpr Bool (mkConst ``Bool) e
+      let v ← unsafe evalExpr (checkMeta := false) Bool (mkConst ``Bool) e
       unless v do
         throwError "Expression{indentExpr e}\ndid not evaluate to `true`"
     else
diff --git a/src/Lean/Meta/Eval.lean b/src/Lean/Meta/Eval.lean
index b49612c728..9e4bf3177e 100644
--- a/src/Lean/Meta/Eval.lean
+++ b/src/Lean/Meta/Eval.lean
@@ -14,7 +14,8 @@ public section
 
 namespace Lean.Meta
 
-unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (safety := DefinitionSafety.safe) : MetaM α :=
+unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit)
+    (safety := DefinitionSafety.safe) (checkMeta : Bool := true) : MetaM α :=
   withoutModifyingEnv do
     -- Avoid waiting for all prior compilation if only imported constants are referenced. This is a
     -- very common case for tactic configurations (`Lean.Elab.Tactic.Config`).
@@ -39,16 +40,18 @@ unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (s
     -- `Task.get` blocking debug code
     withOptions (Elab.async.set · false) do
       addAndCompile decl
-      evalConst α name
+      evalConst (checkMeta := checkMeta) α name
 
-unsafe def evalExpr' (α) (typeName : Name) (value : Expr) (safety := DefinitionSafety.safe) : MetaM α :=
-  evalExprCore (safety := safety) α value fun type => do
+unsafe def evalExpr' (α) (typeName : Name) (value : Expr) (safety := DefinitionSafety.safe)
+    (checkMeta : Bool := true) : MetaM α :=
+  evalExprCore (safety := safety) (checkMeta := checkMeta) α value fun type => do
     let type ← whnfD type
     unless type.isConstOf typeName do
       throwError "unexpected type at evalExpr{indentExpr type}"
 
-unsafe def evalExpr (α) (expectedType : Expr) (value : Expr) (safety := DefinitionSafety.safe) : MetaM α :=
-  evalExprCore (safety := safety) α value fun type => do
+unsafe def evalExpr (α) (expectedType : Expr) (value : Expr) (safety := DefinitionSafety.safe)
+    (checkMeta : Bool := true) : MetaM α :=
+  evalExprCore (safety := safety) (checkMeta := checkMeta) α value fun type => do
     unless ← isDefEq type expectedType do
       throwError "unexpected type at `evalExpr` {← mkHasTypeButIsExpectedMsg type expectedType}"