Opened 2 years ago

Last modified 32 hours ago

#13965 new bug

COMPLETE sets nerf redundant pattern-match warnings

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


If I give redundant patterns for a datatype with a COMPLETE set, then GHC doesn't warn me at all. Here's an 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)
    TooGoodToBeTrue = T
{-# COMPLETE F, TooGoodToBeTrue #-}

catchAll :: Boolean -> Int
catchAll F               = 0
catchAll TooGoodToBeTrue = 1
catchAll F               = 2

GHC thinks this is fine and dandy:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -Wall
GHCi, version  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, 1 module loaded.

This problem also persists across modules:

module Foo where

import Bug

catchAll2 :: Boolean -> Int
catchAll2 F               = 0
catchAll2 TooGoodToBeTrue = 1
catchAll2 F               = 2
$ /opt/ghc/8.2.1/bin/ghci Foo.hs -Wall
GHCi, version  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling Bug              ( Bug.hs, interpreted )
[2 of 2] Compiling Foo              ( Foo.hs, interpreted )

Change History (7)

comment:1 Changed 12 months ago by ckoparkar

Cc: mpickering added

It looks like this was by design when the COMPLETE pragma was added in Phab:D2669.

@@ -1360,8 +1455,8 @@ wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
   = when (flag_i || flag_u) $ do
-      let exists_r = flag_i && notNull redundant
-          exists_i = flag_i && notNull inaccessible
+      let exists_r = flag_i && notNull redundant && onlyBuiltin
+          exists_i = flag_i && notNull inaccessible && onlyBuiltin
           exists_u = flag_u && notNull uncovered
       when exists_r $ forM_ redundant $ \(L l q) -> do
         putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
@@ -1373,7 +1468,8 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result

Relevant comment: compiler/deSugar/Check.hs

data PartialResult = PartialResult {
                        presultProvenance :: Provenance
                         -- keep track of provenance because we don't want
                         -- to warn about redundant matches if the result
                         -- is contaminated with a COMPLETE pragma

Do we want to change this?

comment:2 Changed 12 months ago by ckoparkar

Cc: ckoparkar added

comment:3 Changed 12 months ago by mpickering

It's this way because removing a "redudant" match arising from a COMPLETE pragma can change what a function does.

comment:4 in reply to:  3 Changed 12 months ago by RyanGlScott

Replying to mpickering:

It's this way because removing a "redudant" match arising from a COMPLETE pragma can change what a function does.

Really? What is an example of this?

comment:5 Changed 12 months ago by mpickering

data  T = A | B

{-# COMPLETE A #-}

foo A = 5
foo B = 6

comment:6 Changed 12 months ago by RyanGlScott

I think this comparison is somewhat unfair. For one thing, this isn't even a situation where the COMPLETE set would kick in, since GHC would pick the original set of constructors over the COMPLETE set. Removing the "redundant" match on B wouldn't introduce any warnings either, but that is correct behavior, since now GHC uses the COMPLETE set.

The original program is of a different nature, since the only option it has is a COMPLETE set (as evidenced by module Foo). Moreover, removing the redundant match on F doesn't change the fact that GHC is using the same COMPLETE set. This is why I argue that GHC's warning behavior on the original program is mistaken, since the second match on F is truly redundant, even after factoring in the semantics of COMPLETE sets.

comment:7 Changed 32 hours ago by Marge Bot <ben+marge-bot@…>

In 7915afc/ghc:

Encode shape information in `PmOracle`

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.

This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).

Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149

Metric Decrease:
Note: See TracTickets for help on using tickets.