[GHC] #13964: Pattern-match warnings for datatypes with COMPLETE sets break abstraction
#13964: Pattern-match warnings for datatypes with COMPLETE sets break abstraction -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms, | PatternMatchWarnings | Architecture: | Type of failure: Poor/confusing Unknown/Multiple | error message Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Here's a file: {{{#!hs {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where data Boolean = F | T deriving Eq pattern TooGoodToBeTrue :: Boolean pattern TooGoodToBeTrue <- ((== T) -> True) where TooGoodToBeTrue = T {-# COMPLETE F, TooGoodToBeTrue #-} catchAll :: Boolean -> Int catchAll F = 0 -- catchAll TooGoodToBeTrue = 1 }}} If you compile this with `-Wall`, the warning will warn about `T`, not `TooGoodToBeTrue` (the other conlike in the `COMPLETE` set): {{{ $ /opt/ghc/8.2.1/bin/ghc -fforce-recomp -Wall Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘catchAll’: Patterns not matched: T | 15 | catchAll F = 0 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} Perhaps this isn't so bad, since it's intra-module. But the problem persists even across modules: {{{#!hs module Foo where import Bug catchAll2 :: Boolean -> Int catchAll2 F = 0 -- catchAll2 TooGoodToBeTrue = 1 }}} {{{ $ /opt/ghc/8.2.1/bin/ghc -fforce-recomp -c Bug.hs $ /opt/ghc/8.2.1/bin/ghc -fforce-recomp -c -Wall Foo.hs Foo.hs:6:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘catchAll2’: Patterns not matched: Bug.T | 6 | catchAll2 F = 0 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} This one is really bad, since it's warning about `Bug.T`, which should be hidden! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13964 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13964: Pattern-match warnings for datatypes with COMPLETE sets break abstraction -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * version: 8.0.1 => 8.2.1-rc2 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13964#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13964: Pattern-match warnings for datatypes with COMPLETE sets break abstraction -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): This is nothing unique to `COMPLETE` pragmas, the exhaustiveness checker already breaks abstraction in this way. For example: {{{ module T (D(A)) where data D = A | B }}} {{{ module M where import T foo A = () }}} warns with {{{ M.hs:5:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: T.B | 5 | foo A = () | }}} and after all, to retain safety it has to. A function exported by `T` could mention `B` and then be used in `M`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13964#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13964: Pattern-match warnings for datatypes with COMPLETE sets break abstraction -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Perhaps I'm fundamentally misunderstanding something about `COMPLETE` sets, but this doesn't feel like a very satisfying explanation. My intuition is that specifying a `COMPLETE` set for a data type is tantamount to overriding the pattern match exhaustiveness checker's behavior w.r.t. to that particular data type, and as such, I would any warnings that are emitted under the `-Wincomplete-patterns` label to be adjusted according to whatever `COMPLETE` sets are in scope. For example, in my original example, I would simply expect that in this warning: {{{ Foo.hs:6:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘catchAll2’: Patterns not matched: Bug.T }}} It would warn about `TooGoodToBeTrue`, not `Bug.T`. That's all. Replying to [comment:2 mpickering]:
This is nothing unique to `COMPLETE` pragmas, the exhaustiveness checker already breaks abstraction in this way.
For example:
{{{ module T (D(A)) where
data D = A | B }}}
{{{ module M where
import T
foo A = () }}}
warns with
{{{ M.hs:5:1: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In an equation for ‘foo’: Patterns not matched: T.B | 5 | foo A = () | }}}
That seems fine to me, since the user didn't specify `{-# COMPLETE A #-}` for the data type `D`. If she did, I wouldn't expect a warning for `foo`.
and after all, to retain safety it has to. A function exported by `T` could mention `B` and then be used in `M`.
I don't understand what you mean. A function exported from `T` surely doesn't have any effect on whether a function defined in `M` is exhaustive, right? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13964#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
When the pattern match checker requests a set of constructors for a type constructor `T`, we now return a list of sets which include the normal data constructor set and also any `COMPLETE` pragmas of type `T`. We then
#13964: Pattern-match warnings for datatypes with COMPLETE sets break abstraction -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: | PatternSynonyms, | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Poor/confusing | Unknown/Multiple error message | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another way of phrasing the problem is that the observed behavior here doesn't match the specification laid out in [https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms/CompleteSigs#ErrorMess... the GHC wiki] (and which I'm attempting to enshrine in the GHC users' guide in Phab:D4005). Quoth the wiki: try each of these sets, not warning if any of them are a perfect match. In the case the match isn't perfect, we select one of the branches of the search depending on how good the result is.
The results are prioritised in this order.
1. Fewest uncovered clauses 2. Fewest redundant clauses 3. Fewest inaccessible clauses 4. Whether the match comes from a `COMPLETE` pragma or the built-in set
of data constructors for a type constructor. Going to back to the original example: {{{#!hs {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where data Boolean = F | T deriving Eq pattern TooGoodToBeTrue :: Boolean pattern TooGoodToBeTrue <- ((== T) -> True) where TooGoodToBeTrue = T {-# COMPLETE F, TooGoodToBeTrue #-} }}} {{{#!hs module Foo where import Bug catchAll2 :: Boolean -> Int catchAll2 F = 0 -- catchAll2 TooGoodToBeTrue = 1 }}} Here, we have two sets of conlikes to consider: the original set of data constructors `{F, T}`, as well as the `COMPLETE` set `{F, TooGoodToBeTrue}`. Both sets have exactly one uncovered clause and no redundant or inaccessible clauses, so to break the tie, it must use the fourth rule, which states that the `COMPLETE` pragma should be favored over the built-in set of data constructors. But this isn't happening here, since the original data constructor `T` is being warned about. So we could "fix" this example by just tightening the implementation to actually match the specification. Granted, one could tweak this example slightly to the point where the original data constructor set is once again favored over the `COMPLETE` set (while still following the specification), once again breaking abstraction. In such a scenario, we should consider revising the specification to factor in whether all of the conlikes in a particular set are in-scope. That should supplant "Fewest uncovered clauses" as the new top priority, I believe. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13964#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC