This paper establishes a new, limitative relation between the polymorphic lambda calculus and the kind of higher-order type theory which is embodied in the logic of toposes. It is shown that any embedding in a topos of the cartesian closed category of (closed) types of a model of the polymorphic lambda calculus must place the polymorphic types well away from the powertypes, P(X), of the topos, in the sense that P(X) is a subtype of a polymorphic type only in the case that X is empty (and hence P(X) is terminal). As corollaries, we obtain strengthenings of Reynolds' result on the non-existence of set-theoretic models of polymorphism.