<p>This can be solved as easily as the other problem, as in this <a href="https://cstheory.stackexchange.com/questions/1362/in-system-f-a-la-church-can-we-automatize-type-inference-for-the-for-all-elimina/1366#1366">solution</a>. It's basically unification. </p>

<ol>
<li><p>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$.</p></li>
<li><p>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 <a href="http://www.math.uu.se/~palmgren/tillog/equlogic07.pdf" rel="nofollow noreferrer">this</a>.</p></li>
<li><p>The resulting mgu $[\bar{X}/\bar{W}]$ is the subtitution you require.</p></li>
</ol>

CC BY-SA 2.5
2010-10-06T13:41:50.420Z
2010-10-06T14:14:22.167Z
2017-04-13T12:32:28.077Z
Dave Clarke
<p>Following a <a href="https://cstheory.stackexchange.com/q/1362/743">previous question about how to automatize the type inference in a forall elimination of an application</a>, 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$.</p>

<p>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?</p>

<pl.programming-languages><type-theory><type-inference><polymorphism>
Nested automatization of type inference of forall elimination
Alejandro DC
# Nested automatization of type inference of forall elimination

(Asked by: username_0 on 2010-10-06)

Following a [previous question about how to automatize the type inference in a forall elimination of an application](https://cstheory.stackexchange.com/q/1362/743), 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?

**Tags:** pl.programming-languages, type-theory, type-inference, polymorphism


---

## 1 answers

### Answer by username_1 on 2010-10-06. Score: 5 | Accepted answer

This can be solved as easily as the other problem, as in this [solution](https://cstheory.stackexchange.com/questions/1362/in-system-f-a-la-church-can-we-automatize-type-inference-for-the-for-all-elimina/1366#1366). 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](http://www.math.uu.se/~palmgren/tillog/equlogic07.pdf).
3. The resulting mgu $[\bar{X}/\bar{W}]$ is the subtitution you require.


---

