Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

One can only update the implicitness of binders from () to {} and back. [] cannot be switched to nor from, and ⦃⦄ cannot be switched to (but can be switched from).

Context

In mathlib's measure theory library, we strive to make all MeasurableSpace arguments implicit, unless they are required to be instance arguments for unification purposes. The reason is that mathematically one often wants to consider non-canonical sigma-algebras on a given type (they usually are sigma-subalgebras of a fixed canonical sigma-algebra).

If binder updates towards instance arguments worked, we could do

variable {A : Type} {mA : MeasurableSpace A} -- possibly more instances on `A` here

theorem foo := sorry

theorem bar := sorry

variable (mA) in
def baz := sorry

instead of

-- same thing up to here

def baz {A : Type} [MeasurableSpace A] -- possibly more instances on `A` here
  := sorry

Steps to Reproduce

Consider the following code:

class Foo


variable {foo : Foo}

variable (foo) -- works

variable [foo]
/-
type expected, got
  (foo : Foo)
-/

variable ⦃foo⦄
/-
unexpected syntax
  variable ⦃foo⦄
-/


variable [foo2 : Foo]

variable {foo2}
/-
cannot change the binder annotation of the previously declared local instance `foo2`
-/

variable (foo2)
/-
cannot change the binder annotation of the previously declared local instance `foo2`
-/


variable ⦃foo3 : Foo⦄

variable {foo3} -- works
variable (foo3) -- works

Expected behavior: All binder updates succeed.

Actual behavior: Only some do. Other error in various ways.

Versions

Lean 4.14.0-rc2
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.