Haskell is unsound because of 'undefined :: a'. There you go - a proof of every proposition by the Curry-Howard isomorphism. It's still safe, though, as it div

Haskell is unsound because of 'undefined :: a'. There you go - a proof of every proposition by the Curry-Howard isomorphism. It's still safe, though, as it diverges at run time. Much like the ClassCastException coming from the JVM prevents the unsoundness in the original article from being a safety error. 'unsafeCoerce' (and things that can implement it, like creating a polymorphic mutable cell with 'unsafePerformIO') are worse than unsound - they are also unsafe.