Деконструкция 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) 

Код не 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) 

Но я не могу понять, почему нет. Tag a имеет контекст (Show a, Eq a, Ord a, Storable a, Binary a), и getVa Я должен сохранить этот контекст. Я делаю это неправильно, или это ограничение расширения GADT?

Это работает:

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

Edit: Я изменил пример минимального примера

Edit: Хорошо, почему не это typecheck?

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 имеют ограничения на их типы, но этого недостаточно для typechecker с тех пор, это будет несовместимо с дном.

---

Чтобы ответить на новый вопрос

Когда вы деконструкции типы, как этот

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

GHC не унифицировать их должным образом. Я подозреваю, что это потому, что typechecker уже определился с типом a к моменту достижения соответствия шаблону, но с совпадением верхнего уровня он будет унифицирован должным образом.

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