In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types".
In all the examples I have seen so far in the chapter, in particular Section 23.4 Examples, (not sure if I miss any example):
- all the type abstraction values are parametrically polymorphic functions, by allowing the types of their arguments to have any type, and
- all the universal types, i.e. the types of type abstraction values, are types of parametrically polymorphic functions.
Are type abstraction values and their universal types not for non functions, but only for functions?
More specifically, in any type abstraction value, say $\lambda X.t$, must $t$ have a function type, not a non-function type?
In Section 23.4 Examples, values of base types and of recursive types are type abstraction values, because their definitions in the section are functions by Church encodings.