From ae88ed9a73d52ab103df491ef2e43c483f1d548d Mon Sep 17 00:00:00 2001
From: sheaf <sam.derbyshire@gmail.com>
Date: Tue, 11 Jul 2023 14:00:53 +0200
Subject: [PATCH] Skip PMC for boring patterns
Some patterns introduce no new information to the pattern-match
checker (such as plain variable or wildcard patterns). We can thus
skip doing any pattern-match checking on them when the sole purpose
for doing so was introducing new long-distance information.
See Note [Boring patterns] in GHC.Hs.Pat.
Doing this avoids regressing in performance now that we do additional
pattern-match checking inside do notation.
(cherry picked from commit bea0e323c09e9e4b841a37aacd6b67e87a85e7cb)
---
compiler/GHC/Hs/Pat.hs | 103 +++++++++++++++++-
compiler/GHC/HsToCore/Match.hs | 7 +-
compiler/GHC/HsToCore/Pmc.hs | 2 +-
compiler/GHC/HsToCore/Pmc/Utils.hs | 25 ++++-
.../pmcheck/should_compile/LongDistanceDo.hs | 19 ++++
.../should_compile/LongDistanceGRHS.hs | 22 ++++
testsuite/tests/pmcheck/should_compile/all.T | 2 +
7 files changed, 169 insertions(+), 11 deletions(-)
create mode 100644 testsuite/tests/pmcheck/should_compile/LongDistanceDo.hs
create mode 100644 testsuite/tests/pmcheck/should_compile/LongDistanceGRHS.hs
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index a6a7fbd3e66..7aa9e593bc0 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -43,7 +43,7 @@ module GHC.Hs.Pat (
looksLazyPatBind,
isBangedLPat,
gParPat, patNeedsParens, parenthesizePat,
- isIrrefutableHsPat,
+ isIrrefutableHsPat, isBoringHsPat,
collectEvVarsPat, collectEvVarsPats,
@@ -609,6 +609,55 @@ isSimplePat p = case unLoc p of
VarPat _ x -> Just (unLoc x)
_ -> Nothing
+-- | Is this pattern boring from the perspective of pattern-match checking,
+-- i.e. introduces no new pieces of long-dinstance information
+-- which could influence pattern-match checking?
+--
+-- See Note [Boring patterns].
+isBoringHsPat :: forall p. OutputableBndrId p => LPat (GhcPass p) -> Bool
+-- NB: it's always safe to return 'False' in this function; that just means
+-- performing potentially-redundant pattern-match checking.
+isBoringHsPat = goL
+ where
+ goL :: forall p. OutputableBndrId p => LPat (GhcPass p) -> Bool
+ goL = go . unLoc
+
+ go :: forall p. OutputableBndrId p => Pat (GhcPass p) -> Bool
+ go = \case
+ WildPat {} -> True
+ VarPat {} -> True
+ LazyPat {} -> True
+ BangPat _ pat -> goL pat
+ ParPat _ _ pat _ -> goL pat
+ AsPat {} -> False -- the pattern x@y links x and y together,
+ -- which is a nontrivial piece of information
+ ViewPat _ _ pat -> goL pat
+ SigPat _ pat _ -> goL pat
+ TuplePat _ pats _ -> all goL pats
+ SumPat _ pat _ _ -> goL pat
+ ListPat _ pats -> all goL pats
+ ConPat { pat_con = con, pat_args = details }
+ -> case ghcPass @p of
+ GhcPs -> False -- conservative
+ GhcRn -> False -- conservative
+ GhcTc
+ | isVanillaConLike (unLoc con)
+ -> all goL (hsConPatArgs details)
+ | otherwise
+ -- A pattern match on a GADT constructor can introduce
+ -- type-level information (for example, T18572).
+ -> False
+ LitPat {} -> True
+ NPat {} -> True
+ NPlusKPat {} -> True
+ SplicePat {} -> False
+ XPat ext ->
+ case ghcPass @p of
+ GhcRn -> case ext of
+ HsPatExpanded _ pat -> go pat
+ GhcTc -> case ext of
+ CoPat _ pat _ -> go pat
+ ExpansionPat _ pat -> go pat
{- Note [Unboxed sum patterns aren't irrefutable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -630,6 +679,58 @@ minimum unboxed sum arity is 2.
Failing to mark unboxed sum patterns as non-irrefutable would cause the Just'
case in foo to be unreachable, as GHC would mistakenly believe that Nothing'
is the only thing that could possibly be matched!
+
+Note [Boring patterns]
+~~~~~~~~~~~~~~~~~~~~~~
+A pattern is called boring when no new information is gained upon successfully
+matching on the pattern.
+
+Some examples of boring patterns:
+
+ - x, for a variable x. We learn nothing about x upon matching this pattern.
+ - Just y. This pattern can fail, but if it matches, we don't learn anything
+ about y.
+
+Some examples of non-boring patterns:
+
+ - x@(Just y). A match on this pattern introduces the fact that x is headed
+ by the constructor Just, which means that a subsequent pattern match such as
+
+ case x of { Just z -> ... }
+
+ should not be marked as incomplete.
+ - a@b. Matching on this pattern introduces a relation between 'a' and 'b',
+ which means that we shouldn't emit any warnings in code of the form
+
+ case a of
+ True -> case b of { True -> .. } -- no warning here!
+ False -> ...
+ - GADT patterns. For example, with the GADT
+
+ data G i where { MkGInt :: G Int }
+
+ a match on the pattern 'MkGInt' introduces type-level information:
+
+ foo :: G i -> i
+ foo MkGInt = 3
+
+ Here we learn that i ~ Int after matching on 'MkGInt', so this pattern
+ is not boring.
+
+When a pattern is boring, and we are only interested in additional long-distance
+information (not whether the pattern itself is fallible), we can skip pattern-match
+checking entirely. Doing this saves about 10% allocations in test T11195.
+
+This happens when we are checking pattern-matches in do-notation, for example:
+
+ do { x@(Just y) <- z
+ ; ...
+ ; return $ case x of { Just w -> ... } }
+
+Here we *do not* want to emit a pattern-match warning on the first line for the
+incomplete pattern-match, as incompleteness inside do-notation is handled
+using MonadFail. However, we still want to propagate the fact that x is headed
+by the 'Just' constructor, to avoid a pattern-match warning on the last line.
-}
-- | @'patNeedsParens' p pat@ returns 'True' if the pattern @pat@ needs
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 49dc24ae074..54f9741f01b 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -953,10 +953,9 @@ matchSinglePatVar var mb_scrut ctx pat ty match_result
-- See Note [Long-distance information in matchWrapper] and
-- Note [Long-distance information in do notation] in GHC.HsToCore.Expr.
; ldi_nablas <-
- if isMatchContextPmChecked dflags FromSource ctx
- then
- addCoreScrutTmCs (maybeToList mb_scrut) [var] $
- pmcPatBind (DsMatchContext ctx locn) var (unLoc pat)
+ if isMatchContextPmChecked_SinglePat dflags FromSource ctx pat
+ then addCoreScrutTmCs (maybeToList mb_scrut) [var] $
+ pmcPatBind (DsMatchContext ctx locn) var (unLoc pat)
else getLdiNablas
; let eqn_info = EqnInfo { eqn_pats = [unLoc (decideBangHood dflags pat)]
diff --git a/compiler/GHC/HsToCore/Pmc.hs b/compiler/GHC/HsToCore/Pmc.hs
index f588c842c8b..9fde238fe97 100644
--- a/compiler/GHC/HsToCore/Pmc.hs
+++ b/compiler/GHC/HsToCore/Pmc.hs
@@ -36,7 +36,7 @@
module GHC.HsToCore.Pmc (
-- Checking and printing
pmcPatBind, pmcMatches, pmcGRHSs,
- isMatchContextPmChecked,
+ isMatchContextPmChecked, isMatchContextPmChecked_SinglePat,
-- See Note [Long-distance information]
addTyCs, addCoreScrutTmCs, addHsScrutTmCs, getLdiNablas
diff --git a/compiler/GHC/HsToCore/Pmc/Utils.hs b/compiler/GHC/HsToCore/Pmc/Utils.hs
index b39862821a5..b208723e7b4 100644
--- a/compiler/GHC/HsToCore/Pmc/Utils.hs
+++ b/compiler/GHC/HsToCore/Pmc/Utils.hs
@@ -8,7 +8,8 @@ module GHC.HsToCore.Pmc.Utils (
tracePm, traceWhenFailPm, mkPmId,
allPmCheckWarnings, overlapping, exhaustive, redundantBang,
exhaustiveWarningFlag,
- isMatchContextPmChecked, needToRunPmCheck
+ isMatchContextPmChecked, isMatchContextPmChecked_SinglePat,
+ needToRunPmCheck
) where
@@ -25,7 +26,6 @@ import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Unique.Supply
import GHC.Types.SrcLoc
-import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Logger
import GHC.HsToCore.Monad
@@ -108,16 +108,31 @@ arrowMatchContextExhaustiveWarningFlag = \ case
-- 'HsMatchContext' (does not matter whether it is the redundancy check or the
-- exhaustiveness check).
isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
-isMatchContextPmChecked dflags origin kind
+isMatchContextPmChecked dflags origin ctxt
= requiresPMC origin
- && (overlapping dflags kind || exhaustive dflags kind)
+ && (overlapping dflags ctxt || exhaustive dflags ctxt)
+
+-- | Check whether exhaustivity checks are enabled for this 'HsMatchContext',
+-- when dealing with a single pattern (using the 'matchSinglePatVar' function).
+isMatchContextPmChecked_SinglePat :: DynFlags -> Origin -> HsMatchContext id -> LPat GhcTc -> Bool
+isMatchContextPmChecked_SinglePat dflags origin ctxt pat
+ | not (needToRunPmCheck dflags origin)
+ = False
+ | StmtCtxt {} <- ctxt
+ -- For @StmtCtxt@, we are interested in propagating pattern-match information
+ -- but not in the actual outcome of pattern-match checking, so we skip
+ -- if the pattern is "boring" (gives rise to no long-distance information).
+ -- (This is done purely for runtime performance.)
+ = not (isBoringHsPat pat) -- See Note [Boring patterns] in GHC.Hs.Pat.
+ | otherwise
+ = overlapping dflags ctxt || exhaustive dflags ctxt
-- | Return True when any of the pattern match warnings ('allPmCheckWarnings')
-- are enabled, in which case we need to run the pattern match checker.
needToRunPmCheck :: DynFlags -> Origin -> Bool
needToRunPmCheck dflags origin
= requiresPMC origin
- && notNull (filter (`wopt` dflags) allPmCheckWarnings)
+ && any (`wopt` dflags) allPmCheckWarnings
{- Note [Inaccessible warnings for record updates]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/pmcheck/should_compile/LongDistanceDo.hs b/testsuite/tests/pmcheck/should_compile/LongDistanceDo.hs
new file mode 100644
index 00000000000..8bbbd2c9dc2
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/LongDistanceDo.hs
@@ -0,0 +1,19 @@
+module LongDistanceDo where
+
+data D = T1 | T2
+
+foo1 :: IO D -> IO ()
+foo1 d = do
+ x@y <- d
+ let z = case x of
+ T1 -> ()
+ T2 -> case y of { T2 -> () }
+ return z
+
+foo2 :: IO D -> IO ()
+foo2 d = do
+ x@y <- d
+ let z = case y of
+ T1 -> ()
+ T2 -> case x of { T2 -> () }
+ return z
diff --git a/testsuite/tests/pmcheck/should_compile/LongDistanceGRHS.hs b/testsuite/tests/pmcheck/should_compile/LongDistanceGRHS.hs
new file mode 100644
index 00000000000..7bf7d5e13a7
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/LongDistanceGRHS.hs
@@ -0,0 +1,22 @@
+module LongDistanceGRHS where
+
+data D = T1 | T2
+
+foo1 y
+ | x <- y
+ = case x of
+ T1 -> case y of { T1 -> False }
+ T2 -> True
+
+foo2 y
+ | x <- y
+ = case y of
+ T1 -> case x of { T1 -> False }
+ T2 -> True
+
+foo3 y
+ | x@T1 <- y
+ = case y of
+ T1 -> False
+ | otherwise
+ = True
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 141aa0433b3..0030a9f2d74 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -113,6 +113,8 @@ test('CyclicSubst', [], compile, [overlapping_incomplete])
test('CaseOfKnownCon', [], compile, [overlapping_incomplete])
test('TooManyDeltas', [], compile, [overlapping_incomplete+'-fmax-pmcheck-models=0'])
test('LongDistanceInfo', [], compile, [overlapping_incomplete])
+test('LongDistanceDo', [], compile, [overlapping_incomplete])
+test('LongDistanceGRHS', [], compile, [overlapping_incomplete])
test('T21662', [], compile, [overlapping_incomplete])
test('T19271', [], compile, [overlapping_incomplete])
test('T21761', [], compile, [overlapping_incomplete])
--
GitLab