Wait, so you can write programs in this thing that aren't primitive recursive? That's quite interesting; requiring primitive recursiveness is the usual way to guarantee termination. What class of programs does this language allow you to write? (It of course can't allow all programs that terminate, unless it also allows some that don't, which it claims not to.)
The type system appears to be System Fω[1], the “higher-order polymorphic lambda calculus”. I’m not really familiar with what class of programs it accepts, other than “more than simply typed lambda calculus”, but typechecking is decidable and evaluation is strongly normalising (i.e. both always terminate).
The type system is what prevents System Fw from being Turing complete. Specifically, the key bit is that you cannot unify the type "a -> b" with "a" (which is what prevents self application)
Sorry, that comment was worded badly. Both System F and System Fω can express self-application at a particular type, but they can’t give a general type for self-application, e.g., Ω = ω ω where ω = λx.xx.
