[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 mpickering):

 Replying to [comment:44 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.

 I agree with this.

 > - 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.

 Yes.

 > - 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.

 There are two problems with this I think.

 1. If we allow `COMPLETE` pragmas in modules other than the definition
 module then we would have to include the RHS of a pattern synonym in the
 interface file.
 2. In most instances, the checker will fail and produce a warning, and
 then what? The warning wouldn't be actionable in some way without another
 syntactic clue to tell the compiler to *really* trust us. It seems like a
 lot of effort.

 > - 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?

 With my latest changes, all else being equal we choose the error from the
 builtin set rather than any user specified set so the warnings will remain
 the same.

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

 The correct thing to specify would be `{-# COMPLETE GBool, PInt #-}` and
 in that case, my implementation does not warn about `f3`.

 >  - 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?
 >

 This is a fair point. It would seem that the `A,B` pragma is redundant
 because `A` is a subset of  `A, B` but it is possible for overlapping
 pragmas to make sense. For example, we could have two pattern synonyms for
 `Just`, `PJ1`, `PJ2` and then specify
 `{-# COMPLETE Nothing, PJ1 #-}` and `{-# COMPLETE Nothing, PJ2 #-}`.



 >  - 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.
 >

 It means that we look at the result type of each conlike and then verify
 that the type constructor for each type is the same. In the case of a set
 containing polymorphic patterns, at least one pattern in the set must have
 a definite type or you must specify a type signature to fix the type for
 the whole set.

 > 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:46>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler