No Naive Set Theoretic Models of Polymorphic Lambda Calculus?

In Philip Wadler's paper on Theorems for Free he states in Section 2 on Parametricity that


there are no naive set-theoretic models of polymorphic lambda calculus

In the naive set-theoretic model types are sets and functions are set-theoretic functions which seems reasonable. So why does he say there are no naive set-theoretic models of polymorphic lambda calculus?

The standard reference you are looking for is indeed Reynold's Polymorphism is not Set Theoretic. While it is quite obvious that you cannot form, e.g. the product $\Pi_{S\in\mathrm{Set}}S$ over all sets using the usual set theoretic product, it's a legitimate, and non-trivial question whether there is some weaker notion of product that would work, while preserving the usual binary product $\times$ and function space $\rightarrow$.

This turns out to not be possible either, since on one hand, it is rather easy to build a type $\bf 2$ such that the interpretation has at least 2 elements, and show that the interpretation of $T=\Pi_X(X\rightarrow {\bf 2})\rightarrow{\bf 2}$ is isomorphic to $(T\rightarrow {\bf 2})\rightarrow {\bf 2}$, which is not possible for the usual interpretation of $\rightarrow$ by the usual cantor paradox. In this sense it is somewhat similar to the proof for the untyped calculus.

Note that a further paper, by Andrew Pitts, Polymorphism is Set Theoretic, Constructively, overturns this conclusion somewhat by showing that the above contradiction is only possible to construct in classical set theory, and that there are several constructive theories of sets in which polymorphism can be interpreted with the usual interpretations of functions spaces and products. Most notably these "large products" exists in the Effective Topos, the most comprehensive of introductions being given by Phoa.

StackExchange Computer Science Q#51694, answer score: 14