Rank-2 polymorphism and constrains

Question

I'm trying to recreate the STs rank-2 polymorphism trick to ensure that certain values cannot escape a custom monad. The following code represents something in the spirit of my solution:

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

While the above code compiles just fine, the problems begin when I try to introduce a constrain on 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

The second snippet fails to compile with the following message:

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

Is it possible to get around that? If not then why?

Answer 1

You need to provide a way for ghc to make up that instance. One way to do this is:

{-# 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

I don't think you can have an instance Eq (box (STLike s a)), so there's a slightly inconvenient newtype above.