diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index fcf486aefae5..a84ad444de67 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/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
diff --git a/tests/lean/run/2226.lean b/tests/lean/run/2226.lean
new file mode 100644
index 000000000000..ca9a89905fda
--- /dev/null
+++ b/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
diff --git a/tests/lean/run/3214.lean b/tests/lean/run/3214.lean
new file mode 100644
index 000000000000..09e45bc81dfc
--- /dev/null
+++ 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