Syntactically Restricting Bounded Polymorphism for Decidable Subtyping.

Subtyping of Bounded Polymorphism has long been known to be undecidable when coupled with contra-variance. While decidable forms of bounded polymorphism exist, they all sacrifice either useful properties such as contra-variance (Kernel F\(_{<:}\)), or useful metatheoretic properties (F\(_{<:}^\top \)). In this paper we show how, by syntactically separating contra-variance from the recursive aspects of subtyping in System F\(_{<:}\), decidable subtyping can be ensured while also allowing for both contra-variant subtyping of certain instances of bounded polymorphism, and many of System F\(_{<:}\)’s desirable metatheoretic properties. We then show that this approach can be applied to the related polymorphism present in D\(_{<:}\), a minimal calculus that models core features of the Scala type system.