假设单位类型是否相等是否安全？

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.