From 60aeb79a75974c3197a8606f90dea18985307f8a Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Wed, 5 Feb 2025 10:43:54 -0500
Subject: [PATCH] feat: allow updating binders to and from strict- and
 instance-implicit (#6634)

This PR adds support for changing the binder annotations of existing
variables to and from strict-implicit and instance-implicit using the
`variable` command.

This PR requires a stage0 update to fully take effect.

Closes #6078
---
 src/Lean/Elab/BuiltinCommand.lean            |  69 +++++---
 stage0/src/stdlib_flags.h                    |   2 +
 tests/lean/run/varBinderUpdate.lean          | 166 +++++++++++++++++++
 tests/lean/varBinderUpdate.lean              |  61 -------
 tests/lean/varBinderUpdate.lean.expected.out |  14 --
 5 files changed, 211 insertions(+), 101 deletions(-)
 create mode 100644 tests/lean/run/varBinderUpdate.lean
 delete mode 100644 tests/lean/varBinderUpdate.lean
 delete mode 100644 tests/lean/varBinderUpdate.lean.expected.out

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 36f24ecc1e..7734a59ccc 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -148,17 +148,20 @@ 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]) × Bool)
-  | `(bracketedBinderF|($ids*)) => some (ids, true)
-  | `(bracketedBinderF|{$ids*}) => some (ids, false)
-  | _                          => none
+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)
+  | `(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
 
 /--
-  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)`.
@@ -169,7 +172,7 @@ private def containsId (ids : Array (TSyntax [`ident, ``Parser.Term.hole])) (id
   The second `variable` command updates the binder annotation for `α`, and returns "residue" `γ`.
 -/
 private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBinder) : CommandElabM (Array (TSyntax ``Parser.Term.bracketedBinder)) := do
-  let some (binderIds, explicit) := typelessBinder? binder | return #[binder]
+  let some (binderIds, binderInfo) := typelessBinder? binder | return #[binder]
   let varDecls := (← getScope).varDecls
   let mut varDeclsNew := #[]
   let mut binderIds := binderIds
@@ -177,23 +180,22 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
   let mut modifiedVarDecls := false
   -- Go through declarations in reverse to respect shadowing
   for varDecl in varDecls.reverse do
-    let (ids, ty?, explicit') ← match varDecl with
+    let (ids, ty?, binderInfo') ← match varDecl with
       | `(bracketedBinderF|($ids* $[: $ty?]? $(annot?)?)) =>
         if annot?.isSome then
           for binderId in binderIds do
             if containsId ids binderId then
               throwErrorAt binderId "cannot update binder annotation of variables with default values/tactics"
-        pure (ids, ty?, true)
+        pure (ids, ty?, .default)
       | `(bracketedBinderF|{$ids* $[: $ty?]?}) =>
-        pure (ids, ty?, false)
-      | `(bracketedBinderF|[$id : $_]) =>
-        for binderId in binderIds do
-          if binderId.raw.isIdent && binderId.raw.getId == id.getId then
-            throwErrorAt binderId "cannot change the binder annotation of the previously declared local instance `{id.getId}`"
-        varDeclsNew := varDeclsNew.push varDecl; continue
+        pure (ids, ty?, .implicit)
+      | `(bracketedBinderF|⦃$ids* $[: $ty?]?⦄) =>
+        pure (ids, ty?, .strictImplicit)
+      | `(bracketedBinderF|[$id : $ty]) =>
+        pure (#[⟨id⟩], some ty, .instImplicit)
       | _ =>
         varDeclsNew := varDeclsNew.push varDecl; continue
-    if explicit == explicit' then
+    if binderInfo == binderInfo' then
       -- no update, ensure we don't have redundant annotations.
       for binderId in binderIds do
         if containsId ids binderId then
@@ -203,26 +205,41 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
       -- `binderIds` and `ids` are disjoint
       varDeclsNew := varDeclsNew.push varDecl
     else
-      let mkBinder (id : TSyntax [`ident, ``Parser.Term.hole]) (explicit : Bool) : CommandElabM (TSyntax ``Parser.Term.bracketedBinder) :=
-        if explicit then
-          `(bracketedBinderF| ($id $[: $ty?]?))
-        else
-          `(bracketedBinderF| {$id $[: $ty?]?})
+      let mkBinder (id : TSyntax [`ident, ``Parser.Term.hole]) (binderInfo : BinderInfo) : CommandElabM (TSyntax ``Parser.Term.bracketedBinder) :=
+        match binderInfo with
+        | .default => `(bracketedBinderF| ($id $[: $ty?]?))
+        | .implicit => `(bracketedBinderF| {$id $[: $ty?]?})
+        | .strictImplicit => `(bracketedBinderF| {{$id $[: $ty?]?}})
+        | .instImplicit => do
+          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
-          varDeclsNew := varDeclsNew.push (← mkBinder id explicit)
+          let newBinder ← mkBinder id binderInfo
+          if binderInfo.isInstImplicit then
+            -- We elaborate the new binder to make sure it's valid as instance implicit
+            try
+              runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
+                Term.elabBinder newBinder fun _ => pure ()
+            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 explicit')
+          varDeclsNew := varDeclsNew.push (← mkBinder id binderInfo')
   if modifiedVarDecls then
     modifyScope fun scope => { scope with varDecls := varDeclsNew.reverse }
   if binderIds.size != binderIdsIniSize then
     binderIds.mapM fun binderId =>
-      if explicit then
-        `(bracketedBinderF| ($binderId))
-      else
-        `(bracketedBinderF| {$binderId})
+      match binderInfo with
+        | .default => `(bracketedBinderF| ($binderId))
+        | .implicit => `(bracketedBinderF| {$binderId})
+        | .strictImplicit => `(bracketedBinderF| {{$binderId}})
+        | .instImplicit => throwUnsupportedSyntax
   else
     return #[binder]
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index b647d85f37..ee225c1734 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/varBinderUpdate.lean b/tests/lean/run/varBinderUpdate.lean
new file mode 100644
index 0000000000..239fde2741
--- /dev/null
+++ b/tests/lean/run/varBinderUpdate.lean
@@ -0,0 +1,166 @@
+/-!
+  # 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
+variable (f : α → α)
+variable {f γ α}
+def h (a : α) (c : γ) := (f a, c)
+/-- info: Ex4.h.{u_1} {α : Type} {γ : Type u_1} {f : α → α} (a : α) (c : γ) : α × γ -/
+#guard_msgs in
+#check h
+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}
+/-- error: cannot update binder annotation of variables with default values/tactics -/
+#guard_msgs in
+variable {a h}
+def f := a
+/-- info: Ex6.f (a : Nat) : Nat -/
+#guard_msgs in
+#check f
+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 (α) ⦃β γ⦄
+def g (a : α) (b : β) (c : γ) := (a, b, c)
+/-- info: Ex8.g (α : Type) ⦃β γ : Type⦄ (a : α) (b : β) (c : γ) : α × β × γ -/
+#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 2710b16bdb..0000000000
--- 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 b23fdb0d80..0000000000
--- 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