Exhaustiveness checking for pattern synonyms

[Simon Peyton Jones]

Thanks.

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

The wiki spec doesn't say this (presumably under "semantics").  Could it?

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

Can you say this in the spec?

|  >
|  > * Point out in the spec that COMPLETE pragmas are entirely unchecked.
|  >   It's up to the programmer to get it right.

Can you say this in the spec?  Ah -- it's in "Discussion"... put it under "Semantics".

|  >
|  > * 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 [].

Can you say this in the spec?

|  
|  > * 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 pattern match checker checks each set of patterns individually"

Given a program, what are the "sets of patterns", precisely?

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

Some examples would be a big help.

Simon

|  
|  
|  
|  > Simon
|  >
|  > |  -----Original Message-----
|  > |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
|  > | Matthew  Pickering
|  > |  Sent: 22 November 2016 10:43
|  > |  To: GHC developers <ghc-devs at haskell.org>
|  > |  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 at 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%7C155eb2786cb040d8052908
|  > | d412c453
|  > | b5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636154081815249356&s
|  > | data=MkQ
|  > |  FpwJWaTU%2BdEQSYEBjXLt80BrXLkBp9V8twdKB6BI%3D&reserved=0
|  
|  I updated the wiki page quite a bit. Thanks Simon for the comments.
|  
|  Matt