Problem coercing a record with complex type parameters-CodePudding

I have this record:

import Data.Functor.Identity
import Control.Monad.Trans.Identity
import Data.Coerce

data Env m = Env {
        logger :: String -> m ()
    }

env :: Env IO
env = undefined

and this coercion function

decorate 
    :: Coercible (r_ m) (r_ (IdentityT m))   
    => r_ m -> r_ (IdentityT m)        
decorate = coerce

which is applicable to the record value without problems:

decoratedEnv :: Env (IdentityT IO)
decoratedEnv = decorate env

However, if I define the only slightly more complex record

data Env' h m = Env' {
        logger' :: h (String -> m ())
    }

env' :: Env' Identity IO
env' = undefined

And try to insert an IdentityT wrapper like I did before

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = decorate env'

I get the error:

* Couldn't match type `IO' with `IdentityT IO'
    arising from a use of `decorate'

To my mind, the extra Identity parameter taken by Env' shouldn't stop coerce from working. Why does coerce fail in this case? Is there a way to make coerce work?

CodePudding user response：

A coercion Coercible A B does not imply a coercion Coercion (h A) (h B) for all h.

Consider this GADT:

data T a where
  K1 :: Int  -> T A
  K2 :: Bool -> T B

Coercing T A to T B amounts to coercing Int to Bool, and that clearly should never happen.

We could perform that coercion only if we knew that the parameter of h has the right role (e.g. representational or phantom, but not nominal).

Now, in your specific case h is known (Identity), and has surely the right role, so it should work. I guess the GHC coercion system is not so powerful to handle such a "well behaved" h while rejecting the ill-behaved ones, so it conservatively rejects everything.

Adding a type hole seems to confirm this. I tried

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = _ decorate' @(Env' Identity)

and got the error

* Couldn't match representation of type: r_0 m0
                           with that of: r_0 (IdentityT m0)
    arising from a use of decorate'
  NB: We cannot know what roles the parameters to `r_0' have;
    we must assume that the role is nominal
* In the first argument of `_', namely decorate'
  In the expression: _ decorate' @(Env' Identity)
  In an equation for decoratedEnv':
      decoratedEnv' = _ decorate' @(Env' Identity)

The "NB:" part is right on the spot.

I also tried to insist, and force the role

type role Env' representational representational
data Env' h m = Env' {
        logger' :: h (String -> m ())
    }

to no avail:

* Role mismatch on variable m:
    Annotation says representational but role nominal is required
* while checking a role annotation for Env'

The best workaround I could find is to unwrap/rewrap, and exploit QuantifiedConstraints to essentially require that h has a non-nominal role:

decorate' 
    :: (forall a b. Coercible a b => Coercible (h a) (h' b))
    => Coercible m m'
    => Env' h m -> Env' h' m'
decorate' (Env' x) = Env' (coerce x)

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = decorate' env'

Not an ideal solution, since it goes against the spirit of Coercible. In this case, the rewrapping has only O(1) cost, but if we had, say, a list of Env' Identity IO to convert, we would pay O(N).