haskell - 在存在数据族的情况下键入(中)等式

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 的异构列表中投影出来。)

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

原来这是一个 known GHC bug .该修复程序已经在 GHC 头中，并且应该在下一个即将发布的版本中(GHC 8.0.1 和可能的 7.10.3)。

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