haskell - 假设单位类型相同是否安全？

Question

假设所有类型的 () 都相同是否安全？也就是说，以下可以用来破坏类型安全吗？

-- Bad postulate
unitsEqual :: (x :: ()) :~: (y :: ())
unitsEqual = unsafeCoerce (Refl :: '() :~: '())

Answer 1

这在 GHC 7.8.3 下是不安全的(参见下面的代码)。正如用户2407038所说，以下内容被GHC 7.10.3拒绝。毫不奇怪，这个数据族非常邪恶，以至于类型检查器被更改以禁止它。我仍在尝试查看是否有办法在 7.10.3 下实现此目的。

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

module UnitsEqual where
import Unsafe.Coerce
import Data.Type.Equality

data family Yeah (a :: ()) b c
data instance Yeah '() b c = Yeah { yeah :: b }
data instance Yeah a b c = Nope c

-- Entirely valid
castYeah :: x :~: y -> Yeah x p q -> Yeah y p q
castYeah Refl x = x

-- Bad postulate
unitsEqual :: (x :: ()) :~: (y :: ())
unitsEqual = unsafeCoerce (Refl :: '() :~: '())

-- Oh no! This doesn't actually cast, but
-- it's horrible enough. It consistently produces
-- either segmentation faults or nonsense,
-- whether the types are the same or not.
uc :: a -> b
uc a = yeah $ castYeah unitsEqual (Nope a)

但是，我 相信，可以安全地假设

voidsEqual :: (a :: Void) :~: (b :: Void)

因为没有明显的方法来区分 Void中的任何卡住/伪造类型。