One can imagine a kind of "dependent with" type.
(x : S) & T x
lets you choose at runtime between a "raw" S and a "cooked" T whose type depends on what the S used to be. Both components may be *contemplated* but only one may exist at run time.
Conversation
Replying to
Oooh, reminds me of stuff I'm doing parsing OpenType - there are a bunch of subtables in a sequence, but some subtables need information from other tables in order to be fully parsed (like the number of glyphs), so I break it into dependent phases using an ‘overlay’ format.
But yeah, at the moment the representation type of the overlay formats are dependent pair/record - which is annoying. I'd rather something like you are describing I think?