Fixed points of representative bifunters

Question

The experimental package offers various tools for canceling coercion, some of which I inserted at the end of this question. Class key in package

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 ab -> Coercion (ta) (tb) 

Given the type

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

I hope to write something like

 instance Representational p => Representational (Fix p) 

I believe the following should work, with the exception of one missing piece. I'm also a little worried that bar might be strict enough to throw everything in 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 ab . Coercion ab -> Coercion (Fix pa) (Fix pb) rep x = sym blah . quux . baz . blah where bar :: Coercion (p (Fix pa)) (p (Fix pb)) bar = rep (rep x) baz :: Coercion (p (Fix pa) a) (p (Fix pb) a) baz = eta bar quux :: Coercion (p (Fix pb) a) (p (Fix pb) b) quux = undefined -- ????????? blah :: forall x . Coercion (Fix px) (p (Fix px) x) blah = Coercion 

Bits and pieces roles

 eta :: forall (f :: x -> y) (g :: x -> y) (a :: x). Coercion fg -> Coercion (fa) (ga) instance Representational Coercion instance Representational f => Representational (Compose f) 

Answer 1

The problem, as indicated, cannot be solved, since the fact that p is equal to Representational (or even Phantom ) does not mean that p (Fix pa) is representative. Here's a counterexample:

 data NF ab where NF :: NF a () instance Representational NF where rep _ = Coercion 

It is clear that NF a never representative; we cannot realize

 rep :: Coercion xy -> Coercion (NF ax) (NF ay) 

(regardless of the choice of a ), since NF ax populated only when x ~ () .

Therefore, we need a more refined notion of a representative bifuctor to make this idea reasonable. unsafeCoerce almost certainly necessary for its implementation in any case, because digging through an endless chain of Coercion will take an infinite amount of time, and Coercion cannot be matched lazily.

One (maybe valid?) Concept that I just suggested on GitHub :

 class Birepresentational t where birep :: Coercion pq -> Coercion ab -> Coercion (tpa) (tqb) instance Birepresentational f => Representational (Fix f) where rep (x :: Coercion ab) = (birep :: forall pqxy . Coercion pq -> Coercion xy -> Coercion (fpx) (fqy)) (unsafeCoerce x :: Coercion (Fix fa) (Fix fb)) x `seq` unsafeCoerce x 

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