Opened 2 months ago

Last modified 3 days ago

#13964 new bug

Pattern-match warnings for datatypes with COMPLETE sets break abstraction

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1-rc2
Keywords: PatternSynonyms, PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Here's a file:

{-# 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:

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!

Change History (4)

comment:1 Changed 2 months ago by RyanGlScott

Version: 8.0.18.2.1-rc2

comment:2 Changed 2 months ago 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.

comment:3 in reply to:  2 Changed 2 months ago 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 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?

comment:4 Changed 3 days ago by RyanGlScott

Another way of phrasing the problem is that the observed behavior here doesn't match the specification laid out in the GHC wiki (and which I'm attempting to enshrine in the GHC users' guide in Phab:D4005). Quoth the wiki:

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 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:

{-# 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 #-}
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.

Note: See TracTickets for help on using tickets.