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-20 13:29:28 +0200 |
commit | 08f5ec098ce284a00c74e0b7f22d32374fac3155 (patch) | |
tree | 0ae20d22418bf0154fb805adc40375529cfddb3d | |
parent | acb188e0c02a114927d340dac78a68626c659cd3 (diff) | |
download | haskell-08f5ec098ce284a00c74e0b7f22d32374fac3155.tar.gz |
Pmc: Better SCC annotations and trace outputwip/improve-pmc
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`.
I also increased the acceptance threshold of T11545, which seems to fail
randomly lately due to ghc/max flukes.
-rw-r--r-- | compiler/GHC/HsToCore/Pmc.hs | 10 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver.hs | 115 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Utils.hs | 12 | ||||
-rw-r--r-- | testsuite/tests/perf/compiler/all.T | 2 |
4 files changed, 90 insertions, 49 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 3caced3468..aafac14516 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 @@ -95,6 +96,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 -- @@ -325,23 +329,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!). @@ -624,8 +628,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) } @@ -768,8 +773,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 @@ -1179,7 +1182,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 @@ -1232,11 +1235,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 @@ -1270,7 +1274,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) @@ -1301,7 +1305,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 @@ -1351,12 +1355,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 @@ -1388,9 +1397,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 @@ -1407,28 +1419,45 @@ 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 -- 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 @@ -1443,7 +1472,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 @@ -1458,7 +1487,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. @@ -1577,7 +1606,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: @@ -1715,8 +1744,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 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 -> diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T index 6628fb377e..2044da0f90 100644 --- a/testsuite/tests/perf/compiler/all.T +++ b/testsuite/tests/perf/compiler/all.T @@ -471,7 +471,7 @@ test ('T9198', ['']) test('T11545', - [ collect_compiler_stats('all', 10) ], + [ collect_compiler_stats('all', 15) ], compile, ['-O']) test('T15304', |