[GHC] #8779: Exhaustiveness checks for pattern synonyms

[GHC]

#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