Cannot 'coerce' data type with 'Reader' as a field

Question

I have the following Haskell code, that compiles perfectly:

import Control.Monad.Reader (Reader (..))
import Data.Coerce (Coercible, coerce)

data Flow i o = Flow (i -> o) (o -> i)

coerceFlow
    :: (Coercible i i', Coercible o o')
    => Flow i o
    -> Flow i' o'
coerceFlow = coerce

However, if I change the definition of the Flow type to the following:

data Flow i o = Flow (i -> Reader Int o) (o -> i)

I start seeing a weird error:

Coerce.hs:10:14: error:
    • Couldn't match type ‘o’ with ‘o'’ arising from a use of ‘coerce’
      ‘o’ is a rigid type variable bound by
        the type signature for:
          coerceFlow :: forall i i' o o'.
                        (Coercible i i', Coercible o o') =>
                        Flow i o -> Flow i' o'
        at Coerce.hs:(6,1)-(9,17)
      ‘o'’ is a rigid type variable bound by
        the type signature for:
          coerceFlow :: forall i i' o o'.
                        (Coercible i i', Coercible o o') =>
                        Flow i o -> Flow i' o'
        at Coerce.hs:(6,1)-(9,17)
    • In the expression: coerce
      In an equation for ‘coerceFlow’: coerceFlow = coerce
    • Relevant bindings include
        coerceFlow :: Flow i o -> Flow i' o' (bound at Coerce.hs:10:1)
   |
10 | coerceFlow = coerce
   |              ^^^^^^

As I understand, my data type is no longer Coercible automatically. Is there a way to tell GHC that I can coerce values of type Flow automatically? I can coerce each field manually, but I would like to coerce the whole data type at once (this is required for DerivingVia to work).

I tried using the RoleAnnotations extension like this:

type role Flow representational representational

But I see an error:

Coerce.hs:6:1: error:
    • Role mismatch on variable o:
        Annotation says representational but role nominal is required
    • while checking a role annotation for ‘Flow’
  |
6 | type role Flow representational representational
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

score 5 · Accepted Answer · edited May 16 '20 at 21:05

Let's investigate:

> :info Reader
type Reader r = ReaderT r Data.Functor.Identity.Identity :: * -> *
        -- Defined in `Control.Monad.Trans.Reader'

So, Reader is defined in terms of ReaderT.

> :info ReaderT
type role ReaderT representational representational nominal
newtype ReaderT r (m :: k -> *) (a :: k)
  = ReaderT {runReaderT :: r -> m a}
        -- Defined in `Control.Monad.Trans.Reader'

... and ReaderT is nominal on its third argument, causing Reader to be nominal in its second argument, and making your coercion fail. You can't subvert this using a role annotation for your Flow type, since that would cope with the previous role annotation of ReaderT.

Now, you might wonder why ReaderT has a nominal third argument. To understand that, consider its definition:

newtype ReaderT r m a = ReaderT (r -> m a)

What should be the role of a, above? Well, it depends. If m :: * -> * is representational on its argument, then ReaderT is such on a. The same holds for nominal and phantom. The "best" way to express the role here would be to use a role polymorphism like

type role forall r .
     ReaderT representational (representational :: (* with role r) -> *) r

where the role of the third argument depends on the second higher-kinded argument.

Alas, GHC does not support role polymorphism like the above one, so we get to use only the most restrictive role: nominal.

Ooh, this is actually rather interesting. Note that if you import `ReaderT` (the `newtype` constructor is the important part), you *do* get `coerce :: (Coercible i i', Coercible o o') => Reader i o -> Reader i' o'`. However, even with that imported, the OP's code doesn't work. it appears the coercion solver's ability to ignore roles on `newtype`s doesn't extend to `data`. I'm unsure if that's intended or an oversight or what. — HTNW, May 16 '20 at 23:45
@HTNW That's.. weird. I did not expect that `coerce` to type. It looks like GHC is unfolding the first `data` definition, but not the second one in the OP case. — chi, May 17 '20 at 07:38
I think [this proposal](https://github.com/ghc-proposals/ghc-proposals/pull/276) would actually make the OP's code work by allowing GHC to peer into `data` as well as `newtype` (again, as long as all the relevant constructors are visible). Not sure though. — HTNW, May 18 '20 at 04:40

score 4 · Answer 2 · answered May 16 '20 at 23:32

The issue, explained by @chi, is no longer an issue if you avoid using ReaderT and use a textbook (->) r monad:

{-# LANGUAGE FlexibleContexts #-}
module Foo where
import Data.Coerce (Coercible, coerce)

newtype RT r o = RT { runR :: r -> o }
data Flow i o = Flow (i -> RT Int o) (o -> i)

coerceFlow
    :: (Coercible i i', Coercible o o')
    => Flow i o
    -> Flow i' o'
coerceFlow = coerce

Cannot 'coerce' data type with 'Reader' as a field

2 Answers2