Deconstructing a GADT: Where am I losing the context?

Question

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

Answer 1

Your type signature for getVal isn't correct, you'd like the type

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

The reason this isn't inferred is because you can do things like

 doh :: Tag a
 doh = undefined

Now that a doesn't have any constraints on it. We can do something like

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

if getVal had those constraints.

The only nonbottom instances of Tag have your typeclass constraints on them, but this isn't enough for the typechecker since then it'd be inconsistent with bottom.

---

To answer the new question

When you deconstruct types like this

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

GHC doesn't unify them properly. I suspect this is because the typechecker has already decided on the type of a by the time the pattern match is reached, but with a top level match it will unify properly.

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