Blanvillain, OlivierBrachthäuser, JonathanKjaer, MaximeOdersky, Martin2021-11-112021-11-112021-11-112021https://infoscience.epfl.ch/handle/20.500.14299/182992Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents \emph{match types}, a type-level equivalent of pattern matching. Match types integrate seamlessly into programming languages with subtyping and, despite their simplicity, offer significant additional expressiveness. We formalize the feature of match types in a calculus based on System F sub and prove its soundness. We practically evaluate our system by implementing match types in the Scala 3 reference compiler, thus making type-level programming readily available to a broad audience of programmers.text::report