  Type qualifiers offer a lightweight mechanism for enriching existing type
systems to enforce additional, desirable, program invariants. They do so by
offering a restricted but effective form of subtyping. While the theory of type
qualifiers is well understood and present in many programming languages today,
polymorphism over type qualifiers is an area that is less examined. We explore
how such a polymorphic system could arise by constructing a calculus System
F<:Q which combines the higher-rank bounded polymorphism of System F<: with the
theory of type qualifiers. We explore how the ideas used to construct System
F<:Q can be reused in situations where type qualifiers naturally arise -- in
reference immutability, function colouring, and capture checking. Finally, we
re-examine other qualifier systems in the literature in light of the
observations presented while developing System F<:Q.
