[Git][ghc/ghc][wip/T18565] PmCheck: Big refactor using guard tree variants more closely following source syntax (#18565)
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Aug 31 12:24:10 UTC 2020
Sebastian Graf pushed to branch wip/T18565 at Glasgow Haskell Compiler / GHC
Commits:
65d51d90 by Sebastian Graf at 2020-08-31T14:23:54+02: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.
- - - - -
14 changed files:
- compiler/GHC/Data/OrdList.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/Match.hs
- 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
- testsuite/tests/deSugar/should_compile/ds020.stderr
- testsuite/tests/module/all.T
- testsuite/tests/pmcheck/should_compile/T18572.hs
- testsuite/tests/rename/should_compile/T7085.stderr
- testsuite/tests/unboxedsums/all.T
Changes:
=====================================
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, covCheckGRHSs )
+import GHC.HsToCore.PmCheck ( addTyCs, covCheckGRHSs )
import GHC.Hs -- lots of things
import GHC.Core -- lots of things
@@ -151,14 +151,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
@@ -200,11 +200,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, covCheckGRHSs )
+import GHC.HsToCore.PmCheck ( addTyCs, covCheckGRHSs )
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Core.FamInstEnv( topNormaliseType )
@@ -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
=====================================
compiler/GHC/HsToCore/Match.hs
=====================================
@@ -770,8 +770,8 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
-- Each Match will split off one Deltas for its RHSs from this.
; matches_deltas <- if isMatchContextPmChecked dflags origin ctxt
then addHsScrutTmCs mb_scr new_vars $
- -- See Note [Type and Term Equality Propagation]
- covCheckMatchGroup (DsMatchContext ctxt locn) new_vars matches
+ -- 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
@@ -881,7 +881,7 @@ matchSinglePatVar var mb_scrut ctx pat ty match_result
-- Pattern match check warnings
; when (isMatchContextPmChecked dflags FromSource ctx) $
addCoreScrutTmCs mb_scrut [var] $
- covCheckPatBind dflags (DsMatchContext ctx locn) var (unLoc pat)
+ covCheckPatBind (DsMatchContext ctx locn) var (unLoc pat)
; let eqn_info = EqnInfo { eqn_pats = [unLoc (decideBangHood dflags pat)]
, eqn_orig = FromSource
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -1,24 +1,49 @@
-{-
-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 #-}
+
+-- | 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 'CIRBCollector' such
+-- as 'collectMatch'. 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]. See Section 4.1 of the paper.
module GHC.HsToCore.PmCheck (
-- Checking and printing
- covCheckPatBind, covCheckMatchGroup, covCheckGRHSs,
+ covCheckPatBind, covCheckMatches, covCheckGRHSs,
isMatchContextPmChecked,
- -- See Note [Type and Term Equality Propagation]
- addTyCsDs, addCoreScrutTmCs, addHsScrutTmCs
+ -- See Note [Long-distance information]
+ addTyCs, addCoreScrutTmCs, addHsScrutTmCs
) where
#include "HsVersions.h"
@@ -37,7 +62,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 +86,135 @@ 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:
+-- | 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 <- getPmDeltas
+ 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 collectPatBind ctxt [var] result
+covCheckPatBind _ _ _ = pure ()
- "GADTs Meet Their Match:
- Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
+-- | 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 <- getPmDeltas
+ 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 (collectGRHSs missing) ctxt [] 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
+ missing <- getPmDeltas
+ -- 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 <- getPmNablas
+ 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 collectEmptyCase ctxt vars result
+ Just matches -> do
+ matches <- desugarMatches vars matches
+ result <- unCA (checkMatchGroup matches) missing
+ tracePm "}: " (ppr (cr_uncov result))
+ NE.toList <$> formatReportWarnings (collectMatchGroup missing) ctxt vars 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:
- https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf
+ f :: Void -> ()
+ f x = case x of {}
-%************************************************************************
-%* *
- Pattern Match Check Types
-%* *
-%************************************************************************
+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.
-}
+--
+-- * Guard language
+--
+
-- | A very simple language for pattern guards. Let bindings, bang patterns,
-- and matching variables against flat constructor patterns.
data PmGrd
@@ -106,9 +230,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 +268,118 @@ 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].
+-- | A guard tree denoting 'MatchGroup'.
+newtype GrdMatchGroup = GrdMatchGroup (NonEmpty GrdMatch)
+
+-- | A guard tree denoting 'Match'.
+data GrdMatch = GrdMatch { gm_pats :: ![PmGrd], gm_grhss :: !(NonEmpty GrdGRHS) }
+
+-- | A guard tree denoting 'GRHS'.
+data GrdGRHS = GrdGRHS { gg_grds :: ![PmGrd], gg_rhs :: !SrcInfo }
+
+-- | A guard tree denoting an -XEmptyCase.
+newtype GrdEmptyCase = GrdEmptyCase { ge_var :: Id }
+
+-- | A guard tree denoting a pattern binding.
+newtype GrdPatBind =
+ -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
+ -- rather than on the pattern bindings.
+ GrdPatBind GrdGRHS
+
+-- | 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].
+ }
+
+emptyRedSets :: RedSets
+-- Semigroup instance would be misleading!
+emptyRedSets = RedSets mempty mempty mempty
+
+-- | An annotated tree denoting 'MatchGroup'.
+newtype AnnMatchGroup = AnnMatchGroup (NonEmpty AnnMatch)
+
+-- | An annotated tree denoting 'Match'.
+data AnnMatch = AnnMatch { am_red :: !RedSets, am_grhss :: !(NonEmpty AnnGRHS) }
+
+-- | An annotated tree denoting 'GRHS'.
+data AnnGRHS = AnnGRHS { ag_red :: !RedSets, ag_rhs :: !SrcInfo }
+
+-- | An annotated tree denoting an -XEmptyCase.
+data AnnEmptyCase = AnnEmptyCase
+
+-- | An annotated tree denoting a pattern binding.
+newtype AnnPatBind = AnnPatBind AnnGRHS
+
+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 GrdMatchGroup where
+ ppr (GrdMatchGroup matches) = pprLygSequence matches
+
+instance Outputable GrdMatch where
+ ppr (GrdMatch { gm_pats = grds, gm_grhss = grhss }) =
+ pprLygGuards grds <+> ppr grhss
+
+instance Outputable GrdGRHS where
+ ppr (GrdGRHS { gg_grds = grds, gg_rhs = rhs }) =
+ pprLygGuards grds <+> text "->" <+> pprSrcInfo rhs
+
+instance Outputable GrdPatBind where
+ ppr (GrdPatBind GrdGRHS { gg_grds = grds, gg_rhs = bind }) =
+ ppr bind <+> pprLygGuards grds <+> text "=" <+> text "..."
+
+instance Outputable GrdEmptyCase where
+ ppr (GrdEmptyCase { ge_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 AnnMatchGroup where
+ ppr (AnnMatchGroup matches) = pprLygSequence matches
+
+instance Outputable AnnMatch where
+ ppr (AnnMatch { am_red = red, am_grhss = grhss }) =
+ pprRedSets red <+> ppr grhss
+
+instance Outputable AnnGRHS where
+ ppr (AnnGRHS { ag_red = red, ag_rhs = rhs }) =
+ pprRedSets red <+> text "->" <+> pprSrcInfo rhs
{- Note [Dead bang patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -178,7 +396,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,236 +415,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: covCheckPatBind and covCheckMatchGroup
-%* *
-%************************************************************************
--}
-
--- | Check a pattern binding (let, where) for exhaustiveness.
-covCheckPatBind :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
-covCheckPatBind dflags ctxt@(DsMatchContext _ locn) var p = do
- -- 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.
- -- Given the context in which this function is called, it will only ever do
- -- something for
- -- * PatBindRhs, -Wincomplete-uni-patterns: @let True = False@
- -- * PatBindGuards, -Wincomplete-patterns: @Just x | False = Just 42@
- missing <- getPmDeltas
- tracePm "covCheckPatBind" (vcat [ppr ctxt, ppr var, ppr p, 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.
-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_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)] <- covCheckMatchGroup 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.
-covCheckMatchGroup
- :: 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.
-covCheckMatchGroup ctxt vars matches = do
- tracePm "covCheckMatchGroup" (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
@@ -459,7 +450,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
@@ -477,37 +468,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)
@@ -522,13 +510,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
@@ -536,11 +524,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
@@ -566,7 +554,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"
@@ -595,46 +583,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)
@@ -648,7 +634,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
@@ -659,10 +645,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
@@ -688,77 +674,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 GrdPatBind
+-- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
+desugarPatBind loc var pat =
+ GrdPatBind . flip GrdGRHS (L loc (ppr pat)) <$> desugarPat var pat
+
+desugarEmptyCase :: Id -> DsM GrdEmptyCase
+desugarEmptyCase var = pure GrdEmptyCase { ge_var = var }
+
+-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
+desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
+ -> DsM GrdMatchGroup
+desugarMatches vars matches =
+ GrdMatchGroup <$> traverse (desugarMatch vars) matches
+
+-- Desugar a single match
+desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM GrdMatch
+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 GrdMatch { gm_pats = pats', gm_grhss = grhss' }
+
+desugarGRHSs :: SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty GrdGRHS)
+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 GrdGRHS
+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 GrdGRHS { gg_grds = grds, gg_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
@@ -803,7 +793,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]
@@ -815,52 +805,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))
@@ -875,108 +824,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.
@@ -994,237 +927,241 @@ 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 `add*ScrutTmCs' 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 :: GrdMatchGroup -> CheckAction AnnMatchGroup
+checkMatchGroup (GrdMatchGroup matches) =
+ AnnMatchGroup <$> 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 :: GrdMatch -> CheckAction AnnMatch
+checkMatch (GrdMatch { gm_pats = grds, gm_grhss = grhss }) =
+ leftToRight AnnMatch (checkGrds grds) (checkGRHSs grhss)
--- | 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 locallyExtendPmDelta k $ \deltas ->
- addPmCtsDeltas deltas (unitBag (PmCoreCt x scr))
-addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id"
+checkGRHSs :: NonEmpty GrdGRHS -> CheckAction (NonEmpty AnnGRHS)
+checkGRHSs = checkSequence checkGRHS
--- | '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
+checkGRHS :: GrdGRHS -> CheckAction AnnGRHS
+checkGRHS (GrdGRHS { gg_grds = grds, gg_rhs = rhs_info }) =
+ flip AnnGRHS rhs_info <$> checkGrds grds
-{-
-%************************************************************************
-%* *
- Pretty printing of exhaustiveness/redundancy check warnings
-%* *
-%************************************************************************
--}
+checkEmptyCase :: GrdEmptyCase -> CheckAction AnnEmptyCase
+checkEmptyCase (GrdEmptyCase { ge_var = var }) = CA $ \inc -> do
+ unc <- addPmCtDeltas inc (PmNotBotCt var)
+ pure CheckResult { cr_ret = AnnEmptyCase, cr_uncov = unc, cr_approx = mempty }
--- | 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
+checkPatBind :: GrdPatBind -> CheckAction AnnPatBind
+checkPatBind = coerce checkGRHS
--- | 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 [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.
--- | A type for organising information to be used in warnings.
-data RedundancyInfo
- = RedundancyInfo
- { redundant_rhss :: ![SrcInfo]
- , inaccessible_rhss :: ![SrcInfo]
- , redundant_bangs :: ![Located SDoc]
+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!
+-}
+
+--
+-- * Collecting redundancy information
+--
+
+-- | The result of redundancy checking:
+-- * RHSs classified as /C/overed, /I/naccessible and /R/edundant
+-- * And redundant (B)ang patterns.
+data CIRB
+ = CIRB
+ { cirb_cov :: !(OrdList SrcInfo)
+ , cirb_inacc :: !(OrdList SrcInfo)
+ , cirb_red :: !(OrdList SrcInfo)
+ , cirb_bangs :: !(OrdList SrcInfo)
}
-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 }
+
+-- | A function that walks along an annotated tree @ann@ and extracts two kinds
+-- of coverage info:
+--
+-- 1. A 'CIRB', classifying every encountered RHS in the tree as
+-- redundant, inaccessible or covered.
+-- 2. A piece of long-distance information @ldi@, consisting of a
+-- nesting of 'Deltas' mirroring tree structure.
+-- For example, 'collectMatchGroup' operates on a Match Group and thus
+-- returns a list of 'Deltas' for the pattern part of each Match, as well as
+-- a further nested list of 'Deltas' for each of the GRHS of the Match.
+type CIRBCollector ann ldi = ann -> DsM (CIRB, ldi)
+
+-- | 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. The new inhabited Covered set for long-distance information.
+-- See Note [Recovering from unsatisfiable pattern-matching constraints].
+-- 4. All source bangs whose 'Deltas' were empty, which means they are
+-- redundant.
+testRedSets :: Deltas -> RedSets -> DsM (Bool, Bool, Deltas, OrdList SrcInfo)
+testRedSets ldi 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)
+ -- See Note [Recovering from unsatisfiable pattern-matching constraints]
+ -- Deltas for long-distance info: Use (non-empty!) fallback ldi if Covered
+ -- set was empty
+ let ldi'
+ | is_covered = cov
+ | otherwise = ldi
+ pure (is_covered, may_diverge, ldi', toOL red_bangs)
+
+collectMatchGroup :: Deltas -> CIRBCollector AnnMatchGroup (NonEmpty (Deltas, NonEmpty Deltas))
+collectMatchGroup ldi (AnnMatchGroup matches) = do
+ (cirbs, ldis) <- NE.unzip <$> traverse (collectMatch ldi) matches
+ pure (Semi.sconcat cirbs, ldis)
+
+collectMatch :: Deltas -> CIRBCollector AnnMatch (Deltas, NonEmpty Deltas)
+collectMatch ldi AnnMatch { am_red = red, am_grhss = grhss } = do
+ (is_covered, may_diverge, ldi', red_bangs) <- testRedSets ldi red
+ (cirb, ldis) <- collectGRHSs ldi' grhss
+ let cirb' = addRedundantBangs red_bangs
+ -- See Note [Determining inaccessible clauses]
+ $ applyWhen may_diverge ensureOneNotRedundant
+ $ applyWhen (not is_covered) markAllRedundant
+ $ cirb
+ pure (cirb', (ldi', ldis))
+
+collectGRHSs :: Deltas -> CIRBCollector (NonEmpty AnnGRHS) (NonEmpty Deltas)
+collectGRHSs ldi grhss = do
+ (cirbs, ldis) <- NE.unzip <$> traverse (collectGRHS ldi) grhss
+ pure (Semi.sconcat cirbs, ldis)
+
+collectGRHS :: Deltas -> CIRBCollector AnnGRHS Deltas
+collectGRHS ldi AnnGRHS { ag_red = red, ag_rhs = info } = do
+ (is_covered, may_diverge, ldi', red_bangs) <- testRedSets ldi 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, ldi')
+
+collectEmptyCase :: CIRBCollector AnnEmptyCase ()
+collectEmptyCase _ = pure (mempty, ())
+
+collectPatBind :: CIRBCollector AnnPatBind ()
+-- We don't make use of long-distance information in pattern bindings, hence
+-- @()@ instead of some 'Deltas'.
+collectPatBind (AnnPatBind grhs) = do
+ -- use 'mempty' as fallback 'Deltas' because we discard it anyway
+ (cirb, _) <- collectGRHS mempty grhs
+ pure (cirb, ())
{- Note [Determining inaccessible clauses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1239,26 +1176,30 @@ 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 'CIRBCollector', this function will emit warnings for a
+-- 'CheckResult' and return the collected long-distance information.
+formatReportWarnings :: CIRBCollector ann ldi -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ldi
+formatReportWarnings collect ctx vars cr at CheckResult { cr_ret = ann } = do
+ (cov_info, ldi) <- collect ann
+ dflags <- getDynFlags
+ reportWarnings dflags ctx vars cr{cr_ret=cov_info}
+ pure ldi
+
+-- | 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
@@ -1284,13 +1225,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
@@ -1331,44 +1265,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 =
@@ -1411,18 +1331,151 @@ exhaustiveWarningFlag ThPatQuote = Nothing
-- 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 <- 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
+
+-- | 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 can do better than this, by making sure that the Covered set used for
+Note [Long-distance information] is always inhabited.
+For Covered sets returned by the exported checking functions, that is ensured
+in 'testRedSets', which takes and returns a non-empty fallback 'Deltas' in case
+the refined Covered set became uninhabited.
+Also, whenever "external" knowledge from a type constraint or case scrutinee is
+integrated, we only commit that knowledge to 'GHC.HsToCore.Monad.dsl_deltas' if
+the set remains inhabited. That check happens in 'locallyExtendPmDeltas'.
+-}
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -166,25 +166,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
@@ -1265,7 +1246,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, `covCheckMatchGroup` 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)
=====================================
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
=====================================
@@ -3,10 +3,10 @@
module T18572 where
-True = True
+True = True -- no warning
data SBool (b :: Bool) where
STrue :: SBool True
SFalse :: SBool False
-STrue = SFalse
+STrue = SFalse -- "redundant", not "inaccessible"
=====================================
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/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/-/commit/65d51d90902b5aa1522ac6e8113ef999be4c1f7e
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/65d51d90902b5aa1522ac6e8113ef999be4c1f7e
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/20200831/273e5864/attachment-0001.html>
More information about the ghc-commits
mailing list