In the introduction, the authors cover essential terms such as “parametric polymorphism” and “overloading.” The combination of these two techniques, namely parametric overloading, is the topic of the rest of the paper.

The authors introduce the Wadler and Blott (W&B) type system, which subsumes parametric overloading and is stated to be undecidable, followed by the Volpano and Smith (V&S) restrictions that eliminate this undesirable property. The authors then present a relaxation of the V&S restrictions, called DCO, which maintains the decidability of the type inference problem. After the formal definition, the use of their expanded type system is motivated by a few convincing examples.

After introducing a theory of recursive kinds and providing algorithms for checking for emptiness, subkinding, and intersection, the authors give further insight into type inference with kinded types. This technique extends the unification (U) and type-checking (W) algorithms introduced by Hindley and Milner; the presentation is spiced with several proofs covering the correctness of U and the soundness and completeness of W.

The authors conclude with a good overview of related work, which also points out shortcomings in existing functional languages, including ML and Haskell.

This well-structured paper assumes familiarity with polymorphic type systems, in particular Hindley and Milner’s and Wadler and Blott’s. The detailed proofs cover several pages; they are very technical and are intended for researchers in type theory. Insight is given into recent developments on relaxing the restrictions of type systems with parametric overloading, which aims to combine functional and object-oriented programming languages.