在存在数据系列时键入(in)等式

Question

我有一个类型系列,它确定某些东西是否属于类型级列表的头部.

type family AtHead x xs where
    AtHead x (x ': xs) = True
    AtHead y (x ': xs) = False

我想构造这个结果的单例代表.这适用于简单类型的列表.

data Booly b where
    Truey :: Booly True
    Falsey :: Booly False

test1 :: Booly (AtHead Char [Char, Int])
test1 = Truey
test2 :: Booly (AtHead Int [Char, Int])
test2 = Falsey

但我真正想要做的是为索引的成员列表构造此值data family.(实际上,我试图ID根据类型从异构的s 列表中投射元素.)

data family ID a

data User = User
newtype instance ID User = UserId Int

当ID我们正在寻找的是列表的头部时,这是有效的.

test3 :: Booly (AtHead (ID User) [ID User, Char])
test3 = Truey

但它失败了.

test4 :: Booly (AtHead (ID User) [Int, ID User])
test4 = Falsey

    Couldn't match type ‘AtHead (ID User) '[Int, ID User]’
                  with ‘'False’
    Expected type: Booly (AtHead (ID User) '[Int, ID User])
      Actual type: Booly 'False
    In the expression: Falsey
    In an equation for ‘test4’: test4 = Falsey

AtHead (ID User) '[Int, ID User]没有统一'False.看起来GHC不愿意判断ID User并且Int不相等,即使它ID是一个单射的data family(因此原则上只相等于(减少的东西)ID User).

我对约束求解器将会接受和不接受的直觉是相当弱的:我觉得这应该编译.任何人都可以解释为什么我的代码不进行类型检查？有没有办法让GHC接受它,也许是通过证明一个定理？

Answer 1

事实证明这是一个已知的 GHC bug。该修复已经在 GHC head 中，并且应该在下一个即将发布的版本中（GHC 8.0.1，也许 7.10.3）。

除此之外，@luqui 对新类型包装器的建议似乎是最简单的选择。