This paper presents a new type system that combines strong existential types,higher-rank polymorphism, and polymorphic subtyping. We begin by presenting a declarative type system, and contributing several metatheoretic results. We then detail an algorithmic type inference system featuring bidirectional type checking. We prove that the algorithm is sound. Moreover, we propose two design variants of the declarative system with respect to which the algorithmic system is complete. This work can serve as a basis for further studies on strong existentials, their corresponding type inference algorithms,and their combinations with higher-rank polymorphism and subtyping.