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

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

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 l应该保留此上下文。我做错了吗，还是这是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

最佳答案

您对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的唯一非底部实例具有您的类型类约束，但是对于类型检查器而言，这还不够，因为那样会与bottom不一致。



回答新问题

当您解构这样的类型时

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

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

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

关于haskell - 解构GADT:我在哪里失去背景？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/18641714/