When does a type generalise another type?

In languages like Haskell, with a Hindley-Milner type system, when does a type $t$ generalise a type $u$? I use the definition: $t$ generalises $u$ iff $\forall\ v: v \text{ unifies with } u \rightarrow v \text{ unifies with } t$.

I have an algorithm that given these types returns a unifier if one exist. The unifier is an ordered list of assignments $v_1 \mapsto t_1, v_2 \mapsto t_2, \dots, v_n \mapsto t_n$ such that applying $v_i := t_i$ to both types for ascending $i$ results in two identical types.

For instance, the types $(a,a)$ and $(p,q)$ unify with the unifier $a \mapsto p, p \mapsto q$: after applying these assignments both types are $(q,q)$.

It should be possible to use the unifier to see if a type generalises another type, but I can't figure it out at the moment. I couldn't find an existing algorithm either.

Note: if there is an easier way, without using the unifier, that would be appreciated as well.

A pretty easy way to see if $t$ generalizes $u$ if $u$ matches $t$:

replace all variables in $u$ by (fresh) constants, written $u_c$, and check if $u_c$ unifies with $t$.

If so, then there is a substitution $\sigma$ such that $t\sigma\equiv u$ which means by definition that $t$ is more general than $u$.

As mentioned in the comments, if $\mathrm{mgu}(t,u)$ succeeds and returns a substitution $\tau$, then $u$ matches $t$ iff $u\tau\equiv u$ up to variable renaming.

Note: Pattern matching is usually best implemented independently from unification, as it is simpler in general. In particular it isn't necessary to actually replace variables with constants in $u$. Beware of non-linearities in $t$ though: $\alpha\rightarrow \alpha$ does not match $\mathrm{int}\rightarrow\mathrm{bool}$!

StackExchange Computer Science Q#83034, answer score: 4