Dependent types allow for this kind of thing. Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, w

Dependent types allow for this kind of thing. Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.