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 either sacrifice 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 quantified types, 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.