Earlier quoted context omitted.
> doesn't matter which language you use Idris.
Care to elaborate? I don't see how this can be done without trading space/time over solution without bound checking.
Basically, in Idris I can have a function concat which takes a Vector, a Vector, and produces a Vector. You can have arbitrary expressions there, and even things like a function which returns a different type based on its boolean argument.
So most signatures will just carry dependencies through, but some things are dependent on runtime input and that's when the "N" part of the type will be tracked at runtime. At least, that's how I think it works.
Dependent types help eliminate large swaths of bounds checks. Not all of them, and I'm not sure how much better it does than a good optimizing compiler.