昨天的一个问题具有使用数据家族的HList（来自HList软件包）的定义。基本上：
data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x xs = HCons1 (x, xs)
而不是通常的（IMO更优雅，更直观）GADT定义
data HList (l :: [*]) where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x ': xs)
这是因为数据家族版本使我们胁迫（我们只能强迫HList (x ': xs)案件，因为它是newtype instance，但这已经足够了），而GADT仅侵犯了l的名义角色（因此阻止了任何胁迫）。（我对上述问题的回答有一个具体的例子。）
在这个两年历史的问题中讨论了GADT在HList方面的角色系统的失败。基本上，GHC自动将任何" GADT样"类型变量标记为名义。
鉴于从那以后已经过去了一段时间，并且有人谈论要使角色在类型/数据系列中更加灵活，是否有任何前进的途径（即某些现有想法，一些开放式TRAC票，实际上是什么），以检查更有趣的角色在gadts中（例如HList）？GADT或DataKinds和角色的相互作用是否存在一些基本限制？为此，需要实现/创建什么才能工作？
作者的作者在这里。我知道没有想法会向我们朝这个方向前进。问题是我们需要检查一个微妙的财产，以确保胁迫是安全的。具体来说，我们希望能够胁迫，例如HList [Age, Int, String]至HList [Int, Age, String]，而不是HList [String, String, Int]（或具有三个元素以外的其他内容的HList）。（我假设在这里newtype Age = MkAge Int。）将其删除将需要一些非常光荣的角色般的系统 - 能够准确地描述哪种胁迫对这样的Gadt的安全 - 而且我不知道有任何创建这样的工作系统。
数据家族方法起作用的原因是GHC可以看到HList [Age, Int, String]确实与(Age, (Int, (String, HList '[])))相同，然后它足够知道元组可以完成其余工作。
很抱歉在这里没有鼓励，但这似乎远远超出了我们现在可以做的。