3

I have this type and these functions:

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)

The code doesn't typecheck:

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)

 

But I can't understand why not. Tag a has the context (Show a, Eq a, Ord a, Storable a, Binary a), and getVal ought to preserve this context. Am I doing it wrong, or is this a limitation of the GADTs extension?

This works:

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

Edit: I changed the example to a minimal example

Edit: Ok, why doesn't this typecheck?

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

1 回答 1

6

您的类型签名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
于 2013-09-05T16:50:03.500 回答