Полиморфизм и ограничения Rank-2

Question

Я пытаюсь воссоздать трюк полиморфизма s-2 ST s, чтобы гарантировать, что определенные значения не смогут избежать пользовательской монады. Следующий код представляет собой что-то в духе моего решения:

data STLike s a = STLike a 
class Box box where 
    runBox :: box a -> a 

run :: Box box => (forall s. box (STLike s a)) -> a 
run box = let STLike a = runBox box in a 

Хотя приведенный выше код компилируется нормально, то начинаются проблемы, когда я пытаюсь ввести Ограничить на box (STLike s a):

data STLike s a = STLike a 
class Box box where 
    runBox :: box a -> a 

run :: Box box => (forall s. Eq (box (STLike s a)) => box (STLike s a)) -> a 
run box = let STLike a = runBox box in a 

Второй фрагмент не компилируется со следующим сообщением:

Could not deduce (Eq (box (STLike t0 a))) 
    arising from a use of `box' 
    from the context (Box box) 
    bound by the type signature for 
       run :: Box box => 
         (forall s. Eq (box (STLike s a)) => box (STLike s a)) -> a 
    at src/TPM/GraphDB/Event.hs:36:8-76 
    The type variable `t0' is ambiguous 

Можно ли обойти это? Если нет, то почему?

Answer 1

Вам необходимо предоставить способ для ghc, чтобы составить этот экземпляр. Один из способов сделать это:

{-# LANGUAGE FlexibleContexts, RankNTypes #-} 
data STLike s a = STLike a deriving (Eq) 
class Box box where 
    runBox :: box a -> a 

newtype Boxed box a = Boxed (box a) 

instance (Box box, Eq a) => Eq (Boxed box a) where 
    Boxed a == Boxed b = runBox a == runBox b 

run :: (Eq a, Box box) => (forall s. Eq (Boxed box (STLike s a)) 
              => box (STLike s a)) 
         -> a 
run box = case runBox box of STLike a -> a 

Я не думаю, что вы можете иметь instance Eq (box (STLike s a)), так что немного неудобно Newtype выше.