Run-time type dispatch enables a variety of advanced optimization techniques for
polymorphic languages, including tag-free garbage collection, unboxed function arguments,
and flattened data structures. However, modern type-preserving compilers transform
types between stages of compilation, making type dispatch prohibitively complex at low
levels of typed compilation. It is crucial therefore for type analysis at these low levels
to refer to the types of previous stages. Unfortunately, no current intermediate language
supports this facility.
To fill this gap, we present the language LX, which provides a rich language of type
constructors supporting type analysis (possibly of previous-stage types) as a programming
idiom. This language is quite flexible, supporting a variety of other applications such as
analysis of quantified types, analysis with incomplete type information, and type classes.
We also show that LX is compatible with a type-erasure semantics.