The point is not that you can do explicit casts, it's that because you can form a (fake) instance for impossible types you can do invalid type conversions without doing anything that looks unsafe.

In Haskell you can certainly achieve the same thing with various common extensions ( http://okmij.org/ftp/Haskell/impredicativity-bites.html ). Possibly not in vanilla Haskell '98, at the price of being not a very nice language to work in. (A total language like Idris should permit GADT-like functionality without allowing this kind of issue).

The actual correspondence in haskell are GADTs:

    data EqualityProof a b where
        Refl :: (a ~ b) => EqualityProof a b

    -- compiler error because we don't check that the equality proof is actually Refl
    coerce :: EqualityProof a b -> a -> b
    coerce _ a = a

    -- this works
    coerce Refl a = a

    -- here the Refl pattern match catches the undefined
    -- this is like forcing the programmer to do a null check before the equality is in scope
    -- and throwing a runtime exception when it's null
    coerce undefinded 3 :: String

By “convert” here I mean convince the compiler that any thing of type A is any type B, when it definitely isn't, without using an explicit cast.

Data.Dynamic is type safe. It performs a run-time type check.

Haskell can be made to be unsound using 'unsafeCoerce', but as you'll note, there is a giant unsafe in front of it.

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.

Read about Bottom (⊥).

null can be considered bottom (if it were not for primitives)