I don't know Haskell, but I'm pretty certain that something I recently discovered also applies there: Dependent Types
In short, it's a way to restrict the data types to such a degree that the type checker can do compile-time checks of array sizes and other interesting things, as those aspects are directly expressed as distinct types depending on each other. The principle requires a pretty powerful type system and is cumbersome to use, but I found it fascinating regardless.