Implicitness update changes the first occurence rather than the last

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

It's convenient that Lean 4 allows using the same name for multiple variables; normally, only the last occurrence of the name will be accessible, and all previous ones will be shadowed. However, this behavior is not respected by implicitness updates:

variable (R : Type _) [Add R]
variable (R : Type _) [Mul R]
variable {R} -- this update changes the first R to an implicit variable, but does nothing to the second.
 
theorem add_eq_add (r : R) : r * r = r * r := rfl
#print add_eq_add
/- theorem add_eq_add.{u_1} : ∀ (R : Type u_1) [inst : Mul R] (r : R), r * r = r * r :=
fun R [Mul R] r => rfl 
This is the second R and it remains explicit. -/

If the first R is already implicit, we get an error:

variable {R : Type _} [Add R]
variable (R : Type _) [Mul R]
variable {R} /- redundant binder annotation update -/

It makes no sense to update the first R, since there is no way to refer to it in theorem statements.

Steps to Reproduce

Paste the snippet above into an editor.

Expected behavior: the second R should be made implicit by variable {R}

Actual behavior: the first R is made implicit by variable {R} but the second R remains explicit

Versions

"4.5.0-rc1"
Lean 4 Web Editor (https://live.lean-lang.org/)

Impact

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

Start by reproducing the minimal variable-shadowing snippet in the Lean 4 Web Editor and compare the printed theorem with the expected behavior. Trace the implicitness update handling for repeated variable names; done means variable {R} updates the last, accessible R and reports redundancy only when that binder is already implicit.