#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