Info view term hover shows field notation docs instead of docstring of hovered constant

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

MWE:

example (l : List Nat) : l.get = l.get := _

Context

n/a

Steps to Reproduce

1. put cursor on _ in MWE
2. hover over get in expected type

Expected behavior: See List.get docstring, possibly followed by field notation documentation

Actual behavior: Only field notation docs are shown

Versions

4.16.0-rc2

Additional Information

n/a

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 example in the issue on the Lean nightly release or live. Trace the info view's hover handling for get in the expected type and compare it with the field notation documentation path. Done means hovering List.get shows its docstring, optionally followed by the field notation documentation.