#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: | 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): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => PatternMatchWarnings -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: | 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): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): It's unclear to me what can even be done about this. The GADTs Meet Their Match paper is completely silent on the topic of bang patterns, so this seems like a theory bug, not an implementation one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: | 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): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: alanz, sh.najd@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: | 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): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I tried thinking of an (ad hoc) algorithm to check for this sort of thing. This is the closest I could get: 1. In `mkOneConFull` (which generates pattern-matching information for each constructor), record the type and strictness of each constructor's fields. 2. When checking if a match on that constructor is reachable, perform the following additional checks: i. Check if all fields are strict. ii. Check if each field's type is uninhabitable. If both (i) and (ii) are true, then deem the entire constructor to be unreachable. I think this would work for the original program, but not the program in comment:6 {{{#!hs data Abyss = MkAbyss !Abyss stareIntoTheAbyss :: Abyss -> a stareIntoTheAbyss a = case a of {} }}} Why? In order to check that a match on `(MkAbyss _)` is unreachable, we need to check: i. That the field of `MkAbyss` is strict. (This is the case.) ii. That the type of the field of `MkAbyss` (`Abyss`) is uninhabitable. But in order to check that `Abyss` in uninhabitable, we need to check the `MkAbyss` constructor again, which requires repeating this algorithm. Now we've entered an infinite loop! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new 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): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): My strong instinct here is to go back to the paper. In rule [UConVar] and friends we split up 'x' into a union of constructors {K x1, K2 x2 x3, K3}. Each of those split constructors comes with an extended `Delta`, which describes the constraints in scope. If these constraints prove contradicatory we can drop the entire branch. So for a strict constructor, say {{{ data T a where MkT :: a -> !a -> T a }}} we want to add a constraint to `Delta` that says that the type of that second argument is non-void; that is, it contains at least one element that terminates. So maybe we need a constraint `NonVoid( tau )`. In the OP, `NonVoid( Bar A )` would be a contradiction. In the implementation we have a simple "term oracle" that works alongside the type oracle that is implemented by the constraint solver. Maybe we could add the new constraint to the term oracle? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

I fail to see how this would work for recursive examples like the

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: new 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): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): program in comment:7 Correct. Computing `NonVoid( tau )` is an open-ended question. For some `tau`s (lke `Bar A`) it's easy; for others we could be more ambitious. It's probably undecidable in general. So we could start with something simple and become more ambitious later. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 ): 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

#15305: Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation -------------------------------------+------------------------------------- Reporter: jkoppel | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: fixed | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: error/warning at compile-time | pmcheck/should_compile/T15305 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5087 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => pmcheck/should_compile/T15305 * milestone: Research needed => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15305#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler