
#8779: Exhaustiveness checks for pattern synonyms -------------------------------------+------------------------------------- Reporter: nomeata | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I have to say I don't care for this `COMPLETE_PATTERNS` pragma at all, for several reasons: * In general there may be many sets of complete patterns for a data type, and ensuring that the `COMPLETE_PATTERNS` are correct and complete may be difficult. * The `COMPLETE_PATTERNS` pragmas are hand-written and unchecked, and therefore likely to go out of date as the data type changes, making pattern exhaustiveness checking unreliable. * Unlike the situation of type class methods with their `MINIMAL` pragmas, any module can define new view patterns for a given data type. How can two different modules cooperate to produce new sets of complete patterns containing pattern synonyms from both modules? * Also unlike type classes, it's not obvious (to me anyways) that there is a unique best way to use the information of the `COMPLETE_PATTERNS` pragmas, as pattern matches can be nested. Overall this proposed new feature doesn't seem to offer a very compelling solution (for full disclosure, I don't consider the problem of pattern synonym exhaustiveness checks particularly compelling in the first place; seems like scope creep). I would prefer something simple like * Pattern synonyms are checked for exhaustiveness as though they were expanded to their definitions. No hand-written pragmas needed. * GHC understands that if `p1`, ..., `pn` are exhaustive patterns for the result type of `f`, then `f -> p1`, ..., `f -> pn` are exhaustive patterns for the input type of `f`. This to some extent solves the problem of mixing patterns defined in different modules, as long as those patterns are defined in terms of the same "view functions". In some cases this may require defining several equivalent patterns with different definitions, such as `EmptyL` and `EmptyR`. This seems quite acceptable to me and probably clarifies the intent at the use site of the pattern anyways. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler