I don't follow. If your list is not the right size, your program doesn't compile, period.
If it does, you're not using a dependently typed language.
Am I missing something?
The key insight here is that the check may be performed at compile time or runtime as long as the compiler can see that you've performed the check. It can do this e.g. in pattern match clauses. For example in code like
case inputList of
[a,b,c,d,e] -> branch-A
otherwise -> branch-B
(And if you think about it... if you didn't allow for runtime checks to satisfy such proof obligations there would essentially no way for any dependently programs to depend on any runtime values at all.)
Aside: Another thing which I think has been missed in this entire discussion is that you don't have to actually use List-of-size-N as your type. If you don't actually care about the size of the list in the code you're writing, you're also allowed to just use List-of-any-finite-size as your data type. (Of course this could cause a certain amount of friction if the standard library is all based on List-of-size-N, but it shouldn't be too bad in e.g. Idris.)
Then, at runtime, you can cast an unsized list to a sized list giving - say - a function List[A] => Option[Sized[List[A], N5]] that will fail if the list is not of size 5. From then on you can go on letting the compiler keep track of lengths.
Of course, this does not work at all if you have no clue what size your input will have