Pattern match coverage checking is implemented following the algorithm described in Lower Your Guards. The goal of pattern match coverage checking is to identify the following problems that may arise in a pattern match:

• It is missing clauses (i.e. it is non-exhaustive)
• It contains redundant patterns (i.e. the case can be deleted without altering the program)
• It contains inaccessible patterns (i.e the rhs can never be entered)

Furthermore, in the case of a non-exhaustive match, the goal to present the user with concrete values that do not match any of the existing patterns.

N.B. An inaccessible pattern in unison would be one that performs effects in a guard although the constraints are unsatisfiable. Such a pattern cannot be deleted without altering the program.

High-level algorithm overview

1. Desugar a match expression into a GrdTree.
2. Annotate the GrdTree leaves with refinement types describing values that match this branch. Redundant and inaccessible patterns are then identified by GrdTree leaves with uninhabited refinement types. Inaccessible patterns are distinguished by an effect being performed between the GrdTree root and the leaf.
3. Traverse the GrdTree building up a refinement type describing uncovered values. If the resulting refinement type is inhabited then the match is missing clauses.
4. Find inhabitants of the uncovered refinement type to present to the user.

Step (1) is implemented by desugarMatch. Steps (2) and (3) are implemented as a single traversal: uncoverAnnotate/classify. Step (4) is implemented by expandSolution/generateInhabitants.