Nested automatization of type inference of forall elimination

Question

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?

Answer 1

This can be solved as easily as the other problem, as in this solution. It's basically unification.

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.