As a consequence/means of avoiding Russel's paradox, the standard axiomatization of set theory (ZFC), doesn't allow sets to contain themselves (so no set of all sets). Thus, if types are sets of values, and types are values, you've got a problem since the type of types seems to be a set that contains itself. Of course, I think this just means that well-founded set theories like ZFC are a poor choice for modeling type systems for languages with first-class types. There are set theories that allow sets to contain themselves [http://en.wikipedia.org/wiki/Non-well-founded_set_theory]. Such set theories don't replace ZFC, but rather extend it, adding "hypersets", which are the sets that contain themselves – the well-founded sets behave as usual.