Get rid of fmapCoerce by ensuring our functors are representational

[shlevy]

Note that I didn't try to minimize the use of RepresentationalMonad, since all real functors should be "representational" in this sense anyway, but perhaps some of these changes could be reverted back to Monad.

[phadej]

Nice but restrictive. Many Monads are not representational in the last argument. Essentially all transformers, e.g. ReaderT.

[shlevy]

@phadej Even when fully concrete? I.e. wouldn't ReaderT Int IO be representational?

When not concrete we can just require m to be RepresentationalMonad too, right?

[shlevy]

Indeed the universal instance here when specialized to ReaderT should automatically be morally equivalent to instance RepresentationalMonad m => RepresentationalMonad (ReaderT r m)

[shlevy]

Yes, this works

foo :: (forall a b. Coercible a b => Coercible (f a) (f b), Applicative f) => f ()
foo = pure ()

bar :: IO ()
bar = foo

baz :: ReaderT r IO ()
baz = foo

{- Nope
qux :: (Applicative m) => ReaderT r m ()
qux = foo
-}

quux :: (Applicative m, forall a b. Coercible a b => Coercible (m a) (m b)) => ReaderT r m ()
quux = foo

[phadej]

It works because ReaderT is newtype. That won't work for non-newtype transformers, as there won't be a way to go via through newtype-coercions.

[shlevy]

Hmm I see. I don't fully understand why yet, but yes that's not working here to redefine ReaderT as a data type.

Are there any real-world examples of such transformers? I'm used to always seeing them as newtypes, and all the ones I could find starting from the instance list of MonadReader are.

[shlevy]

It's odd to me that p2 typechecks but p3 doesn't... Is this a necessary limitation?

newtype ReaderT r m a = ReaderT { runReaderT :: r -> m a }

data ReaderTData r m a = ReaderTData { runReaderTData :: r -> m a }

data ReaderTIO r a = ReaderTIO { runReaderTIO :: r -> IO a }

representationalProxy :: (forall a b. Coercible a b => Coercible (f a) (f b)) => Proxy f
representationalProxy = Proxy

p1 :: Proxy (ReaderT r IO)
p1 = representationalProxy

p2 :: Proxy (ReaderTIO r)
p2 = representationalProxy

p3 :: Proxy (ReaderTData r IO)
p3 = representationalProxy

[phadej]

That because ReaderTIO has representational role, but ReaderTData doesn't, because we don't have higher order roles, so GHC has to assume the worst from m.

Load into ghci and look for the roles in :i output.

[shlevy]

Right, but fully unsaturated ReaderT doesn't have representational role either. I'm wondering why partial saturation doesn't change role inference in one case and does in another. It's not clear why you'd need higher-order roles for that.

[phadej]

• newtype ReaderT r IO a works by coercing (using newtype coercion) to r -> IO a, which is coercible to r -> IO b and then back to ReaderT r IO b.
• data variant doesn't have that option, so that example doesn't work, data ReaderT r m a has type role ReaderT representational nominal nominal
• data ReaderTIO is representational, so there is axiom "Coercible a b => Coercible (ReaderTIO r a) (ReaderTIO r b)(in factReaderTIO` is representational in both arguments), so that example works

For more information read through https://www.microsoft.com/en-us/research/uploads/prod/2018/05/coercible-JFP.pdf, in particular section 2.8 Supporting higher order polymorphism and 8.1 Roles for higher-order types

TL;DR this needs support from GHC, higher order stuff just doesn't work. QuantifiedConstraints tricks get us somewhere, but nowhere close to proper support.

[phadej]

And to be clear about expectations: I won't merge this, nor work on other issues. GHC doesn't allow me to express what I want, and that was already identified in the original paper introducing roles.

[phadej]

And FYI:

since all real functors should be "representational" in this sense anyway,

They should, but they aren't. There are fake functors too, e.g. https://hackage.haskell.org/package/bifunctors-5.5.14/docs/src/Data.Biapplicative.html#Mag and people will complain loudly if you suggest forcing Functors to be representational. (That is though inpractical, as GHC fails even with simple ReaderT example - first that have to be possible).

EDIT: I tried to argue against, e.g. Mag can be still made representational, but then people complain that

  One :: a -> Mag a b b

has unboxed (equality) coercion, but

  One :: Coercible b c => a -> Mag a b c

would have unboxed one. So I guess you'd need to figure out how to tell GHC to have boxed coercions.

---

So TL;DR, this issue has long history, and sorry that you had to re-learn it. But I'm somewhat frustrated going though arguments every other year.

[shlevy]

Sorry to bring this back up. I've opened https://gitlab.haskell.org/ghc/ghc/-/issues/22644, which I think would help with specifically the issue here without requiring the full solution of higher order roles or the Functor superclass. I guess we'll see how it's taken.