GADT类型变量的角色的未来？

Question

昨天的一个问题有一个定义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)案例,因为它是a newtype instance,但这就足够了),而GADT只推断一个名义角色l(从而阻止任何强制).(我对上述问题的回答有一个具体的例子.)

HList在这个为期两年的问题中,讨论了GADT角色系统的失败问题.基本上,GHC会自动将任何"类GADT"类型变量标记为名义变量.

鉴于从那时起已经过了一段时间,并且有关于在类型/数据系列中使角色更加灵活的讨论,是否有任何前进的路径(即一些现有的想法,一些开放的Trac票,真的任何东西)用于检查GADT中更有趣的角色(喜欢HList)？GADT或DataKinds角色的相互作用是否存在一些基本限制？需要实现/创建什么才能实现？

Answer 1

角色系统的作者在这里。我不知道有什么想法可以推动我们朝这个方向前进。问题是我们需要检查一个微妙的属性以确保强制转换是安全的。具体来说，我们希望能够强制例如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 '[])))，然后它足够了解元组来完成其余的工作。

很抱歉在这里没有得到鼓励，但这似乎远远超出了我们现在所能做的。