[GHC] #15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation

[GHC]

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness
annotation
-------------------------------------+-------------------------------------
        Reporter:  jkoppel           |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  Research
       Component:  Compiler (Type    |  needed
  checker)                           |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D5087
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Krzysztof Gogolewski <krz.gogolewski@…>):

 In [changeset:"744b034dc2ea5b7b82b5586a263c12f231e803f1/ghc"
 744b034d/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="744b034dc2ea5b7b82b5586a263c12f231e803f1"
 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
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15305#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler