diff options
| author | Sebastian Graf <sebastian.graf@kit.edu> | 2020-09-11 17:08:12 +0200 |
|---|---|---|
| committer | Sebastian Graf <sebastian.graf@kit.edu> | 2020-09-21 12:30:08 +0200 |
| commit | 3a08f97bd270bf67ef92a334bd65794ccfbf06ad (patch) | |
| tree | 7dfb952e03bdce668d96d300cb22307da0c121d0 | |
| parent | c79f14770af18962ee3d2f636db51c62dfc5c2d6 (diff) | |
| download | haskell-3a08f97bd270bf67ef92a334bd65794ccfbf06ad.tar.gz | |
PmCheck: Rewrite inhabitation testwip/T18249
We used to produce inhabitants of a pattern-match refinement type Nabla
in the checker in at least two different and mostly redundant ways:
1. There was `provideEvidence` (now called
`generateInhabitingPatterns`) which is used by
`GHC.HsToCore.PmCheck` to produce non-exhaustive patterns, which
produces inhabitants of a Nabla as a sub-refinement type where all
match variables are instantiated.
2. There also was `ensure{,All}Inhabited` (now called
`inhabitationTest`) which worked slightly different, but was
whenever new type constraints or negative term constraints were
added. See below why `provideEvidence` and `ensureAllInhabited`
can't be the same function, the main reason being performance.
3. And last but not least there was the `nonVoid` test, which tested
that a given type was inhabited. We did use this for strict fields
and -XEmptyCase in the past.
The overlap of (3) with (2) was always a major pet peeve of mine. The
latter was quite efficient and proven to work for recursive data types,
etc, but could not handle negative constraints well (e.g. we often want
to know if a *refined* type is empty, such as `{ x:[a] | x /= [] }`).
Lower Your Guards suggested that we could get by with just one, by
replacing both functions with `inhabitationTest` in this patch.
That was only possible by implementing the structure of φ constraints
as in the paper, namely the semantics of φ constructor constraints.
This has a number of benefits:
a. Proper handling of unlifted types and strict fields, fixing #18249,
without any code duplication between
`GHC.HsToCore.PmCheck.Oracle.instCon` (was `mkOneConFull`) and
`GHC.HsToCore.PmCheck.checkGrd`.
b. `instCon` can perform the `nonVoid` test (3) simply by emitting
unliftedness constraints for strict fields.
c. `nonVoid` (3) is thus simply expressed by a call to
`inhabitationTest`.
d. Similarly, `ensureAllInhabited` (2), which we called after adding
type info, now can similarly be expressed as the fuel-based
`inhabitationTest`.
See the new `Note [Why inhabitationTest doesn't call generateInhabitingPatterns]`
why we still have tests (1) and (2).
Fixes #18249 and brings nice metric decreases for `T17836` (-76%) and
`T17836b` (-46%), as well as `T18478` (-8%) at the cost of a few very
minor regressions (< +2%), potentially due to the fact that
`generateInhabitingPatterns` does more work to suggest the minimal
COMPLETE set.
Metric Decrease:
T17836
T17836b
| -rw-r--r-- | compiler/GHC/Hs/Expr.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck.hs | 86 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Oracle.hs | 2174 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Ppr.hs | 6 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Types.hs | 96 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/PmCheck/Types.hs-boot | 9 | ||||
| -rw-r--r-- | compiler/GHC/HsToCore/Types.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Expr.hs | 2 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T18249.hs | 36 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T18249.stderr | 20 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/all.T | 2 |
11 files changed, 1210 insertions, 1225 deletions
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs index 466260c782..251fae2c48 100644 --- a/compiler/GHC/Hs/Expr.hs +++ b/compiler/GHC/Hs/Expr.hs @@ -1347,8 +1347,10 @@ hsExprNeedsParens p = go ExpansionExpr (HsExpanded a _) -> hsExprNeedsParens p a | GhcRn <- ghcPass @p = case x of HsExpanded a _ -> hsExprNeedsParens p a +#if __GLASGOW_HASKELL__ <= 900 | otherwise = True +#endif -- | @'parenthesizeHsExpr' p e@ checks if @'hsExprNeedsParens' p e@ is true, diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs index 831509d351..bad245cc6e 100644 --- a/compiler/GHC/HsToCore/PmCheck.hs +++ b/compiler/GHC/HsToCore/PmCheck.hs @@ -781,28 +781,6 @@ 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]@. -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 _ = () - -The second clause desugars to @MkT n <- x, !n@. When coverage checked, the -'PmCon' @MkT n <- x@ refines the set of values that reach the bang pattern with -the constraints @x ~ MkT n, n ≁ ⊥@ (this list is computed by 'pmConCts'). -Checking the 'PmBang' @!n@ will then try to add the constraint @n ~ ⊥@ to this -set to get the diverging set, which is found to be empty. Hence the whole -clause is detected as redundant, as expected. - Note [Order of guards matters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Similar to Note [Field match order for RecCon], the order in which the guards @@ -872,17 +850,17 @@ instance Outputable a => Outputable (CheckResult a) where field name value = text name <+> equals <+> ppr value -- | Lift 'addPmCts' over 'Nablas'. -addPmCtsNablas :: Nablas -> PmCts -> DsM Nablas -addPmCtsNablas nablas cts = liftNablasM (\d -> addPmCts d cts) nablas +addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas +addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas -- | 'addPmCtsNablas' for a single 'PmCt'. -addPmCtNablas :: Nablas -> PmCt -> DsM Nablas -addPmCtNablas nablas ct = addPmCtsNablas nablas (unitBag ct) +addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas +addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct) -- | 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@. +-- terms of @notNull <$> generateInhabitingPatterns 1 ds@. isInhabited :: Nablas -> DsM Bool isInhabited (MkNablas ds) = pure (not (null ds)) @@ -938,26 +916,6 @@ throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds) | length new_ds > max limit (length old_ds) = (Approximate, old) | otherwise = (Precise, new) --- | The 'PmCts' arising from a successful 'PmCon' match @T gammas as ys <- x@. --- These include --- --- * @gammas@: Constraints arising from the bound evidence vars --- * @y ≁ ⊥@ constraints for each unlifted field (including strict fields) --- @y@ in @ys@ --- * The constructor constraint itself: @x ~ T as ys@. --- --- See Note [Strict fields and fields of unlifted type]. -pmConCts :: Id -> PmAltCon -> [TyVar] -> [EvVar] -> [Id] -> PmCts -pmConCts x con tvs dicts args = gammas `unionBags` unlifted `snocBag` con_ct - where - gammas = listToBag $ map (PmTyCt . evVarPred) dicts - con_ct = PmConCt x con tvs args - unlifted = listToBag [ PmNotBotCt arg - | (arg, bang) <- - zipEqual "pmConCts" args (pmAltConImplBangs con) - , isBanged bang || isUnliftedType (idType arg) - ] - checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) -- The implementation is pretty similar to -- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@ @@ -969,32 +927,37 @@ checkGrd :: PmGrd -> CheckAction RedSets checkGrd grd = CA $ \inc -> case grd of -- let x = e: Refine with x ~ e PmLet x e -> do - matched <- addPmCtNablas inc (PmCoreCt x e) - -- tracePm "check:Let" (ppr x <+> char '=' <+> ppr e) + matched <- addPhiCtNablas inc (PhiCoreCt 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 <- addPmCtNablas inc (PmBotCt x) - matched <- addPmCtNablas inc (PmNotBotCt x) + div <- addPhiCtNablas inc (PhiBotCt x) + matched <- addPhiCtNablas inc (PhiNotBotCt 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) + 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: Fall through on x ≁ K and refine with x ~ K ys and type info PmCon x con tvs dicts args -> do !div <- if isPmAltConMatchStrict con - then addPmCtNablas inc (PmBotCt x) + then addPhiCtNablas inc (PhiBotCt x) else pure mempty - 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) + !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args) + !uncov <- addPhiCtNablas inc (PhiNotConCt x con) + tracePm "check:Con" $ vcat + [ ppr grd + , ppr inc + , hang (text "div") 2 (ppr div) + , hang (text "matched") 2 (ppr matched) + , hang (text "uncov") 2 (ppr uncov) + ] pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div } , cr_uncov = uncov , cr_approx = Precise } @@ -1028,7 +991,7 @@ checkGRHS (PmGRHS { pg_grds = grds, pg_rhs = rhs_info }) = checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do - unc <- addPmCtNablas inc (PmNotBotCt var) + unc <- addPhiCtNablas inc (PhiNotBotCt var) pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty } checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post) @@ -1275,7 +1238,7 @@ getNFirstUncovered vars n (MkNablas nablas) = go n (bagToList nablas) go 0 _ = pure [] go _ [] = pure [] go n (nabla:nablas) = do - front <- provideEvidence vars n nabla + front <- generateInhabitingPatterns vars n nabla back <- go (n - length front) nablas pure (front ++ back) @@ -1415,7 +1378,8 @@ addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a addTyCs origin ev_vars m = do dflags <- getDynFlags applyWhen (needToRunPmCheck dflags origin) - (locallyExtendPmNablas (\nablas -> addPmCtsNablas nablas (PmTyCt . evVarPred <$> ev_vars))) + (locallyExtendPmNablas $ \nablas -> + addPhiCtsNablas nablas (PhiTyCt . evVarPred <$> ev_vars)) m -- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment @@ -1427,7 +1391,7 @@ addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a addCoreScrutTmCs Nothing _ k = k addCoreScrutTmCs (Just scr) [x] k = flip locallyExtendPmNablas k $ \nablas -> - addPmCtsNablas nablas (unitBag (PmCoreCt x scr)) + addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr)) addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id" -- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first. diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs index 492e993f19..fd76bcf70d 100644 --- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs +++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs @@ -4,26 +4,25 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be> Ryan Scott <ryan.gl.scott@gmail.com> -} -{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf, ScopedTypeVariables #-} +{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, + MultiWayIf, ScopedTypeVariables, MagicHash #-} -- | 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 +-- 'addPhiCts' for adding facts to the oracle, and 'generateInhabitingPatterns' to turn a -- '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'. +-- E.g., it represents refinement types directly as a normalised refinement type 'Nabla'. module GHC.HsToCore.PmCheck.Oracle ( DsM, tracePm, mkPmId, Nabla, initNablas, lookupRefuts, lookupSolution, - PmCt(PmTyCt), PmCts, pattern PmVarCt, pattern PmCoreCt, - pattern PmConCt, pattern PmNotConCt, pattern PmBotCt, - pattern PmNotBotCt, + PhiCt(..), PhiCts, - addPmCts, -- Add a constraint to the oracle. - provideEvidence + addPhiCts, -- Add a constraint to the oracle. + generateInhabitingPatterns ) where #include "HsVersions.h" @@ -39,14 +38,15 @@ import GHC.Utils.Error import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Data.Bag +import GHC.Types.Unique import GHC.Types.Unique.Set import GHC.Types.Unique.DSet -import GHC.Types.Unique -import GHC.Types.Id -import GHC.Types.Var.Env import GHC.Types.Unique.DFM -import GHC.Types.Var (EvVar) +import GHC.Types.Id import GHC.Types.Name +import GHC.Types.Var (EvVar) +import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Core import GHC.Core.FVs (exprFreeVars) import GHC.Core.Map @@ -74,17 +74,18 @@ import GHC.Tc.Instance.Family import GHC.Core.FamInstEnv import Control.Applicative ((<|>)) -import Control.Monad (guard, mzero, when) +import Control.Monad (foldM, forM, guard, mzero, when) import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.State.Strict -import Data.Bifunctor (second) import Data.Either (partitionEithers) import Data.Foldable (foldlM, minimumBy, toList) -import Data.List (find) +import Data.List (sortBy, find) +import qualified Data.List.NonEmpty as NE import Data.Ord (comparing) -import qualified Data.Semigroup as Semigroup import Data.Tuple (swap) +import GHC.Driver.Ppr (pprTrace) + -- Debugging Infrastructure tracePm :: String -> SDoc -> DsM () @@ -95,6 +96,17 @@ tracePm herald doc = do Opt_D_dump_ec_trace "" FormatText (text herald $$ (nest 2 doc)) {-# INLINE tracePm #-} -- see Note [INLINE conditional tracing utilities] +debugOn :: () -> Bool +debugOn _ = False +-- debugOn _ = True + +trc :: String -> SDoc -> a -> a +trc | debugOn () = pprTrace + | otherwise = \_ _ a -> a + +_trcM :: Monad m => String -> SDoc -> m () +_trcM header doc = trc header doc (return ()) + -- | Generate a fresh `Id` of a given type mkPmId :: Type -> DsM Id mkPmId ty = getUniqueM >>= \unique -> @@ -103,14 +115,10 @@ mkPmId ty = getUniqueM >>= \unique -> in return (mkLocalIdOrCoVar name Many ty) ----------------------------------------------- --- * Caching possible matches of a COMPLETE set +-- * Caching residual COMPLETE set -- See Note [Implementation of COMPLETE pragmas] --- | Traverse the COMPLETE sets of 'ResidualCompleteMatches'. -trvRcm :: Applicative f => (ConLikeSet -> f ConLikeSet) -> ResidualCompleteMatches -> f ResidualCompleteMatches -trvRcm f (RCM vanilla pragmas) = RCM <$> traverse f vanilla - <*> traverse (traverse f) pragmas -- | Update the COMPLETE sets of 'ResidualCompleteMatches'. updRcm :: (ConLikeSet -> ConLikeSet) -> ResidualCompleteMatches -> ResidualCompleteMatches updRcm f (RCM vanilla pragmas) = RCM (f <$> vanilla) (fmap f <$> pragmas) @@ -191,7 +199,7 @@ The pattern-match checker will then initialise each variable's 'VarInfo' with well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a COMPLETE set that is ill-typed for that match variable could never be written by the user! And we make sure not to report any ill-typed COMPLETE sets when -formatting 'Nabla's for warnings in 'provideEvidence'. +formatting 'Nabla's for warnings in 'generateInhabitingPatterns'. A 'ResidualCompleteMatches' is a list of all COMPLETE sets, minus the ConLikes we know a particular variable can't be (through negative constructor constraints @@ -214,124 +222,6 @@ that the match in the guards of @f@ is exhaustive, where the COMPLETE set applies due to refined type information. -} ---------------------------------------------------- --- * Instantiating constructors, types and evidence - --- | Instantiate a 'ConLike' given its universal type arguments. Instantiates --- existential and term binders with fresh variables of appropriate type. --- Returns instantiated type and term variables from the match, type evidence --- and the types of strict constructor fields. -mkOneConFull :: [Type] -> ConLike -> DsM ([TyVar], [Id], Bag TyCt, [Type]) --- * 'con' K is a ConLike --- - In the case of DataCons and most PatSynCons, these --- are associated with a particular TyCon T --- - But there are PatSynCons for this is not the case! See #11336, #17112 --- --- * 'arg_tys' tys are the types K's universally quantified type --- variables should be instantiated to. --- - For DataCons and most PatSyns these are the arguments of their TyCon --- - For cases like the PatSyns in #11336, #17112, we can't easily guess --- these, so don't call this function. --- --- After instantiating the universal tyvars of K to tys we get --- K @tys :: forall bs. Q => s1 .. sn -> T tys --- Note that if K is a PatSynCon, depending on arg_tys, T might not necessarily --- be a concrete TyCon. --- --- Suppose y1 is a strict field. Then we get --- Results: bs --- [y1,..,yn] --- Q --- [s1] -mkOneConFull arg_tys con = do - let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta, field_tys, _con_res_ty) - = conLikeFullSig con - -- pprTrace "mkOneConFull" (ppr con $$ ppr arg_tys $$ ppr univ_tvs $$ ppr _con_res_ty) (return ()) - -- Substitute universals for type arguments - let subst_univ = zipTvSubst univ_tvs arg_tys - -- Instantiate fresh existentials as arguments to the constructor. This is - -- important for instantiating the Thetas and field types. - (subst, _) <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM - let field_tys' = substTys subst $ map scaledThing field_tys - -- Instantiate fresh term variables (VAs) as arguments to the constructor - vars <- mapM mkPmId field_tys' - -- All constraints bound by the constructor (alpha-renamed), these are added - -- 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 = map isBanged $ conLikeImplBangs con - strict_arg_tys = filterByList arg_is_strict field_tys' - return (ex_tvs, vars, listToBag ty_cs, strict_arg_tys) - -------------------------- --- * Pattern match oracle - - -------------------------------------- --- * Composable satisfiability checks - --- | 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: --- 1. 'tmIsSatisfiable', adding term oracle facts --- 2. 'tyIsSatisfiable', adding type oracle facts --- 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 (Nabla -> DsM (Maybe Nabla)) - --- | Check the given 'Nabla' for satisfiability by the given --- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Nabla' if --- successful, and 'Nothing' otherwise. -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 nabla = a nabla >>= \case - Nothing -> pure Nothing - Just nabla' -> b nabla' - -instance Monoid SatisfiabilityCheck where - -- We only need this because of mconcat (which we use in place of sconcat, - -- which requires NonEmpty lists as argument, making all call sites ugly) - mempty = SC (pure . Just) - -------------------------------- --- * Oracle transition function - --- | Given a conlike's term constraints, type constraints, and strict argument --- types, check if they are satisfiable. --- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet --- Their Match paper.) --- --- Taking strict argument types into account is something which was not --- discussed in GADTs Meet Their Match. For an explanation of what role they --- serve, see @Note [Strict argument type constraints]@. -pmIsSatisfiable - :: 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 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 = - -- The order is important here! Check the new type constraints before we check - -- whether strict argument types are inhabited given those constraints. - runSatisfiabilityCheck amb_cs $ mconcat - [ tyIsSatisfiable True new_ty_cs - , tmIsSatisfiable new_tm_cs - , tysAreNonVoid initRecTc strict_arg_tys - ] - ----------------------- -- * Type normalisation @@ -359,15 +249,9 @@ data TopNormaliseTypeResult -- in the chain of reduction steps between the Source type and the Core type. -- We also keep the type of the DataCon application and its field, so that we -- don't have to reconstruct it in 'inhabitationCandidates' and - -- 'provideEvidence'. + -- 'generateInhabitingPatterns'. -- For an example, see Note [Type normalisation]. --- | Just give me the potentially normalised source type, unchanged or not! -normalisedSourceType :: TopNormaliseTypeResult -> Type -normalisedSourceType (NoChange ty) = ty -normalisedSourceType (NormalisedByConstraints ty) = ty -normalisedSourceType (HadRedexes ty _ _) = ty - -- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the -- other cases. tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type) @@ -400,8 +284,9 @@ pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult -- NB: Normalisation can potentially change kinds, if the head of the type -- is a type family with a variable result kind. I (Richard E) can't think -- of a way to cause trouble here, though. -pmTopNormaliseType (TySt inert) typ +pmTopNormaliseType (TySt _ inert) typ = do env <- dsGetFamInstEnvs + tracePm "normalise" (ppr typ) -- Before proceeding, we chuck typ into the constraint solver, in case -- solving for given equalities may reduce typ some. See -- "Wrinkle: local equalities" in Note [Type normalisation]. @@ -493,6 +378,30 @@ pmIsClosedType ty is_algebraic_like :: TyCon -> Bool is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon +-- | Normalise the given source type to WHNF. If it isn't already in WHNF +-- ('isSourceTypeInWHNF') , it will normalise the type and then try to step +-- through type family applications, but not data family applications or +-- newtypes. +-- +-- This is a pretty common case of calling 'pmTopNormaliseType' and it should be +-- efficient. +normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type +normaliseSourceTypeWHNF _ ty | isSourceTypeInWHNF ty = pure ty +normaliseSourceTypeWHNF ty_st ty = do + pmTopNormaliseType ty_st ty >>= \case + NoChange ty -> pure ty + NormalisedByConstraints ty -> pure ty + HadRedexes ty _ _ -> pure ty + +-- | Is the source type in WHNF wrt. 'pmTopNormaliseType'? +-- +-- Returns False if the given type is not a TyCon application, or if the TyCon +-- app head is a type family TyCon. (But not for data family TyCons!) +isSourceTypeInWHNF :: Type -> Bool +isSourceTypeInWHNF ty + | Just (tc, _) <- splitTyConApp_maybe ty = not (isTypeFamilyTyCon tc) + | otherwise = False + {- Note [Type normalisation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data @@ -568,160 +477,6 @@ pmTopNormaliseType, using the constraint solver to solve for any local equalities (such as i ~ Int) that may be in scope. -} ----------------- --- * Type oracle - --- | Allocates a fresh 'EvVar' name for 'PredTy's. -nameTyCt :: PredType -> DsM EvVar -nameTyCt pred_ty = do - unique <- getUniqueM - let occname = mkVarOccFS (fsLit ("pm_"++show unique)) - idname = mkInternalName unique occname noSrcSpan - return (mkLocalIdOrCoVar idname Many pred_ty) - --- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we --- find a contradiction (e.g. @Int ~ Bool@). -tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState) -tyOracle (TySt inert) cts - = do { evs <- traverse nameTyCt cts - ; tracePm "tyOracle" (ppr cts) - ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability inert evs - ; case res of - Just mb_new_inert -> return (TySt <$> mb_new_inert) - Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) } - --- | A 'SatisfiabilityCheck' based on new type-level constraints. --- 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 'ResidualCompleteMatches' 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 $ \nabla -> - if isEmptyBag new_ty_cs - then pure (Just nabla) - else tyOracle (nabla_ty_st nabla) new_ty_cs >>= \case - Nothing -> pure Nothing - Just ty_st' -> do - let nabla' = nabla{ nabla_ty_st = ty_st' } - if recheck_complete_sets - then ensureAllInhabited nabla' - else pure (Just nabla') - - -{- ********************************************************************* -* * - DIdEnv with sharing -* * -********************************************************************* -} - - -{- ********************************************************************* -* * - TmState - What we know about terms -* * -********************************************************************* -} - -{- Note [The Pos/Neg invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos', -any entry in 'vi_neg' must be incomparable to C (return Nothing) according to -'eqPmAltCons'. Those entries that are comparable either lead to a refutation -or are redundant. Examples: -* @x ~ Just y@, @x ≁ [Just]@. 'eqPmAltCon' returns @Equal@, so refute. -* @x ~ Nothing@, @x ≁ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative - info is redundant and should be discarded. -* @x ~ I# y@, @x ≁ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal. - We keep this info in order to be able to refute a redundant match on i.e. 4 - later on. - -This carries over to pattern synonyms and overloaded literals. Say, we have - pattern Just42 = Just 42 - case Just42 of x - Nothing -> () - Just _ -> () -Even though we had a solution for the value abstraction called x here in form -of a PatSynCon (Just42,[]), this solution is incomparable to both Nothing and -Just. Hence we retain the info in vi_neg, which eventually allows us to detect -the complete pattern match. - -The Pos/Neg invariant extends to vi_rcm, which stores essentially positive -information. We make sure that vi_neg and vi_rcm never overlap. This isn't -strictly necessary since vi_rcm is just a cache, so doesn't need to be -accurate: Every suggestion of a possible ConLike from vi_rcm might be -refutable by the type oracle anyway. But it helps to maintain sanity while -debugging traces. - -Note [Why record both positive and negative info?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -You might think that knowing positive info (like x ~ Just y) would render -negative info irrelevant, but not so because of pattern synonyms. E.g we might -know that x cannot match (Foo 4), where pattern Foo p = Just p - -Also overloaded literals themselves behave like pattern synonyms. E.g if -postively we know that (x ~ I# y), we might also negatively want to record that -x does not match 45 f 45 = e2 f (I# 22#) = e3 f 45 = e4 -- -Overlapped - -Note [TmState invariants] -~~~~~~~~~~~~~~~~~~~~~~~~~ -The term oracle state is never obviously (i.e., without consulting the type -oracle) contradictory. This implies a few invariants: -* Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute. - This is implied by the Note [Pos/Neg invariant]. -* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_rcm to - detect this, but we could just compare whole COMPLETE sets to vi_neg every - time, if it weren't for performance. - -Maintaining these invariants in 'addVarCt' (the core of the term oracle) and -'addNotConCt' is subtle. -* Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate'). - - (COMPLETE) If we had @x ≁ True@ and @y ≁ False@, then we get - @x ≁ [True,False]@. This is vacuous by matter of comparing to the built-in - COMPLETE set, so should refute. - - (Pos/Neg) If we had @x ≁ True@ and @y ~ True@, we have to refute. -* Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt') - - (Neg) If we had @x ≁ K@, refute. - - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to - 'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute. - - (Refine) If we had @x ≁ K zs@, unify each y with each z in turn. -* Adding negative information. Example: Add the fact @x ≁ Nothing@ (see 'addNotConCt') - - (Refut) If we have @x ~ K ys@, refute. - - (COMPLETE) If K=Nothing and we had @x ≁ Just@, then we get - @x ≁ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in - COMPLETE set, so should refute. - -Note that merging VarInfo in equate can be done by calling out to 'addConCt' and -'addNotConCt' for each of the facts individually. - -Note [Representation of Strings in TmState] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Instead of treating regular String literals as a PmLits, we treat it as a list -of characters in the oracle for better overlap reasoning. The following example -shows why: - - f :: String -> () - f ('f':_) = () - f "foo" = () - f _ = () - -The second case is redundant, and we like to warn about it. Therefore either -the oracle will have to do some smart conversion between the list and literal -representation or treat is as the list it really is at runtime. - -The "smart conversion" has the advantage of leveraging the more compact literal -representation wherever possible, but is really nasty to get right with negative -equalities: Just think of how to encode @x /= "foo"@. -The "list" option is far simpler, but incurs some overhead in representation and -warning messages (which can be alleviated by someone with enough dedication). --} - --- | A 'SatisfiabilityCheck' based on new term-level constraints. --- Returns a new 'Nabla' if the new constraints are compatible with existing --- ones. -tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck -tmIsSatisfiable new_tm_cs = SC $ \nabla -> runMaybeT $ foldlM addTmCt nabla new_tm_cs - ----------------------- -- * Looking up VarInfo @@ -729,16 +484,19 @@ emptyRCM :: ResidualCompleteMatches emptyRCM = RCM Nothing Nothing emptyVarInfo :: Id -> VarInfo --- 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 emptyRCM +emptyVarInfo x + = VI + { vi_id = x + , vi_pos = [] + , vi_neg = emptyPmAltConSet + -- Case (3) in Note [Strict fields and fields of unlifted type] + , vi_bot = if isUnliftedType (idType x) then IsNotBot else MaybeBot + , vi_rcm = emptyRCM + } lookupVarInfo :: TmState -> Id -> VarInfo -- (lookupVarInfo tms x) tells what we know about 'x' -lookupVarInfo (TmSt env _) x = fromMaybe (emptyVarInfo x) (lookupSDIE env 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 @@ -756,10 +514,17 @@ lookupVarInfoNT ts x = case lookupVarInfo ts x of res -> (x, res) where as_newtype = listToMaybe . mapMaybe go - go (PmAltConLike (RealDataCon dc), _, [y]) + go PACA{paca_con = PmAltConLike (RealDataCon dc), paca_ids = [y]} | isNewDataCon dc = Just y go _ = Nothing +trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla) +trvVarInfo f nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts = env} } x + = set_vi <$> f (lookupVarInfo ts x) + where + set_vi (a, vi') = + (a, nabla{ nabla_tm_st = ts{ ts_facts = setEntrySDIE env (vi_id vi') vi' } }) + ------------------------------------------------ -- * Exported utility functions querying 'Nabla' @@ -794,156 +559,218 @@ where you can find the solution in a perhaps more digestible format. lookupRefuts :: Uniquable k => Nabla -> k -> [PmAltCon] -- Unfortunately we need the extra bit of polymorphism and the unfortunate -- duplication of lookupVarInfo here. -lookupRefuts MkNabla{ nabla_tm_st = ts@(TmSt (SDIE env) _) } k = +lookupRefuts MkNabla{ nabla_tm_st = ts@(TmSt{ts_facts = (SDIE env)}) } k = case lookupUDFM_Directly env (getUnique k) of Nothing -> [] Just (Indirect y) -> pmAltConSetElems (vi_neg (lookupVarInfo ts y)) Just (Entry vi) -> pmAltConSetElems (vi_neg vi) -isDataConSolution :: (PmAltCon, [TyVar], [Id]) -> Bool -isDataConSolution (PmAltConLike (RealDataCon _), _, _) = True -isDataConSolution _ = False +isDataConSolution :: PmAltConApp -> Bool +isDataConSolution PACA{paca_con = PmAltConLike (RealDataCon _)} = True +isDataConSolution _ = False -- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from -- possibly many, preferring 'RealDataCon' solutions whenever possible. -lookupSolution :: Nabla -> Id -> Maybe (PmAltCon, [TyVar], [Id]) +lookupSolution :: Nabla -> Id -> Maybe PmAltConApp lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of [] -> Nothing pos | Just sol <- find isDataConSolution pos -> Just sol | otherwise -> Just (head pos) -------------------------------- --- * Adding facts to the oracle - --- | A term constraint. -data TmCt - = TmVarCt !Id !Id - -- ^ @TmVarCt x y@ encodes "x ~ y", equating @x@ and @y@. - | TmCoreCt !Id !CoreExpr - -- ^ @TmCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@. - | TmConCt !Id !PmAltCon ![TyVar] ![Id] - -- ^ @TmConCt x K tvs ys@ encodes "x ~ K @tvs ys", equating @x@ with the 'PmAltCon' - -- application @K @tvs ys@. - | TmNotConCt !Id !PmAltCon - -- ^ @TmNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed +------------------------- +-- * Adding φ constraints +-- +-- Figure 7 in the LYG paper. + +-- | A high-level pattern-match constraint. Corresponds to φ from Figure 3 of +-- the LYG paper. +data PhiCt + = PhiTyCt !PredType + -- ^ A type constraint "T ~ U". + | PhiCoreCt !Id !CoreExpr + -- ^ @PhiCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@. + | PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id] + -- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@ + -- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@, + -- @dicts@ and possibly unlifted fields @ys@ in the process. + -- See Note [Strict fields and fields of unlifted type]. + | PhiNotConCt !Id !PmAltCon + -- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed -- by @K@. - | TmBotCt !Id - -- ^ @TmBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥. + | PhiBotCt !Id + -- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥. -- by @K@. - | TmNotBotCt !Id - -- ^ @TmNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥. - -instance Outputable TmCt where - ppr (TmVarCt x y) = ppr x <+> char '~' <+> ppr y - ppr (TmCoreCt x e) = ppr x <+> char '~' <+> ppr e - ppr (TmConCt x con tvs args) = ppr x <+> char '~' <+> hsep (ppr con : pp_tvs ++ pp_args) + | PhiNotBotCt !Id + -- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥. + +instance Outputable PhiCt where + ppr (PhiTyCt ty_ct) = ppr ty_ct + ppr (PhiCoreCt x e) = ppr x <+> char '~' <+> ppr e + ppr (PhiConCt x con tvs dicts args) = + hsep (ppr con : pp_tvs ++ pp_dicts ++ pp_args) <+> text "<-" <+> ppr x where - pp_tvs = map ((<> char '@') . ppr) tvs - pp_args = map ppr args - ppr (TmNotConCt x con) = ppr x <+> text "≁" <+> ppr con - ppr (TmBotCt x) = ppr x <+> text "~ ⊥" - ppr (TmNotBotCt x) = ppr x <+> text "≁ ⊥" - -type TyCt = PredType - --- | An oracle constraint. -data PmCt - = PmTyCt !TyCt - -- ^ @PmTy pred_ty@ carries 'PredType's, for example equality constraints. - | PmTmCt !TmCt - -- ^ A term constraint. - -type PmCts = Bag PmCt - -pattern PmVarCt :: Id -> Id -> PmCt -pattern PmVarCt x y = PmTmCt (TmVarCt x y) -pattern PmCoreCt :: Id -> CoreExpr -> PmCt -pattern PmCoreCt x e = PmTmCt (TmCoreCt x e) -pattern PmConCt :: Id -> PmAltCon -> [TyVar] -> [Id] -> PmCt -pattern PmConCt x con tvs args = PmTmCt (TmConCt x con tvs args) -pattern PmNotConCt :: Id -> PmAltCon -> PmCt -pattern PmNotConCt x con = PmTmCt (TmNotConCt x con) -pattern PmBotCt :: Id -> PmCt -pattern PmBotCt x = PmTmCt (TmBotCt x) -pattern PmNotBotCt :: Id -> PmCt -pattern PmNotBotCt x = PmTmCt (TmNotBotCt x) -{-# COMPLETE PmTyCt, PmVarCt, PmCoreCt, PmConCt, PmNotConCt, PmBotCt, PmNotBotCt #-} - -instance Outputable PmCt where - ppr (PmTyCt pred_ty) = ppr pred_ty - ppr (PmTmCt tm_ct) = ppr tm_ct + pp_tvs = map ((<> char '@') . ppr) tvs + pp_dicts = map ppr dicts + pp_args = map ppr args + ppr (PhiNotConCt x con) = ppr x <+> text "≁" <+> ppr con + ppr (PhiBotCt x) = ppr x <+> text "~ ⊥" + ppr (PhiNotBotCt x) = ppr x <+> text "≁ ⊥" + +type PhiCts = Bag PhiCt + +-- | The fuel for the inhabitation test. +-- See Note [Fuel for the inhabitation test]. +initFuel :: Int +initFuel = 4 -- 4 because it's the smallest number that passes f' in T17977b -- | Adds new constraints to 'Nabla' and returns 'Nothing' if that leads to a -- contradiction. -addPmCts :: Nabla -> PmCts -> DsM (Maybe Nabla) +-- +-- In terms of the paper, this function models the \(⊕_φ\) function in +-- Figure 7 on batches of φ constraints. +addPhiCts :: Nabla -> PhiCts -> DsM (Maybe Nabla) -- See Note [TmState invariants]. -addPmCts nabla cts = do - let (ty_cts, tm_cts) = partitionTyTmCts cts - runSatisfiabilityCheck nabla $ mconcat - [ tyIsSatisfiable True (listToBag ty_cts) - , tmIsSatisfiable (listToBag tm_cts) - ] - -partitionTyTmCts :: PmCts -> ([TyCt], [TmCt]) -partitionTyTmCts = partitionEithers . map to_either . toList +addPhiCts nabla cts = runMaybeT $ do + let (ty_cts, tm_cts) = partitionPhiCts cts + nabla' <- addTyCts nabla (listToBag ty_cts) + nabla'' <- foldlM addPhiTmCt nabla' (listToBag tm_cts) + inhabitationTest initFuel (nabla_ty_st nabla) nabla'' + +partitionPhiCts :: PhiCts -> ([PredType], [PhiCt]) +partitionPhiCts = partitionEithers . map to_either . toList where - to_either (PmTyCt pred_ty) = Left pred_ty - to_either (PmTmCt tm_ct) = Right tm_ct - --- | Adds a single term constraint by dispatching to the various term oracle --- functions. -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 + to_either (PhiTyCt pred_ty) = Left pred_ty + to_either ct = Right ct + +----------------------------- +-- ** Adding type constraints + +-- | Adds new type-level constraints by calling out to the type-checker via +-- 'tyOracle'. +addTyCts :: Nabla -> Bag PredType -> MaybeT DsM Nabla +addTyCts nabla@MkNabla{ nabla_ty_st = ty_st } new_ty_cs = do + ty_st' <- MaybeT (tyOracle ty_st new_ty_cs) + pure nabla{ nabla_ty_st = ty_st' } + +-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we +-- find a contradiction (e.g. @Int ~ Bool@). +tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState) +tyOracle ty_st@(TySt n inert) cts + | isEmptyBag cts + = pure (Just ty_st) + | otherwise + = do { evs <- traverse nameTyCt cts + ; tracePm "tyOracle" (ppr cts $$ ppr inert) + ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability inert evs + ; case res of + -- return the new inert set and increment the sequence number n + Just mb_new_inert -> return (TySt (n+1) <$> mb_new_inert) + Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) } + +-- | Allocates a fresh 'EvVar' name for 'PredTy's. +nameTyCt :: PredType -> DsM EvVar +nameTyCt pred_ty = do + unique <- getUniqueM + let occname = mkVarOccFS (fsLit ("pm_"++show unique)) + idname = mkInternalName unique occname noSrcSpan + return (mkLocalIdOrCoVar idname Many pred_ty) + +----------------------------- +-- ** Adding term constraints + +-- | Adds a single higher-level φ constraint by dispatching to the various +-- oracle functions. +-- +-- In terms of the paper, this function amounts to the constructor constraint +-- case of \(⊕_φ\) in Figure 7, which "desugars" higher-level φ constraints +-- into lower-level δ constraints. We don't have a data type for δ constraints +-- and call the corresponding oracle function directly instead. +-- +-- Precondition: The φ is /not/ a type constraint! These should be handled by +-- 'addTyCts' before, through 'addPhiCts'. +addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla +addPhiTmCt _ (PhiTyCt ct) = pprPanic "addPhiCt:TyCt" (ppr ct) -- See the precondition +addPhiTmCt nabla (PhiCoreCt x e) = addCoreCt nabla x e +addPhiTmCt nabla (PhiConCt x con tvs dicts args) = do + -- Case (1) of Note [Strict fields and variables of unlifted type] + -- PhiConCt correspond to the higher-level φ constraints from the paper with + -- bindings semantics. It disperses into lower-level δ constraints that the + -- 'add*Ct' functions correspond to. + nabla' <- addTyCts nabla (listToBag dicts) + nabla'' <- addConCt nabla' x con tvs args + foldlM addNotBotCt nabla'' (filterUnliftedFields con args) +addPhiTmCt nabla (PhiNotConCt x con) = addNotConCt nabla x con +addPhiTmCt nabla (PhiBotCt x) = addBotCt nabla x +addPhiTmCt nabla (PhiNotBotCt x) = addNotBotCt nabla x + +filterUnliftedFields :: PmAltCon -> [Id] -> [Id] +filterUnliftedFields con args = + [ arg | (arg, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con) + , isBanged bang || isUnliftedType (idType arg) ] -- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@ -- surely diverges. Quite similar to 'addConCt', only that it only cares about -- ⊥. addBotCt :: Nabla -> Id -> MaybeT DsM Nabla -addBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do +addBotCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x = do let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x case bot of IsNotBot -> mzero -- There was x ≁ ⊥. Contradiction! IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do MaybeBot -> do -- We add x ~ ⊥ let vi' = vi{ vi_bot = IsBot } - pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi') reps} + pure nabla{ nabla_tm_st = ts{ts_facts = setEntrySDIE env y vi' } } + +-- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt', +-- but only cares for the ⊥ "constructor". +addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla +addNotBotCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts=env} } x = do + let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x + case bot of + IsBot -> mzero -- There was x ~ ⊥. Contradiction! + IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do + MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited + -- Mark dirty for a delayed inhabitation test + let vi' = vi{ vi_bot = IsNotBot} + pure $ markDirty y + $ nabla{ nabla_tm_st = ts{ ts_facts = setEntrySDIE env y vi' } } -- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't -- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if -- that leads to a contradiction. -- See Note [TmState invariants]. addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla -addNotConCt _ _ (PmAltConLike (RealDataCon dc)) +addNotConCt _ _ (PmAltConLike (RealDataCon dc)) | isNewDataCon dc = mzero -- (3) in Note [Coverage checking Newtype matches] -addNotConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do - let vi@(VI _ pos neg _ rcm) = 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)) - -- 2. Only record the new fact when it's not already implied by one of the - -- solutions - let implies nalt (cl, _tvs, _args) = eqPmAltCon cl nalt == Disjoint - let neg' - | any (implies nalt) pos = neg - -- See Note [Completeness checking with required Thetas] - | hasRequiredTheta nalt = neg - | otherwise = extendPmAltConSet neg nalt - MASSERT( isPmAltConMatchStrict nalt ) - let vi1 = vi{ vi_neg = neg', vi_bot = IsNotBot } - -- 3. Make sure there's at least one other possible constructor - vi2 <- case nalt of - PmAltConLike cl -> do - rcm' <- lift (markMatched cl rcm) - ensureInhabited nabla vi1{ vi_rcm = rcm' } - _ -> - pure vi1 - pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env x vi2) reps } +addNotConCt nabla x nalt = do + (mb_mark_dirty, nabla') <- trvVarInfo go nabla x + pure $ case mb_mark_dirty of + Just x -> markDirty x nabla' + Nothing -> nabla' + where + go vi@(VI x' pos neg _ rcm) = do + -- 1. Bail out quickly when nalt contradicts a solution + let contradicts nalt sol = eqPmAltCon (paca_con sol) nalt == Equal + guard (not (any (contradicts nalt) pos)) + -- 2. Only record the new fact when it's not already implied by one of the + -- solutions + let implies nalt sol = eqPmAltCon (paca_con sol) nalt == Disjoint + let neg' + | any (implies nalt) pos = neg + -- See Note [Completeness checking with required Thetas] + | hasRequiredTheta nalt = neg + | otherwise = extendPmAltConSet neg nalt + MASSERT( isPmAltConMatchStrict nalt ) + let vi' = vi{ vi_neg = neg', vi_bot = IsNotBot } + -- 3. Make sure there's at least one other possible constructor + case nalt of + PmAltConLike cl -> do + -- Mark dirty to force a delayed inhabitation test + rcm' <- lift (markMatched cl rcm) + pure (Just x', vi'{ vi_rcm = rcm' }) + _ -> + pure (Nothing, vi') hasRequiredTheta :: PmAltCon -> Bool hasRequiredTheta (PmAltConLike cl) = notNull req_theta @@ -951,159 +778,54 @@ hasRequiredTheta (PmAltConLike cl) = notNull req_theta (_,_,_,_,req_theta,_,_) = conLikeFullSig cl hasRequiredTheta _ = False -{- Note [Completeness checking with required Thetas] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider the situation in #11224 - - import Text.Read (readMaybe) - pattern PRead :: Read a => () => a -> String - pattern PRead x <- (readMaybe -> Just x) - f :: String -> Int - f (PRead x) = x - f (PRead xs) = length xs - f _ = 0 - -Is the first match exhaustive on the PRead synonym? Should the second line thus -deemed redundant? The answer is, of course, No! The required theta is like a -hidden parameter which must be supplied at the pattern match site, so PRead -is much more like a view pattern (where behavior depends on the particular value -passed in). -The simple solution here is to forget in 'addNotConCt' that we matched -on synonyms with a required Theta like @PRead@, so that subsequent matches on -the same constructor are never flagged as redundant. The consequence is that -we no longer detect the actually redundant match in - - g :: String -> Int - g (PRead x) = x - g (PRead y) = y -- redundant! - g _ = 0 - -But that's a small price to pay, compared to the proper solution here involving -storing required arguments along with the PmAltConLike in 'vi_neg'. --} - --- | Guess the universal argument types of a ConLike from an instantiation of --- its result type. Rather easy for DataCons, but not so much for PatSynCons. --- See Note [Pattern synonym result type] in "GHC.Core.PatSyn". -guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type] -guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon dc) = do - (tc, tc_args) <- splitTyConApp_maybe res_ty - -- Consider data families: In case of a DataCon, we need to translate to - -- the representation TyCon. For PatSyns, they are relative to the data - -- family TyCon, so we don't need to translate them. - let (rep_tc, tc_args', _) = tcLookupDataFamInst env tc tc_args - if rep_tc == dataConTyCon dc - then Just tc_args' - else Nothing -guessConLikeUnivTyArgsFromResTy _ res_ty (PatSynCon ps) = do - -- We are successful if we managed to instantiate *every* univ_tv of con. - -- This is difficult and bound to fail in some cases, see - -- Note [Pattern synonym result type] in GHC.Core.PatSyn. So we just try our best - -- here and be sure to return an instantiation when we can substitute every - -- universally quantified type variable. - -- We *could* instantiate all the other univ_tvs just to fresh variables, I - -- suppose, but that means we get weird field types for which we don't know - -- anything. So we prefer to keep it simple here. - let (univ_tvs,_,_,_,_,con_res_ty) = patSynSig ps - subst <- tcMatchTy con_res_ty res_ty - traverse (lookupTyVar subst) univ_tvs - --- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt', --- but only cares for the ⊥ "constructor". -addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla -addNotBotCt nabla@MkNabla{ nabla_tm_st = TmSt env reps } x = do - let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x - case bot of - IsBot -> mzero -- There was x ~ ⊥. Contradiction! - IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do - MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited - vi <- ensureInhabited nabla vi{ vi_bot = IsNotBot } - pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi) reps} - --- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE --- set satisfies the oracle --- --- Internally uses and updates the ConLikeSets in vi_rcm. +-- | Add a @x ~ K tvs args ts@ constraint. +-- @addConCt x K tvs args ts@ extends the substitution with a solution +-- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we +-- have on @x@, reject (@Nothing@) otherwise. -- --- 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 (add_matches vi) >>= inst_complete_sets - where - add_matches :: VarInfo -> DsM VarInfo - add_matches vi = do - res <- pmTopNormaliseType (nabla_ty_st nabla) (vi_ty vi) - rcm <- case reprTyCon_maybe (normalisedSourceType res) of - Just tc -> addTyConMatches tc (vi_rcm vi) - Nothing -> addCompleteMatches (vi_rcm vi) - pure vi{ vi_rcm = rcm } - - reprTyCon_maybe :: Type -> Maybe TyCon - reprTyCon_maybe ty = case splitTyConApp_maybe ty of - Nothing -> Nothing - Just (tc, _args) -> case tyConFamInst_maybe tc of - Nothing -> Just tc - Just (tc_fam, _) -> Just tc_fam - - -- | 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. - -- See also Note [Implementation of COMPLETE pragmas]. - inst_complete_sets :: VarInfo -> MaybeT DsM VarInfo - inst_complete_sets vi@VI{ vi_rcm = rcm } = do - rcm' <- trvRcm (\cls -> inst_complete_set vi cls (uniqDSetToList cls)) rcm - pure vi{ vi_rcm = rcm' } - - 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 - inst_complete_set _ _ [] = mzero - inst_complete_set vi cs (con:cons) = lift (inst_and_test vi con) >>= \case - True -> pure cs - False -> inst_complete_set vi (delOneFromUniqDSet cs con) cons - - inst_and_test :: VarInfo -> ConLike -> DsM Bool - -- @inst_and_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly - -- be of form @K _ _ _@. Returning True is always sound. - -- - -- It's like 'DataCon.dataConCannotMatch', but more clever because it takes - -- the facts in 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 "inst_and_test" (ppr con $$ ppr ty_cs) - -- No need to run the term oracle compared to pmIsSatisfiable - fmap isJust <$> runSatisfiabilityCheck nabla $ mconcat - -- Important to pass False to tyIsSatisfiable here, so that we won't - -- 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_rcm', considering the current type information in 'Nabla'. --- This check is necessary after having matched on a GADT con to weed out --- impossible matches. -ensureAllInhabited :: Nabla -> DsM (Maybe Nabla) -ensureAllInhabited nabla@MkNabla{ nabla_tm_st = TmSt env reps } - = runMaybeT (set_tm_cs_env nabla <$> traverseSDIE go env) - where - set_tm_cs_env nabla env = nabla{ nabla_tm_st = TmSt env reps } - go vi = ensureInhabited nabla vi +-- See Note [TmState invariants]. +addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla +addConCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x alt tvs args = do + let vi@(VI _ pos neg bot _) = 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 + -- additional refinement of the possible values x could take) indicate a + -- contradiction + guard (all ((/= Disjoint) . eqPmAltCon alt . paca_con) pos) + -- Now we should be good! Add (alt, tvs, args) as a possible solution, or + -- refine an existing one + case find ((== Equal) . eqPmAltCon alt . paca_con) pos of + Just (PACA _con other_tvs other_args) -> do + -- We must unify existentially bound ty vars and arguments! + let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs) + when (length args /= length other_args) $ + lift $ tracePm "error" (ppr x <+> ppr alt <+> ppr args <+> ppr other_args) + nabla' <- MaybeT $ addPhiCts nabla (listToBag ty_cts) + let add_var_ct nabla (a, b) = addVarCt nabla a b + foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args + Nothing -> do + let pos' = PACA alt tvs args : pos + let nabla_with bot' = + nabla{ nabla_tm_st = ts{ts_facts = setEntrySDIE env x (vi{vi_pos = pos', vi_bot = bot'})} } + -- 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 ⊥ --------------------------------------- --- * Term oracle unification procedure +equateTys :: [Type] -> [Type] -> [PhiCt] +equateTys ts us = + [ PhiTyCt (mkPrimEqPred t u) + | (t, u) <- zipEqual "equateTys" ts us + -- The following line filters out trivial Refl constraints, so that we don't + -- need to initialise the type oracle that often + , not (eqType t u) + ] -- | Adds a @x ~ y@ constraint by trying to unify two 'Id's and record the -- gained knowledge in 'Nabla'. @@ -1114,7 +836,7 @@ ensureAllInhabited nabla@MkNabla{ nabla_tm_st = TmSt env reps } -- -- See Note [TmState invariants]. addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla -addVarCt nabla@MkNabla{ nabla_tm_st = TmSt env _ } x y +addVarCt nabla@MkNabla{ nabla_tm_st = TmSt{ ts_facts = 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 @@ -1130,23 +852,23 @@ addVarCt nabla@MkNabla{ nabla_tm_st = TmSt env _ } x y -- -- See Note [TmState invariants]. equate :: Nabla -> Id -> Id -> MaybeT DsM Nabla -equate nabla@MkNabla{ nabla_tm_st = TmSt env reps } x y +equate nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts = env} } x y = ASSERT( not (sameRepresentativeSDIE env x y) ) case (lookupSDIE env x, lookupSDIE env y) of - (Nothing, _) -> pure (nabla{ nabla_tm_st = TmSt (setIndirectSDIE env x y) reps }) - (_, Nothing) -> pure (nabla{ nabla_tm_st = TmSt (setIndirectSDIE env y x) reps }) + (Nothing, _) -> pure (nabla{ nabla_tm_st = ts{ ts_facts = setIndirectSDIE env x y } }) + (_, Nothing) -> pure (nabla{ nabla_tm_st = ts{ ts_facts = setIndirectSDIE env y x } }) -- 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... -- We should decide how to break the tie - MASSERT2( vi_ty vi_x `eqType` vi_ty vi_y, text "Not same type" ) + MASSERT2( idType (vi_id vi_x) `eqType` idType (vi_id vi_y), text "Not same type" ) -- First assume that x and y are in the same equivalence class let env_ind = setIndirectSDIE env x y -- Then sum up the refinement counters let env_refs = setEntrySDIE env_ind y vi_y - let nabla_refs = nabla{ nabla_tm_st = TmSt env_refs reps } + let nabla_refs = nabla{ nabla_tm_st = ts{ts_facts = env_refs} } -- and then gradually merge every positive fact we have on x into y - let add_fact nabla (cl, tvs, args) = addConCt nabla y cl tvs args + let add_fact nabla (PACA 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 nabla nalt = addNotConCt nabla y nalt @@ -1155,549 +877,6 @@ equate nabla@MkNabla{ nabla_tm_st = TmSt env reps } x y -- go! pure nabla_neg --- | Add a @x ~ K tvs args ts@ constraint. --- @addConCt x K tvs args ts@ extends the substitution with a solution --- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we --- have on @x@, reject (@Nothing@) otherwise. --- --- See Note [TmState invariants]. -addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla -addConCt nabla@MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x alt tvs args = do - let VI ty pos neg bot rcm = 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 - -- additional refinement of the possible values x could take) indicate a - -- contradiction - guard (all ((/= Disjoint) . eqPmAltCon alt . fstOf3) pos) - -- Now we should be good! Add (alt, tvs, args) as a possible solution, or - -- refine an existing one - case find ((== Equal) . eqPmAltCon alt . fstOf3) pos of - Just (_con, other_tvs, other_args) -> do - -- We must unify existentially bound ty vars and arguments! - let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs) - 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 nabla (listToBag ty_cts `unionBags` listToBag tm_cts) - Nothing -> do - let pos' = (alt, tvs, args):pos - let nabla_with bot = - nabla{ nabla_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg bot rcm)) 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 = - [ PmTyCt (mkPrimEqPred t u) - | (t, u) <- zipEqual "equateTys" ts us - -- The following line filters out trivial Refl constraints, so that we don't - -- need to initialise the type oracle that often - , not (eqType t u) - ] - ----------------------------------------- --- * Enumerating inhabitation candidates - --- | Information about a conlike that is relevant to coverage checking. --- It is called an \"inhabitation candidate\" since it is a value which may --- possibly inhabit some type, but only if its term constraints ('ic_tm_cs') --- and type constraints ('ic_ty_cs') are permitting, and if all of its strict --- argument types ('ic_strict_arg_tys') are inhabitable. --- See @Note [Strict argument type constraints]@. -data InhabitationCandidate = - InhabitationCandidate - { ic_cs :: PmCts - , ic_strict_arg_tys :: [Type] - } - -instance Outputable InhabitationCandidate where - ppr (InhabitationCandidate cs strict_arg_tys) = - text "InhabitationCandidate" <+> - vcat [ text "ic_cs =" <+> ppr cs - , text "ic_strict_arg_tys =" <+> ppr strict_arg_tys ] - -mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate --- Precondition: idType x is a TyConApp, so that tyConAppArgs in here is safe. -mkInhabitationCandidate x dc = do - let cl = RealDataCon dc - let tc_args = tyConAppArgs (idType x) - (ty_vars, arg_vars, ty_cs, strict_arg_tys) <- mkOneConFull tc_args cl - pure InhabitationCandidate - { ic_cs = PmTyCt <$> ty_cs `snocBag` PmConCt x (PmAltConLike cl) ty_vars arg_vars - , ic_strict_arg_tys = strict_arg_tys - } - --- | Generate all 'InhabitationCandidate's for a given type. The result is --- either @'Left' ty@, if the type cannot be reduced to a closed algebraic type --- (or if it's one trivially inhabited, like 'Int'), or @'Right' candidates@, --- 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 :: Nabla -> Type - -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) -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' [] - HadRedexes src_ty dcs core_ty -> alts_to_check src_ty core_ty dcs - where - build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, PmCt) - build_newtype (ty, dc, _arg_ty) x = do - -- ty is the type of @dc x@. It's a @dataConTyCon dc@ application. - y <- mkPmId ty - -- Newtypes don't have existentials (yet?!), so passing an empty list as - -- ex_tvs. - pure (y, PmConCt y (PmAltConLike (RealDataCon dc)) [] [x]) - - build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt]) - build_newtypes x = foldrM (\dc (x, cts) -> go dc x cts) (x, []) - where - go dc x cts = second (:cts) <$> build_newtype dc x - - -- Inhabitation candidates, using the result of pmTopNormaliseType - alts_to_check :: Type -> Type -> [(Type, DataCon, Type)] - -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) - alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of - Just (tc, _) - | isTyConTriviallyInhabited tc - -> case dcs of - [] -> return (Left src_ty) - (_:_) -> do inner <- mkPmId core_ty - (outer, new_tm_cts) <- build_newtypes inner dcs - return $ Right (tc, outer, [InhabitationCandidate - { ic_cs = listToBag new_tm_cts - , ic_strict_arg_tys = [] }]) - - | pmIsClosedType core_ty && not (isAbstractTyCon tc) - -- Don't consider abstract tycons since we don't know what their - -- constructors are, which makes the results of coverage checking - -- them extremely misleading. - -> do - inner <- mkPmId core_ty -- it would be wrong to unify inner - alts <- mapM (mkInhabitationCandidate inner) (tyConDataCons tc) - (outer, new_cts) <- build_newtypes inner dcs - let wrap_dcs alt = alt{ ic_cs = listToBag new_cts `unionBags` ic_cs alt} - return $ Right (tc, outer, map wrap_dcs alts) - -- For other types conservatively assume that they are inhabited. - _other -> return (Left src_ty) - --- | All these types are trivially inhabited -triviallyInhabitedTyCons :: UniqSet TyCon -triviallyInhabitedTyCons = mkUniqSet [ - charTyCon, doubleTyCon, floatTyCon, intTyCon, wordTyCon, word8TyCon - ] - -isTyConTriviallyInhabited :: TyCon -> Bool -isTyConTriviallyInhabited tc = elementOfUniqSet tc triviallyInhabitedTyCons - ----------------------------- --- * Detecting vacuous types - -{- Note [Checking EmptyCase Expressions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Empty case expressions are strict on the scrutinee. That is, `case x of {}` -will force argument `x`. Hence, `covCheckMatches` is not sufficient for checking -empty cases, because it assumes that the match is not strict (which is true -for all other cases, apart from EmptyCase). This gave rise to #10746. Instead, -we do the following: - -1. We normalise the outermost type family redex, data family redex or newtype, - using pmTopNormaliseType (in "GHC.Core.FamInstEnv"). This computes 3 - things: - (a) A normalised type src_ty, which is equal to the type of the scrutinee in - source Haskell (does not normalise newtypes or data families) - (b) The actual normalised type core_ty, which coincides with the result - topNormaliseType_maybe. This type is not necessarily equal to the input - type in source Haskell. And this is precicely the reason we compute (a) - and (c): the reasoning happens with the underlying types, but both the - patterns and types we print should respect newtypes and also show the - family type constructors and not the representation constructors. - - (c) A list of all newtype data constructors dcs, each one corresponding to a - newtype rewrite performed in (b). - - For an example see also Note [Type normalisation] - in "GHC.Core.FamInstEnv". - -2. Function Check.checkEmptyCase' performs the check: - - If core_ty is not an algebraic type, then we cannot check for - inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming - that the type is inhabited. - - If core_ty is an algebraic type, then we unfold the scrutinee to all - possible constructor patterns, using inhabitationCandidates, and then - check each one for constraint satisfiability, same as we do for normal - pattern match checking. --} - --- | A 'SatisfiabilityCheck' based on "NonVoid ty" constraints, e.g. Will --- check if the @strict_arg_tys@ are actually all inhabited. --- 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 $ \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 nabla - else Nothing - --- | Implements two performance optimizations, as described in --- @Note [Strict argument type constraints]@. -checkAllNonVoid :: RecTcChecker -> Nabla -> [Type] -> DsM Bool -checkAllNonVoid rec_ts amb_cs strict_arg_tys = do - 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 - = 1 - | otherwise - = 3 - rec_ts' = setRecTcMaxBound rec_max_bound rec_ts - allM (nonVoid rec_ts' amb_cs) tys_to_check - --- | Checks if a strict argument type of a conlike is inhabitable by a --- terminating value (i.e, an 'InhabitationCandidate'). --- See @Note [Strict argument type constraints]@. -nonVoid - :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit. - -> 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 - -- a terminating value (i.e., an 'InhabitationCandidate'). - -- 'False' if it is definitely uninhabitable by anything - -- (except bottom). -nonVoid rec_ts amb_cs strict_arg_ty = do - mb_cands <- inhabitationCandidates amb_cs strict_arg_ty - case mb_cands of - Right (tc, _, cands) - -- See Note [Fuel for the inhabitation test] - | Just rec_ts' <- checkRecTc rec_ts tc - -> anyM (cand_is_inhabitable rec_ts' amb_cs) cands - -- A strict argument type is inhabitable by a terminating value if - -- at least one InhabitationCandidate is inhabitable. - _ -> pure True - -- Either the type is trivially inhabited or we have exceeded the - -- recursion depth for some TyCon (so bail out and conservatively - -- claim the type is inhabited). - where - -- Checks if an InhabitationCandidate for a strict argument type: - -- - -- (1) Has satisfiable term and type constraints. - -- (2) Has 'nonVoid' strict argument types (we bail out of this - -- check if recursion is detected). - -- - -- See Note [Strict argument type constraints] - cand_is_inhabitable :: RecTcChecker -> Nabla - -> InhabitationCandidate -> DsM Bool - cand_is_inhabitable rec_ts amb_cs - (InhabitationCandidate{ ic_cs = new_cs - , ic_strict_arg_tys = new_strict_arg_tys }) = do - let (new_ty_cs, new_tm_cs) = partitionTyTmCts new_cs - fmap isJust $ runSatisfiabilityCheck amb_cs $ mconcat - [ tyIsSatisfiable False (listToBag new_ty_cs) - , tmIsSatisfiable (listToBag new_tm_cs) - , tysAreNonVoid rec_ts new_strict_arg_tys - ] - --- | @'definitelyInhabitedType' ty@ returns 'True' if @ty@ has at least one --- constructor @C@ such that: --- --- 1. @C@ has no equality constraints. --- 2. @C@ has no strict argument types. --- --- See the @Note [Strict argument type constraints]@. -definitelyInhabitedType :: TyState -> Type -> DsM Bool -definitelyInhabitedType ty_st ty = do - res <- pmTopNormaliseType ty_st ty - pure $ case res of - HadRedexes _ cons _ -> any meets_criteria cons - _ -> False - where - meets_criteria :: (Type, DataCon, Type) -> Bool - meets_criteria (_, con, _) = - null (dataConEqSpec con) && -- (1) - null (dataConImplBangs con) -- (2) - -{- Note [Strict argument type constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In the ConVar case of clause processing, each conlike K traditionally -generates two different forms of constraints: - -* A term constraint (e.g., x ~ K y1 ... yn) -* Type constraints from the conlike's context (e.g., if K has type - forall bs. Q => s1 .. sn -> T tys, then Q would be its type constraints) - -As it turns out, these alone are not enough to detect a certain class of -unreachable code. Consider the following example (adapted from #15305): - - data K = K1 | K2 !Void - - f :: K -> () - f K1 = () - -Even though `f` doesn't match on `K2`, `f` is exhaustive in its patterns. Why? -Because it's impossible to construct a terminating value of type `K` using the -`K2` constructor, and thus it's impossible for `f` to ever successfully match -on `K2`. - -The reason is because `K2`'s field of type `Void` is //strict//. Because there -are no terminating values of type `Void`, any attempt to construct something -using `K2` will immediately loop infinitely or throw an exception due to the -strictness annotation. (If the field were not strict, then `f` could match on, -say, `K2 undefined` or `K2 (let x = x in x)`.) - -Since neither the term nor type constraints mentioned above take strict -argument types into account, we make use of the `nonVoid` function to -determine whether a strict type is inhabitable by a terminating value or not. -We call this the "inhabitation test". - -`nonVoid ty` returns True when either: -1. `ty` has at least one InhabitationCandidate for which both its term and type - constraints are satisfiable, and `nonVoid` returns `True` for all of the - strict argument types in that InhabitationCandidate. -2. We're unsure if it's inhabited by a terminating value. - -`nonVoid ty` returns False when `ty` is definitely uninhabited by anything -(except bottom). Some examples: - -* `nonVoid Void` returns False, since Void has no InhabitationCandidates. - (This is what lets us discard the `K2` constructor in the earlier example.) -* `nonVoid (Int :~: Int)` returns True, since it has an InhabitationCandidate - (through the Refl constructor), and its term constraint (x ~ Refl) and - type constraint (Int ~ Int) are satisfiable. -* `nonVoid (Int :~: Bool)` returns False. Although it has an - InhabitationCandidate (by way of Refl), its type constraint (Int ~ Bool) is - not satisfiable. -* Given the following definition of `MyVoid`: - - data MyVoid = MkMyVoid !Void - - `nonVoid MyVoid` returns False. The InhabitationCandidate for the MkMyVoid - constructor contains Void as a strict argument type, and since `nonVoid Void` - returns False, that InhabitationCandidate is discarded, leaving no others. -* Whether or not a type is inhabited is undecidable in general. - See Note [Fuel for the inhabitation test]. -* For some types, inhabitation is evident immediately and we don't need to - perform expensive tests. See Note [Types that are definitely inhabitable]. - -Note [Fuel for the inhabitation test] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Whether or not a type is inhabited is undecidable in general. As a result, we -can run into infinite loops in `nonVoid`. Therefore, we adopt a fuel-based -approach to prevent that. - -Consider the following example: - - data Abyss = MkAbyss !Abyss - stareIntoTheAbyss :: Abyss -> a - stareIntoTheAbyss x = case x of {} - -In principle, stareIntoTheAbyss is exhaustive, since there is no way to -construct a terminating value using MkAbyss. However, both the term and type -constraints for MkAbyss are satisfiable, so the only way one could determine -that MkAbyss is unreachable is to check if `nonVoid Abyss` returns False. -There is only one InhabitationCandidate for Abyss—MkAbyss—and both its term -and type constraints are satisfiable, so we'd need to check if `nonVoid Abyss` -returns False... and now we've entered an infinite loop! - -To avoid this sort of conundrum, `nonVoid` uses a simple test to detect the -presence of recursive types (through `checkRecTc`), and if recursion is -detected, we bail out and conservatively assume that the type is inhabited by -some terminating value. This avoids infinite loops at the expense of making -the coverage checker incomplete with respect to functions like -stareIntoTheAbyss above. Then again, the same problem occurs with recursive -newtypes, like in the following code: - - newtype Chasm = MkChasm Chasm - gazeIntoTheChasm :: Chasm -> a - gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive - -So this limitation is somewhat understandable. - -Note that even with this recursion detection, there is still a possibility that -`nonVoid` can run in exponential time. Consider the following data type: - - data T = MkT !T !T !T - -If we call `nonVoid` on each of its fields, that will require us to once again -check if `MkT` is inhabitable in each of those three fields, which in turn will -require us to check if `MkT` is inhabitable again... As you can see, the -branching factor adds up quickly, and if the recursion depth limit is, say, -100, then `nonVoid T` will effectively take forever. - -To mitigate this, we check the branching factor every time we are about to call -`nonVoid` on a list of strict argument types. If the branching factor exceeds 1 -(i.e., if there is potential for exponential runtime), then we limit the -maximum recursion depth to 1 to mitigate the problem. If the branching factor -is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay -to stick with a larger maximum recursion depth. - -In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was -too large and had detrimental effect on performance of the coverage checker. -Given that we only commit to a best effort anyway, we decided to substantially -decrement the recursion depth to 3, at the cost of precision in some edge cases -like - - data Nat = Z | S Nat - data Down :: Nat -> Type where - Down :: !(Down n) -> Down (S n) - f :: Down (S (S (S (S (S Z))))) -> () - f x = case x of {} - -Since the coverage won't bother to instantiate Down 4 levels deep to see that it -is in fact uninhabited, it will emit a inexhaustivity warning for the case. - -Note [Types that are definitely inhabitable] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Another microoptimization applies to data types like this one: - - data S a = S ![a] !T - -Even though there is a strict field of type [a], it's quite silly to call -nonVoid on it, since it's "obvious" that it is inhabitable. To make this -intuition formal, we say that a type is definitely inhabitable (DI) if: - - * It has at least one constructor C such that: - 1. C has no equality constraints (since they might be unsatisfiable) - 2. C has no strict argument types (since they might be uninhabitable) - -It's relatively cheap to check if a type is DI, so before we call `nonVoid` -on a list of strict argument types, we filter out all of the DI ones. --} - --------------------------------------------- --- * Providing positive evidence for a Nabla - --- | @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 -> Nabla -> DsM [Nabla] -provideEvidence = go - where - go _ 0 _ = pure [] - 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 - -- fields. Example: - -- f x@(Just _) True = case x of SomePatSyn _ -> () - -- after this clause, we want to report that - -- * @f Nothing _@ is uncovered - -- * @f x False@ is uncovered - -- where @x@ will have two possibly compatible solutions, @Just y@ for - -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@ - -- and @z@ that is valid at the same time. These constitute arg_vas below. - let arg_vas = concatMap (\(_cl, _tvs, args) -> args) pos - go (arg_vas ++ xs) n nabla - [] - -- When there are literals involved, just print negative info - -- instead of listing missed constructors - | notNull [ l | PmAltLit l <- pmAltConSetElems neg ] - -> 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 -> Nabla -> DsM [Nabla] - -- Convention: x binds the outer constructor in the chain, y the inner one. - try_instantiate x xs n nabla = do - (_src_ty, dcs, rep_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. - nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y] - pure (y, nabla') - runMaybeT (foldlM build_newtype (x, nabla) dcs) >>= \case - Nothing -> pure [] - Just (y, newty_nabla) -> do - -- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥. - let vi = lookupVarInfo (nabla_tm_st newty_nabla) y - rcm <- case splitTyConApp_maybe rep_ty of - Nothing -> pure (vi_rcm vi) - Just (tc, _) -> addTyConMatches tc (vi_rcm vi) - mb_cls <- pickMinimalCompleteSet rep_ty rcm - case uniqDSetToList <$> mb_cls of - Just cls -> do - nablas <- instantiate_cons y rep_ty xs n newty_nabla cls - if null nablas && vi_bot vi /= IsNotBot - then go xs n newty_nabla -- bot is still possible. Display a wildcard! - else pure nablas - Nothing -> go xs n newty_nabla -- no COMPLETE sets ==> inhabited - - instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla] - instantiate_cons _ _ _ _ _ [] = pure [] - instantiate_cons _ _ _ 0 _ _ = pure [] - instantiate_cons _ ty xs n 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 nabla - instantiate_cons x ty xs n nabla (cl:cls) = do - env <- dsGetFamInstEnvs - case guessConLikeUnivTyArgsFromResTy env ty cl of - 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_nabla <- pmIsSatisfiable nabla new_ty_cs new_tm_cs strict_arg_tys - tracePm "instantiate_cons" (vcat [ ppr x - , ppr (idType x) - , ppr ty - , ppr cl - , ppr arg_tys - , ppr new_tm_cs - , ppr new_ty_cs - , ppr strict_arg_tys - , ppr nabla - , ppr mb_nabla - , ppr n ]) - 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 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 :: Type -> ResidualCompleteMatches -> DsM (Maybe ConLikeSet) -pickMinimalCompleteSet ty rcm = do - env <- dsGetFamInstEnvs - pure $ case filter (all (is_valid env) . uniqDSetToList) (getRcm rcm) of - [] -> Nothing - clss' -> Just (minimumBy (comparing sizeUniqDSet) clss') - where - is_valid :: FamInstEnvs -> ConLike -> Bool - is_valid env cl = isJust (guessConLikeUnivTyArgsFromResTy env ty cl) - --- | Finds a representant of the semantic equality class of the given @e@. --- 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 :: Nabla -> CoreExpr -> DsM (Nabla, Id) -representCoreExpr nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_reps = reps } } e - | Just rep <- lookupCoreMap reps e = pure (nabla, rep) - | otherwise = do - rep <- mkPmId (exprType e) - let reps' = extendCoreMap reps e rep - let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } } - pure (nabla', rep) - -- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based -- on the shape of the 'CoreExpr' @e@. Examples: -- @@ -1795,7 +974,7 @@ addCoreCt nabla x e = do when (not (isNewDataCon dc)) $ modifyT $ \nabla -> addNotBotCt nabla x -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703 - modifyT $ \nabla -> MaybeT $ addPmCts nabla (listToBag ty_cts) + modifyT $ \nabla -> MaybeT $ addPhiCts nabla (listToBag ty_cts) -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ arg_ids <- traverse bind_expr vis_args -- 4. @x ~ K as ys@ @@ -1813,12 +992,119 @@ addCoreCt nabla x e = do 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 +-- | Finds a representant of the semantic equality class of the given @e@. +-- 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 :: Nabla -> CoreExpr -> DsM (Nabla, Id) +representCoreExpr nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_reps = reps } } e + | Just rep <- lookupCoreMap reps e = pure (nabla, rep) + | otherwise = do + rep <- mkPmId (exprType e) + let reps' = extendCoreMap reps e rep + let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } } + pure (nabla', rep) + -- | Like 'modify', but with an effectful modifier action modifyT :: Monad m => (s -> m s) -> StateT s m () modifyT f = StateT $ fmap ((,) ()) . f -{- Note [Detecting pattern synonym applications in expressions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [The Pos/Neg invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Invariant applying to each VarInfo: Whenever we have @C @tvs args@ in 'vi_pos', +any entry in 'vi_neg' must be incomparable to C (return Nothing) according to +'eqPmAltCons'. Those entries that are comparable either lead to a refutation +or are redundant. Examples: +* @x ~ Just y@, @x ≁ [Just]@. 'eqPmAltCon' returns @Equal@, so refute. +* @x ~ Nothing@, @x ≁ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative + info is redundant and should be discarded. +* @x ~ I# y@, @x ≁ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal. + We keep this info in order to be able to refute a redundant match on i.e. 4 + later on. + +This carries over to pattern synonyms and overloaded literals. Say, we have + pattern Just42 = Just 42 + case Just42 of x + Nothing -> () + Just _ -> () +Even though we had a solution for the value abstraction called x here in form +of a PatSynCon Just42, this solution is incomparable to both Nothing and +Just. Hence we retain the info in vi_neg, which eventually allows us to detect +the complete pattern match. + +The Pos/Neg invariant extends to vi_rcm, which essentially stores positive +information. We make sure that vi_neg and vi_rcm never overlap. This isn't +strictly necessary since vi_rcm is just a cache, so doesn't need to be +accurate: Every suggestion of a possible ConLike from vi_rcm might be +refutable by the type oracle anyway. But it helps to maintain sanity while +debugging traces. + +Note [Why record both positive and negative info?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +You might think that knowing positive info (like x ~ Just y) would render +negative info irrelevant, but not so because of pattern synonyms. E.g we might +know that x cannot match (Foo 4), where pattern Foo p = Just p + +Also overloaded literals themselves behave like pattern synonyms. E.g if +postively we know that (x ~ I# y), we might also negatively want to record that +x does not match 45 f 45 = e2 f (I# 22#) = e3 f 45 = e4 -- +Overlapped + +Note [TmState invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~ +The term oracle state is never obviously (i.e., without consulting the type +oracle or doing inhabitation testing) contradictory. This implies a few +invariants: +* Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute. + This is implied by the Note [Pos/Neg invariant]. +* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_rcm to + detect this, but we could just compare whole COMPLETE sets to vi_neg every + time, if it weren't for performance. + +Maintaining these invariants in 'addVarCt' (the core of the term oracle) and +'addNotConCt' is subtle. +* Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate'). + - (COMPLETE) If we had @x ≁ True@ and @y ≁ False@, then we get + @x ≁ [True,False]@. This is vacuous by matter of comparing to the built-in + COMPLETE set, so should refute. + - (Pos/Neg) If we had @x ≁ True@ and @y ~ True@, we have to refute. +* Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt') + - (Neg) If we had @x ≁ K@, refute. + - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to + 'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute. + - (Refine) If we had @x ≁ K zs@, unify each y with each z in turn. +* Adding negative information. Example: Add the fact @x ≁ Nothing@ (see 'addNotConCt') + - (Refut) If we have @x ~ K ys@, refute. + - (COMPLETE) If K=Nothing and we had @x ≁ Just@, then we get + @x ≁ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in + COMPLETE set, so should refute. + +Note that merging VarInfo in equate can be done by calling out to 'addConCt' and +'addNotConCt' for each of the facts individually. + +Note [Representation of Strings in TmState] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Instead of treating regular String literals as a PmLits, we treat it as a list +of characters in the oracle for better overlap reasoning. The following example +shows why: + + f :: String -> () + f ('f':_) = () + f "foo" = () + f _ = () + +The second case is redundant, and we like to warn about it. Therefore either +the oracle will have to do some smart conversion between the list and literal +representation or treat is as the list it really is at runtime. + +The "smart conversion" has the advantage of leveraging the more compact literal +representation wherever possible, but is really nasty to get right with negative +equalities: Just think of how to encode @x /= "foo"@. +The "list" option is far simpler, but incurs some overhead in representation and +warning messages (which can be alleviated by someone with enough dedication). + +Note [Detecting pattern synonym applications in expressions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At the moment we fail to detect pattern synonyms in scrutinees and RHS of guards. This could be alleviated with considerable effort and complexity, but the returns are meager. Consider: @@ -1838,4 +1124,644 @@ knows "If it's a P, then its field is 15". This is a pretty narrow use case and I don't think we should to try to fix it until a user complains energetically. + +Note [Completeness checking with required Thetas] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the situation in #11224 + + import Text.Read (readMaybe) + pattern PRead :: Read a => () => a -> String + pattern PRead x <- (readMaybe -> Just x) + f :: String -> Int + f (PRead x) = x + f (PRead xs) = length xs + f _ = 0 + +Is the first match exhaustive on the PRead synonym? Should the second line thus +deemed redundant? The answer is, of course, No! The required theta is like a +hidden parameter which must be supplied at the pattern match site, so PRead +is much more like a view pattern (where behavior depends on the particular value +passed in). +The simple solution here is to forget in 'addNotConCt' that we matched +on synonyms with a required Theta like @PRead@, so that subsequent matches on +the same constructor are never flagged as redundant. The consequence is that +we no longer detect the actually redundant match in + + g :: String -> Int + g (PRead x) = x + g (PRead y) = y -- redundant! + g _ = 0 + +But that's a small price to pay, compared to the proper solution here involving +storing required arguments along with the PmAltConLike in 'vi_neg'. + +Note [Strict fields and variables of unlifted type] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Binders of unlifted type (and strict fields) are unlifted by construction; +they are conceived with an implicit @≁⊥@ constraint to begin with. Hence, +desugaring in "GHC.HsToCore.PmCheck" is entirely unconcerned by strict fields, +since the forcing happens *before* pattern matching. +And the φ constructor constraints emitted by 'GHC.HsToCore.PmCheck.checkGrd' +have complex binding semantics (binding type constraints and unlifted fields), +so unliftedness semantics are entirely confined to the oracle. + +These are the moving parts: + + 1. For each strict (or more generally, unlifted) field @s@ of a 'PhiConCt' + we have to add a @s ≁ ⊥@ constraint in the corresponding case of + 'addPhiTmCt'. 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 _ = () + + The second clause desugars to @MkT n <- x, !n@. When coverage checked, + the 'PmCon' @MkT n <- x@ refines the set of values that reach the bang + pattern with the φ constraints @MkT n <- x@ (Nothing surprising so far). + Upon that constraint, it disperses into two lower-level δ constraints + @x ~ MkT n, n ≁ ⊥@ per Equation (3) in Figure 7 of the paper. + + 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. + + 2. Similarly, when performing the 'inhabitationTest', when instantiating a + constructor we call 'instCon', which generates a higher-level φ + constructor constraint. + + 3. The preceding points handle unlifted constructor fields, but there also + are regular binders of unlifted type. + Since the oracle as implemented has no notion of scoping and bindings, + we can't know *when* an unlifted variable comes into scope. But that's + not actually a problem, because we can just add the @x ≁ ⊥@ to the + 'emptyVarInfo' when we first encounter it. +-} + +------------------------- +-- * Inhabitation testing +-- +-- Figure 8 in the LYG paper. + +tyStateRefined :: TyState -> TyState -> Bool +-- Makes use of the fact that the two TyStates we compare will never have the +-- same sequence number. It is invalid to call this function when a is not a +-- refinement of b or vice versa! +tyStateRefined a b = ty_st_n a /= ty_st_n b + +markDirty :: Id -> Nabla -> Nabla +markDirty x nabla@MkNabla{nabla_tm_st = ts@TmSt{ts_dirty = dirty} } = + nabla{ nabla_tm_st = ts{ ts_dirty = extendDVarSet dirty x } } + +traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState +traverseDirty f ts@TmSt{ts_facts = env, ts_dirty = dirty} = + go (uniqDSetToList dirty) env + where + go [] env = pure ts{ts_facts=env} + go (x:xs) !env = do + vi' <- f (lookupVarInfo ts x) + go xs (setEntrySDIE env x vi') + +traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState +traverseAll f ts@TmSt{ts_facts = env} = do + env' <- traverseSDIE f env + pure ts{ts_facts = env'} + +-- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate +-- all dirty variables (or all variables when the 'TyState' changed) to concrete +-- inhabitants. It returns a 'Nabla' with the *same* inhabitants, but with some +-- amount of work cached (like failed instantiation attempts) from the test. +-- +-- The \(∇ ⊢ x inh\) judgment form in Figure 8 of the LYG paper. +inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla +inhabitationTest 0 _ nabla = pure nabla +inhabitationTest fuel old_ty_st nabla@MkNabla{ nabla_tm_st = ts } = do + -- lift $ tracePm "inhabitation test" $ vcat + -- [ ppr fuel + -- , ppr old_ty_st + -- , ppr nabla + -- , text "tyStateRefined:" <+> ppr (tyStateRefined old_ty_st (nabla_ty_st nabla)) + -- ] + -- When type state didn't change, we only need to traverse dirty VarInfos + ts' <- if tyStateRefined old_ty_st (nabla_ty_st nabla) + then traverseAll test_one ts + else traverseDirty test_one ts + pure nabla{ nabla_tm_st = ts'{ts_dirty=emptyDVarSet}} + where + nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} } + test_one :: VarInfo -> MaybeT DsM VarInfo + test_one vi = do + lift (varNeedsTesting old_ty_st nabla vi) >>= \case + True -> do + -- tracPm "test_one" (ppr vi) + -- No solution yet and needs testing + -- We have to test with a Nabla where all dirty bits are cleared + instantiate (fuel-1) nabla_not_dirty vi + _ -> pure vi + +-- | Checks whether the given 'VarInfo' needs to be tested for inhabitants. +-- +-- 1. If it already has a solution, we don't have to test. +-- 2. If it's marked dirty because of new negative term constraints, we have +-- to test. +-- 3. Otherwise, if the type state didn't change, we don't need to test. +-- 4. If the type state changed, we compare normalised source types. No need +-- to test if unchanged. +varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool +varNeedsTesting _ _ vi + | notNull (vi_pos vi) = pure False +varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} vi + | elemDVarSet (vi_id vi) (ts_dirty tm_st) = pure True +varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _ + -- Same type state => still inhabited + | not (tyStateRefined old_ty_st new_ty_st) = pure False +varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do + -- These normalisations are relatively expensive, but still better than having + -- to perform a full inhabitation test + (_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (idType $ vi_id vi) + (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi) + if old_norm_ty `eqType` new_norm_ty + then pure False + else pure True + +-- | 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_rcm. +-- +-- 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. +instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo +instantiate fuel nabla vi = instBot fuel nabla vi <|> instCompleteSets fuel nabla vi + +-- | The \(⊢_{Bot}\) rule from the paper +instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo +instBot _fuel nabla vi = do + _nabla' <- addBotCt nabla (vi_id vi) + pure vi + +addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla) +addNormalisedTypeMatches nabla@MkNabla{ nabla_ty_st = ty_st } x + = trvVarInfo add_matches nabla x + where + add_matches vi@VI{ vi_rcm = rcm } + -- important common case, shaving down allocations of PmSeriesG by -5% + | isRcmInitialised rcm = pure (rcm, vi) + add_matches vi@VI{ vi_rcm = rcm } = do + norm_res_ty <- normaliseSourceTypeWHNF ty_st (idType x) + env <- dsGetFamInstEnvs + rcm' <- case splitReprTyConApp_maybe env norm_res_ty of + Just (rep_tc, _args, _co) -> addTyConMatches rep_tc rcm + Nothing -> addCompleteMatches rcm + pure (rcm', vi{ vi_rcm = rcm' }) + +-- | Does a 'splitTyConApp_maybe' and then tries to look through a data family +-- application to find the representation TyCon, to which the data constructors +-- are attached. Returns the representation TyCon, the TyCon application args +-- and a representational coercion that will be Refl for non-data family apps. +splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion) +splitReprTyConApp_maybe env ty = + uncurry (tcLookupDataFamInst env) <$> splitTyConApp_maybe ty + +-- | 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. It returns the updated 'VarInfo' +-- where all the attempted ConLike instantiations have been purged from the +-- 'ResidualCompleteMatches', which functions as a cache. +instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo +instCompleteSets fuel nabla vi = do + let x = vi_id vi + (rcm, nabla) <- lift (addNormalisedTypeMatches nabla x) + nabla <- foldM (\nabla cls -> instCompleteSet fuel nabla x cls) nabla (getRcm rcm) + pure (lookupVarInfo (nabla_tm_st nabla) x) + +anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool +anyConLikeSolution p = any (go . paca_con) + where + go (PmAltConLike cl) = p cl + go _ = False + +-- | @instCompleteSet fuel nabla nabla cls@ iterates over @cls@ until it finds +-- the first inhabited ConLike (as per 'instCon'). Any failed instantiation +-- attempts of a ConLike are recorded as negative information in the returned +-- 'Nabla', so that later calls to this function can skip repeatedly fruitless +-- instantiation of that same constructor. +-- +-- Note that the returned Nabla is just a different representation of the +-- original Nabla, not a proper refinement! No positive information will be +-- added, only negative information from failed instantiation attempts, +-- entirely as an optimisation. +instCompleteSet :: Int -> Nabla -> Id -> ConLikeSet -> MaybeT DsM Nabla +instCompleteSet fuel nabla x cs + | anyConLikeSolution (`elementOfUniqDSet` cs) (vi_pos vi) + -- No need to instantiate a constructor of this COMPLETE set if we already + -- have a solution! + = pure nabla + | otherwise + = go nabla (sorted_candidates cs) + where + vi = lookupVarInfo (nabla_tm_st nabla) x + + sorted_candidates :: ConLikeSet -> [ConLike] + sorted_candidates cs + -- If there aren't many candidates, we can try to sort them by number of + -- strict fields, type constraints, etc., so that we are fast in the + -- common case + -- (either many simple constructors *or* few "complicated" ones). + | sizeUniqDSet cs <= 5 = sortBy compareConLikeTestability (uniqDSetToList cs) + | otherwise = uniqDSetToList cs + + go :: Nabla -> [ConLike] -> MaybeT DsM Nabla + go _ [] = mzero + go nabla (RealDataCon dc:_) + -- See Note [DataCons that are definitely inhabitable] + -- Recall that dc can't be in vi_neg, because then it would be + -- deleted from the residual COMPLETE set. + | isDataConTriviallyInhabited dc + = pure nabla + go nabla (con:cons) = do + let x = vi_id vi + let recur_not_con = do + nabla' <- addNotConCt nabla x (PmAltConLike con) + go nabla' cons + (nabla <$ instCon fuel nabla x con) -- return the original nabla, not the + -- refined one! + <|> recur_not_con -- Assume that x can't be con. Encode that fact + -- with addNotConCt and recur. + +-- | Is this 'DataCon' trivially inhabited, that is, without needing to perform +-- any inhabitation testing because of strict/unlifted fields or type +-- equalities? See Note [DataCons that are definitely inhabitable] +isDataConTriviallyInhabited :: DataCon -> Bool +isDataConTriviallyInhabited dc + | isTyConTriviallyInhabited (dataConTyCon dc) = True +isDataConTriviallyInhabited dc = + null (dataConTheta dc) && -- (1) + null (dataConImplBangs dc) && -- (2) + null (dataConUnliftedFieldTys dc) -- (3) + +dataConUnliftedFieldTys :: DataCon -> [Type] +dataConUnliftedFieldTys = + -- A levity polymorphic field requires an inhabitation test, hence compare to + -- @Just True@ + filter ((== Just True) . isLiftedType_maybe) . map scaledThing . dataConOrigArgTys + +isTyConTriviallyInhabited :: TyCon -> Bool +isTyConTriviallyInhabited tc = elementOfUniqSet tc triviallyInhabitedTyCons + +-- | All these types are trivially inhabited +triviallyInhabitedTyCons :: UniqSet TyCon +triviallyInhabitedTyCons = mkUniqSet [ + charTyCon, doubleTyCon, floatTyCon, intTyCon, wordTyCon, word8TyCon + ] + +compareConLikeTestability :: ConLike -> ConLike -> Ordering +-- We should instantiate DataCons first, because they are likely to occur in +-- multiple COMPLETE sets at once and we might find that multiple COMPLETE sets +-- are inhabitated by instantiating only a single DataCon. +compareConLikeTestability PatSynCon{} _ = GT +compareConLikeTestability _ PatSynCon{} = GT +compareConLikeTestability (RealDataCon a) (RealDataCon b) = mconcat + -- Thetas are most expensive to check, as they might incur a whole new round + -- of inhabitation testing + [ comparing (fast_length . dataConTheta) + -- Unlifted or strict fields only incur an inhabitation test for that + -- particular field. Still something to avoid. + , comparing unlifted_or_strict_fields + ] a b + where + fast_length :: [a] -> Int + fast_length xs = atLength length 6 xs 5 -- @min 6 (length xs)@, but O(1) + + -- An upper bound on the number of strict or unlifted fields. Approximate in + -- the unlikely bogus case of an unlifted field that has a bang. + unlifted_or_strict_fields :: DataCon -> Int + unlifted_or_strict_fields dc = fast_length (dataConImplBangs dc) + + fast_length (dataConUnliftedFieldTys dc) + +-- | @instCon fuel nabla (x::res_ty) K@ tries to instantiate @x@ to @K@. +-- This is the \(Inst\) function from Figure 8 of the LYG paper. +-- +-- As a first step, it tries to guess the universal type arguments of @K@ from +-- the @res_ty@ and @K@'s result type, so that we have +-- +-- K @arg_tys :: forall es. Q => t1 -> ... -> tn -> res_ty +-- +-- See 'guessConLikeUnivTyArgsFromResTy' for when it might fail to guess (only +-- for certain pattern synonyms). +-- If the function /fails/ to guess, 'instCon' trivially succeeds, because it +-- can't be sure if @x@ could be instantiated to @K@ and has to be +-- conservative). +-- If the function /succeeds/ in guessing @arg_tys@, it does the necessary +-- substitution and instantiation dance for @K@'s field types, which may still +-- reference existential type variables of @K@. So it performs the following steps: +-- +-- * It accumulates a substitution mapping @K@'s universal type variables, +-- which are substituted for @arg_tys@. +-- * It instantiates fresh binders for the other type variables @es@ bound by +-- @K@ and adds it to the substitution, so that we have +-- @K \@arg_tys \@ex_tvs :: Q => t1' -> ... -> tn' -> res_ty@ +-- * It substitutes the 'ThetaType' @Q@ for type constraints @gammas@ to add +-- * It substitutes and conjures new binders @arg_ids@ for the argument types +-- @t1' ... tn'@. +-- +-- Finally, it adds a 'PhiConCt' constructor constraint +-- @K ex_tvs gammas arg_ids <- x@ which handles the details regarding type +-- constraints and unlifted fields. +instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla +instCon fuel nabla@MkNabla{nabla_ty_st = ty_st} x con = MaybeT $ do + env <- dsGetFamInstEnvs + let res_ty = idType x + norm_res_ty <- normaliseSourceTypeWHNF ty_st res_ty + let mb_arg_tys = guessConLikeUnivTyArgsFromResTy env norm_res_ty con + case mb_arg_tys of + Just arg_tys -> do + let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta, field_tys, _con_res_ty) + = conLikeFullSig con + -- (1) Substitute universals for type arguments + let subst_univ = zipTvSubst univ_tvs arg_tys + -- (2) Instantiate fresh existentials as arguments to the constructor. + -- This is important for instantiating the Thetas and field types. + (subst, _) <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM + let field_tys' = substTys subst $ map scaledThing field_tys + -- (3) All constraints bound by the constructor (alpha-renamed), these are added + -- to the type oracle + let gammas = substTheta subst (eqSpecPreds eq_spec ++ thetas) + -- (4) Instantiate fresh term variables as arguments to the constructor + arg_ids <- mapM mkPmId field_tys' + tracePm "instCon" $ vcat + [ ppr x <+> dcolon <+> ppr res_ty + , text "In WHNF:" <+> ppr (isSourceTypeInWHNF res_ty) <+> ppr norm_res_ty + , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty + , ppr (zipWith (\tv ty -> ppr tv <+> char '↦' <+> ppr ty) univ_tvs arg_tys) + , ppr gammas + , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids) + , ppr fuel + ] + -- Finally add the constraint + runMaybeT $ do + -- Case (2) of Note [Strict fields and variables of unlifted type] + let alt = PmAltConLike con + nabla' <- addPhiTmCt nabla (PhiConCt x alt ex_tvs gammas arg_ids) + let branching_factor = length $ filterUnliftedFields alt arg_ids + -- See Note [Fuel for the inhabitation test] + let new_fuel + | branching_factor <= 1 = fuel + | otherwise = min fuel 2 + inhabitationTest new_fuel (nabla_ty_st nabla) nabla' + Nothing -> pure (Just nabla) -- Could not guess arg_tys. Just assume inhabited + +-- | Guess the universal argument types of a ConLike from an instantiation of +-- its (normalised!) result type. So, given +-- +-- K :: forall us. forall es. Q => t1 -> ... -> tn -> con_res_ty +-- +-- It tries to guess @arg_tys@ by matching @norm_res_ty@ and @con_res_ty@, such that +-- +-- K @arg_tys :: forall es. Q' => t1' -> ... -> tn' -> norm_res_ty +-- +-- Rather easy for DataCons, but not so much for PatSynCons. See Note [Pattern +-- synonym result type] in "GHC.Core.PatSyn". +guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type] +guessConLikeUnivTyArgsFromResTy env norm_res_ty (RealDataCon dc) = do + -- splitReprTyConApp_maybe rather than splitTyConApp_maybe because of data families. + (rep_tc, tc_args, _co) <- splitReprTyConApp_maybe env norm_res_ty + if rep_tc == dataConTyCon dc + then Just tc_args + else Nothing +guessConLikeUnivTyArgsFromResTy _ norm_res_ty (PatSynCon ps) = do + -- We are successful if we managed to instantiate *every* univ_tv of con. + -- This is difficult and bound to fail in some cases, see + -- Note [Pattern synonym result type] in GHC.Core.PatSyn. So we just try our best + -- here and be sure to return an instantiation when we can substitute every + -- universally quantified type variable. + -- We *could* instantiate all the other univ_tvs just to fresh variables, I + -- suppose, but that means we get weird field types for which we don't know + -- anything. So we prefer to keep it simple here. + let (univ_tvs,_,_,_,_,con_res_ty) = patSynSig ps + subst <- tcMatchTy con_res_ty norm_res_ty + traverse (lookupTyVar subst) univ_tvs + +{- Note [Fuel for the inhabitation test] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Whether or not a type is inhabited is undecidable in general. As a result, we +can run into infinite loops in `inhabitationTest`. Therefore, we adopt a +fuel-based approach to prevent that. + +Consider the following example: + + data Abyss = MkAbyss !Abyss + stareIntoTheAbyss :: Abyss -> a + stareIntoTheAbyss x = case x of {} + +In principle, stareIntoTheAbyss is exhaustive, since there is no way to +construct a terminating value using MkAbyss. But this can't be proven by mere +instantiation and requires an inductive argument, which `inhabitationTest` +currently isn't equipped to do. + +In order to prevent endless instantiation attempts in @inhabitationTest@, we +use the fuel as an upper bound such attempts. + +The same problem occurs with recursive newtypes, like in the following code: + + newtype Chasm = MkChasm Chasm + gazeIntoTheChasm :: Chasm -> a + gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive + +So this limitation is somewhat understandable. + +Note that even with this recursion detection, there is still a possibility that +`inhabitationTest` can run in exponential time in the amount of fuel. Consider +the following data type: + + data T = MkT !T !T !T + +If we try to instantiate each of its fields, that will require us to once again +check if `MkT` is inhabitable in each of those three fields, which in turn will +require us to check if `MkT` is inhabitable again... As you can see, the +branching factor adds up quickly, and if the initial fuel is, say, +100, then the inhabiation test will effectively take forever. + +To mitigate this, we check the branching factor every time we are about to do +inhabitation testing in 'instCon'. If the branching factor exceeds 1 +(i.e., if there is potential for exponential runtime), then we limit the +maximum recursion depth to 1 to mitigate the problem. If the branching factor +is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay +to stick with a larger maximum recursion depth. + +In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was +too large and had detrimental effect on performance of the coverage checker. +Given that we only commit to a best effort anyway, we decided to substantially +decrement the fuel to 4, at the cost of precision in some edge cases +like + + data Nat = Z | S Nat + data Down :: Nat -> Type where + Down :: !(Down n) -> Down (S n) + f :: Down (S (S (S (S (S Z))))) -> () + f x = case x of {} + +Since the coverage won't bother to instantiate Down 4 levels deep to see that it +is in fact uninhabited, it will emit a inexhaustivity warning for the case. + +Note [DataCons that are definitely inhabitable] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Another microoptimization applies to data types like this one: + + data S a = S ![a] !T + +Even though there is a strict field of type [a], it's quite silly to call +'instCon' on it, since it's "obvious" that it is inhabitable. To make this +intuition formal, we say that a DataCon C is definitely inhabitable (DI) if: + + 1. C has no equality constraints (since they might be unsatisfiable) + 2. C has no strict arguments (since they might be uninhabitable) + 3. C has no unlifted argument types (since they might be uninhabitable) + +It's relatively cheap to check if a DataCon is DI, so before we call 'instCon' +on a constructor of a COMPLETE set, we filter out all of the DI ones. + +This fast path shaves down -7% allocations for PmSeriesG, for example. +-} + +-------------------------------------- +-- * Generating inhabitants of a Nabla +-- +-- This is important for warnings. Roughly corresponds to G in Figure 6 of the +-- LYG paper, with a few tweaks for better warning messages. + +-- | @generateInhabitingPatterns vs n nabla@ returns a list of at most @n@ (but +-- perhaps empty) refinements of @nabla@ that represent inhabited patterns. +-- Negative information is only retained if literals are involved or for +-- recursive GADTs. +generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla] +-- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns] +generateInhabitingPatterns _ 0 _ = pure [] +generateInhabitingPatterns [] _ nabla = pure [nabla] +generateInhabitingPatterns (x:xs) n nabla = do + tracePm "generateInhabitingPatterns" (ppr n <+> ppr (x:xs) $$ ppr nabla) + 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 + -- fields. Example: + -- f x@(Just _) True = case x of SomePatSyn _ -> () + -- after this clause, we want to report that + -- * @f Nothing _@ is uncovered + -- * @f x False@ is uncovered + -- where @x@ will have two possibly compatible solutions, @Just y@ for + -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@ + -- and @z@ that is valid at the same time. These constitute arg_vas below. + let arg_vas = concatMap paca_ids pos + generateInhabitingPatterns (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 ] + -> generateInhabitingPatterns xs n nabla + [] -> try_instantiate x xs n nabla + where + -- | 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 -> Nabla -> DsM [Nabla] + -- Convention: x binds the outer constructor in the chain, y the inner one. + try_instantiate x xs n nabla = do + (_src_ty, dcs, rep_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (idType x) + mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs + case mb_stuff of + Nothing -> pure [] + Just (y, newty_nabla) -> do + let vi = lookupVarInfo (nabla_tm_st newty_nabla) y + env <- dsGetFamInstEnvs + rcm <- case splitReprTyConApp_maybe env rep_ty of + Just (tc, _, _) -> addTyConMatches tc (vi_rcm vi) + Nothing -> addCompleteMatches (vi_rcm vi) + + -- Test all COMPLETE sets for inhabitants (n inhs at max). Take care of ⊥. + clss <- pickApplicableCompleteSets rep_ty rcm + case NE.nonEmpty (uniqDSetToList <$> clss) of + Nothing -> + -- No COMPLETE sets ==> inhabited + generateInhabitingPatterns xs n newty_nabla + Just clss -> do + -- Try each COMPLETE set, pick the one with the smallest number of + -- inhabitants + nablass' <- forM clss (instantiate_cons y rep_ty xs n newty_nabla) + let nablas' = minimumBy (comparing length) nablass' + if null nablas' && vi_bot vi /= IsNotBot + then generateInhabitingPatterns xs n newty_nabla -- bot is still possible. Display a wildcard! + else pure nablas' + + -- | Instantiates a chain of newtypes, beginning at @x@. + -- Turns @x nabla [T,U,V]@ to @(y, nabla')@, where @nabla'@ we has the fact + -- @x ~ T (U (V y))@. + instantiate_newtype_chain :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Nabla) + instantiate_newtype_chain x nabla [] = pure (x, nabla) + instantiate_newtype_chain x nabla ((_ty, dc, arg_ty):dcs) = do + y <- lift $ mkPmId arg_ty + -- Newtypes don't have existentials (yet?!), so passing an empty + -- list as ex_tvs. + nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y] + instantiate_newtype_chain y nabla' dcs + + instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla] + instantiate_cons _ _ _ _ _ [] = pure [] + instantiate_cons _ _ _ 0 _ _ = pure [] + 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 + = generateInhabitingPatterns xs n nabla + instantiate_cons x ty xs n nabla (cl:cls) = do + -- The following line is where we call out to the inhabitationTest! + mb_nabla <- runMaybeT $ instCon 4 nabla x cl + tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (idType x) + , ppr ty + , ppr cl + , ppr nabla + , ppr mb_nabla + , ppr n ]) + 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 the inhabitation test would have refuted. + Just nabla' -> generateInhabitingPatterns xs n nabla' + other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls + pure (con_nablas ++ other_cons_nablas) + +pickApplicableCompleteSets :: Type -> ResidualCompleteMatches -> DsM [ConLikeSet] +pickApplicableCompleteSets ty rcm = do + env <- dsGetFamInstEnvs + pure $ filter (all (is_valid env) . uniqDSetToList) (getRcm rcm) + where + is_valid :: FamInstEnvs -> ConLike -> Bool + is_valid env cl = isJust (guessConLikeUnivTyArgsFromResTy env ty cl) + +{- Note [Why inhabitationTest doesn't call generateInhabitingPatterns] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Why can't we define `inhabitationTest` (IT) in terms of +`generateInhabitingPatterns` (GIP) as + + inhabitationTest nabla = do + nablas <- lift $ generateInhabitingPatterns all_variables 1 nabla + guard (notNull nablas) + +There are a few technical reasons, like the lack of a fuel-tracking approach +to stay decidable, that could be overcome. But the nail in the coffin is +performance: In order to provide good warning messages, GIP commits to *one* +COMPLETE set, and goes through some hoops to find the minimal one. This implies +it has to look at *all* constructors in the residual COMPLETE matches and see if +they match, if only to filter out ill-typed COMPLETE sets +(see Note [Implementation of COMPLETE pragmas]). That is untractable for an +efficient IT on huge enumerations. + +But we still need GIP to produce the Nablas as proxies for +uncovered patterns that we display warnings for. It's fine to pay this price +once at the end, but IT is called far more often than that. -} diff --git a/compiler/GHC/HsToCore/PmCheck/Ppr.hs b/compiler/GHC/HsToCore/PmCheck/Ppr.hs index 557fd08c43..94ea9d6361 100644 --- a/compiler/GHC/HsToCore/PmCheck/Ppr.hs +++ b/compiler/GHC/HsToCore/PmCheck/Ppr.hs @@ -146,8 +146,8 @@ pprPmVar :: PprPrec -> Id -> PmPprM SDoc pprPmVar prec x = do nabla <- ask case lookupSolution nabla x of - Just (alt, _tvs, args) -> pprPmAltCon prec alt args - Nothing -> fromMaybe typed_wildcard <$> checkRefuts x + Just (PACA alt _tvs args) -> pprPmAltCon prec alt args + Nothing -> fromMaybe typed_wildcard <$> checkRefuts x where -- if we have no info about the parameter and would just print a -- wildcard, also show its type. @@ -206,7 +206,7 @@ pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList pmExprAsList nabla = go_con [] where go_var rev_pref x - | Just (alt, _tvs, args) <- lookupSolution nabla x + | Just (PACA alt _tvs args) <- lookupSolution nabla x = go_con rev_pref alt args go_var rev_pref x | Just pref <- nonEmpty (reverse rev_pref) diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs index 4602b89611..3577a8d8ad 100644 --- a/compiler/GHC/HsToCore/PmCheck/Types.hs +++ b/compiler/GHC/HsToCore/PmCheck/Types.hs @@ -25,7 +25,7 @@ module GHC.HsToCore.PmCheck.Types ( pmLitAsStringLit, coreExprAsPmLit, -- * Caching residual COMPLETE sets - ConLikeSet, ResidualCompleteMatches(..), getRcm, + ConLikeSet, ResidualCompleteMatches(..), getRcm, isRcmInitialised, -- * PmAltConSet PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet, @@ -33,11 +33,11 @@ module GHC.HsToCore.PmCheck.Types ( -- * A 'DIdEnv' where entries may be shared Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE, - setIndirectSDIE, setEntrySDIE, traverseSDIE, + setIndirectSDIE, setEntrySDIE, traverseSDIE, entriesSDIE, -- * The pattern match oracle - BotInfo(..), VarInfo(..), TmState(..), TyState(..), Nabla(..), - Nablas(..), initNablas, liftNablasM + BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..), + Nabla(..), Nablas(..), initNablas, liftNablasM ) where #include "HsVersions.h" @@ -49,6 +49,7 @@ import GHC.Data.Bag import GHC.Data.FastString import GHC.Types.Id import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Types.Unique.DSet import GHC.Types.Unique.DFM import GHC.Types.Name @@ -437,6 +438,9 @@ data ResidualCompleteMatches getRcm :: ResidualCompleteMatches -> [ConLikeSet] getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas +isRcmInitialised :: ResidualCompleteMatches -> Bool +isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas + instance Outputable ResidualCompleteMatches where -- formats as "[{Nothing,Just},{P,Q}]" ppr rcm = ppr (getRcm rcm) @@ -485,6 +489,12 @@ setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a setEntrySDIE sdie@(SDIE env) x a = SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a) +entriesSDIE :: SharedDIdEnv a -> [a] +entriesSDIE (SDIE env) = mapMaybe preview_entry (eltsUDFM env) + where + preview_entry (Entry e) = Just e + preview_entry _ = Nothing + traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b) traverseSDIE f = fmap (SDIE . listToUDFM_Directly) . traverse g . udfmToList . unSDIE where @@ -501,13 +511,6 @@ 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. @@ -522,6 +525,9 @@ data TmState -- ^ An environment for looking up whether we already encountered semantically -- equivalent expressions that we want to represent by the same 'Id' -- representative. + , ts_dirty :: !DIdSet + -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new + -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@). } -- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@, @@ -532,11 +538,11 @@ data TmState -- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.PmCheck.Oracle". data VarInfo = VI - { vi_ty :: !Type - -- ^ The type of the variable. Important for rejecting possible GADT - -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@). + { vi_id :: !Id + -- ^ The 'Id' in question. Important for adding new constraints relative to + -- this 'VarInfo' when we don't easily have the 'Id' available. - , vi_pos :: ![(PmAltCon, [TyVar], [Id])] + , vi_pos :: ![PmAltConApp] -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all -- at the same time (i.e. conjunctive). We need a list because of nested -- pattern matches involving pattern synonym @@ -576,40 +582,76 @@ data VarInfo -- to recognise completion of a COMPLETE set efficiently for large enums. } +data PmAltConApp + = PACA + { paca_con :: !PmAltCon + , paca_tvs :: ![TyVar] + , paca_ids :: ![Id] + } + +-- | See 'vi_bot'. +data BotInfo + = IsBot + | IsNotBot + | MaybeBot + deriving Eq + +instance Outputable PmAltConApp where + ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} = + hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids) + instance Outputable BotInfo where - ppr MaybeBot = empty + ppr MaybeBot = underscore ppr IsBot = text "~⊥" ppr IsNotBot = text "≁⊥" -- | Not user-facing. instance Outputable TmState where - ppr (TmSt state reps) = ppr state $$ ppr reps + ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty -- | Not user-facing. instance Outputable VarInfo where - ppr (VI ty pos neg bot cache) - = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr bot, ppr cache])) + ppr (VI x pos neg bot cache) + = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache])) + where + pp_x = ppr x <> dcolon <> ppr (idType x) + pp_pos + | [] <- pos = underscore + | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton + | otherwise = char '~' <> ppr pos + pp_neg + | isEmptyPmAltConSet neg = underscore + | otherwise = char '≁' <> ppr neg + pp_cache + | RCM Nothing Nothing <- cache = underscore + | otherwise = ppr cache -- | Initial state of the term oracle. initTmState :: TmState -initTmState = TmSt emptySDIE emptyCoreMap +initTmState = TmSt emptySDIE emptyCoreMap emptyDVarSet --- | The type oracle state. A poor man's 'GHC.Tc.Solver.Monad.InsertSet': The invariant is --- that all constraints in there are mutually compatible. -newtype TyState = TySt InertSet +-- | The type oracle state. An 'GHC.Tc.Solver.Monad.InsertSet' that we +-- incrementally add local type constraints to, together with a sequence +-- number that counts the number of times we extended it with new facts. +data TyState = TySt { ty_st_n :: !Int, ty_st_inert :: !InertSet } -- | Not user-facing. instance Outputable TyState where - ppr (TySt inert) = ppr inert + ppr (TySt n inert) = ppr n <+> ppr inert initTyState :: TyState -initTyState = TySt emptyInert +initTyState = TySt 0 emptyInert -- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of -- canonical (i.e. mutually compatible) term and type constraints that form the -- refinement type's predicate. -data Nabla = MkNabla { nabla_ty_st :: TyState -- Type oracle; things like a~Int - , nabla_tm_st :: TmState } -- Term oracle; things like x~Nothing +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 nabla that is always satisfiable initNabla :: Nabla diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs-boot b/compiler/GHC/HsToCore/PmCheck/Types.hs-boot deleted file mode 100644 index a0505bce9d..0000000000 --- a/compiler/GHC/HsToCore/PmCheck/Types.hs-boot +++ /dev/null @@ -1,9 +0,0 @@ -module GHC.HsToCore.PmCheck.Types where - -import GHC.Data.Bag - -data Nabla - -newtype Nablas = MkNablas (Bag Nabla) - -initNablas :: Nablas diff --git a/compiler/GHC/HsToCore/Types.hs b/compiler/GHC/HsToCore/Types.hs index b99970f55f..d6fd94e723 100644 --- a/compiler/GHC/HsToCore/Types.hs +++ b/compiler/GHC/HsToCore/Types.hs @@ -14,7 +14,7 @@ import GHC.Types.SrcLoc import GHC.Types.Var import GHC.Hs (LForeignDecl, HsExpr, GhcTc) import GHC.Tc.Types (TcRnIf, IfGblEnv, IfLclEnv, CompleteMatches) -import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Nablas) +import GHC.HsToCore.PmCheck.Types (Nablas) import GHC.Core (CoreExpr) import GHC.Core.FamInstEnv import GHC.Utils.Error diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 81b0c6792b..9870c36ff5 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -1229,7 +1229,9 @@ instance OutputableBndrId id => Outputable (HsExprArg id) where ppr (HsEPar _) = text "HsEPar" ppr (HsEWrap w) = case ghcPass @id of GhcTc -> text "HsEWrap" <+> ppr w +#if __GLASGOW_HASKELL__ <= 900 _ -> empty +#endif type family XExprTypeArg id where XExprTypeArg 'Parsed = NoExtField diff --git a/testsuite/tests/pmcheck/should_compile/T18249.hs b/testsuite/tests/pmcheck/should_compile/T18249.hs new file mode 100644 index 0000000000..b9bd048cbd --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T18249.hs @@ -0,0 +1,36 @@ +{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +module T18249 where + +import GHC.Exts + +f :: Int# -> Int +-- redundant, not just inaccessible! +f !_ | False = 1 +f _ = 2 + +newtype UVoid :: TYPE 'UnliftedRep where + UVoid :: UVoid -> UVoid + +g :: UVoid -> Int +-- redundant in a weird way: +-- there's no way to actually write this function. +-- Inhabitation testing currently doesn't find that UVoid is empty, +-- but we should be able to detect the bang as redundant. +g !_ = 1 + +h :: (# (), () #) -> Int +-- redundant, not just inaccessible! +h (# _, _ #) | False = 1 +h _ = 2 + +i :: Int -> Int +i !_ | False = 1 +i (I# !_) | False = 2 +i _ = 3 + diff --git a/testsuite/tests/pmcheck/should_compile/T18249.stderr b/testsuite/tests/pmcheck/should_compile/T18249.stderr new file mode 100644 index 0000000000..b13160e183 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T18249.stderr @@ -0,0 +1,20 @@ + +T18249.hs:14:8: warning: [-Woverlapping-patterns (in -Wdefault)] + Pattern match is redundant + In an equation for ‘f’: f !_ | False = ... + +T18249.hs:25:4: warning: [-Wredundant-bang-patterns] + Pattern match has redundant bang + In an equation for ‘g’: g _ = ... + +T18249.hs:29:16: warning: [-Woverlapping-patterns (in -Wdefault)] + Pattern match is redundant + In an equation for ‘h’: h (# _, _ #) | False = ... + +T18249.hs:33:13: warning: [-Woverlapping-patterns (in -Wdefault)] + Pattern match has inaccessible right hand side + In an equation for ‘i’: i !_ | False = ... + +T18249.hs:34:13: warning: [-Woverlapping-patterns (in -Wdefault)] + Pattern match is redundant + In an equation for ‘i’: i (I# !_) | False = ... diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T index c2f14ce664..bd5fc60f63 100644 --- a/testsuite/tests/pmcheck/should_compile/all.T +++ b/testsuite/tests/pmcheck/should_compile/all.T @@ -134,6 +134,8 @@ 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('T18249', normal, compile, + ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns -Wredundant-bang-patterns']) test('T18273', normal, compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns']) test('T18341', normal, compile, |