The connection between polymorphic and dynamic typing was originally consideredby Curry et al. (1972, Combinatory Logic, vol.ii) in the form of “polymorphic type assignment” for untypedλ-terms. Types are assigned after the fact to what is, in modernterminology, a dynamic language. Interest in type assignment was revitalized bythe proposals of Bracha et al. (1998, OOPSLA) and Banket al. (1997, POPL) to enrich Java with polymorphism(generics), which in turn sparked the development of other languages, such asScala, with similar combinations of features. In such a setting, where thetarget language already has a monomorphic type system, it is desirable tocompile polymorphism to dynamic typing in such a way that as much static typingas possible is preserved, relying on dynamics only insofar as genericity isactually required. The basic approach is to compile polymorphism usingembeddings from each type into a universal “top” type, ${\mathbb{D}}$ , and partial projections that go in theother direction. This scheme is intuitively reasonable, and, indeed, has beenused in practice many times. Proving its correctness, however, is non-trivial.This paper studies the compilation of System F to anextension of Moggi's computational meta-language with a dynamic type and showshow the compilation may be proved correct using a logical relation.