haskell - 解构 GADT : Where am I losing the context?

Question

我有这种类型和这些功能:

data Tag a where
    Tag :: (Show a, Eq a, Ord a, Storable a, Binary a) => a -> BL.ByteString -> Tag a

getVal :: Tag a -> a
getVal (Tag v _) = v

isBigger :: Tag a -> Tag a -> Bool
a `isBigger` b = (getVal a) > (getVal b)

代码不进行类型检查:

No instance for (Ord a)
  arising from a use of `>'
In the expression: (getVal a) > (getVal b)
In an equation for `isBigger':
    a isBigger b = (getVal a) > (getVal b)

 

但我不明白为什么不。 Tag a 具有上下文 (Show a, Eq a, Ord a, Storable a, Binary a)，并且 getVal 应该保留此内容语境。我是否做错了，或者这是 GADT 扩展的限制？

这有效:

isBigger :: Tag a -> Tag a -> Bool
(Tag a _) `isBigger` (Tag b _) = a > b

编辑:我将示例更改为最小示例

编辑:好的，为什么这个没有进行类型检查？

isBigger :: Tag a -> Tag a -> Bool
isBigger ta tb =
    let (Tag a _) = ta
        (Tag b _) = tb
    in
        a > b

Answer 1

您的 getVal 类型签名不正确，您需要该类型

 getVal (Storable a, Ord a, ...) => Tag a -> a
 getVal (Tag v _) = v

之所以没有推断出这一点是因为你可以做类似的事情

 doh :: Tag a
 doh = undefined

现在 a 对它没有任何限制。我们可以做类似的事情

 getVal (doh :: Tag (IO Int)) == getVal (doh :: Tag (IO Int))

如果getVal有这些约束。

Tag 的唯一非底部实例对它们具有类型类约束，但这对于类型检查器来说还不够，因为那样它会与底部不一致。

<小时/>

回答新问题

当你像这样解构类型时

 foo tag = let (Tag a _) = tag
               (Tag b _) = tag
           in a > b

GHC 没有正确统一它们。我怀疑这是因为类型检查器在达到模式匹配时已经决定了 a 的类型，但是通过顶级匹配，它将正确统一。

 foo (Tag a _) (Tag b _) = a > b