fix: variable must execute pending tactics and elaboration problems (…

…leanprover#4370)

closes leanprover#2226
closes leanprover#3214

src/Lean/Elab/BuiltinCommand.lean

@@ -229,7 +229,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
 @[builtin_command_elab «variable»] def elabVariable : CommandElab
   | `(variable $binders*) => do
     -- Try to elaborate `binders` for sanity checking
-    runTermElabM fun _ => Term.withAutoBoundImplicit <|
+    runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
       Term.elabBinders binders fun _ => pure ()
     for binder in binders do
       let binders ← replaceBinderAnnotation binder

tests/lean/run/2226.lean

@@ -0,0 +1,13 @@
+/--
+error: unsolved goals
+A : Nat
+⊢ Sort ?u.3
+-/
+#guard_msgs in
+variable (A : Nat) (B : by skip)
+
+def foo :=
+  A = B
+
+def boo :=
+  B

tests/lean/run/3214.lean

@@ -0,0 +1,12 @@
+class Foo (α : Type)
+
+/--
+error: function expected at
+  Missing
+term has type
+  ?m.9
+-/
+#guard_msgs in
+variable {α : Type} (s : Missing α)
+
+#synth Foo s