> [code below]

    let dyn_array = fn (erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }

Yes, but array(len, t) has a dynamic layout. Your system needs to understand that that is OK because `pointer(array(len, t))` still has a static layout. You need to understand that pointee-monomorphization is not necessary. You can do special hacks for the `pointer` type constructor, but then you cannot eta-expand it (i.e. wrap in a one field struct). To make this work in a first-class way, so custom data types can have type parameters that do not need to be monomorphized, you need your type system to be layout-aware.

Also, you can do

    let dyn_array = fn (dynamic erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }

There is no need to force the element type to be static. The array itself doesn't care. The pointee is already dynamic-layout either way.

> [code below]

    let vtable = fn (erased t : type) -> record { print : pointer(t) -> string, ... }

    let dyn_print = record { t : type @@ dynamic erased, vtable : pointer(vtable(t)), data : pointer(t) }

The problem with this is that `vtable` is being called with a dynamic-erased argument, but it itself requires a static type. That means the whole thing is dynamic (well, depending on exactly how the modalities work). But do want to statically know it is a record with a print field, etc.

> static layout would require parameterizing on the layout of t, so I see your point

:) See https://docs.rs/stack_dst/latest/stack_dst/ for example, which tries to hack it in Rust. It would be much nicely to do it safely!