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.