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 ?