Pmc: Better SCC annotations and trace output

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.

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',