From 15e2a7d5b454a1e22ede0acf7c050cee7fba18e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jun 2022 11:50:21 -0700
Subject: [PATCH] feat: report errors an unassigned metavars at `#eval`

See #1256
---
 src/Lean/Elab/BuiltinCommand.lean         |  1 +
 tests/lean/evalNone.lean                  |  3 +++
 tests/lean/evalNone.lean.expected.out     | 12 ++++++++++++
 tests/lean/evalWithMVar.lean.expected.out |  4 ++--
 4 files changed, 18 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/evalNone.lean
 create mode 100644 tests/lean/evalNone.lean.expected.out

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 6db18e4182..63474f773e 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -324,6 +324,7 @@ unsafe def elabEvalUnsafe : CommandElab
     let elabEvalTerm : TermElabM Expr := do
       let e ← Term.elabTerm term none
       Term.synthesizeSyntheticMVarsNoPostponing
+      if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then throwAbortTerm
       if (← isProp e) then
         mkDecide e
       else
diff --git a/tests/lean/evalNone.lean b/tests/lean/evalNone.lean
new file mode 100644
index 0000000000..f83f87b4f5
--- /dev/null
+++ b/tests/lean/evalNone.lean
@@ -0,0 +1,3 @@
+#eval none
+
+#eval [].head?
diff --git a/tests/lean/evalNone.lean.expected.out b/tests/lean/evalNone.lean.expected.out
new file mode 100644
index 0000000000..7fdcd9ce11
--- /dev/null
+++ b/tests/lean/evalNone.lean.expected.out
@@ -0,0 +1,12 @@
+evalNone.lean:1:6-1:10: error: don't know how to synthesize implicit argument
+  @none ?m
+context:
+⊢ Type ?u
+evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
+  @List.head? ?m []
+context:
+⊢ Type ?u
+evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
+  @List.nil ?m
+context:
+⊢ Type ?u
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
index 3a24ada2c6..350971fecd 100644
--- a/tests/lean/evalWithMVar.lean.expected.out
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -2,10 +2,10 @@ Sum.someRight c : Option Nat
 evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
   @c ?m
 context:
-⊢ Type u_1
+⊢ Type ?u
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m Nat c
 context:
-⊢ Type u_1
+⊢ Type ?u
 Sum.someRight c : Option Nat
 Sum.someRight c : Option Nat