I think part of the reason the type system in Haskell works and doesn't seem to get in your way is because of type inference.

Also, Haskell is more strongly (and richly) typed than Java\C++\C# so having strongly-typed code works really well.

About proving correctness, I guess you may have seen this amusing piece: http://perl.plover.com/yak/typing/samples/slide030.html

The type system found an infinite-loop bug in the code at compile-time.