Fixed points of representational bifunctors

Question

Edward Kmett's experimental roles package offers various utilities for lifting coercions, some of which I've pasted at the end of this question. The key class in the package is

class Representational (t :: k1 -> k2) where
  -- | An argument is representational if you can lift a coercion of the argument into one of the whole
  rep :: Coercion a b -> Coercion (t a) (t b)

Given the type

newtype Fix p a = In {out :: p (Fix p a) a}

I'm hoping to write something like

instance Representational p => Representational (Fix p)

I believe the following should work, except for one missing piece. I'm also a bit concerned that bar may be strict enough to throw everything into an infinite loop.

-- With {-# LANGUAGE PolyKinds, ScopedTypeVariables, etc.)
import Data.Type.Coercion
import Data.Coerce
import Data.Roles

instance Representational p => Representational (Fix p) where
  rep :: forall a b . Coercion a b -> Coercion (Fix p a) (Fix p b)
  rep x = sym blah . quux . baz . blah
    where
      bar :: Coercion (p (Fix p a)) (p (Fix p b))
      bar = rep (rep x)

      baz :: Coercion (p (Fix p a) a) (p (Fix p b) a)
      baz = eta bar

      quux :: Coercion (p (Fix p b) a) (p (Fix p b) b)
      quux = undefined -- ?????????

      blah :: forall x . Coercion (Fix p x) (p (Fix p x) x)
      blah = Coercion

Bits and pieces of roles

eta :: forall (f :: x -> y) (g :: x -> y) (a :: x). 
       Coercion f g -> Coercion (f a) (g a)

instance Representational Coercion
instance Representational f => Representational (Compose f)

Answer 1

The problem, as stated, cannot be solved, because the fact that p is Representational (or even Phantom) does not imply that p (Fix p a) is representational. Here's a counterexample:

data NF a b where
  NF :: NF a ()

instance Representational NF where
  rep _ = Coercion

Clearly, NF a is never representational; we cannot possibly implement

rep :: Coercion x y -> Coercion (NF a x) (NF a y)

(regardless of the choice of a) because NF a x is only inhabited when x ~ ().

Therefore, we need a more refined notion of representational bifunctor to make this idea sensible. unsafeCoerce is almost certainly necessary to implement it in any case, because digging through an infinite chain of Coercions would take an infinite amount of time, and Coercions can't be matched lazily.

One (possibly valid?) concept, which I just suggested on GitHub:

class Birepresentational t where
  birep :: Coercion p q -> Coercion a b -> Coercion (t p a) (t q b)

instance Birepresentational f => Representational (Fix f) where
  rep (x :: Coercion a b) = (birep :: forall p q x y . Coercion p q -> Coercion x y -> Coercion (f p x) (f q y))
                            (unsafeCoerce x :: Coercion (Fix f a) (Fix f b))
                            x `seq` unsafeCoerce x

The point of forcing application of birep is to (hopefully) make sure that it actually terminates, and therefore its type can be trusted.