[nathanrf]

The quoted paragraph is correct as written. E.g. if

f: ∀A, B. A -> B -> A

Then we have poly type π = "∀A, B. A -> B -> A".

The monotype μ = Str -> Int -> Str is a specialization of π, so we are also permitted to judge that f has type μ.

The type specialization operator "looks backwards", where we write sorta "π ≤ μ" because there's a kind of "subtyping" relationship (though most HM type systems don't actually contain subtyping) - anywhere that a term of type μ is used, a term of type π can be used instead because it can be specialized to μ.

I think this is a good complementary article: https://boxbase.org/entries/2018/mar/5/hindley-milner/ (it also links to three more academic sources for more context/detail)