What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of those systems include/exclude? Is it possible to express the intuition behind the criteria with words?

In the simply-typed lambda calculus, the type of a function must be fully specified, even when it's irrelevant. A trivial example is the identity function: in the lambda calculus, it's $\lambda x.x$; in the simply-typed lambda calculus, there isn't a single identity function but rather a family of identity functions $\lambda x:T. x$ for every type $T$. This means that the simply-typed lambda calculus has no polymorphism. If you think about data structures, more concrete examples come up — you can't write, say, a generic function like list reversal, you have to write it all over again for each type of list elements. You can't even write basic primitives like nil and cons, only typed-indexed primitives $\texttt{nil}_T$ and $\texttt{cons}_T$.

To give a concrete example in the pure lambda-calculus (without constants), natural numbers can be encoded as Church numerals in the untyped lambda calculus:
$$\begin{align}
0 &= \lambda f. \lambda x. x \\
1 &= \lambda f. \lambda x. f x \\
2 &= \lambda f. \lambda x. f (f x) \\
&\ldots
\end{align}$$
In the simply-typed lambda calculs, there is a separate family of Church numerals for each type:
$$\begin{align}
0_T &= \lambda f : T\to T. \lambda x : T. x \\
1_T &= \lambda f : T\to T. \lambda x : T. f x \\
2_T &= \lambda f : T\to T. \lambda x : T. f (f x) \\
&\ldots
\end{align}$$
You can't compose Church numerals of different types, which makes it difficult to use the same number for different things.

In the Hindley-Milner type system (which I'm including because it's an important step), polymorphic functions are possible, but with restrictions. Hindley-Milner requires a new syntactic form in addition to variables, application and abstraction: the let binding $\texttt{let } x = M \texttt{ in } N$. If all or part of the type of $M$ is irrelevant then it can be left as a variable, and the variable $x$ has not a type but a type scheme of the form $\forall \alpha_1,\ldots,\alpha_k, T$ where the $\alpha_i$ are type variables and the type expression $T$ can contain these variables. For example, it is possible to define the identity function once and for all:
$$
\texttt{let } \texttt{id} : (\forall \alpha, \alpha\to\alpha) = (\lambda x:\alpha. x) \texttt{ in } \ldots
$$
Similarly one can define Church numerals and (more practically) data structure manipulation (e.g. of lists, arrays, etc.) without having to duplicate the definitions for every type of element.

This form of polymorphism is known as parametric polymorphism; HM does not allow functions to behave differently depending on the types of their arguments. This allows proving properties of programs, such as “a function of type $\forall \alpha, \texttt{list}(\alpha) \to \texttt{int}$ only depends on the length of the list and not on the value of the elements”. This is known as “theorems for free” after the famous paper by Phil Wadler. An example of a practically useful function that cannot be expressed in HM is $\ge : \forall \alpha, \alpha \to \alpha \to \texttt{bool}$ which defines a total order — by parametricity, any such function is consant or non-terminating. More generally, HM cannot express ad hoc polymorphism (also known as generic programming in type theoretist circles, but beware that “generics” means parametric polymorphism in OOP circles).

In System F, functions can be parametrically polymorphic with no restrictions. Any lambda term can have universal quantifiers on types, which removes the distinction between $\lambda$ and $\texttt{let}$. Ad hoc polymorphism is still impossible (parametricity results still hold). System F allows more polymorphism than HM, at the expense of type inference (which is relatively easy for HM, and undecidable in System F).

Above I gave examples of programs that can't be expressed in HM and can't be expressed in System F either. Let me now give examples of programs that can be expressed in System F but not in HM. Simple examples are a bit more subtle. One simple example is the lambda term $\lambda x. x \, x$. What does it take to type it? In order for $\lambda x:T. x\,x$ to be well-typed, $T$ must satisfy the equations $T = T_1 \to T_2$ (for the occurrence of $x$ in function position) and $T_1 = T$ (for the occurrence of $x$ in application position). In Hindley-Milner, this is impossible, because types have a simple tree structure and a type satisfying these equations would have to be infinite. In System F, this term can be typed by breaking the recursion with a type abstraction:
$$
\Delta_F = \lambda x: (\forall \alpha, \alpha\to\alpha). x \, (\forall \alpha, \alpha\to\alpha) \, x
$$
While this may look of theoretical interest only, this is of highly practical interest when generalized to data structures. The term $\Delta$ condenses the wish for a single object to behave in a polymorphic way. System F, unlike HM, can express objects with polymorphic methods.

Besides ad hoc polymorphism, an important class of terms that still cannot be typed in System F is non-

StackExchange Computer Science Q#49189, answer score: 5