编写涉及Rank-n类型的重写规则

以下是我面临的非常类似问题的简化版本。

考虑以下类型和函数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)

注意f1实际上可以是id，因为如果我们通过了对所有功能都有效的函数，那么t我们当然可以像这样专门化它：

f1 = id

现在让我们考虑“逆”函数f2：

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

此功能“非专业化”，可以按以下方式实现：

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

我们可以结合f2和f1如下，这基本上是一种身份的功能：

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

实际上，g该id函数与该函数几乎等效，并且实际上我们可以定义g如下：

g = id

因此，我们已将设置为f2 . f1 == id。

但是，当我们撰写本文时f2 . f1，我怀疑GHC可能无法将其编译为id，因为f2至少至少做了一些琐碎的工作。

我想为编写重写规则f2 . f1，这是我的尝试：

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

正如我g所定义的那样，id这可能很好。

但是不幸的是，这无法编译。我怀疑这是由于中排名较高的类型造成的f1。

我意识到如果我改变了f1如下的类型签名：

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

我可以编写如下的重写规则：

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

但是现在，无论何时我使用f1它不只是id，而且要复杂得多。

有没有办法编写类似的重写规则f2 . f1 == id，而不给出f1非id样式实现？

更多的信息：

请注意，在我的实际问题中，D和T都不是新类型。

D任何Functor f和T实际上是一个Coyoneda从下面就这个问题以前就NEWTYPE推导。