From 0a0f1d7cc717592d1014bf6ec929372654e97965 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 6 Jun 2024 15:06:18 +0200
Subject: [PATCH] fix: `variable` must execute pending tactics and elaboration
 problems (#4370)

closes #2226
closes #3214
---
 src/Lean/Elab/BuiltinCommand.lean |  2 +-
 tests/lean/run/2226.lean          | 13 +++++++++++++
 tests/lean/run/3214.lean          | 12 ++++++++++++
 3 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/2226.lean
 create mode 100644 tests/lean/run/3214.lean

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