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

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