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?