diff options
| author | Sebastian Graf <sebastian.graf@kit.edu> | 2020-07-01 15:48:41 +0200 |
|---|---|---|
| committer | Sebastian Graf <sebastian.graf@kit.edu> | 2020-09-10 17:03:12 +0200 |
| commit | 3777be14e104f040b826762f5ab42a8b898d85ae (patch) | |
| tree | 1af2c1cc113db6f142486c111ca467bb8b7195a4 /compiler/GHC/HsToCore | |
| parent | 6abe4a1c427a511aa698424055639ea789fccf97 (diff) | |
| download | haskell-wip/T18341.tar.gz | |
PmCheck: Handle ⊥ and strict fields correctly (#18341)wip/T18341
In #18341, we discovered an incorrect digression from Lower Your Guards.
This MR changes what's necessary to support properly fixing #18341.
In particular, bottomness constraints are now properly tracked in the
oracle/inhabitation testing, as an additional field
`vi_bot :: Maybe Bool` in `VarInfo`. That in turn allows us to
model newtypes as advertised in the Appendix of LYG and fix #17725.
Proper handling of ⊥ also fixes #17977 (once again) and fixes #18670.
For some reason I couldn't follow, this also fixes #18273.
I also added a couple of regression tests that were missing. Most of
them were already fixed before.
In summary, this patch fixes #18341, #17725, #18273, #17977 and #18670.
Metric Decrease:
T12227
Diffstat (limited to 'compiler/GHC/HsToCore')
| -rw-r--r-- | compiler/GHC/HsToCore/Binds.hs | 4 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/Expr.hs | 8 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/GuardedRHSs.hs | 50 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/Match.hs | 38 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/Monad.hs | 16 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck.hs | 266 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Oracle.hs | 538 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Ppr.hs | 50 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Types.hs | 88 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Types.hs-boot | 6 |
10 files changed, 572 insertions, 492 deletions
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs index b83c228d27..3adecc0d5b 100644 --- a/compiler/GHC/HsToCore/Binds.hs +++ b/compiler/GHC/HsToCore/Binds.hs @@ -185,8 +185,8 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss , pat_ext = ty , pat_ticks = (rhs_tick, var_ticks) }) - = do { rhss_deltas <- covCheckGRHSs PatBindGuards grhss - ; body_expr <- dsGuarded grhss ty rhss_deltas + = do { rhss_nablas <- covCheckGRHSs PatBindGuards grhss + ; body_expr <- dsGuarded grhss ty rhss_nablas ; let body' = mkOptTickBox rhs_tick body_expr pat' = decideBangHood dflags pat ; (force_var,sel_binds) <- mkSelectorBinds var_ticks pat body' diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index 05bb46bfbe..671e525bb1 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -215,8 +215,8 @@ dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss , pat_ext = ty }) body = -- let C x# y# = rhs in body -- ==> case rhs of C x# y# -> body - do { match_deltas <- covCheckGRHSs PatBindGuards grhss - ; rhs <- dsGuarded grhss ty match_deltas + do { match_nablas <- covCheckGRHSs PatBindGuards grhss + ; rhs <- dsGuarded grhss ty match_nablas ; let upat = unLoc pat eqn = EqnInfo { eqn_pats = [upat], eqn_orig = FromSource, @@ -486,8 +486,8 @@ dsExpr (HsMultiIf res_ty alts) | otherwise = do { let grhss = GRHSs noExtField alts (noLoc emptyLocalBinds) - ; rhss_deltas <- covCheckGRHSs IfAlt grhss - ; match_result <- dsGRHSs IfAlt grhss res_ty rhss_deltas + ; rhss_nablas <- covCheckGRHSs IfAlt grhss + ; match_result <- dsGRHSs IfAlt grhss res_ty rhss_nablas ; error_expr <- mkErrorExpr ; extractMatchResult match_result error_expr } where diff --git a/compiler/GHC/HsToCore/GuardedRHSs.hs b/compiler/GHC/HsToCore/GuardedRHSs.hs index 55ede1ddcb..14b01f440a 100644 --- a/compiler/GHC/HsToCore/GuardedRHSs.hs +++ b/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 ) +import GHC.HsToCore.PmCheck.Types ( Nablas ) import GHC.Core.Type ( Type ) import GHC.Utils.Misc import GHC.Types.SrcLoc @@ -48,9 +48,9 @@ producing an expression with a runtime error in the corner case if necessary. The type argument gives the type of the @ei@. -} -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 +dsGuarded :: GRHSs GhcTc (LHsExpr GhcTc) -> Type -> NonEmpty Nablas -> DsM CoreExpr +dsGuarded grhss rhs_ty rhss_nablas = do + match_result <- dsGRHSs PatBindRhs grhss rhs_ty rhss_nablas error_expr <- mkErrorAppDs nON_EXHAUSTIVE_GUARDS_ERROR_ID rhs_ty empty extractMatchResult match_result error_expr @@ -59,28 +59,28 @@ dsGuarded grhss rhs_ty rhss_deltas = do dsGRHSs :: HsMatchContext GhcRn -> GRHSs GhcTc (LHsExpr GhcTc) -- ^ Guarded RHSs -> Type -- ^ Type of RHS - -> NonEmpty Deltas -- ^ Refined pattern match checking + -> NonEmpty Nablas -- ^ 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 rhss_deltas +dsGRHSs hs_ctx (GRHSs _ grhss binds) rhs_ty rhss_nablas = ASSERT( notNull grhss ) - 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 + do { match_results <- ASSERT( length grhss == length rhss_nablas ) + zipWithM (dsGRHS hs_ctx rhs_ty) (toList rhss_nablas) grhss + ; nablas <- getPmNablas + -- We need to remember the Nablas 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 + ; let ds_binds = updPmNablas nablas . 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) +dsGRHS :: HsMatchContext GhcRn -> Type -> Nablas -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM (MatchResult CoreExpr) -dsGRHS hs_ctx rhs_ty rhs_deltas (L _ (GRHS _ guards rhs)) - = matchGuards (map unLoc guards) (PatGuard hs_ctx) rhs_deltas rhs rhs_ty +dsGRHS hs_ctx rhs_ty rhs_nablas (L _ (GRHS _ guards rhs)) + = matchGuards (map unLoc guards) (PatGuard hs_ctx) rhs_nablas rhs rhs_ty {- ************************************************************************ @@ -92,7 +92,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 + -> Nablas -- The RHS's covered set for PmCheck -> LHsExpr GhcTc -- RHS -> Type -- Type of RHS of guard -> DsM (MatchResult CoreExpr) @@ -100,8 +100,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 [] _ deltas rhs _ - = do { core_rhs <- updPmDeltas deltas (dsLExpr rhs) +matchGuards [] _ nablas rhs _ + = do { core_rhs <- updPmNablas nablas (dsLExpr rhs) ; return (cantFailMatchResult core_rhs) } -- BodyStmts must be guards @@ -111,31 +111,31 @@ matchGuards [] _ deltas 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 deltas rhs rhs_ty +matchGuards (BodyStmt _ e _ _ : stmts) ctx nablas rhs rhs_ty | Just addTicks <- isTrueLHsExpr e = do - match_result <- matchGuards stmts ctx deltas rhs rhs_ty + match_result <- matchGuards stmts ctx nablas rhs rhs_ty return (adjustMatchResultDs addTicks match_result) -matchGuards (BodyStmt _ expr _ _ : stmts) ctx deltas rhs rhs_ty = do - match_result <- matchGuards stmts ctx deltas rhs rhs_ty +matchGuards (BodyStmt _ expr _ _ : stmts) ctx nablas rhs rhs_ty = do + match_result <- matchGuards stmts ctx nablas rhs rhs_ty pred_expr <- dsLExpr expr return (mkGuardedMatchResult pred_expr match_result) -matchGuards (LetStmt _ binds : stmts) ctx deltas rhs rhs_ty = do - match_result <- matchGuards stmts ctx deltas rhs rhs_ty +matchGuards (LetStmt _ binds : stmts) ctx nablas rhs rhs_ty = do + match_result <- matchGuards stmts ctx nablas 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 deltas rhs rhs_ty = do +matchGuards (BindStmt _ pat bind_rhs : stmts) ctx nablas 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 deltas rhs rhs_ty + match_result <- matchGuards stmts ctx nablas rhs rhs_ty core_rhs <- dsLExpr bind_rhs match_result' <- matchSinglePatVar match_var (Just core_rhs) (StmtCtxt ctx) pat rhs_ty match_result diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs index eeca77cd5d..a33e3d9b41 100644 --- a/compiler/GHC/HsToCore/Match.hs +++ b/compiler/GHC/HsToCore/Match.hs @@ -35,7 +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.HsToCore.PmCheck.Types ( Nablas, initNablas ) import GHC.Core import GHC.Types.Literal import GHC.Core.Utils @@ -766,31 +766,31 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches (hsLMatchPats m)) -- 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. - ; matches_deltas <- if isMatchContextPmChecked dflags origin ctxt + -- @rhss_nablas@ is a flat list of covered Nablas for each RHS. + -- Each Match will split off one Nablas for its RHSs from this. + ; matches_nablas <- if isMatchContextPmChecked dflags origin ctxt then addHsScrutTmCs mb_scr new_vars $ -- See Note [Long-distance information] covCheckMatches (DsMatchContext ctxt locn) new_vars matches - else pure (initDeltasMatches matches) + else pure (initNablasMatches matches) - ; eqns_info <- zipWithM mk_eqn_info matches matches_deltas + ; eqns_info <- zipWithM mk_eqn_info matches matches_nablas ; result_expr <- handleWarnings $ matchEquations ctxt new_vars eqns_info rhs_ty ; return (new_vars, result_expr) } where -- Called once per equation in the match, or alternative in the case - 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) + mk_eqn_info :: LMatch GhcTc (LHsExpr GhcTc) -> (Nablas, NonEmpty Nablas) -> DsM EquationInfo + mk_eqn_info (L _ (Match { m_pats = pats, m_grhss = grhss })) (pat_nablas, rhss_nablas) = do { dflags <- getDynFlags ; let upats = map (unLoc . decideBangHood dflags) pats - -- pat_deltas is the covered set *after* matching the pattern, but - -- before any of the GRHSs. We extend the environment with pat_deltas - -- (via updPmDeltas) so that the where-clause of 'grhss' can profit + -- pat_nablas is the covered set *after* matching the pattern, but + -- before any of the GRHSs. We extend the environment with pat_nablas + -- (via updPmNablas) so that the where-clause of 'grhss' can profit -- from that knowledge (#18533) - ; match_result <- updPmDeltas pat_deltas $ - dsGRHSs ctxt grhss rhs_ty rhss_deltas + ; match_result <- updPmNablas pat_nablas $ + dsGRHSs ctxt grhss rhs_ty rhss_nablas ; return EqnInfo { eqn_pats = upats , eqn_orig = FromSource , eqn_rhs = match_result } } @@ -799,14 +799,14 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches then discardWarningsDs else id - initDeltasMatches :: [LMatch GhcTc b] -> [(Deltas, NonEmpty Deltas)] - initDeltasMatches ms - = map (\(L _ m) -> (initDeltas, initDeltasGRHSs (m_grhss m))) ms + initNablasMatches :: [LMatch GhcTc b] -> [(Nablas, NonEmpty Nablas)] + initNablasMatches ms + = map (\(L _ m) -> (initNablas, initNablasGRHSs (m_grhss m))) ms - initDeltasGRHSs :: GRHSs GhcTc b -> NonEmpty Deltas - initDeltasGRHSs m = expectJust "GRHSs non-empty" + initNablasGRHSs :: GRHSs GhcTc b -> NonEmpty Nablas + initNablasGRHSs m = expectJust "GRHSs non-empty" $ NEL.nonEmpty - $ replicate (length (grhssGRHSs m)) initDeltas + $ replicate (length (grhssGRHSs m)) initNablas matchEquations :: HsMatchContext GhcRn diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs index b6b0305a25..08b62ee14f 100644 --- a/compiler/GHC/HsToCore/Monad.hs +++ b/compiler/GHC/HsToCore/Monad.hs @@ -34,7 +34,7 @@ module GHC.HsToCore.Monad ( DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv, -- Getting and setting pattern match oracle states - getPmDeltas, updPmDeltas, + getPmNablas, updPmNablas, -- Get COMPLETE sets of a TyCon dsGetCompleteMatches, @@ -304,7 +304,7 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var cc_st_var } lcl_env = DsLclEnv { dsl_meta = emptyNameEnv , dsl_loc = real_span - , dsl_deltas = initDeltas + , dsl_nablas = initNablas } in (gbl_env, lcl_env) @@ -403,14 +403,14 @@ the @SrcSpan@ being carried around. getGhcModeDs :: DsM GhcMode getGhcModeDs = getDynFlags >>= return . ghcMode --- | Get the current pattern match oracle state. See 'dsl_deltas'. -getPmDeltas :: DsM Deltas -getPmDeltas = do { env <- getLclEnv; return (dsl_deltas env) } +-- | Get the current pattern match oracle state. See 'dsl_nablas'. +getPmNablas :: DsM Nablas +getPmNablas = do { env <- getLclEnv; return (dsl_nablas env) } -- | Set the pattern match oracle state within the scope of the given action. --- See 'dsl_deltas'. -updPmDeltas :: Deltas -> DsM a -> DsM a -updPmDeltas deltas = updLclEnv (\env -> env { dsl_deltas = deltas }) +-- See 'dsl_nablas'. +updPmNablas :: Nablas -> DsM a -> DsM a +updPmNablas nablas = updLclEnv (\env -> env { dsl_nablas = nablas }) getSrcSpanDs :: DsM SrcSpan getSrcSpanDs = do { env <- getLclEnv diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs index 99b81d3e69..9b9ce9d700 100644 --- a/compiler/GHC/HsToCore/PmCheck.hs +++ b/compiler/GHC/HsToCore/PmCheck.hs @@ -29,14 +29,14 @@ -- 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". +-- Basically the UA function from Section 5.1. The Normalised Refinement +-- Types 'Nablas' are maintained in "GHC.HsToCore.PmCheck.Oracle". -- 3. Collect redundancy information into a 'CIRB' with a function such -- as 'cirbsMatch'. Follows the R function from Figure 6 of the paper. -- 4. Format and report uncovered patterns and redundant equations ('CIRB') -- with 'formatReportWarnings'. Basically job of the G function, plus proper -- pretty printing of the warnings (Section 5.4 of the paper). --- 5. Return 'Deltas' reaching syntactic sub-components for +-- 5. Return 'Nablas' reaching syntactic sub-components for -- Note [Long-distance information]. Collected by functions such as -- 'ldiMatch'. See Section 4.1 of the paper. module GHC.HsToCore.PmCheck ( @@ -70,7 +70,6 @@ import GHC.Utils.Misc import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Core.DataCon -import GHC.Core.TyCon import GHC.Types.Var (EvVar) import GHC.Core.Coercion import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper) @@ -102,21 +101,21 @@ import Data.Coerce -- -- | A non-empty delta that is initialised from the ambient refinement type --- capturing long-distance information, or the trivially habitable 'Deltas' if +-- capturing long-distance information, or the trivially habitable 'Nablas' if -- the former is uninhabited. -- See Note [Recovering from unsatisfiable pattern-matching constraints]. -getLdiDeltas :: DsM Deltas -getLdiDeltas = do - deltas <- getPmDeltas - isInhabited deltas >>= \case - True -> pure deltas - False -> pure initDeltas +getLdiNablas :: DsM Nablas +getLdiNablas = do + nablas <- getPmNablas + isInhabited nablas >>= \case + True -> pure nablas + False -> pure initNablas -- | Check a pattern binding (let, where) for exhaustiveness. covCheckPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM () -- See Note [covCheckPatBind only checks PatBindRhs] covCheckPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do - missing <- getLdiDeltas + missing <- getLdiNablas 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 @@ -125,17 +124,17 @@ covCheckPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do covCheckPatBind _ _ _ = pure () -- | Exhaustive for guard matches, is used for guards in pattern bindings and --- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs. +-- in @MultiIf@ expressions. Returns the 'Nablas' 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 + -> DsM (NonEmpty Nablas) -- ^ Covered 'Nablas' for each RHS, for long -- distance info covCheckGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do let combined_loc = foldl1 combineSrcSpans (map getLoc grhss) ctxt = DsMatchContext hs_ctxt combined_loc matches <- desugarGRHSs combined_loc empty guards - missing <- getLdiDeltas + missing <- getLdiNablas tracePm "covCheckGRHSs" (hang (vcat [ppr ctxt , text "Guards:"]) 2 @@ -154,7 +153,7 @@ covCheckGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do -- f _ _ = 3 -- clause with a single, un-guarded RHS -- @ -- --- Returns one non-empty 'Deltas' for 1.) each pattern of a 'Match' and 2.) +-- Returns one non-empty 'Nablas' 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 @@ -164,13 +163,13 @@ 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 + -> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and -- GRHS, for long distance info. covCheckMatches ctxt vars matches = do -- We have to force @missing@ before printing out the trace message, -- otherwise we get interleaved output from the solver. This function -- should be strict in @missing@ anyway! - !missing <- getLdiDeltas + !missing <- getLdiNablas tracePm "covCheckMatches {" $ hang (vcat [ppr ctxt, ppr vars, text "Matches:"]) 2 @@ -223,7 +222,7 @@ 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. +initial Nabla and check if there are any values left to match on. -} -- @@ -249,8 +248,8 @@ data PmGrd -- 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) + pm_id :: !Id, + _pm_loc :: !(Maybe SrcInfo) } -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually @@ -296,15 +295,15 @@ type SrcInfo = Located SDoc -- (later digested into a 'CIRB'). data RedSets = RedSets - { rs_cov :: !Deltas + { rs_cov :: !Nablas -- ^ The /Covered/ set; the set of values reaching a particular program -- point. - , rs_div :: !Deltas + , rs_div :: !Nablas -- ^ 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 + , rs_bangs :: !(OrdList (Nablas, SrcInfo)) + -- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points -- a bang pattern in source that is redundant. See Note [Dead bang patterns]. } @@ -447,7 +446,7 @@ vanillaConGrd scrut con arg_ids = -- For example: -- @mkListGrds "a" "[(x, True <- x),(y, !y)]"@ -- to --- @"[(x:b) <- a, True <- x, (y:c) <- b, seq y True, [] <- c]"@ +-- @"[(x:b) <- a, True <- x, (y:c) <- b, !y, [] <- c]"@ -- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match -- variable. mkListGrds :: Id -> [(Id, GrdVec)] -> DsM GrdVec @@ -631,7 +630,7 @@ desugarListPat x pats = do -- | Desugar a constructor pattern desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar] - -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec + -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec 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]) @@ -651,14 +650,14 @@ desugarConPatOut x con univ_tys ex_tvs dicts = \case lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls go_field_pats tagged_pats = do - -- The fields that appear might not be in the correct order. So first - -- do a PmCon match, then force according to field strictness and then - -- force evaluation of the field patterns in the order given by - -- the first field of @tagged_pats@. + -- The fields that appear might not be in the correct order. So + -- 1. Do the PmCon match + -- 2. Then pattern match on the fields in the order given by the first + -- field of @tagged_pats@. -- See Note [Field match order for RecCon] -- Desugar the mentioned field patterns. We're doing this first to get - -- the Ids for pm_con_args. + -- the Ids for pm_con_args and bring them in order afterwards. let trans_pat (n, pat) = do (var, pvec) <- desugarLPatV pat pure ((n, var), pvec) @@ -672,19 +671,11 @@ desugarConPatOut x con univ_tys ex_tvs dicts = \case arg_ids <- zipWithM get_pat_id [0..] arg_tys let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids - -- 2. bang strict fields - let arg_is_banged = map isBanged $ conLikeImplBangs con - noSrcPmBang i = PmBang {pm_id = i, pm_loc = Nothing} - bang_grds = map noSrcPmBang (filterByList arg_is_banged arg_ids) - - -- 3. guards from field selector patterns + -- 2. guards from field selector patterns let arg_grds = concat arg_grdss -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids) - -- - -- Store the guards in exactly that order - -- 1. 2. 3. - pure (con_grd : bang_grds ++ arg_grds) + pure (con_grd : arg_grds) desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre) -- See 'GrdPatBind' for how this simply repurposes GrdGRHS. @@ -772,30 +763,45 @@ desugarBoolGuard e -> pure [vanillaConGrd y trueDataCon []] rhs -> do x <- mkPmId boolTy - pure $ [PmLet x rhs, vanillaConGrd x trueDataCon []] + pure [PmLet x rhs, vanillaConGrd x trueDataCon []] {- Note [Field match order for RecCon] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The order for RecCon field patterns actually determines evaluation order of the pattern match. For example: - data T = T { a :: !Bool, b :: Char, c :: Int } + data T = T { a :: Char, b :: Int } f :: T -> () - f T{ c = 42, b = 'b' } = () + f T{ b = 42, a = 'a' } = () + +Then @f (T (error "a") (error "b"))@ errors out with "b" because it is mentioned +first in the pattern match. -Then - * @f (T (error "a") (error "b") (error "c"))@ errors out with "a" because of - the strict field. - * @f (T True (error "b") (error "c"))@ errors out with "c" because it - is mentioned frist in the pattern match. +This means we can't just desugar the pattern match to +@[T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the +right order: @[T a b <- x, 42 <- b, 'a' <- a]@. -This means we can't just desugar the pattern match to the PatVec -@[T !_ 'b' 42]@. Instead we have to generate variable matches that have -strictness according to the field declarations and afterwards force them in the -right order. As a result, we get the PatVec @[T !_ b c, 42 <- c, 'b' <- b]@. +Note [Strict fields and fields of unlifted type] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +How do strict fields play into Note [Field match order for RecCon]? Answer: +They don't. Desugaring is entirely unconcerned by strict fields; the forcing +happens *before* pattern matching. But for each strict (or more generally, +unlifted) field @s@ we have to add @s /~ ⊥@ constraints when we check the PmCon +guard in 'checkGrd'. Strict fields are devoid of ⊥ by construction, there's +nothing that a bang pattern would act on. Example from #18341: + + data T = MkT !Int + f :: T -> () + f (MkT _) | False = () -- inaccessible + f (MkT !_) | False = () -- redundant, not only inaccessible! + f _ = () -Of course, when the labels occur in the order they are defined, we can just use -the simpler desugaring. +The second clause desugars to @MkT n <- x, !n@. When coverage checked, the +'PmCon' @MkT n <- x@ refines the set of values that reach the bang pattern with +the constraints @x ~ MkT n, n /~ ⊥@ (this list is computed by 'pmConCts'). +Checking the 'PmBang' @!n@ will then try to add the constraint @n ~ ⊥@ to this +set to get the diverging set, which is found to be empty. Hence the whole +clause is detected as redundant, as expected. Note [Order of guards matters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -847,7 +853,7 @@ data CheckResult a = CheckResult { cr_ret :: !a -- ^ A hole for redundancy info and covered sets. - , cr_uncov :: !Deltas + , cr_uncov :: !Nablas -- ^ The set of uncovered values falling out at the bottom. -- (for -Wincomplete-patterns, but also important state for the algorithm) , cr_approx :: !Precision @@ -865,23 +871,23 @@ instance Outputable a => Outputable (CheckResult a) where 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 +-- | Lift 'addPmCts' over 'Nablas'. +addPmCtsNablas :: Nablas -> PmCts -> DsM Nablas +addPmCtsNablas nablas cts = liftNablasM (\d -> addPmCts d cts) nablas --- | 'addPmCtsDeltas' for a single 'PmCt'. -addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas -addPmCtDeltas deltas ct = addPmCtsDeltas deltas (unitBag ct) +-- | 'addPmCtsNablas' for a single 'PmCt'. +addPmCtNablas :: Nablas -> PmCt -> DsM Nablas +addPmCtNablas nablas ct = addPmCtsNablas nablas (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 +-- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because +-- we preserve the invariant that there are no uninhabited 'Nabla's. But that -- could change in the future, for example by implementing this function in -- terms of @notNull <$> provideEvidence 1 ds@. -isInhabited :: Deltas -> DsM Bool -isInhabited (MkDeltas ds) = pure (not (null ds)) +isInhabited :: Nablas -> DsM Bool +isInhabited (MkNablas ds) = pure (not (null ds)) -- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'. -newtype CheckAction a = CA { unCA :: Deltas -> DsM (CheckResult a) } +newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) } deriving Functor -- | Composes 'CheckAction's top-to-bottom: @@ -923,23 +929,34 @@ leftToRight f (CA left) (CA right) = CA $ \inc -> do , 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. +-- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@ +-- is exceeding the given @limit@ and the @old@ number of 'Nabla's. -- See Note [Countering exponential blowup]. -throttle :: Int -> Deltas -> Deltas -> (Precision, Deltas) -throttle limit old@(MkDeltas old_ds) new@(MkDeltas new_ds) +throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas) +throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds) --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined | length new_ds > max limit (length old_ds) = (Approximate, old) | otherwise = (Precise, new) --- | Matching on a newtype doesn't force anything. --- See Note [Divergence of Newtype matches] in "GHC.HsToCore.PmCheck.Oracle". -conMatchForces :: PmAltCon -> Bool -conMatchForces (PmAltConLike (RealDataCon dc)) - | isNewTyCon (dataConTyCon dc) = False -conMatchForces _ = True - --- First the functions that correspond to checking LYG primitives: +-- | The 'PmCts' arising from a successful 'PmCon' match @T gammas as ys <- x@. +-- These include +-- +-- * @gammas@: Constraints arising from the bound evidence vars +-- * @y /~ ⊥@ constraints for each unlifted field (including strict fields) +-- @y@ in @ys@ +-- * The constructor constraint itself: @x ~ T as ys@. +-- +-- See Note [Strict fields and fields of unlifted type]. +pmConCts :: Id -> PmAltCon -> [TyVar] -> [EvVar] -> [Id] -> PmCts +pmConCts x con tvs dicts args = gammas `unionBags` unlifted `snocBag` con_ct + where + gammas = listToBag $ map (PmTyCt . evVarPred) dicts + con_ct = PmConCt x con tvs args + unlifted = listToBag [ PmNotBotCt arg + | (arg, bang) <- + zipEqual "pmConCts" args (pmAltConImplBangs con) + , isBanged bang || isUnliftedType (idType arg) + ] checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) -- The implementation is pretty similar to @@ -952,31 +969,32 @@ 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) + matched <- addPmCtNablas inc (PmCoreCt x e) + -- tracePm "check:Let" (ppr x <+> char '=' <+> ppr 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) + div <- addPmCtNablas inc (PmBotCt x) + matched <- addPmCtNablas 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 + -- tracePm "check:Bang" (ppr x <+> ppr div) 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 + -- Con: 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) + !div <- if isPmAltConMatchStrict con + then addPmCtNablas 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) + let con_cts = pmConCts x con tvs dicts args + !matched <- addPmCtsNablas inc con_cts + !uncov <- addPmCtNablas inc (PmNotConCt x con) + -- tracePm "checkGrd:Con" (ppr inc $$ ppr grd $$ ppr con_cts $$ ppr matched) pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div } , cr_uncov = uncov , cr_approx = Precise } @@ -1010,7 +1028,7 @@ checkGRHS (PmGRHS { pg_grds = grds, pg_rhs = rhs_info }) = checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do - unc <- addPmCtDeltas inc (PmNotBotCt var) + unc <- addPmCtNablas inc (PmNotBotCt var) pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty } checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post) @@ -1020,7 +1038,7 @@ checkPatBind = coerce checkGRHS ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 +the -fmax-pmcheck-models flag, limiting the number of Nablas we check against each pattern by a constant. How do we do that? Consider @@ -1029,13 +1047,13 @@ How do we do that? Consider 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 +will be checked against the initial Nabla, {}. 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 +with a singleton Uncovered set of the initial Nabla {}. 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 @@ -1062,14 +1080,14 @@ program, so we don't actually get useful information out of that split! -- * Collecting long-distance information -- -ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Deltas, NonEmpty Deltas) +ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas) ldiMatchGroup (PmMatchGroup matches) = ldiMatch <$> matches -ldiMatch :: PmMatch Post -> (Deltas, NonEmpty Deltas) +ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas) ldiMatch (PmMatch { pm_pats = red, pm_grhss = grhss }) = (rs_cov red, ldiGRHS <$> grhss) -ldiGRHS :: PmGRHS Post -> Deltas +ldiGRHS :: PmGRHS Post -> Nablas ldiGRHS (PmGRHS { pg_grds = red }) = rs_cov red -- @@ -1114,17 +1132,17 @@ addRedundantBangs _red_bangs cirb@CIRB { cirb_cov = NilOL, cirb_inacc = NilOL } addRedundantBangs red_bangs cirb = cirb { cirb_bangs = cirb_bangs cirb Semi.<> red_bangs } --- | Checks the 'Deltas' in a 'RedSets' for inhabitants and returns +-- | Checks the 'Nablas' in a 'RedSets' for inhabitants and returns -- 1. Whether the Covered set was inhabited -- 2. Whether the Diverging set was inhabited --- 3. All source bangs whose 'Deltas' were empty, which means they are +-- 3. All source bangs whose 'Nablas' were empty, which means they are -- redundant. testRedSets :: RedSets -> DsM (Bool, Bool, OrdList SrcInfo) testRedSets RedSets { rs_cov = cov, rs_div = div, rs_bangs = bangs } = do is_covered <- isInhabited cov may_diverge <- isInhabited div - red_bangs <- flip mapMaybeM (fromOL bangs) $ \(deltas, bang) -> do - isInhabited deltas >>= \case + red_bangs <- flip mapMaybeM (fromOL bangs) $ \(nablas, bang) -> do + isInhabited nablas >>= \case True -> pure Nothing False -> pure (Just bang) pure (is_covered, may_diverge, toOL red_bangs) @@ -1233,10 +1251,10 @@ reportWarnings dflags ctx@(DsMatchContext kind loc) vars f (q <+> matchSeparator kind <+> text "...") -- Print several clauses (for uncovered clauses) - pprEqns vars deltas = pprContext False ctx (text "are non-exhaustive") $ \_ -> + pprEqns vars nablas = pprContext False ctx (text "are non-exhaustive") $ \_ -> case vars of -- See #11245 [] -> text "Guards do not cover entire pattern space" - _ -> let us = map (\delta -> pprUncovered delta vars) deltas + _ -> let us = map (\nabla -> pprUncovered nabla vars) nablas in hang (text "Patterns not matched:") 4 (vcat (take maxPatterns us) $$ dots maxPatterns us) @@ -1251,14 +1269,14 @@ reportWarnings dflags ctx@(DsMatchContext kind loc) vars $$ bullet <+> text "Patterns reported as unmatched might actually be matched") , text "Increase the limit or resolve the warnings to suppress this message." ] -getNFirstUncovered :: [Id] -> Int -> Deltas -> DsM [Delta] -getNFirstUncovered vars n (MkDeltas deltas) = go n (bagToList deltas) +getNFirstUncovered :: [Id] -> Int -> Nablas -> DsM [Nabla] +getNFirstUncovered vars n (MkNablas nablas) = go n (bagToList nablas) where go 0 _ = pure [] go _ [] = pure [] - go n (delta:deltas) = do - front <- provideEvidence vars n delta - back <- go (n - length front) deltas + go n (nabla:nablas) = do + front <- provideEvidence vars n nabla + back <- go (n - length front) nablas pure (front ++ back) dots :: Int -> [a] -> SDoc @@ -1383,13 +1401,13 @@ code that we don't want to warn about. -- * Long-distance information -- --- | Locally update 'dsl_deltas' with the given action, but defer evaluation +-- | Locally update 'dsl_nablas' with the given action, but defer evaluation -- with 'unsafeInterleaveM' in order not to do unnecessary work. -locallyExtendPmDeltas :: (Deltas -> DsM Deltas) -> DsM a -> DsM a -locallyExtendPmDeltas ext k = do - deltas <- getLdiDeltas - deltas' <- unsafeInterleaveM $ ext deltas - updPmDeltas deltas' k +locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a +locallyExtendPmNablas ext k = do + nablas <- getLdiNablas + nablas' <- unsafeInterleaveM $ ext nablas + updPmNablas nablas' k -- | Add in-scope type constraints if the coverage checker might run and then -- run the given action. @@ -1397,7 +1415,7 @@ 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))) + (locallyExtendPmNablas (\nablas -> addPmCtsNablas nablas (PmTyCt . evVarPred <$> ev_vars))) m -- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment @@ -1408,8 +1426,8 @@ addTyCs origin ev_vars m = do 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)) + flip locallyExtendPmNablas k $ \nablas -> + addPmCtsNablas nablas (unitBag (PmCoreCt x scr)) addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id" -- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first. @@ -1437,10 +1455,10 @@ of @f@. 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 +as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas'. +We fill that set with Covered Nablas returned by the exported checking functions, which the call sites put into place with -'GHC.HsToCore.Monad.updPmDeltas'. +'GHC.HsToCore.Monad.updPmNablas'. Call sites also extend this set with facts from type-constraint dictionaries, case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs' and 'addHsScrutTmCs'. @@ -1458,7 +1476,7 @@ This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the coverage checker deems any matches with unsatisfiable constraint sets to be unreachable. -We make sure to always start from an inhabited 'Deltas' by calling -'getLdiDeltas', which falls back to the trivially inhabited 'Deltas' if the -long-distance info returned by 'GHC.HsToCore.Monad.getPmDeltas' is empty. +We make sure to always start from an inhabited 'Nablas' by calling +'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the +long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty. -} diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs index b3a6010b23..78238965fc 100644 --- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs +++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs @@ -4,22 +4,25 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be> Ryan Scott <ryan.gl.scott@gmail.com> -} -{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-} +{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf, ScopedTypeVariables #-} -- | The pattern match oracle. The main export of the module are the functions -- 'addPmCts' for adding facts to the oracle, and 'provideEvidence' to turn a --- 'Delta' into a concrete evidence for an equation. +-- 'Nabla' into a concrete evidence for an equation. +-- +-- In terms of the [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989) +-- describing the implementation, this module is concerned with Sections 3.4, 3.6 and 3.7. +-- E.g., it represents refinement types diretly as a normalised refinement type 'Nabla'. module GHC.HsToCore.PmCheck.Oracle ( DsM, tracePm, mkPmId, - Delta, initDeltas, lookupRefuts, lookupSolution, + Nabla, initNablas, lookupRefuts, lookupSolution, PmCt(PmTyCt), PmCts, pattern PmVarCt, pattern PmCoreCt, pattern PmConCt, pattern PmNotConCt, pattern PmBotCt, pattern PmNotBotCt, addPmCts, -- Add a constraint to the oracle. - canDiverge, -- Try to add the term equality x ~ ⊥ provideEvidence ) where @@ -154,12 +157,7 @@ mkOneConFull arg_tys con = do -- to the type oracle let ty_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas) -- Figure out the types of strict constructor fields - let arg_is_strict - | RealDataCon dc <- con - , isNewTyCon (dataConTyCon dc) - = [True] -- See Note [Divergence of Newtype matches] - | otherwise - = map isBanged $ conLikeImplBangs con + let arg_is_strict = map isBanged $ conLikeImplBangs con strict_arg_tys = filterByList arg_is_strict field_tys' return (ex_tvs, vars, listToBag ty_cs, strict_arg_tys) @@ -170,8 +168,8 @@ mkOneConFull arg_tys con = do ------------------------------------- -- * Composable satisfiability checks --- | Given a 'Delta', check if it is compatible with new facts encoded in this --- this check. If so, return 'Just' a potentially extended 'Delta'. Return +-- | Given a 'Nabla', check if it is compatible with new facts encoded in this +-- this check. If so, return 'Just' a potentially extended 'Nabla'. Return -- 'Nothing' if unsatisfiable. -- -- There are three essential SatisfiabilityChecks: @@ -180,22 +178,22 @@ mkOneConFull arg_tys con = do -- 3. 'tysAreNonVoid', checks if the given types have an inhabitant -- Functions like 'pmIsSatisfiable', 'nonVoid' and 'testInhabited' plug these -- together as they see fit. -newtype SatisfiabilityCheck = SC (Delta -> DsM (Maybe Delta)) +newtype SatisfiabilityCheck = SC (Nabla -> DsM (Maybe Nabla)) --- | Check the given 'Delta' for satisfiability by the given --- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Delta' if +-- | Check the given 'Nabla' for satisfiability by the given +-- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Nabla' if -- successful, and 'Nothing' otherwise. -runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta) -runSatisfiabilityCheck delta (SC chk) = chk delta +runSatisfiabilityCheck :: Nabla -> SatisfiabilityCheck -> DsM (Maybe Nabla) +runSatisfiabilityCheck nabla (SC chk) = chk nabla -- | Allowing easy composition of 'SatisfiabilityCheck's. instance Semigroup SatisfiabilityCheck where -- This is @a >=> b@ from MaybeT DsM SC a <> SC b = SC c where - c delta = a delta >>= \case + c nabla = a nabla >>= \case Nothing -> pure Nothing - Just delta' -> b delta' + Just nabla' -> b nabla' instance Monoid SatisfiabilityCheck where -- We only need this because of mconcat (which we use in place of sconcat, @@ -214,13 +212,13 @@ instance Monoid SatisfiabilityCheck where -- discussed in GADTs Meet Their Match. For an explanation of what role they -- serve, see @Note [Strict argument type constraints]@. pmIsSatisfiable - :: Delta -- ^ The ambient term and type constraints + :: Nabla -- ^ The ambient term and type constraints -- (known to be satisfiable). -> Bag TyCt -- ^ The new type constraints. -> Bag TmCt -- ^ The new term constraints. -> [Type] -- ^ The strict argument types. - -> DsM (Maybe Delta) - -- ^ @'Just' delta@ if the constraints (@delta@) are + -> DsM (Maybe Nabla) + -- ^ @'Just' nabla@ if the constraints (@nabla@) are -- satisfiable, and each strict argument type is inhabitable. -- 'Nothing' otherwise. pmIsSatisfiable amb_cs new_ty_cs new_tm_cs strict_arg_tys = @@ -493,21 +491,21 @@ tyOracle (TySt inert) cts Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) } -- | A 'SatisfiabilityCheck' based on new type-level constraints. --- Returns a new 'Delta' if the new constraints are compatible with existing +-- Returns a new 'Nabla' if the new constraints are compatible with existing -- ones. Doesn't bother calling out to the type oracle if the bag of new type -- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle -- for emptiness if the first argument is 'True'. tyIsSatisfiable :: Bool -> Bag PredType -> SatisfiabilityCheck -tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> +tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \nabla -> if isEmptyBag new_ty_cs - then pure (Just delta) - else tyOracle (delta_ty_st delta) new_ty_cs >>= \case + then pure (Just nabla) + else tyOracle (nabla_ty_st nabla) new_ty_cs >>= \case Nothing -> pure Nothing Just ty_st' -> do - let delta' = delta{ delta_ty_st = ty_st' } + let nabla' = nabla{ nabla_ty_st = ty_st' } if recheck_complete_sets - then ensureAllPossibleMatchesInhabited delta' - else pure (Just delta') + then ensureAllInhabited nabla' + else pure (Just nabla') {- ********************************************************************* @@ -619,21 +617,46 @@ warning messages (which can be alleviated by someone with enough dedication). -} -- | A 'SatisfiabilityCheck' based on new term-level constraints. --- Returns a new 'Delta' if the new constraints are compatible with existing +-- Returns a new 'Nabla' if the new constraints are compatible with existing -- ones. tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck -tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM addTmCt delta new_tm_cs +tmIsSatisfiable new_tm_cs = SC $ \nabla -> runMaybeT $ foldlM addTmCt nabla new_tm_cs ----------------------- -- * Looking up VarInfo emptyVarInfo :: Id -> VarInfo -emptyVarInfo x = VI (idType x) [] emptyPmAltConSet NoPM +-- We could initialise @bot@ to @Just False@ in case of an unlifted type here, +-- but it's cleaner to let the user of the constraint solver take care of this. +-- After all, there are also strict fields, the unliftedness of which isn't +-- evident in the type. So treating unlifted types here would never be +-- sufficient anyway. +emptyVarInfo x = VI (idType x) [] emptyPmAltConSet MaybeBot NoPM lookupVarInfo :: TmState -> Id -> VarInfo -- (lookupVarInfo tms x) tells what we know about 'x' lookupVarInfo (TmSt env _) x = fromMaybe (emptyVarInfo x) (lookupSDIE env x) +-- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks +-- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the +-- returned @y@ doesn't have a positive newtype constructor constraint +-- associated with it (yet). The 'VarInfo' returned is that of @y@'s +-- representative. +-- +-- Careful, this means that @idType x@ might be different to @idType y@, even +-- modulo type normalisation! +-- +-- See also Note [Coverage checking Newtype matches]. +lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo) +lookupVarInfoNT ts x = case lookupVarInfo ts x of + VI{ vi_pos = as_newtype -> Just y } -> lookupVarInfoNT ts y + res -> (x, res) + where + as_newtype = listToMaybe . mapMaybe go + go (PmAltConLike (RealDataCon dc), _, [y]) + | isNewDataCon dc = Just y + go _ = Nothing + initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do -- New evidence might lead to refined info on ty, in turn leading to discovery @@ -670,13 +693,6 @@ initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do Just cs -> pure vi{ vi_ty = ty', vi_cache = PM (mkUniqDSet <$> cs) } initPossibleMatches _ vi = pure vi --- | @initLookupVarInfo ts x@ looks up the 'VarInfo' for @x@ in @ts@ and tries --- to initialise the 'vi_cache' component if it was 'NoPM' through --- 'initPossibleMatches'. -initLookupVarInfo :: Delta -> Id -> DsM VarInfo -initLookupVarInfo MkDelta{ delta_tm_st = ts, delta_ty_st = ty_st } x - = initPossibleMatches ty_st (lookupVarInfo ts x) - {- Note [COMPLETE sets on data families] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ User-defined COMPLETE sets involving data families are attached to the family @@ -721,22 +737,11 @@ TyCon, so tc_rep = tc_fam afterwards. -} ------------------------------------------------ --- * Exported utility functions querying 'Delta' +-- * Exported utility functions querying 'Nabla' --- | Check whether adding a constraint @x ~ BOT@ to 'Delta' succeeds. -canDiverge :: Delta -> Id -> Bool -canDiverge delta@MkDelta{ delta_tm_st = ts } x - | VI _ pos neg _ <- lookupVarInfo ts x - = isEmptyPmAltConSet neg && all pos_can_diverge pos - where - pos_can_diverge (PmAltConLike (RealDataCon dc), _, [y]) - -- See Note [Divergence of Newtype matches] - | isNewTyCon (dataConTyCon dc) = canDiverge delta y - pos_can_diverge _ = False - -{- Note [Divergence of Newtype matches] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Newtypes behave rather strangely when compared to ordinary DataCons. In a +{- Note [Coverage checking Newtype matches] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Newtypes have quite peculiar match semantics compared to ordinary DataCons. In a pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation testing purposes (e.g. at construction sites), they behave rather like a DataCon with a *strict* field, because they don't contribute their own bottom and are @@ -751,19 +756,21 @@ This distinction becomes apparent in #17248: If we treat Newtypes like we treat regular DataCons, we would mark the third clause as redundant, which clearly is unsound. The solution: -1. When compiling the PmCon guard in 'pmCompileTree', don't add a @DivergeIf@, - because the match will never diverge. -2. Regard @T2 x@ as 'canDiverge' iff @x@ 'canDiverge'. E.g. @T2 x ~ _|_@ <=> - @x ~ _|_@. This way, the third clause will still be marked as inaccessible - RHS instead of redundant. -3. When testing for inhabitants ('mkOneConFull'), we regard the newtype field as - strict, so that the newtype is inhabited iff its field is inhabited. +1. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a + newtype match is lazy. +2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@) + to @y@, similar to what 'equate' does, and don't add a @x /~ ⊥@ constraint. + This way, the third clause will still be marked as inaccessible RHS instead + of redundant. This is ensured by calling 'lookupVarInfoNT'. +3. Immediately reject when we find @x /~ T2@. +Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper, +where you can find the solution in a perhaps more digestible format. -} -lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon] +lookupRefuts :: Uniquable k => Nabla -> k -> [PmAltCon] -- Unfortunately we need the extra bit of polymorphism and the unfortunate -- duplication of lookupVarInfo here. -lookupRefuts MkDelta{ delta_tm_st = ts@(TmSt (SDIE env) _) } k = +lookupRefuts MkNabla{ nabla_tm_st = ts@(TmSt (SDIE env) _) } k = case lookupUDFM_Directly env (getUnique k) of Nothing -> [] Just (Indirect y) -> pmAltConSetElems (vi_neg (lookupVarInfo ts y)) @@ -773,10 +780,10 @@ isDataConSolution :: (PmAltCon, [TyVar], [Id]) -> Bool isDataConSolution (PmAltConLike (RealDataCon _), _, _) = True isDataConSolution _ = False --- @lookupSolution delta x@ picks a single solution ('vi_pos') of @x@ from +-- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from -- possibly many, preferring 'RealDataCon' solutions whenever possible. -lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [TyVar], [Id]) -lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of +lookupSolution :: Nabla -> Id -> Maybe (PmAltCon, [TyVar], [Id]) +lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of [] -> Nothing pos | Just sol <- find isDataConSolution pos -> Just sol @@ -843,13 +850,13 @@ instance Outputable PmCt where ppr (PmTyCt pred_ty) = ppr pred_ty ppr (PmTmCt tm_ct) = ppr tm_ct --- | Adds new constraints to 'Delta' and returns 'Nothing' if that leads to a +-- | Adds new constraints to 'Nabla' and returns 'Nothing' if that leads to a -- contradiction. -addPmCts :: Delta -> PmCts -> DsM (Maybe Delta) +addPmCts :: Nabla -> PmCts -> DsM (Maybe Nabla) -- See Note [TmState invariants]. -addPmCts delta cts = do +addPmCts nabla cts = do let (ty_cts, tm_cts) = partitionTyTmCts cts - runSatisfiabilityCheck delta $ mconcat + runSatisfiabilityCheck nabla $ mconcat [ tyIsSatisfiable True (listToBag ty_cts) , tmIsSatisfiable (listToBag tm_cts) ] @@ -862,44 +869,40 @@ partitionTyTmCts = partitionEithers . map to_either . toList -- | Adds a single term constraint by dispatching to the various term oracle -- functions. -addTmCt :: Delta -> TmCt -> MaybeT DsM Delta -addTmCt delta (TmVarCt x y) = addVarCt delta x y -addTmCt delta (TmCoreCt x e) = addCoreCt delta x e -addTmCt delta (TmConCt x con tvs args) = addConCt delta x con tvs args -addTmCt delta (TmNotConCt x con) = addNotConCt delta x con -addTmCt delta (TmBotCt x) = addBotCt delta x -addTmCt delta (TmNotBotCt x) = addNotBotCt delta x +addTmCt :: Nabla -> TmCt -> MaybeT DsM Nabla +addTmCt nabla (TmVarCt x y) = addVarCt nabla x y +addTmCt nabla (TmCoreCt x e) = addCoreCt nabla x e +addTmCt nabla (TmConCt x con tvs args) = addConCt nabla x con tvs args +addTmCt nabla (TmNotConCt x con) = addNotConCt nabla x con +addTmCt nabla (TmBotCt x) = addBotCt nabla x +addTmCt nabla (TmNotBotCt x) = addNotBotCt nabla x -- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@ --- surely diverges. --- --- Only that's a lie, because we don't currently preserve the fact in 'Delta' --- after we checked compatibility. See Note [Preserving TmBotCt] -addBotCt :: Delta -> Id -> MaybeT DsM Delta -addBotCt delta x - | canDiverge delta x = pure delta - | otherwise = mzero - -{- Note [Preserving TmBotCt] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Whenever we add a new constraint to 'Delta' via 'addTmCt', we want to check it -for compatibility with existing constraints in the modeled indert set and then -add it the constraint itself to the inert set. -For a 'TmBotCt' @x ~ ⊥@ we don't actually add it to the inert set after checking -it for compatibility with 'Delta'. -And that is fine in the context of the patter-match checking algorithm! -Whenever we add a 'TmBotCt' (we only do so for checking divergence of bang -patterns and strict constructor matches), we don't add any more constraints to -the inert set afterwards, so we don't need to preserve it. --} +-- surely diverges. Quite similar to 'addConCt', only that it only cares about +-- ⊥. +addBotCt :: Nabla -> Id -> MaybeT DsM Nabla +addBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do + let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x + case bot of + IsNotBot -> mzero -- There was x /~ ⊥. Contradiction! + IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do + MaybeBot -> do -- We add x ~ ⊥ + let vi' = vi{ vi_bot = IsBot } + pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi') reps} -- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't --- take the shape of a 'PmAltCon' @K@ in the 'Delta' and return @Nothing@ if +-- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if -- that leads to a contradiction. -- See Note [TmState invariants]. -addNotConCt :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta -addNotConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do - vi@(VI _ pos neg pm) <- lift (initLookupVarInfo delta x) +addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla +addNotConCt _ _ (PmAltConLike (RealDataCon dc)) + | isNewDataCon dc = mzero -- (3) in Note [Coverage checking Newtype matches] +addNotConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do + -- For good performance, it's important to initPossibleMatches here. + -- Otherwise we can't mark nalt as matched later on, incurring unnecessary + -- inhabitation tests for nalt. + vi@(VI _ pos neg _ pm) <- lift $ initPossibleMatches (nabla_ty_st nabla) + (lookupVarInfo ts x) -- 1. Bail out quickly when nalt contradicts a solution let contradicts nalt (cl, _tvs, _args) = eqPmAltCon cl nalt == Equal guard (not (any (contradicts nalt) pos)) @@ -911,13 +914,14 @@ addNotConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do -- See Note [Completeness checking with required Thetas] | hasRequiredTheta nalt = neg | otherwise = extendPmAltConSet neg nalt - let vi_ext = vi{ vi_neg = neg' } + MASSERT( isPmAltConMatchStrict nalt ) + let vi1 = vi{ vi_neg = neg', vi_bot = IsNotBot } -- 3. Make sure there's at least one other possible constructor - vi' <- case nalt of + vi2 <- case nalt of PmAltConLike cl - -> MaybeT (ensureInhabited delta vi_ext{ vi_cache = markMatched cl pm }) - _ -> pure vi_ext - pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') reps } + -> ensureInhabited nabla vi1{ vi_cache = markMatched cl pm } + _ -> pure vi1 + pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env x vi2) reps } hasRequiredTheta :: PmAltCon -> Bool hasRequiredTheta (PmAltConLike cl) = notNull req_theta @@ -980,100 +984,104 @@ guessConLikeUnivTyArgsFromResTy _ res_ty (PatSynCon ps) = do subst <- tcMatchTy con_res_ty res_ty traverse (lookupTyVar subst) univ_tvs --- | Adds the constraint @x ~/ ⊥@ to 'Delta'. +-- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt', +-- but only cares for the ⊥ "constructor". +addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla +addNotBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do + let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x + case bot of + IsBot -> mzero -- There was x ~ ⊥. Contradiction! + IsNotBot -> pure nabla -- There already is x /~ ⊥. Nothing left to do + MaybeBot -> do -- We add x /~ ⊥ and test if x is still inhabited + vi <- ensureInhabited nabla vi{ vi_bot = IsNotBot } + pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi) reps} + +-- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE +-- set satisfies the oracle -- --- But doesn't really commit to upholding that constraint in the future. This --- will be rectified in a follow-up patch. The status quo should work good --- enough for now. -addNotBotCt :: Delta -> Id -> MaybeT DsM Delta -addNotBotCt delta@MkDelta{ delta_tm_st = TmSt env reps } x = do - vi <- lift $ initLookupVarInfo delta x - vi' <- MaybeT $ ensureInhabited delta vi - -- vi' has probably constructed and then thinned out some PossibleMatches. - -- We want to cache that work - pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') reps} - -ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo) - -- Returns (Just vi) if at least one member of each ConLike in the COMPLETE - -- set satisfies the oracle - -- - -- Internally uses and updates the ConLikeSets in vi_cache. - -- - -- NB: Does /not/ filter each ConLikeSet with the oracle; members may - -- remain that do not statisfy it. This lazy approach just - -- avoids doing unnecessary work. -ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This would be much less tedious with lenses +-- Internally uses and updates the ConLikeSets in vi_cache. +-- +-- NB: Does /not/ filter each ConLikeSet with the oracle; members may +-- remain that do not statisfy it. This lazy approach just +-- avoids doing unnecessary work. +ensureInhabited :: Nabla -> VarInfo -> MaybeT DsM VarInfo +ensureInhabited nabla vi = case vi_bot vi of + MaybeBot -> pure vi -- The |-Bot rule from the paper + IsBot -> pure vi + IsNotBot -> lift (initPossibleMatches (nabla_ty_st nabla) vi) >>= inst_complete_sets where - set_cache vi cache = vi { vi_cache = cache } - - test NoPM = pure (Just NoPM) - test (PM ms) = runMaybeT (PM <$> traverse one_set ms) - - one_set cs = find_one_inh cs (uniqDSetToList cs) - - find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet - -- (find_one_inh cs cls) iterates over cls, deleting from cs + -- | This is the |-Inst rule from the paper (section 4.5). Tries to + -- find an inhabitant in every complete set by instantiating with one their + -- constructors. If there is any complete set where we can't find an + -- inhabitant, the whole thing is uninhabited. + inst_complete_sets :: VarInfo -> MaybeT DsM VarInfo + inst_complete_sets vi@VI{ vi_cache = NoPM } = pure vi + inst_complete_sets vi@VI{ vi_cache = PM ms } = do + ms <- traverse (\cs -> inst_complete_set vi cs (uniqDSetToList cs)) ms + pure vi{ vi_cache = PM ms } + + inst_complete_set :: VarInfo -> ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet + -- (inst_complete_set cs cls) iterates over cls, deleting from cs -- any uninhabited elements of cls. Stop (returning Just cs) -- when you see an inhabited element; return Nothing if all -- are uninhabited - find_one_inh _ [] = mzero - find_one_inh cs (con:cons) = lift (inh_test con) >>= \case + inst_complete_set _ _ [] = mzero + inst_complete_set vi cs (con:cons) = lift (inst_and_test vi con) >>= \case True -> pure cs - False -> find_one_inh (delOneFromUniqDSet cs con) cons + False -> inst_complete_set vi (delOneFromUniqDSet cs con) cons - inh_test :: ConLike -> DsM Bool - -- @inh_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly + inst_and_test :: VarInfo -> ConLike -> DsM Bool + -- @inst_and_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly -- be of form @K _ _ _@. Returning True is always sound. -- -- It's like 'DataCon.dataConCannotMatch', but more clever because it takes - -- the facts in Delta into account. - inh_test con = do + -- the facts in Nabla into account. + inst_and_test vi con = do env <- dsGetFamInstEnvs case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of Nothing -> pure True -- be conservative about this Just arg_tys -> do (_tvs, _vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con - tracePm "inh_test" (ppr con $$ ppr ty_cs) + tracePm "inst_and_test" (ppr con $$ ppr ty_cs) -- No need to run the term oracle compared to pmIsSatisfiable - fmap isJust <$> runSatisfiabilityCheck delta $ mconcat + fmap isJust <$> runSatisfiabilityCheck nabla $ mconcat -- Important to pass False to tyIsSatisfiable here, so that we won't - -- recursively call ensureAllPossibleMatchesInhabited, leading to an + -- recursively call ensureAllInhabited, leading to an -- endless recursion. [ tyIsSatisfiable False ty_cs , tysAreNonVoid initRecTc strict_arg_tys ] -- | Checks if every 'VarInfo' in the term oracle has still an inhabited --- 'vi_cache', considering the current type information in 'Delta'. +-- 'vi_cache', considering the current type information in 'Nabla'. -- This check is necessary after having matched on a GADT con to weed out -- impossible matches. -ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta) -ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env reps } - = runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env) +ensureAllInhabited :: Nabla -> DsM (Maybe Nabla) +ensureAllInhabited nabla@MkNabla{ nabla_tm_st = TmSt env reps } + = runMaybeT (set_tm_cs_env nabla <$> traverseSDIE go env) where - set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env reps } - go vi = MaybeT $ - initPossibleMatches (delta_ty_st delta) vi >>= ensureInhabited delta + set_tm_cs_env nabla env = nabla{ nabla_tm_st = TmSt env reps } + go vi = ensureInhabited nabla vi -------------------------------------- -- * Term oracle unification procedure -- | Adds a @x ~ y@ constraint by trying to unify two 'Id's and record the --- gained knowledge in 'Delta'. +-- gained knowledge in 'Nabla'. -- --- Returns @Nothing@ when there's a contradiction. Returns @Just delta@ --- when the constraint was compatible with prior facts, in which case @delta@ +-- Returns @Nothing@ when there's a contradiction. Returns @Just nabla@ +-- when the constraint was compatible with prior facts, in which case @nabla@ -- has integrated the knowledge from the equality constraint. -- -- See Note [TmState invariants]. -addVarCt :: Delta -> Id -> Id -> MaybeT DsM Delta -addVarCt delta@MkDelta{ delta_tm_st = TmSt env _ } x y +addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla +addVarCt nabla@MkNabla{ nabla_tm_st = TmSt env _ } x y -- It's important that we never @equate@ two variables of the same equivalence -- class, otherwise we might get cyclic substitutions. -- Cf. 'extendSubstAndSolve' and -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@. - | sameRepresentativeSDIE env x y = pure delta - | otherwise = equate delta x y + | sameRepresentativeSDIE env x y = pure nabla + | otherwise = equate nabla x y -- | @equate ts@(TmSt env) x y@ merges the equivalence classes of @x@ and @y@ by -- adding an indirection to the environment. @@ -1082,12 +1090,12 @@ addVarCt delta@MkDelta{ delta_tm_st = TmSt env _ } x y -- Preconditions: @not (sameRepresentativeSDIE env x y)@ -- -- See Note [TmState invariants]. -equate :: Delta -> Id -> Id -> MaybeT DsM Delta -equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y +equate :: Nabla -> Id -> Id -> MaybeT DsM Nabla +equate nabla@MkNabla{ nabla_tm_st = TmSt env reps } x y = ASSERT( not (sameRepresentativeSDIE env x y) ) case (lookupSDIE env x, lookupSDIE env y) of - (Nothing, _) -> pure (delta{ delta_tm_st = TmSt (setIndirectSDIE env x y) reps }) - (_, Nothing) -> pure (delta{ delta_tm_st = TmSt (setIndirectSDIE env y x) reps }) + (Nothing, _) -> pure (nabla{ nabla_tm_st = TmSt (setIndirectSDIE env x y) reps }) + (_, Nothing) -> pure (nabla{ nabla_tm_st = TmSt (setIndirectSDIE env y x) reps }) -- Merge the info we have for x into the info for y (Just vi_x, Just vi_y) -> do -- This assert will probably trigger at some point... @@ -1097,16 +1105,16 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y let env_ind = setIndirectSDIE env x y -- Then sum up the refinement counters let env_refs = setEntrySDIE env_ind y vi_y - let delta_refs = delta{ delta_tm_st = TmSt env_refs reps } + let nabla_refs = nabla{ nabla_tm_st = TmSt env_refs reps } -- and then gradually merge every positive fact we have on x into y - let add_fact delta (cl, tvs, args) = addConCt delta y cl tvs args - delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x) + let add_fact nabla (cl, tvs, args) = addConCt nabla y cl tvs args + nabla_pos <- foldlM add_fact nabla_refs (vi_pos vi_x) -- Do the same for negative info - let add_refut delta nalt = addNotConCt delta y nalt - delta_neg <- foldlM add_refut delta_pos (pmAltConSetElems (vi_neg vi_x)) + let add_refut nabla nalt = addNotConCt nabla y nalt + nabla_neg <- foldlM add_refut nabla_pos (pmAltConSetElems (vi_neg vi_x)) -- vi_cache will be updated in addNotConCt, so we are good to -- go! - pure delta_neg + pure nabla_neg -- | Add a @x ~ K tvs args ts@ constraint. -- @addConCt x K tvs args ts@ extends the substitution with a solution @@ -1114,9 +1122,9 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y -- have on @x@, reject (@Nothing@) otherwise. -- -- See Note [TmState invariants]. -addConCt :: Delta -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Delta -addConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do - VI ty pos neg cache <- lift (initLookupVarInfo delta x) +addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla +addConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x alt tvs args = do + let VI ty pos neg bot cache = lookupVarInfo ts x -- First try to refute with a negative fact guard (not (elemPmAltConSet alt neg)) -- Then see if any of the other solutions (remember: each of them is an @@ -1132,10 +1140,19 @@ addConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do when (length args /= length other_args) $ lift $ tracePm "error" (ppr x <+> ppr alt <+> ppr args <+> ppr other_args) let tm_cts = zipWithEqual "addConCt" PmVarCt args other_args - MaybeT $ addPmCts delta (listToBag ty_cts `unionBags` listToBag tm_cts) + MaybeT $ addPmCts nabla (listToBag ty_cts `unionBags` listToBag tm_cts) Nothing -> do let pos' = (alt, tvs, args):pos - pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg cache)) reps} + let nabla_with bot = nabla{ nabla_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg bot cache)) reps} + -- Do (2) in Note [Coverage checking Newtype matches] + case (alt, args) of + (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc -> + case bot of + MaybeBot -> pure (nabla_with MaybeBot) + IsBot -> addBotCt (nabla_with MaybeBot) y + IsNotBot -> addNotBotCt (nabla_with MaybeBot) y + _ -> ASSERT( isPmAltConMatchStrict alt ) + pure (nabla_with IsNotBot) -- strict match ==> not ⊥ equateTys :: [Type] -> [Type] -> [PmCt] equateTys ts us = @@ -1184,9 +1201,9 @@ mkInhabitationCandidate x dc = do -- if it can. In this case, the candidates are the signature of the tycon, each -- one accompanied by the term- and type- constraints it gives rise to. -- See also Note [Checking EmptyCase Expressions] -inhabitationCandidates :: Delta -> Type +inhabitationCandidates :: Nabla -> Type -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) -inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do +inhabitationCandidates MkNabla{ nabla_ty_st = ty_st } ty = do pmTopNormaliseType ty_st ty >>= \case NoChange _ -> alts_to_check ty ty [] NormalisedByConstraints ty' -> alts_to_check ty' ty' [] @@ -1282,20 +1299,20 @@ we do the following: -- | A 'SatisfiabilityCheck' based on "NonVoid ty" constraints, e.g. Will -- check if the @strict_arg_tys@ are actually all inhabited. --- Returns the old 'Delta' if all the types are non-void according to 'Delta'. +-- Returns the old 'Nabla' if all the types are non-void according to 'Nabla'. tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck -tysAreNonVoid rec_env strict_arg_tys = SC $ \delta -> do - all_non_void <- checkAllNonVoid rec_env delta strict_arg_tys +tysAreNonVoid rec_env strict_arg_tys = SC $ \nabla -> do + all_non_void <- checkAllNonVoid rec_env nabla strict_arg_tys -- Check if each strict argument type is inhabitable pure $ if all_non_void - then Just delta + then Just nabla else Nothing -- | Implements two performance optimizations, as described in -- @Note [Strict argument type constraints]@. -checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool +checkAllNonVoid :: RecTcChecker -> Nabla -> [Type] -> DsM Bool checkAllNonVoid rec_ts amb_cs strict_arg_tys = do - let definitely_inhabited = definitelyInhabitedType (delta_ty_st amb_cs) + let definitely_inhabited = definitelyInhabitedType (nabla_ty_st amb_cs) tys_to_check <- filterOutM definitely_inhabited strict_arg_tys -- See Note [Fuel for the inhabitation test] let rec_max_bound | tys_to_check `lengthExceeds` 1 @@ -1310,7 +1327,7 @@ checkAllNonVoid rec_ts amb_cs strict_arg_tys = do -- See @Note [Strict argument type constraints]@. nonVoid :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit. - -> Delta -- ^ The ambient term/type constraints (known to be + -> Nabla -- ^ The ambient term/type constraints (known to be -- satisfiable). -> Type -- ^ The strict argument type. -> DsM Bool -- ^ 'True' if the strict argument type might be inhabited by @@ -1338,7 +1355,7 @@ nonVoid rec_ts amb_cs strict_arg_ty = do -- check if recursion is detected). -- -- See Note [Strict argument type constraints] - cand_is_inhabitable :: RecTcChecker -> Delta + cand_is_inhabitable :: RecTcChecker -> Nabla -> InhabitationCandidate -> DsM Bool cand_is_inhabitable rec_ts amb_cs (InhabitationCandidate{ ic_cs = new_cs @@ -1517,21 +1534,21 @@ on a list of strict argument types, we filter out all of the DI ones. -} -------------------------------------------- --- * Providing positive evidence for a Delta +-- * Providing positive evidence for a Nabla --- | @provideEvidence vs n delta@ returns a list of --- at most @n@ (but perhaps empty) refinements of @delta@ that instantiate +-- | @provideEvidence vs n nabla@ returns a list of +-- at most @n@ (but perhaps empty) refinements of @nabla@ that instantiate -- @vs@ to compatible constructor applications or wildcards. -- Negative information is only retained if literals are involved or when -- for recursive GADTs. -provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta] +provideEvidence :: [Id] -> Int -> Nabla -> DsM [Nabla] provideEvidence = go where go _ 0 _ = pure [] - go [] _ delta = pure [delta] - go (x:xs) n delta = do - tracePm "provideEvidence" (ppr x $$ ppr xs $$ ppr delta $$ ppr n) - VI _ pos neg _ <- initLookupVarInfo delta x + go [] _ nabla = pure [nabla] + go (x:xs) n nabla = do + tracePm "provideEvidence" (ppr x $$ ppr xs $$ ppr nabla $$ ppr n) + let VI _ pos neg _ _ = lookupVarInfo (nabla_tm_st nabla) x case pos of _:_ -> do -- All solutions must be valid at once. Try to find candidates for their @@ -1544,56 +1561,58 @@ provideEvidence = go -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@ -- and @z@ that is valid at the same time. These constitute arg_vas below. let arg_vas = concatMap (\(_cl, _tvs, args) -> args) pos - go (arg_vas ++ xs) n delta + go (arg_vas ++ xs) n nabla [] -- When there are literals involved, just print negative info -- instead of listing missed constructors | notNull [ l | PmAltLit l <- pmAltConSetElems neg ] - -> go xs n delta - [] -> try_instantiate x xs n delta + -> go xs n nabla + [] -> try_instantiate x xs n nabla -- | Tries to instantiate a variable by possibly following the chain of -- newtypes and then instantiating to all ConLikes of the wrapped type's -- minimal residual COMPLETE set. - try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta] + try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla] -- Convention: x binds the outer constructor in the chain, y the inner one. - try_instantiate x xs n delta = do - (_src_ty, dcs, core_ty) <- tntrGuts <$> pmTopNormaliseType (delta_ty_st delta) (idType x) - let build_newtype (x, delta) (_ty, dc, arg_ty) = do + try_instantiate x xs n nabla = do + (_src_ty, dcs, core_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (idType x) + let build_newtype (x, nabla) (_ty, dc, arg_ty) = do y <- lift $ mkPmId arg_ty -- Newtypes don't have existentials (yet?!), so passing an empty -- list as ex_tvs. - delta' <- addConCt delta x (PmAltConLike (RealDataCon dc)) [] [y] - pure (y, delta') - runMaybeT (foldlM build_newtype (x, delta) dcs) >>= \case + nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y] + pure (y, nabla') + runMaybeT (foldlM build_newtype (x, nabla) dcs) >>= \case Nothing -> pure [] - Just (y, newty_delta) -> do + Just (y, newty_nabla) -> do -- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥. - pm <- vi_cache <$> initLookupVarInfo newty_delta y - mb_cls <- pickMinimalCompleteSet newty_delta pm + let vi = lookupVarInfo (nabla_tm_st newty_nabla) y + vi <- initPossibleMatches (nabla_ty_st newty_nabla) vi + mb_cls <- pickMinimalCompleteSet newty_nabla (vi_cache vi) case uniqDSetToList <$> mb_cls of - Just cls@(_:_) -> instantiate_cons y core_ty xs n newty_delta cls - Just [] | not (canDiverge newty_delta y) -> pure [] - -- Either ⊥ is still possible (think Void) or there are no COMPLETE - -- sets available, so we can assume it's inhabited - _ -> go xs n newty_delta - - instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta] + Just cls -> do + nablas <- instantiate_cons y core_ty xs n newty_nabla cls + if null nablas && vi_bot vi /= IsNotBot + then go xs n newty_nabla -- bot is still possible. Display a wildcard! + else pure nablas + Nothing -> go xs n newty_nabla -- no COMPLETE sets ==> inhabited + + instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla] instantiate_cons _ _ _ _ _ [] = pure [] instantiate_cons _ _ _ 0 _ _ = pure [] - instantiate_cons _ ty xs n delta _ + instantiate_cons _ ty xs n nabla _ -- We don't want to expose users to GHC-specific constructors for Int etc. | fmap (isTyConTriviallyInhabited . fst) (splitTyConApp_maybe ty) == Just True - = go xs n delta - instantiate_cons x ty xs n delta (cl:cls) = do + = go xs n nabla + instantiate_cons x ty xs n nabla (cl:cls) = do env <- dsGetFamInstEnvs case guessConLikeUnivTyArgsFromResTy env ty cl of - Nothing -> pure [delta] -- No idea how to refine this one, so just finish off with a wildcard + Nothing -> pure [nabla] -- No idea how to refine this one, so just finish off with a wildcard Just arg_tys -> do (tvs, arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl let new_tm_cs = unitBag (TmConCt x (PmAltConLike cl) tvs arg_vars) -- Now check satifiability - mb_delta <- pmIsSatisfiable delta new_ty_cs new_tm_cs strict_arg_tys + mb_nabla <- pmIsSatisfiable nabla new_ty_cs new_tm_cs strict_arg_tys tracePm "instantiate_cons" (vcat [ ppr x , ppr (idType x) , ppr ty @@ -1602,21 +1621,21 @@ provideEvidence = go , ppr new_tm_cs , ppr new_ty_cs , ppr strict_arg_tys - , ppr delta - , ppr mb_delta + , ppr nabla + , ppr mb_nabla , ppr n ]) - con_deltas <- case mb_delta of + con_nablas <- case mb_nabla of Nothing -> pure [] -- NB: We don't prepend arg_vars as we don't have any evidence on -- them and we only want to split once on a data type. They are -- inhabited, otherwise pmIsSatisfiable would have refuted. - Just delta' -> go xs n delta' - other_cons_deltas <- instantiate_cons x ty xs (n - length con_deltas) delta cls - pure (con_deltas ++ other_cons_deltas) + Just nabla' -> go xs n nabla' + other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls + pure (con_nablas ++ other_cons_nablas) -pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet) +pickMinimalCompleteSet :: Nabla -> PossibleMatches -> DsM (Maybe ConLikeSet) pickMinimalCompleteSet _ NoPM = pure Nothing --- TODO: First prune sets with type info in delta. But this is good enough for +-- TODO: First prune sets with type info in nabla. But this is good enough for -- now and less costly. See #17386. pickMinimalCompleteSet _ (PM clss) = do tracePm "pickMinimalCompleteSet" (ppr $ NonEmpty.toList clss) @@ -1626,14 +1645,14 @@ pickMinimalCompleteSet _ (PM clss) = do -- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically -- equivalent to @e'@) we encountered earlier, or a fresh identifier if -- there weren't any such constraints. -representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id) -representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e - | Just rep <- lookupCoreMap reps e = pure (delta, rep) +representCoreExpr :: Nabla -> CoreExpr -> DsM (Nabla, Id) +representCoreExpr nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_reps = reps } } e + | Just rep <- lookupCoreMap reps e = pure (nabla, rep) | otherwise = do rep <- mkPmId (exprType e) let reps' = extendCoreMap reps e rep - let delta' = delta{ delta_tm_st = ts{ ts_reps = reps' } } - pure (delta', rep) + let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } } + pure (nabla', rep) -- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based -- on the shape of the 'CoreExpr' @e@. Examples: @@ -1647,16 +1666,16 @@ representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e -- for other literals. See 'coreExprAsPmLit'. -- * Finally, if we have @let x = e@ and we already have seen @let y = e@, we -- want to record @x ~ y@. -addCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta -addCoreCt delta x e = do +addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla +addCoreCt nabla x e = do simpl_opts <- initSimpleOpts <$> getDynFlags let e' = simpleOptExpr simpl_opts e - lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e') - execStateT (core_expr x e') delta + -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e') + execStateT (core_expr x e') nabla where -- | Takes apart a 'CoreExpr' and tries to extract as much information about -- literals and constructor applications as possible. - core_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) () + core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) () -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon -- This is the right thing for casts involving data family instances and -- their representation TyCon, though (which are not visible in source @@ -1681,7 +1700,7 @@ addCoreCt delta x e = do -- See Note [Detecting pattern synonym applications in expressions] | Var y <- e, Nothing <- isDataConId_maybe x -- We don't consider DataCons flexible variables - = modifyT (\delta -> addVarCt delta x y) + = modifyT (\nabla -> addVarCt nabla x y) | otherwise -- Any other expression. Try to find other uses of a semantically -- equivalent expression and represent them by the same variable! @@ -1699,13 +1718,13 @@ addCoreCt delta x e = do -- see if we already encountered a constraint @let y = e'@ with @e'@ -- semantically equivalent to @e@, in which case we may add the constraint -- @x ~ y@. - equate_with_similar_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) () + equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) () equate_with_similar_expr x e = do - rep <- StateT $ \delta -> swap <$> lift (representCoreExpr delta e) + rep <- StateT $ \nabla -> swap <$> lift (representCoreExpr nabla e) -- Note that @rep == x@ if we encountered @e@ for the first time. - modifyT (\delta -> addVarCt delta x rep) + modifyT (\nabla -> addVarCt nabla x rep) - bind_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id + bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id bind_expr e = do x <- lift (lift (mkPmId (exprType e))) core_expr x e @@ -1713,10 +1732,12 @@ addCoreCt delta x e = do -- | Look at @let x = K taus theta es@ and generate the following -- constraints (assuming universals were dropped from @taus@ before): - -- 1. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@ - -- 2. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ - -- 3. @x ~ K as ys@ - data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Delta (MaybeT DsM) () + -- 1. @x /~ ⊥@ if 'K' is not a Newtype constructor. + -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@ + -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ + -- 4. @x ~ K as ys@ + -- This is quite similar to PmCheck.pmConCts. + data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) () data_con_app x in_scope dc args = do let dc_ex_tvs = dataConExTyCoVars dc arty = dataConSourceArity dc @@ -1726,20 +1747,27 @@ addCoreCt delta x e = do uniq_supply <- lift $ lift $ getUniqueSupplyM let (_, ex_tvs) = cloneTyVarBndrs (mkEmptyTCvSubst in_scope) dc_ex_tvs uniq_supply ty_cts = equateTys (map mkTyVarTy ex_tvs) ex_tys - -- 1. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703 - modifyT $ \delta -> MaybeT $ addPmCts delta (listToBag ty_cts) - -- 2. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ + -- 1. @x /~ ⊥@ if 'K' is not a Newtype constructor (#18341) + when (not (isNewDataCon dc)) $ + modifyT $ \nabla -> addNotBotCt nabla x + -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703 + modifyT $ \nabla -> MaybeT $ addPmCts nabla (listToBag ty_cts) + -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ arg_ids <- traverse bind_expr vis_args - -- 3. @x ~ K as ys@ + -- 4. @x ~ K as ys@ pm_alt_con_app x (PmAltConLike (RealDataCon dc)) ex_tvs arg_ids -- | Adds a literal constraint, i.e. @x ~ 42@. - pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) () - pm_lit x lit = pm_alt_con_app x (PmAltLit lit) [] [] + -- Also we assume that literal expressions won't diverge, so this + -- will add a @x ~/ ⊥@ constraint. + pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) () + pm_lit x lit = do + modifyT $ \nabla -> addNotBotCt nabla x + pm_alt_con_app x (PmAltLit lit) [] [] -- | Adds the given constructor application as a solution for @x@. - pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Delta (MaybeT DsM) () - pm_alt_con_app x con tvs args = modifyT $ \delta -> addConCt delta x con tvs args + pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) () + pm_alt_con_app x con tvs args = modifyT $ \nabla -> addConCt nabla x con tvs args -- | Like 'modify', but with an effectful modifier action modifyT :: Monad m => (s -> m s) -> StateT s m () diff --git a/compiler/GHC/HsToCore/PmCheck/Ppr.hs b/compiler/GHC/HsToCore/PmCheck/Ppr.hs index dc1739908f..557fd08c43 100644 --- a/compiler/GHC/HsToCore/PmCheck/Ppr.hs +++ b/compiler/GHC/HsToCore/PmCheck/Ppr.hs @@ -2,7 +2,7 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} --- | Provides factilities for pretty-printing 'Delta's in a way appropriate for +-- | Provides factilities for pretty-printing 'Nabla's in a way appropriate for -- user facing pattern match warnings. module GHC.HsToCore.PmCheck.Ppr ( pprUncovered @@ -42,8 +42,8 @@ import GHC.HsToCore.PmCheck.Oracle -- -- When the set of refutable shapes contains more than 3 elements, the -- additional elements are indicated by "...". -pprUncovered :: Delta -> [Id] -> SDoc -pprUncovered delta vas +pprUncovered :: Nabla -> [Id] -> SDoc +pprUncovered nabla vas | isNullUDFM refuts = fsep vec -- there are no refutations | otherwise = hang (fsep vec) 4 $ text "where" <+> vcat (map (pprRefutableShapes . snd) (udfmToList refuts)) @@ -54,8 +54,8 @@ pprUncovered delta vas | [_] <- vas = topPrec | otherwise = appPrec ppr_action = mapM (pprPmVar init_prec) vas - (vec, renamings) = runPmPpr delta ppr_action - refuts = prettifyRefuts delta renamings + (vec, renamings) = runPmPpr nabla ppr_action + refuts = prettifyRefuts nabla renamings -- | Output refutable shapes of a variable in the form of @var is not one of {2, -- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is @@ -98,21 +98,21 @@ substitution to the vectors before printing them out (see function `pprOne' in -- | Extract and assigns pretty names to constraint variables with refutable -- shapes. -prettifyRefuts :: Delta -> DIdEnv SDoc -> DIdEnv (SDoc, [PmAltCon]) -prettifyRefuts delta = listToUDFM_Directly . map attach_refuts . udfmToList +prettifyRefuts :: Nabla -> DIdEnv SDoc -> DIdEnv (SDoc, [PmAltCon]) +prettifyRefuts nabla = listToUDFM_Directly . map attach_refuts . udfmToList where - attach_refuts (u, sdoc) = (u, (sdoc, lookupRefuts delta u)) + attach_refuts (u, sdoc) = (u, (sdoc, lookupRefuts nabla u)) -type PmPprM a = RWS Delta () (DIdEnv SDoc, [SDoc]) a +type PmPprM a = RWS Nabla () (DIdEnv SDoc, [SDoc]) a -- Try nice names p,q,r,s,t before using the (ugly) t_i nameList :: [SDoc] nameList = map text ["p","q","r","s","t"] ++ [ text ('t':show u) | u <- [(0 :: Int)..] ] -runPmPpr :: Delta -> PmPprM a -> (a, DIdEnv SDoc) -runPmPpr delta m = case runRWS m delta (emptyDVarEnv, nameList) of +runPmPpr :: Nabla -> PmPprM a -> (a, DIdEnv SDoc) +runPmPpr nabla m = case runRWS m nabla (emptyDVarEnv, nameList) of (a, (renamings, _), _) -> (a, renamings) -- | Allocates a new, clean name for the given 'Id' if it doesn't already have @@ -129,8 +129,8 @@ getCleanName x = do checkRefuts :: Id -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached checkRefuts x = do - delta <- ask - case lookupRefuts delta x of + nabla <- ask + case lookupRefuts nabla x of [] -> pure Nothing -- Will just be a wildcard later on _ -> Just <$> getCleanName x @@ -144,8 +144,8 @@ pprPmVar :: PprPrec -> Id -> PmPprM SDoc -- The useful information in the latter case is the constructor that we missed, -- not the types of the wildcards in the places that aren't matched as a result. pprPmVar prec x = do - delta <- ask - case lookupSolution delta x of + nabla <- ask + case lookupSolution nabla x of Just (alt, _tvs, args) -> pprPmAltCon prec alt args Nothing -> fromMaybe typed_wildcard <$> checkRefuts x where @@ -160,24 +160,24 @@ pprPmVar prec x = do pprPmAltCon :: PprPrec -> PmAltCon -> [Id] -> PmPprM SDoc pprPmAltCon _prec (PmAltLit l) _ = pure (ppr l) pprPmAltCon prec (PmAltConLike cl) args = do - delta <- ask - pprConLike delta prec cl args + nabla <- ask + pprConLike nabla prec cl args -pprConLike :: Delta -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc -pprConLike delta _prec cl args - | Just pm_expr_list <- pmExprAsList delta (PmAltConLike cl) args +pprConLike :: Nabla -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc +pprConLike nabla _prec cl args + | Just pm_expr_list <- pmExprAsList nabla (PmAltConLike cl) args = case pm_expr_list of NilTerminated list -> brackets . fsep . punctuate comma <$> mapM (pprPmVar appPrec) list WcVarTerminated pref x -> parens . fcat . punctuate colon <$> mapM (pprPmVar appPrec) (toList pref ++ [x]) -pprConLike _delta _prec (RealDataCon con) args +pprConLike _nabla _prec (RealDataCon con) args | isUnboxedTupleDataCon con , let hash_parens doc = text "(#" <+> doc <+> text "#)" = hash_parens . fsep . punctuate comma <$> mapM (pprPmVar appPrec) args | isTupleDataCon con = parens . fsep . punctuate comma <$> mapM (pprPmVar appPrec) args -pprConLike _delta prec cl args +pprConLike _nabla prec cl args | conLikeIsInfix cl = case args of [x, y] -> do x' <- pprPmVar funPrec x y' <- pprPmVar funPrec y @@ -202,11 +202,11 @@ data PmExprList -- ending in a wildcard variable x (of list type). Should be pretty-printed as -- (1:2:_). -- * @pmExprAsList [] == Just ('NilTerminated' [])@ -pmExprAsList :: Delta -> PmAltCon -> [Id] -> Maybe PmExprList -pmExprAsList delta = go_con [] +pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList +pmExprAsList nabla = go_con [] where go_var rev_pref x - | Just (alt, _tvs, args) <- lookupSolution delta x + | Just (alt, _tvs, args) <- lookupSolution nabla x = go_con rev_pref alt args go_var rev_pref x | Just pref <- nonEmpty (reverse rev_pref) diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs index 0014935ceb..aa778cd34b 100644 --- a/compiler/GHC/HsToCore/PmCheck/Types.hs +++ b/compiler/GHC/HsToCore/PmCheck/Types.hs @@ -15,6 +15,7 @@ Author: George Karachalias <george.karachalias@cs.kuleuven.be> module GHC.HsToCore.PmCheck.Types ( -- * Representations for Literals and AltCons PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType, + isPmAltConMatchStrict, pmAltConImplBangs, -- ** Equality on 'PmAltCon's PmEquality(..), eqPmAltCon, @@ -35,8 +36,8 @@ module GHC.HsToCore.PmCheck.Types ( setIndirectSDIE, setEntrySDIE, traverseSDIE, -- * The pattern match oracle - VarInfo(..), TmState(..), TyState(..), Delta(..), - Deltas(..), initDeltas, liftDeltasM + BotInfo(..), VarInfo(..), TmState(..), TyState(..), Nabla(..), + Nablas(..), initNablas, liftNablasM ) where #include "HsVersions.h" @@ -226,6 +227,19 @@ pmAltConType :: PmAltCon -> [Type] -> Type pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys +-- | Is a match on this constructor forcing the match variable? +-- True of data constructors, literals and pattern synonyms (#17357), but not of +-- newtypes. +-- See Note [Coverage checking Newtype matches] in "GHC.HsToCore.PmCheck.Oracle". +isPmAltConMatchStrict :: PmAltCon -> Bool +isPmAltConMatchStrict PmAltLit{} = True +isPmAltConMatchStrict (PmAltConLike PatSynCon{}) = True -- #17357 +isPmAltConMatchStrict (PmAltConLike (RealDataCon dc)) = not (isNewDataCon dc) + +pmAltConImplBangs :: PmAltCon -> [HsImplBang] +pmAltConImplBangs PmAltLit{} = [] +pmAltConImplBangs (PmAltConLike con) = conLikeImplBangs con + {- Note [Undecidable Equality for PmAltCons] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Equality on overloaded literals is undecidable in the general case. Consider @@ -477,6 +491,13 @@ instance Outputable a => Outputable (Shared a) where instance Outputable a => Outputable (SharedDIdEnv a) where ppr (SDIE env) = ppr env +-- | See 'vi_bot'. +data BotInfo + = IsBot + | IsNotBot + | MaybeBot + deriving Eq + -- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These -- entries are possibly shared when we figure out that two variables must be -- equal, thus represent the same set of values. @@ -531,6 +552,13 @@ data VarInfo -- because files like Cabal's `LicenseId` define relatively huge enums -- that lead to quadratic or worse behavior. + , vi_bot :: BotInfo + -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and + -- @x ≁ ⊥@ constraints. E.g. + -- * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@. + -- * 'IsBot': @x ~ ⊥@ + -- * 'IsNotBot': @x ≁ ⊥@ + , vi_cache :: !PossibleMatches -- ^ A cache of the associated COMPLETE sets. At any time a superset of -- possible constructors of each COMPLETE set. So, if it's not in here, we @@ -538,14 +566,19 @@ data VarInfo -- to recognise completion of a COMPLETE set efficiently for large enums. } +instance Outputable BotInfo where + ppr MaybeBot = empty + ppr IsBot = text "~⊥" + ppr IsNotBot = text "≁⊥" + -- | Not user-facing. instance Outputable TmState where ppr (TmSt state reps) = ppr state $$ ppr reps -- | Not user-facing. instance Outputable VarInfo where - ppr (VI ty pos neg cache) - = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache])) + ppr (VI ty pos neg bot cache) + = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr bot, ppr cache])) -- | Initial state of the term oracle. initTmState :: TmState @@ -563,37 +596,38 @@ instance Outputable TyState where initTyState :: TyState initTyState = TySt emptyBag --- | An inert set of canonical (i.e. mutually compatible) term and type --- constraints. -data Delta = MkDelta { delta_ty_st :: TyState -- Type oracle; things like a~Int - , delta_tm_st :: TmState } -- Term oracle; things like x~Nothing +-- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of +-- canonical (i.e. mutually compatible) term and type constraints that form the +-- refinement type's predicate. +data Nabla = MkNabla { nabla_ty_st :: TyState -- Type oracle; things like a~Int + , nabla_tm_st :: TmState } -- Term oracle; things like x~Nothing --- | An initial delta that is always satisfiable -initDelta :: Delta -initDelta = MkDelta initTyState initTmState +-- | An initial nabla that is always satisfiable +initNabla :: Nabla +initNabla = MkNabla initTyState initTmState -instance Outputable Delta where - ppr delta = hang (text "Delta") 2 $ vcat [ +instance Outputable Nabla where + ppr nabla = hang (text "Nabla") 2 $ vcat [ -- intentionally formatted this way enable the dev to comment in only -- the info she needs - ppr (delta_tm_st delta), - ppr (delta_ty_st delta) + ppr (nabla_tm_st nabla), + ppr (nabla_ty_st nabla) ] --- | A disjunctive bag of 'Delta's, representing a refinement type. -newtype Deltas = MkDeltas (Bag Delta) +-- | A disjunctive bag of 'Nabla's, representing a refinement type. +newtype Nablas = MkNablas (Bag Nabla) -initDeltas :: Deltas -initDeltas = MkDeltas (unitBag initDelta) +initNablas :: Nablas +initNablas = MkNablas (unitBag initNabla) -instance Outputable Deltas where - ppr (MkDeltas deltas) = ppr deltas +instance Outputable Nablas where + ppr (MkNablas nablas) = ppr nablas -instance Semigroup Deltas where - MkDeltas l <> MkDeltas r = MkDeltas (l `unionBags` r) +instance Semigroup Nablas where + MkNablas l <> MkNablas r = MkNablas (l `unionBags` r) -instance Monoid Deltas where - mempty = MkDeltas emptyBag +instance Monoid Nablas where + mempty = MkNablas emptyBag -liftDeltasM :: Monad m => (Delta -> m (Maybe Delta)) -> Deltas -> m Deltas -liftDeltasM f (MkDeltas ds) = MkDeltas . catBagMaybes <$> (traverse f ds) +liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas +liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds) diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs-boot b/compiler/GHC/HsToCore/PmCheck/Types.hs-boot index a7c472faa6..a0505bce9d 100644 --- a/compiler/GHC/HsToCore/PmCheck/Types.hs-boot +++ b/compiler/GHC/HsToCore/PmCheck/Types.hs-boot @@ -2,8 +2,8 @@ module GHC.HsToCore.PmCheck.Types where import GHC.Data.Bag -data Delta +data Nabla -newtype Deltas = MkDeltas (Bag Delta) +newtype Nablas = MkNablas (Bag Nabla) -initDeltas :: Deltas +initNablas :: Nablas |