小编aav*_*ogt的帖子

此数据类型可以具有type role HCons' representational representational,允许使用coerce添加或删除应用于元素的新类型,而无需遍历列表.

data HNil' = HNil'
data HCons' a b = HCons' a b

但是,这些列表的语法不如具有以下GADT的语法好

data HList (l::[*]) where
    HNil  :: HList '[]
    HCons :: e -> HList l -> HList (e ': l)

我有一个类在这两个表示之间进行转换,这样Prime (HList [a,b]) ~ HCons' a (HCons' b HNil').该课程是否成功？

coerceHList :: Coercible (Prime a) (Prime b) => HList a -> HList b
coerceHList = unsafeCoerce

安全？