Skip to content

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.

Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information