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
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
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
.
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With