# `Tptp.Lint.Rules.Rank1`
[🔗](https://github.com/jcschuster/tptp/blob/v0.1.3/lib/tptp/lint/rules/rank1.ex#L1)

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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*