Emit quantified Coercible constraints in GeneralizedNewtypeDeriving
This thread on ghc-devs identifies a real shortcoming of the new roles system. Here's a compact example, from the thread
class C m where
ret :: a -> m a
bind :: m a -> (a -> m b) -> m b
join :: m (m a) -> m a
newtype T m a = MkT (m a) deriving( C )
The deriving(C) is accepted without join in the class, but rejected when join is added.
T9123.hs:10:37:
Could not coerce from `m (m a)' to `m (T m a)'
because `m (m a)'
and `m (T m a)'
are different types.
arising from the coercion of the method `join'
from type `forall a. m (m a) -> m a'
to type `forall a. T m (T m a) -> T m a'
Note that the AMP proposal adds join to class Monad!
In one way it is rightly rejected: it really would be unsound to derive an instance for C (T K) where K's argument had nominal (but not representational) role. But we have no way to limit the type constructors at which T can be used.
This deficiency is noted in the Safe Coercions paper, but this seems to be the first occasion on which it has bitten us badly.
Edward made a suggestion on the thread.