jump-to-definition for instances to parent classes

[fpvandoorn]

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

Jump-to-definition doesn't work for automatically generated instances to parent classes, see the MWE below.

class MySemigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class MyMulComm (G : Type u) extends Mul G where
  mul_comm : ∀ a b : G, a * b = b * a

class MyCommSemigroup (G : Type u) extends MySemigroup G, MyMulComm G

#check MySemigroup -- jump to definition works
#check MySemigroup.mul_assoc -- jump to definition works
#check MySemigroup.toMul -- jump to definition doesn't work
#check MyCommSemigroup.toMySemigroup -- jump to definition doesn't work
#check MyCommSemigroup.toMyMulComm -- jump to definition doesn't work

Expected behavior: jumping to all these declarations should work with F12 (it should jump to the line containing the class (or extends) command.

Versions

4.4.0-rc1

Impact

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