From cc520d422cac299217acfe5e7cc7cebf63d96663 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Sep 2020 07:18:43 -0700
Subject: [PATCH] fix: ensure no unassigned mvars at #eval

---
 src/Lean/Elab/Command.lean                |  1 +
 tests/lean/evalWithMVar.lean              | 13 +++++++++++++
 tests/lean/evalWithMVar.lean.expected.out |  9 +++++++++
 3 files changed, 23 insertions(+)
 create mode 100644 tests/lean/evalWithMVar.lean
 create mode 100644 tests/lean/evalWithMVar.lean.expected.out

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 477c1130b1..30a620d02b 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -533,6 +533,7 @@ fun stx => do
     type ← inferType value;
     let decl := Declaration.defnDecl { name := n, lparams := [], type := type,
       value := value, hints := ReducibilityHints.opaque, isUnsafe := true };
+    Term.ensureNoUnassignedMVars decl;
     addAndCompile decl
   };
   let elabMetaEval : CommandElabM Unit := runTermElabM (some n) fun _ => do {
diff --git a/tests/lean/evalWithMVar.lean b/tests/lean/evalWithMVar.lean
new file mode 100644
index 0000000000..6efec2acdf
--- /dev/null
+++ b/tests/lean/evalWithMVar.lean
@@ -0,0 +1,13 @@
+new_frontend
+
+def c {α} : Sum α Nat :=
+Sum.inr 10
+
+def Sum.someRight {α β} (s : Sum α β) : Option β :=
+match s with
+| Sum.inl _ => none
+| Sum.inr b => some b
+
+#check Sum.someRight c
+
+#eval Sum.someRight c
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
new file mode 100644
index 0000000000..8bc19e8414
--- /dev/null
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -0,0 +1,9 @@
+Sum.someRight c : Option Nat
+evalWithMVar.lean:13:6: error: don't know how to synthesize placeholder
+  @Sum.someRight ?m.177 … …
+context:
+⊢ Type ?
+evalWithMVar.lean:13:20: error: don't know how to synthesize placeholder
+  @c ?m.177
+context:
+⊢ Type ?