Version 2 (modified by goldfire, 3 years ago) (diff)


Update to Roles

It has become (somewhat) clear that the Roles mechanism as implemented in GHC 7.8 is insufficient. (See examples below.) This page is dedicated to creating a new design for roles that might fix the problems.

Problem examples

We have three known examples of where current roles are failing us.

Adding join to Monad

As part of the Applicative-Monad Proposal, we wish to add join to Monad, thus:

class Applicative m => Monad m where
  join :: forall a. m (m a) -> m a

This is all well and good, and would work with GeneralizedNewtypeDeriving (GND) most of the time. But, consider this:

newtype T m a = T (m a)
  deriving (Functor, Applicative, Monad)

readRef :: MonadIO m => IORef a -> T m a
readRef = T . liftIO . readIORef

The designer of T will export it abstractly, allowing only the reading of IORefs in the T monad but not other operations.

Sadly, the use of GND fails here, with join in the Monad class. Here is the relevant generated code:

instance Monad m => Monad (T m) where
  join = coerce (join :: m (m a) -> m a) :: forall a. T m (T m a) -> T m a

Thus, GHC must derive Coercible (m (m a) -> m a) (T m (T m a) -> T m a). This requirement reduces (in part) to Coercible (m (m a)) (T m (T m a)). We try to solve this by applying a newtype-unwrapping instance, Coercible x (m a) => Coercible x (T m a). Then, we must solve Coercible (m (m a)) (m (T m a)). And here, we are stuck. We do know Coercible (m a) (T m a), but we don't know the role of m's parameter, and must assume (for safety) that it could be nominal. Thus, we can't solve for Coercible (m (m a)) (m (T m a)).

This problem would occur if join were in Monad and a programmer used GND on any monad transformer. This is a common enough idiom to make us want to fix the situation.

The MVector class

A redesign of the vector package is underway, introducing the Vector class, among other changes. Here is the offending method:

class (...) => Vector v a where
  basicUnsafeIndexM :: Monad m => v a -> Int -> m a

Here, a is the type of the thing stored in the vector, and it is natural to want to coerce a vector of Ints to a vector of Ages. But, GND would not work here, for very similar reasons to the case above -- we won't be able to coerce m Int to m Age, because we don't know enough about m.

The acme-schoenfinkel package

This next example is the one known case of type-safe code that existed before GHC 7.8 that does not work with GHC 7.8's roles. The package acme-schoenfinkel-0.1.1 package (by Ertugrul Söylemez) defines

    WrappedSchoenfinkel {
      unwrapSchoenfinkel :: cat a b
    deriving (Alternative, Applicative, Arrow, ArrowApply,
              ArrowChoice, ArrowLoop, ArrowPlus, ArrowZero,
              Category, Functor)

GND fails on ArrowApply:

class Arrow a => ArrowApply (a :: * -> * -> *) where
  app :: forall b c. a (a b c, b) c

The problem here echoes the join problem quite closely.

The best known solution

Edward Kmett initially described an approach in an email, roughly as follows (names subject to bikeshedding, as always):

Currently, Data.Type.Coercion makes this definition:

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

Building on that, define a class Rep like this:

class Rep (f :: k1 -> k2) where
  co :: Coercible a b => Coercion (f a) (f b)