Re: Exhaustiveness checking for pattern synonyms

13 Jan 2017

      On Tue, Jan 10, 2017 at 4:05 PM, Simon Peyton Jones
 wrote:
...
Questions
* What if there are multiple COMPLETE pragmas e.g.
  {-# COMPLETE A, B, C #-}
  {-# COMPLETE A, X, Y, Z #-}
  Is that ok?  I guess it should be!
Will the pattern-match exhaustiveness check then succeed
  if a function uses either set?
What happens if you use a mixture of constructors in a match
  (e.g. A, X, C, Z)?  Presumably all bets are off?
Yes this is fine. In the case you ask about then as neither COMPLETE
pragma will match then the "best" one as described in the error
messages section will be chosen.
...
* Note that COMPLETE pragmas could be a new source of orphan modules
     module M where
       import N( pattern P, pattern Q )
       {-# COMPLETE P, Q #-}
  where neither P nor Q is defined in M.  Then every module that is
  transitively "above" M would need to read M.hi just in case its
  COMPLETE pragmas was relevant.
* Point out in the spec that COMPLETE pragmas are entirely unchecked.
  It's up to the programmer to get it right.
* Typing.  What does it mean for the types to "agree" with each other.
  E.g  A :: a -> [(a, Int)]
       B :: b -> [(Int, b)]
  Is this ok?  Please say explicitly with examples.
This would be ok as the type constructor of both result types is [].
There are now examples I see which could never be used together but
are currently accepted e.g.

    P :: Int -> [Int]
    Q :: Int -> [Char]

could be specified together in a COMPLETE pragma but then the actual
type checker will reject any usages of `P` and `Q` together for
obvious reasons.

I am not too worried about this as I don't want to reimplement the
type checker for pattern matches poorly -- a simple sanity check is
the reason why there is any type checking at all for these pragmas.
...
* I didn't really didn't understand the "Error messages" section.
I can't really help unless I know what you don't understand.
The idea is simply that all the different sets of patterns are tried
and that the results are prioritised by

1. Fewest uncovered clauses
2. Fewest redundant clauses
3. Fewest inaccessible clauses
4. Whether the match comes from a COMPLETE pragma or the build in set
of data constructors for a type constructor.
...
Simon
|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Matthew
|  Pickering
|  Sent: 22 November 2016 10:43
|  To: GHC developers 
|  Subject: Exhaustiveness checking for pattern synonyms
|
|  Hello devs,
|
|  I have implemented exhaustiveness checking for pattern synonyms. The idea is
|  very simple, you specify a set of pattern synonyms (or data
|  constructors) which are regarded as a complete match.
|  The pattern match checker then uses this information in order to check
|  whether a function covers all possibilities.
|
|  Specification:
|
|  https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs
|
|  https://phabricator.haskell.org/D2669
|  https://phabricator.haskell.org/D2725
|
|  https://ghc.haskell.org/trac/ghc/ticket/8779
|
|  Matt
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs@haskell.org
|  https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell
|  .org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
|  devs&data=02%7C01%7Csimonpj%40microsoft.com%7C155eb2786cb040d8052908d412c453
|  b5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636154081815249356&sdata=MkQ
|  FpwJWaTU%2BdEQSYEBjXLt80BrXLkBp9V8twdKB6BI%3D&reserved=0
I updated the wiki page quite a bit. Thanks Simon for the comments.

Matt

Re: Exhaustiveness checking for pattern synonyms

Matthew Pickering