Borrow annotation affects auto-completion

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

Adding borrowing annotation to an argument breaks auto-completion of its fields.

Steps to Reproduce

structure A where
  n : Nat

opaque f (a : @& A) (i : Fin a.n) : Nat

Expected behavior: when typing "." after "Fin a" the provided auto-completion choice is as if a had type A: "n".

Actual behavior: the provided auto-completion is: "a", "abbrev", ...

Versions

Lean (version 4.2.0-rc1, commit a62d2fd49796, Release)
Lean (version 4.1.0, commit a832f398b80a, Release)
Linux fedora 6.5.6-200.fc38.x86_64

Additional Information

There is a commit referencing this issue: 3318c75.

Impact

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

Start with the minimal Lean reproduction in the issue and run it against the listed Lean versions. Trace the auto-completion behavior after Fin a. for the borrowed a; done means the completion includes n, as it would for type A.