First-class polymorphism is what System F gives you: functions from types to values. Second-class polymorphism is what Damas-Milner gives you: let-bound identi

First-class polymorphism is what System F gives you: functions from types to values. Second-class polymorphism is what Damas-Milner gives you: let-bound identifiers may admit more than one type, in which case every type they admit is subsumed by a type schema. Second-class polymorphism rules out polymorphic recursion if you consider every recursive definition as syntactic sugar for applying a fixed point combinator to some expression of type `a -> a`, for whatever monotype `a`.