Yes, but my question is: even if you use erasure, what are you going to do at the call site? Won&#x27;t you need to state a concrete size there? For usual generic types, erasure and code generation are equivalent in what they can do, because at some point you will specialize to concrete types.<p>I would be curious to see an Idris program that reads two vectors out of some file (without knowing the size a priori) and concatenates them