\emph{Type refinements}, introduced by Freeman and Pfenning and explored by
Davies and Dunfield, unify the ontological and epistemic views of typing.
Types tell us what programming language constructs exist, whereas refinements
express properties of the values of a type. Here we show that refinements are
very useful in compiler correctness proofs, wherein it often arises that two
expressions that are inequivalent in general are equivalent in the particular
context in which they occur. Refinements serve to restrict the contexts
sufficiently so that the desired equivalence holds. For example, an
expression might be replaced by a more efficient one, even though it is not
generally equivalent to the original, but is interchangeable in any context
satisfying a specified refinement of the type of those expressions.
We study here in detail a particular problem of compiler correctness, namely
the correctness of compiling polymorphism (generics) to dynamic types by
treating values of variable type as values of a universal dynamic type.
Although this technique is widely used (for example, to compile Java
generics), no proof of its correctness for System~F has been given to date.
Surprisingly, standard arguments based on logical relations do not suffice,
precisely because it is necessary to record deeper invariants about the
compiled code than is expressible in their types alone. We show that
refinements provide an elegant solution to this problem by capturing the
required invariants so that a critical invertibility property that is false is
general can be proved to hold in the contexts that arise in the translated
code. This proof not only establishes the correctness of this compilation
method, but also exemplifies the importance of refinements for compiler
correctness proofs more generally.