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.