Note that when apply a context as a substitution, the substitution should be applied either
right to left
simultaneously
Specifically, this means that applying the context [e0 = A, e1 = e0 -> A] is equivalent to applying either:
from right to left, the substitution A/e0, (e0 -> A)/e1
simultaneously, the substitution A/e0, (A ->A)/e1
The effect of this is that any assignments between existential variables are resolved as much as possible. This is important because when typechecking a function type we generate assignments between existentials such as e0 = e1 -> e2, e1 = A, e2 = B.
We should double check we're doing this correctly.
Note that when apply a context as a substitution, the substitution should be applied either
Specifically, this means that applying the context
[e0 = A, e1 = e0 -> A]is equivalent to applying either:A/e0, (e0 -> A)/e1A/e0, (A ->A)/e1The effect of this is that any assignments between existential variables are resolved as much as possible. This is important because when typechecking a function type we generate assignments between existentials such as
e0 = e1 -> e2, e1 = A, e2 = B.We should double check we're doing this correctly.