[GHC] #8779: Exhaustiveness checks for pattern synonyms

[GHC]

#8779: Exhaustiveness checks for pattern synonyms
-------------------------------------+-------------------------------------
        Reporter:  nomeata           |                Owner:  mpickering
            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):  Phab:D2669
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Somehow I've not looked at this thread, finding this only by a mention of
 `COMPLETE` elsewhere. (This is my fault -- just explaining my silence on
 this topic which is in my area of interest.)

 A few nitpicks about the specification:
  - The wiki page uses "total" in several places, but I think you mean
 "covering". I use "total" to refer to functions that are both covering and
 terminating.

 - Would the following be acceptable?

 {{{
 data Void
 data T = T1 Int | T2 Bool | T3 Void
 {-# COMPLETE T1, T2 #-}
 }}}

     It would seem so. I'm happy for this to be accepted; I'm just stress-
 testing the spec.

 - The argument for not having the pattern-match checker look through
 pattern synonyms is reasonable. But is there a way to have GHC do some
 checking on `COMPLETE` declarations? It would be great -- especially if
 the `COMPLETE` pragma were in the synonyms' defining module -- to check
 these declarations. Of course, GHC will issue false negatives (that is,
 say that a set is not complete when it actually is) but some checking is
 better than none.

 - How does this interact with GADTs? For example, load this code into your
 head:

 {{{
 data G a where
   GInt  :: G Int
   GBool :: G Bool

 pattern PInt :: forall a. () => a ~ Int => G a
 pattern PInt = GInt

 f1 :: G a -> ()
 f1 GInt = ()

 f2 :: G Int -> ()
 f2 GInt = ()

 f3 :: G Int -> ()
 f3 PInt = ()
 }}}

    By default, `f1` and `f3` will get incomplete match warnings, and `f2`
 does not.

    a. If I say `{-# COMPLETE GInt, GBool #-}`, does this change the
 default warning behavior?

    b. How can I have GHC notice that `f3` is a complete match? Saying `{-#
 COMPLETE PInt #-}` would seem disastrous.

  - What if multiple conflicting `COMPLETE` pragmas are in scope? For
 example, I have `{-# COMPLETE A, B #-}` and `{-# COMPLETE A #-}` in scope.
 Is a match over `A` complete? Is a warning/error issued about the pragmas?

  - The spec says "We verify that the result types of each constructor in a
 complete match agrees with each other." What does this sentence mean?
 Consider the possibility of pattern synonyms that match against functions,
 polymorphic patterns, and possibly even higher-rank patterns.

 I've not looked at all at the implementation, wanting to nail down the
 spec before considering any implementation.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8779#comment:44>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler