Why do I have to coerce this data type by fields, rather than all at once?

Question

I have two types (<->) and (<-->) representing isomorphisms between types:

data Iso (m :: k -> k -> *) a b = Iso { to :: m a b, from :: m b a }
type (<->) = Iso (->)
infix 0 <->

data (<-->) a b = Iso' { to' :: a -> b, from' :: b -> a }
infix 0 <-->

The only difference between the two is that (<->) is a specialization of a more general type.

I can coerce (<-->) isomorphisms easily:

coerceIso' :: (Coercible a a', Coercible b b') => (a <--> b) -> (a' <--> b')
coerceIso' = coerce 

But I get an error when I try the same with (<->) isomorphisms:

coerceIso :: (Coercible a a', Coercible b b') => (a <-> b) -> (a' <-> b')
coerceIso = coerce
{-
src/Data/Iso.hs:27:13: error:
    • Couldn't match type ‘a’ with ‘a'’ arising from a use of ‘coerce’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          coerceIso :: forall a a' b b'.
                       (Coercible a a', Coercible b b') =>
                       (a <-> b) -> a' <-> b'
        at src/Data/Iso.hs:25:1-73
      ‘a'’ is a rigid type variable bound by
        the type signature for:
          coerceIso :: forall a a' b b'.
                       (Coercible a a', Coercible b b') =>
                       (a <-> b) -> a' <-> b'
        at src/Data/Iso.hs:25:1-73

-}

My current work-around is to coerce the forwards and backwards functions separately:

coerceIso :: (Coercible a a', Coercible b b') => (a <-> b) -> (a' <-> b')
coerceIso (Iso f f') = Iso (coerce f) (coerce f')

But why is such a workaround is necessary? Why can't (<->) be coerced directly?

Answer 1

The problem lies in the roles of the arguments m in your general Iso type.

Consider:

data T a b where
  K1 :: Int    -> T () ()
  K2 :: String -> T () (Identity ())

type (<->) = Iso T

You can't really expect to be able to convert T () () into T () (Identity ()) even if () and Identity () are coercible.

You would need something like (pseudo code):

type role m representational representational =>
          (Iso m) representational representational

but this can not be done in current Haskell, I believe.