Extending a structure in a field-dependent manner

Stream: lean4

[Thomas Murrills]

I'd like to be able to write things along the lines of

axiom F : Bool → Type -- some type family, demonstration purposes only

structure Foo (b : Bool) where -- some structure parametrized by data
  a : F b

structure Bar where
  b : Bool
  extends Foo b

This doesn't work, and we (seem to) have to resort to

structure Bar where
  b : Bool
  toFoo : Foo b

However, I'm specifically after the ability to write structure instances nicely (in a flat manner) that you get with extends, as opposed to simply having something that typechecks/functions well. Is there a nice way to achieve this?