Type variables in patterns

TL;DR

This paper provides a formal specification for binding type variables in patterns in Haskell, clarifying previous ambiguities and improving language design by extending existing features.

Contribution

It offers a formal specification for type variable binding in patterns, enabling more explicit and cleaner language semantics in Haskell.

Findings

Formal specification clarifies previous ambiguities

Extension of ScopedTypeVariables for explicit binding

Elimination of Proxy workaround

Abstract

For many years, GHC has implemented an extension to Haskell that allows type variables to be bound in type signatures and patterns, and to scope over terms. This extension was never properly specified. We rectify that oversight here. With the formal specification in hand, the otherwise-labyrinthine path toward a design for binding type variables in patterns becomes blindingly clear. We thus extend ScopedTypeVariables to bind type variables explicitly, obviating the Proxy workaround to the dustbin of history.