Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
like image 302
Shersh Avatar asked May 16 '20 16:05

Shersh


2 Answers

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.

like image 119
chi Avatar answered Nov 20 '22 07:11

chi


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
like image 26
Thomas M. DuBuisson Avatar answered Nov 20 '22 06:11

Thomas M. DuBuisson