Take strict fields into account in coverage checking
authorRyan Scott <ryan.gl.scott@gmail.com>
Mon, 27 Aug 2018 12:05:45 +0000 (14:05 +0200)
committerKrzysztof Gogolewski <krz.gogolewski@gmail.com>
Mon, 27 Aug 2018 12:05:45 +0000 (14:05 +0200)
commit744b034dc2ea5b7b82b5586a263c12f231e803f1
tree7650a75d9b2c9bff104d2e7f03db806aac7f70b6
parent7a3cda534d1447c813aa37cdd86e20b8d782cb02
Take strict fields into account in coverage checking

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
compiler/deSugar/Check.hs
docs/users_guide/8.8.1-notes.rst
testsuite/tests/pmcheck/should_compile/T15305.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T15305.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/all.T
testsuite/tests/simplCore/should_compile/T13990.stderr [new file with mode: 0644]