fix: #guard should work with the module system (#10535)

This PR ensures that `#guard` can be called under the module system
without issues.

Author: hargoniX

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

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}"