This question is about using relational parametricity to resolve practical questions in pure functional programming in System F.
Consider the following types of polymorphic functions:
$$ \forall a.\, ((a \rightarrow r) \rightarrow r) \rightarrow ((a \rightarrow r) \rightarrow r) $$
and
$$ \forall a.\, ((a \rightarrow r) \rightarrow s) \rightarrow ((a \rightarrow r) \rightarrow s) $$
where $s$ and $r$ are free type variables, i.e., fixed arbitrary types. Here we only consider pure lambda terms from System F, there are no side effects, all code is fully parametric, and so the parametricity theorems apply. In particular, all functions of the above types will be natural transformations.
It appears that the last type is equivalent to a pair of functions $ (r \rightarrow r, s \rightarrow s) $. But I don't know how to derive that type equivalence rigorously, and it is not clearly the correct type equivalence that one expects here.
As an example where a similar question can be answered straightforwardly, consider the type $\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$.
The type $\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$ can be simplified to $r \rightarrow s$ by using the (contravariant) Yoneda lemma:
$$ \forall a. (a \rightarrow t) \rightarrow (F\, a) \cong F\, t \quad \textrm{where } F \textrm { is a contravariant functor} $$
if we set $F\,x \overset{def}{=} x\rightarrow s $.
The Yoneda lemma may be used here because we assume that all values are pure lambda terms from System F. Then, by parametricity theorems of Reynolds and Wadler, all functions of type $\forall a. (a \rightarrow r) \rightarrow (a \rightarrow s)$ are natural transformations (their naturality law is a "free theorem" in the terminology of Wadler). So, the Yoneda lemma applies.
We may also use the relational parametricity theorems directly to derive this type equivalence:
$$ \forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s) \cong r \rightarrow s $$
Without the Yoneda lemma, we need a longer and more complicated proof, but we will still need to begin by deriving the naturality law and to proceed from there, in order to show that each function of type $\forall a.\, (a \rightarrow r) \rightarrow (a \rightarrow s)$ is expressed via a unique function of type $s \rightarrow r$.
However, the Yoneda lemma does not apply to the types shown at the beginning. (See solution below.)
Relational parametricity theorems can be used to simplify certain types containing universal quantifiers. However, it is never obvious how to use relational parametricity when the Yoneda lemma cannot be used. I don't seem to find a good trick to resolve this and similar questions about quantified types of the form $\forall a. (a \rightarrow r) \rightarrow s$.
