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
2025-02-05 10:43:54 -05:00 · 2025-02-05 10:43:54 -05:00 · 60aeb79a75
commit 60aeb79a75
parent f1ed830b9a
5 changed files with 211 additions and 101 deletions
--- 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]

--- 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;
--- a/tests/lean/run/varBinderUpdate.lean
+++ 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
--- a/tests/lean/varBinderUpdate.lean
+++ b/tests/lean/varBinderUpdate.lean
@ -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
--- a/tests/lean/varBinderUpdate.lean.expected.out
+++ b/tests/lean/varBinderUpdate.lean.expected.out
@ -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