C also has arrays with dimensions as part of the type. The trick is that the dimension must be determined statically. This is different than vectors in Haskell which allow the size of the vector to be determined (and even vary) dynamically, yet still guarantee memory safety statically (I.e. no runtime cost for bounds checking).
You can think of an array with a static size of 10 as being like shorthand notation for a struct with ten fields (sans padding). It really is no more complicated than that.
I believe that works fine (at least in C). You have to statically put the array size into the function signature, so it will only work on arrays of that size. I was simply pointing out the difference between dependently typed vectors which have the type checker prove you use the vector correctly, and arrays in c and pascal whose sizes are known at compile time. I am agreeing with the author that this makes it hard to create generic array bounds if you don't have the ability to make unbounded arrays (as c does). I was disagreeing with the gp, who was conflating these two different sorts of types.
It's been a few years since I've written a lot of C. ufo's sibling comment reminded me of how it acts (the last dimension is ignored).
Anyway, this is completely beside the point of what I was talking about. The point is that a static size is a very different level of type system machinery from a dynamic size.
IIRC, if you have multidimensional arrays only the last dimension is ignored so arr[3][4] is equivalent to arr[3][]. Of course, in the one dimensional case it means that the dimension is ignored.
You can think of an array with a static size of 10 as being like shorthand notation for a struct with ten fields (sans padding). It really is no more complicated than that.