From 7c3826d3e971fd26409dcd2759ba25eaa10bfc5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 9 Sep 2022 14:29:48 -0700
Subject: [PATCH] fix: fixes #1576

---
 src/Lean/Elab/Tactic/Config.lean  | 4 +++-
 src/Lean/Meta/Eval.lean           | 3 +++
 tests/lean/1576.lean              | 1 +
 tests/lean/1576.lean.expected.out | 2 ++
 4 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/1576.lean
 create mode 100644 tests/lean/1576.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean
index 6bcb160731..cb05ee95a4 100644
--- a/src/Lean/Elab/Tactic/Config.lean
+++ b/src/Lean/Elab/Tactic/Config.lean
@@ -19,13 +19,15 @@ macro (name := configElab) doc?:(docComment)? "declare_config_elab" elabName:ide
      if optConfig.isNone then
        return { : $type }
      else
-       let c ← withoutModifyingState <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
+       let c ← withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext <| Term.withSynthesize do
          let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``$type)
          Term.synthesizeSyntheticMVarsNoPostponing
          instantiateMVars c
        eval c
   )
 
+#check @evalExpr'
+
 open Linter.MissingDocs in
 @[builtinMissingDocsHandler Elab.Tactic.configElab]
 def checkConfigElab : SimpleHandler := mkSimpleHandler "config elab"
diff --git a/src/Lean/Meta/Eval.lean b/src/Lean/Meta/Eval.lean
index a93853130a..5145a67df9 100644
--- a/src/Lean/Meta/Eval.lean
+++ b/src/Lean/Meta/Eval.lean
@@ -10,6 +10,9 @@ namespace Lean.Meta
 unsafe def evalExprCore (α) (value : Expr) (checkType : Expr → MetaM Unit) (safety := DefinitionSafety.safe) : MetaM α :=
   withoutModifyingEnv do
     let name ← mkFreshUserName `_tmp
+    let value ← instantiateMVars value
+    if value.hasMVar then
+      throwError "failed to evaluate expression, it contains metavariables{indentExpr value}"
     let type ← inferType value
     checkType type
     let decl := Declaration.defnDecl {
diff --git a/tests/lean/1576.lean b/tests/lean/1576.lean
new file mode 100644
index 0000000000..bfa141a069
--- /dev/null
+++ b/tests/lean/1576.lean
@@ -0,0 +1 @@
+example : True := by rw (config := non / sense) []
diff --git a/tests/lean/1576.lean.expected.out b/tests/lean/1576.lean.expected.out
new file mode 100644
index 0000000000..7ad0f7f2b8
--- /dev/null
+++ b/tests/lean/1576.lean.expected.out
@@ -0,0 +1,2 @@
+1576.lean:1:35-1:38: error: unknown identifier 'non'
+1576.lean:1:41-1:46: error: unknown identifier 'sense'