 We can see that constraining separation in this way avoids impredicativity, by  observing that the proof theoretic strength of CZF, which has only restricted separation, is within the range of predicativity. However, by adding full separation to CZF one obtains an impredicative theory, in fact, one with the same proof-theoretic strength as full second order arithmetic (Lubarsky 2006). See also Section 5 for a discussion of the role of proof theory in analysing constructive and intuitionistic set theories. 