fix: ensure no unassigned mvars at #eval

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 {

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

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 ?