diff options
author | Sebastian Graf <sebastian.graf@kit.edu> | 2021-08-17 18:50:25 +0200 |
---|---|---|
committer | Sebastian Graf <sebastian.graf@kit.edu> | 2021-08-17 18:55:31 +0200 |
commit | 2ffe3e425e68e3d847996497f834338e0402edbe (patch) | |
tree | 647d0c2fa5c776e4b1a12124bdf2e6c592b269e1 | |
parent | 10124b16538091806953d732e24ca485a0664895 (diff) | |
download | haskell-2ffe3e425e68e3d847996497f834338e0402edbe.tar.gz |
A few improvements to the pattern-match checkerwip/T20106
While investigating #20106, I made a few refactorings to the pattern-match
checker that I don't want to lose. Here are the changes:
* Some key functions of the checker now have SCC annotations
* Better `-ddump-ec-trace` diagnostics for easier debugging. I added
'traceWhenFailPm' to see *why* a particular `MaybeT` computation fails and
made use of it in `instCon`.
* `varNeedsTesting` now additionally returns an updated `VarInfo` that
remembers which DataCons it tried to instantiate fruitlessly, thus caching
some work.
* `VarInfo` gets a new field `vi_norm_ty` that is a cache for the normalised
`idType` of `vi_id`. In some cases that may shortcut and obviate the need to
normalise with the previous type state in `varNeedsTesting`.
So two refactorings and two perf improvements (hopefully).
-rw-r--r-- | compiler/GHC/HsToCore/Pmc.hs | 10 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver.hs | 172 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver/Types.hs | 11 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Utils.hs | 12 |
4 files changed, 134 insertions, 71 deletions
diff --git a/compiler/GHC/HsToCore/Pmc.hs b/compiler/GHC/HsToCore/Pmc.hs index 04236d54b9..0b2ef7f8cb 100644 --- a/compiler/GHC/HsToCore/Pmc.hs +++ b/compiler/GHC/HsToCore/Pmc.hs @@ -150,7 +150,7 @@ pmcMatches -> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches -> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and -- GRHS, for long distance info. -pmcMatches ctxt vars matches = do +pmcMatches ctxt vars matches = {-# SCC "pmcMatches" #-} do -- We have to force @missing@ before printing out the trace message, -- otherwise we get interleaved output from the solver. This function -- should be strict in @missing@ anyway! @@ -169,10 +169,12 @@ pmcMatches ctxt vars matches = do formatReportWarnings cirbsEmptyCase ctxt vars result return [] Just matches -> do - matches <- noCheckDs $ desugarMatches vars matches - result <- unCA (checkMatchGroup matches) missing + matches <- {-# SCC "desugarMatches" #-} + noCheckDs $ desugarMatches vars matches + result <- {-# SCC "checkMatchGroup" #-} + unCA (checkMatchGroup matches) missing tracePm "}: " (ppr (cr_uncov result)) - formatReportWarnings cirbsMatchGroup ctxt vars result + {-# SCC "formatReportWarnings" #-} formatReportWarnings cirbsMatchGroup ctxt vars result return (NE.toList (ldiMatchGroup (cr_ret result))) {- Note [pmcPatBind only checks PatBindRhs] diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs index 1b6121f31f..efc0f95d3c 100644 --- a/compiler/GHC/HsToCore/Pmc/Solver.hs +++ b/compiler/GHC/HsToCore/Pmc/Solver.hs @@ -36,7 +36,7 @@ module GHC.HsToCore.Pmc.Solver ( import GHC.Prelude import GHC.HsToCore.Pmc.Types -import GHC.HsToCore.Pmc.Utils (tracePm, mkPmId) +import GHC.HsToCore.Pmc.Utils (tracePm, traceWhenFailPm, mkPmId) import GHC.Driver.Session import GHC.Driver.Config @@ -70,6 +70,7 @@ 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.Builtin.Types.Prim (tYPETyCon) import GHC.Core.TyCo.Rep @@ -94,6 +95,9 @@ import Data.List (sortBy, find) import qualified Data.List.NonEmpty as NE import Data.Ord (comparing) +import GHC.Utils.Trace +_ = pprTrace -- to silence unused import warnings + -- -- * Main exports -- @@ -324,23 +328,23 @@ pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult -- NB: Normalisation can potentially change kinds, if the head of the type -- is a type family with a variable result kind. I (Richard E) can't think -- of a way to cause trouble here, though. -pmTopNormaliseType (TySt _ inert) typ - = do env <- dsGetFamInstEnvs - tracePm "normalise" (ppr typ) - -- Before proceeding, we chuck typ into the constraint solver, in case - -- solving for given equalities may reduce typ some. See - -- "Wrinkle: local equalities" in Note [Type normalisation]. - 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 - Nothing -> NormalisedByConstraints typ' - Just ((ty_f,tm_f), ty) -> HadRedexes src_ty newtype_dcs core_ty - where - src_ty = eq_src_ty ty (typ' : ty_f [ty]) - newtype_dcs = tm_f [] - core_ty = ty +pmTopNormaliseType (TySt _ inert) typ = {-# SCC "pmTopNormaliseType" #-} do + env <- dsGetFamInstEnvs + tracePm "normalise" (ppr typ) + -- Before proceeding, we chuck typ into the constraint solver, in case + -- solving for given equalities may reduce typ some. See + -- "Wrinkle: local equalities" in Note [Type normalisation]. + 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 + Nothing -> NormalisedByConstraints typ' + Just ((ty_f,tm_f), ty) -> HadRedexes src_ty newtype_dcs core_ty + where + src_ty = eq_src_ty ty (typ' : ty_f [ty]) + newtype_dcs = tm_f [] + core_ty = 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!). @@ -620,8 +624,9 @@ tyOracle ty_st@(TySt n inert) cts | isEmptyBag cts = pure (Just ty_st) | otherwise - = do { evs <- traverse nameTyCt cts - ; tracePm "tyOracle" (ppr cts $$ ppr inert) + = {-# SCC "tyOracle" #-} + do { evs <- traverse nameTyCt 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) } @@ -711,7 +716,7 @@ addNotConCt nabla x nalt = do -- 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 vi@(VI x' pos neg _ rcm) = do + go vi@(VI x' _ pos neg _ rcm) = do -- 1. Bail out quickly when nalt contradicts a solution let contradicts nalt sol = eqPmAltCon (paca_con sol) nalt == Equal guard (not (any (contradicts nalt) pos)) @@ -751,7 +756,7 @@ hasRequiredTheta _ = False -- See Note [TmState invariants]. addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla addConCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x alt tvs args = do - let vi@(VI _ pos neg bot _) = lookupVarInfo ts x + let vi@(VI _ _ pos neg bot _) = lookupVarInfo ts x -- First try to refute with a negative fact guard (not (elemPmAltConSet alt neg)) -- Then see if any of the other solutions (remember: each of them is an @@ -764,8 +769,6 @@ addConCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x alt tvs args = Just (PACA _con other_tvs other_args) -> do -- We must unify existentially bound ty vars and arguments! let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs) - when (length args /= length other_args) $ - lift $ tracePm "error" (ppr x <+> ppr alt <+> ppr args <+> ppr other_args) nabla' <- MaybeT $ addPhiCts nabla (listToBag ty_cts) let add_var_ct nabla (a, b) = addVarCt nabla a b foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args @@ -1175,7 +1178,7 @@ traverseAll f ts@TmSt{ts_facts = env} = do -- The \(∇ ⊢ x inh\) judgment form in Figure 8 of the LYG paper. inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla inhabitationTest 0 _ nabla = pure nabla -inhabitationTest fuel old_ty_st nabla@MkNabla{ nabla_tm_st = ts } = do +inhabitationTest fuel old_ty_st nabla@MkNabla{ nabla_tm_st = ts } = {-# SCC "inhabitationTest" #-} do -- lift $ tracePm "inhabitation test" $ vcat -- [ ppr fuel -- , ppr old_ty_st @@ -1190,34 +1193,48 @@ inhabitationTest fuel old_ty_st nabla@MkNabla{ nabla_tm_st = ts } = do where nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} } test_one :: VarInfo -> MaybeT DsM VarInfo - test_one vi = - lift (varNeedsTesting old_ty_st nabla vi) >>= \case - True -> do + test_one vi = do + (need_test, vi') <- lift (varNeedsTesting old_ty_st nabla vi) + if need_test + then 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 - instantiate (fuel-1) nabla_not_dirty vi - _ -> pure vi + instantiate (fuel-1) nabla_not_dirty vi' + else pure 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, VarInfo) varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} vi - | elemDVarSet (vi_id vi) (ts_dirty tm_st) = pure True + | elemDVarSet (vi_id vi) (ts_dirty tm_st) = pure (True, vi) varNeedsTesting _ _ vi - | notNull (vi_pos vi) = pure False -varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _ + | notNull (vi_pos vi) = pure (False, vi) +varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi -- Same type state => still inhabited - | not (tyStateRefined old_ty_st new_ty_st) = pure False -varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do + | not (tyStateRefined old_ty_st new_ty_st) = pure (False, vi) +varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = {-# SCC "varNeedsTesting" #-} do -- These normalisations are relatively expensive, but still better than having -- to perform a full inhabitation test - (_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (idType $ vi_id vi) - (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi) - if old_norm_ty `eqType` new_norm_ty - then pure False - else pure True + -- First check whether the cached (and potentially outdated) vi_norm_ty is + -- already equal to the new one, in which case we saved normalisation with + -- the old_ty_st + (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (vi_norm_ty vi) + let vi' = vi{vi_norm_ty=new_norm_ty} + let no_change = vi_norm_ty vi `eqType` new_norm_ty + --tracePm "varNeedsTesting1" (ppr (not no_change) $$ ppr (idType (vi_id vi)) $$ ppr (vi_norm_ty vi) $$ ppr new_norm_ty) + if no_change + then pure (False, vi') + else do + -- Now try to normalise vi_norm_ty again with old_ty_st, maybe it wasn't + -- up to date. + (_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (vi_norm_ty vi) + let no_change = old_norm_ty `eqType` new_norm_ty + --tracePm "varNeedsTesting2" (ppr (not no_change) $$ ppr old_norm_ty $$ ppr new_norm_ty) + if no_change + then pure (False, vi') + else pure (True, vi') -- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE -- set satisfies the oracle @@ -1228,11 +1245,12 @@ varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do -- remain that do not statisfy it. This lazy approach just -- avoids doing unnecessary work. instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo -instantiate fuel nabla vi = instBot fuel nabla vi <|> instCompleteSets fuel nabla vi +instantiate fuel nabla vi = {-# SCC "instantiate" #-} + (instBot fuel nabla vi <|> instCompleteSets fuel nabla vi) -- | The \(⊢_{Bot}\) rule from the paper instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo -instBot _fuel nabla vi = do +instBot _fuel nabla vi = {-# SCC "instBot" #-} do _nabla' <- addBotCt nabla (vi_id vi) pure vi @@ -1249,7 +1267,7 @@ addNormalisedTypeMatches nabla@MkNabla{ nabla_ty_st = ty_st } x rcm' <- case splitReprTyConApp_maybe env norm_res_ty of Just (rep_tc, _args, _co) -> addTyConMatches rep_tc rcm Nothing -> addCompleteMatches rcm - pure (rcm', vi{ vi_rcm = rcm' }) + pure (rcm', vi{ vi_rcm = rcm', vi_norm_ty = norm_res_ty }) -- | Does a 'splitTyConApp_maybe' and then tries to look through a data family -- application to find the representation TyCon, to which the data constructors @@ -1266,7 +1284,7 @@ splitReprTyConApp_maybe env ty = -- where all the attempted ConLike instantiations have been purged from the -- 'ResidualCompleteMatches', which functions as a cache. instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo -instCompleteSets fuel nabla vi = do +instCompleteSets fuel nabla vi = {-# SCC "instCompleteSets" #-} do let x = vi_id vi (rcm, nabla) <- lift (addNormalisedTypeMatches nabla x) nabla <- foldM (\nabla cls -> instCompleteSet fuel nabla x cls) nabla (getRcm rcm) @@ -1297,7 +1315,7 @@ instCompleteSet fuel nabla x cs | not (completeMatchAppliesAtType (varType x) cs) = pure nabla | otherwise - = go nabla (sorted_candidates cs) + = {-# SCC "instCompleteSet" #-} go nabla (sorted_candidates cs) where vi = lookupVarInfo (nabla_tm_st nabla) x @@ -1347,12 +1365,17 @@ dataConUnliftedFieldTys = filter ((== Just True) . isLiftedType_maybe) . map scaledThing . dataConOrigArgTys isTyConTriviallyInhabited :: TyCon -> Bool -isTyConTriviallyInhabited tc = elementOfUniqSet tc triviallyInhabitedTyCons +isTyConTriviallyInhabited tc = elementOfUniqSet (getUnique tc) triviallyInhabitedTyConKeys -- | All these types are trivially inhabited -triviallyInhabitedTyCons :: UniqSet TyCon -triviallyInhabitedTyCons = mkUniqSet [ - charTyCon, doubleTyCon, floatTyCon, intTyCon, wordTyCon, word8TyCon +triviallyInhabitedTyConKeys :: UniqSet Unique +triviallyInhabitedTyConKeys = mkUniqSet [ + charTyConKey, doubleTyConKey, floatTyConKey, + intTyConKey, int8TyConKey, int16TyConKey, int32TyConKey, int64TyConKey, + intPrimTyConKey, int8PrimTyConKey, int16PrimTyConKey, int32PrimTyConKey, int64PrimTyConKey, + wordTyConKey, word8TyConKey, word16TyConKey, word32TyConKey, word64TyConKey, + wordPrimTyConKey, word8PrimTyConKey, word16PrimTyConKey, word32PrimTyConKey, word64PrimTyConKey, + trTyConTyConKey ] compareConLikeTestability :: ConLike -> ConLike -> Ordering @@ -1384,9 +1407,12 @@ compareConLikeTestability (RealDataCon a) (RealDataCon b) = mconcat -- -- See Note [Instantiating a ConLike]. instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla -instCon fuel nabla@MkNabla{nabla_ty_st = ty_st} x con = MaybeT $ do +instCon fuel nabla@MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} MaybeT $ do + let hdr what = "instCon " ++ show fuel ++ " " ++ what env <- dsGetFamInstEnvs let match_ty = idType 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 @@ -1403,28 +1429,46 @@ instCon fuel nabla@MkNabla{nabla_ty_st = ty_st} x con = MaybeT $ do -- (4) Instantiate fresh term variables as arguments to the constructor let field_tys' = substTys sigma_ex $ map scaledThing field_tys arg_ids <- mapM mkPmId field_tys' - tracePm "instCon" $ vcat + 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 (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs) , ppr gammas , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids) - , ppr fuel ] -- (5) Finally add the new constructor constraint runMaybeT $ do -- Case (2) of Note [Strict fields and variables of unlifted type] let alt = PmAltConLike con - nabla' <- addPhiTmCt nabla (PhiConCt x alt ex_tvs gammas arg_ids) - let branching_factor = length $ filterUnliftedFields alt arg_ids + let ct = PhiConCt x alt ex_tvs gammas arg_ids + nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $ + addPhiTmCt nabla ct + let branching_factor = length (filterUnliftedFields alt arg_ids) + + length gammas -- See Note [Fuel for the inhabitation test] let new_fuel | branching_factor <= 1 = fuel | otherwise = min fuel 2 - inhabitationTest new_fuel (nabla_ty_st nabla) nabla' - Nothing -> pure (Just nabla) -- Matching against match_ty failed. Inhabited! - -- See Note [Instantiating a ConLike]. + 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 (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs) + , ppr gammas + , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType 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 + Nothing -> do + tracePm (hdr "(match_ty not instance of res_ty) }") empty + pure (Just 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 @@ -1439,7 +1483,7 @@ matchConLikeResTy env _ ty (RealDataCon dc) = pure $ do if rep_tc == dataConTyCon dc then Just (zipTCvSubst (dataConUnivTyVars dc) tc_args) else Nothing -matchConLikeResTy _ (TySt _ inert) ty (PatSynCon ps) = runMaybeT $ do +matchConLikeResTy _ (TySt _ inert) ty (PatSynCon ps) = {-# SCC "matchConLikeResTy" #-} runMaybeT $ do let (univ_tvs,req_theta,_,_,_,con_res_ty) = patSynSig ps subst <- MaybeT $ pure $ tcMatchTy con_res_ty ty guard $ all (`elemTCvSubst` subst) univ_tvs -- See the Note about T11336b @@ -1454,7 +1498,7 @@ matchConLikeResTy _ (TySt _ inert) ty (PatSynCon ps) = runMaybeT $ do {- Note [Soundness and completeness] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Soundness and completeness of the pattern-match checker depends entirely on the +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. @@ -1573,7 +1617,7 @@ instantiation and requires an inductive argument, which `inhabitationTest` currently isn't equipped to do. In order to prevent endless instantiation attempts in @inhabitationTest@, we -use the fuel as an upper bound such attempts. +use the fuel as an upper bound on such attempts. The same problem occurs with recursive newtypes, like in the following code: @@ -1711,8 +1755,8 @@ 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. -(Type refinement from unpacking GADT constructors might monomorphise `match_ty` -so much that `res_ty` ultimately subsumes it.) +(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 @@ -1756,7 +1800,7 @@ generateInhabitingPatterns _ 0 _ = pure [] generateInhabitingPatterns [] _ nabla = pure [nabla] generateInhabitingPatterns (x:xs) n nabla = do tracePm "generateInhabitingPatterns" (ppr n <+> ppr (x:xs) $$ ppr nabla) - let VI _ pos neg _ _ = lookupVarInfo (nabla_tm_st nabla) x + let VI _ _ pos neg _ _ = lookupVarInfo (nabla_tm_st nabla) x case pos of _:_ -> do -- All solutions must be valid at once. Try to find candidates for their diff --git a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs index a111bbdd33..1ca3b75bc1 100644 --- a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs +++ b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs @@ -159,6 +159,12 @@ data VarInfo -- ^ The 'Id' in question. Important for adding new constraints relative to -- this 'VarInfo' when we don't easily have the 'Id' available. + , vi_norm_ty :: !Type + -- ^ A cached (and perhaps out of date) version of @'idType' vi_id@, + -- normalised according to the accompanying 'TyState'. It speeds up type + -- normalisation a bit and speeds up 'varNeedsTesting' in case the the cached + -- type conincides with the new normalised type after 'TyState' refinement. + , vi_pos :: ![PmAltConApp] -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all -- at the same time (i.e. conjunctive). We need a list because of nested @@ -228,10 +234,10 @@ instance Outputable TmState where -- | Not user-facing. instance Outputable VarInfo where - ppr (VI x pos neg bot cache) + ppr (VI x ty pos neg bot cache) = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache])) where - pp_x = ppr x <> dcolon <> ppr (idType x) + pp_x = ppr x <> dcolon <> ppr ty -- ty is a refinement of idType x pp_pos | [] <- pos = underscore | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton @@ -287,6 +293,7 @@ emptyVarInfo :: Id -> VarInfo emptyVarInfo x = VI { vi_id = x + , vi_norm_ty = idType x , vi_pos = [] , vi_neg = emptyPmAltConSet -- Case (3) in Note [Strict fields and fields of unlifted type] diff --git a/compiler/GHC/HsToCore/Pmc/Utils.hs b/compiler/GHC/HsToCore/Pmc/Utils.hs index 0bafac4088..12ccd6516b 100644 --- a/compiler/GHC/HsToCore/Pmc/Utils.hs +++ b/compiler/GHC/HsToCore/Pmc/Utils.hs @@ -4,7 +4,7 @@ -- | Utility module for the pattern-match coverage checker. module GHC.HsToCore.Pmc.Utils ( - tracePm, mkPmId, + tracePm, traceWhenFailPm, mkPmId, allPmCheckWarnings, overlapping, exhaustive, redundantBang, exhaustiveWarningFlag, isMatchContextPmChecked, needToRunPmCheck @@ -19,6 +19,7 @@ import GHC.Hs import GHC.Core.Type import GHC.Data.FastString import GHC.Data.IOEnv +import GHC.Data.Maybe import GHC.Types.Id import GHC.Types.Name import GHC.Types.Unique.Supply @@ -28,6 +29,8 @@ import GHC.Utils.Outputable import GHC.Utils.Logger import GHC.HsToCore.Monad +import Control.Monad + tracePm :: String -> SDoc -> DsM () tracePm herald doc = do logger <- getLogger @@ -36,6 +39,13 @@ tracePm herald doc = do Opt_D_dump_ec_trace "" FormatText (text herald $$ (nest 2 doc)) {-# INLINE tracePm #-} -- see Note [INLINE conditional tracing utilities] +traceWhenFailPm :: String -> SDoc -> MaybeT DsM a -> MaybeT DsM a +traceWhenFailPm herald doc act = MaybeT $ do + mb_a <- runMaybeT act + when (isNothing mb_a) $ tracePm herald doc + pure mb_a +{-# INLINE traceWhenFailPm #-} -- see Note [INLINE conditional tracing utilities] + -- | Generate a fresh `Id` of a given type mkPmId :: Type -> DsM Id mkPmId ty = getUniqueM >>= \unique -> |