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 )
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
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.