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

A 昨天的问题 https://stackoverflow.com/q/41135212/3072788有一个定义HList（来自HList https://hackage.haskell.org/package/HList-0.4.1.0/docs/Data-HList-HList.html包）使用数据族。基本上：

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（从而阻止任何强制）。 (我对上述问题的回答有一个具体的例子 https://stackoverflow.com/a/41135693/3072788.)

GADT 角色系统在以下方面的缺陷HList在此讨论。基本上，GHC 会自动将任何“类似 GADT”类型的变量标记为名义变量。

鉴于自那时以来已经过去了一段时间并且有人讨论让角色围绕类型/数据族变得更加灵活 https://ghc.haskell.org/trac/ghc/ticket/8177，是否有任何前进的道路（即一些现有的想法，一些开放的 Trac 票证，任何真正的东西）来检查 GADT 中更有趣的角色（例如HList）？ GADT 或两者之间的相互作用是否存在一些基本限制？DataKinds和角色？需要实施/创建什么才能使其发挥作用？

角色系统的作者在这里。我不知道有什么想法可以推动我们朝这个方向前进。问题是我们需要检查一个微妙的属性以确保强制转换是安全的。具体来说，我们希望能够强制例如HList [Age, Int, String] to HList [Int, Age, String]但不HList [String, String, Int] (or an HList与三个元素以外的其他元素）。 （我假设newtype Age = MkAge Int）要实现这一点，需要一些非常光荣的类似角色的系统——能够准确描述对于这样的 GADT 来说什么强制是安全的——而且我不知道有任何创建这样一个系统的工作。

数据族方法起作用的原因是 GHC 可以看到HList [Age, Int, String]确实是一样的(Age, (Int, (String, HList '[])))，然后它就足够了解元组来完成其余的工作。

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