Mixing binder updates and variable declarations gives confusing errors

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The variable command is used both to declare new variables, and to update the binder type (implicit / explicit / instance implicit) of existing variables.

Using both features at the same time can produce error messages that advise the user to make things even worse

Context

Zulip thread

Steps to Reproduce

Run the following code

class one (A : Nat)
class two (A : Nat) [one A] := t : Nat

variable (A : Nat) [one A]

section fails
variable {A} [two A]
/-
failed to synthesize instance
  one A
-/
end fails

section bad_advice
-- ok, the error told me to write `one A` again I guess
variable {A} [one A] [two A]

example : True := 
  -- put your cursor here; now `one A` is here twice!
  trivial

end bad_advice

section works
variable {A} [two (by exact A)]
end works

section also_works
variable {A}
variable [two A]
end also_works

Expected behavior: The section fails should either succeed, or it should emit an error message that does not encourage me to write section bad_advice. If you put your cursor at the exact, A should appear once in the goal view.
Actual behavior: The error message tricks me into making a mess of duplicate variables. Putting the cursor at exact shows A twice (as there are two copies!).

Versions

4.2.0-rc4 on the web editor

Impact

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

[Kha]

Fixed in #5142