Exhaustiveness checking for pattern synonyms

[Matthew Pickering]

On Tue, Jan 10, 2017 at 4:05 PM, Simon Peyton Jones
<simonpj at microsoft.com> 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 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%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