diff options
Diffstat (limited to 'compiler')
| -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 |
8 files changed, 1152 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 |