解构GADT:我在哪里失去了背景？

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),getVa我应该保留这种背景.我做错了,还是这是GADTs扩展的限制？

这有效:

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