Summary

Since commit fdce7a9 there is support in Lean 4 for strutures that extend multiple structures that share the same field (diamonds).
However, to my knowledge it is not recorded in the environment which structures are extended this way (note: some structures are not fields and are not returned by Lean.getParentStructures).

Proposal

Add a field parents : Array Name to StructureInfo that lists all the parents of a structure, i.e. all the structures that are listed after extend.
There is a guarantee that if (getStructureInfo? env strName).get!.parents.contains parentName then strName ++ parentName is a valid declaration, and this can be used to obtain all the information about this parent. (Alternatively, we could record more information about this parent in a new structure.)

Example:

structure Foo1 where
  a : Nat
  b : Nat

structure Foo2 where
  a : Nat
  c : Nat

structure Foo3 extends Foo1, Foo2 where
  d : Nat

-- In the proposal we have ``(getStructureInfo? env Foo3).get!.parents == #[`toFoo1, `toFoo2]``

We will rename getParentStructures to getParentFieldStructures and similarly for getAllParentStructures.
Then we provide new versions that give all (transitive) parent structures (the new getAllParentStructures will be deduplicated).

Applications

It is useful to expose this for metaprogramming. In Mathlib4 we have the @[to_additive] attribute that creates a (modified) copy of each tagged declaration, including auxiliary declarations.
Currently the environment doesn't have enough information to find all auxiliary declarations created by a structure command. This could fix leanprover-community/mathlib4#660

We could also use this to allow projection notation for all extended structures, which I think would be useful.
Continuing with the previous example:

def Foo1.bar1 (_ : Foo1) : Nat := 0
def Foo2.bar2 (_ : Foo2) : Nat := 1
example (x : Foo3) := x.bar1 -- works
example (x : Foo3) := x.bar2 -- currently fails, but could be accepted

Implementation

I'm happy to implement this after a thumbs up from a core developer. I'm of course also happy if a core developer decides to implement this.