GHC type role inference and checking has the big stupid.

Roles.hs

{-# LANGUAGE RoleAnnotations, DerivingVia #-}

module Roles where

import Control.Monad.Reader (MonadReader, ReaderT(..))


-- | In the case of:
--
-- > newtype ReaderT r m a = ReaderT (r -> m a)
--
--   GHC should derive the role of @a@ from the role signature of @m@, but
--   because it doesn't know anything about @m@, it infers (and asserts) the
--   worst case for @a@. Hence it produces:
--
-- > type role ReaderT representational representational nominal


-- | Here GHC knows:
--
-- > type role IO representational
--
--   Yet the following produces an error:
--
-- > type role App representational
--
--   GHC instead continues to infer and assert the worst case, taking the
--   sloppy role signature of 'ReaderT' as gospel, completely forgetting why
--   @a@ was roled as nominal in the first place.
type role App nominal
newtype App a = App (ReaderT () IO a)
  deriving (Functor, Applicative, Monad, MonadReader ())


-- | To make GHC accept the correct role, you must dispense with the structure
--   you've imbued on the representation and lay it bare; if the type isn't
--   built out of newtypes, you might just be SOL.
--
--   DerivingVia, at least, offers up a consolation prize in the form of a
--   post-credits cameo.
type role App2 representational
newtype App2 a = App2 (() -> IO a)
  deriving (Functor, Applicative, Monad, MonadReader ()) via ReaderT () IO