GADTs and Exhaustiveness: Looking for the Impossible

TL;DR

This paper investigates the limitations of exhaustiveness checking in GADT pattern matching, proving its undecidability, and proposes an improved algorithm to enhance practical coverage in functional programming languages like OCaml.

Contribution

It demonstrates the undecidability of exhaustiveness checking for GADTs and introduces a strengthened algorithm to improve practical detection of non-exhaustive patterns.

Findings

Proves the undecidability of exhaustiveness checking for GADTs.

Develops a modified type inference algorithm for better pattern analysis.

Enhances OCaml's pattern matching checks to cover more practical cases.

Abstract

Sound exhaustiveness checking of pattern-matching is an essential feature of functional programming languages, and OCaml supports it for GADTs. However this check is incomplete, in that it may fail to detect that a pattern can match no concrete value. In this paper we show that this problem is actually undecidable, but that we can strengthen the exhaustiveness and redundancy checks so that they cover more practical cases. The new algorithm relies on a clever modification of type inference for patterns.