Singleton kinds provide an elegant device for expressing type equality
information resulting from modern module languages, but they can
complicate the metatheory of languages in which they appear. I present a
translation from a language with singleton kinds to one without, and prove that
translation to be sound and complete. This translation is useful for
type-preserving compilers generating typed target languages. The proof of
soundness and completeness is done by normalizing type equivalence derivations
using Stone and Harper's type equivalence decision procedure.
