You will notice that you use the array the wrong way when you try to prove the correctness of the client of the array. Somewhere in the specification of the client it will be required to, let's say, sum up all of the elements of the array. If the array index range is [-1, 4[, but the client sums over [1, 4[, then this is wrong.

The client will have its own spec, and when it uses the array, you need to prove that it does so in a way that its own spec is fulfilled.

You need to know the entire semantics of the interaction. You need to know what the array represents for the client, and that may depend on the client of the client.

But with multiple dispatch you are constantly tempted to pretend that correctness just depends on the type, because that's what you dispatch on. So that's the problem.

In general, I like types for organising things. I don't like them for correctness.

PS: Edited the above a few times to make my point more clearly.