Exhaustiveness checking for pattern synonyms

[Benno Fünfstück]

An idea: could we perhaps use the same syntax as for MINIMAL pragmas also
for COMPLETE pragmas, since those two feel very similar to me? So instead
of multiple pragmas, let's have {-# COMPLETE (Pat1, Pat2) | (Pat3, Pat4)
#}, just like with {-# MINIMAL #-} ?

Regards,
Benno

Simon Peyton Jones via ghc-devs <ghc-devs at haskell.org> schrieb am Fr., 13.
Jan. 2017 um 16:50 Uhr:

> 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170114/55a12382/attachment.html>