The actual correspondence in haskell are GADTs: data EqualityProof a b where Refl :: (a ~ b) => EqualityProof a b -- compiler error because we

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