[Git][ghc/ghc][wip/T18638] 4 commits: Add long-distance info for pattern bindings (#18572)
Simon Peyton Jones
gitlab at gitlab.haskell.org
Thu Sep 10 15:51:07 UTC 2020
Simon Peyton Jones pushed to branch wip/T18638 at Glasgow Haskell Compiler / GHC
Commits:
67ce72da by Sebastian Graf at 2020-09-10T10:35:33-04:00
Add long-distance info for pattern bindings (#18572)
We didn't consider the RHS of a pattern-binding before, which led to
surprising warnings listed in #18572.
As can be seen from the regression test T18572, we get the expected
output now.
- - - - -
1207576a by Sebastian Graf at 2020-09-10T10:35:33-04:00
PmCheck: Big refactor using guard tree variants more closely following source syntax (#18565)
Previously, we desugared and coverage checked plain guard trees as
described in Lower Your Guards. That caused (in !3849) quite a bit of
pain when we need to partially recover tree structure of the input
syntax to return covered sets for long-distance information, for
example.
In this refactor, I introduced a guard tree variant for each relevant
source syntax component of a pattern-match (mainly match groups, match,
GRHS, empty case, pattern binding). I made sure to share as much
coverage checking code as possible, so that the syntax-specific checking
functions are just wrappers around the more substantial checking
functions for the LYG primitives (`checkSequence`, `checkGrds`).
The refactoring payed off in clearer code and elimination of all panics
related to assumed guard tree structure and thus fixes #18565.
I also took the liberty to rename and re-arrange the order of functions
and comments in the module, deleted some dead and irrelevant Notes,
wrote some new ones and gave an overview module haddock.
- - - - -
95455982 by GHC GitLab CI at 2020-09-10T10:36:09-04:00
hadrian: Don't include -fdiagnostics-color in argument hash
Otherwise the input hash will vary with whether colors are requested,
which changed with `isatty`.
Fixes #18672.
- - - - -
04f0cae6 by Simon Peyton Jones at 2020-09-10T16:50:38+01:00
Do absence analysis on stable unfoldings
Ticket #18638 showed that Very Bad Things happen if we fail
to do absence analysis on stable unfoldings. It's all described
in Note [Absence analysis for stable unfoldings].
I'm a bit surprised this hasn't bitten us before. Fortunately
the fix is pretty simple.
- - - - -
25 changed files:
- compiler/GHC/Core/Opt/DmdAnal.hs
- compiler/GHC/Data/OrdList.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/GuardedRHSs.hs
- compiler/GHC/HsToCore/ListComp.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/HsToCore/Match.hs-boot
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Utils/Misc.hs
- hadrian/src/Settings/Builders/Ghc.hs
- hadrian/src/Target.hs
- testsuite/tests/deSugar/should_compile/ds020.stderr
- testsuite/tests/module/all.T
- + testsuite/tests/pmcheck/should_compile/T18572.hs
- + testsuite/tests/pmcheck/should_compile/T18572.stderr
- testsuite/tests/pmcheck/should_compile/all.T
- testsuite/tests/rename/should_compile/T7085.stderr
- + testsuite/tests/simplCore/should_run/T18638.hs
- + testsuite/tests/simplCore/should_run/T18638.stdout
- testsuite/tests/simplCore/should_run/all.T
- testsuite/tests/unboxedsums/all.T
Changes:
=====================================
compiler/GHC/Core/Opt/DmdAnal.hs
=====================================
@@ -552,7 +552,18 @@ dmdAnalRhsLetDown rec_flag env let_dmd id rhs
-- See Note [Demand signatures are computed for a threshold demand based on idArity]
= mkRhsDmd env rhs_arity rhs
- (DmdType rhs_fv rhs_dmds rhs_div, rhs') = dmdAnal env rhs_dmd rhs
+ (rhs_dmd_ty, rhs') = dmdAnal env rhs_dmd rhs
+
+ -- See Note [Absence analysis for stable unfoldings]
+ unf = realIdUnfolding id
+ full_dmd_ty | isStableUnfolding unf
+ , Just unf_body <- maybeUnfoldingTemplate unf
+ , (unf_dmd_ty, _unf_body') <- dmdAnal env rhs_dmd unf_body
+ = rhs_dmd_ty `bothDmdType` toBothDmdArg unf_dmd_ty
+ | otherwise
+ = rhs_dmd_ty
+
+ DmdType rhs_fv rhs_dmds rhs_div = full_dmd_ty
sig = mkStrictSigForArity rhs_arity (DmdType sig_fv rhs_dmds rhs_div)
-- See Note [Aggregated demand for cardinality]
@@ -799,6 +810,41 @@ Fortunately, GHC.Core.Opt.Arity gives 'foo' arity 2, which is enough for LetDown
forward plusInt's demand signature, and all is well (see Note [Newtype arity] in
GHC.Core.Opt.Arity)! A small example is the test case NewtypeArity.
+Note [Absence analysis for stable unfoldings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Ticket #18638 shows that it's really important to do absence analysis
+for stable unfoldings. Consider
+
+ g = blah
+
+ f = \x. ...no use of g....
+ {- f's stable unfolding is f = \x. ...g... -}
+
+If f is ever inlined we use 'g'. But f's current RHS makes no use
+of 'g', so if we don't look at the unfolding we'll mark g as Absent,
+and transform to
+
+ g = error "Entered absent value"
+ f = \x. ...
+ {- f's stable unfolding is f = \x. ...g... -}
+
+Now if f is subsequently inlined, we'll use 'g' and ... disaster.
+
+SOLUTION: if f has a stable unfolding, do demand analysis on its
+body. (We dicard the resulting term, using only the DmdType,
+specifically the DmdEnv which captures uses of the free variables.
+
+PS: You may wonder how it can be that f's optimised RHS has somehow
+discarded 'g', but when f is inlined we /don't/ discard g in the same
+way. I think a simple example is
+ g = (a,b)
+ f = \x. fst g
+ {-# INLNE f #-}
+
+Now f's optimised RHS will be \x.a, but if we change g to (error "..")
+(since it is apparently Absent) and then inline (\x. fst g) we get
+disaster. But regardless, #18638 was a more complicated version of
+this, that actually happened in practice.
Historical Note [Product demands for function body]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Data/OrdList.hs
=====================================
@@ -5,13 +5,16 @@
-}
{-# LANGUAGE DeriveFunctor #-}
-
{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE UnboxedTuples #-}
-- | Provide trees (of instructions), so that lists of instructions can be
-- appended in linear time.
module GHC.Data.OrdList (
- OrdList,
+ OrdList, pattern NilOL, pattern ConsOL, pattern SnocOL,
nilOL, isNilOL, unitOL, appOL, consOL, snocOL, concatOL, lastOL,
headOL,
mapOL, fromOL, toOL, foldrOL, foldlOL, reverseOL, fromOLReverse,
@@ -79,6 +82,50 @@ snocOL as b = Snoc as b
consOL a bs = Cons a bs
concatOL aas = foldr appOL None aas
+pattern NilOL :: OrdList a
+pattern NilOL <- (isNilOL -> True) where
+ NilOL = None
+
+-- | An unboxed 'Maybe' type with two unboxed fields in the 'Just' case.
+-- Useful for defining 'viewCons' and 'viewSnoc' without overhead.
+type VMaybe a b = (# (# a, b #) | (# #) #)
+pattern VJust :: a -> b -> VMaybe a b
+pattern VJust a b = (# (# a, b #) | #)
+pattern VNothing :: VMaybe a b
+pattern VNothing = (# | (# #) #)
+{-# COMPLETE VJust, VNothing #-}
+
+pattern ConsOL :: a -> OrdList a -> OrdList a
+pattern ConsOL x xs <- (viewCons -> VJust x xs) where
+ ConsOL x xs = consOL x xs
+{-# COMPLETE NilOL, ConsOL #-}
+viewCons :: OrdList a -> VMaybe a (OrdList a)
+viewCons (One a) = VJust a NilOL
+viewCons (Cons a as) = VJust a as
+viewCons (Snoc as a) = case viewCons as of
+ VJust a' as' -> VJust a' (Snoc as' a)
+ VNothing -> VJust a NilOL
+viewCons (Two as1 as2) = case viewCons as1 of
+ VJust a' as1' -> VJust a' (Two as1' as2)
+ VNothing -> viewCons as2
+viewCons _ = VNothing
+
+pattern SnocOL :: OrdList a -> a -> OrdList a
+pattern SnocOL xs x <- (viewSnoc -> VJust xs x) where
+ SnocOL xs x = snocOL xs x
+{-# COMPLETE NilOL, SnocOL #-}
+viewSnoc :: OrdList a -> VMaybe (OrdList a) a
+viewSnoc (One a) = VJust NilOL a
+viewSnoc (Many (reverse -> a:as)) = VJust (Many (reverse as)) a
+viewSnoc (Snoc as a) = VJust as a
+viewSnoc (Cons a as) = case viewSnoc as of
+ VJust as' a' -> VJust (Cons a as') a'
+ VNothing -> VJust NilOL a
+viewSnoc (Two as1 as2) = case viewSnoc as2 of
+ VJust as2' a' -> VJust (Two as1 as2') a'
+ VNothing -> viewSnoc as1
+viewSnoc _ = VNothing
+
headOL None = panic "headOL"
headOL (One a) = a
headOL (Many as) = head as
@@ -189,5 +236,3 @@ strictlyOrdOL (Two a1 a2) (Two b1 b2) =
strictlyOrdOL (Two _ _) _ = LT
strictlyOrdOL (Many as) (Many bs) = compare as bs
strictlyOrdOL (Many _ ) _ = GT
-
-
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -33,7 +33,7 @@ import {-# SOURCE #-} GHC.HsToCore.Match ( matchWrapper )
import GHC.HsToCore.Monad
import GHC.HsToCore.GuardedRHSs
import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck ( addTyCsDs, checkGRHSs )
+import GHC.HsToCore.PmCheck ( addTyCs, covCheckGRHSs )
import GHC.Hs -- lots of things
import GHC.Core -- lots of things
@@ -152,14 +152,14 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
, fun_matches = matches
, fun_ext = co_fn
, fun_tick = tick })
- = do { (args, body) <- addTyCsDs FromSource (hsWrapDictBinders co_fn) $
+ = do { (args, body) <- addTyCs FromSource (hsWrapDictBinders co_fn) $
-- FromSource might not be accurate (we don't have any
-- origin annotations for things in this module), but at
-- worst we do superfluous calls to the pattern match
-- oracle.
- -- addTyCsDs: Add type evidence to the refinement type
+ -- addTyCs: Add type evidence to the refinement type
-- predicate of the coverage checker
- -- See Note [Type and Term Equality Propagation] in "GHC.HsToCore.PmCheck"
+ -- See Note [Long-distance information] in "GHC.HsToCore.PmCheck"
matchWrapper
(mkPrefixFunRhs (L loc (idName fun)))
Nothing matches
@@ -185,7 +185,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss
, pat_ext = ty
, pat_ticks = (rhs_tick, var_ticks) })
- = do { rhss_deltas <- checkGRHSs PatBindGuards grhss
+ = do { rhss_deltas <- covCheckGRHSs PatBindGuards grhss
; body_expr <- dsGuarded grhss ty rhss_deltas
; let body' = mkOptTickBox rhs_tick body_expr
pat' = decideBangHood dflags pat
@@ -201,11 +201,11 @@ dsHsBind dflags (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
, abs_exports = exports
, abs_ev_binds = ev_binds
, abs_binds = binds, abs_sig = has_sig })
- = do { ds_binds <- addTyCsDs FromSource (listToBag dicts) $
+ = do { ds_binds <- addTyCs FromSource (listToBag dicts) $
dsLHsBinds binds
- -- addTyCsDs: push type constraints deeper
+ -- addTyCs: push type constraints deeper
-- for inner pattern match check
- -- See Check, Note [Type and Term Equality Propagation]
+ -- See Check, Note [Long-distance information]
; ds_ev_binds <- dsTcEvBinds_s ev_binds
=====================================
compiler/GHC/HsToCore/Expr.hs
=====================================
@@ -31,7 +31,7 @@ import GHC.HsToCore.ListComp
import GHC.HsToCore.Utils
import GHC.HsToCore.Arrows
import GHC.HsToCore.Monad
-import GHC.HsToCore.PmCheck ( addTyCsDs, checkGRHSs )
+import GHC.HsToCore.PmCheck ( addTyCs, covCheckGRHSs )
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Core.FamInstEnv( topNormaliseType )
@@ -215,7 +215,7 @@ dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss
, pat_ext = ty }) body
= -- let C x# y# = rhs in body
-- ==> case rhs of C x# y# -> body
- do { match_deltas <- checkGRHSs PatBindGuards grhss
+ do { match_deltas <- covCheckGRHSs PatBindGuards grhss
; rhs <- dsGuarded grhss ty match_deltas
; let upat = unLoc pat
eqn = EqnInfo { eqn_pats = [upat],
@@ -283,7 +283,7 @@ dsExpr hswrap@(XExpr (WrapExpr (HsWrap co_fn e)))
HsConLikeOut _ (RealDataCon dc) -> return $ varToCoreExpr (dataConWrapId dc)
XExpr (WrapExpr (HsWrap _ _)) -> pprPanic "dsExpr: HsWrap inside HsWrap" (ppr hswrap)
HsPar _ _ -> pprPanic "dsExpr: HsPar inside HsWrap" (ppr hswrap)
- _ -> addTyCsDs FromSource (hsWrapDictBinders co_fn) $
+ _ -> addTyCs FromSource (hsWrapDictBinders co_fn) $
dsExpr e
-- See Note [Detecting forced eta expansion]
; wrap' <- dsHsWrapper co_fn
@@ -486,7 +486,7 @@ dsExpr (HsMultiIf res_ty alts)
| otherwise
= do { let grhss = GRHSs noExtField alts (noLoc emptyLocalBinds)
- ; rhss_deltas <- checkGRHSs IfAlt grhss
+ ; rhss_deltas <- covCheckGRHSs IfAlt grhss
; match_result <- dsGRHSs IfAlt grhss res_ty rhss_deltas
; error_expr <- mkErrorExpr
; extractMatchResult match_result error_expr }
@@ -981,7 +981,7 @@ dsDo ctx stmts
= do { body <- goL stmts
; rhs' <- dsLExpr rhs
; var <- selectSimpleMatchVarL (xbstc_boundResultMult xbs) pat
- ; match <- matchSinglePatVar var (StmtCtxt ctx) pat
+ ; match <- matchSinglePatVar var Nothing (StmtCtxt ctx) pat
(xbstc_boundResultType xbs) (cantFailMatchResult body)
; match_code <- dsHandleMonadicFailure ctx pat match (xbstc_failOp xbs)
; dsSyntaxExpr (xbstc_bindOp xbs) [rhs', Lam var match_code] }
@@ -1002,7 +1002,7 @@ dsDo ctx stmts
; let match_args (pat, fail_op) (vs,body)
= do { var <- selectSimpleMatchVarL Many pat
- ; match <- matchSinglePatVar var (StmtCtxt ctx) pat
+ ; match <- matchSinglePatVar var Nothing (StmtCtxt ctx) pat
body_ty (cantFailMatchResult body)
; match_code <- dsHandleMonadicFailure ctx pat match fail_op
; return (var:vs, match_code)
=====================================
compiler/GHC/HsToCore/GuardedRHSs.hs
=====================================
@@ -36,7 +36,7 @@ import Control.Monad ( zipWithM )
import Data.List.NonEmpty ( NonEmpty, toList )
{-
- at dsGuarded@ is used for pattern bindings.
+ at dsGuarded@ is used for GRHSs.
It desugars:
\begin{verbatim}
| g1 -> e1
@@ -44,7 +44,7 @@ It desugars:
| gn -> en
where binds
\end{verbatim}
-producing an expression with a runtime error in the corner if
+producing an expression with a runtime error in the corner case if
necessary. The type argument gives the type of the @ei at .
-}
@@ -137,8 +137,8 @@ matchGuards (BindStmt _ pat bind_rhs : stmts) ctx deltas rhs rhs_ty = do
match_result <- matchGuards stmts ctx deltas rhs rhs_ty
core_rhs <- dsLExpr bind_rhs
- match_result' <- matchSinglePatVar match_var (StmtCtxt ctx) pat rhs_ty
- match_result
+ match_result' <- matchSinglePatVar match_var (Just core_rhs) (StmtCtxt ctx)
+ pat rhs_ty match_result
pure $ bindNonRec match_var core_rhs <$> match_result'
matchGuards (LastStmt {} : _) _ _ _ _ = panic "matchGuards LastStmt"
=====================================
compiler/GHC/HsToCore/ListComp.hs
=====================================
@@ -617,7 +617,7 @@ dsMcBindStmt :: LPat GhcTc
dsMcBindStmt pat rhs' bind_op fail_op res1_ty stmts
= do { body <- dsMcStmts stmts
; var <- selectSimpleMatchVarL Many pat
- ; match <- matchSinglePatVar var (StmtCtxt (DoExpr Nothing)) pat
+ ; match <- matchSinglePatVar var Nothing (StmtCtxt (DoExpr Nothing)) pat
res1_ty (cantFailMatchResult body)
; match_code <- dsHandleMonadicFailure (MonadComp :: HsStmtContext GhcRn) pat match fail_op
; dsSyntaxExpr bind_op [rhs', Lam var match_code] }
=====================================
compiler/GHC/HsToCore/Match.hs
=====================================
@@ -66,7 +66,7 @@ import GHC.Data.FastString
import GHC.Types.Unique
import GHC.Types.Unique.DFM
-import Control.Monad(zipWithM, unless )
+import Control.Monad ( zipWithM, unless, when )
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NEL
import qualified Data.Map as Map
@@ -769,9 +769,9 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
-- @rhss_deltas@ is a flat list of covered Deltas for each RHS.
-- Each Match will split off one Deltas for its RHSs from this.
; matches_deltas <- if isMatchContextPmChecked dflags origin ctxt
- then addScrutTmCs mb_scr new_vars $
- -- See Note [Type and Term Equality Propagation]
- checkMatches (DsMatchContext ctxt locn) new_vars matches
+ then addHsScrutTmCs mb_scr new_vars $
+ -- See Note [Long-distance information]
+ covCheckMatches (DsMatchContext ctxt locn) new_vars matches
else pure (initDeltasMatches matches)
; eqns_info <- zipWithM mk_eqn_info matches matches_deltas
@@ -820,25 +820,24 @@ matchEquations ctxt vars eqns_info rhs_ty
; fail_expr <- mkErrorAppDs pAT_ERROR_ID rhs_ty error_doc
; extractMatchResult match_result fail_expr }
-{-
-************************************************************************
-* *
-\subsection[matchSimply]{@matchSimply@: match a single expression against a single pattern}
-* *
-************************************************************************
-
- at mkSimpleMatch@ is a wrapper for @match@ which deals with the
-situation where we want to match a single expression against a single
-pattern. It returns an expression.
--}
-
+-- | @matchSimply@ is a wrapper for 'match' which deals with the
+-- situation where we want to match a single expression against a single
+-- pattern. It returns an expression.
matchSimply :: CoreExpr -- ^ Scrutinee
-> HsMatchContext GhcRn -- ^ Match kind
-> LPat GhcTc -- ^ Pattern it should match
-> CoreExpr -- ^ Return this if it matches
-> CoreExpr -- ^ Return this if it doesn't
-> DsM CoreExpr
--- Do not warn about incomplete patterns; see matchSinglePat comments
+-- Some reasons 'matchSimply' is not defined using 'matchWrapper' (#18572):
+-- * Some call sites like in 'deBindComp' specify a @fail_expr@ that isn't a
+-- straight @patError@
+-- * It receives an already desugared 'CoreExpr' for the scrutinee, not an
+-- 'HsExpr' like 'matchWrapper' expects
+-- * Filling in all the phony fields for the 'MatchGroup' for a single pattern
+-- match is awkward
+-- * And we still export 'matchSinglePatVar', so not much is gained if we
+-- don't also implement it in terms of 'matchWrapper'
matchSimply scrut hs_ctx pat result_expr fail_expr = do
let
match_result = cantFailMatchResult result_expr
@@ -858,7 +857,7 @@ matchSinglePat :: CoreExpr -> HsMatchContext GhcRn -> LPat GhcTc
matchSinglePat (Var var) ctx pat ty match_result
| not (isExternalName (idName var))
- = matchSinglePatVar var ctx pat ty match_result
+ = matchSinglePatVar var Nothing ctx pat ty match_result
matchSinglePat scrut hs_ctx pat ty match_result
= do { var <- selectSimpleMatchVarL Many pat
@@ -867,22 +866,22 @@ matchSinglePat scrut hs_ctx pat ty match_result
-- and to create field selectors. All of which only
-- bind unrestricted variables, hence the 'Many'
-- above.
- ; match_result' <- matchSinglePatVar var hs_ctx pat ty match_result
+ ; match_result' <- matchSinglePatVar var (Just scrut) hs_ctx pat ty match_result
; return $ bindNonRec var scrut <$> match_result'
}
matchSinglePatVar :: Id -- See Note [Match Ids]
+ -> Maybe CoreExpr -- ^ The scrutinee the match id is bound to
-> HsMatchContext GhcRn -> LPat GhcTc
-> Type -> MatchResult CoreExpr -> DsM (MatchResult CoreExpr)
-matchSinglePatVar var ctx pat ty match_result
+matchSinglePatVar var mb_scrut ctx pat ty match_result
= ASSERT2( isInternalName (idName var), ppr var )
do { dflags <- getDynFlags
; locn <- getSrcSpanDs
-
-- Pattern match check warnings
- ; if isMatchContextPmChecked dflags FromSource ctx
- then checkSingle dflags (DsMatchContext ctx locn) var (unLoc pat)
- else pure ()
+ ; when (isMatchContextPmChecked dflags FromSource ctx) $
+ addCoreScrutTmCs mb_scrut [var] $
+ covCheckPatBind (DsMatchContext ctx locn) var (unLoc pat)
; let eqn_info = EqnInfo { eqn_pats = [unLoc (decideBangHood dflags pat)]
, eqn_orig = FromSource
=====================================
compiler/GHC/HsToCore/Match.hs-boot
=====================================
@@ -29,6 +29,7 @@ matchSimply
matchSinglePatVar
:: Id
+ -> Maybe CoreExpr
-> HsMatchContext GhcRn
-> LPat GhcTc
-> Type
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -1,24 +1,51 @@
-{-
-Author: George Karachalias <george.karachalias at cs.kuleuven.be>
-
-Pattern Matching Coverage Checking.
--}
-
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE MultiWayIf #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE NamedFieldPuns #-}
-
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+-- | This module coverage checks pattern matches. It finds
+--
+-- * Uncovered patterns, certifying non-exhaustivity
+-- * Redundant equations
+-- * Equations with an inaccessible right-hand-side
+--
+-- The algorithm is based on the paper
+-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989)
+--
+-- There is an overview Figure 2 in there that's probably helpful.
+-- Here is an overview of how it's implemented, which follows the structure of
+-- the entry points such as 'covCheckMatches':
+--
+-- 1. Desugar source syntax (like 'LMatch') to guard tree variants (like
+-- 'GrdMatch'), with one of the desugaring functions (like 'desugarMatch').
+-- Follows Section 3.1 in the paper.
+-- 2. Coverage check guard trees (with a function like 'checkMatch') to get a
+-- 'CheckResult', containing
+-- a. The set of uncovered values, 'cr_uncov'
+-- b. And an annotated tree variant (like 'AnnMatch') that captures
+-- redundancy and inaccessibility information as 'RedSets' annotations
+-- Basically the UA function from Section 5.1. The Normalised Refinement Types
+-- Nabla are modeled as 'Deltas' and checked in "GHC.HsToCore.PmCheck.Oracle".
+-- 3. Collect redundancy information into a 'CIRB' with a function such
+-- as 'cirbsMatch'. Follows the R function from Figure 6 of the paper.
+-- 4. Format and report uncovered patterns and redundant equations ('CIRB')
+-- with 'formatReportWarnings'. Basically job of the G function, plus proper
+-- pretty printing of the warnings (Section 5.4 of the paper).
+-- 5. Return 'Deltas' reaching syntactic sub-components for
+-- Note [Long-distance information]. Collected by functions such as
+-- 'ldiMatch'. See Section 4.1 of the paper.
module GHC.HsToCore.PmCheck (
-- Checking and printing
- checkSingle, checkMatches, checkGRHSs,
+ covCheckPatBind, covCheckMatches, covCheckGRHSs,
isMatchContextPmChecked,
- -- See Note [Type and Term Equality Propagation]
- addTyCsDs, addScrutTmCs
+ -- See Note [Long-distance information]
+ addTyCs, addCoreScrutTmCs, addHsScrutTmCs
) where
#include "HsVersions.h"
@@ -37,7 +64,6 @@ import GHC.Tc.Utils.Zonk (shortCutLit)
import GHC.Types.Id
import GHC.Core.ConLike
import GHC.Types.Name
-import GHC.Tc.Instance.Family
import GHC.Builtin.Types
import GHC.Types.SrcLoc
import GHC.Utils.Misc
@@ -62,35 +88,148 @@ import GHC.Core.Type
import GHC.HsToCore.Utils (isTrueLHsExpr)
import GHC.Data.Maybe
import qualified GHC.LanguageExtensions as LangExt
-import GHC.Utils.Monad (concatMapM)
+import GHC.Utils.Monad (concatMapM, mapMaybeM)
import Control.Monad (when, forM_, zipWithM)
import Data.List (elemIndex)
import qualified Data.Semigroup as Semi
-import Data.List.NonEmpty (NonEmpty(..))
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+import Data.Coerce
-{-
-This module checks pattern matches for:
-\begin{enumerate}
- \item Equations that are redundant
- \item Equations with inaccessible right-hand-side
- \item Exhaustiveness
-\end{enumerate}
+--
+-- * Exported entry points to the checker
+--
-The algorithm is based on the paper:
+-- | A non-empty delta that is initialised from the ambient refinement type
+-- capturing long-distance information, or the trivially habitable 'Deltas' if
+-- the former is uninhabited.
+-- See Note [Recovering from unsatisfiable pattern-matching constraints].
+getLdiDeltas :: DsM Deltas
+getLdiDeltas = do
+ deltas <- getPmDeltas
+ isInhabited deltas >>= \case
+ True -> pure deltas
+ False -> pure initDeltas
+
+-- | Check a pattern binding (let, where) for exhaustiveness.
+covCheckPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
+-- See Note [covCheckPatBind only checks PatBindRhs]
+covCheckPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
+ missing <- getLdiDeltas
+ pat_bind <- desugarPatBind loc var p
+ tracePm "covCheckPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
+ result <- unCA (checkPatBind pat_bind) missing
+ tracePm "}: " (ppr (cr_uncov result))
+ formatReportWarnings cirbsPatBind ctxt [var] result
+covCheckPatBind _ _ _ = pure ()
+
+-- | Exhaustive for guard matches, is used for guards in pattern bindings and
+-- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs.
+covCheckGRHSs
+ :: HsMatchContext GhcRn -- ^ Match context, for warning messages
+ -> GRHSs GhcTc (LHsExpr GhcTc) -- ^ The GRHSs to check
+ -> DsM (NonEmpty Deltas) -- ^ Covered 'Deltas' for each RHS, for long
+ -- distance info
+covCheckGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
+ let combined_loc = foldl1 combineSrcSpans (map getLoc grhss)
+ ctxt = DsMatchContext hs_ctxt combined_loc
+ matches <- desugarGRHSs combined_loc empty guards
+ missing <- getLdiDeltas
+ tracePm "covCheckGRHSs" (hang (vcat [ppr ctxt
+ , text "Guards:"])
+ 2
+ (pprGRHSs hs_ctxt guards $$ ppr missing))
+ result <- unCA (checkGRHSs matches) missing
+ tracePm "}: " (ppr (cr_uncov result))
+ formatReportWarnings cirbsGRHSs ctxt [] result
+ return (ldiGRHS <$> cr_ret result)
+
+-- | Check a list of syntactic 'Match'es (part of case, functions, etc.), each
+-- with a 'Pat' and one or more 'GRHSs':
+--
+-- @
+-- f x y | x == y = 1 -- match on x and y with two guarded RHSs
+-- | otherwise = 2
+-- f _ _ = 3 -- clause with a single, un-guarded RHS
+-- @
+--
+-- Returns one non-empty 'Deltas' for 1.) each pattern of a 'Match' and 2.)
+-- each of a 'Match'es 'GRHS' for Note [Long-distance information].
+--
+-- Special case: When there are /no matches/, then the functionassumes it
+-- checks and @-XEmptyCase@ with only a single match variable.
+-- See Note [Checking EmptyCase].
+covCheckMatches
+ :: DsMatchContext -- ^ Match context, for warnings messages
+ -> [Id] -- ^ Match variables, i.e. x and y above
+ -> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches
+ -> DsM [(Deltas, NonEmpty Deltas)] -- ^ One covered 'Deltas' per Match and
+ -- GRHS, for long distance info.
+covCheckMatches ctxt vars matches = do
+ -- We have to force @missing@ before printing out the trace message,
+ -- otherwise we get interleaved output from the solver. This function
+ -- should be strict in @missing@ anyway!
+ !missing <- getLdiDeltas
+ tracePm "covCheckMatches {" $
+ hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
+ 2
+ (vcat (map ppr matches) $$ ppr missing)
+ case NE.nonEmpty matches of
+ Nothing -> do
+ -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
+ let var = only vars
+ empty_case <- desugarEmptyCase var
+ result <- unCA (checkEmptyCase empty_case) missing
+ tracePm "}: " (ppr (cr_uncov result))
+ formatReportWarnings cirbsEmptyCase ctxt vars result
+ return []
+ Just matches -> do
+ matches <- desugarMatches vars matches
+ result <- unCA (checkMatchGroup matches) missing
+ tracePm "}: " (ppr (cr_uncov result))
+ formatReportWarnings cirbsMatchGroup ctxt vars result
+ return (NE.toList (ldiMatchGroup (cr_ret result)))
+
+{- Note [covCheckPatBind only checks PatBindRhs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ at covCheckPatBind@'s sole purpose is to check vanilla pattern bindings, like
+ at x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
+But its caller is also called for individual pattern guards in a @StmtCtxt at .
+For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
+go through this function. It makes no sense to do coverage checking there:
+ * Pattern guards may well fail. Fall-through is not an unrecoverable panic,
+ but rather behavior the programmer expects, so inexhaustivity should not be
+ reported.
+ * Redundancy is already reported for the whole GRHS via one of the other
+ exported coverage checking functions. Also reporting individual redundant
+ guards is... redundant. See #17646.
+Note that we can't just omit checking of @StmtCtxt@ altogether (by adjusting
+'isMatchContextPmChecked'), because that affects the other checking functions,
+too.
+
+Note [Checking EmptyCase]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-XEmptyCase is useful for matching on empty data types like 'Void'. For example,
+the following is a complete match:
- "GADTs Meet Their Match:
- Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
+ f :: Void -> ()
+ f x = case x of {}
- https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf
+Really, -XEmptyCase is the only way to write a program that at the same time is
+safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
+(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
+exception into divergence (@f x = f x@).
-%************************************************************************
-%* *
- Pattern Match Check Types
-%* *
-%************************************************************************
+Semantically, unlike every other case expression, -XEmptyCase is strict in its
+match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the
+initial Delta and check if there are any values left to match on.
-}
+--
+-- * Guard language
+--
+
-- | A very simple language for pattern guards. Let bindings, bang patterns,
-- and matching variables against flat constructor patterns.
data PmGrd
@@ -106,9 +245,9 @@ data PmGrd
}
-- | @PmBang x@ corresponds to a @seq x True@ guard.
- -- If the extra SrcInfo is present, the bang guard came from a source
- -- bang pattern, in which case we might want to report it as redundant,
- -- see Note [Dead bang patterns].
+ -- If the extra 'SrcInfo' is present, the bang guard came from a source
+ -- bang pattern, in which case we might want to report it as redundant.
+ -- See Note [Dead bang patterns].
| PmBang {
pm_id :: !Id,
pm_loc :: !(Maybe SrcInfo)
@@ -144,24 +283,115 @@ instance Monoid Precision where
mempty = Precise
mappend = (Semi.<>)
--- | Means by which we identify source location for later pretty-printing
--- in a warning message. 'SDoc' for the equation to show, 'Located' for
--- the location.
+--
+-- * Guard tree language
+--
+
+-- | Means by which we identify a source construct for later pretty-printing in
+-- a warning message. 'SDoc' for the equation to show, 'Located' for the
+-- location.
type SrcInfo = Located SDoc
--- | A representation of the desugaring to 'PmGrd's of all clauses of a
--- function definition/pattern match/etc.
-data GrdTree
- = Rhs !SrcInfo
- | Guard !PmGrd !GrdTree
- -- ^ @Guard grd t@ will try to match @grd@ and on success continue to match
- -- @t at . Falls through if either match fails. Models left-to-right semantics
- -- of pattern matching.
- | Sequence ![GrdTree]
- -- ^ @Sequence (t:ts)@ matches against @t@, and then matches all
- -- fallen-through values against @Sequence ts at . Models top-to-bottom semantics
- -- of pattern matching.
- -- @Sequence []@ always fails; it is useful for Note [Checking EmptyCase].
+-- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
+-- (later digested into a 'CIRB').
+data RedSets
+ = RedSets
+ { rs_cov :: !Deltas
+ -- ^ The /Covered/ set; the set of values reaching a particular program
+ -- point.
+ , rs_div :: !Deltas
+ -- ^ The /Diverging/ set; empty if no match can lead to divergence.
+ -- If it wasn't empty, we have to turn redundancy warnings into
+ -- inaccessibility warnings for any subclauses.
+ , rs_bangs :: !(OrdList (Deltas, SrcInfo))
+ -- ^ If any of the 'Deltas' is empty, the corresponding 'SrcInfo' pin-points
+ -- a bang pattern in source that is redundant. See Note [Dead bang patterns].
+ }
+
+-- The following two type synonyms instantiate our tree structures to guard
+-- trees and annotated trees, respectively, by giving the types to attach as
+-- payload.
+
+-- | Used as tree payload pre-checking. The LYG guards to check.
+type Pre = [PmGrd]
+
+-- | Used as tree payload post-checking. The redundancy info we elaborated.
+type Post = RedSets
+
+-- | A guard tree denoting 'MatchGroup'.
+newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
+
+-- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
+-- GRHS.
+data PmMatch p = PmMatch { pm_pats :: !p, pm_grhss :: !(NonEmpty (PmGRHS p)) }
+
+-- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
+-- useful for printing out in warnings messages.
+data PmGRHS p = PmGRHS { pg_grds :: !p, pg_rhs :: !SrcInfo }
+
+-- | A guard tree denoting an -XEmptyCase.
+newtype PmEmptyCase = PmEmptyCase { pe_var :: Id }
+
+-- | A guard tree denoting a pattern binding.
+newtype PmPatBind p =
+ -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
+ -- rather than on the pattern bindings.
+ PmPatBind (PmGRHS p)
+
+emptyRedSets :: RedSets
+-- Semigroup instance would be misleading!
+emptyRedSets = RedSets mempty mempty mempty
+
+pprSrcInfo :: SrcInfo -> SDoc
+pprSrcInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
+pprSrcInfo (L s _) = ppr s
+
+-- | Format LYG guards as @| True <- x, let x = 42, !z@
+pprLygGuards :: [PmGrd] -> SDoc
+pprLygGuards [] = empty
+pprLygGuards (g:gs) = fsep (char '|' <+> ppr g : map ((comma <+>) . ppr) gs)
+
+-- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
+-- @{ <first alt>; ...; <last alt> }@
+pprLygSequence :: Outputable a => NonEmpty a -> SDoc
+pprLygSequence (NE.toList -> as) =
+ braces (space <> fsep (punctuate semi (map ppr as)) <> space)
+
+instance Outputable (PmMatchGroup Pre) where
+ ppr (PmMatchGroup matches) = pprLygSequence matches
+
+instance Outputable (PmMatch Pre) where
+ ppr (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
+ pprLygGuards grds <+> ppr grhss
+
+instance Outputable (PmGRHS Pre) where
+ ppr (PmGRHS { pg_grds = grds, pg_rhs = rhs }) =
+ pprLygGuards grds <+> text "->" <+> pprSrcInfo rhs
+
+instance Outputable (PmPatBind Pre) where
+ ppr (PmPatBind PmGRHS { pg_grds = grds, pg_rhs = bind }) =
+ ppr bind <+> pprLygGuards grds <+> text "=" <+> text "..."
+
+instance Outputable PmEmptyCase where
+ ppr (PmEmptyCase { pe_var = var }) =
+ text "<empty case on " <> ppr var <> text ">"
+
+pprRedSets :: RedSets -> SDoc
+-- It's useful to change this definition for different verbosity levels in
+-- printf-debugging
+pprRedSets RedSets { rs_cov = _cov, rs_div = _div, rs_bangs = _bangs }
+ = empty
+
+instance Outputable (PmMatchGroup Post) where
+ ppr (PmMatchGroup matches) = pprLygSequence matches
+
+instance Outputable (PmMatch Post) where
+ ppr (PmMatch { pm_pats = red, pm_grhss = grhss }) =
+ pprRedSets red <+> ppr grhss
+
+instance Outputable (PmGRHS Post) where
+ ppr (PmGRHS { pg_grds = red, pg_rhs = rhs }) =
+ pprRedSets red <+> text "->" <+> pprSrcInfo rhs
{- Note [Dead bang patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -178,7 +408,7 @@ that under no circumstances can force a thunk that wasn't already forced.
Dead bangs are a form of redundant bangs; see below.
We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
-where the PmBang appears in 'checkGrdTree'. If not, then clearly the bang is
+where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
dead. Such a dead bang is then indicated in the annotated pattern-match tree by
a 'RedundantSrcBang' wrapping. In 'redundantAndInaccessibles', we collect
all dead bangs to warn about.
@@ -197,235 +427,9 @@ it is redundant with the forcing done by the () match. We currently don't
detect redundant bangs that aren't dead.
-}
--- | The digest of 'checkGrdTree', representing the annotated pattern-match
--- tree. 'extractRedundancyInfo' can figure out redundant and proper
--- inaccessible RHSs from this, as well as dead bangs.
-data AnnotatedTree
- = AccessibleRhs !Deltas !SrcInfo
- -- ^ A RHS deemed accessible. The 'Deltas' is the (non-empty) set of covered
- -- values.
- | InaccessibleRhs !SrcInfo
- -- ^ A RHS deemed inaccessible; it covers no value.
- | MayDiverge !AnnotatedTree
- -- ^ Asserts that the tree may force diverging values, so not all of its
- -- clauses can be redundant.
- | SequenceAnn !Deltas ![AnnotatedTree]
- -- ^ @SequenceAnn inc ts@ mirrors @'Sequence' ts@ for preserving the
- -- skeleton of a 'GrdTree's @ts at . It also carries the set of incoming values
- -- @inc at .
- | RedundantSrcBang !SrcInfo !AnnotatedTree
- -- ^ For tracking redundant bangs. See Note [Dead bang patterns]
-
-pprSrcInfo :: SrcInfo -> SDoc
-pprSrcInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
-pprSrcInfo (L s _) = ppr s
-
-instance Outputable GrdTree where
- ppr (Rhs info) = text "->" <+> pprSrcInfo info
- -- Format guards as "| True <- x, let x = 42, !z"
- ppr g at Guard{} = fsep (prefix (map ppr grds)) <+> ppr t
- where
- (t, grds) = collect_grds g
- collect_grds (Guard grd t) = (grd :) <$> collect_grds t
- collect_grds t = (t, [])
- prefix [] = []
- prefix (s:sdocs) = char '|' <+> s : map (comma <+>) sdocs
- ppr (Sequence []) = text "<empty case>"
- ppr (Sequence ts) = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
-
-instance Outputable AnnotatedTree where
- ppr (AccessibleRhs _delta info) = parens (ppr _delta) <+> pprSrcInfo info
- ppr (InaccessibleRhs info) = text "inaccessible" <+> pprSrcInfo info
- ppr (MayDiverge t) = text "div" <+> ppr t
- ppr (SequenceAnn _ []) = text "<empty case>"
- ppr (SequenceAnn _ ts) = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
- ppr (RedundantSrcBang l t) = text "redundant bang" <+> pprSrcInfo l <+> ppr t
-
--- | Lift 'addPmCts' over 'Deltas'.
-addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
-addPmCtsDeltas deltas cts = liftDeltasM (\d -> addPmCts d cts) deltas
-
--- | 'addPmCtsDeltas' a single 'PmCt'.
-addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas
-addPmCtDeltas deltas ct = addPmCtsDeltas deltas (unitBag ct)
-
--- | Test if any of the 'Delta's is inhabited. Currently this is pure, because
--- we preserve the invariant that there are no uninhabited 'Delta's. But that
--- could change in the future, for example by implementing this function in
--- terms of @notNull <$> provideEvidence 1 ds at .
-isInhabited :: Deltas -> DsM Bool
-isInhabited (MkDeltas ds) = pure (not (null ds))
-
--- | Pattern-match check result
-data CheckResult
- = CheckResult
- { cr_clauses :: !AnnotatedTree
- -- ^ Captures redundancy info for each clause in the original program.
- -- (for -Woverlapping-patterns)
- , cr_uncov :: !Deltas
- -- ^ The set of uncovered values falling out at the bottom.
- -- (for -Wincomplete-patterns)
- , cr_approx :: !Precision
- -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
- -- purpose of suggesting to crank it up in the warning message
- }
-
-instance Outputable CheckResult where
- ppr (CheckResult c unc pc)
- = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
- [ field "clauses" c <> comma
- , field "uncov" unc])
- where
- ppr_precision Precise = empty
- ppr_precision Approximate = text "(Approximate)"
- field name value = text name <+> equals <+> ppr value
-
-{-
-%************************************************************************
-%* *
- Entry points to the checker: checkSingle and checkMatches
-%* *
-%************************************************************************
--}
-
--- | Check a single pattern binding (let) for exhaustiveness.
-checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
-checkSingle dflags ctxt@(DsMatchContext kind locn) var p = do
- tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
- -- We only ever need to run this in a context where we need exhaustivity
- -- warnings (so not in pattern guards or comprehensions, for example, because
- -- they are perfectly fine to fail).
- -- Omitting checking this flag emits redundancy warnings twice in obscure
- -- cases like #17646.
- when (exhaustive dflags kind) $ do
- -- TODO: This could probably call checkMatches, like checkGRHSs.
- missing <- getPmDeltas
- tracePm "checkSingle: missing" (ppr missing)
- fam_insts <- dsGetFamInstEnvs
- grd_tree <- mkGrdTreeRhs (L locn $ ppr p) <$> translatePat fam_insts var p
- res <- checkGrdTree grd_tree missing
- dsPmWarn dflags ctxt [var] res
-
--- | Exhaustive for guard matches, is used for guards in pattern bindings and
--- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs.
-checkGRHSs
- :: HsMatchContext GhcRn -- ^ Match context, for warning messages
- -> GRHSs GhcTc (LHsExpr GhcTc) -- ^ The GRHSs to check
- -> DsM (NonEmpty Deltas) -- ^ Covered 'Deltas' for each RHS, for long
- -- distance info
-checkGRHSs hs_ctx guards@(GRHSs _ grhss _) = do
- let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
- dsMatchContext = DsMatchContext hs_ctx combinedLoc
- match = L combinedLoc $
- Match { m_ext = noExtField
- , m_ctxt = hs_ctx
- , m_pats = []
- , m_grhss = guards }
- [(_, deltas)] <- checkMatches dsMatchContext [] [match]
- pure deltas
-
--- | Check a list of syntactic /match/es (part of case, functions, etc.), each
--- with a /pat/ and one or more /grhss/:
--
--- @
--- f x y | x == y = 1 -- match on x and y with two guarded RHSs
--- | otherwise = 2
--- f _ _ = 3 -- clause with a single, un-guarded RHS
--- @
+-- * Desugaring source syntax to guard trees
--
--- Returns one 'Deltas' for each GRHS, representing its covered values, or the
--- incoming uncovered 'Deltas' (from 'getPmDeltas') if the GRHS is inaccessible.
--- Since there is at least one /grhs/ per /match/, the list of 'Deltas' is at
--- least as long as the list of matches.
-checkMatches
- :: DsMatchContext -- ^ Match context, for warnings messages
- -> [Id] -- ^ Match variables, i.e. x and y above
- -> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches
- -> DsM [(Deltas, NonEmpty Deltas)] -- ^ One covered 'Deltas' per RHS, for long
- -- distance info.
-checkMatches ctxt vars matches = do
- tracePm "checkMatches" (hang (vcat [ppr ctxt
- , ppr vars
- , text "Matches:"])
- 2
- (vcat (map ppr matches)))
-
- init_deltas <- getPmDeltas
- missing <- case matches of
- -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
- [] | [var] <- vars -> addPmCtDeltas init_deltas (PmNotBotCt var)
- _ -> pure init_deltas
- fam_insts <- dsGetFamInstEnvs
- grd_tree <- translateMatches fam_insts vars matches
- res <- checkGrdTree grd_tree missing
-
- dflags <- getDynFlags
- dsPmWarn dflags ctxt vars res
-
- return (extractRhsDeltas (cr_clauses res))
-
--- | Extract the 'Deltas' reaching the RHSs of the 'AnnotatedTree' for a match
--- group.
--- For 'AccessibleRhs's, this is stored in the tree node, whereas
--- 'InaccessibleRhs's fall back to the supplied original 'Deltas'.
--- See @Note [Recovering from unsatisfiable pattern-matching constraints]@.
-extractRhsDeltas :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
-extractRhsDeltas = go_matches
- where
- go_matches :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
- go_matches (SequenceAnn def ts) = map (go_match def) ts -- -XEmptyCase handled here!
- go_matches t = pprPanic "extractRhsDeltas.go_matches" (text "Matches must start with SequenceAnn. But was" $$ ppr t)
-
- go_match :: Deltas -> AnnotatedTree -> (Deltas, NonEmpty Deltas)
- -- There is no -XEmptyCase at this level, only at the Matches level. So @ts@
- -- is non-empty!
- go_match def (SequenceAnn pat ts) = (pat, foldMap1 (text "go_match: empty SequenceAnn") (go_grhss def) ts)
- go_match def (MayDiverge t) = go_match def t
- go_match def (RedundantSrcBang _ t) = go_match def t
- -- Even if there's only a single GRHS, we wrap it in a SequenceAnn for the
- -- Deltas covered by the pattern. So the remaining cases are impossible!
- go_match _ t = pprPanic "extractRhsDeltas.go_match" (text "Single GRHS must be wrapped in SequenceAnn. But got " $$ ppr t)
-
- go_grhss :: Deltas -> AnnotatedTree -> NonEmpty Deltas
- -- There is no -XEmptyCase at this level, only at the Matches level. So @ts@
- -- is non-empty!
- go_grhss def (SequenceAnn _ ts) = foldMap1 (text "go_grhss: empty SequenceAnn") (go_grhss def) ts
- go_grhss def (MayDiverge t) = go_grhss def t
- go_grhss def (RedundantSrcBang _ t) = go_grhss def t
- go_grhss _ (AccessibleRhs deltas _) = deltas :| []
- go_grhss def (InaccessibleRhs _) = def :| []
-
- foldMap1 msg _ [] = pprPanic "extractRhsDeltas.foldMap1" msg
- foldMap1 _ f (x:xs) = foldl' (\acc x -> acc Semi.<> f x) (f x) xs
-
-{- Note [Checking EmptyCase]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--XEmptyCase is useful for matching on empty data types like 'Void'. For example,
-the following is a complete match:
-
- f :: Void -> ()
- f x = case x of {}
-
-Really, -XEmptyCase is the only way to write a program that at the same time is
-safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
-(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
-exception into divergence (@f x = f x@).
-
-Semantically, unlike every other case expression, -XEmptyCase is strict in its
-match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the
-initial Delta and check if there are any values left to match on.
--}
-
-{-
-%************************************************************************
-%* *
- Transform source syntax to *our* syntax
-%* *
-%************************************************************************
--}
-
--- -----------------------------------------------------------------------
--- * Utilities
-- | Smart constructor that eliminates trivial lets
mkPmLetVar :: Id -> Id -> GrdVec
@@ -458,7 +462,7 @@ mkListGrds a ((x, head_grds):xs) = do
-- | Create a 'GrdVec' refining a match variable to a 'PmLit'.
mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
mkPmLitGrds x (PmLit _ (PmLitString s)) = do
- -- We translate String literals to list literals for better overlap reasoning.
+ -- We desugar String literals to list literals for better overlap reasoning.
-- It's a little unfortunate we do this here rather than in
-- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and
-- 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much simpler
@@ -476,37 +480,34 @@ mkPmLitGrds x lit = do
, pm_con_args = [] }
pure [grd]
--- -----------------------------------------------------------------------
--- * Transform (Pat Id) into GrdVec
-
--- | @translatePat _ x pat@ transforms @pat@ into a 'GrdVec', where
+-- | @desugarPat _ x pat@ transforms @pat@ into a 'GrdVec', where
-- the variable representing the match is @x at .
-translatePat :: FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
-translatePat fam_insts x pat = case pat of
+desugarPat :: Id -> Pat GhcTc -> DsM GrdVec
+desugarPat x pat = case pat of
WildPat _ty -> pure []
VarPat _ y -> pure (mkPmLetVar (unLoc y) x)
- ParPat _ p -> translateLPat fam_insts x p
+ ParPat _ p -> desugarLPat x p
LazyPat _ _ -> pure [] -- like a wildcard
BangPat _ p@(L l p') ->
-- Add the bang in front of the list, because it will happen before any
-- nested stuff.
- (PmBang x pm_loc :) <$> translateLPat fam_insts x p
- where pm_loc = Just (L l (ppr p'))
+ (PmBang x pm_loc :) <$> desugarLPat x p
+ where pm_loc = Just (L l (ppr p'))
- -- (x at pat) ==> Translate pat with x as match var and handle impedance
+ -- (x at pat) ==> Desugar pat with x as match var and handle impedance
-- mismatch with incoming match var
- AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> translateLPat fam_insts y p
+ AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> desugarLPat y p
- SigPat _ p _ty -> translateLPat fam_insts x p
+ SigPat _ p _ty -> desugarLPat x p
- -- See Note [Translate CoPats]
+ -- See Note [Desugar CoPats]
-- Generally the translation is
-- pat |> co ===> let y = x |> co, pat <- y where y is a match var of pat
XPat (CoPat wrapper p _ty)
- | isIdHsWrapper wrapper -> translatePat fam_insts x p
- | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts x p
+ | isIdHsWrapper wrapper -> desugarPat x p
+ | WpCast co <- wrapper, isReflexiveCo co -> desugarPat x p
| otherwise -> do
- (y, grds) <- translatePatV fam_insts p
+ (y, grds) <- desugarPatV p
wrap_rhs_y <- dsHsWrapper wrapper
pure (PmLet y (wrap_rhs_y (Var x)) : grds)
@@ -521,13 +522,13 @@ translatePat fam_insts x pat = case pat of
-- (fun -> pat) ===> let y = fun x, pat <- y where y is a match var of pat
ViewPat _arg_ty lexpr pat -> do
- (y, grds) <- translateLPatV fam_insts pat
+ (y, grds) <- desugarLPatV pat
fun <- dsLExpr lexpr
pure $ PmLet y (App fun (Var x)) : grds
-- list
ListPat (ListPatTc _elem_ty Nothing) ps ->
- translateListPat fam_insts x ps
+ desugarListPat x ps
-- overloaded list
ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do
@@ -535,11 +536,11 @@ translatePat fam_insts x pat = case pat of
case splitListTyConApp_maybe pat_ty of
Just _e_ty
| not (xopt LangExt.RebindableSyntax dflags)
- -- Just translate it as a regular ListPat
- -> translateListPat fam_insts x pats
+ -- Just desugar it as a regular ListPat
+ -> desugarListPat x pats
_ -> do
y <- mkPmId (mkListTy elem_ty)
- grds <- translateListPat fam_insts y pats
+ grds <- desugarListPat y pats
rhs_y <- dsSyntaxExpr to_list [Var x]
pure $ PmLet y rhs_y : grds
@@ -565,7 +566,7 @@ translatePat fam_insts x pat = case pat of
, cpt_dicts = dicts
}
} -> do
- translateConPatOut fam_insts x con arg_tys ex_tvs dicts ps
+ desugarConPatOut x con arg_tys ex_tvs dicts ps
NPat ty (L _ olit) mb_neg _ -> do
-- See Note [Literal short cut] in "GHC.HsToCore.Match.Literal"
@@ -594,46 +595,44 @@ translatePat fam_insts x pat = case pat of
mkPmLitGrds x lit
TuplePat _tys pats boxity -> do
- (vars, grdss) <- mapAndUnzipM (translateLPatV fam_insts) pats
+ (vars, grdss) <- mapAndUnzipM desugarLPatV pats
let tuple_con = tupleDataCon boxity (length vars)
pure $ vanillaConGrd x tuple_con vars : concat grdss
SumPat _ty p alt arity -> do
- (y, grds) <- translateLPatV fam_insts p
+ (y, grds) <- desugarLPatV p
let sum_con = sumDataCon alt arity
-- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
pure $ vanillaConGrd x sum_con [y] : grds
- -- --------------------------------------------------------------------------
- -- Not supposed to happen
- SplicePat {} -> panic "Check.translatePat: SplicePat"
+ SplicePat {} -> panic "Check.desugarPat: SplicePat"
--- | 'translatePat', but also select and return a new match var.
-translatePatV :: FamInstEnvs -> Pat GhcTc -> DsM (Id, GrdVec)
-translatePatV fam_insts pat = do
+-- | 'desugarPat', but also select and return a new match var.
+desugarPatV :: Pat GhcTc -> DsM (Id, GrdVec)
+desugarPatV pat = do
x <- selectMatchVar Many pat
- grds <- translatePat fam_insts x pat
+ grds <- desugarPat x pat
pure (x, grds)
-translateLPat :: FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
-translateLPat fam_insts x = translatePat fam_insts x . unLoc
+desugarLPat :: Id -> LPat GhcTc -> DsM GrdVec
+desugarLPat x = desugarPat x . unLoc
--- | 'translateLPat', but also select and return a new match var.
-translateLPatV :: FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
-translateLPatV fam_insts = translatePatV fam_insts . unLoc
+-- | 'desugarLPat', but also select and return a new match var.
+desugarLPatV :: LPat GhcTc -> DsM (Id, GrdVec)
+desugarLPatV = desugarPatV . unLoc
--- | @translateListPat _ x [p1, ..., pn]@ is basically
--- @translateConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
+-- | @desugarListPat _ x [p1, ..., pn]@ is basically
+-- @desugarConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
-- constructing the 'ConPatOut's.
-translateListPat :: FamInstEnvs -> Id -> [LPat GhcTc] -> DsM GrdVec
-translateListPat fam_insts x pats = do
- vars_and_grdss <- traverse (translateLPatV fam_insts) pats
+desugarListPat :: Id -> [LPat GhcTc] -> DsM GrdVec
+desugarListPat x pats = do
+ vars_and_grdss <- traverse desugarLPatV pats
mkListGrds x vars_and_grdss
--- | Translate a constructor pattern
-translateConPatOut :: FamInstEnvs -> Id -> ConLike -> [Type] -> [TyVar]
+-- | Desugar a constructor pattern
+desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
-> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec
-translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
+desugarConPatOut x con univ_tys ex_tvs dicts = \case
PrefixCon ps -> go_field_pats (zip [0..] ps)
InfixCon p1 p2 -> go_field_pats (zip [0..] [p1,p2])
RecCon (HsRecFields fs _) -> go_field_pats (rec_field_ps fs)
@@ -647,7 +646,7 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
where
tagged_pat f = (lbl_to_index (getName (hsRecFieldId f)), hsRecFieldArg f)
-- Unfortunately the label info is empty when the DataCon wasn't defined
- -- with record field labels, hence we translate to field index.
+ -- with record field labels, hence we desugar to field index.
orig_lbls = map flSelector $ conLikeFieldLabels con
lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls
@@ -658,10 +657,10 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
-- the first field of @tagged_pats at .
-- See Note [Field match order for RecCon]
- -- Translate the mentioned field patterns. We're doing this first to get
+ -- Desugar the mentioned field patterns. We're doing this first to get
-- the Ids for pm_con_args.
let trans_pat (n, pat) = do
- (var, pvec) <- translateLPatV fam_insts pat
+ (var, pvec) <- desugarLPatV pat
pure ((n, var), pvec)
(tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats
@@ -687,77 +686,81 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
-- 1. 2. 3.
pure (con_grd : bang_grds ++ arg_grds)
--- | Translate a the 'Match'es of a 'MatchGroup'
-translateMatches :: FamInstEnvs -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)]
- -> DsM GrdTree
-translateMatches fam_insts vars matches =
- -- It's important that we wrap a 'Sequence' even if it only wraps a singleton.
- -- 'extractRhsDeltas' needs this to recover 'MatchGroup' structure.
- Sequence <$> traverse (translateMatch fam_insts vars) matches
-
--- Translate a single match
-translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc)
- -> DsM GrdTree
-translateMatch fam_insts vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
- pats' <- concat <$> zipWithM (translateLPat fam_insts) vars pats
- grhss' <- translateGRHSs fam_insts match_loc (sep (map ppr pats)) grhss
- -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
- return (foldr Guard grhss' pats')
-
-mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
-mkGrdTreeRhs sdoc = foldr Guard (Rhs sdoc)
-
-translateGRHSs :: FamInstEnvs -> SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM GrdTree
-translateGRHSs fam_insts match_loc pp_pats grhss =
- -- It's important that we wrap a 'Sequence' even if it only wraps a singleton.
- -- 'extractRhsDeltas' needs this to recover 'GRHSs' structure.
- Sequence <$> traverse (translateLGRHS fam_insts match_loc pp_pats) (grhssGRHSs grhss)
-
--- | Translate a guarded right-hand side to a single 'GrdTree'
-translateLGRHS :: FamInstEnvs -> SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
-translateLGRHS fam_insts match_loc pp_pats (L _loc (GRHS _ gs _)) =
- -- _loc points to the match separator (ie =, ->) that comes after the guards..
- mkGrdTreeRhs loc_sdoc <$> concatMapM (translateGuard fam_insts . unLoc) gs
- where
- loc_sdoc
- -- pp_pats is the space-separated pattern of the current Match this
- -- GRHS belongs to, so the @A B x@ part in @A B x | 0 <- x at .
- | null gs = L match_loc pp_pats
- | otherwise = L grd_loc (pp_pats <+> vbar <+> interpp'SP gs)
- L grd_loc _ = head gs
-
--- | Translate a guard statement to a 'GrdVec'
-translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
-translateGuard fam_insts guard = case guard of
- BodyStmt _ e _ _ -> translateBoolGuard e
- LetStmt _ binds -> translateLet (unLoc binds)
- BindStmt _ p e -> translateBind fam_insts p e
- LastStmt {} -> panic "translateGuard LastStmt"
- ParStmt {} -> panic "translateGuard ParStmt"
- TransStmt {} -> panic "translateGuard TransStmt"
- RecStmt {} -> panic "translateGuard RecStmt"
- ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
-
--- | Translate let-bindings
-translateLet :: HsLocalBinds GhcTc -> DsM GrdVec
-translateLet _binds = return []
-
--- | Translate a pattern guard
+desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre)
+-- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
+desugarPatBind loc var pat =
+ PmPatBind . flip PmGRHS (L loc (ppr pat)) <$> desugarPat var pat
+
+desugarEmptyCase :: Id -> DsM PmEmptyCase
+desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
+
+-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
+desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
+ -> DsM (PmMatchGroup Pre)
+desugarMatches vars matches =
+ PmMatchGroup <$> traverse (desugarMatch vars) matches
+
+-- Desugar a single match
+desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PmMatch Pre)
+desugarMatch vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
+ pats' <- concat <$> zipWithM desugarLPat vars pats
+ grhss' <- desugarGRHSs match_loc (sep (map ppr pats)) grhss
+ -- tracePm "desugarMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
+ return PmMatch { pm_pats = pats', pm_grhss = grhss' }
+
+desugarGRHSs :: SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty (PmGRHS Pre))
+desugarGRHSs match_loc pp_pats grhss
+ = traverse (desugarLGRHS match_loc pp_pats)
+ . expectJust "desugarGRHSs"
+ . NE.nonEmpty
+ $ grhssGRHSs grhss
+
+-- | Desugar a guarded right-hand side to a single 'GrdTree'
+desugarLGRHS :: SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM (PmGRHS Pre)
+desugarLGRHS match_loc pp_pats (L _loc (GRHS _ gs _)) = do
+ -- _loc points to the match separator (ie =, ->) that comes after the guards.
+ -- Hence we have to pass in the match_loc, which we use in case that the RHS
+ -- is unguarded.
+ -- pp_pats is the space-separated pattern of the current Match this
+ -- GRHS belongs to, so the @A B x@ part in @A B x | 0 <- x at .
+ let rhs_info = case gs of
+ [] -> L match_loc pp_pats
+ (L grd_loc _):_ -> L grd_loc (pp_pats <+> vbar <+> interpp'SP gs)
+ grds <- concatMapM (desugarGuard . unLoc) gs
+ pure PmGRHS { pg_grds = grds, pg_rhs = rhs_info }
+
+-- | Desugar a guard statement to a 'GrdVec'
+desugarGuard :: GuardStmt GhcTc -> DsM GrdVec
+desugarGuard guard = case guard of
+ BodyStmt _ e _ _ -> desugarBoolGuard e
+ LetStmt _ binds -> desugarLet (unLoc binds)
+ BindStmt _ p e -> desugarBind p e
+ LastStmt {} -> panic "desugarGuard LastStmt"
+ ParStmt {} -> panic "desugarGuard ParStmt"
+ TransStmt {} -> panic "desugarGuard TransStmt"
+ RecStmt {} -> panic "desugarGuard RecStmt"
+ ApplicativeStmt {} -> panic "desugarGuard ApplicativeLastStmt"
+
+-- | Desugar let-bindings
+desugarLet :: HsLocalBinds GhcTc -> DsM GrdVec
+desugarLet _binds = return []
+
+-- | Desugar a pattern guard
-- @pat <- e ==> let x = e; <guards for pat <- x>@
-translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
-translateBind fam_insts p e = dsLExpr e >>= \case
+desugarBind :: LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
+desugarBind p e = dsLExpr e >>= \case
Var y
| Nothing <- isDataConId_maybe y
-- RHS is a variable, so that will allow us to omit the let
- -> translateLPat fam_insts y p
+ -> desugarLPat y p
rhs -> do
- (x, grds) <- translateLPatV fam_insts p
+ (x, grds) <- desugarLPatV p
pure (PmLet x rhs : grds)
--- | Translate a boolean guard
+-- | Desugar a boolean guard
-- @e ==> let x = e; True <- x@
-translateBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
-translateBoolGuard e
+desugarBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
+desugarBoolGuard e
| isJust (isTrueLHsExpr e) = return []
-- The formal thing to do would be to generate (True <- True)
-- but it is trivial to solve so instead we give back an empty
@@ -802,7 +805,7 @@ for a pattern match appear matter. Consider a situation similar to T5117:
f (0:_) = ()
f (0:[]) = ()
-The latter clause is clearly redundant. Yet if we translate the second clause as
+The latter clause is clearly redundant. Yet if we desugar the second clause as
[x:xs' <- xs, [] <- xs', 0 <- x]
@@ -814,52 +817,11 @@ translation would have been
And we have to take in the guards on list cells into @mkListGrds at .
-Note [Countering exponential blowup]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Precise pattern match exhaustiveness checking is necessarily exponential in
-the size of some input programs. We implement a counter-measure in the form of
-the -fmax-pmcheck-models flag, limiting the number of Deltas we check against
-each pattern by a constant.
-
-How do we do that? Consider
-
- f True True = ()
- f True True = ()
-
-And imagine we set our limit to 1 for the sake of the example. The first clause
-will be checked against the initial Delta, {}. Doing so will produce an
-Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}.
-Also we find the first clause to cover the model {x~True,y~True}.
-
-But the Uncovered set we get out of the match is too huge! We somehow have to
-ensure not to make things worse as they are already, so we continue checking
-with a singleton Uncovered set of the initial Delta {}. Why is this
-sound (wrt. notion of the GADTs Meet their Match paper)? Well, it basically
-amounts to forgetting that we matched against the first clause. The values
-represented by {} are a superset of those represented by its two refinements
-{x/~True} and {x~True,y/~True}.
-
-This forgetfulness becomes very apparent in the example above: By continuing
-with {} we don't detect the second clause as redundant, as it again covers the
-same non-empty subset of {}. So we don't flag everything as redundant anymore,
-but still will never flag something as redundant that isn't.
-
-For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
-and report @f _ _@ as missing, which is a superset of the actual missing
-matches. But soundness means we will never fail to report a missing match.
-
-This mechanism is implemented in 'throttle'.
-
-Guards are an extreme example in this regard, with #11195 being a particularly
-dreadful example: Since their RHS are often pretty much unique, we split on a
-variable (the one representing the RHS) that doesn't occur anywhere else in the
-program, so we don't actually get useful information out of that split!
-
-Note [Translate CoPats]
+Note [Desugar CoPats]
~~~~~~~~~~~~~~~~~~~~~~~
-The pattern match checker did not know how to handle coerced patterns `CoPat`
-efficiently, which gave rise to #11276. The original approach translated
-`CoPat`s:
+The pattern match checker did not know how to handle coerced patterns
+`CoPat` efficiently, which gave rise to #11276. The original approach
+desugared `CoPat`s:
pat |> co ===> x (pat <- (x |> co))
@@ -874,108 +836,92 @@ a lot of false warnings.
But we can check whether the coercion is a hole or if it is just refl, in
which case we can drop it.
-
-%************************************************************************
-%* *
- Utilities for Pattern Match Checking
-%* *
-%************************************************************************
-}
--- ----------------------------------------------------------------------------
--- * Basic utilities
-
-{-
-Note [Extensions to GADTs Meet Their Match]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The GADTs Meet Their Match paper presents the formalism that GHC's coverage
-checker adheres to. Since the paper's publication, there have been some
-additional features added to the coverage checker which are not described in
-the paper. This Note serves as a reference for these new features.
-
-* Value abstractions are severely simplified to the point where they are just
- variables. The information about the shape of a variable is encoded in
- the oracle state 'Delta' instead.
-* Handling of uninhabited fields like `!Void`.
- See Note [Strict argument type constraints] in GHC.HsToCore.PmCheck.Oracle.
-* Efficient handling of literal splitting, large enumerations and accurate
- redundancy warnings for `COMPLETE` groups through the oracle.
-
-Note [Filtering out non-matching COMPLETE sets]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Currently, conlikes in a COMPLETE set are simply grouped by the
-type constructor heading the return type. This is nice and simple, but it does
-mean that there are scenarios when a COMPLETE set might be incompatible with
-the type of a scrutinee. For instance, consider (from #14135):
-
- data Foo a = Foo1 a | Foo2 a
-
- pattern MyFoo2 :: Int -> Foo Int
- pattern MyFoo2 i = Foo2 i
-
- {-# COMPLETE Foo1, MyFoo2 #-}
-
- f :: Foo a -> a
- f (Foo1 x) = x
-
-`f` has an incomplete pattern-match, so when choosing which constructors to
-report as unmatched in a warning, GHC must choose between the original set of
-data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe
-that GHC shouldn't even consider the COMPLETE set as a possibility: the return
-type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since
-there's no substitution `s` such that s(Foo Int) = Foo a.
-
-To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern
-synonym constructor's return type matches the type of the scrutinee, and if one
-doesn't, then we remove the whole COMPLETE set from consideration.
-
-One might wonder why GHC only checks /pattern synonym/ constructors, and not
-/data/ constructors as well. The reason is because that the type of a
-GADT constructor very well may not match the type of a scrutinee, and that's
-OK. Consider this example (from #14059):
-
- data SBool (z :: Bool) where
- SFalse :: SBool False
- STrue :: SBool True
-
- pattern STooGoodToBeTrue :: forall (z :: Bool). ()
- => z ~ True
- => SBool z
- pattern STooGoodToBeTrue = STrue
- {-# COMPLETE SFalse, STooGoodToBeTrue #-}
-
- wobble :: SBool z -> Bool
- wobble STooGoodToBeTrue = True
-
-In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse
-should be matched against, even though its type, SBool False, does not match
-the scrutinee type, SBool z.
-
-SG: Another angle at this is that the implied constraints when we instantiate
-universal type variables in the return type of a GADT will lead to *provided*
-thetas, whereas when we instantiate the return type of a pattern synonym that
-corresponds to a *required* theta. See Note [Pattern synonym result type] in
-PatSyn. Note how isValidCompleteMatches will successfully filter out
-
- pattern Just42 :: Maybe Int
- pattern Just42 = Just 42
-
-But fail to filter out the equivalent
-
- pattern Just'42 :: (a ~ Int) => Maybe a
- pattern Just'42 = Just 42
-
-Which seems fine as far as tcMatchTy is concerned, but it raises a few eye
-brows.
--}
+--
+-- * Coverage checking guard trees into annotated trees
+--
-{-
-%************************************************************************
-%* *
- Heart of the algorithm: checkGrdTree
-%* *
-%************************************************************************
--}
+-- | Pattern-match coverage check result
+data CheckResult a
+ = CheckResult
+ { cr_ret :: !a
+ -- ^ A hole for redundancy info and covered sets.
+ , cr_uncov :: !Deltas
+ -- ^ The set of uncovered values falling out at the bottom.
+ -- (for -Wincomplete-patterns, but also important state for the algorithm)
+ , cr_approx :: !Precision
+ -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
+ -- purpose of suggesting to crank it up in the warning message. Writer state.
+ } deriving Functor
+
+instance Outputable a => Outputable (CheckResult a) where
+ ppr (CheckResult c unc pc)
+ = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
+ [ field "ret" c <> comma
+ , field "uncov" unc])
+ where
+ ppr_precision Precise = empty
+ ppr_precision Approximate = text "(Approximate)"
+ field name value = text name <+> equals <+> ppr value
+
+-- | Lift 'addPmCts' over 'Deltas'.
+addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
+addPmCtsDeltas deltas cts = liftDeltasM (\d -> addPmCts d cts) deltas
+
+-- | 'addPmCtsDeltas' for a single 'PmCt'.
+addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas
+addPmCtDeltas deltas ct = addPmCtsDeltas deltas (unitBag ct)
+
+-- | Test if any of the 'Delta's is inhabited. Currently this is pure, because
+-- we preserve the invariant that there are no uninhabited 'Delta's. But that
+-- could change in the future, for example by implementing this function in
+-- terms of @notNull <$> provideEvidence 1 ds at .
+isInhabited :: Deltas -> DsM Bool
+isInhabited (MkDeltas ds) = pure (not (null ds))
+
+-- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
+newtype CheckAction a = CA { unCA :: Deltas -> DsM (CheckResult a) }
+ deriving Functor
+
+-- | Composes 'CheckAction's top-to-bottom:
+-- If a value falls through the resulting action, then it must fall through the
+-- first action and then through the second action.
+-- If a value matches the resulting action, then it either matches the
+-- first action or matches the second action.
+-- Basically the semantics of the LYG branching construct.
+topToBottom :: (top -> bot -> ret)
+ -> CheckAction top
+ -> CheckAction bot
+ -> CheckAction ret
+topToBottom f (CA top) (CA bot) = CA $ \inc -> do
+ t <- top inc
+ b <- bot (cr_uncov t)
+ pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
+ , cr_uncov = cr_uncov b
+ , cr_approx = cr_approx t Semi.<> cr_approx b }
+
+
+-- | Composes 'CheckAction's left-to-right:
+-- If a value falls through the resulting action, then it either falls through the
+-- first action or through the second action.
+-- If a value matches the resulting action, then it must match the first action
+-- and then match the second action.
+-- Basically the semantics of the LYG guard construct.
+leftToRight :: (RedSets -> right -> ret)
+ -> CheckAction RedSets
+ -> CheckAction right
+ -> CheckAction ret
+leftToRight f (CA left) (CA right) = CA $ \inc -> do
+ l <- left inc
+ r <- right (rs_cov (cr_ret l))
+ limit <- maxPmCheckModels <$> getDynFlags
+ let uncov = cr_uncov l Semi.<> cr_uncov r
+ -- See Note [Countering exponential blowup]
+ let (prec', uncov') = throttle limit inc uncov
+ pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
+ , cr_uncov = uncov'
+ , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }
-- | @throttle limit old new@ returns @old@ if the number of 'Delta's in @new@
-- is exceeding the given @limit@ and the @old@ number of 'Delta's.
@@ -993,230 +939,226 @@ conMatchForces (PmAltConLike (RealDataCon dc))
| isNewTyCon (dataConTyCon dc) = False
conMatchForces _ = True
--- | Makes sure that we only wrap a single 'MayDiverge' around an
--- 'AnnotatedTree', purely for esthetic reasons.
-mayDiverge :: AnnotatedTree -> AnnotatedTree
-mayDiverge a@(MayDiverge _) = a
-mayDiverge a = MayDiverge a
-
--- | Computes two things:
---
--- * The set of uncovered values not matched by any of the clauses of the
--- 'GrdTree'. Note that 'PmCon' guards are the only way in which values
--- fall through from one 'Many' branch to the next.
--- * An 'AnnotatedTree' that contains divergence and inaccessibility info
--- for all clauses. Will be fed to 'extractRedundancyInfo' for
--- presenting redundant and proper innaccessible RHSs, as well as dead
--- bangs to the user.
-checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
--- RHS: Check that it covers something and wrap Inaccessible if not
-checkGrdTree' (Rhs sdoc) deltas = do
- is_covered <- isInhabited deltas
- let clauses
- | is_covered = AccessibleRhs deltas sdoc
- | otherwise = InaccessibleRhs sdoc
- pure CheckResult
- { cr_clauses = clauses
- , cr_uncov = MkDeltas emptyBag
- , cr_approx = Precise }
--- let x = e: Refine with x ~ e
-checkGrdTree' (Guard (PmLet x e) tree) deltas = do
- deltas' <- addPmCtDeltas deltas (PmCoreCt x e)
- checkGrdTree' tree deltas'
--- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
-checkGrdTree' (Guard (PmBang x src_bang_info) tree) deltas = do
- has_diverged <- addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
- deltas' <- addPmCtDeltas deltas (PmNotBotCt x)
- res <- checkGrdTree' tree deltas'
- let clauses
- | not has_diverged
- , Just info <- src_bang_info
- = RedundantSrcBang info (cr_clauses res)
- | has_diverged
- = mayDiverge (cr_clauses res)
- | otherwise -- won't diverge and it wasn't a source bang
- = cr_clauses res
-
- pure res{ cr_clauses = clauses }
-
--- Con: Diverge on x ~ ⊥, fall through on x /~ K and refine with x ~ K ys
--- and type info
-checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
- has_diverged <-
- if conMatchForces con
- then addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
- else pure False
- unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
- deltas' <- addPmCtsDeltas deltas $
- listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con tvs args
- -- tracePm "checkGrdTree:Con" (ppr deltas $$ ppr x $$ ppr con $$ ppr dicts $$ ppr deltas')
- CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
- limit <- maxPmCheckModels <$> getDynFlags
- let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
- pure CheckResult
- { cr_clauses = applyWhen has_diverged mayDiverge tree'
- , cr_uncov = unc'
- , cr_approx = prec Semi.<> prec' }
--- Sequence: Thread residual uncovered sets from equation to equation
-checkGrdTree' (Sequence ts) init_unc = go [] init_unc Precise ts
+-- First the functions that correspond to checking LYG primitives:
+
+checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
+-- The implementation is pretty similar to
+-- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
+checkSequence act (t :| []) = (:| []) <$> act t
+checkSequence act (t1 :| (t2:ts)) =
+ topToBottom (NE.<|) (act t1) (checkSequence act (t2:|ts))
+
+checkGrd :: PmGrd -> CheckAction RedSets
+checkGrd grd = CA $ \inc -> case grd of
+ -- let x = e: Refine with x ~ e
+ PmLet x e -> do
+ matched <- addPmCtDeltas inc (PmCoreCt x e)
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
+ -- Bang x _: Diverge on x ~ ⊥, refine with x /~ ⊥
+ PmBang x mb_info -> do
+ div <- addPmCtDeltas inc (PmBotCt x)
+ matched <- addPmCtDeltas inc (PmNotBotCt x)
+ -- See Note [Dead bang patterns]
+ -- mb_info = Just info <==> PmBang originates from bang pattern in source
+ let bangs | Just info <- mb_info = unitOL (div, info)
+ | otherwise = NilOL
+ pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
+ -- Con: Diverge on x ~ ⊥, fall through on x /~ K and refine with x ~ K ys
+ -- and type info
+ PmCon x con tvs dicts args -> do
+ div <- if conMatchForces con
+ then addPmCtDeltas inc (PmBotCt x)
+ else pure mempty
+ uncov <- addPmCtDeltas inc (PmNotConCt x con)
+ matched <- addPmCtsDeltas inc $
+ listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con tvs args
+ -- tracePm "checkGrd:Con" (ppr inc $$ ppr x $$ ppr con $$ ppr dicts $$ ppr matched)
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
+ , cr_uncov = uncov
+ , cr_approx = Precise }
+
+checkGrds :: [PmGrd] -> CheckAction RedSets
+checkGrds [] = CA $ \inc ->
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = inc }
+ , cr_uncov = mempty
+ , cr_approx = Precise }
+checkGrds (g:grds) = leftToRight merge (checkGrd g) (checkGrds grds)
where
- -- | Accumulates a CheckResult. Its type is more like
- -- @CheckResult -> [GrdTree] -> CheckResult@, but cr_clauses is a single
- -- 'AnnotatedTree', not a list thereof. Hence 3 parameters to thread the
- -- fields.
- go :: [AnnotatedTree] -> Deltas -> Precision -> [GrdTree] -> DsM CheckResult
- -- No cases left: Fall through for all values
- go ts' unc prec [] = pure CheckResult
- { cr_clauses = SequenceAnn init_unc (reverse ts')
- , cr_uncov = unc
- , cr_approx = prec }
- go ts' unc prec (t:ts) = do
- CheckResult t' unc_1 prec_t <- checkGrdTree' t unc
- go (t':ts') unc_1 (prec_t Semi.<> prec) ts
-
--- | Print diagnostic info and actually call 'checkGrdTree''.
-checkGrdTree :: GrdTree -> Deltas -> DsM CheckResult
-checkGrdTree guards deltas = do
- tracePm "checkGrdTree {" $ vcat [ ppr guards
- , ppr deltas ]
- res <- checkGrdTree' guards deltas
- tracePm "checkGrdTree }:" (ppr res) -- braces are easier to match by tooling
- return res
-
--- ----------------------------------------------------------------------------
--- * Propagation of term constraints inwards when checking nested matches
-
-{- Note [Type and Term Equality Propagation]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When checking a match it would be great to have all type and term information
-available so we can get more precise results. For this reason we have functions
-`addDictsDs' and `addTmVarCsDs' in GHC.HsToCore.Monad that store in the
-environment type and term constraints (respectively) as we go deeper.
-
-The type constraints we propagate inwards are collected by `collectEvVarsPats'
-in GHC.Hs.Pat. This handles bug #4139 ( see example
- https://gitlab.haskell.org/ghc/ghc/snippets/672 )
-where this is needed.
-
-For term equalities we do less, we just generate equalities for HsCase. For
-example we accurately give 2 redundancy warnings for the marked cases:
-
-f :: [a] -> Bool
-f x = case x of
-
- [] -> case x of -- brings (x ~ []) in scope
- [] -> True
- (_:_) -> False -- can't happen
-
- (_:_) -> case x of -- brings (x ~ (_:_)) in scope
- (_:_) -> True
- [] -> False -- can't happen
-
-Functions `addScrutTmCs' is responsible for generating
-these constraints.
--}
+ merge ri_g ri_grds = -- This operation would /not/ form a Semigroup!
+ RedSets { rs_cov = rs_cov ri_grds
+ , rs_div = rs_div ri_g Semi.<> rs_div ri_grds
+ , rs_bangs = rs_bangs ri_g Semi.<> rs_bangs ri_grds }
--- | Locally update 'dsl_deltas' with the given action, but defer evaluation
--- with 'unsafeInterleaveM' in order not to do unnecessary work.
-locallyExtendPmDelta :: (Deltas -> DsM Deltas) -> DsM a -> DsM a
-locallyExtendPmDelta ext k = do
- deltas <- getPmDeltas
- deltas' <- unsafeInterleaveM $ do
- deltas' <- ext deltas
- inh <- isInhabited deltas'
- -- If adding a constraint would lead to a contradiction, don't add it.
- -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@
- -- for why this is done.
- if inh
- then pure deltas'
- else pure deltas
- updPmDeltas deltas' k
+checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
+checkMatchGroup (PmMatchGroup matches) =
+ PmMatchGroup <$> checkSequence checkMatch matches
--- | Add in-scope type constraints if the coverage checker might run and then
--- run the given action.
-addTyCsDs :: Origin -> Bag EvVar -> DsM a -> DsM a
-addTyCsDs origin ev_vars m = do
- dflags <- getDynFlags
- applyWhen (needToRunPmCheck dflags origin)
- (locallyExtendPmDelta (\deltas -> addPmCtsDeltas deltas (PmTyCt . evVarPred <$> ev_vars)))
- m
+checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
+checkMatch (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
+ leftToRight PmMatch (checkGrds grds) (checkGRHSs grhss)
--- | Add equalities for the scrutinee to the local 'DsM' environment when
--- checking a case expression:
--- case e of x { matches }
--- When checking matches we record that (x ~ e) where x is the initial
--- uncovered. All matches will have to satisfy this equality.
-addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
-addScrutTmCs Nothing _ k = k
-addScrutTmCs (Just scr) [x] k = do
- scr_e <- dsLExpr scr
- locallyExtendPmDelta (\deltas -> addPmCtsDeltas deltas (unitBag (PmCoreCt x scr_e))) k
-addScrutTmCs _ _ _ = panic "addScrutTmCs: HsCase with more than one case binder"
-
-{-
-%************************************************************************
-%* *
- Pretty printing of exhaustiveness/redundancy check warnings
-%* *
-%************************************************************************
+checkGRHSs :: NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
+checkGRHSs = checkSequence checkGRHS
+
+checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
+checkGRHS (PmGRHS { pg_grds = grds, pg_rhs = rhs_info }) =
+ flip PmGRHS rhs_info <$> checkGrds grds
+
+checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
+checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
+ unc <- addPmCtDeltas inc (PmNotBotCt var)
+ pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
+
+checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
+checkPatBind = coerce checkGRHS
+
+{- Note [Countering exponential blowup]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Precise pattern match exhaustiveness checking is necessarily exponential in
+the size of some input programs. We implement a counter-measure in the form of
+the -fmax-pmcheck-models flag, limiting the number of Deltas we check against
+each pattern by a constant.
+
+How do we do that? Consider
+
+ f True True = ()
+ f True True = ()
+
+And imagine we set our limit to 1 for the sake of the example. The first clause
+will be checked against the initial Delta, {}. Doing so will produce an
+Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}.
+Also we find the first clause to cover the model {x~True,y~True}.
+
+But the Uncovered set we get out of the match is too huge! We somehow have to
+ensure not to make things worse as they are already, so we continue checking
+with a singleton Uncovered set of the initial Delta {}. Why is this
+sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
+to forgetting that we matched against the first clause. The values represented
+by {} are a superset of those represented by its two refinements {x/~True} and
+{x~True,y/~True}.
+
+This forgetfulness becomes very apparent in the example above: By continuing
+with {} we don't detect the second clause as redundant, as it again covers the
+same non-empty subset of {}. So we don't flag everything as redundant anymore,
+but still will never flag something as redundant that isn't.
+
+For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
+and report @f _ _@ as missing, which is a superset of the actual missing
+matches. But soundness means we will never fail to report a missing match.
+
+This mechanism is implemented in 'throttle'.
+
+Guards are an extreme example in this regard, with #11195 being a particularly
+dreadful example: Since their RHS are often pretty much unique, we split on a
+variable (the one representing the RHS) that doesn't occur anywhere else in the
+program, so we don't actually get useful information out of that split!
-}
--- | Check whether any part of pattern match checking is enabled for this
--- 'HsMatchContext' (does not matter whether it is the redundancy check or the
--- exhaustiveness check).
-isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
-isMatchContextPmChecked dflags origin kind
- | isGenerated origin
- = False
- | otherwise
- = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
+--
+-- * Collecting long-distance information
+--
--- | 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
- | isGenerated origin
- = False
- | otherwise
- = notNull (filter (`wopt` dflags) allPmCheckWarnings)
+ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Deltas, NonEmpty Deltas)
+ldiMatchGroup (PmMatchGroup matches) = ldiMatch <$> matches
+
+ldiMatch :: PmMatch Post -> (Deltas, NonEmpty Deltas)
+ldiMatch (PmMatch { pm_pats = red, pm_grhss = grhss }) =
+ (rs_cov red, ldiGRHS <$> grhss)
+
+ldiGRHS :: PmGRHS Post -> Deltas
+ldiGRHS (PmGRHS { pg_grds = red }) = rs_cov red
--- | A type for organising information to be used in warnings.
-data RedundancyInfo
- = RedundancyInfo
- { redundant_rhss :: ![SrcInfo]
- , inaccessible_rhss :: ![SrcInfo]
- , redundant_bangs :: ![Located SDoc]
+--
+-- * Collecting redundancy information
+--
+
+-- | The result of redundancy checking:
+-- * RHSs classified as /C/overed, /I/naccessible and /R/edundant
+-- * And redundant /B/ang patterns. See Note [Dead bang patterns].
+data CIRB
+ = CIRB
+ { cirb_cov :: !(OrdList SrcInfo) -- ^ Covered clauses
+ , cirb_inacc :: !(OrdList SrcInfo) -- ^ Inaccessible clauses
+ , cirb_red :: !(OrdList SrcInfo) -- ^ Redundant clauses
+ , cirb_bangs :: !(OrdList SrcInfo) -- ^ Redundant bang patterns
}
-extractRedundancyInfo :: AnnotatedTree -> RedundancyInfo
-extractRedundancyInfo tree =
- RedundancyInfo { redundant_rhss = fromOL ol_red
- , inaccessible_rhss = fromOL ol_inacc
- , redundant_bangs = fromOL ol_bangs }
- where
- (_ol_acc, ol_inacc, ol_red, ol_bangs) = go tree
- -- | Collects
- -- 1. accessible RHSs
- -- 2. proper inaccessible RHSs (so we can't delete them)
- -- 3. hypothetically redundant RHSs (so not only inaccessible, but we can
- -- even safely delete the equation without altering semantics)
- -- 4. 'Dead' bangs from the source, collected to be warned about
- -- See Note [Determining inaccessible clauses]
- -- See Note [Dead bang patterns]
- go :: AnnotatedTree -> (OrdList SrcInfo, OrdList SrcInfo, OrdList SrcInfo, OrdList SrcInfo)
- go (AccessibleRhs _ info) = (unitOL info, nilOL, nilOL , nilOL)
- go (InaccessibleRhs info) = (nilOL, nilOL, unitOL info, nilOL) -- presumably redundant
- go (MayDiverge t) = case go t of
- -- See Note [Determining inaccessible clauses]
- (acc, inacc, red, bs)
- | isNilOL acc && isNilOL inacc -> (nilOL, red, nilOL, bs)
- res -> res
- go (SequenceAnn _ ts) = foldMap go ts
- go (RedundantSrcBang l t) = case go t of
- -- See Note [Dead bang patterns]
- res@(acc, inacc, _, _)
- | isNilOL acc, isNilOL inacc -> res
- | otherwise -> (nilOL, nilOL, nilOL, unitOL l) Semi.<> res
+instance Semigroup CIRB where
+ CIRB a b c d <> CIRB e f g h = CIRB (a <> e) (b <> f) (c <> g) (d <> h)
+ where (<>) = (Semi.<>)
+
+instance Monoid CIRB where
+ mempty = CIRB mempty mempty mempty mempty
+
+markAllRedundant :: CIRB -> CIRB
+markAllRedundant CIRB { cirb_cov = cov, cirb_inacc = inacc, cirb_red = red } =
+ mempty { cirb_red = cov Semi.<> inacc Semi.<> red }
+
+-- See Note [Determining inaccessible clauses]
+ensureOneNotRedundant :: CIRB -> CIRB
+ensureOneNotRedundant ci = case ci of
+ CIRB { cirb_cov = NilOL, cirb_inacc = NilOL, cirb_red = ConsOL r rs }
+ -> ci { cirb_inacc = unitOL r, cirb_red = rs }
+ _ -> ci
+
+-- | Only adds the redundant bangs to the @CIRB@ if there is at least one
+-- non-redundant 'SrcInfo'. There is no point in remembering a redundant bang
+-- if the whole match is redundant!
+addRedundantBangs :: OrdList SrcInfo -> CIRB -> CIRB
+addRedundantBangs _red_bangs cirb at CIRB { cirb_cov = NilOL, cirb_inacc = NilOL } =
+ cirb
+addRedundantBangs red_bangs cirb =
+ cirb { cirb_bangs = cirb_bangs cirb Semi.<> red_bangs }
+
+-- | Checks the 'Deltas' in a 'RedSets' for inhabitants and returns
+-- 1. Whether the Covered set was inhabited
+-- 2. Whether the Diverging set was inhabited
+-- 3. All source bangs whose 'Deltas' were empty, which means they are
+-- redundant.
+testRedSets :: RedSets -> DsM (Bool, Bool, OrdList SrcInfo)
+testRedSets RedSets { rs_cov = cov, rs_div = div, rs_bangs = bangs } = do
+ is_covered <- isInhabited cov
+ may_diverge <- isInhabited div
+ red_bangs <- flip mapMaybeM (fromOL bangs) $ \(deltas, bang) -> do
+ isInhabited deltas >>= \case
+ True -> pure Nothing
+ False -> pure (Just bang)
+ pure (is_covered, may_diverge, toOL red_bangs)
+
+cirbsMatchGroup :: PmMatchGroup Post -> DsM CIRB
+cirbsMatchGroup (PmMatchGroup matches) =
+ Semi.sconcat <$> traverse cirbsMatch matches
+
+cirbsMatch :: PmMatch Post -> DsM CIRB
+cirbsMatch PmMatch { pm_pats = red, pm_grhss = grhss } = do
+ (is_covered, may_diverge, red_bangs) <- testRedSets red
+ cirb <- cirbsGRHSs grhss
+ pure $ addRedundantBangs red_bangs
+ -- See Note [Determining inaccessible clauses]
+ $ applyWhen may_diverge ensureOneNotRedundant
+ $ applyWhen (not is_covered) markAllRedundant
+ $ cirb
+
+cirbsGRHSs :: NonEmpty (PmGRHS Post) -> DsM CIRB
+cirbsGRHSs grhss = Semi.sconcat <$> traverse cirbsGRHS grhss
+
+cirbsGRHS :: PmGRHS Post -> DsM CIRB
+cirbsGRHS PmGRHS { pg_grds = red, pg_rhs = info } = do
+ (is_covered, may_diverge, red_bangs) <- testRedSets red
+ let cirb | is_covered = mempty { cirb_cov = unitOL info }
+ | may_diverge = mempty { cirb_inacc = unitOL info }
+ | otherwise = mempty { cirb_red = unitOL info }
+ pure (addRedundantBangs red_bangs cirb)
+
+cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
+cirbsEmptyCase _ = pure mempty
+
+cirbsPatBind :: PmPatBind Post -> DsM CIRB
+cirbsPatBind = coerce cirbsGRHS
{- Note [Determining inaccessible clauses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1231,26 +1173,29 @@ arguments we can ever reach clause 2's RHS, so we say it has inaccessible RHS
(as opposed to being completely redundant).
We detect an inaccessible RHS simply by pretending it's redundant, until we see
-that it's part of a sub-tree in the pattern match that forces some argument
-(which corresponds to wrapping the 'AnnotatedTree' in 'MayDiverge'). Then we
-turn all supposedly redundant RHSs into inaccessible ones.
-
-But as it turns out (@g@ from #17465) this is too conservative:
- g () | False = ()
- | otherwise = ()
-g's first clause has an inaccessible RHS, but it's also safe to delete. So it's
-redundant, really! But by just turning all redundant child clauses into
-inaccessible ones, we report the first clause as inaccessible.
-
-Clearly, it is enough if we say that we only degrade if *not all* of the child
-clauses are redundant. As long as there is at least one clause which we announce
-not to be redundant, the guard prefix responsible for the 'MayDiverge' will
-survive. Hence we check for that in 'extractRedundancyInfo'.
-}
--- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
-dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
-dsPmWarn dflags ctx@(DsMatchContext kind loc) vars result
+--
+-- * Formatting and reporting warnings
+--
+
+-- | Given a function that collects 'CIRB's, this function will emit warnings
+-- for a 'CheckResult'.
+formatReportWarnings :: (ann -> DsM CIRB) -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
+formatReportWarnings collect ctx vars cr at CheckResult { cr_ret = ann } = do
+ cov_info <- collect ann
+ dflags <- getDynFlags
+ reportWarnings dflags ctx vars cr{cr_ret=cov_info}
+
+-- | Issue all the warnings
+-- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
+reportWarnings :: DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
+reportWarnings dflags ctx@(DsMatchContext kind loc) vars
+ CheckResult { cr_ret = CIRB { cirb_inacc = inaccessible_rhss
+ , cirb_red = redundant_rhss
+ , cirb_bangs = redundant_bangs }
+ , cr_uncov = uncovered
+ , cr_approx = precision }
= when (flag_i || flag_u || flag_b) $ do
unc_examples <- getNFirstUncovered vars (maxPatterns + 1) uncovered
let exists_r = flag_i && notNull redundant_rhss
@@ -1276,13 +1221,6 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) vars result
when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
pprEqns vars unc_examples
where
- CheckResult
- { cr_clauses = clauses
- , cr_uncov = uncovered
- , cr_approx = precision } = result
- RedundancyInfo{redundant_rhss, inaccessible_rhss, redundant_bangs}
- = extractRedundancyInfo clauses
-
flag_i = overlapping dflags kind
flag_u = exhaustive dflags kind
flag_b = redundant_bang dflags
@@ -1323,44 +1261,30 @@ getNFirstUncovered vars n (MkDeltas deltas) = go n (bagToList deltas)
back <- go (n - length front) deltas
pure (front ++ back)
-{- Note [Inaccessible warnings for record updates]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#12957)
- data T a where
- T1 :: { x :: Int } -> T Bool
- T2 :: { x :: Int } -> T a
- T3 :: T a
-
- f :: T Char -> T a
- f r = r { x = 3 }
-
-The desugarer will (conservatively generate a case for T1 even though
-it's impossible:
- f r = case r of
- T1 x -> T1 3 -- Inaccessible branch
- T2 x -> T2 3
- _ -> error "Missing"
-
-We don't want to warn about the inaccessible branch because the programmer
-didn't put it there! So we filter out the warning here.
-
-The same can happen for long distance term constraints instead of type
-constraints (#17783):
-
- data T = A { x :: Int } | B { x :: Int }
- f r at A{} = r { x = 3 }
- f _ = B 0
-
-Here, the long distance info from the FunRhs match (@r ~ A x@) will make the
-clause matching on @B@ of the desugaring to @case@ redundant. It's generated
-code that we don't want to warn about.
--}
-
dots :: Int -> [a] -> SDoc
dots maxPatterns qs
| qs `lengthExceeds` maxPatterns = text "..."
| otherwise = empty
+pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
+pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
+ = vcat [text txt <+> msg,
+ sep [ text "In" <+> ppr_match <> char ':'
+ , nest 4 (rest_of_msg_fun pref)]]
+ where
+ txt | singular = "Pattern match"
+ | otherwise = "Pattern match(es)"
+
+ (ppr_match, pref)
+ = case kind of
+ FunRhs { mc_fun = L _ fun }
+ -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
+ _ -> (pprMatchContext kind, \ pp -> pp)
+
+--
+-- * Utilities
+--
+
-- | All warning flags that need to run the pattern match checker.
allPmCheckWarnings :: [WarningFlag]
allPmCheckWarnings =
@@ -1399,23 +1323,142 @@ exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
exhaustiveWarningFlag ThPatSplice = Nothing
exhaustiveWarningFlag PatSyn = Nothing
exhaustiveWarningFlag ThPatQuote = Nothing
-exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns
- -- in list comprehensions, pattern guards
- -- etc. They are often *supposed* to be
- -- incomplete
+-- Don't warn about incomplete patterns in list comprehensions, pattern guards
+-- etc. They are often *supposed* to be incomplete
+exhaustiveWarningFlag (StmtCtxt {}) = Nothing
--- True <==> singular
-pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
-pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
- = vcat [text txt <+> msg,
- sep [ text "In" <+> ppr_match <> char ':'
- , nest 4 (rest_of_msg_fun pref)]]
- where
- txt | singular = "Pattern match"
- | otherwise = "Pattern match(es)"
+-- | Check whether any part of pattern match checking is enabled for this
+-- 'HsMatchContext' (does not matter whether it is the redundancy check or the
+-- exhaustiveness check).
+isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
+isMatchContextPmChecked dflags origin kind
+ | isGenerated origin
+ = False
+ | otherwise
+ = overlapping dflags kind || exhaustive dflags kind
- (ppr_match, pref)
- = case kind of
- FunRhs { mc_fun = L _ fun }
- -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
- _ -> (pprMatchContext kind, \ pp -> pp)
+-- | 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
+ | isGenerated origin
+ = False
+ | otherwise
+ = notNull (filter (`wopt` dflags) allPmCheckWarnings)
+
+{- Note [Inaccessible warnings for record updates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#12957)
+ data T a where
+ T1 :: { x :: Int } -> T Bool
+ T2 :: { x :: Int } -> T a
+ T3 :: T a
+
+ f :: T Char -> T a
+ f r = r { x = 3 }
+
+The desugarer will conservatively generate a case for T1 even though
+it's impossible:
+ f r = case r of
+ T1 x -> T1 3 -- Inaccessible branch
+ T2 x -> T2 3
+ _ -> error "Missing"
+
+We don't want to warn about the inaccessible branch because the programmer
+didn't put it there! So we filter out the warning here.
+
+The same can happen for long distance term constraints instead of type
+constraints (#17783):
+
+ data T = A { x :: Int } | B { x :: Int }
+ f r at A{} = r { x = 3 }
+ f _ = B 0
+
+Here, the long distance info from the FunRhs match (@r ~ A x@) will make the
+clause matching on @B@ of the desugaring to @case@ redundant. It's generated
+code that we don't want to warn about.
+-}
+
+--
+-- * Long-distance information
+--
+
+-- | Locally update 'dsl_deltas' with the given action, but defer evaluation
+-- with 'unsafeInterleaveM' in order not to do unnecessary work.
+locallyExtendPmDeltas :: (Deltas -> DsM Deltas) -> DsM a -> DsM a
+locallyExtendPmDeltas ext k = do
+ deltas <- getLdiDeltas
+ deltas' <- unsafeInterleaveM $ ext deltas
+ updPmDeltas deltas' k
+
+-- | Add in-scope type constraints if the coverage checker might run and then
+-- run the given action.
+addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
+addTyCs origin ev_vars m = do
+ dflags <- getDynFlags
+ applyWhen (needToRunPmCheck dflags origin)
+ (locallyExtendPmDeltas (\deltas -> addPmCtsDeltas deltas (PmTyCt . evVarPred <$> ev_vars)))
+ m
+
+-- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment
+-- when checking a case expression:
+-- case e of x { matches }
+-- When checking matches we record that (x ~ e) where x is the initial
+-- uncovered. All matches will have to satisfy this equality.
+addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
+addCoreScrutTmCs Nothing _ k = k
+addCoreScrutTmCs (Just scr) [x] k =
+ flip locallyExtendPmDeltas k $ \deltas ->
+ addPmCtsDeltas deltas (unitBag (PmCoreCt x scr))
+addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id"
+
+-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first.
+addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
+addHsScrutTmCs Nothing _ k = k
+addHsScrutTmCs (Just scr) vars k = do
+ scr_e <- dsLExpr scr
+ addCoreScrutTmCs (Just scr_e) vars k
+
+{- Note [Long-distance information]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+ data Color = R | G | B
+ f :: Color -> Int
+ f R = …
+ f c = … (case c of
+ G -> True
+ B -> False) …
+
+Humans can make the "long-distance connection" between the outer pattern match
+and the nested case pattern match to see that the inner pattern match is
+exhaustive: @c@ can't be @R@ anymore because it was matched in the first clause
+of @f at .
+
+To achieve similar reasoning in the coverage checker, we keep track of the set
+of values that can reach a particular program point (often loosely referred to
+as "Covered set") in 'GHC.HsToCore.Monad.dsl_deltas'.
+We fill that set with Covered Deltas returned by the exported checking
+functions, which the call sites put into place with
+'GHC.HsToCore.Monad.updPmDeltas'.
+Call sites also extend this set with facts from type-constraint dictionaries,
+case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
+and 'addHsScrutTmCs'.
+
+Note [Recovering from unsatisfiable pattern-matching constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following code (see #12957 and #15450):
+
+ f :: Int ~ Bool => ()
+ f = case True of { False -> () }
+
+We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
+used not to do this; in fact, it would warn that the match was /redundant/!
+This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
+coverage checker deems any matches with unsatisfiable constraint sets to be
+unreachable.
+
+We make sure to always start from an inhabited 'Deltas' by calling
+'getLdiDeltas', which falls back to the trivially inhabited 'Deltas' if the
+long-distance info returned by 'GHC.HsToCore.Monad.getPmDeltas' is empty.
+-}
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -167,25 +167,6 @@ mkOneConFull arg_tys con = do
-- * Pattern match oracle
-{- Note [Recovering from unsatisfiable pattern-matching constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following code (see #12957 and #15450):
-
- f :: Int ~ Bool => ()
- f = case True of { False -> () }
-
-We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
-used not to do this; in fact, it would warn that the match was /redundant/!
-This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
-coverage checker deems any matches with unsatisfiable constraint sets to be
-unreachable.
-
-We decide to better than this. When beginning coverage checking, we first
-check if the constraints in scope are unsatisfiable, and if so, we start
-afresh with an empty set of constraints. This way, we'll get the warnings
-that we expect.
--}
-
-------------------------------------
-- * Composable satisfiability checks
@@ -1266,7 +1247,7 @@ isTyConTriviallyInhabited tc = elementOfUniqSet tc triviallyInhabitedTyCons
{- Note [Checking EmptyCase Expressions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Empty case expressions are strict on the scrutinee. That is, `case x of {}`
-will force argument `x`. Hence, `checkMatches` is not sufficient for checking
+will force argument `x`. Hence, `covCheckMatches` is not sufficient for checking
empty cases, because it assumes that the match is not strict (which is true
for all other cases, apart from EmptyCase). This gave rise to #10746. Instead,
we do the following:
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs
=====================================
@@ -592,5 +592,8 @@ instance Outputable Deltas where
instance Semigroup Deltas where
MkDeltas l <> MkDeltas r = MkDeltas (l `unionBags` r)
+instance Monoid Deltas where
+ mempty = MkDeltas emptyBag
+
liftDeltasM :: Monad m => (Delta -> m (Maybe Delta)) -> Deltas -> m Deltas
liftDeltasM f (MkDeltas ds) = MkDeltas . catBagMaybes <$> (traverse f ds)
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -323,7 +323,7 @@ data DsLclEnv = DsLclEnv {
dsl_meta :: DsMetaEnv, -- Template Haskell bindings
dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs
- -- See Note [Note [Type and Term Equality Propagation] in "GHC.HsToCore.PmCheck"
+ -- See Note [Note [Long-distance information] in "GHC.HsToCore.PmCheck"
-- The set of reaching values Deltas is augmented as we walk inwards,
-- refined through each pattern match in turn
dsl_deltas :: Deltas
=====================================
compiler/GHC/Utils/Misc.hs
=====================================
@@ -556,9 +556,8 @@ isSingleton :: [a] -> Bool
isSingleton [_] = True
isSingleton _ = False
-notNull :: [a] -> Bool
-notNull [] = False
-notNull _ = True
+notNull :: Foldable f => f a -> Bool
+notNull = not . null
only :: [a] -> a
#if defined(DEBUG)
=====================================
hadrian/src/Settings/Builders/Ghc.hs
=====================================
@@ -35,6 +35,9 @@ compileAndLinkHs = (builder (Ghc CompileHs) ||^ builder (Ghc LinkHs)) ? do
hasDynamic = elem dynamic ways
mconcat [ arg "-Wall"
, not useColor ? builder (Ghc CompileHs) ?
+ -- N.B. Target.trackArgument ignores this argument from the
+ -- input hash to avoid superfluous recompilation, avoiding
+ -- #18672.
arg "-fdiagnostics-color=never"
, (hasVanilla && hasDynamic) ? builder (Ghc CompileHs) ?
platformSupportsSharedLibs ? way vanilla ?
=====================================
hadrian/src/Target.hs
=====================================
@@ -21,11 +21,12 @@ type Target = H.Target Context Builder
trackArgument :: Target -> String -> Bool
trackArgument target arg = case builder target of
Make _ -> not $ threadArg arg
- Ghc _ _ -> not $ verbosityArg arg
+ Ghc _ _ -> not $ verbosityArg arg || diagnosticsColorArg arg
Cabal _ _ -> not $ verbosityArg arg || cabal_configure_ignore arg
_ -> True
where
threadArg s = dropWhileEnd isDigit s `elem` ["-j", "MAKEFLAGS=-j", "THREADS="]
verbosityArg s = dropWhileEnd isDigit s == "-v"
+ diagnosticsColorArg s = "-fdiagnostics-color=" `isPrefixOf` s -- N.B. #18672
cabal_configure_ignore s =
s `elem` [ "--configure-option=--quiet", "--configure-option=--disable-option-checking" ]
=====================================
testsuite/tests/deSugar/should_compile/ds020.stderr
=====================================
@@ -18,3 +18,11 @@ ds020.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
ds020.hs:23:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match is redundant
In an equation for ‘f’: f x@(~[]) = ...
+
+ds020.hs:32:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In a pattern binding: (x1 : xs1 : ys1) = ...
+
+ds020.hs:33:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In a pattern binding: (~x : ~xs : ~ys) = ...
=====================================
testsuite/tests/module/all.T
=====================================
@@ -83,7 +83,7 @@ test('mod61', normal, compile_fail, [''])
test('mod62', normal, compile_fail, [''])
test('mod63', normal, compile_fail, [''])
test('mod64', normal, compile, [''])
-test('mod65', normal, compile, [''])
+test('mod65', normal, compile, ['-Wno-overlapping-patterns'])
test('mod66', normal, compile_fail, [''])
test('mod67', normal, compile_fail, [''])
test('mod68', normal, compile_fail, [''])
=====================================
testsuite/tests/pmcheck/should_compile/T18572.hs
=====================================
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -Wincomplete-uni-patterns -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
+
+module T18572 where
+
+True = True -- no warning
+
+data SBool (b :: Bool) where
+ STrue :: SBool True
+ SFalse :: SBool False
+
+STrue = SFalse -- "redundant", not "inaccessible"
=====================================
testsuite/tests/pmcheck/should_compile/T18572.stderr
=====================================
@@ -0,0 +1,16 @@
+
+T18572.hs:12:1: warning: [-Winaccessible-code (in -Wdefault)]
+ • Couldn't match type ‘'False’ with ‘'True’
+ Inaccessible code in
+ a pattern with constructor: STrue :: SBool 'True,
+ in a pattern binding
+ • In the pattern: STrue
+ In a pattern binding: STrue = SFalse
+
+T18572.hs:12:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In a pattern binding: STrue = ...
+
+T18572.hs:12:1: warning: [-Wincomplete-uni-patterns]
+ Pattern match(es) are non-exhaustive
+ In a pattern binding: Patterns not matched: SFalse
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -102,6 +102,8 @@ test('T17234', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17248', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17340', normal, compile,
+ ['-Wredundant-bang-patterns'])
test('T17357', expect_broken(17357), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17376', normal, compile,
@@ -124,8 +126,8 @@ test('T18478', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18533', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
-test('T17340', normal, compile,
- ['-Wredundant-bang-patterns'])
+test('T18572', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-incomplete-uni-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
=====================================
testsuite/tests/rename/should_compile/T7085.stderr
=====================================
@@ -1,3 +1,7 @@
T7085.hs:8:6: warning: [-Wunused-pattern-binds (in -Wextra, -Wunused-binds)]
This pattern-binding binds no variables: Nothing = Just n
+
+T7085.hs:8:6: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In a pattern binding: Nothing = ...
=====================================
testsuite/tests/simplCore/should_run/T18638.hs
=====================================
@@ -0,0 +1,54 @@
+{-# LANGUAGE ExistentialQuantification, BangPatterns #-}
+{-# OPTIONS_GHC -O #-}
+
+module Main (main) where
+
+import Data.IORef (newIORef, readIORef)
+
+data Step s = Done
+ | Skip !s
+ | Yield !Char !s
+
+data Stream = forall s. Stream (s -> Step s) !s !Int
+
+unstreamList :: Stream -> [Char]
+unstreamList (Stream next s0 _) = unfold s0
+ where unfold !s = case next s of
+ Done -> []
+ Skip s' -> unfold s'
+ Yield x s' -> x : unfold s'
+{-# INLINE [0] unstreamList #-}
+
+appendS :: Stream -> Stream -> Stream
+appendS (Stream next s len) _ = Stream next s len
+{-# INLINE [0] appendS #-}
+
+justifyLeftI :: Int -> Int -> Stream
+justifyLeftI k u =
+ let
+ next Nothing = next (Just 0)
+ next (Just n)
+ | n < k = Yield 'a' (Just (n+1))
+ | otherwise = Done
+ {-# INLINE next #-}
+
+ in Stream next Nothing (max k u)
+{-# INLINE [0] justifyLeftI #-}
+
+prettyPrintLogStats :: Int -> [String]
+prettyPrintLogStats rawResults = map fromRow columns
+ where
+ columns :: [Int]
+ columns = map (\_ -> 0) [rawResults]
+
+ moduleLen, lineLen :: Int
+ (moduleLen, lineLen) = foldr (\_ (_,_) -> (5, 2)) (0, 0) columns
+
+ fromRow :: Int -> String
+ fromRow x = unstreamList (justifyLeftI moduleLen x `appendS` justifyLeftI lineLen x)
+
+main :: IO ()
+main = do
+ timingsRef <- newIORef 0
+ timings <- readIORef timingsRef
+ putStrLn $ concat $ prettyPrintLogStats timings
=====================================
testsuite/tests/simplCore/should_run/T18638.stdout
=====================================
@@ -0,0 +1 @@
+aaaaa
=====================================
testsuite/tests/simplCore/should_run/all.T
=====================================
@@ -92,3 +92,4 @@ test('T17206', exit_code(1), compile_and_run, [''])
test('T17151', [], multimod_compile_and_run, ['T17151', ''])
test('T18012', normal, compile_and_run, [''])
test('T17744', normal, compile_and_run, [''])
+test('T18638', normal, compile_and_run, [''])
=====================================
testsuite/tests/unboxedsums/all.T
=====================================
@@ -30,5 +30,5 @@ test('T12711', only_ways(['ghci']), ghci_script, ['T12711.script'])
# extra_files([ "unboxedsums" + str(i) + ".hs" for i in range(1, 12) ])],
# makefile_test, [])
-test('UbxSumLevPoly', normal, compile, [''])
+test('UbxSumLevPoly', normal, compile, ['-Wno-overlapping-patterns'])
test('T14051', normal, multi_compile, ['T14051.hs', [('T14051a.hs', '')], '-O2 -v0'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c34a51ae9c43abe51c34279e511d8358d039d739...04f0cae614fecbd20581326fdebdc74282305027
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c34a51ae9c43abe51c34279e511d8358d039d739...04f0cae614fecbd20581326fdebdc74282305027
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200910/09498759/attachment-0001.html>
More information about the ghc-commits
mailing list