Type applications should be unified

[atennapel]

At the moment you're doing the following in subtype:
t1 t2 <: t1' t2' => t1 <: t1' /\ t2 <: t2'
But you don't know in general whether to compare it covariantly or contravariantly.
If I define, for example:
type Fun a b = a -> b
Then Fun a <: Fun b should actually be compared contravariantly b <: a.
So one solution is to give up and switch to unification in the case of type applications. Comparing foralls by alpha-equality.
That's also what Purescript does (and what I am planning to do for my own language).