type-checking of `coerce` depends on which newtype constructors are imported
Consider
module M where
newtype M m a = MkM (m a)
module Test where
import M (M)
import Data.Coerce
import Data.Functor.Identity
f :: M IO Int -> M IO (Identity Int)
f x = coerce x
Test
won't compile in GHC 8.10, 9.0 (haven't tried HEAD yet).
But if I also import the newtype constructor MkM
, it compiles, presumably because it can look at the definition of M
to figure out that its use of a
is representational if IO
's first type param has a representational role, which it can only do with the information avaialble at its use site.
Why do I need to import MkM
? Can't GHC do this automatically for me? What if M
didn't export MkM
?
This came up in !7329 (comment 401587), where EtaReaderT
wraps around ReaderT
and now EtaReader
has to export the ReaderT
newtype constructor or otherwise has to force all use sites to import Control.Monad.Trans.Reader
, which I'd say is an implementation detail.
Do note that hiding the implementation of M
leads to a degradation in the ability to coerce it, even though doing so would be safe. (Of course the other side of the coin is that use sites might break if we change the implementation of M
...)
Is this expected behavior? I was very confused by what I thought would just have been a refactoring.
To be clear, I don't want the fact of whether or not I import an unused newtype constructor to influence type-checking. That means I could live with either
- Always unfold newtype definitions, whether it is or can be imported or not. (I see problems, like "the other side of the coin" above.)
-
Never unfold newtype definitions to type-check
coerce
. The only means of reasoning about whether a coerce is permitted should be based on inferred or annotated roles.
I'd favor (2), but that would amount to a lot of back compat problems.
In order for (2) to be realistic, it seems we'd need higher-order role annotations to encode the necessary information, so that we no longer need to unfold definitions at use sites. E.g.,
type role IO :: representational
-- so the abstraction of IO in terms of roles is like `(\r -> r) :: Role -> Role`
newtype M m a = MkM (m a)
type role M \rm. representational (rm representational)
-- so the abstraction of M in terms of roles is like `(\rm ra -> worseRole (rm ra) ra) :: (Role -> Role) -> Role -> Role`
Then M IO Int
would compute to (\rm ra -> worseRole (rm ra) ra) (\r -> r) Representational => worseRole (id Repr.) Repr. => Representational
. Very roughly speaking (of course eventually we must relate the two types we coerce). I hope you get the idea.
I think these abstractions can be defined generically, over all kinds (and are overriden by user-defined role annotations).