extends generates non ctrl+clickable constants, causing ctrl+click to lead to the wrong definition

[JovanGerb]

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

When using the extends keyword for defining classes, the generated projection function is not ctrl-clickable. This can cause ctrl+clicking on the constant to lead to the definition of a different constant.

Context

I was ctrl+clicking on type class projection functions, and got really confused, because it went to the wrong definition.

Steps to Reproduce

Minimal example:

class A (n : Nat)

class B (n : Nat) extends A n

instance {n : Nat} : B n where

variable [i : B 3]

#check i.toA

#check (inferInstance : B 4).toA

In this code, put the cursor on either i.toA, or (inferInstance : B 4).toA. Then go to the infoview and ctrl+click on .toA.

Expected behavior: [Clear and concise description of what you expect to happen]

ctrl+click on .toA leads to the definition of class B.

Actual behavior: [Clear and concise description of what actually happens]

ctrl+click at i.toA doesn't work.
ctrl+click at (inferInstance : B 4).toA leads to the definition of instance instOfNatNat.

Versions

4.11.0-nightly-2024-07-03

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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

[mhuisi]

This looks like a duplicate of #3063.

[JovanGerb]

You're right, sorry about that.

[mhuisi]

Closed for being a duplicate of #3063.