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

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/ https://boxbase.org/entries/2018/mar/5/hindley-milner/ (it also links to three more academic sources for more context/detail)