Writing a rewrite rule involving rank-n types

Question

Below is a simplified version of a very similar problem I'm facing.

Consider the following types, and the function f1:

{-# LANGUAGE RankNTypes #-}

newtype D t = D t deriving Functor
newtype T t = T { getT :: t }

f1 :: (forall t'. t' -> D t') -> T t -> D (T t)

Notice that f1 can actually be id, because if we get passed function that works for all t we can of course specialise it like so:

f1 = id

Now lets consider the "inverse" function, f2:

f2 :: (T t -> D (T t)) -> t -> D t

This "unspecialises" the function, which can be implemented as follows:

f2 f x = getT <$> (f (T x))

We can combine f2 and f1 as follows, which is basically an identity function:

g :: (forall t'. t' -> D t') -> t -> D t
g x = f2 (f1 x)

Indeed, g is pretty much equivalent to the id function, and indeed we can instead define g as follows:

g = id

So we've established as f2 . f1 == id.

But when we write f2 . f1, I suspect GHC may not compile that down to id, because, f2 at least does some non trivial work.

I'd like to write a rewrite rule for f2 . f1, and here's my attempt:

{-# RULES
"f2f1" forall x. f2 (f1 x) = g x
#-}

As g as can be defined as id I figured this might be good.

But unfortunately this fails to compile. I suspect this is due to the higher ranked type in f1.

I realise if I changed the type signature of f1 like follows:

f1 :: (t -> D t) -> T t -> D (T t)
f1 f x = T <$> f (getT x) 

I could write a rewrite rule like follows:

{-# RULES
"f2f1" forall x. f2 (f1 x) = x
#-}

But now whenever I use f1 it isn't just id, but quite a bit more complex.

Is there a way to write a rewrite rule like f2 . f1 == id, without giving f1 an non id style implementation?

Further information:

Note that in my actual problem, both D and T are not newtypes.

D is any Functor f, and T is actually a Coyoneda, following on from this previous question regarding newtype deriving.

Answer 1

Polymorphic free variables in RULES must have type signatures. Simply use

{-# RULES
"f2/f1" forall (x :: forall t. t -> D t). f2 (f1 x) = x
  #-}