[Git][ghc/ghc][wip/T18533] PmCheck: Better long-distance info for where bindings (#18533)
Sebastian Graf
gitlab at gitlab.haskell.org
Tue Aug 11 18:06:23 UTC 2020
Sebastian Graf pushed to branch wip/T18533 at Glasgow Haskell Compiler / GHC
Commits:
19e9c8e3 by Sebastian Graf at 2020-08-11T20:06:14+02:00
PmCheck: Better long-distance info for where bindings (#18533)
Where bindings can see evidence from the pattern match of the `GRHSs`
they belong to, but not from anything in any of the guards (which belong
to one of possibly many RHSs).
Before this patch, we did *not* consider said evidence, causing #18533,
where the lack of considering type information from a case pattern match
leads to failure to resolve the vanilla COMPLETE set of a data type.
Making available that information required a medium amount of
refactoring so that `checkMatches` can return a
`[(Deltas, NonEmpty Deltas)]`; one `(Deltas, NonEmpty Deltas)` for each
`GRHSs` of the match group. The first component of the pair is the
covered set of the pattern, the second component is one covered set per
RHS.
Fixes #18533.
Regression test case: T18533
- - - - -
9 changed files:
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/GuardedRHSs.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- + testsuite/tests/pmcheck/should_compile/T18533.hs
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
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, checkGuardMatches )
+import GHC.HsToCore.PmCheck ( addTyCsDs, checkGRHSs )
import GHC.Hs -- lots of things
import GHC.Core -- lots of things
@@ -76,7 +76,6 @@ import GHC.Types.Unique.Set( nonDetEltsUniqSet )
import GHC.Utils.Monad
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
-import Data.List.NonEmpty ( nonEmpty )
{-**********************************************************************
* *
@@ -183,8 +182,8 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss
, pat_ext = NPatBindTc _ ty
, pat_ticks = (rhs_tick, var_ticks) })
- = do { rhss_deltas <- checkGuardMatches PatBindGuards grhss
- ; body_expr <- dsGuarded grhss ty (nonEmpty rhss_deltas)
+ = do { rhss_deltas <- checkGRHSs PatBindGuards grhss
+ ; body_expr <- dsGuarded grhss ty rhss_deltas
; let body' = mkOptTickBox rhs_tick body_expr
pat' = decideBangHood dflags pat
; (force_var,sel_binds) <- mkSelectorBinds var_ticks pat body'
=====================================
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, checkGuardMatches )
+import GHC.HsToCore.PmCheck ( addTyCsDs, checkGRHSs )
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Core.FamInstEnv( topNormaliseType )
@@ -69,7 +69,6 @@ import GHC.Utils.Outputable as Outputable
import GHC.Core.PatSyn
import Control.Monad
-import Data.List.NonEmpty ( nonEmpty )
{-
************************************************************************
@@ -215,8 +214,8 @@ dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss
, pat_ext = NPatBindTc _ ty }) body
= -- let C x# y# = rhs in body
-- ==> case rhs of C x# y# -> body
- do { rhs_deltas <- checkGuardMatches PatBindGuards grhss
- ; rhs <- dsGuarded grhss ty (nonEmpty rhs_deltas)
+ do { match_deltas <- checkGRHSs PatBindGuards grhss
+ ; rhs <- dsGuarded grhss ty match_deltas
; let upat = unLoc pat
eqn = EqnInfo { eqn_pats = [upat],
eqn_orig = FromSource,
@@ -486,8 +485,8 @@ dsExpr (HsMultiIf res_ty alts)
| otherwise
= do { let grhss = GRHSs noExtField alts (noLoc emptyLocalBinds)
- ; rhss_deltas <- checkGuardMatches IfAlt grhss
- ; match_result <- dsGRHSs IfAlt grhss res_ty (nonEmpty rhss_deltas)
+ ; rhss_deltas <- checkGRHSs IfAlt grhss
+ ; match_result <- dsGRHSs IfAlt grhss res_ty rhss_deltas
; error_expr <- mkErrorExpr
; extractMatchResult match_result error_expr }
where
=====================================
compiler/GHC/HsToCore/GuardedRHSs.hs
=====================================
@@ -25,7 +25,7 @@ import GHC.Core.Utils (bindNonRec)
import GHC.HsToCore.Monad
import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck.Types ( Deltas, initDeltas )
+import GHC.HsToCore.PmCheck.Types ( Deltas )
import GHC.Core.Type ( Type )
import GHC.Utils.Misc
import GHC.Types.SrcLoc
@@ -47,9 +47,9 @@ producing an expression with a runtime error in the corner if
necessary. The type argument gives the type of the @ei at .
-}
-dsGuarded :: GRHSs GhcTc (LHsExpr GhcTc) -> Type -> Maybe (NonEmpty Deltas) -> DsM CoreExpr
-dsGuarded grhss rhs_ty mb_rhss_deltas = do
- match_result <- dsGRHSs PatBindRhs grhss rhs_ty mb_rhss_deltas
+dsGuarded :: GRHSs GhcTc (LHsExpr GhcTc) -> Type -> NonEmpty Deltas -> DsM CoreExpr
+dsGuarded grhss rhs_ty rhss_deltas = do
+ match_result <- dsGRHSs PatBindRhs grhss rhs_ty rhss_deltas
error_expr <- mkErrorAppDs nON_EXHAUSTIVE_GUARDS_ERROR_ID rhs_ty empty
extractMatchResult match_result error_expr
@@ -58,25 +58,28 @@ dsGuarded grhss rhs_ty mb_rhss_deltas = do
dsGRHSs :: HsMatchContext GhcRn
-> GRHSs GhcTc (LHsExpr GhcTc) -- ^ Guarded RHSs
-> Type -- ^ Type of RHS
- -> Maybe (NonEmpty Deltas) -- ^ Refined pattern match checking
- -- models, one for each GRHS. Defaults
- -- to 'initDeltas' if 'Nothing'.
+ -> NonEmpty Deltas -- ^ Refined pattern match checking
+ -- models, one for the pattern part and
+ -- one for each GRHS.
-> DsM (MatchResult CoreExpr)
-dsGRHSs hs_ctx (GRHSs _ grhss binds) rhs_ty mb_rhss_deltas
+dsGRHSs hs_ctx (GRHSs _ grhss binds) rhs_ty rhss_deltas
= ASSERT( notNull grhss )
- do { match_results <- case toList <$> mb_rhss_deltas of
- Nothing -> mapM (dsGRHS hs_ctx rhs_ty initDeltas) grhss
- Just rhss_deltas -> ASSERT( length grhss == length rhss_deltas )
- zipWithM (dsGRHS hs_ctx rhs_ty) rhss_deltas grhss
- ; let match_result1 = foldr1 combineMatchResults match_results
- match_result2 = adjustMatchResultDs (dsLocalBinds binds) match_result1
+ do { match_results <- ASSERT( length grhss == length rhss_deltas )
+ zipWithM (dsGRHS hs_ctx rhs_ty) (toList rhss_deltas) grhss
+ ; deltas <- getPmDeltas
+ -- We need to remember the Deltas from the particular match context we
+ -- are in, which might be different to when dsLocalBinds is actually
+ -- called.
+ ; let ds_binds = updPmDeltas deltas . dsLocalBinds binds
+ match_result1 = foldr1 combineMatchResults match_results
+ match_result2 = adjustMatchResultDs ds_binds match_result1
-- NB: nested dsLet inside matchResult
; return match_result2 }
dsGRHS :: HsMatchContext GhcRn -> Type -> Deltas -> LGRHS GhcTc (LHsExpr GhcTc)
-> DsM (MatchResult CoreExpr)
dsGRHS hs_ctx rhs_ty rhs_deltas (L _ (GRHS _ guards rhs))
- = updPmDeltas rhs_deltas (matchGuards (map unLoc guards) (PatGuard hs_ctx) rhs rhs_ty)
+ = matchGuards (map unLoc guards) (PatGuard hs_ctx) rhs_deltas rhs rhs_ty
{-
************************************************************************
@@ -88,6 +91,7 @@ dsGRHS hs_ctx rhs_ty rhs_deltas (L _ (GRHS _ guards rhs))
matchGuards :: [GuardStmt GhcTc] -- Guard
-> HsStmtContext GhcRn -- Context
+ -> Deltas -- The RHS's covered set for PmCheck
-> LHsExpr GhcTc -- RHS
-> Type -- Type of RHS of guard
-> DsM (MatchResult CoreExpr)
@@ -95,8 +99,8 @@ matchGuards :: [GuardStmt GhcTc] -- Guard
-- See comments with HsExpr.Stmt re what a BodyStmt means
-- Here we must be in a guard context (not do-expression, nor list-comp)
-matchGuards [] _ rhs _
- = do { core_rhs <- dsLExpr rhs
+matchGuards [] _ deltas rhs _
+ = do { core_rhs <- updPmDeltas deltas (dsLExpr rhs)
; return (cantFailMatchResult core_rhs) }
-- BodyStmts must be guards
@@ -106,41 +110,41 @@ matchGuards [] _ rhs _
-- NB: The success of this clause depends on the typechecker not
-- wrapping the 'otherwise' in empty HsTyApp or HsWrap constructors
-- If it does, you'll get bogus overlap warnings
-matchGuards (BodyStmt _ e _ _ : stmts) ctx rhs rhs_ty
+matchGuards (BodyStmt _ e _ _ : stmts) ctx deltas rhs rhs_ty
| Just addTicks <- isTrueLHsExpr e = do
- match_result <- matchGuards stmts ctx rhs rhs_ty
+ match_result <- matchGuards stmts ctx deltas rhs rhs_ty
return (adjustMatchResultDs addTicks match_result)
-matchGuards (BodyStmt _ expr _ _ : stmts) ctx rhs rhs_ty = do
- match_result <- matchGuards stmts ctx rhs rhs_ty
+matchGuards (BodyStmt _ expr _ _ : stmts) ctx deltas rhs rhs_ty = do
+ match_result <- matchGuards stmts ctx deltas rhs rhs_ty
pred_expr <- dsLExpr expr
return (mkGuardedMatchResult pred_expr match_result)
-matchGuards (LetStmt _ binds : stmts) ctx rhs rhs_ty = do
- match_result <- matchGuards stmts ctx rhs rhs_ty
+matchGuards (LetStmt _ binds : stmts) ctx deltas rhs rhs_ty = do
+ match_result <- matchGuards stmts ctx deltas rhs rhs_ty
return (adjustMatchResultDs (dsLocalBinds binds) match_result)
-- NB the dsLet occurs inside the match_result
-- Reason: dsLet takes the body expression as its argument
-- so we can't desugar the bindings without the
-- body expression in hand
-matchGuards (BindStmt _ pat bind_rhs : stmts) ctx rhs rhs_ty = do
+matchGuards (BindStmt _ pat bind_rhs : stmts) ctx deltas rhs rhs_ty = do
let upat = unLoc pat
match_var <- selectMatchVar Many upat
-- We only allow unrestricted patterns in guard, hence the `Many`
-- above. It isn't clear what linear patterns would mean, maybe we will
-- figure it out in the future.
- match_result <- matchGuards stmts ctx rhs rhs_ty
+ match_result <- matchGuards stmts ctx deltas rhs rhs_ty
core_rhs <- dsLExpr bind_rhs
match_result' <- matchSinglePatVar match_var (StmtCtxt ctx) pat rhs_ty
match_result
pure $ bindNonRec match_var core_rhs <$> match_result'
-matchGuards (LastStmt {} : _) _ _ _ = panic "matchGuards LastStmt"
-matchGuards (ParStmt {} : _) _ _ _ = panic "matchGuards ParStmt"
-matchGuards (TransStmt {} : _) _ _ _ = panic "matchGuards TransStmt"
-matchGuards (RecStmt {} : _) _ _ _ = panic "matchGuards RecStmt"
-matchGuards (ApplicativeStmt {} : _) _ _ _ =
+matchGuards (LastStmt {} : _) _ _ _ _ = panic "matchGuards LastStmt"
+matchGuards (ParStmt {} : _) _ _ _ _ = panic "matchGuards ParStmt"
+matchGuards (TransStmt {} : _) _ _ _ _ = panic "matchGuards TransStmt"
+matchGuards (RecStmt {} : _) _ _ _ _ = panic "matchGuards RecStmt"
+matchGuards (ApplicativeStmt {} : _) _ _ _ _ =
panic "matchGuards ApplicativeLastStmt"
{-
=====================================
compiler/GHC/HsToCore/Match.hs
=====================================
@@ -35,6 +35,7 @@ import GHC.Tc.Utils.Zonk
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.Monad
import GHC.HsToCore.PmCheck
+import GHC.HsToCore.PmCheck.Types ( Deltas, initDeltas )
import GHC.Core
import GHC.Types.Literal
import GHC.Core.Utils
@@ -64,7 +65,7 @@ import GHC.Data.FastString
import GHC.Types.Unique
import GHC.Types.Unique.DFM
-import Control.Monad( unless )
+import Control.Monad(zipWithM, unless )
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NEL
import qualified Data.Map as Map
@@ -766,49 +767,46 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
-- Pattern match check warnings for /this match-group/.
-- @rhss_deltas@ is a flat list of covered Deltas for each RHS.
-- Each Match will split off one Deltas for its RHSs from this.
- ; rhss_deltas <- if isMatchContextPmChecked dflags origin ctxt
+ ; matches_deltas <- if isMatchContextPmChecked dflags origin ctxt
then addScrutTmCs mb_scr new_vars $
- -- See Note [Type and Term Equality Propagation]
- checkMatches (DsMatchContext ctxt locn) new_vars matches
- else pure [] -- Ultimately this will result in passing Nothing
- -- to dsGRHSs as match_deltas
+ -- See Note [Type and Term Equality Propagation]
+ checkMatches (DsMatchContext ctxt locn) new_vars matches
+ else pure (initDeltasMatches matches)
- ; eqns_info <- mk_eqn_infos matches rhss_deltas
+ ; eqns_info <- zipWithM mk_eqn_info matches matches_deltas
; result_expr <- handleWarnings $
matchEquations ctxt new_vars eqns_info rhs_ty
; return (new_vars, result_expr) }
where
- -- rhss_deltas is a flat list, whereas there are multiple GRHSs per match.
- -- mk_eqn_infos will thread rhss_deltas as state through calls to
- -- mk_eqn_info, distributing each rhss_deltas to a GRHS.
- mk_eqn_infos (L _ match : matches) rhss_deltas
- = do { (info, rhss_deltas') <- mk_eqn_info match rhss_deltas
- ; infos <- mk_eqn_infos matches rhss_deltas'
- ; return (info:infos) }
- mk_eqn_infos [] _ = return []
-- Called once per equation in the match, or alternative in the case
- mk_eqn_info (Match { m_pats = pats, m_grhss = grhss }) rhss_deltas
- | GRHSs _ grhss' _ <- grhss, let n_grhss = length grhss'
+ mk_eqn_info :: LMatch GhcTc (LHsExpr GhcTc) -> (Deltas, NonEmpty Deltas) -> DsM EquationInfo
+ mk_eqn_info (L _ (Match { m_pats = pats, m_grhss = grhss })) (pat_deltas, rhss_deltas)
= do { dflags <- getDynFlags
; let upats = map (unLoc . decideBangHood dflags) pats
- -- Split off one Deltas for each GRHS of the current Match from the
- -- flat list of GRHS Deltas *for all matches* (see the call to
- -- checkMatches above).
- ; let (match_deltas, rhss_deltas') = splitAt n_grhss rhss_deltas
- -- The list of Deltas is empty iff we don't perform any coverage
- -- checking, in which case nonEmpty does the right thing by passing
- -- Nothing.
- ; match_result <- dsGRHSs ctxt grhss rhs_ty (NEL.nonEmpty match_deltas)
- ; return ( EqnInfo { eqn_pats = upats
- , eqn_orig = FromSource
- , eqn_rhs = match_result }
- , rhss_deltas' ) }
+ -- pat_deltas is the covered set *after* matching the pattern, but
+ -- before any of the GRHSs. It is the evidence that is visible in
+ -- the associated where clauses of the match.
+ ; match_result <- updPmDeltas pat_deltas $
+ dsGRHSs ctxt grhss rhs_ty rhss_deltas
+ ; return EqnInfo { eqn_pats = upats
+ , eqn_orig = FromSource
+ , eqn_rhs = match_result } }
handleWarnings = if isGenerated origin
then discardWarningsDs
else id
+ initDeltasMatches :: [LMatch GhcTc b] -> [(Deltas, NonEmpty Deltas)]
+ initDeltasMatches ms
+ = map (\(L _ m) -> (initDeltas, initDeltasGRHSs (m_grhss m))) ms
+
+ initDeltasGRHSs :: GRHSs GhcTc b -> NonEmpty Deltas
+ initDeltasGRHSs m = expectJust "GRHSs non-empty"
+ $ NEL.nonEmpty
+ $ replicate (length (grhssGRHSs m)) initDeltas
+
+
matchEquations :: HsMatchContext GhcRn
-> [MatchId] -> [EquationInfo] -> Type
-> DsM CoreExpr
=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -405,7 +405,7 @@ getPmDeltas = do { env <- getLclEnv; return (dsl_deltas env) }
-- | Set the pattern match oracle state within the scope of the given action.
-- See 'dsl_deltas'.
updPmDeltas :: Deltas -> DsM a -> DsM a
-updPmDeltas delta = updLclEnv (\env -> env { dsl_deltas = delta })
+updPmDeltas deltas = updLclEnv (\env -> env { dsl_deltas = deltas })
getSrcSpanDs :: DsM SrcSpan
getSrcSpanDs = do { env <- getLclEnv
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -13,7 +13,7 @@ Pattern Matching Coverage Checking.
module GHC.HsToCore.PmCheck (
-- Checking and printing
- checkSingle, checkMatches, checkGuardMatches,
+ checkSingle, checkMatches, checkGRHSs,
isMatchContextPmChecked,
-- See Note [Type and Term Equality Propagation]
@@ -65,6 +65,7 @@ import GHC.Utils.Monad (concatMapM)
import Control.Monad (when, forM_, zipWithM)
import Data.List (elemIndex)
import qualified Data.Semigroup as Semi
+import Data.List.NonEmpty (NonEmpty(..))
{-
This module checks pattern matches for:
@@ -149,13 +150,11 @@ data 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 !GrdTree
- -- ^ @Sequence l r@ first matches against @l@, and then matches all
- -- fallen-through values against @r at . Models top-to-bottom semantics of
- -- pattern matching.
- | Empty
- -- ^ A @GrdTree@ that always fails. Most useful for
- -- Note [Checking EmptyCase]. A neutral element to 'Sequence'.
+ | 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].
-- | The digest of 'checkGrdTree', representing the annotated pattern-match
-- tree. 'redundantAndInaccessibleRhss' can figure out redundant and proper
@@ -169,10 +168,10 @@ data AnnotatedTree
| MayDiverge !AnnotatedTree
-- ^ Asserts that the tree may force diverging values, so not all of its
-- clauses can be redundant.
- | SequenceAnn !AnnotatedTree !AnnotatedTree
- -- ^ Mirrors 'Sequence' for preserving the skeleton of a 'GrdTree's.
- | EmptyAnn
- -- ^ Mirrors 'Empty' for preserving the skeleton of a 'GrdTree's.
+ | 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 .
pprRhsInfo :: RhsInfo -> SDoc
pprRhsInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
@@ -188,23 +187,15 @@ instance Outputable GrdTree where
collect_grds t = (t, [])
prefix [] = []
prefix (s:sdocs) = char '|' <+> s : map (comma <+>) sdocs
- -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
- ppr t at Sequence{} = braces (space <> fsep (punctuate semi (collect_seqs t)) <> space)
- where
- collect_seqs (Sequence l r) = collect_seqs l ++ collect_seqs r
- collect_seqs t = [ppr t]
- ppr Empty = text "<empty case>"
+ ppr (Sequence []) = text "<empty case>"
+ ppr (Sequence ts) = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
instance Outputable AnnotatedTree where
- ppr (AccessibleRhs _ info) = pprRhsInfo info
+ ppr (AccessibleRhs _delta info) = parens (ppr _delta) <+> pprRhsInfo info
ppr (InaccessibleRhs info) = text "inaccessible" <+> pprRhsInfo info
ppr (MayDiverge t) = text "div" <+> ppr t
- -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
- ppr t at SequenceAnn{} = braces (space <> fsep (punctuate semi (collect_seqs t)) <> space)
- where
- collect_seqs (SequenceAnn l r) = collect_seqs l ++ collect_seqs r
- collect_seqs t = [ppr t]
- ppr EmptyAnn = text "<empty case>"
+ ppr (SequenceAnn _ []) = text "<empty case>"
+ ppr (SequenceAnn _ ts) = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
-- | Lift 'addPmCts' over 'Deltas'.
addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
@@ -263,7 +254,7 @@ checkSingle dflags ctxt@(DsMatchContext kind locn) var p = do
-- Omitting checking this flag emits redundancy warnings twice in obscure
-- cases like #17646.
when (exhaustive dflags kind) $ do
- -- TODO: This could probably call checkMatches, like checkGuardMatches.
+ -- TODO: This could probably call checkMatches, like checkGRHSs.
missing <- getPmDeltas
tracePm "checkSingle: missing" (ppr missing)
fam_insts <- dsGetFamInstEnvs
@@ -273,12 +264,12 @@ checkSingle dflags ctxt@(DsMatchContext kind locn) var p = do
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs.
-checkGuardMatches
+checkGRHSs
:: HsMatchContext GhcRn -- ^ Match context, for warning messages
-> GRHSs GhcTc (LHsExpr GhcTc) -- ^ The GRHSs to check
- -> DsM [Deltas] -- ^ Covered 'Deltas' for each RHS, for long
+ -> DsM (NonEmpty Deltas) -- ^ Covered 'Deltas' for each RHS, for long
-- distance info
-checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
+checkGRHSs hs_ctx guards@(GRHSs _ grhss _) = do
let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
dsMatchContext = DsMatchContext hs_ctx combinedLoc
match = L combinedLoc $
@@ -286,7 +277,8 @@ checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
, m_ctxt = hs_ctx
, m_pats = []
, m_grhss = guards }
- checkMatches dsMatchContext [] [match]
+ [(_, deltas)] <- checkMatches dsMatchContext [] [match]
+ pure deltas
-- | Check a list of syntactic /match/es (part of case, functions, etc.), each
-- with a /pat/ and one or more /grhss/:
@@ -305,10 +297,9 @@ checkMatches
:: DsMatchContext -- ^ Match context, for warnings messages
-> [Id] -- ^ Match variables, i.e. x and y above
-> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches
- -> DsM [Deltas] -- ^ One covered 'Deltas' per RHS, for long
+ -> DsM [(Deltas, NonEmpty Deltas)] -- ^ One covered 'Deltas' per RHS, for long
-- distance info.
checkMatches ctxt vars matches = do
- dflags <- getDynFlags
tracePm "checkMatches" (hang (vcat [ppr ctxt
, ppr vars
, text "Matches:"])
@@ -321,25 +312,45 @@ checkMatches ctxt vars matches = do
[] | [var] <- vars -> addPmCtDeltas init_deltas (PmNotBotCt var)
_ -> pure init_deltas
fam_insts <- dsGetFamInstEnvs
- grd_tree <- mkGrdTreeMany [] <$> mapM (translateMatch fam_insts vars) matches
+ grd_tree <- translateMatches fam_insts vars matches
res <- checkGrdTree grd_tree missing
+ dflags <- getDynFlags
dsPmWarn dflags ctxt vars res
- return (extractRhsDeltas init_deltas (cr_clauses res))
+ return (extractRhsDeltas (cr_clauses res))
--- | Extract the 'Deltas' reaching the RHSs of the 'AnnotatedTree'.
+-- | 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 :: Deltas -> AnnotatedTree -> [Deltas]
-extractRhsDeltas orig_deltas = fromOL . go
+extractRhsDeltas :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
+extractRhsDeltas = go_matches
where
- go (AccessibleRhs deltas _) = unitOL deltas
- go (InaccessibleRhs _) = unitOL orig_deltas
- go (MayDiverge t) = go t
- go (SequenceAnn l r) = go l Semi.<> go r
- go EmptyAnn = nilOL
+ 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
+ -- 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 _ (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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -628,34 +639,43 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
-- 1. 2. 3.
pure (con_grd : bang_grds ++ arg_grds)
-mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
-mkGrdTreeRhs sdoc = foldr Guard (Rhs sdoc)
-
-mkGrdTreeMany :: GrdVec -> [GrdTree] -> GrdTree
-mkGrdTreeMany _ [] = Empty
-mkGrdTreeMany grds trees = foldr Guard (foldr1 Sequence trees) 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' <- mapM (translateLGRHS fam_insts match_loc pats) (grhssGRHSs grhss)
- -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss, ppr grhss'])
- return (mkGrdTreeMany pats' grhss')
+ 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')
--- -----------------------------------------------------------------------
--- * Transform source guards (GuardStmt Id) to simpler PmGrds
+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 -> [LPat GhcTc] -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
-translateLGRHS fam_insts match_loc pats (L _loc (GRHS _ gs _)) =
- -- _loc apparently points to the match separator that comes after the guards..
+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
- | null gs = L match_loc (sep (map ppr pats))
- | otherwise = L grd_loc (sep (map ppr pats) <+> vbar <+> interpp'SP gs)
+ -- 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'
@@ -970,6 +990,7 @@ checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
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)
@@ -978,19 +999,21 @@ checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
, cr_uncov = unc'
, cr_approx = prec Semi.<> prec' }
-- Sequence: Thread residual uncovered sets from equation to equation
-checkGrdTree' (Sequence l r) unc_0 = do
- CheckResult l' unc_1 prec_l <- checkGrdTree' l unc_0
- CheckResult r' unc_2 prec_r <- checkGrdTree' r unc_1
- pure CheckResult
- { cr_clauses = SequenceAnn l' r'
- , cr_uncov = unc_2
- , cr_approx = prec_l Semi.<> prec_r }
--- Empty: Fall through for all values
-checkGrdTree' Empty unc = do
- pure CheckResult
- { cr_clauses = EmptyAnn
- , cr_uncov = unc
- , cr_approx = Precise }
+checkGrdTree' (Sequence ts) init_unc = go [] init_unc Precise ts
+ 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
@@ -1116,8 +1139,7 @@ redundantAndInaccessibleRhss tree = (fromOL ol_red, fromOL ol_inacc)
(acc, inacc, red)
| isNilOL acc && isNilOL inacc -> (nilOL, red, nilOL)
res -> res
- go (SequenceAnn l r) = go l Semi.<> go r
- go EmptyAnn = (nilOL, nilOL, nilOL)
+ go (SequenceAnn _ ts) = foldMap go ts
{- Note [Determining inaccessible clauses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -1069,7 +1069,8 @@ ensureAllPossibleMatchesInhabited delta at MkDelta{ delta_tm_st = TmSt env reps }
= runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env)
where
set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env reps }
- go vi = MaybeT (ensureInhabited delta vi)
+ go vi = MaybeT $
+ initPossibleMatches (delta_ty_st delta) vi >>= ensureInhabited delta
--------------------------------------
-- * Term oracle unification procedure
@@ -1667,7 +1668,7 @@ addCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
addCoreCt delta x e = do
dflags <- getDynFlags
let e' = simpleOptExpr dflags e
- lift $ tracePm "addCoreCt" (ppr x $$ ppr e $$ ppr e')
+ lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
execStateT (core_expr x e') delta
where
-- | Takes apart a 'CoreExpr' and tries to extract as much information about
=====================================
testsuite/tests/pmcheck/should_compile/T18533.hs
=====================================
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE GADTs, DataKinds, TypeFamilies, BangPatterns #-}
+
+module T18533 where
+
+data SBool (b :: Bool) where
+ STrue :: SBool 'True
+ SFalse :: SBool 'False
+
+type family Fam (b :: Bool)
+type instance Fam 'True = T
+
+data T = T Bool
+
+f :: Fam b -> SBool b -> Bool
+f !t s = case s of
+ STrue -> a where a = case t of T a -> a
+ _ -> False
+
+
+g :: Bool -> Bool
+g x = case x of
+ True -> a where a = case x of True -> False
+ False -> True
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -122,6 +122,8 @@ test('T18049', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18478', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18533', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/19e9c8e3932a0a7d30c1024640b3b65ca89a2c44
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/19e9c8e3932a0a7d30c1024640b3b65ca89a2c44
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/20200811/cfab0b17/attachment-0001.html>
More information about the ghc-commits
mailing list