Coercion of newtyped reader monad given coercion for its value type

Question

A typeclass C with associated data family X requires a function coerceX. If I implement the typeclass like below, how do I write coerceX?

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}

import Data.Type.Coercion
import Control.Monad.Reader

data (T r t)

class C t where
  data X t :: * -> *
  coerceX :: Coercion a b -> Coercion (X t a) (X t b)

instance (C t) => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX = ...

Answer 1

It looks like you can lead GHC by the nose through the necessary coercions, like so:

{-# LANGUAGE InstanceSigs #-}
instance (C t) => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX :: forall a b. Coercion a b -> Coercion (X (T r t) a) (X (T r t) b)
  coerceX Coercion
    = gcoerceWith (coerceX Coercion :: Coercion (X t a) (X t b)) $
        (Coercion :: Coercion (X (T r t) a) (Reader r (X t a))) `trans`
        (Coercion :: Coercible a' b' => Coercion (Reader r a') (Reader r b')) `trans`
        (Coercion :: Coercion (Reader r (X t b)) (X (T r t) b))

Once the pattern match:

coerceX Coercion = ...

brings Coercible a b into scope, I think you need to explicitly invoke coerceX for the C t instance to get Coercion (X t a) (X t b). I don't see how GHC could deduce this automatically.

Now, in an ideal world, it would be then enough to write:

coerceX Coercion = gcoerceWith (coerceX Coercion :: Coercion (X t a) (X t b)) Coercion

and with Coercible (X t a) (X t b) in scope, GHC would be able to infer the representational equality of Reader r (X t a) and Reader r (X t b) and consequently the representation equality of X (T r t) a and X (T r t) b, but it can't quite make this leap.