RankNTypes for instance declarations?

Question

Hi,

I've been playing around with RankNTypes recently and wonder if it is possible to use them in instance declarations.

Here is a simple example using open datatypes

data (Expr a, Expr b) => Add a b = Add a b deriving(Show)                          

instance (Expr a, Expr b) => Expr (Add a b)

instance (Evaluation a, Evaluation b) => Evaluation (Add a b) where
  eval (Add x y) = eval x + eval y

Here I have to write constraints like (Evaluation a, Evaluation b), but basically I just want a to write something like (forall a. Evaluation a). Is this even possible?

Regards, raichoo

Answer 1

(forall a . Evaluation a) doesn't really make sense: it would mean that every single type (including any future type someone might make) was an instance of Evaluation.

Also, in this case I think your code listing the instances of Evaluation that you want is the right thing to do; don't demand more than you actually need.

But there certainly are cases where it would be nice to be able to quantify over class constraints along the lines you describe, and it's not possible directly. One example is that you might want to automatically make MonadPlus instances from Monoid (using a wrapper type to avoid OverlappingInstances problems):

newtype MonoidWrapper m a = MonoidWrapper { unMonoidWrapper :: m a }

instance Monad m => Monad (MonoidWrapper m) where ...

instance (Monad m, forall a . Monoid (m a)) => MonadPlus (MonoidWrapper m) where
    mzero = MonoidWrapper mempty
    mplus (MonoidWrapper a) (MonoidWrapper b) = MonoidWrapper (mappend a b)

You can't write this, but using GADTs or existential types you can simulate it, with some syntactic pain:

data MonoidDict a where
    MonoidDict :: Monoid a => MonoidDict a

class AlwaysMonoid m where
    alwaysMonoidDict :: MonoidDict (m a) -- note the implicit forall a here

instance Monad m => Monad (MonoidWrapper m)

instance (Monad m, AlwaysMonoid m) => MonadPlus (MonoidWrapper m) where
    mzero = mymzero
     where
       -- needed to give name to 'a' for ScopedTypeVariables
      mymzero :: forall a . MonoidWrapper m a
      mymzero = case (alwaysMonoidDict :: MonoidDict (m a)) of
                  MonoidDict -> MonoidWrapper mempty
    mplus = mymplus
     where
      mymplus :: forall a . MonoidWrapper m a
              -> MonoidWrapper m a -> MonoidWrapper m a
      mymplus (MonoidWrapper a) (MonoidWrapper b)
         = case (alwaysMonoidDict :: MonoidDict (m a)) of
            MonoidDict -> MonoidWrapper (mappend a b)