The current pattern-match coverage checker implements the
formalism presented in the GADTs Meet Their Match paper in a
fairly faithful matter. However, it was discovered recently that
there is a class of unreachable patterns that
GADTs Meet Their Match does not handle: unreachable code due to
strict argument types, as demonstrated in Trac #15305. This patch
therefore goes off-script a little and implements an extension to
the formalism presented in the paper to handle this case.
Essentially, when determining if each constructor can be matched on,
GHC checks if its associated term and type constraints are
satisfiable. This patch introduces a new form of constraint,
NonVoid(ty), and checks if each constructor's strict argument types
satisfy NonVoid. If any of them do not, then that constructor is
deemed uninhabitable, and thus cannot be matched on. For the full
story of how this works, see
Note [Extensions to GADTs Meet Their Match].
Along the way, I did a little bit of much-needed refactoring. In
particular, several functions in Check were passing a triple of
(ValAbs, ComplexEq, Bag EvVar) around to represent a constructor
and its constraints. Now that we're adding yet another form of
constraint to the mix, I thought it appropriate to turn this into
a proper data type, which I call InhabitationCandidate.