reusing instance when classes and structures use `extends`

Stream: lean4

[Markus Schmaus]

Given a class ClassB which extends another class ClassA and a structure StructB which extends StructA, is it possible to reuse the instance of StructA for ClassA when constructing the instance of StructB for ClassB?

This mwe should make clear what I mean:

class ClassA (α β: Type) where
  a (x : β) : α
  b (x : β) : α

class ClassB (α β : Type) extends ClassA α β where
  c (x : β) : α
  d (x : β) : α

structure StructA (α : Type) where
  a : α
  b : α

instance instA : ClassA α (StructA α) where
  a := StructA.a
  b := StructA.b

structure StructB (α : Type) extends StructA α where
  c : α
  d : α

instance instB : ClassB α (StructB α) where
  toClassA := instA -- error: wrong type
  c := StructB.c
  d := StructB.d

[Eric Wieser]

This works:

class ClassA (α β: Type) where
  a (x : β) : α
  b (x : β) : α

class ClassB (α β : Type) extends ClassA α β where
  c (x : β) : α
  d (x : β) : α

structure StructA (α : Type) where
  a : α
  b : α

instance instA : ClassA α (StructA α) where
  a := StructA.a
  b := StructA.b

abbrev ClassA.comp [ClassA α β]  (f : γ → β) : ClassA α γ where
  a c := ClassA.a (f c)
  b c := ClassA.b (f c)

structure StructB (α : Type) extends StructA α where
  c : α
  d : α

instance instB : ClassB α (StructB α) where
  toClassA := ClassA.comp StructB.toStructA
  c := StructB.c
  d := StructB.d