  This work introduces the novel concept of kind refinement, which we develop
in the context of an explicitly polymorphic ML-like language with type-level
computation. Just as type refinements embed rich specifications by means of
comprehension principles expressed by predicates over values in the type
domain, kind refinements provide rich kind specifications by means of
predicates over types in the kind domain. By leveraging our powerful refinement
kind discipline, types in our language are not just used to statically classify
program expressions and values, but also conveniently manipulated as tree-like
data structures, with their kinds refined by logical constraints on such
structures. Remarkably, the resulting typing and kinding disciplines allow for
powerful forms of type reflection, ad-hoc polymorphism and type
meta-programming, which are often found in modern software development, but not
typically expressible in a type-safe manner in general purpose languages. We
validate our approach both formally and pragmatically by establishing the
standard meta-theoretical results of type safety and via a prototype
implementation of a kind checker, type checker and interpreter for our
language.
