By modeling incomplete programs as typed expressions with \emph{holes}, Hazel could provide meaningful feedback for incomplete programs. However, it only supports simple case analysis on binary sum types and does not support nested patterns nor pattern holes.

The paper formalizes full-fledges \emph{pattern matching} with typed holes. For a match expression with expression and pattern holes, we can still evaluate it when pattern matching must succeed or wait until the holes are filled when the pattern matching may succeed. The main contribution of the work is allowing for static reasoning about \emph{exhaustiveness} and \emph{redundancy} in an incomplete match expression. We define a constraint language with a 3-way logic by introducing the concept of maybe. By connecting the relationship between constraints and patterns, we reason about the runtime behavior of incomplete match expressions in static semantics. As a result, we can generate a warning when the match expression can’t be exhaustive or some rule must be redundant regardless of how the holes are filled.