Autocomplete shows incorrect type

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

Consider this code:

variable (a : Vector Bool 3)

#check a.set

When I put my cursor at the end of the code and trigger autocomplete via Ctrl+Space, then I get various suggestions. At the top are the two suggestions I expect: set and set! (both Vector.set and Vector.set! exist). However, the type signature shown as part of the autocomplete box is not always correct, and it seems to depend on the version. When I try this on live.lean-lang.org with the "latest nightly" setting, which is Lean version 4.19.0-nightly-2025-03-22, I see the following two types:

The first is clearly wrong, the second one is right.

In my local project, which uses the toolchain leanprover/lean4:v4.17.0, I get the following:

So here the first is right and the second is wrong.

Versions

See above.

Impact

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

Start by running the minimal Vector Bool 3 example in the issue on the referenced Lean versions and compare the two autocomplete signatures. Trace the autocomplete path that produces the set and set! suggestions. Done means both displayed types consistently match the corresponding Vector.set and Vector.set! declarations.