{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} {- Authors: George Karachalias <george.karachalias@cs.kuleuven.be> Sebastian Graf <sgraf1337@gmail.com> Ryan Scott <ryan.gl.scott@gmail.com> -} -- | Model refinements type as per the -- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989). -- The main export of the module are the functions 'addPhiCtsNablas' for adding -- facts to the oracle, 'isInhabited' to check if a refinement type is inhabited -- and 'generateInhabitingPatterns' to turn a 'Nabla' into a concrete pattern -- for an equation. -- -- In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6 -- and 3.7. E.g., it represents refinement types directly as a bunch of -- normalised refinement types 'Nabla'. module GHC.HsToCore.Pmc.Solver ( Nabla, Nablas(..), initNablas, PhiCt(..), PhiCts, addPhiCtNablas, addPhiCtsNablas, isInhabited, generateInhabitingPatterns, GenerateInhabitingPatternsMode(..) ) where import GHC.Prelude import GHC.HsToCore.Pmc.Types import GHC.HsToCore.Pmc.Utils (tracePm, traceWhenFailPm, mkPmId) import GHC.HsToCore.Types (DsGblEnv(..)) import GHC.Driver.DynFlags import GHC.Driver.Config import GHC.Utils.Outputable import GHC.Utils.Misc import GHC.Utils.Monad (allM) import GHC.Utils.Panic import GHC.Data.Bag import GHC.Types.CompleteMatch import GHC.Types.Unique.Set import GHC.Types.Unique.DSet import GHC.Types.Unique.SDFM import GHC.Types.Id import GHC.Types.Name import GHC.Types.Name.Reader (lookupGRE_Name, GlobalRdrEnv) import GHC.Types.Var (EvVar) import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Types.Unique.Supply import GHC.Tc.Utils.Monad (getGblEnv) import GHC.Core import GHC.Core.FVs (exprFreeVars) import GHC.Core.TyCo.Compare( eqType ) import GHC.Core.Map.Expr import GHC.Core.Predicate (typeDeterminesValue) import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe) import GHC.Core.Utils (exprType) import GHC.Core.Make (mkListExpr, mkCharExpr, mkImpossibleExpr) import GHC.Data.FastString import GHC.Types.SrcLoc import GHC.Data.Maybe import GHC.Core.ConLike import GHC.Core.DataCon import GHC.Core.PatSyn import GHC.Core.TyCon import GHC.Core.TyCon.RecWalk import GHC.Builtin.Names import GHC.Builtin.Types import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Subst (elemSubst) import GHC.Core.Type import GHC.Tc.Solver (tcNormalise, tcCheckGivens, tcCheckWanteds) import GHC.Core.Unify (tcMatchTy) import GHC.Core.Coercion import GHC.Core.Reduction import GHC.HsToCore.Monad hiding (foldlM) import GHC.Tc.Instance.Family import GHC.Core.FamInstEnv import Control.Applicative ((<|>)) import Control.Monad (foldM, forM, guard, mzero, when, filterM) import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.State.Strict import Data.Coerce import Data.Foldable (foldlM, minimumBy, toList) import Data.Monoid (Any(..)) import Data.List (sortBy, find) import qualified Data.List.NonEmpty as NE import Data.Ord (comparing) -- -- * Main exports -- -- | Add a bunch of 'PhiCt's to all the 'Nabla's. -- Lifts 'addPhiCts' over many 'Nablas'. addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas addPhiCtsNablas Nablas nablas PhiCts cts = (Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)) -> Nablas -> DsM Nablas forall (m :: * -> *). Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas liftNablasM (\Nabla d -> Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) addPhiCts Nabla d PhiCts cts) Nablas nablas -- | 'addPmCtsNablas' for a single 'PmCt'. addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas addPhiCtNablas Nablas nablas PhiCt ct = Nablas -> PhiCts -> DsM Nablas addPhiCtsNablas Nablas nablas (PhiCt -> PhiCts forall a. a -> Bag a unitBag PhiCt ct) liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas liftNablasM :: forall (m :: * -> *). Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas liftNablasM Nabla -> m (Maybe Nabla) f (MkNablas Bag Nabla ds) = Bag Nabla -> Nablas MkNablas (Bag Nabla -> Nablas) -> (Bag (Maybe Nabla) -> Bag Nabla) -> Bag (Maybe Nabla) -> Nablas forall b c a. (b -> c) -> (a -> b) -> a -> c . Bag (Maybe Nabla) -> Bag Nabla forall a. Bag (Maybe a) -> Bag a catBagMaybes (Bag (Maybe Nabla) -> Nablas) -> m (Bag (Maybe Nabla)) -> m Nablas forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> ((Nabla -> m (Maybe Nabla)) -> Bag Nabla -> m (Bag (Maybe Nabla)) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> Bag a -> f (Bag b) traverse Nabla -> m (Maybe Nabla) f Bag Nabla ds) -- | 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 <$> generateInhabitingPatterns 1 ds@. isInhabited :: Nablas -> DsM Bool isInhabited :: Nablas -> DsM Bool isInhabited (MkNablas Bag Nabla ds) = Bool -> DsM Bool forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Bool -> Bool not (Bag Nabla -> Bool forall a. Bag a -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null Bag Nabla ds)) ----------------------------------------------- -- * Caching residual COMPLETE sets -- See Note [Implementation of COMPLETE pragmas] -- | Update the COMPLETE sets of 'ResidualCompleteMatches', or 'Nothing' -- if there was no change as per the update function. updRcm :: (DsCompleteMatch -> (Bool, DsCompleteMatch)) -> ResidualCompleteMatches -> (Maybe ResidualCompleteMatches) updRcm :: (DsCompleteMatch -> (Bool, DsCompleteMatch)) -> ResidualCompleteMatches -> Maybe ResidualCompleteMatches updRcm DsCompleteMatch -> (Bool, DsCompleteMatch) f (RCM Maybe DsCompleteMatch vanilla Maybe [DsCompleteMatch] pragmas) | Bool -> Bool not Bool any_change = Maybe ResidualCompleteMatches forall a. Maybe a Nothing | Bool otherwise = ResidualCompleteMatches -> Maybe ResidualCompleteMatches forall a. a -> Maybe a Just (Maybe DsCompleteMatch -> Maybe [DsCompleteMatch] -> ResidualCompleteMatches RCM Maybe DsCompleteMatch vanilla' Maybe [DsCompleteMatch] pragmas') where f' :: DsCompleteMatch -> (Any, DsCompleteMatch) f' :: DsCompleteMatch -> (Any, DsCompleteMatch) f' = (DsCompleteMatch -> (Bool, DsCompleteMatch)) -> DsCompleteMatch -> (Any, DsCompleteMatch) forall a b. Coercible a b => a -> b coerce DsCompleteMatch -> (Bool, DsCompleteMatch) f (Any chgd, Maybe DsCompleteMatch vanilla') = (DsCompleteMatch -> (Any, DsCompleteMatch)) -> Maybe DsCompleteMatch -> (Any, Maybe DsCompleteMatch) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> Maybe a -> f (Maybe b) traverse DsCompleteMatch -> (Any, DsCompleteMatch) f' Maybe DsCompleteMatch vanilla (Any chgds, Maybe [DsCompleteMatch] pragmas') = ([DsCompleteMatch] -> (Any, [DsCompleteMatch])) -> Maybe [DsCompleteMatch] -> (Any, Maybe [DsCompleteMatch]) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> Maybe a -> f (Maybe b) traverse ((DsCompleteMatch -> (Any, DsCompleteMatch)) -> [DsCompleteMatch] -> (Any, [DsCompleteMatch]) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> [a] -> f [b] traverse DsCompleteMatch -> (Any, DsCompleteMatch) f') Maybe [DsCompleteMatch] pragmas any_change :: Bool any_change = Any -> Bool getAny (Any -> Bool) -> Any -> Bool forall a b. (a -> b) -> a -> b $ Any chgd Any -> Any -> Any forall a. Monoid a => a -> a -> a `mappend` Any chgds -- | A pseudo-'CompleteMatch' for the vanilla complete set of the given data -- 'TyCon'. -- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@ vanillaCompleteMatchTC :: TyCon -> Maybe DsCompleteMatch vanillaCompleteMatchTC :: TyCon -> Maybe DsCompleteMatch vanillaCompleteMatchTC TyCon tc = let mb_dcs :: Maybe [DataCon] mb_dcs | -- TYPE acts like an empty data type on the term level (#14086), -- but it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. -- Hence a special case. TyCon tc TyCon -> TyCon -> Bool forall a. Eq a => a -> a -> Bool == TyCon tYPETyCon = [DataCon] -> Maybe [DataCon] forall a. a -> Maybe a Just [] | -- Similarly, treat `type data` declarations as empty data types on -- the term level, as `type data` data constructors only exist at -- the type level (#22964). See wrinkle (W2a) in -- Note [Type data declarations] in GHC.Rename.Module. TyCon -> Bool isTypeDataTyCon TyCon tc = [DataCon] -> Maybe [DataCon] forall a. a -> Maybe a Just [] | Bool otherwise = TyCon -> Maybe [DataCon] tyConDataCons_maybe TyCon tc in UniqDSet ConLike -> DsCompleteMatch forall con. UniqDSet con -> CompleteMatchX con vanillaCompleteMatch (UniqDSet ConLike -> DsCompleteMatch) -> ([DataCon] -> UniqDSet ConLike) -> [DataCon] -> DsCompleteMatch forall b c a. (b -> c) -> (a -> b) -> a -> c . [ConLike] -> UniqDSet ConLike forall a. Uniquable a => [a] -> UniqDSet a mkUniqDSet ([ConLike] -> UniqDSet ConLike) -> ([DataCon] -> [ConLike]) -> [DataCon] -> UniqDSet ConLike forall b c a. (b -> c) -> (a -> b) -> a -> c . (DataCon -> ConLike) -> [DataCon] -> [ConLike] forall a b. (a -> b) -> [a] -> [b] map DataCon -> ConLike RealDataCon ([DataCon] -> DsCompleteMatch) -> Maybe [DataCon] -> Maybe DsCompleteMatch forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Maybe [DataCon] mb_dcs -- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas) -- if the given 'ResidualCompleteMatches' were empty. addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches addCompleteMatches (RCM Maybe DsCompleteMatch v Maybe [DsCompleteMatch] Nothing) = Maybe DsCompleteMatch -> Maybe [DsCompleteMatch] -> ResidualCompleteMatches RCM Maybe DsCompleteMatch v (Maybe [DsCompleteMatch] -> ResidualCompleteMatches) -> ([DsCompleteMatch] -> Maybe [DsCompleteMatch]) -> [DsCompleteMatch] -> ResidualCompleteMatches forall b c a. (b -> c) -> (a -> b) -> a -> c . [DsCompleteMatch] -> Maybe [DsCompleteMatch] forall a. a -> Maybe a Just ([DsCompleteMatch] -> ResidualCompleteMatches) -> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch] -> DsM ResidualCompleteMatches forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch] dsGetCompleteMatches addCompleteMatches ResidualCompleteMatches rcm = ResidualCompleteMatches -> DsM ResidualCompleteMatches forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure ResidualCompleteMatches rcm -- | Adds the declared 'CompleteMatches' from COMPLETE pragmas, as well as the -- vanilla data defn if it is a 'DataCon'. addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addConLikeMatches (RealDataCon DataCon dc) ResidualCompleteMatches rcm = TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addTyConMatches (DataCon -> TyCon dataConTyCon DataCon dc) ResidualCompleteMatches rcm addConLikeMatches (PatSynCon PatSyn _) ResidualCompleteMatches rcm = ResidualCompleteMatches -> DsM ResidualCompleteMatches addCompleteMatches ResidualCompleteMatches rcm -- | Adds -- * the 'CompleteMatches' from COMPLETE pragmas -- * and the /vanilla/ 'CompleteMatch' from the data 'TyCon' -- to the 'ResidualCompleteMatches', if not already present. addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addTyConMatches TyCon tc ResidualCompleteMatches rcm = ResidualCompleteMatches -> ResidualCompleteMatches add_tc_match (ResidualCompleteMatches -> ResidualCompleteMatches) -> DsM ResidualCompleteMatches -> DsM ResidualCompleteMatches forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> ResidualCompleteMatches -> DsM ResidualCompleteMatches addCompleteMatches ResidualCompleteMatches rcm where -- Add the vanilla COMPLETE set from the data defn, if any. But only if -- it's not already present. add_tc_match :: ResidualCompleteMatches -> ResidualCompleteMatches add_tc_match ResidualCompleteMatches rcm = ResidualCompleteMatches rcm{rcm_vanilla = rcm_vanilla rcm <|> vanillaCompleteMatchTC tc} markMatched :: PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches) -- Nothing means the PmAltCon didn't occur in any COMPLETE set. -- See Note [Shortcutting the inhabitation test] for how this is useful for -- performance on T17836. markMatched :: PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches) markMatched (PmAltLit PmLit _) ResidualCompleteMatches _ = Maybe ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe ResidualCompleteMatches forall a. Maybe a Nothing -- lits are never part of a COMPLETE set markMatched (PmAltConLike ConLike cl) ResidualCompleteMatches rcm = do rcm' <- ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addConLikeMatches ConLike cl ResidualCompleteMatches rcm let go DsCompleteMatch cm = case UniqDSet ConLike -> ConLike -> Maybe ConLike forall a. Uniquable a => UniqDSet a -> a -> Maybe a lookupUniqDSet (DsCompleteMatch -> UniqDSet ConLike forall con. CompleteMatchX con -> UniqDSet con cmConLikes DsCompleteMatch cm) ConLike cl of Maybe ConLike Nothing -> (Bool False, DsCompleteMatch cm) Just ConLike _ -> (Bool True, DsCompleteMatch cm { cmConLikes = delOneFromUniqDSet (cmConLikes cm) cl }) pure $ updRcm go rcm' {- Note [Implementation of COMPLETE pragmas] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A COMPLETE set represents a set of conlikes (i.e., constructors or pattern synonyms) such that if they are all pattern-matched against in a function, it gives rise to a total function. An example is: newtype Boolean = Boolean Int pattern F, T :: Boolean pattern F = Boolean 0 pattern T = Boolean 1 {-# COMPLETE F, T #-} -- This is a total function booleanToInt :: Boolean -> Int booleanToInt F = 0 booleanToInt T = 1 COMPLETE sets are represented internally in GHC as a set of 'ConLike's. For example, the pragma {-# COMPLETE F, T #-} would be represented as: CompleteMatch {F, T} Nothing What is the Maybe for? Answer: COMPLETE pragmas may optionally specify a result *type constructor* (cf. T14422): class C f where foo :: f a -> () pattern P :: C f => f a pattern P <- (foo -> ()) instance C State where foo _ = () {-# COMPLETE P :: State #-} f :: State a -> () f P = () g :: C f => f a -> () g P = () The @:: State@ here means that the types at which the COMPLETE pragma *applies* is restricted to scrutinee types that are applications of the 'State' TyCon. So it applies to the match in @f@ but not in @g@ above, resulting in a warning for the latter but not for the former. The pragma is represented as CompleteMatch {P} (Just State) GHC collects all COMPLETE pragmas from the current module and from imports into a field in the DsM environment, which can be accessed with dsGetCompleteMatches from "GHC.HsToCore.Monad". Currently, COMPLETE pragmas can't be orphans (e.g. at least one ConLike must also be defined in the module of the pragma) and do not impact recompilation checking (#18675). The pattern-match checker will then initialise each variable's 'VarInfo' with *all* imported COMPLETE sets (in 'GHC.HsToCore.Pmc.Solver.addCompleteMatches'), 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 '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 @x /~ K@ or a failed attempt at instantiating that ConLike during inhabitation testing). If *any* of the COMPLETE sets become empty, we know that the match was exhaustive. We assume that a COMPLETE set does not apply if for one of its ConLikes we fail to 'matchConLikeResTy' or the type of the match variable isn't an application of the optional result type constructor from the pragma. Why don't we simply prune inapplicable COMPLETE sets from 'ResidualCompleteMatches'? The answer is that additional type constraints might make more COMPLETE sets applicable! Example: h :: a -> a :~: Boolean -> () h x Refl | T <- x = () | F <- x = () If we eagerly prune {F,T} from the residual matches of @x@, then we don't see that the match in the guards of @h@ is exhaustive, where the COMPLETE set applies due to refined type information. -} ----------------------- -- * Type normalisation -- | The return value of 'pmTopNormaliseType' data TopNormaliseTypeResult = NormalisedByConstraints Type -- ^ 'tcNormalise' was able to simplify the type with some local constraint -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type -- redex. | HadRedexes Type [(Type, DataCon, Type)] Type -- ^ 'tcNormalise' may or may not been able to simplify the type, but -- 'topNormaliseTypeX' made progress either way and got rid of at least one -- outermost type or data family redex or newtype. -- The first field is the last type that was reduced solely through type -- family applications (possibly just the 'tcNormalise'd type). This is the -- one that is equal (in source Haskell) to the initial type. -- The third field is the type that we get when also looking through data -- family applications and newtypes. This would be the representation type in -- Core (modulo casts). -- The second field is the list of Newtype 'DataCon's that we looked through -- 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 -- 'generateInhabitingPatterns'. -- For an example, see Note [Type normalisation]. -- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the -- other cases. tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type) tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type) tntrGuts (NormalisedByConstraints Type ty) = (Type ty, [], Type ty) tntrGuts (HadRedexes Type src_ty [(Type, DataCon, Type)] ds Type core_ty) = (Type src_ty, [(Type, DataCon, Type)] ds, Type core_ty) instance Outputable TopNormaliseTypeResult where ppr :: TopNormaliseTypeResult -> SDoc ppr (NormalisedByConstraints Type ty) = String -> SDoc forall doc. IsLine doc => String -> doc text String "NormalisedByConstraints" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty ppr (HadRedexes Type src_ty [(Type, DataCon, Type)] ds Type core_ty) = String -> SDoc forall doc. IsLine doc => String -> doc text String "HadRedexes" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> SDoc -> SDoc forall doc. IsLine doc => doc -> doc braces SDoc fields where fields :: SDoc fields = [SDoc] -> SDoc forall doc. IsLine doc => [doc] -> doc fsep (SDoc -> [SDoc] -> [SDoc] forall doc. IsLine doc => doc -> [doc] -> [doc] punctuate SDoc forall doc. IsLine doc => doc comma [ String -> SDoc forall doc. IsLine doc => String -> doc text String "src_ty =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type src_ty , String -> SDoc forall doc. IsLine doc => String -> doc text String "newtype_dcs =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [(Type, DataCon, Type)] -> SDoc forall a. Outputable a => a -> SDoc ppr [(Type, DataCon, Type)] ds , String -> SDoc forall doc. IsLine doc => String -> doc text String "core_ty =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type core_ty ]) pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult -- ^ Get rid of *outermost* (or toplevel) -- * type function redex -- * data family redex -- * newtypes -- -- Behaves like `topNormaliseType_maybe`, but instead of returning a -- coercion, it returns useful information for issuing pattern matching -- warnings. See Note [Type normalisation] for details. -- It also initially 'tcNormalise's the type with the bag of local constraints. -- -- See 'TopNormaliseTypeResult' for the meaning of the return value. -- -- 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 :: TyState -> Type -> DsM TopNormaliseTypeResult pmTopNormaliseType (TySt Int _ InertSet inert) Type typ = {-# SCC "pmTopNormaliseType" #-} do env <- DsM FamInstEnvs 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]. typ' <- initTcDsForSolver $ tcNormalise inert typ -- Now we look with topNormaliseTypeX through type and data family -- applications and newtypes, which tcNormalise does not do. -- See also 'TopNormaliseTypeResult'. pure $ case topNormaliseTypeX (stepper env) comb typ' of Maybe ((ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]), Type) Nothing -> Type -> TopNormaliseTypeResult NormalisedByConstraints Type typ' Just ((ThetaType -> ThetaType ty_f,[(Type, DataCon, Type)] -> [(Type, DataCon, Type)] tm_f), Type ty) -> Type -> [(Type, DataCon, Type)] -> Type -> TopNormaliseTypeResult HadRedexes Type src_ty [(Type, DataCon, Type)] newtype_dcs Type core_ty where src_ty :: Type src_ty = Type -> ThetaType -> Type eq_src_ty Type ty (Type typ' Type -> ThetaType -> ThetaType forall a. a -> [a] -> [a] : ThetaType -> ThetaType ty_f [Type ty]) newtype_dcs :: [(Type, DataCon, Type)] newtype_dcs = [(Type, DataCon, Type)] -> [(Type, DataCon, Type)] tm_f [] core_ty :: Type core_ty = Type ty where -- Find the first type in the sequence of rewrites that is a data type, -- newtype, or a data family application (not the representation tycon!). -- This is the one that is equal (in source Haskell) to the initial type. -- If none is found in the list, then all of them are type family -- applications, so we simply return the last one, which is the *simplest*. eq_src_ty :: Type -> [Type] -> Type eq_src_ty :: Type -> ThetaType -> Type eq_src_ty Type ty ThetaType tys = Type -> (Type -> Type) -> Maybe Type -> Type forall b a. b -> (a -> b) -> Maybe a -> b maybe Type ty Type -> Type forall a. a -> a id ((Type -> Bool) -> ThetaType -> Maybe Type forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find Type -> Bool is_closed_or_data_family ThetaType tys) is_closed_or_data_family :: Type -> Bool is_closed_or_data_family :: Type -> Bool is_closed_or_data_family Type ty = Type -> Bool pmIsClosedType Type ty Bool -> Bool -> Bool || Type -> Bool isDataFamilyAppType Type ty -- For efficiency, represent both lists as difference lists. -- comb performs the concatenation, for both lists. comb :: (b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c) comb (b -> c tyf1, b -> c tmf1) (a -> b tyf2, a -> b tmf2) = (b -> c tyf1 (b -> c) -> (a -> b) -> a -> c forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> b tyf2, b -> c tmf1 (b -> c) -> (a -> b) -> a -> c forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> b tmf2) stepper :: FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) stepper FamInstEnvs env = NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) newTypeStepper NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) -> NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) -> NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) forall ev. NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev `composeSteppers` FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) forall a. FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a) tyFamStepper FamInstEnvs env -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into -- a loop. If it would fall into a loop, it produces 'NS_Abort'. newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) newTypeStepper :: NormaliseStepper (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) newTypeStepper RecTcChecker rec_nts TyCon tc ThetaType tys | Just (Type ty', Coercion _co) <- TyCon -> ThetaType -> Maybe (Type, Coercion) instNewTyCon_maybe TyCon tc ThetaType tys , let orig_ty :: Type orig_ty = TyCon -> ThetaType -> Type TyConApp TyCon tc ThetaType tys = case RecTcChecker -> TyCon -> Maybe RecTcChecker checkRecTc RecTcChecker rec_nts TyCon tc of Just RecTcChecker rec_nts' -> let tyf :: ThetaType -> ThetaType tyf = (Type orig_tyType -> ThetaType -> ThetaType forall a. a -> [a] -> [a] :) tmf :: [(Type, DataCon, Type)] -> [(Type, DataCon, Type)] tmf = ((Type orig_ty, TyCon -> DataCon tyConSingleDataCon TyCon tc, Type ty')(Type, DataCon, Type) -> [(Type, DataCon, Type)] -> [(Type, DataCon, Type)] forall a. a -> [a] -> [a] :) in RecTcChecker -> Type -> (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) -> NormaliseStepResult (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev NS_Step RecTcChecker rec_nts' Type ty' (ThetaType -> ThetaType tyf, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)] tmf) Maybe RecTcChecker Nothing -> NormaliseStepResult (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) forall ev. NormaliseStepResult ev NS_Abort | Bool otherwise = NormaliseStepResult (ThetaType -> ThetaType, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) forall ev. NormaliseStepResult ev NS_Done tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a) tyFamStepper :: forall a. FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a) tyFamStepper FamInstEnvs env RecTcChecker rec_nts TyCon tc ThetaType tys -- Try to step a type/data family = case FamInstEnvs -> TyCon -> ThetaType -> Maybe HetReduction topReduceTyFamApp_maybe FamInstEnvs env TyCon tc ThetaType tys of Just (HetReduction (Reduction Coercion _ Type rhs) MCoercionN _) -> RecTcChecker -> Type -> (ThetaType -> ThetaType, a -> a) -> NormaliseStepResult (ThetaType -> ThetaType, a -> a) forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev NS_Step RecTcChecker rec_nts Type rhs ((Type rhsType -> ThetaType -> ThetaType forall a. a -> [a] -> [a] :), a -> a forall a. a -> a id) Maybe HetReduction _ -> NormaliseStepResult (ThetaType -> ThetaType, a -> a) forall ev. NormaliseStepResult ev NS_Done -- | Returns 'True' if the argument 'Type' is a fully saturated application of -- a closed type constructor. -- -- Closed type constructors are those with a fixed right hand side, as -- opposed to e.g. associated types. These are of particular interest for -- pattern-match coverage checking, because GHC can exhaustively consider all -- possible forms that values of a closed type can take on. -- -- Note that this function is intended to be used to check types of value-level -- patterns, so as a consequence, the 'Type' supplied as an argument to this -- function should be of kind @Type@. pmIsClosedType :: Type -> Bool pmIsClosedType :: Type -> Bool pmIsClosedType Type ty = case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType) Type -> Maybe (TyCon, ThetaType) splitTyConApp_maybe Type ty of Just (TyCon tc, ThetaType ty_args) | TyCon -> Bool is_algebraic_like TyCon tc Bool -> Bool -> Bool && Bool -> Bool not (TyCon -> Bool isFamilyTyCon TyCon tc) -> Bool -> SDoc -> Bool -> Bool forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr (ThetaType ty_args ThetaType -> Int -> Bool forall a. [a] -> Int -> Bool `lengthIs` TyCon -> Int tyConArity TyCon tc) (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty) Bool True Maybe (TyCon, ThetaType) _other -> Bool False where -- This returns True for TyCons which /act like/ algebraic types. -- (See "Type#type_classification" for what an algebraic type is.) -- -- This is qualified with \"like\" because of a particular special -- case: TYPE (the underlying kind behind Type, among others). TYPE -- is conceptually a datatype (and thus algebraic), but in practice it is -- a primitive builtin type, so we must check for it specially. -- -- NB: it makes sense to think of TYPE as a closed type in a value-level, -- pattern-matching context. However, at the kind level, TYPE is certainly -- not closed! Since this function is specifically tailored towards pattern -- matching, however, it's OK to label TYPE as closed. is_algebraic_like :: TyCon -> Bool is_algebraic_like :: TyCon -> Bool is_algebraic_like TyCon tc = TyCon -> Bool isAlgTyCon TyCon tc Bool -> Bool -> Bool || TyCon tc TyCon -> TyCon -> Bool forall a. Eq a => a -> a -> Bool == TyCon 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 :: TyState -> Type -> DsM Type normaliseSourceTypeWHNF TyState _ Type ty | Type -> Bool isSourceTypeInWHNF Type ty = Type -> DsM Type forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Type ty normaliseSourceTypeWHNF TyState ty_st Type ty = TyState -> Type -> DsM TopNormaliseTypeResult pmTopNormaliseType TyState ty_st Type ty DsM TopNormaliseTypeResult -> (TopNormaliseTypeResult -> DsM Type) -> DsM Type forall a b. IOEnv (Env DsGblEnv DsLclEnv) a -> (a -> IOEnv (Env DsGblEnv DsLclEnv) b) -> IOEnv (Env DsGblEnv DsLclEnv) b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= \case NormalisedByConstraints Type ty -> Type -> DsM Type forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Type ty HadRedexes Type ty [(Type, DataCon, Type)] _ Type _ -> Type -> DsM Type forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Type 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 :: Type -> Bool isSourceTypeInWHNF Type ty | Just (TyCon tc, ThetaType _) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType) Type -> Maybe (TyCon, ThetaType) splitTyConApp_maybe Type ty = Bool -> Bool not (TyCon -> Bool isTypeFamilyTyCon TyCon tc) | Bool otherwise = Bool False {- Note [Type normalisation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data constructor place a non-void constraint on the matched thing. This means that it boils down to checking whether the type of the scrutinee is inhabited. Function pmTopNormaliseType gets rid of the outermost type function/data family redex and newtypes, in search of an algebraic type constructor, which is easier to check for inhabitation. It returns 3 results instead of one, because there are 2 subtle points: 1. Newtypes are isomorphic to the underlying type in core but not in the source language, 2. The representational data family tycon is used internally but should not be shown to the user Hence, if pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty), then (a) src_ty is the rewritten type which we can show to the user. That is, the type we get if we rewrite type families but not data families or newtypes. (b) dcs is the list of newtype constructors "skipped", every time we normalise a newtype to its core representation, we keep track of the source data constructor. For convenience, we also track the type we unwrap and the type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)] (c) core_ty is the rewritten type. That is, pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty) implies topNormaliseType_maybe env ty = Just (co, core_ty) for some coercion co. To see how all cases come into play, consider the following example: data family T a :: * data instance T Int = T1 | T2 Bool -- Which gives rise to FC: -- data T a -- data R:TInt = T1 | T2 Bool -- axiom ax_ti : T Int ~R R:TInt newtype G1 = MkG1 (T Int) newtype G2 = MkG2 G1 type instance F Int = F Char type instance F Char = G2 In this case pmTopNormaliseType env ty_cs (F Int) results in Just (G2, [(G2,MkG2,G1),(G1,MkG1,T Int)], R:TInt) Which means that in source Haskell: - G2 is equivalent to F Int (in contrast, G1 isn't). - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int). ----- -- Wrinkle: Local equalities ----- Given the following type family: type family F a type instance F Int = Void Should the following program (from #14813) be considered exhaustive? f :: (i ~ Int) => F i -> a f x = case x of {} You might think "of course, since `x` is obviously of type Void". But the idType of `x` is technically F i, not Void, so if we pass F i to inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive. In order to avoid this pitfall, we need to normalise the type passed to pmTopNormaliseType, using the constraint solver to solve for any local equalities (such as i ~ Int) that may be in scope. Note [Coverage checking Newtype matches] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Newtypes have quite peculiar match semantics compared to ordinary DataCons. In a pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation testing purposes (e.g. at construction sites), they behave rather like a DataCon with a *strict* field, because they don't contribute their own bottom and are inhabited iff the wrapped type is inhabited. This distinction becomes apparent in #17248: newtype T2 a = T2 a g _ True = () g (T2 _) True = () g !_ True = () If we treat Newtypes like we treat regular DataCons, we would mark the third clause as redundant, which clearly is unsound. The solution: 1. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a newtype match is lazy. 2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@) to @y@, similar to what 'equate' does, and don't add a @x ≁ ⊥@ constraint. This way, the third clause will still be marked as inaccessible RHS instead of redundant. This is ensured by calling 'lookupVarInfoNT'. 3. Immediately reject when we find @x ≁ T2@. Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper, where you can find the solution in a perhaps more digestible format. -} ------------------------- -- * 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 variables of unlifted type]. | PhiNotConCt !Id !PmAltCon -- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed -- by @K@. | PhiBotCt !Id -- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥. -- by @K@. | PhiNotBotCt !Id -- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥. instance Outputable PhiCt where ppr :: PhiCt -> SDoc ppr (PhiTyCt Type ty_ct) = Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ty_ct ppr (PhiCoreCt Id x CoreExpr e) = Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Char -> SDoc forall doc. IsLine doc => Char -> doc char Char '~' SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> CoreExpr -> SDoc forall a. Outputable a => a -> SDoc ppr CoreExpr e ppr (PhiConCt Id x PmAltCon con [Id] tvs ThetaType dicts [Id] args) = [SDoc] -> SDoc forall doc. IsLine doc => [doc] -> doc hsep (PmAltCon -> SDoc forall a. Outputable a => a -> SDoc ppr PmAltCon con SDoc -> [SDoc] -> [SDoc] forall a. a -> [a] -> [a] : [SDoc] pp_tvs [SDoc] -> [SDoc] -> [SDoc] forall a. [a] -> [a] -> [a] ++ [SDoc] pp_dicts [SDoc] -> [SDoc] -> [SDoc] forall a. [a] -> [a] -> [a] ++ [SDoc] pp_args) SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> String -> SDoc forall doc. IsLine doc => String -> doc text String "<-" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x where pp_tvs :: [SDoc] pp_tvs = (Id -> SDoc) -> [Id] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map ((SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <> Char -> SDoc forall doc. IsLine doc => Char -> doc char Char '@') (SDoc -> SDoc) -> (Id -> SDoc) -> Id -> SDoc forall b c a. (b -> c) -> (a -> b) -> a -> c . Id -> SDoc forall a. Outputable a => a -> SDoc ppr) [Id] tvs pp_dicts :: [SDoc] pp_dicts = (Type -> SDoc) -> ThetaType -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Type -> SDoc forall a. Outputable a => a -> SDoc ppr ThetaType dicts pp_args :: [SDoc] pp_args = (Id -> SDoc) -> [Id] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Id -> SDoc forall a. Outputable a => a -> SDoc ppr [Id] args ppr (PhiNotConCt Id x PmAltCon con) = Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> String -> SDoc forall doc. IsLine doc => String -> doc text String "≁" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> PmAltCon -> SDoc forall a. Outputable a => a -> SDoc ppr PmAltCon con ppr (PhiBotCt Id x) = Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> String -> SDoc forall doc. IsLine doc => String -> doc text String "~ ⊥" ppr (PhiNotBotCt Id x) = Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> String -> SDoc forall doc. IsLine doc => String -> doc text String "≁ ⊥" type PhiCts = Bag PhiCt -- | The fuel for the inhabitation test. -- See Note [Fuel for the inhabitation test]. initFuel :: Int initFuel :: Int initFuel = Int 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. -- -- 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]. addPhiCts :: Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) addPhiCts Nabla nabla PhiCts cts = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) forall (m :: * -> *) a. MaybeT m a -> m (Maybe a) runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) forall a b. (a -> b) -> a -> b $ do let (ThetaType ty_cts, [PhiCt] tm_cts) = PhiCts -> (ThetaType, [PhiCt]) partitionPhiCts PhiCts cts nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addTyCts Nabla nabla (ThetaType -> Bag Type forall a. [a] -> Bag a listToBag ThetaType ty_cts) nabla'' <- foldlM addPhiTmCt nabla' (listToBag tm_cts) inhabitationTest initFuel (nabla_ty_st nabla) nabla'' partitionPhiCts :: PhiCts -> ([PredType], [PhiCt]) partitionPhiCts :: PhiCts -> (ThetaType, [PhiCt]) partitionPhiCts = (PhiCt -> Either Type PhiCt) -> [PhiCt] -> (ThetaType, [PhiCt]) forall a b c. (a -> Either b c) -> [a] -> ([b], [c]) partitionWith PhiCt -> Either Type PhiCt to_either ([PhiCt] -> (ThetaType, [PhiCt])) -> (PhiCts -> [PhiCt]) -> PhiCts -> (ThetaType, [PhiCt]) forall b c a. (b -> c) -> (a -> b) -> a -> c . PhiCts -> [PhiCt] forall a. Bag a -> [a] forall (t :: * -> *) a. Foldable t => t a -> [a] toList where to_either :: PhiCt -> Either Type PhiCt to_either (PhiTyCt Type pred_ty) = Type -> Either Type PhiCt forall a b. a -> Either a b Left Type pred_ty to_either PhiCt ct = PhiCt -> Either Type PhiCt forall a b. b -> Either a b Right PhiCt 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 -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addTyCts nabla :: Nabla nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState nabla_ty_st = TyState ty_st } Bag Type new_ty_cs = do ty_st' <- DsM (Maybe TyState) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TyState forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a MaybeT (TyState -> Bag Type -> DsM (Maybe TyState) tyOracle TyState ty_st Bag Type 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@). -- -- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver. tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState) tyOracle :: TyState -> Bag Type -> DsM (Maybe TyState) tyOracle ty_st :: TyState ty_st@(TySt Int n InertSet inert) Bag Type cts | Bag Type -> Bool forall a. Bag a -> Bool isEmptyBag Bag Type cts = Maybe TyState -> DsM (Maybe TyState) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (TyState -> Maybe TyState forall a. a -> Maybe a Just TyState ty_st) | Bool otherwise = {-# SCC "tyOracle" #-} do { evs <- (Type -> IOEnv (Env DsGblEnv DsLclEnv) Id) -> Bag Type -> IOEnv (Env DsGblEnv DsLclEnv) (Bag Id) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> Bag a -> f (Bag b) traverse Type -> IOEnv (Env DsGblEnv DsLclEnv) Id nameTyCt Bag Type cts ; tracePm "tyOracle" (ppr n $$ ppr cts $$ ppr inert) ; mb_new_inert <- initTcDsForSolver $ tcCheckGivens inert evs -- return the new inert set and increment the sequence number n ; return (TySt (n+1) <$> mb_new_inert) } -- | Allocates a fresh 'EvVar' name for 'PredTy's. nameTyCt :: PredType -> DsM EvVar nameTyCt :: Type -> IOEnv (Env DsGblEnv DsLclEnv) Id nameTyCt Type pred_ty = do unique <- IOEnv (Env DsGblEnv DsLclEnv) Unique forall (m :: * -> *). MonadUnique m => m Unique getUniqueM let occname = FastString -> OccName mkVarOccFS (String -> FastString fsLit (String "pm_"String -> String -> String forall a. [a] -> [a] -> [a] ++Unique -> String forall a. Show a => a -> String show Unique unique)) return (mkUserLocalOrCoVar occname unique ManyTy pred_ty noSrcSpan) ----------------------------- -- ** 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 :: Nabla -> PhiCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addPhiTmCt Nabla _ (PhiTyCt Type ct) = String -> SDoc -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. HasCallStack => String -> SDoc -> a pprPanic String "addPhiCt:TyCt" (Type -> SDoc forall a. Outputable a => a -> SDoc ppr Type ct) -- See the precondition addPhiTmCt Nabla nabla (PhiCoreCt Id x CoreExpr e) = Nabla -> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addCoreCt Nabla nabla Id x CoreExpr e addPhiTmCt Nabla nabla (PhiConCt Id x PmAltCon con [Id] tvs ThetaType dicts [Id] 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' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addTyCts Nabla nabla (ThetaType -> Bag Type forall a. [a] -> Bag a listToBag ThetaType dicts) nabla'' <- addConCt nabla' x con tvs args foldlM addNotBotCt nabla'' (filterUnliftedFields con args) addPhiTmCt Nabla nabla (PhiNotConCt Id x PmAltCon con) = Nabla -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotConCt Nabla nabla Id x PmAltCon con addPhiTmCt Nabla nabla (PhiBotCt Id x) = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addBotCt Nabla nabla Id x addPhiTmCt Nabla nabla (PhiNotBotCt Id x) = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotBotCt Nabla nabla Id x filterUnliftedFields :: PmAltCon -> [Id] -> [Id] filterUnliftedFields :: PmAltCon -> [Id] -> [Id] filterUnliftedFields PmAltCon con [Id] args = [ Id arg | (Id arg, HsImplBang bang) <- String -> [Id] -> [HsImplBang] -> [(Id, HsImplBang)] forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)] zipEqual String "addPhiCt" [Id] args (PmAltCon -> [HsImplBang] pmAltConImplBangs PmAltCon con) , HsImplBang -> Bool isBanged HsImplBang bang Bool -> Bool -> Bool || Type -> Bool definitelyUnliftedType (Id -> Type idType Id 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 -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addBotCt nabla :: Nabla nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState nabla_tm_st = ts :: TmState ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo ts_facts=UniqSDFM Id VarInfo env } } Id x = do let (Id y, vi :: VarInfo vi@VI { vi_bot :: VarInfo -> BotInfo vi_bot = BotInfo bot }) = TmState -> Id -> (Id, VarInfo) lookupVarInfoNT (Nabla -> TmState nabla_tm_st Nabla nabla) Id x case BotInfo bot of BotInfo IsNotBot -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (m :: * -> *) a. MonadPlus m => m a mzero -- There was x ≁ ⊥. Contradiction! BotInfo IsBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla -- There already is x ~ ⊥. Nothing left to do BotInfo MaybeBot -- We add x ~ ⊥ | Type -> Bool definitelyUnliftedType (Id -> Type idType Id x) -- Case (3) in Note [Strict fields and variables of unlifted type] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (m :: * -> *) a. MonadPlus m => m a mzero -- unlifted vars can never be ⊥ | Bool otherwise -> do let vi' :: VarInfo vi' = VarInfo vi{ vi_bot = IsBot } Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM 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 -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotBotCt nabla :: Nabla nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState nabla_tm_st = ts :: TmState ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo ts_facts=UniqSDFM Id VarInfo env} } Id x = do let (Id y, vi :: VarInfo vi@VI { vi_bot :: VarInfo -> BotInfo vi_bot = BotInfo bot }) = TmState -> Id -> (Id, VarInfo) lookupVarInfoNT (Nabla -> TmState nabla_tm_st Nabla nabla) Id x case BotInfo bot of BotInfo IsBot -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (m :: * -> *) a. MonadPlus m => m a mzero -- There was x ~ ⊥. Contradiction! BotInfo IsNotBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla -- There already is x ≁ ⊥. Nothing left to do BotInfo MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited -- Mark dirty for a delayed inhabitation test let vi' :: VarInfo vi' = VarInfo vi{ vi_bot = IsNotBot} Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a b. (a -> b) -> a -> b $ Id -> Nabla -> Nabla markDirty Id y (Nabla -> Nabla) -> Nabla -> Nabla forall a b. (a -> b) -> a -> b $ Nabla nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM 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 :: Nabla -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotConCt Nabla _ Id _ (PmAltConLike (RealDataCon DataCon dc)) | DataCon -> Bool isNewDataCon DataCon dc = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (m :: * -> *) a. MonadPlus m => m a mzero -- (3) in Note [Coverage checking Newtype matches] addNotConCt Nabla nabla Id x PmAltCon nalt = do (mb_mark_dirty, nabla') <- (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)) -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, Nabla) forall (f :: * -> *) a. Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla) trvVarInfo VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo) go Nabla nabla Id x pure $ case mb_mark_dirty of Just Id x -> Id -> Nabla -> Nabla markDirty Id x Nabla nabla' Maybe Id Nothing -> Nabla nabla' where -- Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction, -- otherwise return updated entry and `Just x'` if `x` should be marked dirty, -- where `x'` is the representative of `x`. go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo) go :: VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo) go vi :: VarInfo vi@(VI Id x' [PmAltConApp] pos PmAltConSet neg BotInfo _ ResidualCompleteMatches rcm) = do -- 1. Bail out quickly when nalt contradicts a solution let contradicts :: PmAltCon -> PmAltConApp -> Bool contradicts PmAltCon nalt PmAltConApp sol = PmAltCon -> PmAltCon -> PmEquality eqPmAltCon (PmAltConApp -> PmAltCon paca_con PmAltConApp sol) PmAltCon nalt PmEquality -> PmEquality -> Bool forall a. Eq a => a -> a -> Bool == PmEquality Equal Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) () forall (f :: * -> *). Alternative f => Bool -> f () guard (Bool -> Bool not ((PmAltConApp -> Bool) -> [PmAltConApp] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool any (PmAltCon -> PmAltConApp -> Bool contradicts PmAltCon nalt) [PmAltConApp] pos)) -- 2. Only record the new fact when it's not already implied by one of the -- solutions let implies :: PmAltCon -> PmAltConApp -> Bool implies PmAltCon nalt PmAltConApp sol = PmAltCon -> PmAltCon -> PmEquality eqPmAltCon (PmAltConApp -> PmAltCon paca_con PmAltConApp sol) PmAltCon nalt PmEquality -> PmEquality -> Bool forall a. Eq a => a -> a -> Bool == PmEquality Disjoint let neg' :: PmAltConSet neg' | (PmAltConApp -> Bool) -> [PmAltConApp] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool any (PmAltCon -> PmAltConApp -> Bool implies PmAltCon nalt) [PmAltConApp] pos = PmAltConSet neg -- See Note [Completeness checking with required Thetas] | PmAltCon -> Bool hasRequiredTheta PmAltCon nalt = PmAltConSet neg | Bool otherwise = PmAltConSet -> PmAltCon -> PmAltConSet extendPmAltConSet PmAltConSet neg PmAltCon nalt Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) () forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m () massert (PmAltCon -> Bool isPmAltConMatchStrict PmAltCon nalt) let vi' :: VarInfo vi' = VarInfo vi{ vi_neg = neg', vi_bot = IsNotBot } -- 3. Make sure there's at least one other possible constructor mb_rcm' <- DsM (Maybe ResidualCompleteMatches) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe ResidualCompleteMatches) forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches) markMatched PmAltCon nalt ResidualCompleteMatches rcm) pure $ case mb_rcm' of -- If nalt could be removed from a COMPLETE set, we'll get back Just and -- have to mark x dirty, by returning Just x'. Just ResidualCompleteMatches rcm' -> (Id -> Maybe Id forall a. a -> Maybe a Just Id x', VarInfo vi'{ vi_rcm = rcm' }) -- Otherwise, nalt didn't occur in any residual COMPLETE set and we -- don't have to mark it dirty. So we return Nothing, which in the case -- above would have compromised precision. -- See Note [Shortcutting the inhabitation test], grep for T17836. Maybe ResidualCompleteMatches Nothing -> (Maybe Id forall a. Maybe a Nothing, VarInfo vi') hasRequiredTheta :: PmAltCon -> Bool hasRequiredTheta :: PmAltCon -> Bool hasRequiredTheta (PmAltConLike ConLike cl) = ThetaType -> Bool forall (f :: * -> *) a. Foldable f => f a -> Bool notNull ThetaType req_theta where ([Id] _,[Id] _,[EqSpec] _,ThetaType _,ThetaType req_theta,[Scaled Type] _,Type _) = ConLike -> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type], Type) conLikeFullSig ConLike cl hasRequiredTheta PmAltCon _ = Bool False -- | 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 -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addConCt nabla :: Nabla nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState nabla_tm_st = ts :: TmState ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo ts_facts=UniqSDFM Id VarInfo env } } Id x PmAltCon alt [Id] tvs [Id] args = do let vi :: VarInfo vi@(VI Id _ [PmAltConApp] pos PmAltConSet neg BotInfo bot ResidualCompleteMatches _) = TmState -> Id -> VarInfo lookupVarInfo TmState ts Id x -- First try to refute with a negative fact Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) () forall (f :: * -> *). Alternative f => Bool -> f () guard (Bool -> Bool not (PmAltCon -> PmAltConSet -> Bool elemPmAltConSet PmAltCon alt PmAltConSet 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 Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) () forall (f :: * -> *). Alternative f => Bool -> f () guard ((PmAltConApp -> Bool) -> [PmAltConApp] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all ((PmEquality -> PmEquality -> Bool forall a. Eq a => a -> a -> Bool /= PmEquality Disjoint) (PmEquality -> Bool) -> (PmAltConApp -> PmEquality) -> PmAltConApp -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . PmAltCon -> PmAltCon -> PmEquality eqPmAltCon PmAltCon alt (PmAltCon -> PmEquality) -> (PmAltConApp -> PmAltCon) -> PmAltConApp -> PmEquality forall b c a. (b -> c) -> (a -> b) -> a -> c . PmAltConApp -> PmAltCon paca_con) [PmAltConApp] pos) -- Now we should be good! Add (alt, tvs, args) as a possible solution, or -- refine an existing one case (PmAltConApp -> Bool) -> [PmAltConApp] -> Maybe PmAltConApp forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find ((PmEquality -> PmEquality -> Bool forall a. Eq a => a -> a -> Bool == PmEquality Equal) (PmEquality -> Bool) -> (PmAltConApp -> PmEquality) -> PmAltConApp -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . PmAltCon -> PmAltCon -> PmEquality eqPmAltCon PmAltCon alt (PmAltCon -> PmEquality) -> (PmAltConApp -> PmAltCon) -> PmAltConApp -> PmEquality forall b c a. (b -> c) -> (a -> b) -> a -> c . PmAltConApp -> PmAltCon paca_con) [PmAltConApp] pos of Just (PACA PmAltCon _con [Id] other_tvs [Id] other_args) -> do -- We must unify existentially bound ty vars and arguments! let ty_cts :: [PhiCt] ty_cts = ThetaType -> ThetaType -> [PhiCt] equateTys ((Id -> Type) -> [Id] -> ThetaType forall a b. (a -> b) -> [a] -> [b] map Id -> Type mkTyVarTy [Id] tvs) ((Id -> Type) -> [Id] -> ThetaType forall a b. (a -> b) -> [a] -> [b] map Id -> Type mkTyVarTy [Id] other_tvs) nabla' <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a b. (a -> b) -> a -> b $ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) addPhiCts Nabla nabla ([PhiCt] -> PhiCts forall a. [a] -> Bag a listToBag [PhiCt] ty_cts) let add_var_ct Nabla nabla (Id a, Id b) = Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addVarCt Nabla nabla Id a Id b foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args Maybe PmAltConApp Nothing -> do let pos' :: [PmAltConApp] pos' = PmAltCon -> [Id] -> [Id] -> PmAltConApp PACA PmAltCon alt [Id] tvs [Id] args PmAltConApp -> [PmAltConApp] -> [PmAltConApp] forall a. a -> [a] -> [a] : [PmAltConApp] pos let nabla_with :: BotInfo -> Nabla nabla_with BotInfo bot' = Nabla nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} } -- Do (2) in Note [Coverage checking Newtype matches] case (PmAltCon alt, [Id] args) of (PmAltConLike (RealDataCon DataCon dc), [Id y]) | DataCon -> Bool isNewDataCon DataCon dc -> case BotInfo bot of BotInfo MaybeBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure (BotInfo -> Nabla nabla_with BotInfo MaybeBot) BotInfo IsBot -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addBotCt (BotInfo -> Nabla nabla_with BotInfo MaybeBot) Id y BotInfo IsNotBot -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotBotCt (BotInfo -> Nabla nabla_with BotInfo MaybeBot) Id y (PmAltCon, [Id]) _ -> Bool -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. HasCallStack => Bool -> a -> a assert (PmAltCon -> Bool isPmAltConMatchStrict PmAltCon alt ) Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure (BotInfo -> Nabla nabla_with BotInfo IsNotBot) -- strict match ==> not ⊥ equateTys :: [Type] -> [Type] -> [PhiCt] equateTys :: ThetaType -> ThetaType -> [PhiCt] equateTys ThetaType ts ThetaType us = [ Type -> PhiCt PhiTyCt (Type -> Type -> Type mkPrimEqPred Type t Type u) | (Type t, Type u) <- String -> ThetaType -> ThetaType -> [(Type, Type)] forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)] zipEqual String "equateTys" ThetaType ts ThetaType us -- The following line filters out trivial Refl constraints, so that we don't -- need to initialise the type oracle that often , Bool -> Bool not (HasCallStack => Type -> Type -> Bool Type -> Type -> Bool eqType Type t Type u) ] -- | Adds a @x ~ y@ constraint by merging the two 'VarInfo's and record the -- gained knowledge in 'Nabla'. -- -- Returns @Nothing@ when there's a contradiction while merging. Returns @Just -- nabla@ when the constraint was compatible with prior facts, in which case -- @nabla@ has integrated the knowledge from the equality constraint. -- -- See Note [TmState invariants]. addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla addVarCt :: Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addVarCt nabla :: Nabla nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState nabla_tm_st = ts :: TmState ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo ts_facts = UniqSDFM Id VarInfo env } } Id x Id y = case UniqSDFM Id VarInfo -> Id -> Id -> (Maybe VarInfo, UniqSDFM Id VarInfo) forall key ele. Uniquable key => UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele) equateUSDFM UniqSDFM Id VarInfo env Id x Id y of (Maybe VarInfo Nothing, UniqSDFM Id VarInfo env') -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Nabla nabla{ nabla_tm_st = ts{ ts_facts = env' } }) -- Add the constraints we had for x to y (Just VarInfo vi_x, UniqSDFM Id VarInfo env') -> do let nabla_equated :: Nabla nabla_equated = Nabla nabla{ nabla_tm_st = ts{ts_facts = env'} } -- and then gradually merge every positive fact we have on x into y let add_pos :: Nabla -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla add_pos Nabla nabla (PACA PmAltCon cl [Id] tvs [Id] args) = Nabla -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addConCt Nabla nabla Id y PmAltCon cl [Id] tvs [Id] args nabla_pos <- (Nabla -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> Nabla -> [PmAltConApp] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall (t :: * -> *) (m :: * -> *) b a. (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b foldlM Nabla -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla add_pos Nabla nabla_equated (VarInfo -> [PmAltConApp] vi_pos VarInfo vi_x) -- Do the same for negative info let add_neg Nabla nabla PmAltCon nalt = Nabla -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotConCt Nabla nabla Id y PmAltCon nalt foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x)) -- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based -- on the shape of the 'CoreExpr' @e@. Examples: -- -- * For @let x = Just (42, 'z')@ we want to record the -- constraints @x ~ Just a, a ~ (b, c), b ~ 42, c ~ 'z'@. -- See 'data_con_app'. -- * For @let x = unpackCString# "tmp"@ we want to record the literal -- constraint @x ~ "tmp"@. -- * For @let x = I# 42@ we want the literal constraint @x ~ 42@. Similar -- for other literals. See 'coreExprAsPmLit'. -- * Finally, if we have @let x = e@ and we already have seen @let y = e@, we -- want to record @x ~ y@. addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addCoreCt Nabla nabla Id x CoreExpr e = do simpl_opts <- DynFlags -> SimpleOpts initSimpleOpts (DynFlags -> SimpleOpts) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) DynFlags -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) SimpleOpts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) DynFlags forall (m :: * -> *). HasDynFlags m => m DynFlags getDynFlags let e' = HasDebugCallStack => SimpleOpts -> CoreExpr -> CoreExpr SimpleOpts -> CoreExpr -> CoreExpr simpleOptExpr SimpleOpts simpl_opts CoreExpr e -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e') execStateT (core_expr x e') nabla where -- Takes apart a 'CoreExpr' and tries to extract as much information about -- literals and constructor applications as possible. core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) () -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon -- This is the right thing for casts involving data family instances and -- their representation TyCon, though (which are not visible in source -- syntax). See Note [COMPLETE sets on data families] -- core_expr x e | pprTrace "core_expr" (ppr x $$ ppr e) False = undefined core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () core_expr Id x (Cast CoreExpr e Coercion _co) = Id -> CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () core_expr Id x CoreExpr e core_expr Id x (Tick CoreTickish _t CoreExpr e) = Id -> CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () core_expr Id x CoreExpr e core_expr Id x CoreExpr e | Just (PmLit -> Maybe FastString pmLitAsStringLit -> Just FastString s) <- CoreExpr -> Maybe PmLit coreExprAsPmLit CoreExpr e , Type expr_ty HasCallStack => Type -> Type -> Bool Type -> Type -> Bool `eqType` Type stringTy -- See Note [Representation of Strings in TmState] = case FastString -> String unpackFS FastString s of -- We need this special case to break a loop with coreExprAsPmLit -- Otherwise we alternate endlessly between [] and "" [] -> Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () data_con_app Id x InScopeSet emptyInScopeSet DataCon nilDataCon [] String s' -> Id -> CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () core_expr Id x (Type -> [CoreExpr] -> CoreExpr mkListExpr Type charTy ((Char -> CoreExpr) -> String -> [CoreExpr] forall a b. (a -> b) -> [a] -> [b] map Char -> CoreExpr mkCharExpr String s')) | Just PmLit lit <- CoreExpr -> Maybe PmLit coreExprAsPmLit CoreExpr e = Id -> PmLit -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () pm_lit Id x PmLit lit | Just (InScopeSet in_scope, _empty_floats :: [FloatBind] _empty_floats@[], DataCon dc, ThetaType _arg_tys, [CoreExpr] args) <- HasDebugCallStack => InScopeEnv -> CoreExpr -> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr]) InScopeEnv -> CoreExpr -> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr]) exprIsConApp_maybe InScopeEnv in_scope_env CoreExpr e = Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () data_con_app Id x InScopeSet in_scope DataCon dc [CoreExpr] args -- See Note [Detecting pattern synonym applications in expressions] | Var Id y <- CoreExpr e, Maybe DataCon Nothing <- Id -> Maybe DataCon isDataConId_maybe Id x -- We don't consider DataCons flexible variables = (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m () modifyT (\Nabla nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addVarCt Nabla nabla Id x Id y) | Bool otherwise -- Any other expression. Try to find other uses of a semantically -- equivalent expression and represent them by the same variable! = Id -> CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () equate_with_similar_expr Id x CoreExpr e where expr_ty :: Type expr_ty = HasDebugCallStack => CoreExpr -> Type CoreExpr -> Type exprType CoreExpr e expr_in_scope :: InScopeSet expr_in_scope = VarSet -> InScopeSet mkInScopeSet (CoreExpr -> VarSet exprFreeVars CoreExpr e) in_scope_env :: InScopeEnv in_scope_env = InScopeSet -> IdUnfoldingFun -> InScopeEnv ISE InScopeSet expr_in_scope IdUnfoldingFun noUnfoldingFun -- It's inconvenient to get hold of a global in-scope set -- here, but it'll only be needed if exprIsConApp_maybe ends -- up substituting inside a forall or lambda (i.e. seldom) -- so using exprFreeVars seems fine. See MR !1647. -- The @e@ in @let x = e@ had no familiar form. But we can still see if -- see if we already encountered a constraint @let y = e'@ with @e'@ -- semantically equivalent to @e@, in which case we may add the constraint -- @x ~ y@. equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) () equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () equate_with_similar_expr Id x CoreExpr e = do rep <- (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a StateT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id) -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id forall a b. (a -> b) -> a -> b $ \Nabla nabla -> DsM (Id, Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla) forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Nabla -> CoreExpr -> DsM (Id, Nabla) representCoreExpr Nabla nabla CoreExpr e) -- Note that @rep == x@ if we encountered @e@ for the first time. modifyT (\Nabla nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addVarCt Nabla nabla Id x Id rep) bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id bind_expr :: CoreExpr -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id bind_expr CoreExpr e = do x <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id forall (m :: * -> *) a. Monad m => m a -> StateT Nabla m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (IOEnv (Env DsGblEnv DsLclEnv) Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Type -> IOEnv (Env DsGblEnv DsLclEnv) Id mkPmId (HasDebugCallStack => CoreExpr -> Type CoreExpr -> Type exprType CoreExpr e))) core_expr x e pure x -- Look at @let x = K taus theta es@ and generate the following -- constraints (assuming universals were dropped from @taus@ before): -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor. -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@ -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@ -- 4. @x ~ K as ys@ -- This is quite similar to PmCheck.pmConCts. data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) () data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () data_con_app Id x InScopeSet in_scope DataCon dc [CoreExpr] args = do let dc_ex_tvs :: [Id] dc_ex_tvs = DataCon -> [Id] dataConExTyCoVars DataCon dc arty :: Int arty = DataCon -> Int dataConSourceArity DataCon dc ([CoreExpr] ex_ty_args, [CoreExpr] val_args) = [Id] -> [CoreExpr] -> ([CoreExpr], [CoreExpr]) forall b a. [b] -> [a] -> ([a], [a]) splitAtList [Id] dc_ex_tvs [CoreExpr] args ex_tys :: ThetaType ex_tys = (CoreExpr -> Type) -> [CoreExpr] -> ThetaType forall a b. (a -> b) -> [a] -> [b] map CoreExpr -> Type exprToType [CoreExpr] ex_ty_args vis_args :: [CoreExpr] vis_args = [CoreExpr] -> [CoreExpr] forall a. [a] -> [a] reverse ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr] forall a b. (a -> b) -> a -> b $ Int -> [CoreExpr] -> [CoreExpr] forall a. Int -> [a] -> [a] take Int arty ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr] forall a b. (a -> b) -> a -> b $ [CoreExpr] -> [CoreExpr] forall a. [a] -> [a] reverse [CoreExpr] val_args uniq_supply <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply forall (m :: * -> *) a. Monad m => m a -> StateT Nabla m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply forall a b. (a -> b) -> a -> b $ DsM UniqSupply -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (DsM UniqSupply -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply) -> DsM UniqSupply -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply forall a b. (a -> b) -> a -> b $ DsM UniqSupply forall (m :: * -> *). MonadUnique m => m UniqSupply getUniqueSupplyM let (_, ex_tvs) = cloneTyVarBndrs (mkEmptySubst in_scope) dc_ex_tvs uniq_supply ty_cts = ThetaType -> ThetaType -> [PhiCt] equateTys ((Id -> Type) -> [Id] -> ThetaType forall a b. (a -> b) -> [a] -> [b] map Id -> Type mkTyVarTy [Id] ex_tvs) ThetaType ex_tys -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor (#18341) when (not (isNewDataCon dc)) $ modifyT $ \Nabla nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotBotCt Nabla nabla Id x -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703 modifyT $ \Nabla nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a b. (a -> b) -> a -> b $ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) addPhiCts Nabla nabla ([PhiCt] -> PhiCts forall a. [a] -> Bag a listToBag [PhiCt] 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@ pm_alt_con_app x (PmAltConLike (RealDataCon dc)) ex_tvs arg_ids -- Adds a literal constraint, i.e. @x ~ 42@. -- Also we assume that literal expressions won't diverge, so this -- will add a @x ~/ ⊥@ constraint. pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) () pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () pm_lit Id x PmLit lit = do (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m () modifyT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()) -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () forall a b. (a -> b) -> a -> b $ \Nabla nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotBotCt Nabla nabla Id x Id -> PmAltCon -> [Id] -> [Id] -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () pm_alt_con_app Id x (PmLit -> PmAltCon PmAltLit PmLit lit) [] [] -- Adds the given constructor application as a solution for @x@. pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) () pm_alt_con_app :: Id -> PmAltCon -> [Id] -> [Id] -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () pm_alt_con_app Id x PmAltCon con [Id] tvs [Id] args = (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m () modifyT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()) -> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) () forall a b. (a -> b) -> a -> b $ \Nabla nabla -> Nabla -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addConCt Nabla nabla Id x PmAltCon con [Id] tvs [Id] args -- | Like 'modify', but with an effectful modifier action modifyT :: Monad m => (s -> m s) -> StateT s m () modifyT :: forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m () modifyT s -> m s f = (s -> m ((), s)) -> StateT s m () forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a StateT ((s -> m ((), s)) -> StateT s m ()) -> (s -> m ((), s)) -> StateT s m () forall a b. (a -> b) -> a -> b $ (s -> ((), s)) -> m s -> m ((), s) forall a b. (a -> b) -> m a -> m b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ((,) ()) (m s -> m ((), s)) -> (s -> m s) -> s -> m ((), s) forall b c a. (b -> c) -> (a -> b) -> a -> c . s -> m s f -- | 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 (Id, Nabla) representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla) representCoreExpr nabla :: Nabla nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState nabla_tm_st = ts :: TmState ts@TmSt{ ts_reps :: TmState -> CoreMap Id ts_reps = CoreMap Id reps } } CoreExpr e | Just Id rep <- CoreMap Id -> CoreExpr -> Maybe Id forall a. CoreMap a -> CoreExpr -> Maybe a lookupCoreMap CoreMap Id reps CoreExpr key = (Id, Nabla) -> DsM (Id, Nabla) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Id rep, Nabla nabla) | Bool otherwise = do rep <- Type -> IOEnv (Env DsGblEnv DsLclEnv) Id mkPmId (HasDebugCallStack => CoreExpr -> Type CoreExpr -> Type exprType CoreExpr e) let reps' = CoreMap Id -> CoreExpr -> Id -> CoreMap Id forall a. CoreMap a -> CoreExpr -> a -> CoreMap a extendCoreMap CoreMap Id reps CoreExpr key Id rep let nabla' = Nabla nabla{ nabla_tm_st = ts{ ts_reps = reps' } } pure (rep, nabla') where key :: CoreExpr key = CoreExpr -> CoreExpr makeDictsCoherent CoreExpr e -- Use a key in which dictionaries for the same type become equal. -- See Note [Unique dictionaries in the TmOracle CoreMap] -- | Change out 'Id's which are uniquely determined by their type to a -- common value, so that different names for dictionaries of the same type -- are considered equal when building a 'CoreMap'. -- -- See Note [Unique dictionaries in the TmOracle CoreMap] makeDictsCoherent :: CoreExpr -> CoreExpr makeDictsCoherent :: CoreExpr -> CoreExpr makeDictsCoherent var :: CoreExpr var@(Var Id v) | let ty :: Type ty = Id -> Type idType Id v , Type -> Bool typeDeterminesValue Type ty = Type -> String -> CoreExpr mkImpossibleExpr Type ty String "Solver.makeDictsCoherent" | Bool otherwise = CoreExpr var makeDictsCoherent lit :: CoreExpr lit@(Lit {}) = CoreExpr lit makeDictsCoherent (App CoreExpr f CoreExpr a) = CoreExpr -> CoreExpr -> CoreExpr forall b. Expr b -> Expr b -> Expr b App (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr f) (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr a) makeDictsCoherent (Lam Id f CoreExpr body) = Id -> CoreExpr -> CoreExpr forall b. b -> Expr b -> Expr b Lam Id f (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr body) makeDictsCoherent (Let Bind Id bndr CoreExpr body) = Bind Id -> CoreExpr -> CoreExpr forall b. Bind b -> Expr b -> Expr b Let (Bind Id -> Bind Id go_bndr Bind Id bndr) (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr body) where go_bndr :: Bind Id -> Bind Id go_bndr (NonRec Id bndr CoreExpr expr) = Id -> CoreExpr -> Bind Id forall b. b -> Expr b -> Bind b NonRec Id bndr (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr expr) go_bndr (Rec [(Id, CoreExpr)] bndrs) = [(Id, CoreExpr)] -> Bind Id forall b. [(b, Expr b)] -> Bind b Rec (((Id, CoreExpr) -> (Id, CoreExpr)) -> [(Id, CoreExpr)] -> [(Id, CoreExpr)] forall a b. (a -> b) -> [a] -> [b] map ( \(Id b, CoreExpr expr) -> (Id b, CoreExpr -> CoreExpr makeDictsCoherent CoreExpr expr) ) [(Id, CoreExpr)] bndrs) makeDictsCoherent (Case CoreExpr scrut Id bndr Type ty [Alt Id] alts) = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr forall b. Expr b -> b -> Type -> [Alt b] -> Expr b Case CoreExpr scrut Id bndr Type ty [ AltCon -> [Id] -> CoreExpr -> Alt Id forall b. AltCon -> [b] -> Expr b -> Alt b Alt AltCon con [Id] bndr CoreExpr expr' | Alt AltCon con [Id] bndr CoreExpr expr <- [Alt Id] alts , let expr' :: CoreExpr expr' = CoreExpr -> CoreExpr makeDictsCoherent CoreExpr expr ] makeDictsCoherent (Cast CoreExpr expr Coercion co) = CoreExpr -> Coercion -> CoreExpr forall b. Expr b -> Coercion -> Expr b Cast (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr expr) Coercion co makeDictsCoherent (Tick CoreTickish tick CoreExpr expr) = CoreTickish -> CoreExpr -> CoreExpr forall b. CoreTickish -> Expr b -> Expr b Tick CoreTickish tick (CoreExpr -> CoreExpr makeDictsCoherent CoreExpr expr) makeDictsCoherent ty :: CoreExpr ty@(Type {}) = CoreExpr ty makeDictsCoherent co :: CoreExpr co@(Coercion {}) = CoreExpr co {- Note [Unique dictionaries in the TmOracle CoreMap] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Any two dictionaries for a coherent typeclass should be considered equal in the TmOracle CoreMap, as this allows us to report better pattern-match warnings. Consider for example T21662: view_fn :: forall (n :: Nat). KnownNat n => Int -> Bool foo :: Int -> Int foo (view_fn @12 -> True ) = 0 foo (view_fn @12 -> False) = 1 In this example, the pattern match is exhaustive because we have covered the range of the view pattern function. However, we may fail to recognise the fact that the two cases use the same view function if the KnownNat dictionaries aren't syntactically equal: eqn 1: [let ds_d1p0 = view_fn @12 $dKnownNat_a1ny ds_d1oR, True <- ds_d1p0] eqn 2: [let ds_d1p6 = view_fn @12 $dKnownNat_a1nC ds_d1oR, False <- ds_d1p6] Note that the uniques of the KnownNat 12 dictionary differ. If we fail to utilise the coherence of the KnownNat constraint, then we have to pessimistically assume that we have two function calls with different arguments: foo (fn arg1 -> True ) = ... foo (fn arg2 -> False) = ... In this case we can't determine whether the pattern matches are complete, so we emit a pattern match warning. Solution: replace all 'Id's whose type uniquely determines its value with a common value, e.g. in the above example we would replace both $dKnownNat_a1ny and $dKnownNat_a1nC with error @(KnownNat 12). Why did we choose this solution? Here are some alternatives that were considered: 1. Perform CSE first. This would common up the dictionaries before we compare using the CoreMap. However, this is architecturally difficult as it would require threading a CSEnv through to desugarPat. 2. Directly modify CoreMap so that any two dictionaries of the same type are considered equal. The problem is that this affects all users of CoreMap. For example, CSE would now assume that any two dictionaries of the same type are equal, but this isn't necessarily true in the presence of magicDict, which violates coherence by design. It seems more prudent to limit the changes to the pattern-match checker only, to avoid undesirable consequences. In the end, replacing dictionaries with an error value in the pattern-match checker was the most self-contained, although we might want to revisit once we implement a more robust approach to computing equality in the pattern-match checker (see #19272). -} {- 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 orthogonal. 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 [The 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: pattern P pattern Q case P 15 of Q _ -> ... P 15 -> Compared to the situation where P and Q are DataCons, the lack of generativity means we could never flag Q as redundant. (also see Note [Undecidable Equality for PmAltCons] in PmTypes.) On the other hand, if we fail to recognise the pattern synonym, we flag the pattern match as inexhaustive. That wouldn't happen if we had knowledge about the scrutinee, in which case the oracle basically 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 (but delayed checked) @≁⊥@ constraint to begin with. Hence, desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned by strict fields, since the forcing happens *before* pattern matching. And the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.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. We simply fail in 'addBotCt' for any binder of unlifted type. It would be enough to check for unliftedness once, when the binder comes into scope, but we haven't really a way to track that. 4. Why not start an 'emptyVarInfo' of unlifted type with @vi_bot = IsNotBot@? Because then we'd need to trigger an inhabitation test, because the var might actually be void to begin with. But we can't trigger the test from 'emptyVarInfo'. Historically, that is what we did and not doing the test led to #20631, where 'addNotBotCt' trivially succeeded, because the 'VarInfo' already said 'IsNotBot', implying that a prior inhabitation test succeeded. -} ------------------------- -- * 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 :: TyState -> TyState -> Bool tyStateRefined TyState a TyState b = TyState -> Int ty_st_n TyState a Int -> Int -> Bool forall a. Eq a => a -> a -> Bool /= TyState -> Int ty_st_n TyState b markDirty :: Id -> Nabla -> Nabla markDirty :: Id -> Nabla -> Nabla markDirty Id x nabla :: Nabla nabla@MkNabla{nabla_tm_st :: Nabla -> TmState nabla_tm_st = ts :: TmState ts@TmSt{ts_dirty :: TmState -> DIdSet ts_dirty = DIdSet dirty} } = Nabla nabla{ nabla_tm_st = ts{ ts_dirty = extendDVarSet dirty x } } traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState traverseDirty :: forall (m :: * -> *). Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState traverseDirty VarInfo -> m VarInfo f ts :: TmState ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo ts_facts = UniqSDFM Id VarInfo env, ts_dirty :: TmState -> DIdSet ts_dirty = DIdSet dirty} = [Id] -> UniqSDFM Id VarInfo -> m TmState go (DIdSet -> [Id] forall a. UniqDSet a -> [a] uniqDSetToList DIdSet dirty) UniqSDFM Id VarInfo env where go :: [Id] -> UniqSDFM Id VarInfo -> m TmState go [] UniqSDFM Id VarInfo env = TmState -> m TmState forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure TmState ts{ts_facts=env} go (Id x:[Id] xs) !UniqSDFM Id VarInfo env = do vi' <- VarInfo -> m VarInfo f (TmState -> Id -> VarInfo lookupVarInfo TmState ts Id x) go xs (addToUSDFM env x vi') traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState traverseAll :: forall (m :: * -> *). Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState traverseAll VarInfo -> m VarInfo f ts :: TmState ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo ts_facts = UniqSDFM Id VarInfo env} = do env' <- (VarInfo -> m VarInfo) -> UniqSDFM Id VarInfo -> m (UniqSDFM Id VarInfo) forall key a b (f :: * -> *). Applicative f => (a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b) traverseUSDFM VarInfo -> m VarInfo f UniqSDFM Id VarInfo 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 :: Int -> TyState -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla inhabitationTest Int 0 TyState _ Nabla nabla = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla inhabitationTest Int fuel TyState old_ty_st nabla :: Nabla nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState nabla_tm_st = TmState ts } = {-# SCC "inhabitationTest" #-} 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 TyState -> TyState -> Bool tyStateRefined TyState old_ty_st (Nabla -> TyState nabla_ty_st Nabla nabla) then (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo) -> TmState -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TmState forall (m :: * -> *). Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState traverseAll VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo test_one TmState ts else (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo) -> TmState -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TmState forall (m :: * -> *). Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState traverseDirty VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo test_one TmState ts pure nabla{ nabla_tm_st = ts'{ts_dirty=emptyDVarSet}} where nabla_not_dirty :: Nabla nabla_not_dirty = Nabla nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} } test_one :: VarInfo -> MaybeT DsM VarInfo test_one :: VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo test_one VarInfo vi = DsM Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (TyState -> Nabla -> VarInfo -> DsM Bool varNeedsTesting TyState old_ty_st Nabla nabla VarInfo vi) MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool -> (Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo forall a b. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a -> (a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= \case Bool True -> do -- lift $ tracePm "test_one" (ppr vi) -- No solution yet and needs testing -- We have to test with a Nabla where all dirty bits are cleared Int -> Nabla -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo instantiate (Int fuelInt -> Int -> Int forall a. Num a => a -> a -> a -Int 1) Nabla nabla_not_dirty VarInfo vi Bool _ -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure VarInfo vi -- | Checks whether the given 'VarInfo' needs to be tested for inhabitants. -- Returns `False` when we can skip the inhabitation test, presuming it would -- say "yes" anyway. See Note [Shortcutting the inhabitation test]. varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool varNeedsTesting TyState _ MkNabla{nabla_tm_st :: Nabla -> TmState nabla_tm_st=TmState tm_st} VarInfo vi | Id -> DIdSet -> Bool elemDVarSet (VarInfo -> Id vi_id VarInfo vi) (TmState -> DIdSet ts_dirty TmState tm_st) = Bool -> DsM Bool forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Bool True varNeedsTesting TyState _ Nabla _ VarInfo vi | [PmAltConApp] -> Bool forall (f :: * -> *) a. Foldable f => f a -> Bool notNull (VarInfo -> [PmAltConApp] vi_pos VarInfo vi) = Bool -> DsM Bool forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Bool False varNeedsTesting TyState old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState nabla_ty_st=TyState new_ty_st} VarInfo _ -- Same type state => still inhabited | Bool -> Bool not (TyState -> TyState -> Bool tyStateRefined TyState old_ty_st TyState new_ty_st) = Bool -> DsM Bool forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Bool False varNeedsTesting TyState old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState nabla_ty_st=TyState new_ty_st} VarInfo vi = do -- These normalisations are relatively expensive, but still better than having -- to perform a full inhabitation test (_, _, old_norm_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type) tntrGuts (TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)) -> DsM TopNormaliseTypeResult -> IOEnv (Env DsGblEnv DsLclEnv) (Type, [(Type, DataCon, Type)], Type) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> TyState -> Type -> DsM TopNormaliseTypeResult pmTopNormaliseType TyState old_ty_st (Id -> Type idType (Id -> Type) -> Id -> Type forall a b. (a -> b) -> a -> b $ VarInfo -> Id vi_id VarInfo 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 CompleteMatchs in vi_rcm. -- -- NB: Does /not/ filter each CompleteMatch with the oracle; members may -- remain that do not satisfy it. This lazy approach just -- avoids doing unnecessary work. instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo instantiate :: Int -> Nabla -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo instantiate Int fuel Nabla nabla VarInfo vi = {-# SCC "instantiate" #-} (Int -> Nabla -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo instBot Int fuel Nabla nabla VarInfo vi MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Alternative f => f a -> f a -> f a <|> Int -> Nabla -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo instCompleteSets Int fuel Nabla nabla VarInfo vi) -- | The \(⊢_{Bot}\) rule from the paper instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo instBot :: Int -> Nabla -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo instBot Int _fuel Nabla nabla VarInfo vi = {-# SCC "instBot" #-} do _nabla' <- Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addBotCt Nabla nabla (VarInfo -> Id vi_id VarInfo vi) pure vi addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla) addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla) addNormalisedTypeMatches nabla :: Nabla nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState nabla_ty_st = TyState ty_st } Id x = (VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)) -> Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla) forall (f :: * -> *) a. Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla) trvVarInfo VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo) add_matches Nabla nabla Id x where add_matches :: VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo) add_matches vi :: VarInfo vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches vi_rcm = ResidualCompleteMatches rcm } -- important common case, shaving down allocations of PmSeriesG by -5% | ResidualCompleteMatches -> Bool isRcmInitialised ResidualCompleteMatches rcm = (ResidualCompleteMatches, VarInfo) -> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (ResidualCompleteMatches rcm, VarInfo vi) add_matches vi :: VarInfo vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches vi_rcm = ResidualCompleteMatches rcm } = do norm_res_ty <- TyState -> Type -> DsM Type normaliseSourceTypeWHNF TyState ty_st (Id -> Type idType Id x) env <- dsGetFamInstEnvs rcm' <- case splitReprTyConApp_maybe env norm_res_ty of Just (TyCon rep_tc, ThetaType _args, Coercion _co) -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addTyConMatches TyCon rep_tc ResidualCompleteMatches rcm Maybe (TyCon, ThetaType, Coercion) Nothing -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addCompleteMatches ResidualCompleteMatches 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 :: FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion) splitReprTyConApp_maybe FamInstEnvs env Type ty = (TyCon -> ThetaType -> (TyCon, ThetaType, Coercion)) -> (TyCon, ThetaType) -> (TyCon, ThetaType, Coercion) forall a b c. (a -> b -> c) -> (a, b) -> c uncurry (FamInstEnvs -> TyCon -> ThetaType -> (TyCon, ThetaType, Coercion) tcLookupDataFamInst FamInstEnvs env) ((TyCon, ThetaType) -> (TyCon, ThetaType, Coercion)) -> Maybe (TyCon, ThetaType) -> Maybe (TyCon, ThetaType, Coercion) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> HasDebugCallStack => Type -> Maybe (TyCon, ThetaType) Type -> Maybe (TyCon, ThetaType) splitTyConApp_maybe Type 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 :: Int -> Nabla -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo instCompleteSets Int fuel Nabla nabla VarInfo vi = {-# SCC "instCompleteSets" #-} do let x :: Id x = VarInfo -> Id vi_id VarInfo vi (rcm, nabla) <- DsM (ResidualCompleteMatches, Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (ResidualCompleteMatches, Nabla) forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla) addNormalisedTypeMatches Nabla nabla Id x) nabla <- foldM (\Nabla nabla DsCompleteMatch cls -> Int -> Nabla -> Id -> DsCompleteMatch -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla instCompleteSet Int fuel Nabla nabla Id x DsCompleteMatch cls) nabla (getRcm rcm) pure (lookupVarInfo (nabla_tm_st nabla) x) anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool anyConLikeSolution ConLike -> Bool p = (PmAltConApp -> Bool) -> [PmAltConApp] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool any (PmAltCon -> Bool go (PmAltCon -> Bool) -> (PmAltConApp -> PmAltCon) -> PmAltConApp -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . PmAltConApp -> PmAltCon paca_con) where go :: PmAltCon -> Bool go (PmAltConLike ConLike cl) = ConLike -> Bool p ConLike cl go PmAltCon _ = Bool False -- | @instCompleteSet fuel nabla x 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 -> DsCompleteMatch -> MaybeT DsM Nabla instCompleteSet :: Int -> Nabla -> Id -> DsCompleteMatch -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla instCompleteSet Int fuel Nabla nabla Id x DsCompleteMatch cs | (ConLike -> Bool) -> [PmAltConApp] -> Bool anyConLikeSolution (ConLike -> UniqDSet ConLike -> Bool forall a. Uniquable a => a -> UniqDSet a -> Bool `elementOfUniqDSet` (DsCompleteMatch -> UniqDSet ConLike forall con. CompleteMatchX con -> UniqDSet con cmConLikes DsCompleteMatch cs)) (VarInfo -> [PmAltConApp] vi_pos VarInfo vi) -- No need to instantiate a constructor of this COMPLETE set if we already -- have a solution! = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla | Bool -> Bool not (Type -> DsCompleteMatch -> Bool forall con. Type -> CompleteMatchX con -> Bool completeMatchAppliesAtType (Id -> Type varType Id x) DsCompleteMatch cs) = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla | Bool otherwise = {-# SCC "instCompleteSet" #-} Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla go Nabla nabla (DsCompleteMatch -> [ConLike] sorted_candidates DsCompleteMatch cs) where vi :: VarInfo vi = TmState -> Id -> VarInfo lookupVarInfo (Nabla -> TmState nabla_tm_st Nabla nabla) Id x sorted_candidates :: DsCompleteMatch -> [ConLike] sorted_candidates :: DsCompleteMatch -> [ConLike] sorted_candidates DsCompleteMatch cm -- 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). | UniqDSet ConLike -> Int forall a. UniqDSet a -> Int sizeUniqDSet UniqDSet ConLike cs Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int 5 = (ConLike -> ConLike -> Ordering) -> [ConLike] -> [ConLike] forall a. (a -> a -> Ordering) -> [a] -> [a] sortBy ConLike -> ConLike -> Ordering compareConLikeTestability (UniqDSet ConLike -> [ConLike] forall a. UniqDSet a -> [a] uniqDSetToList UniqDSet ConLike cs) | Bool otherwise = UniqDSet ConLike -> [ConLike] forall a. UniqDSet a -> [a] uniqDSetToList UniqDSet ConLike cs where cs :: UniqDSet ConLike cs = DsCompleteMatch -> UniqDSet ConLike forall con. CompleteMatchX con -> UniqDSet con cmConLikes DsCompleteMatch cm go :: Nabla -> [ConLike] -> MaybeT DsM Nabla go :: Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla go Nabla _ [] = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (m :: * -> *) a. MonadPlus m => m a mzero go Nabla nabla (RealDataCon DataCon dc:[ConLike] _) -- 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. | DataCon -> Bool isDataConTriviallyInhabited DataCon dc = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nabla nabla go Nabla nabla (ConLike con:[ConLike] cons) = do let x :: Id x = VarInfo -> Id vi_id VarInfo vi let recur_not_con :: MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla recur_not_con = do nabla' <- Nabla -> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla addNotConCt Nabla nabla Id x (ConLike -> PmAltCon PmAltConLike ConLike con) go nabla' cons (Nabla nabla Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a b. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a b. Functor f => a -> f b -> f a <$ Int -> Nabla -> Id -> ConLike -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla instCon Int fuel Nabla nabla Id x ConLike con) -- return the original nabla, not the -- refined one! MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Alternative f => f a -> f a -> f a <|> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla 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 :: DataCon -> Bool isDataConTriviallyInhabited DataCon dc | TyCon -> Bool isTyConTriviallyInhabited (DataCon -> TyCon dataConTyCon DataCon dc) = Bool True isDataConTriviallyInhabited DataCon dc = ThetaType -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null (DataCon -> ThetaType dataConTheta DataCon dc) Bool -> Bool -> Bool && -- (1) [HsImplBang] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null (DataCon -> [HsImplBang] dataConImplBangs DataCon dc) Bool -> Bool -> Bool && -- (2) ThetaType -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null (DataCon -> ThetaType dataConMightBeUnliftedFieldTys DataCon dc) -- (3) dataConMightBeUnliftedFieldTys :: DataCon -> [Type] dataConMightBeUnliftedFieldTys :: DataCon -> ThetaType dataConMightBeUnliftedFieldTys = (Type -> Bool) -> ThetaType -> ThetaType forall a. (a -> Bool) -> [a] -> [a] filter Type -> Bool mightBeUnliftedType (ThetaType -> ThetaType) -> (DataCon -> ThetaType) -> DataCon -> ThetaType forall b c a. (b -> c) -> (a -> b) -> a -> c . (Scaled Type -> Type) -> [Scaled Type] -> ThetaType forall a b. (a -> b) -> [a] -> [b] map Scaled Type -> Type forall a. Scaled a -> a scaledThing ([Scaled Type] -> ThetaType) -> (DataCon -> [Scaled Type]) -> DataCon -> ThetaType forall b c a. (b -> c) -> (a -> b) -> a -> c . DataCon -> [Scaled Type] dataConOrigArgTys isTyConTriviallyInhabited :: TyCon -> Bool isTyConTriviallyInhabited :: TyCon -> Bool isTyConTriviallyInhabited TyCon tc = Unique -> UniqueSet -> Bool memberUniqueSet (TyCon -> Unique forall a. Uniquable a => a -> Unique getUnique TyCon tc) UniqueSet triviallyInhabitedTyConKeys -- | All these types are trivially inhabited triviallyInhabitedTyConKeys :: UniqueSet triviallyInhabitedTyConKeys :: UniqueSet triviallyInhabitedTyConKeys = [Unique] -> UniqueSet fromListUniqueSet [ Unique charTyConKey, Unique doubleTyConKey, Unique floatTyConKey, Unique intTyConKey, Unique int8TyConKey, Unique int16TyConKey, Unique int32TyConKey, Unique int64TyConKey, Unique intPrimTyConKey, Unique int8PrimTyConKey, Unique int16PrimTyConKey, Unique int32PrimTyConKey, Unique int64PrimTyConKey, Unique wordTyConKey, Unique word8TyConKey, Unique word16TyConKey, Unique word32TyConKey, Unique word64TyConKey, Unique wordPrimTyConKey, Unique word8PrimTyConKey, Unique word16PrimTyConKey, Unique word32PrimTyConKey, Unique word64PrimTyConKey, Unique trTyConTyConKey ] 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 inhabited by instantiating only a single DataCon. compareConLikeTestability :: ConLike -> ConLike -> Ordering compareConLikeTestability PatSynCon{} ConLike _ = Ordering GT compareConLikeTestability ConLike _ PatSynCon{} = Ordering GT compareConLikeTestability (RealDataCon DataCon a) (RealDataCon DataCon b) = [DataCon -> DataCon -> Ordering] -> DataCon -> DataCon -> Ordering forall a. Monoid a => [a] -> a mconcat -- Thetas are most expensive to check, as they might incur a whole new round -- of inhabitation testing [ (DataCon -> Int) -> DataCon -> DataCon -> Ordering forall a b. Ord a => (b -> a) -> b -> b -> Ordering comparing (ThetaType -> Int forall a. [a] -> Int fast_length (ThetaType -> Int) -> (DataCon -> ThetaType) -> DataCon -> Int forall b c a. (b -> c) -> (a -> b) -> a -> c . DataCon -> ThetaType dataConTheta) -- Unlifted or strict fields only incur an inhabitation test for that -- particular field. Still something to avoid. , (DataCon -> Int) -> DataCon -> DataCon -> Ordering forall a b. Ord a => (b -> a) -> b -> b -> Ordering comparing DataCon -> Int unlifted_or_strict_fields ] DataCon a DataCon b where fast_length :: [a] -> Int fast_length :: forall a. [a] -> Int fast_length [a] xs = ([a] -> Int) -> Int -> [a] -> Int -> Int forall a b. ([a] -> b) -> b -> [a] -> Int -> b atLength [a] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length Int 6 [a] xs Int 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 :: DataCon -> Int unlifted_or_strict_fields DataCon dc = [HsImplBang] -> Int forall a. [a] -> Int fast_length (DataCon -> [HsImplBang] dataConImplBangs DataCon dc) Int -> Int -> Int forall a. Num a => a -> a -> a + ThetaType -> Int forall a. [a] -> Int fast_length (DataCon -> ThetaType dataConMightBeUnliftedFieldTys DataCon dc) -- | @instCon fuel nabla (x::match_ty) K@ tries to instantiate @x@ to @K@ by -- adding the proper constructor constraint. -- -- See Note [Instantiating a ConLike]. instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla instCon Int fuel nabla :: Nabla nabla@MkNabla{nabla_ty_st :: Nabla -> TyState nabla_ty_st = TyState ty_st} Id x ConLike con = {-# SCC "instCon" #-} IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla) -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla forall a b. (a -> b) -> a -> b $ do let hdr :: String -> String hdr String what = String "instCon " String -> String -> String forall a. [a] -> [a] -> [a] ++ Int -> String forall a. Show a => a -> String show Int fuel String -> String -> String forall a. [a] -> [a] -> [a] ++ String " " String -> String -> String forall a. [a] -> [a] -> [a] ++ String what env <- DsM FamInstEnvs dsGetFamInstEnvs let match_ty = Id -> Type idType Id x tracePm (hdr "{") $ ppr con <+> text "... <-" <+> ppr x <+> dcolon <+> ppr match_ty norm_match_ty <- normaliseSourceTypeWHNF ty_st match_ty mb_sigma_univ <- matchConLikeResTy env ty_st norm_match_ty con case mb_sigma_univ of Just Subst sigma_univ -> do let ([Id] _univ_tvs, [Id] ex_tvs, [EqSpec] eq_spec, ThetaType thetas, ThetaType _req_theta, [Scaled Type] field_tys, Type _con_res_ty) = ConLike -> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type], Type) conLikeFullSig ConLike con -- Following Note [Instantiating a ConLike]: -- (1) _req_theta has been tested in 'matchConLikeResTy' -- (2) Instantiate fresh existentials (sigma_ex, _) <- Subst -> [Id] -> UniqSupply -> (Subst, [Id]) cloneTyVarBndrs Subst sigma_univ [Id] ex_tvs (UniqSupply -> (Subst, [Id])) -> DsM UniqSupply -> IOEnv (Env DsGblEnv DsLclEnv) (Subst, [Id]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> DsM UniqSupply forall (m :: * -> *). MonadUnique m => m UniqSupply getUniqueSupplyM -- (3) Substitute provided constraints bound by the constructor. -- These are added to the type oracle as new facts (in a moment) let gammas = HasDebugCallStack => Subst -> ThetaType -> ThetaType Subst -> ThetaType -> ThetaType substTheta Subst sigma_ex ([EqSpec] -> ThetaType eqSpecPreds [EqSpec] eq_spec ThetaType -> ThetaType -> ThetaType forall a. [a] -> [a] -> [a] ++ ThetaType thetas) -- (4) Instantiate fresh term variables as arguments to the constructor let field_tys' = HasDebugCallStack => Subst -> ThetaType -> ThetaType Subst -> ThetaType -> ThetaType substTys Subst sigma_ex (ThetaType -> ThetaType) -> ThetaType -> ThetaType forall a b. (a -> b) -> a -> b $ (Scaled Type -> Type) -> [Scaled Type] -> ThetaType forall a b. (a -> b) -> [a] -> [b] map Scaled Type -> Type forall a. Scaled a -> a scaledThing [Scaled Type] field_tys arg_ids <- mapM mkPmId field_tys' tracePm (hdr "(cts)") $ vcat [ ppr x <+> dcolon <+> ppr match_ty , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty , ppr (map (\Id tv -> Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id tv SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Char -> SDoc forall doc. IsLine doc => Char -> doc char Char '↦' SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Subst -> Id -> Type substTyVar Subst sigma_univ Id tv)) _univ_tvs) , ppr gammas , ppr (map (\Id x -> Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> SDoc dcolon SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Id -> Type idType Id x)) arg_ids) ] -- (5) Finally add the new constructor constraint runMaybeT $ do -- Case (2) of Note [Strict fields and variables of unlifted type] let alt = ConLike -> PmAltCon PmAltConLike ConLike con let branching_factor = [Id] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length ([Id] -> Int) -> [Id] -> Int forall a b. (a -> b) -> a -> b $ PmAltCon -> [Id] -> [Id] filterUnliftedFields PmAltCon alt [Id] arg_ids let ct = Id -> PmAltCon -> [Id] -> ThetaType -> [Id] -> PhiCt PhiConCt Id x PmAltCon alt [Id] ex_tvs ThetaType gammas [Id] arg_ids nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $ addPhiTmCt nabla ct -- See Note [Fuel for the inhabitation test] let new_fuel | Int branching_factor Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int 1 = Int fuel | Bool otherwise = Int -> Int -> Int forall a. Ord a => a -> a -> a min Int fuel Int 2 lift $ tracePm (hdr "(ct satisfiable)") $ vcat [ ppr ct , ppr x <+> dcolon <+> ppr match_ty , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty , ppr (map (\Id tv -> Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id tv SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Char -> SDoc forall doc. IsLine doc => Char -> doc char Char '↦' SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Subst -> Id -> Type substTyVar Subst sigma_univ Id tv)) _univ_tvs) , ppr gammas , ppr (map (\Id x -> Id -> SDoc forall a. Outputable a => a -> SDoc ppr Id x SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> SDoc dcolon SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Id -> Type idType Id x)) arg_ids) , ppr branching_factor , ppr new_fuel ] nabla2 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla1) $ inhabitationTest new_fuel (nabla_ty_st nabla) nabla1 lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla2) pure nabla2 Maybe Subst Nothing -> do String -> SDoc -> DsM () tracePm (String -> String hdr String "(match_ty not instance of res_ty) }") SDoc forall doc. IsOutput doc => doc empty Maybe Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Nabla -> Maybe Nabla forall a. a -> Maybe a Just Nabla nabla) -- Matching against match_ty failed. Inhabited! -- See Note [Instantiating a ConLike]. -- | @matchConLikeResTy _ _ ty K@ tries to match @ty@ against the result -- type of @K@, @res_ty@. It returns a substitution @s@ for @K@'s universal -- tyvars such that @s(res_ty)@ equals @ty@ if successful. -- -- Make sure that @ty@ is normalised before. -- -- See Note [Matching against a ConLike result type]. matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe Subst) matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe Subst) matchConLikeResTy FamInstEnvs env TyState _ Type ty (RealDataCon DataCon dc) = Maybe Subst -> DsM (Maybe Subst) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Maybe Subst -> DsM (Maybe Subst)) -> Maybe Subst -> DsM (Maybe Subst) forall a b. (a -> b) -> a -> b $ do (rep_tc, tc_args, _co) <- FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion) splitReprTyConApp_maybe FamInstEnvs env Type ty if rep_tc == dataConTyCon dc then Just (zipTCvSubst (dataConUnivTyVars dc) tc_args) else Nothing matchConLikeResTy FamInstEnvs _ (TySt Int _ InertSet inert) Type ty (PatSynCon PatSyn ps) = {-# SCC "matchConLikeResTy" #-} MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst) forall (m :: * -> *) a. MaybeT m a -> m (Maybe a) runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst)) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst) forall a b. (a -> b) -> a -> b $ do let ([Id] univ_tvs,ThetaType req_theta,[Id] _,ThetaType _,[Scaled Type] _,Type con_res_ty) = PatSyn -> ([Id], ThetaType, [Id], ThetaType, [Scaled Type], Type) patSynSig PatSyn ps subst <- DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a MaybeT (DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst) -> DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst forall a b. (a -> b) -> a -> b $ Maybe Subst -> DsM (Maybe Subst) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Maybe Subst -> DsM (Maybe Subst)) -> Maybe Subst -> DsM (Maybe Subst) forall a b. (a -> b) -> a -> b $ Type -> Type -> Maybe Subst tcMatchTy Type con_res_ty Type ty guard $ all (`elemSubst` subst) univ_tvs -- See the Note about T11336b if null req_theta then pure subst else do let req_theta' = HasDebugCallStack => Subst -> ThetaType -> ThetaType Subst -> ThetaType -> ThetaType substTys Subst subst ThetaType req_theta satisfiable <- lift $ initTcDsForSolver $ tcCheckWanteds inert req_theta' if satisfiable then pure subst else mzero {- Note [Soundness and Completeness] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Soundness and completeness of the pattern-match checker depend entirely on the soundness and completeness of the inhabitation test. Achieving both soundness and completeness at the same time is undecidable. See also T17977 and Note [Fuel for the inhabitation test]. Losing soundness would make the algorithm pointless; hence we give up on completeness, but try to get as close as possible (how close is called the 'precision' of the algorithm). Soundness means that you 1. Can remove clauses flagged as redundant without changing program semantics (no false positives). 2. Can be sure that your program is free of incomplete pattern matches when the checker doesn't flag any inexhaustive definitions (no false negatives). A complete algorithm would mean that 1. When a clause can be deleted without changing program semantics, it will be flagged as redundant (no false negatives). 2. A program that is free of incomplete pattern matches will never have a definition be flagged as inexhaustive (no false positives). Via the LYG algorithm, we reduce both these properties to a property on the inhabitation test of refinement types: *Soundness*: If the inhabitation test says "no" for a given refinement type Nabla, then it provably has no inhabitant. *Completeness*: If the inhabitation test says "yes" for a given refinement type Nabla, then it provably has an inhabitant. Our test is sound, but incomplete, so there are instances where we say "yes" but in fact the Nabla is empty. Which entails false positive exhaustivity and false negative redundancy warnings, as above. In summary, we have the following correspondence: Property | Exhaustiveness warnings | Redundancy warnings | Inhabitation test | -------------|-------------------------|---------------------|-------------------| Soundness | No false negatives | No false positives | Only says "no" | | | | if there is no | | | | inhabitant | Completeness | No false positives | No false negatives | Only says "yes" | | | | if there is an | | | | inhabitant | Note [Shortcutting the inhabitation test] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Generally, we have to re-test a refinement type for inhabitants whenever we add a new constraint. Often, we can say "no" early, upon trying to add a contradicting constraint, see Note [The Pos/Neg invariant]. Still, COMPLETE sets and type evidence are best handled in a delayed fashion, because of the recursive nature of the test and our fuel-based approach. But even then there are some cases in which we can skip the full test, because we are sure that the refinement type is still inhabited. These conditions are monitored by 'varNeedsTesting'. It returns - `True` whenever a full inhabitation test is needed - `False` whenever the test can be skipped, amounting to an inhabitation test that says "yes". According to Note [Soundness and Completeness], this test will never compromise soundness: The `True` case just forwards to the actual inhabitation test and the `False` case amounts to an inhabitation test that is trivially sound, because it never says "no". Of course, if the returns says `False`, Completeness (and thus Precision) of the algorithm is affected, but we get to skip costly inhabitation tests. We try to trade as little Precision as possible against as much Performance as possible. Here are the tests, in order: 1. If a variable is dirty (because of a newly added negative term constraint), we have to test. 2. If a variable has positive information, we don't have to test: The positive information acts as constructive proof for inhabitation. 3. If the type state didn't change, there is no need to test. 4. If the variable's normalised type didn't change, there is no need to test. 5. Otherwise, we have to test. Why (1) before (2)? ------------------- Consider the reverse for (T18960): pattern P x = x {-# COMPLETE P :: () #-} foo = case () of x@(P _) -> () This should be exhaustive. But if we say "We know `x` has solution `()`, so it's inhabited", then we'll get a warning saying that `()` wasn't matched. But the match on `P` added the new negative information to the uncovered set, in the process of which we marked `x` as dirty. By giving the dirty flag a higher priority than positive info, we get to test again and see that `x` is uninhabited and the match is exhaustive. But suppose that `P` wasn't mentioned in any COMPLETE set. Then we simply don't mark `x` as dirty and will emit a warning again (which we would anyway), without running a superfluous inhabitation test. That speeds up T17836 considerably. Why (2) before (3) and (4)? --------------------------- Simply because (2) is more efficient to test than (3) (not by a lot), which is more efficient to test than (4), which is still more efficient than running the full inhabitation test (5). Note [Fuel for the inhabitation test] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Whether or not a type is inhabited is undecidable in general, see also Note [Soundness and Completeness]. 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 on 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 inhabitation 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. Note [Matching against a ConLike result type] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given a ConLike > C :: forall us. R => ... -> res_ty is a pattern `C ...` compatible with the type `ty`? Clearly that is the case if `res_ty` /subsumes/ `ty` and the required constraints `R` (strictly a feature of pattern synonyms) are satisfiable. In that case, 'matchConLikeResTy' returns a substitution σ over `us` such that `σ(res_ty) == ty`. It's surprisingly tricky to implement correctly, and works quite different for DataCons and PatSynCons: * For data cons, we look at `ty` and see if it's a TyCon app `T t1 ... tn`. If that is the case, we make sure that `C` is a DataCon of `T` and return a substitution mapping `C`'s universal tyvars `us` to `t1`...`tn`. Wrinkle: Since `T` might be a data family TyCon, we have to look up its representation TyCon before we compare to `C`'s TyCon. So we use 'splitReprTyConApp_maybe' instead of 'splitTyConApp_maybe'. * For pattern synonyms, we directly match `ty` against `res_ty` to get the substitution σ. See Note [Pattern synonym result type] in "GHC.Core.PatSyn". Fortunately, we don't have to treat data family TyCons specially: Pattern synonyms /never/ apply to a data family representation TyCon. We do have to consider the required constraints `σ(R)`, though, as we have seen in #19475. That is done by solving them as Wanted constraints given the inert set of the current type state (which is part of a Nabla's TySt). Since spinning up a constraint solver session is costly, we only do so in the rare cases that a pattern synonym actually carries any required constraints. We can get into the strange situation that not all universal type variables `us` occur in `res_ty`. Example from T11336b: instance C Proxy where ... -- impl uninteresting pattern P :: forall f a. C f => f a -> Proxy a -- impl uninteresting fun :: Proxy a -> () fun (P Proxy) = () fun (P Proxy) = () -- ideally detected as redundant `f` is a universal type variable and `C f` the required constraint of pattern synonym `P`. But `f` doesn't occur in the result type `Proxy a` of `P`, so σ will not even have `f` in its in-scope set. It's a bit unclear what to do here; we might want to freshen `f` to `f'` and see if we can solve `C f'` as a Wanted constraint, which we most likely can't. Hence, we simply skip the freshening and declare the match as failed when there is a variable like `f`. For the definition of `fun`, that means we will not remember that we matched on `P` and thus will not detect its second clause as redundant. See Note [Pattern synonym result type] in "GHC.Core.PatSyn" for similar oddities. Note [Instantiating a ConLike] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ `instCon` implements the \(Inst\) function from Figure 8 of the LYG paper. Given the following type of ConLike `K` > K :: forall us. R => forall es. P => t1 -> ... -> tn -> res_ty and a variable `x::match_ty`, it tries to find an instantiation `K ex_tvs gammas arg_ids :: match_ty` (for fresh `arg_ids`) and ultimately adds a constructor constraint `K ex_tvs gammas arg_ids <- x` to the given Nabla. As a first step, it tries (via 'matchConLikeResTy') to match `match_ty` against `res_ty` and checks that that the required constraints @R@ are satisfiable. See Note [Matching against a ConLike result type]. If matching /fails/, it trivially (and conservatively) reports "inhabited" by returning the unrefined input Nabla. After all, the match might have failed due to incomplete type information in Nabla. (Later type refinement from unpacking GADT constructors might monomorphise `match_ty` so much that `res_ty` ultimately subsumes it.) If matching /succeeds/, we get a substitution σ for the (universal) tyvars `us`. After applying σ, we get > K @σ(us) :: σ(R) => forall σ(es). σ(P) => σ(t1) -> ... -> σ(tn) -> match_ty The existentials `es` might still occur in argument types `σ(tn)`, though. Now 'instCon' performs the following steps: 1. It drops the required constraints `σ(R)`, as they have already been discharged by 'matchConLikeResTy'. 2. It instantiates fresh binders `es'` for the other type variables `es` bound by `K` and adds the mapping to σ to get σ', so that we have > K @σ(us) @es' :: σ'(P) => σ'(t1) -> ... -> σ'(tn) -> match_ty 3. It adds new type constraints from the substituted provided constraints @σ'(P)@. 4. It substitutes and conjures new binders @arg_ids@ for the argument types @σ'(t1) ... σ'(tn)@. 5. It adds a term constraint @K es' σ'(P) arg_ids <- x@, which handles the details regarding type constraints and unlifted fields. And finally the extended 'Nabla' is returned if all the constraints were compatible. -} -------------------------------------- -- * 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. -- | See Note [Case split inhabiting patterns] data GenerateInhabitingPatternsMode = CaseSplitTopLevel | MinimalCover deriving (GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool (GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool) -> (GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool) -> Eq GenerateInhabitingPatternsMode forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool == :: GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool $c/= :: GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool /= :: GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool Eq, Int -> GenerateInhabitingPatternsMode -> String -> String [GenerateInhabitingPatternsMode] -> String -> String GenerateInhabitingPatternsMode -> String (Int -> GenerateInhabitingPatternsMode -> String -> String) -> (GenerateInhabitingPatternsMode -> String) -> ([GenerateInhabitingPatternsMode] -> String -> String) -> Show GenerateInhabitingPatternsMode forall a. (Int -> a -> String -> String) -> (a -> String) -> ([a] -> String -> String) -> Show a $cshowsPrec :: Int -> GenerateInhabitingPatternsMode -> String -> String showsPrec :: Int -> GenerateInhabitingPatternsMode -> String -> String $cshow :: GenerateInhabitingPatternsMode -> String show :: GenerateInhabitingPatternsMode -> String $cshowList :: [GenerateInhabitingPatternsMode] -> String -> String showList :: [GenerateInhabitingPatternsMode] -> String -> String Show) instance Outputable GenerateInhabitingPatternsMode where ppr :: GenerateInhabitingPatternsMode -> SDoc ppr = String -> SDoc forall doc. IsLine doc => String -> doc text (String -> SDoc) -> (GenerateInhabitingPatternsMode -> String) -> GenerateInhabitingPatternsMode -> SDoc forall b c a. (b -> c) -> (a -> b) -> a -> c . GenerateInhabitingPatternsMode -> String forall a. Show a => a -> String show -- | @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 :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] -- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns] generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode _ [Id] _ Int 0 Nabla _ = [Nabla] -> DsM [Nabla] forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure [] generateInhabitingPatterns GenerateInhabitingPatternsMode _ [] Int _ Nabla nabla = [Nabla] -> DsM [Nabla] forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure [Nabla nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode (Id x:[Id] xs) Int n Nabla nabla = do String -> SDoc -> DsM () tracePm String "generateInhabitingPatterns" (GenerateInhabitingPatternsMode -> SDoc forall a. Outputable a => a -> SDoc ppr GenerateInhabitingPatternsMode mode SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Int -> SDoc forall a. Outputable a => a -> SDoc ppr Int n SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [Id] -> SDoc forall a. Outputable a => a -> SDoc ppr (Id xId -> [Id] -> [Id] forall a. a -> [a] -> [a] :[Id] xs) SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ Nabla -> SDoc forall a. Outputable a => a -> SDoc ppr Nabla nabla) let VI Id _ [PmAltConApp] pos PmAltConSet neg BotInfo _ ResidualCompleteMatches _ = TmState -> Id -> VarInfo lookupVarInfo (Nabla -> TmState nabla_tm_st Nabla nabla) Id x case [PmAltConApp] pos of PmAltConApp _:[PmAltConApp] _ -> do -- Example for multiple solutions (must involve a PatSyn): -- f x@(Just _) True | SomePatSyn _ <- x = ... -- within the RHS, we know that -- * @x ~ Just y@ for some @y@ -- * @x ~ SomePatSyn z@ for some @z@ -- and both conditions have to hold /at the same time/. Hence we must -- find evidence for @y@ and @z@ that is valid at the same time. These -- constitute arg_vas below. let arg_vas :: [Id] arg_vas = (PmAltConApp -> [Id]) -> [PmAltConApp] -> [Id] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap PmAltConApp -> [Id] paca_ids [PmAltConApp] pos GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode ([Id] arg_vas [Id] -> [Id] -> [Id] forall a. [a] -> [a] -> [a] ++ [Id] xs) Int n Nabla nabla [] -- When there are literals involved, just print negative info -- instead of listing missed constructors | [PmLit] -> Bool forall (f :: * -> *) a. Foldable f => f a -> Bool notNull [ PmLit l | PmAltLit PmLit l <- PmAltConSet -> [PmAltCon] pmAltConSetElems PmAltConSet neg ] -> GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode [Id] xs Int n Nabla nabla -- When some constructors are impossible or when we don't care for a -- minimal cover (Note [Case split inhabiting patterns]), do a case split. | Bool -> Bool not (PmAltConSet -> Bool isEmptyPmAltConSet PmAltConSet neg) Bool -> Bool -> Bool || GenerateInhabitingPatternsMode mode GenerateInhabitingPatternsMode -> GenerateInhabitingPatternsMode -> Bool forall a. Eq a => a -> a -> Bool == GenerateInhabitingPatternsMode CaseSplitTopLevel -> Id -> [Id] -> Int -> Nabla -> DsM [Nabla] try_instantiate Id x [Id] xs Int n Nabla nabla -- Else don't do a case split on this var, just print a wildcard. -- But try splitting for the remaining vars, of course | Bool otherwise -> GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode [Id] xs Int n Nabla 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 :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla] try_instantiate Id x [Id] xs Int n Nabla nabla = do (_src_ty, dcs, rep_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type) tntrGuts (TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)) -> DsM TopNormaliseTypeResult -> IOEnv (Env DsGblEnv DsLclEnv) (Type, [(Type, DataCon, Type)], Type) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> TyState -> Type -> DsM TopNormaliseTypeResult pmTopNormaliseType (Nabla -> TyState nabla_ty_st Nabla nabla) (Id -> Type idType Id x) mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs case mb_stuff of Maybe (Id, Nabla) Nothing -> [Nabla] -> DsM [Nabla] forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure [] Just (Id y, Nabla newty_nabla) -> do let vi :: VarInfo vi = TmState -> Id -> VarInfo lookupVarInfo (Nabla -> TmState nabla_tm_st Nabla newty_nabla) Id y env <- DsM FamInstEnvs dsGetFamInstEnvs rcm <- case splitReprTyConApp_maybe env rep_ty of Just (TyCon tc, ThetaType _, Coercion _) -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addTyConMatches TyCon tc (VarInfo -> ResidualCompleteMatches vi_rcm VarInfo vi) Maybe (TyCon, ThetaType, Coercion) Nothing -> ResidualCompleteMatches -> DsM ResidualCompleteMatches addCompleteMatches (VarInfo -> ResidualCompleteMatches vi_rcm VarInfo vi) -- Test all COMPLETE sets for inhabitants (n inhs at max). Take care of ⊥. clss <- pickApplicableCompleteSets (nabla_ty_st nabla) rep_ty rcm case NE.nonEmpty (uniqDSetToList . cmConLikes <$> clss) of Maybe (NonEmpty [ConLike]) Nothing -> -- No COMPLETE sets ==> inhabited GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode [Id] xs Int n Nabla newty_nabla Just NonEmpty [ConLike] clss -> do -- Try each COMPLETE set. nablass' <- NonEmpty [ConLike] -> ([ConLike] -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)]) -> IOEnv (Env DsGblEnv DsLclEnv) (NonEmpty [(Maybe ConLike, Nabla)]) forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => t a -> (a -> m b) -> m (t b) forM NonEmpty [ConLike] clss (Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)] instantiate_cons Id y Type rep_ty [Id] xs Int n Nabla newty_nabla) if any null nablass' && vi_bot vi /= IsNotBot then generateInhabitingPatterns mode xs n newty_nabla -- bot is still possible. Display a wildcard! else do -- Pick the residual COMPLETE set with the smallest cost (see 'completeSetCost'). -- See Note [Prefer in-scope COMPLETE matches]. DsGblEnv { ds_gbl_rdr_env = rdr_env } <- getGblEnv let bestSet = ((Maybe ConLike, Nabla) -> Nabla) -> [(Maybe ConLike, Nabla)] -> [Nabla] forall a b. (a -> b) -> [a] -> [b] map (Maybe ConLike, Nabla) -> Nabla forall a b. (a, b) -> b snd ([(Maybe ConLike, Nabla)] -> [Nabla]) -> [(Maybe ConLike, Nabla)] -> [Nabla] forall a b. (a -> b) -> a -> b $ ([(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] -> Ordering) -> NonEmpty [(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] forall (t :: * -> *) a. Foldable t => (a -> a -> Ordering) -> t a -> a minimumBy (([(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int)) -> [(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] -> Ordering forall a b. Ord a => (b -> a) -> b -> b -> Ordering comparing (([(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int)) -> [(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] -> Ordering) -> ([(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int)) -> [(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] -> Ordering forall a b. (a -> b) -> a -> b $ GlobalRdrEnv -> [(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int) forall a. GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int) completeSetCost GlobalRdrEnv rdr_env) NonEmpty [(Maybe ConLike, Nabla)] nablass' pure bestSet -- 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 :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla) instantiate_newtype_chain Id x Nabla nabla [] = (Id, Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla) forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a forall (f :: * -> *) a. Applicative f => a -> f a pure (Id x, Nabla nabla) instantiate_newtype_chain Id x Nabla nabla ((Type _ty, DataCon dc, Type arg_ty):[(Type, DataCon, Type)] dcs) = do y <- IOEnv (Env DsGblEnv DsLclEnv) Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id forall (m :: * -> *) a. Monad m => m a -> MaybeT m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (IOEnv (Env DsGblEnv DsLclEnv) Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id) -> IOEnv (Env DsGblEnv DsLclEnv) Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id forall a b. (a -> b) -> a -> b $ Type -> IOEnv (Env DsGblEnv DsLclEnv) Id mkPmId Type 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 [(Maybe ConLike, Nabla)] instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)] instantiate_cons Id _ Type _ [Id] _ Int _ Nabla _ [] = [(Maybe ConLike, Nabla)] -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)] forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure [] instantiate_cons Id _ Type _ [Id] _ Int 0 Nabla _ [ConLike] _ = [(Maybe ConLike, Nabla)] -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)] forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure [] instantiate_cons Id _ Type ty [Id] xs Int n Nabla nabla [ConLike] _ -- We don't want to expose users to GHC-specific constructors for Int etc. | ((TyCon, ThetaType) -> Bool) -> Maybe (TyCon, ThetaType) -> Maybe Bool forall a b. (a -> b) -> Maybe a -> Maybe b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (TyCon -> Bool isTyConTriviallyInhabited (TyCon -> Bool) -> ((TyCon, ThetaType) -> TyCon) -> (TyCon, ThetaType) -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (TyCon, ThetaType) -> TyCon forall a b. (a, b) -> a fst) (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType) Type -> Maybe (TyCon, ThetaType) splitTyConApp_maybe Type ty) Maybe Bool -> Maybe Bool -> Bool forall a. Eq a => a -> a -> Bool == Bool -> Maybe Bool forall a. a -> Maybe a Just Bool True = (Nabla -> (Maybe ConLike, Nabla)) -> [Nabla] -> [(Maybe ConLike, Nabla)] forall a b. (a -> b) -> [a] -> [b] map (Maybe ConLike forall a. Maybe a Nothing,) ([Nabla] -> [(Maybe ConLike, Nabla)]) -> DsM [Nabla] -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode [Id] xs Int n Nabla nabla instantiate_cons Id x Type ty [Id] xs Int n Nabla nabla (ConLike cl:[ConLike] cls) = do -- The following line is where we call out to the inhabitationTest! mb_nabla <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) forall (m :: * -> *) a. MaybeT m a -> m (Maybe a) runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla) forall a b. (a -> b) -> a -> b $ Int -> Nabla -> Id -> ConLike -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla instCon Int 4 Nabla nabla Id x ConLike 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 Maybe Nabla Nothing -> [Nabla] -> DsM [Nabla] forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a 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 nabla' -> GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla] generateInhabitingPatterns GenerateInhabitingPatternsMode mode [Id] xs Int n Nabla nabla' other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls pure (map (Just cl,) con_nablas ++ other_cons_nablas) -- | If multiple residual COMPLETE sets apply, pick one as follows: -- -- - prefer COMPLETE sets in which all constructors are in scope, -- as per Note [Prefer in-scope COMPLETE matches], -- - if there are ties, pick the one with the fewest (residual) ConLikes, -- - if there are ties, pick the one with the fewest "trivially inhabited" types, -- - if there are ties, pick the one with the fewest PatSyns, -- - if there are still ties, pick the one that comes first in the list of -- COMPLETE pragmas, which means the one that was brought into scope first. completeSetCost :: GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int) completeSetCost :: forall a. GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int) completeSetCost GlobalRdrEnv _ [] = (Bool False, Int 0, Int 0, Int 0) completeSetCost GlobalRdrEnv rdr_env ((Maybe ConLike mb_con, a _) : [(Maybe ConLike, a)] cons) = let con_out_of_scope :: Bool con_out_of_scope | Just ConLike con <- Maybe ConLike mb_con = Maybe (GlobalRdrEltX GREInfo) -> Bool forall a. Maybe a -> Bool isNothing (Maybe (GlobalRdrEltX GREInfo) -> Bool) -> Maybe (GlobalRdrEltX GREInfo) -> Bool forall a b. (a -> b) -> a -> b $ GlobalRdrEnv -> Name -> Maybe (GlobalRdrEltX GREInfo) forall info. Outputable info => GlobalRdrEnvX info -> Name -> Maybe (GlobalRdrEltX info) lookupGRE_Name GlobalRdrEnv rdr_env (ConLike -> Name conLikeName ConLike con) | Bool otherwise = Bool False (Bool any_out_of_scope, Int nb_cons, Int nb_triv, Int nb_ps) = GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int) forall a. GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int) completeSetCost GlobalRdrEnv rdr_env [(Maybe ConLike, a)] cons in ( Bool any_out_of_scope Bool -> Bool -> Bool || Bool con_out_of_scope , Int nb_cons Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1 , Int nb_triv Int -> Int -> Int forall a. Num a => a -> a -> a + case Maybe ConLike mb_con of { Maybe ConLike Nothing -> Int 1; Maybe ConLike _ -> Int 0 } , Int nb_ps Int -> Int -> Int forall a. Num a => a -> a -> a + case Maybe ConLike mb_con of { Just (PatSynCon {}) -> Int 1; Maybe ConLike _ -> Int 0 } ) {- Note [Prefer in-scope COMPLETE matches] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prefer using COMPLETE pragmas in which all ConLikes are in scope, as this improves error messages. See for example T25115: - T25115a defines pattern Foo :: a with {-# COMPLETE Foo #-} - T25115 imports T25115a, but not Foo. (This means it imports the COMPLETE pragma, which behaves like an instance.) Then, for the following incomplete pattern match in T25115: baz :: Ordering -> Int baz = \case EQ -> 5 we would prefer reporting that 'LT' and 'GT' are not matched, rather than saying that 'T25115a.Foo' is not matched. However, if ALL ConLikes are out of scope, then we should still report something, so we don't want to outright filter out all COMPLETE sets with an out-of-scope ConLike. -} pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> DsM DsCompleteMatches -- See Note [Implementation of COMPLETE pragmas] on what "applicable" means pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch] pickApplicableCompleteSets TyState ty_st Type ty ResidualCompleteMatches rcm = do let cl_res_ty_ok :: ConLike -> DsM Bool cl_res_ty_ok :: ConLike -> DsM Bool cl_res_ty_ok ConLike cl = do env <- DsM FamInstEnvs dsGetFamInstEnvs isJust <$> matchConLikeResTy env ty_st ty cl let cm_applicable :: DsCompleteMatch -> DsM Bool cm_applicable :: DsCompleteMatch -> DsM Bool cm_applicable DsCompleteMatch cm = do cls_ok <- (ConLike -> DsM Bool) -> [ConLike] -> DsM Bool forall (m :: * -> *) (f :: * -> *) a. (Monad m, Foldable f) => (a -> m Bool) -> f a -> m Bool allM ConLike -> DsM Bool cl_res_ty_ok (UniqDSet ConLike -> [ConLike] forall a. UniqDSet a -> [a] uniqDSetToList (DsCompleteMatch -> UniqDSet ConLike forall con. CompleteMatchX con -> UniqDSet con cmConLikes DsCompleteMatch cm)) let match_ty_ok = Type -> DsCompleteMatch -> Bool forall con. Type -> CompleteMatchX con -> Bool completeMatchAppliesAtType Type ty DsCompleteMatch cm pure (cls_ok && match_ty_ok) applicable_cms <- (DsCompleteMatch -> DsM Bool) -> [DsCompleteMatch] -> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch] forall (m :: * -> *) a. Applicative m => (a -> m Bool) -> [a] -> m [a] filterM DsCompleteMatch -> DsM Bool cm_applicable (ResidualCompleteMatches -> [DsCompleteMatch] getRcm ResidualCompleteMatches rcm) tracePm "pickApplicableCompleteSets:" $ vcat [ ppr ty , ppr rcm , ppr applicable_cms ] return applicable_cms {- 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. Note [Case split inhabiting patterns] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we have an -XEmptyCase, ```hs f :: Maybe a -> () f x = case x of {} ``` we want to show the different missing patterns {'Just _', 'Nothing'} to the user instead of an uninformative wildcard pattern '_'. But when we have a match as part of a function definition, such as ```hs g :: (Bool, [a]) -> () g (_, []) = () ``` we established in #20642 that we *do not* want to report P1={'(False, (_:_))', '(True, (_:_))'} when we could just give the singleton set P2={'(_, (_:_))'}! The latter set M is a "minimal cover" of the space of missing patterns S, in that 1. The union of M is *exactly* S 2. The size of M is minimal under all such candidates. In terms of 'g', P2 satisfies both (1) and (2). While P1 satisfies (1), it does not satisfy (2). The set {'_'} satisfies (2), but it does not satisfy (1) as it also covers the pattern '(_,[])' which is not part of the space of missing patterns of 'g', so it would be a bad (too conservative) suggestion. Note that for -XEmptyCase, we don't want to emit a minimal cover. We arrange that by passing 'CaseSplitTopLevel' to 'generateInhabitingPatterns'. We detect the -XEmptyCase case in 'reportWarnings' by looking for 'ReportEmptyCase'. -}