-
Summary: 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 #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`. Test Plan: make test TEST=T15305 Reviewers: simonpj, bgamari Reviewed By: simonpj Subscribers: rwbarton, carter GHC Trac Issues: #15305 Differential Revision: https://phabricator.haskell.org/D5087
744b034d
