As other commenters have said, this doesn't need dependent types. Rust's const generics / C++'s non-type template parameters are enough.

Even in languages with dependent types, people tend to find it overly cumbersome to use them for actually prevent runtime errors like out-of-bounds access; they instead tend to save the dependent types for (1) data structure invariants that can be propagated easily, and (2) verification after the program has been defined.[0][1]

[0]: https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

[1]: https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pd... ("Programming with dependent types: passing fad or useful tool?" by Xavier Leroy in 2009; things might have changed since 2009)