Abstract
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.