That’s not true. Even if you don’t know the size (n) of something at compile. You can always make sure in one of branches of your program that some other number

That’s not true. Even if you don’t know the size (n) of something at compile. You can always make sure in one of branches of your program that some other number m is equal to n even if they’re unknown. This the compiler can tell. For instance to produce an element x of type Fin n from an integer (n known at runtime), the compiler can make sure that you produced a proof that x < n. Usually the cast operation looks like this: Integer -> Maybe (Fin n). There is then only two possible branches in your program at this point and the compiler enforces it. (Just (Fin n) case and Nothing case).