The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.

Now, suppose this is an arrow and we want to give it an argument, then we would need to apply this term to the proper type such that it can receive such an argument. That is what I am asking if I can automatize: Is is possible to construct a function $f$ taking two terms and returning a type such that $f^{\Lambda X.t}_{r}$ give us the type needed to be replaced by $X$ in $t$ such that $t$ can accept the argument $r$?

Some examples:

• $f_{\lambda x^T.x}^{\Lambda X.\lambda x^{X\to X}.t}=T$.

• $f_{(\lambda x^{R\to T}.t)~s}^{\Lambda X.\lambda x^X.r}=T$