I think those can be modeled without explicitly separating layouts from types (not that doing so is necessarily a bad idea).

For arrays:

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

For "dyn trait":

  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) }

Both use dependent records and the dynamic modality I mentioned above. dyn_print doesn't match C++ since it doesn't inline the data, and giving that a static layout would require parameterizing on the layout of t, so I see your point. However, it might be fine to give dyn_print an "incomplete" layout that can only appear behind a pointer.