#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