Re: Exhaustiveness checking for pattern synonyms

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 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@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 %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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs