I was reading about type unification and it moves through of substitution of variables. To me it looks like a search for an alpha equivalence... I mean, two types are unifiable if they are alpha equivalent, at last if they are in polymorphic form, is this right?
If I have
forall a.a -> a and
forall b.b -> b I can apply
[b/a]forall a.a -> a to achieve
forall a.a -> a. So they are unifiable!?
Going deeper I could unify
forall a.a -> a to
int -> int and then deduce that the first is more general because I can achieve the second by
[a/int] substitution on the first right?