| 24 | |
| 25 | readRef :: MonadIO m => IORef a -> T m a |
| 26 | readRef = T . liftIO . readIORef |
| 27 | }}} |
| 28 | |
| 29 | The designer of `T` will export it abstractly, allowing only the reading of `IORef`s in the `T` monad but not other operations. |
| 30 | |
| 31 | Sadly, the use of GND fails here, with `join` in the `Monad` class. Here is the relevant generated code: |
| 32 | |
| 33 | {{{ |
| 34 | instance Monad m => Monad (T m) where |
| 35 | ... |
| 36 | join = coerce (join :: m (m a) -> m a) :: forall a. T m (T m a) -> T m a |
| 37 | }}} |
| 38 | |
| 39 | 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))`. |
| 40 | |
| 41 | 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. |
| 42 | |
| 43 | === The `MVector` class === |
| 44 | |
| 45 | A redesign of the `vector` package is underway, introducing the `Vector` class, among other changes. Here is the offending method: |
| 46 | |
| 47 | {{{ |
| 48 | class (...) => Vector v a where |
| 49 | basicUnsafeIndexM :: Monad m => v a -> Int -> m a |
| 50 | ... |
| 51 | }}} |
| 52 | |
| 53 | Here, `a` is the type of the thing stored in the vector, and it is natural to want to coerce a vector of `Int`s to a vector of `Age`s. 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`. |
| 54 | |
| 55 | === The `acme-schoenfinkel` package === |
| 56 | |
| 57 | 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 |
| 58 | |
| 59 | {{{ |
| 60 | WrappedSchoenfinkel { |
| 61 | unwrapSchoenfinkel :: cat a b |
| 62 | } |
| 63 | deriving (Alternative, Applicative, Arrow, ArrowApply, |
| 64 | ArrowChoice, ArrowLoop, ArrowPlus, ArrowZero, |
| 65 | Category, Functor) |
| 66 | }}} |
| 67 | |
| 68 | GND fails on `ArrowApply`: |
| 69 | |
| 70 | {{{ |
| 71 | class Arrow a => ArrowApply (a :: * -> * -> *) where |
| 72 | app :: forall b c. a (a b c, b) c |
| 73 | }}} |
| 74 | |
| 75 | The problem here echoes the `join` problem quite closely. |
| 76 | |
| 77 | == The best known solution == |
| 78 | |
| 79 | Edward Kmett initially described an approach in an [http://www.haskell.org/pipermail/ghc-devs/2014-May/004974.html email], roughly as follows (names subject to bikeshedding, as always): |
| 80 | |
| 81 | Currently, `Data.Type.Coercion` makes this definition: |
| 82 | |
| 83 | {{{ |
| 84 | data Coercion a b where |
| 85 | Coercion :: Coercible a b => Coercion a b |
| 86 | }}} |
| 87 | |
| 88 | Building on that, define a class `Rep` like this: |
| 89 | {{{ |
| 90 | class Rep (f :: k1 -> k2) where |
| 91 | co :: Coercible a b => Coercion (f a) (f b) |
| 92 | }}} |