Technical Report No. 240 - Abstract

Stefan Wehr, Peter Thiemann
Subtyping Existential Types

Constrained existential types are a powerful language feature that subsumes Java-like interface and wildcard types. But existentials do not mingle well with subtyping: subtyping is already undecidable for very restrictive settings. This paper defines two subtyping relations by extracting the features specific to existentials from current language proposals (JavaGI, WildFJ, Scala). Both subtyping relations are undecidable. The paper also discusses the consequences of removing existentials from JavaGI and possible amendments to regain their features.