diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 3b019066f86..afd0add1b63 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -151,17 +151,24 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
 open Lean.Parser.Term
 
 private def typelessBinder? : Syntax → Option (Array (TSyntax [`ident, `Lean.Parser.Term.hole]) × BinderInfo)
-  | `(bracketedBinderF|($ids*)) => some (ids, .default)
-  | `(bracketedBinderF|{$ids*}) => some (ids, .implicit)
-  | `(bracketedBinderF|⦃$ids*⦄)  => some (ids, .strictImplicit)
-  | _                           => none
+  | `(bracketedBinderF|($ids*))     => some (ids, .default)
+  | `(bracketedBinderF|{$ids*})     => some (ids, .implicit)
+  | `(bracketedBinderF|⦃$ids*⦄)     => some (ids, .strictImplicit)
+  | `(bracketedBinderF|[$id:ident]) => some (#[id], .instImplicit)
+  | _                               => none
 
 /--  If `id` is an identifier, return true if `ids` contains `id`. -/
 private def containsId (ids : Array (TSyntax [`ident, ``Parser.Term.hole])) (id : TSyntax [`ident, ``Parser.Term.hole]) : Bool :=
   id.raw.isIdent && ids.any fun id' => id'.raw.getId == id.raw.getId
 
+/-- Elaborates `binders` using `withSynthesize` and `withAutoBoundImplicit`. -/
+private def elabBindersSynthesizingAutoBound (binders : TSyntaxArray ``bracketedBinder) :=
+  runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
+    Term.elabBinders binders fun _ => pure ()
+
 /--
-  Auxiliary method for processing binder annotation update commands: `variable (α)` and `variable {α}`.
+  Auxiliary method for processing binder annotation update commands:
+  `variable (α)`, `variable {α}`, `variable ⦃α⦄`, and `variable [α]`.
   The argument `binder` is the binder of the `variable` command.
   The method returns an array containing the "residue", that is, variables that do not correspond to updates.
   Recall that a `bracketedBinder` can be of the form `(x y)`.
@@ -211,12 +218,22 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
         | .implicit => `(bracketedBinderF| {$id $[: $ty?]?})
         | .strictImplicit => `(bracketedBinderF| {{$id $[: $ty?]?}})
         | .instImplicit => do
-          let some ty := ty? | throwErrorAt id "instance-implicit binders must provide an explicit type"
+          let some ty := ty?
+            | throwErrorAt binder "cannot update binder annotation of variable `{id}` to instance-implicit:\n\
+                variable was originally declared without an explicit type"
           `(bracketedBinderF| [$(⟨id⟩) : $ty])
       for id in ids.reverse do
         if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
           binderIds := binderIds.eraseIdx idx
           modifiedVarDecls := true
+          let newBinder ← mkBinder id binderInfo
+          if binderInfo.isInstImplicit then
+            -- We elaborate the new binder to make sure it's valid as instance-implicit
+            try
+              elabBindersSynthesizingAutoBound #[newBinder]
+            catch e =>
+              throwErrorAt binder m!"cannot update binder annotation of variable `{id}` to instance-implicit:\n\
+                {e.toMessageData}"
           varDeclsNew := varDeclsNew.push (← mkBinder id binderInfo)
         else
           varDeclsNew := varDeclsNew.push (← mkBinder id binderInfo')
@@ -228,7 +245,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
         | .default => `(bracketedBinderF| ($binderId))
         | .implicit => `(bracketedBinderF| {$binderId})
         | .strictImplicit => `(bracketedBinderF| {{$binderId}})
-        | .instImplicit => throwErrorAt binderId "instance-implicit binders must provide an explicit type"
+        | .instImplicit => throwUnsupportedSyntax
   else
     return #[binder]
 
@@ -236,8 +253,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
   | `(variable $binders*) => do
     let binders ← binders.flatMapM replaceBinderAnnotation
     -- Try to elaborate `binders` for sanity checking
-    runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
-      Term.elabBinders binders fun _ => pure ()
+    elabBindersSynthesizingAutoBound binders
     -- Remark: if we want to produce error messages when variables shadow existing ones, here is the place to do it.
     for binder in binders do
       let varUIds ← (← getBracketedBinderIds binder) |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)
diff --git a/tests/lean/run/varBinderUpdate.lean b/tests/lean/run/varBinderUpdate.lean
new file mode 100644
index 00000000000..febb7d22c45
--- /dev/null
+++ b/tests/lean/run/varBinderUpdate.lean
@@ -0,0 +1,192 @@
+/-!
+  # Changing variable binder annotations
+
+  Tests the use of the `variable` command to update the binder annotations of existing variables. -/
+
+/-! Test updating between default and implicit annotations. -/
+
+namespace Ex1
+
+variable {α : Type}
+variable [Add α]
+variable (α)
+def f (a : α) := a + a
+/--
+info: f Nat 5 : Nat
+-/
+#guard_msgs in
+#check f Nat 5
+variable {α}
+def g (b : α) := b
+/--
+info: g 5 : Nat
+-/
+#guard_msgs in
+#check g 5
+/--
+info: Ex1.f (α : Type) [Add α] (a : α) : α
+-/
+#guard_msgs in
+#check f
+/--
+info: Ex1.g {α : Type} (b : α) : α
+-/
+#guard_msgs in
+#check g
+end Ex1
+
+namespace Ex2
+
+variable {α β : Type}
+variable (α)
+def f (a : α) := a
+def g (b : β) := b
+/--
+info: f Nat 5 : Nat
+-/
+#guard_msgs in
+#check f Nat 5
+/--
+info: g 5 : Nat
+-/
+#guard_msgs in
+#check g 5
+/--
+info: Ex2.f (α : Type) (a : α) : α
+-/
+#guard_msgs in
+#check f
+/--
+info: Ex2.g {β : Type} (b : β) : β
+-/
+#guard_msgs in
+#check g
+/--
+error: redundant binder annotation update
+-/
+#guard_msgs in
+variable (α)
+end Ex2
+
+namespace Ex3
+
+variable {α : Type}
+variable (f : α → α)
+variable (α)
+def g (a : α) := f a
+/--
+info: Ex3.g (α : Type) (f : α → α) (a : α) : α
+-/
+#guard_msgs in
+#check g
+variable {f}
+def h (a : α) := f a
+/--
+info: Ex3.h (α : Type) {f : α → α} (a : α) : α
+-/
+#guard_msgs in
+#check h
+end Ex3
+
+namespace Ex4
+
+variable {α β : Type}
+variable (α γ)
+def g (a : α) (b : β) (c : γ) := (a, b, c)
+/--
+info: g Nat Bool 10 "hello" true : Nat × String × Bool
+-/
+#guard_msgs in
+#check g Nat Bool 10 "hello" true
+end Ex4
+
+/-! Test updating from and to instance-implicit. -/
+
+namespace Ex5
+
+variable [i : Add α]
+variable (i)
+def f (x y : α) := x + y
+/--
+info: Ex5.f.{u_1} {α : Type u_1} (i : Add α) (x y : α) : α
+-/
+#guard_msgs in
+#check f
+variable [i]
+def g (x y : α) := x + y
+/--
+info: Ex5.g.{u_1} {α : Type u_1} [i : Add α] (x y : α) : α
+-/
+#guard_msgs in
+#check g
+end Ex5
+
+/-! Test that variables with default values/tactics cannot be updated. -/
+
+namespace Ex6
+
+variable (a : Nat)
+variable (h : a = a := rfl)
+/--
+error: cannot update binder annotation of variables with default values/tactics
+-/
+#guard_msgs in
+variable {h}
+end Ex6
+
+/-! Test that variables that cannot be instance-implicit fail to be updated thereto. -/
+
+namespace Ex7
+
+variable (n : Nat)
+/--
+error: cannot update binder annotation of variable `n` to instance-implicit:
+invalid binder annotation, type is not a class instance
+  Nat
+use the command `set_option checkBinderAnnotations false` to disable the check
+-/
+#guard_msgs in
+variable [n]
+variable (x)
+/--
+error: cannot update binder annotation of variable `x` to instance-implicit:
+variable was originally declared without an explicit type
+-/
+#guard_msgs in
+variable [x]
+end Ex7
+
+/-! Test updating to and from strict-implicit annotations. -/
+
+namespace Ex8
+
+variable {α : Type} (β : Type)
+variable ⦃α⦄
+def f (a : α) (_ : β) := a
+/--
+info: Ex8.f ⦃α : Type⦄ (β : Type) (a : α) : β → α
+-/
+#guard_msgs in
+#check f
+variable (α)
+variable ⦃β⦄
+def g (a : α) (b : β) := (a, b)
+/--
+info: Ex8.g (α : Type) ⦃β : Type⦄ (a : α) (b : β) : α × β
+-/
+#guard_msgs in
+#check g
+variable {β}
+def h (b : β) := b
+/--
+info: Ex8.h {β : Type} (b : β) : β
+-/
+#guard_msgs in
+#check h
+variable {{β}}
+/--
+error: redundant binder annotation update
+-/
+#guard_msgs in
+variable ⦃β⦄
+end Ex8
diff --git a/tests/lean/varBinderUpdate.lean b/tests/lean/varBinderUpdate.lean
deleted file mode 100644
index 2710b16bdbe..00000000000
--- a/tests/lean/varBinderUpdate.lean
+++ /dev/null
@@ -1,61 +0,0 @@
-namespace Ex1
-
-variable {α : Type}
-variable [Add α]
-variable (α)
-def f (a : α) := a + a
-#check f Nat 5
-variable {α}
-def g (b : α) := b
-#check g 5
-#check f
-#check g
-end Ex1
-
-namespace Ex2
-
-variable {α β : Type}
-variable (α)
-def f (a : α) := a
-def g (b : β) := b
-#check f Nat 5
-#check g 5
-#check f
-#check g
-variable (α)
-end Ex2
-
-namespace Ex3
-
-variable {α : Type}
-variable (f : α → α)
-variable (α)
-def g (a : α) := f a
-#check g
-variable {f}
-def h (a : α) := f a
-#check h
-end Ex3
-
-namespace Ex4
-
-variable {α β : Type}
-variable (α γ)
-def g (a : α) (b : β) (c : γ) := (a, b, c)
-#check g Nat Bool 10 "hello" true
-end Ex4
-
-namespace Ex5
-
-variable [i : Add α]
-variable (i) -- Error
-
-end Ex5
-
-namespace Ex6
-
-variable (a : Nat)
-variable (h : a = a := rfl)
-variable {h} -- Error
-
-end Ex6
diff --git a/tests/lean/varBinderUpdate.lean.expected.out b/tests/lean/varBinderUpdate.lean.expected.out
deleted file mode 100644
index b23fdb0d800..00000000000
--- a/tests/lean/varBinderUpdate.lean.expected.out
+++ /dev/null
@@ -1,14 +0,0 @@
-f Nat 5 : Nat
-g 5 : Nat
-Ex1.f (α : Type) [Add α] (a : α) : α
-Ex1.g {α : Type} (b : α) : α
-f Nat 5 : Nat
-g 5 : Nat
-Ex2.f (α : Type) (a : α) : α
-Ex2.g {β : Type} (b : β) : β
-varBinderUpdate.lean:25:10-25:11: error: redundant binder annotation update
-Ex3.g (α : Type) (f : α → α) (a : α) : α
-Ex3.h (α : Type) {f : α → α} (a : α) : α
-g Nat Bool 10 "hello" true : Nat × String × Bool
-varBinderUpdate.lean:51:10-51:11: error: cannot change the binder annotation of the previously declared local instance `i`
-varBinderUpdate.lean:59:10-59:11: error: cannot update binder annotation of variables with default values/tactics