"In general, neither can ensure at compile time that an index only known at runtime is in bounds, even if the bounds themselves are statically known."

I remember being able to use telescopes [1] in Haskell long time ago, around 2012 or so.

[1] https://www.pls-lab.org/en/telescope

Haskell was not and is not properly dependently typed.