If you would have substituted coq (or even ACL2 with guards checking enabled...) in the place of haskell I would agree. hindley-milner style type checking is n

If you would have substituted coq (or even ACL2 with guards checking enabled...) in the place of haskell I would agree. hindley-milner style type checking is nice, but once you admit that things like arrays exist (rather than just algebraic data types or cons cells), the power of languages like haskell is in design patterns like map() and reduce() rather than the type checker, IMO. Having worked in functional languages with an imperative bent (esp. ACL2 in the context of modeling microprocessors), you can get an awful lot of mileage out of a good static proof strategy that can be instantiated over a known design pattern (equivalence relations, map, reduce, etc) even when you pass a single, huge, state object to all your top level functions.