It's also hard to massage your invariants into a form that a type checker will accept, since you're now restricted to weird, (usually) non-Turing-complete language.

A good example of this is matrix operations - there are plenty of invariants and contracts to check (e.g. multiplication must be between m x n and n x p matrices), but I don't believe there's yet a particularly convincing Haskell matrix library, in part because the range of relevant mathematical invariants don't cleanly fit into Haskell's type system.

For those cases, checking the invariants at runtime is your escape hatch to utilize the full expressive power of the language.