The goal is to get static time checking of dynamic types. For example, if I take two dynamic length arrays and loop n times, appending (optionally?) an element

The goal is to get static time checking of dynamic types. For example, if I take two dynamic length arrays and loop n times, appending (optionally?) an element to each array, can you still provide a compile-time check that both arrays are necessarily the same length. It’s much more powerful than what you describe.