I believe the Idris runtime uses <i>erasure</i> rather than code generation[1]. The key here is that Idris will make <i>call sites</i> prove statically that the conditions hold, either through having static conditions of their own <i>or</i> proving that the programmer has <i>checked</i> (at runtime) that the conditions hold.<p>(This case of append-n-to-m-vector is a bit weird since it basically just amounts to <i>calculating</i> the length of the output, but my previous statement applies a bit more generally.)<p>[1] So one plausible representation for Vec n a would be a size + array of pointers to a&#x27;s. I believe they&#x27;re actually using linked list for Vec at the moment, though.