feat: report errors an unassigned metavars at #eval

See #1256

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

tests/lean/evalNone.lean

@@ -0,0 +1,3 @@
+#eval none
+
+#eval [].head?

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

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