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