redundant instances when extending overlapping classes

Stream: lean4

[Yuyang Zhao]

import Lean.Meta.Instances

class A
class B
class C extends A, B
class D extends A, C
structure E extends A, C

#eval Lean.Meta.getInstancePriority? `D.toB -- some 1000
#eval Lean.Meta.getInstancePriority? `E.toB -- some 1000

It seems like Lean generates instances for all instance parameters from ancestor classes in *.mk.

[Eric Wieser]

I didn't see this message, but as you saw, filed lean4#2905 with a similar example