Subtyping provides polymorphism at a low cost: a higher-order function can take a parameter at the concise type $Int \to Top$, accepting every function on integers whatever it returns. The parametric alternative $\forall B.,(Int \to B) \to \ldots$ spends a quantifier and a type parameter to express the same, and this cognitive overhead grows as types get larger. Polymorphism via subtyping, however, is not always enough, as $Int \to Top$ forgets the precise result type, so a program that needs it must abandon the concise signature and return to full parameterization. What is missing is a lightweight form of polymorphism that is as concise and readable as subtyping yet recovers the precision of parametricity. Hofmann and Pierce’s type destructors provide such polymorphism for covariant type formers but do not address contravariant positions, such as function arguments. Projection types in practice, such as TypeScript’s Parameters<T> and ReturnType<T>, rely on the unsound any type for abstract function types.

To close this gap, we present $F^{DR}{<:}$, an extension of System $F{<:}$ with first-class domain and range projection types, $Dom(T)$ and $Range(T)$, and an application rule that types $f(x)$ from $f : F$ and $x : Dom(F)$ for an arbitrary type $F$. The requirement to expose $F$ as an arrow type is delayed from the definition site to the call site and discharged by the argument itself, as a value of type $Dom(F)$ exists only when $F$ is a subtype of an arrow type. The type variable $F$ then needs no informative bound to represent a function type, only $<: Top$, yet a function $f : F$ can still be applied without losing precision. We call this boundless quantification.

We prove semantic type soundness and weak normalization by logical relations, where path selection delays a projection’s interpretation until the underlying arrow type is resolved. The approach generalizes beyond arrow types, for example to product projections, which cooperate with domain and range in one system. All of our development has been mechanized in Rocq.