[Git][ghc/ghc][wip/T18341] PmCheck: Handle ⊥ and strict fields correctly (#18341)
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Aug 31 17:19:37 UTC 2020
Sebastian Graf pushed to branch wip/T18341 at Glasgow Haskell Compiler / GHC
Commits:
42f9bf20 by Sebastian Graf at 2020-08-31T19:19:21+02:00
PmCheck: Handle ⊥ and strict fields correctly (#18341)
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.
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.
- - - - -
27 changed files:
- .gitignore
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Data/Bag.hs
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/HsToCore/GuardedRHSs.hs
- compiler/GHC/HsToCore/Match.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Ppr.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs-boot
- compiler/GHC/Tc/Types.hs
- + testsuite/tests/pmcheck/should_compile/T10183.hs
- testsuite/tests/pmcheck/should_compile/T17340.stderr
- + testsuite/tests/pmcheck/should_compile/T17378.hs
- + testsuite/tests/pmcheck/should_compile/T17725.hs
- + testsuite/tests/pmcheck/should_compile/T17725.stderr
- + testsuite/tests/pmcheck/should_compile/T17729.hs
- + testsuite/tests/pmcheck/should_compile/T17729.stderr
- + testsuite/tests/pmcheck/should_compile/T18273.hs
- + testsuite/tests/pmcheck/should_compile/T18341.hs
- + testsuite/tests/pmcheck/should_compile/T18341.stderr
- testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs
- testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
.gitignore
=====================================
@@ -232,3 +232,6 @@ ghc.nix/
# Tooling - vscode
.vscode
+
+# Tooling - ghcide
+*.hiedb
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -53,7 +53,7 @@ module GHC.Core.DataCon (
-- ** Predicates on DataCons
isNullarySrcDataCon, isNullaryRepDataCon, isTupleDataCon, isUnboxedTupleCon,
isUnboxedSumCon,
- isVanillaDataCon, classDataCon, dataConCannotMatch,
+ isVanillaDataCon, isNewDataCon, classDataCon, dataConCannotMatch,
dataConUserTyVarsArePermuted,
isBanged, isMarkedStrict, eqHsBang, isSrcStrict, isSrcUnpacked,
specialPromotedDc,
@@ -1477,6 +1477,10 @@ isUnboxedSumCon (MkData {dcRepTyCon = tc}) = isUnboxedSumTyCon tc
isVanillaDataCon :: DataCon -> Bool
isVanillaDataCon dc = dcVanilla dc
+-- | Is this the 'DataCon' of a newtype?
+isNewDataCon :: DataCon -> Bool
+isNewDataCon dc = isNewTyCon (dataConTyCon dc)
+
-- | Should this DataCon be allowed in a type even without -XDataKinds?
-- Currently, only Lifted & Unlifted
specialPromotedDc :: DataCon -> Bool
=====================================
compiler/GHC/Data/Bag.hs
=====================================
@@ -6,7 +6,7 @@
Bag: an unordered collection with duplicates
-}
-{-# LANGUAGE ScopedTypeVariables, CPP, DeriveFunctor #-}
+{-# LANGUAGE ScopedTypeVariables, CPP, DeriveFunctor, TypeFamilies #-}
module GHC.Data.Bag (
Bag, -- abstract type
@@ -27,9 +27,9 @@ module GHC.Data.Bag (
import GHC.Prelude
+import GHC.Exts ( IsList(..) )
import GHC.Utils.Outputable
import GHC.Utils.Misc
-
import GHC.Utils.Monad
import Control.Monad
import Data.Data
@@ -333,3 +333,8 @@ instance Traversable Bag where
traverse f (UnitBag x) = UnitBag <$> f x
traverse f (TwoBags b1 b2) = TwoBags <$> traverse f b1 <*> traverse f b2
traverse f (ListBag xs) = ListBag <$> traverse f xs
+
+instance IsList (Bag a) where
+ type Item (Bag a) = a
+ fromList = listToBag
+ toList = bagToList
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -184,8 +184,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'
=====================================
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
=====================================
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 at .
-}
-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
=====================================
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
=====================================
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
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -28,14 +28,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 'CIRBCollector' such
-- as 'collectMatch'. Follows the R function from Figure 6 of the paper.
-- 4. Format and report uncovered patterns and redundant equations ('CIRB')
-- with 'formatReportWarnings'. Basically job of the G function, plus proper
-- pretty printing of the warnings (Section 5.4 of the paper).
--- 5. Return 'Deltas' reaching syntactic sub-components for
+-- 5. Return 'Nablas' reaching syntactic sub-components for
-- Note [Long-distance information]. See Section 4.1 of the paper.
module GHC.HsToCore.PmCheck (
-- Checking and printing
@@ -68,7 +68,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)
@@ -103,7 +102,7 @@ import Data.Coerce
covCheckPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
-- See Note [covCheckPatBind only checks PatBindRhs]
covCheckPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
- missing <- getPmDeltas
+ missing <- getPmNablas
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
@@ -112,17 +111,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 <- getPmDeltas
+ missing <- getPmNablas
tracePm "covCheckGRHSs" (hang (vcat [ppr ctxt
, text "Guards:"])
2
@@ -140,7 +139,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
@@ -150,13 +149,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 <- getPmDeltas
+ !missing <- getPmNablas
tracePm "covCheckMatches {" $
hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
2
@@ -207,7 +206,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.
-}
--
@@ -233,8 +232,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
@@ -298,15 +297,15 @@ newtype GrdPatBind =
-- (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].
}
@@ -434,7 +433,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
@@ -618,7 +617,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])
@@ -638,14 +637,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 at .
+ -- 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 at .
-- 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)
@@ -659,19 +658,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 GrdPatBind
-- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
@@ -759,30 +750,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 at . 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -834,7 +840,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
@@ -852,23 +858,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 at .
-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:
@@ -910,23 +916,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 at .
+-- 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 at .
+--
+-- 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
@@ -939,31 +956,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 }
@@ -997,7 +1015,7 @@ checkGRHS (GrdGRHS { gg_grds = grds, gg_rhs = rhs_info }) =
checkEmptyCase :: GrdEmptyCase -> CheckAction AnnEmptyCase
checkEmptyCase (GrdEmptyCase { ge_var = var }) = CA $ \inc -> do
- unc <- addPmCtDeltas inc (PmNotBotCt var)
+ unc <- addPmCtNablas inc (PmNotBotCt var)
pure CheckResult { cr_ret = AnnEmptyCase, cr_uncov = unc, cr_approx = mempty }
checkPatBind :: GrdPatBind -> CheckAction AnnPatBind
@@ -1007,7 +1025,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
@@ -1016,13 +1034,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
@@ -1093,41 +1111,41 @@ addRedundantBangs red_bangs cirb =
-- 1. A 'CIRB', classifying every encountered RHS in the tree as
-- redundant, inaccessible or covered.
-- 2. A piece of long-distance information @ldi@, consisting of a
--- nesting of 'Deltas' mirroring tree structure.
+-- nesting of 'Nablas' mirroring tree structure.
-- For example, 'collectMatchGroup' operates on a Match Group and thus
--- returns a list of 'Deltas' for the pattern part of each Match, as well as
--- a further nested list of 'Deltas' for each of the GRHS of the Match.
+-- returns a list of 'Nablas' for the pattern part of each Match, as well as
+-- a further nested list of 'Nablas' for each of the GRHS of the Match.
type CIRBCollector ann ldi = ann -> DsM (CIRB, ldi)
--- | Checks the 'Deltas' in a 'RedSets' for inhabitants and returns
+-- | 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. The new inhabited Covered set for long-distance information.
-- See Note [Recovering from unsatisfiable pattern-matching constraints].
--- 4. All source bangs whose 'Deltas' were empty, which means they are
+-- 4. All source bangs whose 'Nablas' were empty, which means they are
-- redundant.
-testRedSets :: Deltas -> RedSets -> DsM (Bool, Bool, Deltas, OrdList SrcInfo)
+testRedSets :: Nablas -> RedSets -> DsM (Bool, Bool, Nablas, OrdList SrcInfo)
testRedSets ldi RedSets { rs_cov = cov, rs_div = div, rs_bangs = bangs } = do
is_covered <- isInhabited cov
may_diverge <- isInhabited div
- red_bangs <- flip mapMaybeM (fromOL bangs) $ \(deltas, bang) -> do
- isInhabited deltas >>= \case
+ red_bangs <- flip mapMaybeM (fromOL bangs) $ \(nablas, bang) -> do
+ isInhabited nablas >>= \case
True -> pure Nothing
False -> pure (Just bang)
-- See Note [Recovering from unsatisfiable pattern-matching constraints]
- -- Deltas for long-distance info: Use (non-empty!) fallback ldi if Covered
+ -- Nablas for long-distance info: Use (non-empty!) fallback ldi if Covered
-- set was empty
let ldi'
| is_covered = cov
| otherwise = ldi
pure (is_covered, may_diverge, ldi', toOL red_bangs)
-collectMatchGroup :: Deltas -> CIRBCollector AnnMatchGroup (NonEmpty (Deltas, NonEmpty Deltas))
+collectMatchGroup :: Nablas -> CIRBCollector AnnMatchGroup (NonEmpty (Nablas, NonEmpty Nablas))
collectMatchGroup ldi (AnnMatchGroup matches) = do
(cirbs, ldis) <- NE.unzip <$> traverse (collectMatch ldi) matches
pure (Semi.sconcat cirbs, ldis)
-collectMatch :: Deltas -> CIRBCollector AnnMatch (Deltas, NonEmpty Deltas)
+collectMatch :: Nablas -> CIRBCollector AnnMatch (Nablas, NonEmpty Nablas)
collectMatch ldi AnnMatch { am_red = red, am_grhss = grhss } = do
(is_covered, may_diverge, ldi', red_bangs) <- testRedSets ldi red
(cirb, ldis) <- collectGRHSs ldi' grhss
@@ -1138,12 +1156,12 @@ collectMatch ldi AnnMatch { am_red = red, am_grhss = grhss } = do
$ cirb
pure (cirb', (ldi', ldis))
-collectGRHSs :: Deltas -> CIRBCollector (NonEmpty AnnGRHS) (NonEmpty Deltas)
+collectGRHSs :: Nablas -> CIRBCollector (NonEmpty AnnGRHS) (NonEmpty Nablas)
collectGRHSs ldi grhss = do
(cirbs, ldis) <- NE.unzip <$> traverse (collectGRHS ldi) grhss
pure (Semi.sconcat cirbs, ldis)
-collectGRHS :: Deltas -> CIRBCollector AnnGRHS Deltas
+collectGRHS :: Nablas -> CIRBCollector AnnGRHS Nablas
collectGRHS ldi AnnGRHS { ag_red = red, ag_rhs = info } = do
(is_covered, may_diverge, ldi', red_bangs) <- testRedSets ldi red
let cirb | is_covered = mempty { cirb_cov = unitOL info }
@@ -1156,9 +1174,9 @@ collectEmptyCase _ = pure (mempty, ())
collectPatBind :: CIRBCollector AnnPatBind ()
-- We don't make use of long-distance information in pattern bindings, hence
--- @()@ instead of some 'Deltas'.
+-- @()@ instead of some 'Nablas'.
collectPatBind (AnnPatBind grhs) = do
- -- use 'mempty' as fallback 'Deltas' because we discard it anyway
+ -- use 'mempty' as fallback 'Nablas' because we discard it anyway
(cirb, _) <- collectGRHS mempty grhs
pure (cirb, ())
@@ -1236,10 +1254,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)
@@ -1254,14 +1272,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
@@ -1386,21 +1404,21 @@ 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 <- getPmDeltas
- deltas' <- unsafeInterleaveM $ do
- deltas' <- ext deltas
- inh <- isInhabited deltas'
+locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a
+locallyExtendPmNablas ext k = do
+ nablas <- getPmNablas
+ nablas' <- unsafeInterleaveM $ do
+ nablas' <- ext nablas
+ inh <- isInhabited nablas'
-- If adding a constraint would lead to a contradiction, don't add it.
-- See Note [Recovering from unsatisfiable pattern-matching constraints]
-- for why this is done.
if inh
- then pure deltas'
- else pure deltas
- updPmDeltas deltas' k
+ then pure nablas'
+ else pure nablas
+ updPmNablas nablas' k
-- | Add in-scope type constraints if the coverage checker might run and then
-- run the given action.
@@ -1408,7 +1426,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
@@ -1419,8 +1437,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.
@@ -1448,10 +1466,10 @@ of @f at .
To achieve similar reasoning in the coverage checker, we keep track of the set
of values that can reach a particular program point (often loosely referred to
-as "Covered set") in 'GHC.HsToCore.Monad.dsl_deltas'.
-We fill that set with Covered Deltas returned by the exported checking
+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'.
@@ -1472,9 +1490,9 @@ unreachable.
We can do better than this, by making sure that the Covered set used for
Note [Long-distance information] is always inhabited.
For Covered sets returned by the exported checking functions, that is ensured
-in 'testRedSets', which takes and returns a non-empty fallback 'Deltas' in case
+in 'testRedSets', which takes and returns a non-empty fallback 'Nablas' in case
the refined Covered set became uninhabited.
Also, whenever "external" knowledge from a type constraint or case scrutinee is
-integrated, we only commit that knowledge to 'GHC.HsToCore.Monad.dsl_deltas' if
-the set remains inhabited. That check happens in 'locallyExtendPmDeltas'.
+integrated, we only commit that knowledge to 'GHC.HsToCore.Monad.dsl_nablas' if
+the set remains inhabited. That check happens in 'locallyExtendPmNablas'.
-}
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -4,22 +4,25 @@ Authors: George Karachalias <george.karachalias at cs.kuleuven.be>
Ryan Scott <ryan.gl.scott at 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
@@ -153,12 +156,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)
@@ -169,8 +167,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:
@@ -179,22 +177,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,
@@ -213,13 +211,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 =
@@ -492,21 +490,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')
{- *********************************************************************
@@ -618,21 +616,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 at VI{ vi_ty = ty, vi_cache = NoPM } = do
-- New evidence might lead to refined info on ty, in turn leading to discovery
@@ -669,13 +692,6 @@ initPossibleMatches ty_st vi at 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
@@ -720,22 +736,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 at 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
@@ -750,19 +755,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 ~ _|_ at . 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 at .
+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))
@@ -772,10 +779,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
@@ -842,13 +849,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)
]
@@ -861,44 +868,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 at MkNabla{ nabla_tm_st = TmSt env reps } x = do
+ let (y, vi at 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 at 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 at 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))
@@ -910,13 +913,14 @@ addNotConCt delta at 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
@@ -979,100 +983,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 at MkNabla{ nabla_tm_st = TmSt env reps } x = do
+ let (y, vi at 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
+--
+-- Internally uses and updates the ConLikeSets in vi_cache.
--
--- 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 at 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
+-- 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 at VI{ vi_cache = NoPM } = pure vi
+ inst_complete_sets vi at 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 _ _ _ at . 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 at MkDelta{ delta_tm_st = TmSt env reps }
- = runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env)
+ensureAllInhabited :: Nabla -> DsM (Maybe Nabla)
+ensureAllInhabited nabla at 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 at MkDelta{ delta_tm_st = TmSt env _ } x y
+addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
+addVarCt nabla at 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 at .
- | 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.
@@ -1081,12 +1089,12 @@ addVarCt delta at 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 at MkDelta{ delta_tm_st = TmSt env reps } x y
+equate :: Nabla -> Id -> Id -> MaybeT DsM Nabla
+equate nabla at 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...
@@ -1096,16 +1104,16 @@ equate delta at 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
@@ -1113,9 +1121,9 @@ equate delta at 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 at 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 at 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
@@ -1131,10 +1139,19 @@ addConCt delta at 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 =
@@ -1183,9 +1200,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' []
@@ -1281,20 +1298,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
@@ -1309,7 +1326,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
@@ -1337,7 +1354,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
@@ -1516,21 +1533,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
@@ -1543,56 +1560,57 @@ provideEvidence = go
-- some @y@ and @SomePatSyn z@ for some @z at . 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 []
+ Just cls@(_:_) -> instantiate_cons y core_ty xs n newty_nabla cls
+ Just [] | vi_bot vi == IsNotBot -> 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
+ _ -> go xs n newty_nabla
- instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
+ 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
@@ -1601,21 +1619,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)
@@ -1625,14 +1643,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 at MkDelta{ delta_tm_st = ts at TmSt{ ts_reps = reps } } e
- | Just rep <- lookupCoreMap reps e = pure (delta, rep)
+representCoreExpr :: Nabla -> CoreExpr -> DsM (Nabla, Id)
+representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at 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 at . Examples:
@@ -1646,16 +1664,16 @@ representCoreExpr delta at MkDelta{ delta_tm_st = ts at 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 at .
-addCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
-addCoreCt delta x e = do
+addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
+addCoreCt nabla x e = do
dflags <- getDynFlags
let e' = simpleOptExpr dflags 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
@@ -1680,7 +1698,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!
@@ -1698,13 +1716,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 at .
- 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
@@ -1712,10 +1730,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
@@ -1725,20 +1745,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 at . 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 at . 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 at .
- 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 at .
- 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 ()
=====================================
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
| isUnboxedTupleCon 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)
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs
=====================================
@@ -15,6 +15,7 @@ Author: George Karachalias <george.karachalias at 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, 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)
=====================================
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
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -106,7 +106,7 @@ import GHC.Tc.Types.Origin
import GHC.Types.Annotations
import GHC.Core.InstEnv
import GHC.Core.FamInstEnv
-import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Deltas)
+import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Nablas)
import GHC.Data.IOEnv
import GHC.Types.Name.Reader
import GHC.Types.Name
@@ -324,9 +324,9 @@ data DsLclEnv = DsLclEnv {
dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs
-- See Note [Note [Long-distance information] in "GHC.HsToCore.PmCheck"
- -- The set of reaching values Deltas is augmented as we walk inwards,
+ -- The set of reaching values Nablas is augmented as we walk inwards,
-- refined through each pattern match in turn
- dsl_deltas :: Deltas
+ dsl_nablas :: Nablas
}
-- Inside [| |] brackets, the desugarer looks
=====================================
testsuite/tests/pmcheck/should_compile/T10183.hs
=====================================
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, DataKinds, TypeOperators, UnicodeSyntax #-}
+
+module Foo where
+
+import GHC.TypeLits
+
+data List l t where
+ Nil ∷ List 0 t
+ (:-) ∷ t → List l t → List (l+1) t
+
+head' ∷ (1<=l) ⇒ List l t → t
+head' (x :- _) = x
+
+data T a where
+ TT :: T Bool
+ TF :: T Int
+
+f :: T Bool -> Bool
+f TT = True
+
+g :: (a ~ Bool) => T a -> Bool
+g TT = True
=====================================
testsuite/tests/pmcheck/should_compile/T17340.stderr
=====================================
@@ -7,6 +7,10 @@ T17340.hs:19:4: warning: [-Wredundant-bang-patterns]
Pattern match has redundant bang
In an equation for ‘g’: g x = ...
+T17340.hs:23:9: warning: [-Wredundant-bang-patterns]
+ Pattern match has redundant bang
+ In an equation for ‘h’: h x = ...
+
T17340.hs:27:4: warning: [-Wredundant-bang-patterns]
Pattern match has redundant bang
In an equation for ‘k’: k _ = ...
=====================================
testsuite/tests/pmcheck/should_compile/T17378.hs
=====================================
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE EmptyCase #-}
+module Lib where
+
+import Data.Type.Equality
+import Data.Functor.Identity
+import Data.Void
+
+f :: a :~: Int -> a :~: Bool -> ()
+f !_ x = case x of {}
+
+g :: Identity (a :~: Int) -> a :~: Bool -> ()
+g (Identity _) Refl = ()
+
+data SMaybe a = SNothing
+ | SJust !a
+
+-- | Exhaustive. Note how in addition to @{(a,b) | b /~ True}@, the value set
+-- @{(a,b) | y /~ SNothing, b ~ True}@ flows into the next equation, but @y@ is
+-- no longer in scope. Normally, we have no way of matching on that without a
+-- wildcard match, but in this case we refute @y ~ SJust z@ by unleashing type
+-- evidence saying that @z@ must be 'Void' by matching on 'Void'.
+h :: forall a. a :~: Void -> Bool -> ()
+h _ True | let y = undefined :: SMaybe a, SNothing <- y = ()
+h Refl False = ()
=====================================
testsuite/tests/pmcheck/should_compile/T17725.hs
=====================================
@@ -0,0 +1,10 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+module Lib where
+
+newtype IInt = IInt Int
+
+f :: IInt -> Bool -> ()
+f !(IInt _) True = ()
+f (IInt 42) True = ()
+f _ _ = ()
=====================================
testsuite/tests/pmcheck/should_compile/T17725.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T17725.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘f’: f (IInt 42) True = ...
=====================================
testsuite/tests/pmcheck/should_compile/T17729.hs
=====================================
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
+
+incomplete :: Maybe a -> Bool
+incomplete ma = case (ma, ()) of
+ (Nothing, _) -> False
+
+{-# COMPLETE Pat #-}
+pattern Pat :: a -> b -> (a, b)
+pattern Pat a b = (a, b)
+
+main :: IO ()
+main = print $ incomplete (Just ())
=====================================
testsuite/tests/pmcheck/should_compile/T17729.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T17729.hs:5:17: warning: [-Wincomplete-patterns (in -Wextra)]
+ Pattern match(es) are non-exhaustive
+ In a case alternative: Patterns not matched: ((Just _), ())
=====================================
testsuite/tests/pmcheck/should_compile/T18273.hs
=====================================
@@ -0,0 +1,41 @@
+{-# OPTIONS_GHC -fforce-recomp -Wincomplete-patterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Bug where
+
+import Data.Kind
+import Data.Void
+
+type SFalse = SBool 'False
+type STrue = SBool 'True
+
+data SBool :: Bool -> Type where
+ SFalse :: SFalse
+ STrue :: STrue
+
+type family F (b :: Bool) :: Type where
+ F 'False = Void
+ F 'True = ()
+
+data T (b :: Bool)
+ = MkT1
+ | MkT2 !(F b)
+
+ex :: SBool b -> T b -> ()
+ex sb t =
+ case t of
+ MkT1 -> ()
+ MkT2 f ->
+ case sb of
+ STrue -> f
+
+ex2 :: SBool b -> T b -> ()
+ex2 sb t =
+ case t of
+ MkT2 f ->
+ case sb of
+ STrue -> f
+ MkT1 -> ()
=====================================
testsuite/tests/pmcheck/should_compile/T18341.hs
=====================================
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+
+module Lib where
+
+import GHC.Exts
+
+data T = MkT !Int {-# UNPACK #-} !Int Int#
+
+f :: T -> ()
+f (MkT _ _ _) | False = () -- inaccessible
+f (MkT !_ _ _) | False = () -- redundant, not only inaccessible!
+f _ = ()
+
+g :: T -> ()
+g (MkT _ _ _) | False = () -- inaccessible
+g (MkT _ !_ _) | False = () -- redundant, not only inaccessible!
+g _ = ()
+
+h :: T -> ()
+h (MkT _ _ _) | False = () -- inaccessible
+h (MkT _ _ !_) | False = () -- redundant, not only inaccessible!
+h _ = ()
=====================================
testsuite/tests/pmcheck/should_compile/T18341.stderr
=====================================
@@ -0,0 +1,24 @@
+
+T18341.hs:12:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘f’: f (MkT _ _ _) | False = ...
+
+T18341.hs:13:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘f’: f (MkT !_ _ _) | False = ...
+
+T18341.hs:17:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘g’: g (MkT _ _ _) | False = ...
+
+T18341.hs:18:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘g’: g (MkT _ !_ _) | False = ...
+
+T18341.hs:22:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘h’: h (MkT _ _ _) | False = ...
+
+T18341.hs:23:18: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘h’: h (MkT _ _ !_) | False = ...
=====================================
testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs
=====================================
@@ -3,8 +3,10 @@
-- As a result, these functions elicit the symptoms describe in the warnings
-- message, e.g.
-- - False positives on exhaustivity
--- - Turns redundant into inaccessible clauses
-- - Fails to report redundant matches
+--
+-- We used to turn redundant into inaccessible clauses, but SG was unable to
+-- produce a testcase. See the comment below.
module TooManyDeltas where
data T = A | B
@@ -13,12 +15,19 @@ data T = A | B
f :: T -> T -> ()
f A A = ()
+-- SG: As of July 2020, g doesn't reproduce anymore.
+-- Because we treat constructor matches lazily and push data con match
+-- strictness into a preceding bang guard, The single place that calls the
+-- throttling function will not regress in laziness. Note that by throttling we
+-- can only "forget" the x /~ K constraint from unc_this, not the preceding
+-- x /~ ⊥ constraint.
+
-- | Reports that the third clause is inaccessible, when really it is
-- redundant.
g :: T -> T -> ()
g _ A = ()
g A A = () -- inaccessible, correctly flagged
-g A A = () -- redundant, not inaccessible!
+g A A = () -- redundant, used to be inaccessible (see above).
g _ _ = () -- (this one is not about exhaustivity)
-- | Fails to report that the second clause is redundant.
=====================================
testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
=====================================
@@ -1,12 +1,12 @@
-TooManyDeltas.hs:14:1: warning:
+TooManyDeltas.hs:16:1: warning:
Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
• Redundant clauses might not be reported at all
• Redundant clauses might be reported as inaccessible
• Patterns reported as unmatched might actually be matched
Increase the limit or resolve the warnings to suppress this message.
-TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
+TooManyDeltas.hs:16:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’:
Patterns not matched:
@@ -15,17 +15,17 @@ TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
B A
B B
-TooManyDeltas.hs:19:1: warning:
+TooManyDeltas.hs:28:1: warning:
Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
• Redundant clauses might not be reported at all
• Redundant clauses might be reported as inaccessible
• Patterns reported as unmatched might actually be matched
Increase the limit or resolve the warnings to suppress this message.
-TooManyDeltas.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+TooManyDeltas.hs:29:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘g’: g A A = ...
-TooManyDeltas.hs:21:1: warning: [-Woverlapping-patterns (in -Wdefault)]
- Pattern match has inaccessible right hand side
+TooManyDeltas.hs:30:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
In an equation for ‘g’: g A A = ...
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -36,6 +36,8 @@ test('T9951b', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T9951', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T10183', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T11303', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
test('T11276', collect_compiler_stats('bytes allocated',10), compile,
@@ -108,12 +110,18 @@ test('T17357', expect_broken(17357), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17376', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17378', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17465', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17646', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17703', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17725', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17729', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17783', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17977', collect_compiler_stats('bytes allocated',10), compile,
@@ -122,6 +130,10 @@ test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18049', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18273', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18341', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18478', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18533', normal, compile,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42f9bf20d2d7c9d190023ad053eec82b9d1aad27
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42f9bf20d2d7c9d190023ad053eec82b9d1aad27
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200831/ae830198/attachment-0001.html>
More information about the ghc-commits
mailing list