I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file.<p>You cannot apply directly any of the size-aware functions, because it will not typecheck. I only see two avenues:<p>Either you assert statically that the vector has some concrete size, in which case the size is known statically and the code generation will work as well;<p>Or you use some other size-unaware function, in which case it is false that Idris can use runtime values as type parameters.<p>If I understand correctly, you are saying that there is a third possibility, but I am missing it