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

1 files changed, 13 insertions, 0 deletions

diff --git a/docs/users_guide/8.8.1-notes.rst b/docs/users_guide/8.8.1-notes.rst
index f97e79a3cf..0a095f02f2 100644
--- a/docs/users_guide/8.8.1-notes.rst
+++ b/docs/users_guide/8.8.1-notes.rst
@@ -27,6 +27,19 @@ Language
   they could only stand in for other type variables, but this restriction was deemed
   unnecessary in `GHC proposal #29 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst>`__. Also see :ghc-ticket:`15050`.
 
+- The pattern-match coverage checker now checks for cases that are unreachable
+  due to constructors have strict argument types. For instance, in the
+  following example: ::
+
+    data K = K1 | K2 !Void
+
+    f :: K -> ()
+    f K1 = ()
+
+  ``K2`` cannot be matched on in ``f``, since it is impossible to construct a
+  terminating value of type ``Void``. Accordingly, GHC will not warn about
+  ``K2`` (whereas previous versions of GHC would).
+
 Compiler
 ~~~~~~~~