RFC: `@[flat]` annotation for names in the `extend` clause of a structure

Proposal

What?

When working with a structure hierarchy like

structure A where a : Unit
structure B extends A where b : Unit
structure C extends A where c : Unit
structure D extends B, C where

the type of D.mk is asymmetric:

D.mk (toB : B) (c : Unit) : D

More precisely, the representation of D is to embed an entire B structure, but then only take the parts of the C structure that do not overlap with B, namely c : Unit.

I have no doubt that this behavior is useful in some circumstances, but in situations where a symmetric API is more important than performance, this behavior is annoying.

Let's imagine that the symmetric API we want is D.mk (toA : A) (b c : Unit). Right now, there are the following workarounds to achieve that

1. Write the type of D manually without extends:

   structure A where a : Unit
   structure B extends A where b : Unit
   structure C extends A where c : Unit
   structure D extends A where
     b : Unit
     c : Unit
   
   -- user has to write this boilerplate
   def D.toB (d : D) : B := { toA := d.toA, b := d.b }
   def D.toC (d : D) : C := { toA := d.toA, c := d.c }
   

   This boilerplate can be rather a burden, epsecially since the naive := { d with } approach performs unwanted eta-expansion
2. Use the hack from https://arxiv.org/abs/2306.00617 §4.2, which exploits the 'avoid overlaps' rule to our advantage, as

   structure DFlatHack where
   
   structure A where a : Unit
   structure B extends DFlaHack , A where b : Unit
   structure C extends DFlatHack, A where c : Unit
   structure D extends DFlatHack, B, C where
   

   which gives us D.mk (toDFlatHack : DFlatHack) (toA : A) (b c : Unit) : D, where the first argument is vacuous and can always be passed as ⟨⟩.

In Lean 3 we had set_option old_structure_cmd true; but this was a bad design because it did not allow parent structures to selectively be flattened (among other reasons).

The proposal is to remove the need for a hack here, such that the user can write

structure A where a : Unit
structure B extends A where b : Unit
structure C extends A where c : Unit
structure D extends @[flat] B, @[flat] C where

or any other reasonable syntax.

How?

The presence of flat simply means "skip the overlapping fields check, and behave as if the fields overlap"; that is, a check for the syntactic marker would be added to the conditions here:

https://github.com/leanprover/lean4/blob/57e23917b605d1f1e6b6ff70aa022065d55bb60c/src/Lean/Elab/Structure.lean#L423-L428

https://github.com/leanprover/lean4/blob/57e23917b605d1f1e6b6ff70aa022065d55bb60c/src/Lean/Elab/Structure.lean#L479-L483

Why?

• Nested structures are involved in frequent peformance issues in mathlib (for example, #2451)
• Nested structures break symmetries in unfortunate ways for things like RingHom, which has to pick between MonoidHom and AddMonoidHom as it's "main" parent. This affects the shape of the constructor, the simp lemmas about it, and adds ugly additional angle brackets to anonymous constructors

In both cases, having a @[flat] attribute would make it vastly easier to perform performance and API experiments in mathlib to work out where nested structures help, and where they're a hindrance.

Community Feedback

Mario originally proposed this syntax here.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the referenced sections of src/Lean/Elab/Structure.lean at lines 423-428 and 479-483, then inspect how structure parent annotations are parsed and elaborated. Done means the proposed flat-parent syntax is supported and produces the symmetric constructor behavior shown for D, without requiring the existing workaround.