We present a variant of the explicitly-typed second-order polymorphic λ-calculus with primitive open existential types, i.e., a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. We claim that open existential types model abstract types and module type generativity. Our proposal can be understood as a logically-motivated variant of Dreyer’s RTG where type generativity is no more seen as a side effect. As recursive types arise naturally with open existential types, even without recursion at the term-level, we present a technique to disable them by enriching the structure of environments with dependencies. The double vision problem is addressed and solved with the use of additional equalities to reconcile the two views.