A type quantifier in a position admitting only rank-1 polymorphism.
!>[A: $tType]: ... binds a type variable, which TPTP permits only at the
outermost position of a type. The TF1 grammar enforces this directly, since
<tf1_quantified_type> occurs only beneath <tff_top_level_type>. The TH1
grammar cannot, because THF identifies types with terms and therefore cannot
delimit a type. Consequently thf(f, type, f: ($i > !>[A: $tType]: A) > $o).
parses, denotes a rank-2 type, and is accepted by no TPTP implementation.
This is the only rule concerning a type rather than a term, and it remains
syntactic: a !> or ?* occurring beneath an arrow within the same typing is
rank-2. No elaboration is performed and the meaning of the type is not
considered.
A warning, since an implementation with genuine rank-N support may define its own extension.