Said like that it's wrong. In FOL +ZFC a variable *can* represent a set.
I suppose that to explain the problem with FOL, we must inform the reader that there exists two kinds of variables. One of them represents
the so-called individuals. The second represents propositions. In FOL only the variables that represent individuals can be quantified.
Regarding the types introduced by Russel, I suppose one must say his main issue was to remove the paradox discovered by him
regarding some previous works by Frege. According to Frege a variable representing any collection can be quantified. That can't work. With
types you constrain what can be quantified. The second way to solve the paradox is to make a distinction between the classes and the
sets. A class represents any collection. Sets are a sub-collection of classes. Axioms determinate what classes are sets. This is the
solution used in set theory, also called ZFC (Zermelo Fraenkel with choice after its inventors).
But the logic used by TLA+ is a subset of FOL + ZFC. And it uses a Gentzen style of proof with the natural deduction axioms
available. And there are some oddities like the construct of a function. But it is due to the fact that it is algorithm oriented and according to
Leslie, few mathematics are needed to speak of algorithms (that doesn't mean simple mathematics, a look at Knuth's books will demonstrate
the opposite). So anyway no type, no higher-order language.
--
FL