Is type unification a kind of search for alpha equivalence?

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?

• Where were you reading this? It might help to know the context of your question. Certainly unification is not $\alpha$-equivalence in general, if that's all you're asking.
– cody
Dec 10 '20 at 18:38
• cs.cornell.edu/courses/cs3110/2011sp/Lectures/… It was just a reasoning, I read about substitution and then this come to me that type unification may have some parallel with alpha equivalence Dec 10 '20 at 20:42