PmCheck: Better long-distance info for where bindings (#18533)

Where bindings can see evidence from the pattern match of the `GRHSs`
they belong to, but not from anything in any of the guards (which belong
to one of possibly many RHSs).

Before this patch, we did *not* consider said evidence, causing #18533,
where the lack of considering type information from a case pattern match
leads to failure to resolve the vanilla COMPLETE set of a data type.

Making available that information required a medium amount of
refactoring so that `checkMatches` can return a
`[(Deltas, NonEmpty Deltas)]`; one `(Deltas, NonEmpty Deltas)` for each
`GRHSs` of the match group. The first component of the pair is the
covered set of the pattern, the second component is one covered set per
RHS.

Fixes #18533.
Regression test case: T18533

15 files changed, 211 insertions, 146 deletions

diff --git a/compiler/GHC/Cmm/DebugBlock.hs b/compiler/GHC/Cmm/DebugBlock.hs
index 4e39fb7ecd..2d8ec5f2b3 100644
--- a/compiler/GHC/Cmm/DebugBlock.hs
+++ b/compiler/GHC/Cmm/DebugBlock.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiWayIf #-}
 
@@ -110,7 +111,9 @@ cmmDebugGen modLoc decls = map (blocksForScope Nothing) topScopes
               -- recover by copying ticks below.
               scp' | SubScope _ scp' <- scp      = scp'
                    | CombinedScope scp' _ <- scp = scp'
+#if __GLASGOW_HASKELL__ <= 810
                    | otherwise                   = panic "findP impossible"
+#endif
 
       scopeMap = foldr (uncurry insertMulti) Map.empty childScopes
 
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 2de2089904..fb2bde23d1 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -559,7 +559,10 @@ opt_univ env sym prov role oty1 oty2
 
   where
     prov' = case prov of
+#if __GLASGOW_HASKELL__ <= 810
+-- This alt is redundant with the first match of the FunDef
       PhantomProv kco    -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
+#endif
       ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
       PluginProv _       -> prov
 
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index d08e2079b0..806ee1d3a7 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -1243,7 +1243,9 @@ ppr_infix_expr (HsConLikeOut _ c)   = Just (pprInfixOcc (conLikeName c))
 ppr_infix_expr (HsRecFld _ f)       = Just (pprInfixOcc f)
 ppr_infix_expr (HsUnboundVar _ occ) = Just (pprInfixOcc occ)
 ppr_infix_expr (XExpr x)            = case (ghcPass @p, x) of
+#if __GLASGOW_HASKELL__ <= 810
   (GhcPs, _)                              -> Nothing
+#endif
   (GhcRn, HsExpanded a _)                 -> ppr_infix_expr a
   (GhcTc, WrapExpr (HsWrap _ e))          -> ppr_infix_expr e
   (GhcTc, ExpansionExpr (HsExpanded a _)) -> ppr_infix_expr a
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index 59873ac600..1bf9715d18 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -845,8 +845,10 @@ patNeedsParens p = go
     go (SigPat {})       = p >= sigPrec
     go (ViewPat {})      = True
     go (XPat ext)        = case ghcPass @p of
+#if __GLASGOW_HASKELL__ <= 810
       GhcPs -> noExtCon ext
       GhcRn -> noExtCon ext
+#endif
       GhcTc -> go inner
         where CoPat _ inner _ = ext
     go (WildPat {})      = False
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 2a61406792..5e01bc7a8f 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -33,7 +33,7 @@ import {-# SOURCE #-}   GHC.HsToCore.Match ( matchWrapper )
 import GHC.HsToCore.Monad
 import GHC.HsToCore.GuardedRHSs
 import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck ( addTyCsDs, checkGuardMatches )
+import GHC.HsToCore.PmCheck ( addTyCsDs, checkGRHSs )
 
 import GHC.Hs             -- lots of things
 import GHC.Core           -- lots of things
@@ -78,7 +78,6 @@ import GHC.Types.Unique.Set( nonDetEltsUniqSet )
 import GHC.Utils.Monad
 import qualified GHC.LanguageExtensions as LangExt
 import Control.Monad
-import Data.List.NonEmpty ( nonEmpty )
 
 {-**********************************************************************
 *                                                                      *
@@ -185,8 +184,8 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
 dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss
                          , pat_ext = NPatBindTc _ ty
                          , pat_ticks = (rhs_tick, var_ticks) })
-  = do  { rhss_deltas <- checkGuardMatches PatBindGuards grhss
-        ; body_expr <- dsGuarded grhss ty (nonEmpty rhss_deltas)
+  = do  { rhss_deltas <- checkGRHSs PatBindGuards grhss
+        ; body_expr <- dsGuarded grhss ty rhss_deltas
         ; let body' = mkOptTickBox rhs_tick body_expr
               pat'  = decideBangHood dflags pat
         ; (force_var,sel_binds) <- mkSelectorBinds var_ticks pat body'
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index be6c207dd6..144a652484 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -31,7 +31,7 @@ import GHC.HsToCore.ListComp
 import GHC.HsToCore.Utils
 import GHC.HsToCore.Arrows
 import GHC.HsToCore.Monad
-import GHC.HsToCore.PmCheck ( addTyCsDs, checkGuardMatches )
+import GHC.HsToCore.PmCheck ( addTyCsDs, checkGRHSs )
 import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Core.FamInstEnv( topNormaliseType )
@@ -70,7 +70,6 @@ import GHC.Utils.Panic
 import GHC.Core.PatSyn
 
 import Control.Monad
-import Data.List.NonEmpty ( nonEmpty )
 
 {-
 ************************************************************************
@@ -216,8 +215,8 @@ dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss
                         , pat_ext = NPatBindTc _ ty }) body
   =     -- let C x# y# = rhs in body
         -- ==> case rhs of C x# y# -> body
-    do { rhs_deltas <- checkGuardMatches PatBindGuards grhss
-       ; rhs         <- dsGuarded grhss ty (nonEmpty rhs_deltas)
+    do { match_deltas <- checkGRHSs PatBindGuards grhss
+       ; rhs          <- dsGuarded grhss ty match_deltas
        ; let upat = unLoc pat
              eqn = EqnInfo { eqn_pats = [upat],
                              eqn_orig = FromSource,
@@ -487,8 +486,8 @@ dsExpr (HsMultiIf res_ty alts)
 
   | otherwise
   = do { let grhss = GRHSs noExtField alts (noLoc emptyLocalBinds)
-       ; rhss_deltas  <- checkGuardMatches IfAlt grhss
-       ; match_result <- dsGRHSs IfAlt grhss res_ty (nonEmpty rhss_deltas)
+       ; rhss_deltas  <- checkGRHSs IfAlt grhss
+       ; match_result <- dsGRHSs IfAlt grhss res_ty rhss_deltas
        ; error_expr   <- mkErrorExpr
        ; extractMatchResult match_result error_expr }
   where
diff --git a/compiler/GHC/HsToCore/GuardedRHSs.hs b/compiler/GHC/HsToCore/GuardedRHSs.hs
index 88439c9e0c..6ff171febc 100644
--- a/compiler/GHC/HsToCore/GuardedRHSs.hs
+++ b/compiler/GHC/HsToCore/GuardedRHSs.hs
@@ -25,7 +25,7 @@ import GHC.Core.Utils (bindNonRec)
 
 import GHC.HsToCore.Monad
 import GHC.HsToCore.Utils
-import GHC.HsToCore.PmCheck.Types ( Deltas, initDeltas )
+import GHC.HsToCore.PmCheck.Types ( Deltas )
 import GHC.Core.Type ( Type )
 import GHC.Utils.Misc
 import GHC.Types.SrcLoc
@@ -48,9 +48,9 @@ producing an expression with a runtime error in the corner if
 necessary.  The type argument gives the type of the @ei@.
 -}
 
-dsGuarded :: GRHSs GhcTc (LHsExpr GhcTc) -> Type -> Maybe (NonEmpty Deltas) -> DsM CoreExpr
-dsGuarded grhss rhs_ty mb_rhss_deltas = do
-    match_result <- dsGRHSs PatBindRhs grhss rhs_ty mb_rhss_deltas
+dsGuarded :: GRHSs GhcTc (LHsExpr GhcTc) -> Type -> NonEmpty Deltas -> DsM CoreExpr
+dsGuarded grhss rhs_ty rhss_deltas = do
+    match_result <- dsGRHSs PatBindRhs grhss rhs_ty rhss_deltas
     error_expr <- mkErrorAppDs nON_EXHAUSTIVE_GUARDS_ERROR_ID rhs_ty empty
     extractMatchResult match_result error_expr
 
@@ -59,25 +59,28 @@ dsGuarded grhss rhs_ty mb_rhss_deltas = do
 dsGRHSs :: HsMatchContext GhcRn
         -> GRHSs GhcTc (LHsExpr GhcTc) -- ^ Guarded RHSs
         -> Type                        -- ^ Type of RHS
-        -> Maybe (NonEmpty Deltas)     -- ^ Refined pattern match checking
-                                       --   models, one for each GRHS. Defaults
-                                       --   to 'initDeltas' if 'Nothing'.
+        -> NonEmpty Deltas             -- ^ Refined pattern match checking
+                                       --   models, one for the pattern part and
+                                       --   one for each GRHS.
         -> DsM (MatchResult CoreExpr)
-dsGRHSs hs_ctx (GRHSs _ grhss binds) rhs_ty mb_rhss_deltas
+dsGRHSs hs_ctx (GRHSs _ grhss binds) rhs_ty rhss_deltas
   = ASSERT( notNull grhss )
-    do { match_results <- case toList <$> mb_rhss_deltas of
-           Nothing          -> mapM     (dsGRHS hs_ctx rhs_ty initDeltas) grhss
-           Just rhss_deltas -> ASSERT( length grhss == length rhss_deltas )
-                               zipWithM (dsGRHS hs_ctx rhs_ty) rhss_deltas grhss
-       ; let match_result1 = foldr1 combineMatchResults match_results
-             match_result2 = adjustMatchResultDs (dsLocalBinds binds) match_result1
+    do { match_results <- ASSERT( length grhss == length rhss_deltas )
+                          zipWithM (dsGRHS hs_ctx rhs_ty) (toList rhss_deltas) grhss
+       ; deltas <- getPmDeltas
+       -- We need to remember the Deltas from the particular match context we
+       -- are in, which might be different to when dsLocalBinds is actually
+       -- called.
+       ; let ds_binds      = updPmDeltas deltas . dsLocalBinds binds
+             match_result1 = foldr1 combineMatchResults match_results
+             match_result2 = adjustMatchResultDs ds_binds match_result1
                              -- NB: nested dsLet inside matchResult
        ; return match_result2 }
 
 dsGRHS :: HsMatchContext GhcRn -> Type -> Deltas -> LGRHS GhcTc (LHsExpr GhcTc)
        -> DsM (MatchResult CoreExpr)
 dsGRHS hs_ctx rhs_ty rhs_deltas (L _ (GRHS _ guards rhs))
-  = updPmDeltas rhs_deltas (matchGuards (map unLoc guards) (PatGuard hs_ctx) rhs rhs_ty)
+  = matchGuards (map unLoc guards) (PatGuard hs_ctx) rhs_deltas rhs rhs_ty
 
 {-
 ************************************************************************
@@ -89,6 +92,7 @@ dsGRHS hs_ctx rhs_ty rhs_deltas (L _ (GRHS _ guards rhs))
 
 matchGuards :: [GuardStmt GhcTc]     -- Guard
             -> HsStmtContext GhcRn   -- Context
+            -> Deltas                -- The RHS's covered set for PmCheck
             -> LHsExpr GhcTc         -- RHS
             -> Type                  -- Type of RHS of guard
             -> DsM (MatchResult CoreExpr)
@@ -96,8 +100,8 @@ matchGuards :: [GuardStmt GhcTc]     -- Guard
 -- See comments with HsExpr.Stmt re what a BodyStmt means
 -- Here we must be in a guard context (not do-expression, nor list-comp)
 
-matchGuards [] _ rhs _
-  = do  { core_rhs <- dsLExpr rhs
+matchGuards [] _ deltas rhs _
+  = do  { core_rhs <- updPmDeltas deltas (dsLExpr rhs)
         ; return (cantFailMatchResult core_rhs) }
 
         -- BodyStmts must be guards
@@ -107,41 +111,41 @@ matchGuards [] _ rhs _
         -- NB:  The success of this clause depends on the typechecker not
         --      wrapping the 'otherwise' in empty HsTyApp or HsWrap constructors
         --      If it does, you'll get bogus overlap warnings
-matchGuards (BodyStmt _ e _ _ : stmts) ctx rhs rhs_ty
+matchGuards (BodyStmt _ e _ _ : stmts) ctx deltas rhs rhs_ty
   | Just addTicks <- isTrueLHsExpr e = do
-    match_result <- matchGuards stmts ctx rhs rhs_ty
+    match_result <- matchGuards stmts ctx deltas rhs rhs_ty
     return (adjustMatchResultDs addTicks match_result)
-matchGuards (BodyStmt _ expr _ _ : stmts) ctx rhs rhs_ty = do
-    match_result <- matchGuards stmts ctx rhs rhs_ty
+matchGuards (BodyStmt _ expr _ _ : stmts) ctx deltas rhs rhs_ty = do
+    match_result <- matchGuards stmts ctx deltas rhs rhs_ty
     pred_expr <- dsLExpr expr
     return (mkGuardedMatchResult pred_expr match_result)
 
-matchGuards (LetStmt _ binds : stmts) ctx rhs rhs_ty = do
-    match_result <- matchGuards stmts ctx rhs rhs_ty
+matchGuards (LetStmt _ binds : stmts) ctx deltas rhs rhs_ty = do
+    match_result <- matchGuards stmts ctx deltas rhs rhs_ty
     return (adjustMatchResultDs (dsLocalBinds binds) match_result)
         -- NB the dsLet occurs inside the match_result
         -- Reason: dsLet takes the body expression as its argument
         --         so we can't desugar the bindings without the
         --         body expression in hand
 
-matchGuards (BindStmt _ pat bind_rhs : stmts) ctx rhs rhs_ty = do
+matchGuards (BindStmt _ pat bind_rhs : stmts) ctx deltas rhs rhs_ty = do
     let upat = unLoc pat
     match_var <- selectMatchVar Many upat
        -- We only allow unrestricted patterns in guard, hence the `Many`
        -- above. It isn't clear what linear patterns would mean, maybe we will
        -- figure it out in the future.
 
-    match_result <- matchGuards stmts ctx rhs rhs_ty
+    match_result <- matchGuards stmts ctx deltas rhs rhs_ty
     core_rhs <- dsLExpr bind_rhs
     match_result' <- matchSinglePatVar match_var (StmtCtxt ctx) pat rhs_ty
                                        match_result
     pure $ bindNonRec match_var core_rhs <$> match_result'
 
-matchGuards (LastStmt  {} : _) _ _ _ = panic "matchGuards LastStmt"
-matchGuards (ParStmt   {} : _) _ _ _ = panic "matchGuards ParStmt"
-matchGuards (TransStmt {} : _) _ _ _ = panic "matchGuards TransStmt"
-matchGuards (RecStmt   {} : _) _ _ _ = panic "matchGuards RecStmt"
-matchGuards (ApplicativeStmt {} : _) _ _ _ =
+matchGuards (LastStmt  {} : _) _ _ _ _ = panic "matchGuards LastStmt"
+matchGuards (ParStmt   {} : _) _ _ _ _ = panic "matchGuards ParStmt"
+matchGuards (TransStmt {} : _) _ _ _ _ = panic "matchGuards TransStmt"
+matchGuards (RecStmt   {} : _) _ _ _ _ = panic "matchGuards RecStmt"
+matchGuards (ApplicativeStmt {} : _) _ _ _ _ =
   panic "matchGuards ApplicativeLastStmt"
 
 {-
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index bc28e2110d..98a27c97f3 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -35,6 +35,7 @@ import GHC.Tc.Utils.Zonk
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.Monad
 import GHC.HsToCore.PmCheck
+import GHC.HsToCore.PmCheck.Types ( Deltas, initDeltas )
 import GHC.Core
 import GHC.Types.Literal
 import GHC.Core.Utils
@@ -65,7 +66,7 @@ import GHC.Data.FastString
 import GHC.Types.Unique
 import GHC.Types.Unique.DFM
 
-import Control.Monad( unless )
+import Control.Monad(zipWithM,  unless )
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.List.NonEmpty as NEL
 import qualified Data.Map as Map
@@ -767,49 +768,47 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
         -- Pattern match check warnings for /this match-group/.
         -- @rhss_deltas@ is a flat list of covered Deltas for each RHS.
         -- Each Match will split off one Deltas for its RHSs from this.
-        ; rhss_deltas <- if isMatchContextPmChecked dflags origin ctxt
+        ; matches_deltas <- if isMatchContextPmChecked dflags origin ctxt
             then addScrutTmCs mb_scr new_vars $
-              -- See Note [Type and Term Equality Propagation]
-              checkMatches (DsMatchContext ctxt locn) new_vars matches
-            else pure [] -- Ultimately this will result in passing Nothing
-                         -- to dsGRHSs as match_deltas
+                 -- See Note [Type and Term Equality Propagation]
+                 checkMatches (DsMatchContext ctxt locn) new_vars matches
+            else pure (initDeltasMatches matches)
 
-        ; eqns_info   <- mk_eqn_infos matches rhss_deltas
+        ; eqns_info   <- zipWithM mk_eqn_info matches matches_deltas
 
         ; result_expr <- handleWarnings $
                          matchEquations ctxt new_vars eqns_info rhs_ty
         ; return (new_vars, result_expr) }
   where
-    -- rhss_deltas is a flat list, whereas there are multiple GRHSs per match.
-    -- mk_eqn_infos will thread rhss_deltas as state through calls to
-    -- mk_eqn_info, distributing each rhss_deltas to a GRHS.
-    mk_eqn_infos (L _ match : matches) rhss_deltas
-      = do { (info, rhss_deltas') <- mk_eqn_info  match   rhss_deltas
-           ; infos                <- mk_eqn_infos matches rhss_deltas'
-           ; return (info:infos) }
-    mk_eqn_infos [] _ = return []
     -- Called once per equation in the match, or alternative in the case
-    mk_eqn_info (Match { m_pats = pats, m_grhss = grhss }) rhss_deltas
-      | GRHSs _ grhss' _  <- grhss, let n_grhss = length grhss'
+    mk_eqn_info :: LMatch GhcTc (LHsExpr GhcTc) -> (Deltas, NonEmpty Deltas) -> DsM EquationInfo
+    mk_eqn_info (L _ (Match { m_pats = pats, m_grhss = grhss })) (pat_deltas, rhss_deltas)
       = do { dflags <- getDynFlags
            ; let upats = map (unLoc . decideBangHood dflags) pats
-           -- Split off one Deltas for each GRHS of the current Match from the
-           -- flat list of GRHS Deltas *for all matches* (see the call to
-           -- checkMatches above).
-           ; let (match_deltas, rhss_deltas') = splitAt n_grhss rhss_deltas
-           -- The list of Deltas is empty iff we don't perform any coverage
-           -- checking, in which case nonEmpty does the right thing by passing
-           -- Nothing.
-           ; match_result <- dsGRHSs ctxt grhss rhs_ty (NEL.nonEmpty match_deltas)
-           ; return ( EqnInfo { eqn_pats = upats
-                              , eqn_orig = FromSource
-                              , eqn_rhs = match_result }
-                    , rhss_deltas' ) }
+           -- pat_deltas is the covered set *after* matching the pattern, but
+           -- before any of the GRHSs. We extend the environment with pat_deltas
+           -- (via updPmDeltas) so that the where-clause of 'grhss' can profit
+           -- from that knowledge (#18533)
+           ; match_result <- updPmDeltas pat_deltas $
+                             dsGRHSs ctxt grhss rhs_ty rhss_deltas
+           ; return EqnInfo { eqn_pats = upats
+                            , eqn_orig = FromSource
+                            , eqn_rhs  = match_result } }
 
     handleWarnings = if isGenerated origin
                      then discardWarningsDs
                      else id
 
+    initDeltasMatches :: [LMatch GhcTc b] -> [(Deltas, NonEmpty Deltas)]
+    initDeltasMatches ms
+      = map (\(L _ m) -> (initDeltas, initDeltasGRHSs (m_grhss m))) ms
+
+    initDeltasGRHSs :: GRHSs GhcTc b -> NonEmpty Deltas
+    initDeltasGRHSs m = expectJust "GRHSs non-empty"
+                      $ NEL.nonEmpty
+                      $ replicate (length (grhssGRHSs m)) initDeltas
+
+
 matchEquations  :: HsMatchContext GhcRn
                 -> [MatchId] -> [EquationInfo] -> Type
                 -> DsM CoreExpr
diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs
index c78b35f6f2..43b4376752 100644
--- a/compiler/GHC/HsToCore/Monad.hs
+++ b/compiler/GHC/HsToCore/Monad.hs
@@ -407,7 +407,7 @@ getPmDeltas = do { env <- getLclEnv; return (dsl_deltas env) }
 -- | Set the pattern match oracle state within the scope of the given action.
 -- See 'dsl_deltas'.
 updPmDeltas :: Deltas -> DsM a -> DsM a
-updPmDeltas delta = updLclEnv (\env -> env { dsl_deltas = delta })
+updPmDeltas deltas = updLclEnv (\env -> env { dsl_deltas = deltas })
 
 getSrcSpanDs :: DsM SrcSpan
 getSrcSpanDs = do { env <- getLclEnv
diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index 564aa12f04..9d5f2e5581 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -13,7 +13,7 @@ Pattern Matching Coverage Checking.
 
 module GHC.HsToCore.PmCheck (
         -- Checking and printing
-        checkSingle, checkMatches, checkGuardMatches,
+        checkSingle, checkMatches, checkGRHSs,
         isMatchContextPmChecked,
 
         -- See Note [Type and Term Equality Propagation]
@@ -66,6 +66,7 @@ import GHC.Utils.Monad (concatMapM)
 import Control.Monad (when, forM_, zipWithM)
 import Data.List (elemIndex)
 import qualified Data.Semigroup as Semi
+import Data.List.NonEmpty (NonEmpty(..))
 
 {-
 This module checks pattern matches for:
@@ -150,13 +151,11 @@ data GrdTree
   -- ^ @Guard grd t@ will try to match @grd@ and on success continue to match
   -- @t@. Falls through if either match fails. Models left-to-right semantics
   -- of pattern matching.
-  | Sequence !GrdTree !GrdTree
-  -- ^ @Sequence l r@ first matches against @l@, and then matches all
-  -- fallen-through values against @r@. Models top-to-bottom semantics of
-  -- pattern matching.
-  | Empty
-  -- ^ A @GrdTree@ that always fails. Most useful for
-  -- Note [Checking EmptyCase]. A neutral element to 'Sequence'.
+  | Sequence ![GrdTree]
+  -- ^ @Sequence (t:ts)@ matches against @t@, and then matches all
+  -- fallen-through values against @Sequence ts@. Models top-to-bottom semantics
+  -- of pattern matching.
+  -- @Sequence []@ always fails; it is useful for Note [Checking EmptyCase].
 
 -- | The digest of 'checkGrdTree', representing the annotated pattern-match
 -- tree. 'redundantAndInaccessibleRhss' can figure out redundant and proper
@@ -170,10 +169,10 @@ data AnnotatedTree
   | MayDiverge !AnnotatedTree
   -- ^ Asserts that the tree may force diverging values, so not all of its
   -- clauses can be redundant.
-  | SequenceAnn !AnnotatedTree !AnnotatedTree
-  -- ^ Mirrors 'Sequence' for preserving the skeleton of a 'GrdTree's.
-  | EmptyAnn
-  -- ^ Mirrors 'Empty' for preserving the skeleton of a 'GrdTree's.
+  | SequenceAnn !Deltas ![AnnotatedTree]
+  -- ^ @SequenceAnn inc ts@ mirrors @'Sequence' ts@ for preserving the
+  -- skeleton of a 'GrdTree's @ts@. It also carries the set of incoming values
+  -- @inc@.
 
 pprRhsInfo :: RhsInfo -> SDoc
 pprRhsInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
@@ -189,23 +188,15 @@ instance Outputable GrdTree where
       collect_grds t             = (t, [])
       prefix []                  = []
       prefix (s:sdocs)           = char '|' <+> s : map (comma <+>) sdocs
-  -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
-  ppr t@Sequence{}    = braces (space <> fsep (punctuate semi (collect_seqs t)) <> space)
-    where
-      collect_seqs (Sequence l r) = collect_seqs l ++ collect_seqs r
-      collect_seqs t              = [ppr t]
-  ppr Empty          = text "<empty case>"
+  ppr (Sequence [])   = text "<empty case>"
+  ppr (Sequence ts)   = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
 
 instance Outputable AnnotatedTree where
-  ppr (AccessibleRhs _ info) = pprRhsInfo info
+  ppr (AccessibleRhs _delta info) = parens (ppr _delta) <+> pprRhsInfo info
   ppr (InaccessibleRhs info) = text "inaccessible" <+> pprRhsInfo info
   ppr (MayDiverge t)         = text "div" <+> ppr t
-    -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
-  ppr t@SequenceAnn{}        = braces (space <> fsep (punctuate semi (collect_seqs t)) <> space)
-    where
-      collect_seqs (SequenceAnn l r) = collect_seqs l ++ collect_seqs r
-      collect_seqs t                 = [ppr t]
-  ppr EmptyAnn               = text "<empty case>"
+  ppr (SequenceAnn _ [])       = text "<empty case>"
+  ppr (SequenceAnn _ ts)       = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
 
 -- | Lift 'addPmCts' over 'Deltas'.
 addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
@@ -264,7 +255,7 @@ checkSingle dflags ctxt@(DsMatchContext kind locn) var p = do
   -- Omitting checking this flag emits redundancy warnings twice in obscure
   -- cases like #17646.
   when (exhaustive dflags kind) $ do
-    -- TODO: This could probably call checkMatches, like checkGuardMatches.
+    -- TODO: This could probably call checkMatches, like checkGRHSs.
     missing   <- getPmDeltas
     tracePm "checkSingle: missing" (ppr missing)
     fam_insts <- dsGetFamInstEnvs
@@ -274,12 +265,12 @@ checkSingle dflags ctxt@(DsMatchContext kind locn) var p = do
 
 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
 -- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs.
-checkGuardMatches
+checkGRHSs
   :: HsMatchContext GhcRn         -- ^ Match context, for warning messages
   -> GRHSs GhcTc (LHsExpr GhcTc)  -- ^ The GRHSs to check
-  -> DsM [Deltas]                 -- ^ Covered 'Deltas' for each RHS, for long
+  -> DsM (NonEmpty Deltas)        -- ^ Covered 'Deltas' for each RHS, for long
                                   --   distance info
-checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
+checkGRHSs hs_ctx guards@(GRHSs _ grhss _) = do
     let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
         dsMatchContext = DsMatchContext hs_ctx combinedLoc
         match = L combinedLoc $
@@ -287,7 +278,8 @@ checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
                         , m_ctxt = hs_ctx
                         , m_pats = []
                         , m_grhss = guards }
-    checkMatches dsMatchContext [] [match]
+    [(_, deltas)] <- checkMatches dsMatchContext [] [match]
+    pure deltas
 
 -- | Check a list of syntactic /match/es (part of case, functions, etc.), each
 -- with a /pat/ and one or more /grhss/:
@@ -306,10 +298,9 @@ checkMatches
   :: DsMatchContext                  -- ^ Match context, for warnings messages
   -> [Id]                            -- ^ Match variables, i.e. x and y above
   -> [LMatch GhcTc (LHsExpr GhcTc)]  -- ^ List of matches
-  -> DsM [Deltas]                    -- ^ One covered 'Deltas' per RHS, for long
+  -> DsM [(Deltas, NonEmpty Deltas)] -- ^ One covered 'Deltas' per RHS, for long
                                      --   distance info.
 checkMatches ctxt vars matches = do
-  dflags <- getDynFlags
   tracePm "checkMatches" (hang (vcat [ppr ctxt
                                , ppr vars
                                , text "Matches:"])
@@ -322,25 +313,45 @@ checkMatches ctxt vars matches = do
     [] | [var] <- vars -> addPmCtDeltas init_deltas (PmNotBotCt var)
     _                  -> pure init_deltas
   fam_insts <- dsGetFamInstEnvs
-  grd_tree  <- mkGrdTreeMany [] <$> mapM (translateMatch fam_insts vars) matches
+  grd_tree  <- translateMatches fam_insts vars matches
   res <- checkGrdTree grd_tree missing
 
+  dflags <- getDynFlags
   dsPmWarn dflags ctxt vars res
 
-  return (extractRhsDeltas init_deltas (cr_clauses res))
+  return (extractRhsDeltas (cr_clauses res))
 
--- | Extract the 'Deltas' reaching the RHSs of the 'AnnotatedTree'.
+-- | Extract the 'Deltas' reaching the RHSs of the 'AnnotatedTree' for a match
+-- group.
 -- For 'AccessibleRhs's, this is stored in the tree node, whereas
 -- 'InaccessibleRhs's fall back to the supplied original 'Deltas'.
 -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@.
-extractRhsDeltas :: Deltas -> AnnotatedTree -> [Deltas]
-extractRhsDeltas orig_deltas = fromOL . go
+extractRhsDeltas :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
+extractRhsDeltas = go_matches
   where
-    go (AccessibleRhs deltas _) = unitOL deltas
-    go (InaccessibleRhs _)      = unitOL orig_deltas
-    go (MayDiverge t)           = go t
-    go (SequenceAnn l r)        = go l Semi.<> go r
-    go EmptyAnn                 = nilOL
+    go_matches :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
+    go_matches (SequenceAnn def ts) = map (go_match def) ts -- -XEmptyCase handled here!
+    go_matches t                    = pprPanic "extractRhsDeltas.go_matches" (text "Matches must start with SequenceAnn. But was" $$ ppr t)
+
+    go_match :: Deltas -> AnnotatedTree -> (Deltas, NonEmpty Deltas)
+    -- There is no -XEmptyCase at this level, only at the Matches level. So @ts@
+    -- is non-empty!
+    go_match def (SequenceAnn pat ts) = (pat, foldMap1 (text "go_match: empty SequenceAnn") (go_grhss def) ts)
+    go_match def (MayDiverge t)       = go_match def t
+    -- Even if there's only a single GRHS, we wrap it in a SequenceAnn for the
+    -- Deltas covered by the pattern. So the remaining cases are impossible!
+    go_match _   t                    = pprPanic "extractRhsDeltas.go_match" (text "Single GRHS must be wrapped in SequenceAnn. But got " $$ ppr t)
+
+    go_grhss :: Deltas -> AnnotatedTree -> NonEmpty Deltas
+    -- There is no -XEmptyCase at this level, only at the Matches level. So @ts@
+    -- is non-empty!
+    go_grhss def (SequenceAnn _ ts)       = foldMap1 (text "go_grhss: empty SequenceAnn") (go_grhss def) ts
+    go_grhss def (MayDiverge t)           = go_grhss def t
+    go_grhss _   (AccessibleRhs deltas _) = deltas :| []
+    go_grhss def (InaccessibleRhs _)      = def    :| []
+
+    foldMap1 msg _ []     = pprPanic "extractRhsDeltas.foldMap1" msg
+    foldMap1 _   f (x:xs) = foldl' (\acc x -> acc Semi.<> f x) (f x) xs
 
 {- Note [Checking EmptyCase]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -629,34 +640,43 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
       --      1.         2.           3.
       pure (con_grd : bang_grds ++ arg_grds)
 
-mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
-mkGrdTreeRhs sdoc = foldr Guard (Rhs sdoc)
-
-mkGrdTreeMany :: GrdVec -> [GrdTree] -> GrdTree
-mkGrdTreeMany _    []    = Empty
-mkGrdTreeMany grds trees = foldr Guard (foldr1 Sequence trees) grds
+-- | Translate a the 'Match'es of a 'MatchGroup'
+translateMatches :: FamInstEnvs -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)]
+                 -> DsM GrdTree
+translateMatches fam_insts vars matches =
+  -- It's important that we wrap a 'Sequence' even if it only wraps a singleton.
+  -- 'extractRhsDeltas' needs this to recover 'MatchGroup' structure.
+  Sequence <$> traverse (translateMatch fam_insts vars) matches
 
 -- Translate a single match
 translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc)
                -> DsM GrdTree
 translateMatch fam_insts vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
-  pats'   <- concat <$> zipWithM (translateLPat fam_insts) vars pats
-  grhss' <- mapM (translateLGRHS fam_insts match_loc pats) (grhssGRHSs grhss)
-  -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss, ppr grhss'])
-  return (mkGrdTreeMany pats' grhss')
+  pats'  <- concat <$> zipWithM (translateLPat fam_insts) vars pats
+  grhss' <- translateGRHSs fam_insts match_loc (sep (map ppr pats)) grhss
+  -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
+  return (foldr Guard grhss' pats')
 
--- -----------------------------------------------------------------------
--- * Transform source guards (GuardStmt Id) to simpler PmGrds
+mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
+mkGrdTreeRhs sdoc = foldr Guard (Rhs sdoc)
+
+translateGRHSs :: FamInstEnvs -> SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM GrdTree
+translateGRHSs fam_insts match_loc pp_pats grhss =
+  -- It's important that we wrap a 'Sequence' even if it only wraps a singleton.
+  -- 'extractRhsDeltas' needs this to recover 'GRHSs' structure.
+  Sequence <$> traverse (translateLGRHS fam_insts match_loc pp_pats) (grhssGRHSs grhss)
 
 -- | Translate a guarded right-hand side to a single 'GrdTree'
-translateLGRHS :: FamInstEnvs -> SrcSpan -> [LPat GhcTc] -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
-translateLGRHS fam_insts match_loc pats (L _loc (GRHS _ gs _)) =
-  -- _loc apparently points to the match separator that comes after the guards..
+translateLGRHS :: FamInstEnvs -> SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
+translateLGRHS fam_insts match_loc pp_pats (L _loc (GRHS _ gs _)) =
+  -- _loc points to the match separator (ie =, ->) that comes after the guards..
   mkGrdTreeRhs loc_sdoc <$> concatMapM (translateGuard fam_insts . unLoc) gs
     where
       loc_sdoc
-        | null gs   = L match_loc (sep (map ppr pats))
-        | otherwise = L grd_loc   (sep (map ppr pats) <+> vbar <+> interpp'SP gs)
+        -- pp_pats is the space-separated pattern of the current Match this
+        -- GRHS belongs to, so the @A B x@ part in @A B x | 0 <- x@.
+        | null gs   = L match_loc pp_pats
+        | otherwise = L grd_loc   (pp_pats <+> vbar <+> interpp'SP gs)
       L grd_loc _ = head gs
 
 -- | Translate a guard statement to a 'GrdVec'
@@ -971,6 +991,7 @@ checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
   unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
   deltas' <- addPmCtsDeltas deltas $
     listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con tvs args
+  -- tracePm "checkGrdTree:Con" (ppr deltas $$ ppr x $$ ppr con $$ ppr dicts $$ ppr deltas')
   CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
   limit <- maxPmCheckModels <$> getDynFlags
   let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
@@ -979,19 +1000,21 @@ checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
     , cr_uncov = unc'
     , cr_approx = prec Semi.<> prec' }
 -- Sequence: Thread residual uncovered sets from equation to equation
-checkGrdTree' (Sequence l r) unc_0 = do
-  CheckResult l' unc_1 prec_l <- checkGrdTree' l unc_0
-  CheckResult r' unc_2 prec_r <- checkGrdTree' r unc_1
-  pure CheckResult
-    { cr_clauses = SequenceAnn l' r'
-    , cr_uncov = unc_2
-    , cr_approx = prec_l Semi.<> prec_r }
--- Empty: Fall through for all values
-checkGrdTree' Empty unc = do
-  pure CheckResult
-    { cr_clauses = EmptyAnn
-    , cr_uncov = unc
-    , cr_approx = Precise }
+checkGrdTree' (Sequence ts) init_unc = go [] init_unc Precise ts
+  where
+    -- | Accumulates a CheckResult. Its type is more like
+    -- @CheckResult -> [GrdTree] -> CheckResult@, but cr_clauses is a single
+    -- 'AnnotatedTree', not a list thereof. Hence 3 parameters to thread the
+    -- fields.
+    go :: [AnnotatedTree] -> Deltas -> Precision -> [GrdTree] -> DsM CheckResult
+    -- No cases left: Fall through for all values
+    go ts' unc prec [] = pure CheckResult
+                          { cr_clauses = SequenceAnn init_unc (reverse ts')
+                          , cr_uncov = unc
+                          , cr_approx = prec }
+    go ts' unc prec (t:ts) = do
+      CheckResult t' unc_1 prec_t <- checkGrdTree' t unc
+      go (t':ts') unc_1 (prec_t Semi.<> prec) ts
 
 -- | Print diagnostic info and actually call 'checkGrdTree''.
 checkGrdTree :: GrdTree -> Deltas -> DsM CheckResult
@@ -1117,8 +1140,7 @@ redundantAndInaccessibleRhss tree = (fromOL ol_red, fromOL ol_inacc)
       (acc, inacc, red)
         | isNilOL acc && isNilOL inacc -> (nilOL, red, nilOL)
       res                              -> res
-    go (SequenceAnn l r)      = go l Semi.<> go r
-    go EmptyAnn               = (nilOL,       nilOL, nilOL)
+    go (SequenceAnn _ ts)     = foldMap go ts
 
 {- Note [Determining inaccessible clauses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 0a03b05228..bf21c8594b 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -1070,7 +1070,8 @@ ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env reps }
   = runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env)
   where
     set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env reps }
-    go vi = MaybeT (ensureInhabited delta vi)
+    go vi = MaybeT $
+      initPossibleMatches (delta_ty_st delta) vi >>= ensureInhabited delta
 
 --------------------------------------
 -- * Term oracle unification procedure
@@ -1668,7 +1669,7 @@ addCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
 addCoreCt delta x e = do
   dflags <- getDynFlags
   let e' = simpleOptExpr dflags e
-  lift $ tracePm "addCoreCt" (ppr x $$ ppr e $$ ppr e')
+  lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
   execStateT (core_expr x e') delta
   where
     -- | Takes apart a 'CoreExpr' and tries to extract as much information about
diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index 600a84eb94..06a75e2a1f 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -779,7 +780,9 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
                                            Just (dataConWrapId con, dataConNonlinearType con)
                                        _ -> Nothing }
             where name = case hfc of
+#if __GLASGOW_HASKELL__ <= 810
                            IdHFCand id -> idName id
+#endif
                            GreHFCand gre -> gre_name gre
                            NameHFCand name -> name
           discard_it = go subs seen maxleft ty elts
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 410844793f..3a1ab09c9b 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1079,7 +1079,9 @@ tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
                   HsUnboxedTuple    -> UnboxedTuple
                   HsBoxedTuple      -> BoxedTuple
                   HsConstraintTuple -> ConstraintTuple
+#if __GLASGOW_HASKELL__ <= 810
                   _                 -> panic "tc_hs_type HsTupleTy"
+#endif
 
 tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
   = do { let arity = length hs_tys
diff --git a/testsuite/tests/pmcheck/should_compile/T18533.hs b/testsuite/tests/pmcheck/should_compile/T18533.hs
new file mode 100644
index 0000000000..3b4fdf8b89
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T18533.hs
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE GADTs, DataKinds, TypeFamilies, BangPatterns #-}
+
+module T18533 where
+
+data SBool (b :: Bool) where
+  STrue  :: SBool 'True
+  SFalse :: SBool 'False
+
+type family Fam (b :: Bool)
+type instance Fam 'True = T
+
+data T = T Bool
+
+f :: Fam b -> SBool b -> Bool
+f !t s = case s of
+    STrue -> a where a = case t of T a -> a
+    _     -> False
+
+
+g :: Bool -> Bool
+g x = case x of
+  True -> a where a = case x of True -> False
+  False -> True
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 57527977ff..054ad82873 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -122,6 +122,8 @@ test('T18049', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T18478', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18533', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,