  We use a semantic interpretation to investigate the problem of defining an
expressive but decidable type system with bounded quantification. Typechecking
in the widely studied System Fsub is undecidable thanks to an undecidable
subtyping relation, for which the culprit is the rule for subtyping bounded
quantification. Weaker versions of this rule, allowing decidable subtyping,
have been proposed. One of the resulting type systems (Kernel Fsub) lacks
expressiveness, another (System Fsubtop) lacks the minimal typing property and
thus has no evident typechecking algorithm.
  We consider these rules as defining distinct forms of bounded quantification,
one for interpreting type variable abstraction, and the other for type
instantiation. By giving a semantic interpretation for both in terms of
unbounded quantification, using the dinaturality of type instantiation with
respect to subsumption, we show that they can coexist within a single type
system. This does have the minimal typing property and thus a simple
typechecking procedure.
  We consider the fragments of this unified type system over types which
contain only one form of bounded quantifier. One of these is equivalent to
Kernel Fsub, while the other can type strictly more terms than System Fsubtop
but the same set of beta-normal terms. We show decidability of typechecking for
this fragment, and thus for System Fsubtop typechecking of beta-normal terms.
