# Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\Lambda X_2.\dots.\Lambda X_n.\lambda x:U.t)$ is a function of type $\forall \vec{X}.U\to T$ and we want to apply it to an argument of type $V$. Then we need to find types $W_1,\dots,W_n$ such that $U[\vec{X}/\vec{W}]=V$.

This is clearly another unification problem. Can we solve this problem as easily as the problem with one variable? What is the algorithm for doing this?

1. Ensure that the variables $X_1,\ldots,X_n$ do not appear in $V$. Replace any variables that do by fresh ones and perform appropriate substitution into $W$.
2. Unify $V$ and $W$ using an algorithm that finds the most general unifier (mgu). The essence of this is in the other algorithm, or, for example, page 10 of this.
3. The resulting mgu $[\bar{X}/\bar{W}]$ is the subtitution you require.