Virtual types are a combined genericity and covariance mechanism first introduced in BETA. Like most other covariant language constructs, virtual types in their original form depend on dynamic checking for type safety. This paper presents full statical type checking for virtual types, while not relying on any other special language mechanisms for safety. Good expressiveness is retained, as demonstrated by a simple but effective solution to the infamous ColourPoint problem.

Full paper [ps.gz]