Foundations for the implementation of higher-order subtyping

We show how to implement a calculus with higher-order subtyping and subkinding by replacing uses of implicit subsumption with explicit coercions. To ensure this can be done, a polymorphic function is adjusted to take, as an additional argument, a proof that its type constructor argument has the desired kind. Such a proof is extracted from the derivation of a kinding judgement and may in turn require proof coercions, which are extracted from subkinding judgements. This technique is formalized as a type-directed translation from a calculus of higher-order subtyping to a subtyping-free calculus. This translation generalizes an existing result for second-order subtyping calculi (such as F-less than or equal to). We also discuss two interpretations of subtyping, one that views it as type inclusion and another that views it as the existence of a well-behaved coercion, and we show, by a type-theoretic construction, that our translation is the minimum consequence of shifting from the inclusion interpretation to the coercion-existence interpretation. This construction shows that the translation is the natural one, and it also provides a framework for extending the translation to richer type systems. Finally, we show how the two interpretations can be reconciled in a common semantics. It is then easy to show the coherence of the translation relative to that semantics.