#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: | -------------------------------------+------------------------------------- Description changed by bgamari: Old description:
Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!
Another missing piece is exhaustiveness checks. Given this pattern {{{ initLast [] = Nothing initLast xs = Just (init xs, last xs) pattern xs ::: x <- (initLast -> Just (xs,x)) }}} we want the compiler to tell the programmer that {{{ f [] = ... f (xs ::: x) = ... }}} is complete, while {{{ g (xs ::: x) = ... }}} is not.
With view pattern directly, this is impossible. But the programmer did not write view patterns!
So here is what I think might work well, inspired by the new `MINIMAL` pragma:
We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case.
{{{ {-# COMPLETE_PATTERNS [] && (:::) #-} }}}
Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors.
When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`.
Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement.
New description: Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting! Another missing piece is exhaustiveness checks. Given this pattern {{{#!hs initLast [] = Nothing initLast xs = Just (init xs, last xs) pattern xs ::: x <- (initLast -> Just (xs,x)) }}} we want the compiler to tell the programmer that {{{#!hs f [] = ... f (xs ::: x) = ... }}} is complete, while {{{#!hs g (xs ::: x) = ... }}} is not. With view pattern directly, this is impossible. But the programmer did not write view patterns! So here is what I think might work well, inspired by the new `MINIMAL` pragma: We add a new pragma `COMPLETE_PATTERNS` (any ideas for a shorter name). The syntax is essentially the same as for `MINIMAL`, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case. {{{#!hs {-# COMPLETE_PATTERNS [] && (:::) #-} }}} Multiple pragmas are obviously combined with `||`, and there is an implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data constructors. When checking for exhaustiveness, this would be done before unfolding view patterns, and for `g` above we get a warning that `[]` is not matched. Again, the implementation is very much analogous to `MINIMAL`. Clearly, a library author can mess up and give wrong `COMPLETE_PATTERNS` pragmas. I think that is ok (like with `MINIMAL`), and generally an improvement. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8779#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler