PmCheck: Big refactor of module structure

  * Move everything from `GHC.HsToCore.PmCheck.*` to
    `GHC.HsToCore.Pmc.*` in analogy to `GHC.Tc`, rename exported
    `covCheck*` functions to `pmc*`
  * Rename `Pmc.Oracle` to `Pmc.Solver`
  * Split off the LYG desugaring and checking steps into their own
    modules (`Pmc.Desugar` and `Pmc.Check` respectively)
  * Split off a `Pmc.Utils` module with stuff shared by
    `Pmc.{,Desugar,Check,Solver}`
  * Move `Pmc.Types` to `Pmc.Solver.Types`, add a new `Pmc.Types` module
    with all the LYG types, which form the interfaces between
    `Pmc.{Desugar,Check,Solver,}`.

18 files changed, 2001 insertions, 1826 deletions

diff --git a/compiler/GHC/Hs/Extension.hs b/compiler/GHC/Hs/Extension.hs
index db1738ec02..119997cdb1 100644
--- a/compiler/GHC/Hs/Extension.hs
+++ b/compiler/GHC/Hs/Extension.hs
@@ -247,7 +247,7 @@ NoExtCon. But since (1) the field is strict and (2) NoExtCon is an empty data
 type, there is no possible way to reach the right-hand side of the XHsDecl
 case. As a result, the coverage checker concludes that the XHsDecl case is
 inaccessible, so it can be removed.
-(See Note [Strict argument type constraints] in GHC.HsToCore.PmCheck.Oracle for
+(See Note [Strict argument type constraints] in GHC.HsToCore.Pmc.Solver for
 more on how this works.)
 
 Bottom line: if you add a TTG extension constructor that uses NoExtCon, make
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 3adecc0d5b..53926361fc 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 ( addTyCs, covCheckGRHSs )
+import GHC.HsToCore.Pmc ( addTyCs, pmcGRHSs )
 
 import GHC.Hs             -- lots of things
 import GHC.Core           -- lots of things
@@ -159,7 +159,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
                           -- oracle.
                           -- addTyCs: Add type evidence to the refinement type
                           --            predicate of the coverage checker
-                          -- See Note [Long-distance information] in "GHC.HsToCore.PmCheck"
+                          -- See Note [Long-distance information] in "GHC.HsToCore.Pmc"
                           matchWrapper
                            (mkPrefixFunRhs (L loc (idName fun)))
                            Nothing matches
@@ -185,7 +185,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
 dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss
                          , pat_ext = ty
                          , pat_ticks = (rhs_tick, var_ticks) })
-  = do  { rhss_nablas <- covCheckGRHSs PatBindGuards grhss
+  = do  { rhss_nablas <- pmcGRHSs PatBindGuards grhss
         ; body_expr <- dsGuarded grhss ty rhss_nablas
         ; let body' = mkOptTickBox rhs_tick body_expr
               pat'  = decideBangHood dflags pat
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 783e8b098b..5f1aa24035 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 ( addTyCs, covCheckGRHSs )
+import GHC.HsToCore.Pmc ( addTyCs, pmcGRHSs )
 import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Core.FamInstEnv( topNormaliseType )
@@ -215,7 +215,7 @@ dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss
                         , pat_ext = ty }) body
   =     -- let C x# y# = rhs in body
         -- ==> case rhs of C x# y# -> body
-    do { match_nablas <- covCheckGRHSs PatBindGuards grhss
+    do { match_nablas <- pmcGRHSs PatBindGuards grhss
        ; rhs          <- dsGuarded grhss ty match_nablas
        ; let upat = unLoc pat
              eqn = EqnInfo { eqn_pats = [upat],
@@ -490,7 +490,7 @@ dsExpr (HsMultiIf res_ty alts)
 
   | otherwise
   = do { let grhss = GRHSs noExtField alts (noLoc emptyLocalBinds)
-       ; rhss_nablas  <- covCheckGRHSs IfAlt grhss
+       ; rhss_nablas  <- pmcGRHSs IfAlt grhss
        ; match_result <- dsGRHSs IfAlt grhss res_ty rhss_nablas
        ; error_expr   <- mkErrorExpr
        ; extractMatchResult match_result error_expr }
diff --git a/compiler/GHC/HsToCore/GuardedRHSs.hs b/compiler/GHC/HsToCore/GuardedRHSs.hs
index 14b01f440a..c2ac2f0ef8 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 ( Nablas )
+import GHC.HsToCore.Pmc.Types ( Nablas )
 import GHC.Core.Type ( Type )
 import GHC.Utils.Misc
 import GHC.Types.SrcLoc
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index a33e3d9b41..afc31ec58d 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -34,8 +34,8 @@ import GHC.Hs
 import GHC.Tc.Utils.Zonk
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.Monad
-import GHC.HsToCore.PmCheck
-import GHC.HsToCore.PmCheck.Types ( Nablas, initNablas )
+import GHC.HsToCore.Pmc
+import GHC.HsToCore.Pmc.Types ( Nablas, initNablas )
 import GHC.Core
 import GHC.Types.Literal
 import GHC.Core.Utils
@@ -771,7 +771,7 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches
         ; matches_nablas <- if isMatchContextPmChecked dflags origin ctxt
             then addHsScrutTmCs mb_scr new_vars $
                  -- See Note [Long-distance information]
-                 covCheckMatches (DsMatchContext ctxt locn) new_vars matches
+                 pmcMatches (DsMatchContext ctxt locn) new_vars matches
             else pure (initNablasMatches matches)
 
         ; eqns_info   <- zipWithM mk_eqn_info matches matches_nablas
@@ -881,7 +881,7 @@ matchSinglePatVar var mb_scrut ctx pat ty match_result
        -- Pattern match check warnings
        ; when (isMatchContextPmChecked dflags FromSource ctx) $
            addCoreScrutTmCs mb_scrut [var] $
-           covCheckPatBind (DsMatchContext ctx locn) var (unLoc pat)
+           pmcPatBind (DsMatchContext ctx locn) var (unLoc pat)
 
        ; let eqn_info = EqnInfo { eqn_pats = [unLoc (decideBangHood dflags pat)]
                                 , eqn_orig = FromSource
diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs
index 0c9717d4eb..fce4e2d580 100644
--- a/compiler/GHC/HsToCore/Monad.hs
+++ b/compiler/GHC/HsToCore/Monad.hs
@@ -75,7 +75,7 @@ import GHC.Core.DataCon
 import GHC.Core.ConLike
 import GHC.Core.TyCon
 import GHC.HsToCore.Types
-import GHC.HsToCore.PmCheck.Types
+import GHC.HsToCore.Pmc.Solver.Types (Nablas, initNablas)
 import GHC.Types.Id
 import GHC.Unit.Module
 import GHC.Utils.Outputable
diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
deleted file mode 100644
index bad245cc6e..0000000000
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ /dev/null
@@ -1,1446 +0,0 @@
-{-# LANGUAGE CPP                        #-}
-{-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE TupleSections              #-}
-{-# LANGUAGE ViewPatterns               #-}
-{-# LANGUAGE MultiWayIf                 #-}
-{-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE DeriveFunctor              #-}
-{-# LANGUAGE NamedFieldPuns             #-}
-{-# LANGUAGE FlexibleInstances          #-}
-
--- | This module coverage checks pattern matches. It finds
---
---     * Uncovered patterns, certifying non-exhaustivity
---     * Redundant equations
---     * Equations with an inaccessible right-hand-side
---
--- The algorithm is based on the paper
--- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989)
---
--- There is an overview Figure 2 in there that's probably helpful.
--- Here is an overview of how it's implemented, which follows the structure of
--- the entry points such as 'covCheckMatches':
---
---  1. Desugar source syntax (like 'LMatch') to guard tree variants (like
---     'GrdMatch'), with one of the desugaring functions (like 'desugarMatch').
---     Follows Section 3.1 in the paper.
---  2. Coverage check guard trees (with a function like 'checkMatch') to get a
---     'CheckResult', containing
---       a. The set of uncovered values, 'cr_uncov'
---       b. And an annotated tree variant (like 'AnnMatch') that captures
---          redundancy and inaccessibility information as 'RedSets' annotations
---     Basically the UA function from Section 5.1. The Normalised Refinement
---     Types 'Nablas' are maintained in "GHC.HsToCore.PmCheck.Oracle".
---  3. Collect redundancy information into a 'CIRB' with a function such
---     as 'cirbsMatch'. Follows the R function from Figure 6 of the paper.
---  4. Format and report uncovered patterns and redundant equations ('CIRB')
---     with 'formatReportWarnings'. Basically job of the G function, plus proper
---     pretty printing of the warnings (Section 5.4 of the paper).
---  5. Return 'Nablas' reaching syntactic sub-components for
---     Note [Long-distance information]. Collected by functions such as
---     'ldiMatch'. See Section 4.1 of the paper.
-module GHC.HsToCore.PmCheck (
-        -- Checking and printing
-        covCheckPatBind, covCheckMatches, covCheckGRHSs,
-        isMatchContextPmChecked,
-
-        -- See Note [Long-distance information]
-        addTyCs, addCoreScrutTmCs, addHsScrutTmCs
-    ) where
-
-#include "HsVersions.h"
-
-import GHC.Prelude
-
-import GHC.HsToCore.PmCheck.Types
-import GHC.HsToCore.PmCheck.Oracle
-import GHC.HsToCore.PmCheck.Ppr
-import GHC.Types.Basic (Origin(..), isGenerated)
-import GHC.Core (CoreExpr, Expr(Var,App))
-import GHC.Data.FastString (unpackFS, lengthFS)
-import GHC.Driver.Session
-import GHC.Hs
-import GHC.Tc.Utils.Zonk (shortCutLit)
-import GHC.Types.Id
-import GHC.Core.ConLike
-import GHC.Types.Name
-import GHC.Builtin.Types
-import GHC.Types.SrcLoc
-import GHC.Utils.Misc
-import GHC.Utils.Outputable
-import GHC.Utils.Panic
-import GHC.Core.DataCon
-import GHC.Types.Var (EvVar)
-import GHC.Core.Coercion
-import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper)
-import GHC.Tc.Utils.TcType (evVarPred)
-import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr)
-import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper)
-import GHC.HsToCore.Utils (selectMatchVar)
-import GHC.HsToCore.Match.Literal (dsLit, dsOverLit)
-import GHC.HsToCore.Monad
-import GHC.Data.Bag
-import GHC.Data.IOEnv (unsafeInterleaveM)
-import GHC.Data.OrdList
-import GHC.Core.TyCo.Rep
-import GHC.Core.Type
-import GHC.HsToCore.Utils       (isTrueLHsExpr)
-import GHC.Data.Maybe
-import qualified GHC.LanguageExtensions as LangExt
-import GHC.Utils.Monad (concatMapM, mapMaybeM)
-
-import Control.Monad (when, forM_, zipWithM)
-import Data.List (elemIndex)
-import qualified Data.Semigroup as Semi
-import Data.List.NonEmpty ( NonEmpty(..) )
-import qualified Data.List.NonEmpty as NE
-import Data.Coerce
-
---
--- * Exported entry points to the checker
---
-
--- | A non-empty delta that is initialised from the ambient refinement type
--- capturing long-distance information, or the trivially habitable 'Nablas' if
--- the former is uninhabited.
--- See Note [Recovering from unsatisfiable pattern-matching constraints].
-getLdiNablas :: DsM Nablas
-getLdiNablas = do
-  nablas <- getPmNablas
-  isInhabited nablas >>= \case
-    True  -> pure nablas
-    False -> pure initNablas
-
--- | Check a pattern binding (let, where) for exhaustiveness.
-covCheckPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
--- See Note [covCheckPatBind only checks PatBindRhs]
-covCheckPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
-  missing   <- getLdiNablas
-  pat_bind <- desugarPatBind loc var p
-  tracePm "covCheckPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
-  result <- unCA (checkPatBind pat_bind) missing
-  tracePm "}: " (ppr (cr_uncov result))
-  formatReportWarnings cirbsPatBind ctxt [var] result
-covCheckPatBind _ _ _ = pure ()
-
--- | Exhaustive for guard matches, is used for guards in pattern bindings and
--- in @MultiIf@ expressions. Returns the 'Nablas' covered by the RHSs.
-covCheckGRHSs
-  :: HsMatchContext GhcRn         -- ^ Match context, for warning messages
-  -> GRHSs GhcTc (LHsExpr GhcTc)  -- ^ The GRHSs to check
-  -> DsM (NonEmpty Nablas)        -- ^ Covered 'Nablas' for each RHS, for long
-                                  --   distance info
-covCheckGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
-  let combined_loc = foldl1 combineSrcSpans (map getLoc grhss)
-      ctxt = DsMatchContext hs_ctxt combined_loc
-  matches <- desugarGRHSs combined_loc empty guards
-  missing   <- getLdiNablas
-  tracePm "covCheckGRHSs" (hang (vcat [ppr ctxt
-                                , text "Guards:"])
-                                2
-                                (pprGRHSs hs_ctxt guards $$ ppr missing))
-  result <- unCA (checkGRHSs matches) missing
-  tracePm "}: " (ppr (cr_uncov result))
-  formatReportWarnings cirbsGRHSs ctxt [] result
-  return (ldiGRHS <$> cr_ret result)
-
--- | Check a list of syntactic 'Match'es (part of case, functions, etc.), each
--- with a 'Pat' and one or more 'GRHSs':
---
--- @
---   f x y | x == y    = 1   -- match on x and y with two guarded RHSs
---         | otherwise = 2
---   f _ _             = 3   -- clause with a single, un-guarded RHS
--- @
---
--- Returns one non-empty 'Nablas' for 1.) each pattern of a 'Match' and 2.)
--- each of a 'Match'es 'GRHS' for Note [Long-distance information].
---
--- Special case: When there are /no matches/, then the functionassumes it
--- checks and @-XEmptyCase@ with only a single match variable.
--- See Note [Checking EmptyCase].
-covCheckMatches
-  :: DsMatchContext                  -- ^ Match context, for warnings messages
-  -> [Id]                            -- ^ Match variables, i.e. x and y above
-  -> [LMatch GhcTc (LHsExpr GhcTc)]  -- ^ List of matches
-  -> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and
-                                     --   GRHS, for long distance info.
-covCheckMatches ctxt vars matches = 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!
-  !missing   <- getLdiNablas
-  tracePm "covCheckMatches {" $
-          hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
-               2
-               (vcat (map ppr matches) $$ ppr missing)
-  case NE.nonEmpty matches of
-    Nothing -> do
-      -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
-      let var = only vars
-      empty_case <- desugarEmptyCase var
-      result <- unCA (checkEmptyCase empty_case) missing
-      tracePm "}: " (ppr (cr_uncov result))
-      formatReportWarnings cirbsEmptyCase ctxt vars result
-      return []
-    Just matches -> do
-      matches <- desugarMatches vars matches
-      result <- unCA (checkMatchGroup matches) missing
-      tracePm "}: " (ppr (cr_uncov result))
-      formatReportWarnings cirbsMatchGroup ctxt vars result
-      return (NE.toList (ldiMatchGroup (cr_ret result)))
-
-{- Note [covCheckPatBind only checks PatBindRhs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-@covCheckPatBind@'s sole purpose is to check vanilla pattern bindings, like
-@x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
-But its caller is also called for individual pattern guards in a @StmtCtxt@.
-For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
-go through this function. It makes no sense to do coverage checking there:
-  * Pattern guards may well fail. Fall-through is not an unrecoverable panic,
-    but rather behavior the programmer expects, so inexhaustivity should not be
-    reported.
-  * Redundancy is already reported for the whole GRHS via one of the other
-    exported coverage checking functions. Also reporting individual redundant
-    guards is... redundant. See #17646.
-Note that we can't just omit checking of @StmtCtxt@ altogether (by adjusting
-'isMatchContextPmChecked'), because that affects the other checking functions,
-too.
-
-Note [Checking EmptyCase]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--XEmptyCase is useful for matching on empty data types like 'Void'. For example,
-the following is a complete match:
-
-    f :: Void -> ()
-    f x = case x of {}
-
-Really, -XEmptyCase is the only way to write a program that at the same time is
-safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
-(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
-exception into divergence (@f x = f x@).
-
-Semantically, unlike every other case expression, -XEmptyCase is strict in its
-match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
-initial Nabla and check if there are any values left to match on.
--}
-
---
--- * Guard language
---
-
--- | A very simple language for pattern guards. Let bindings, bang patterns,
--- and matching variables against flat constructor patterns.
-data PmGrd
-  = -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
-    -- The @args@ are bound in this construct, the @x@ is just a use.
-    -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
-    PmCon {
-      pm_id          :: !Id,
-      pm_con_con     :: !PmAltCon,
-      pm_con_tvs     :: ![TyVar],
-      pm_con_dicts   :: ![EvVar],
-      pm_con_args    :: ![Id]
-    }
-
-    -- | @PmBang x@ corresponds to a @seq x True@ guard.
-    -- If the extra 'SrcInfo' is present, the bang guard came from a source
-    -- bang pattern, in which case we might want to report it as redundant.
-    -- See Note [Dead bang patterns].
-  | PmBang {
-      pm_id   :: !Id,
-      _pm_loc :: !(Maybe SrcInfo)
-    }
-
-    -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
-    -- /binds/ @x@.
-  | PmLet {
-      pm_id        :: !Id,
-      _pm_let_expr :: !CoreExpr
-    }
-
--- | Should not be user-facing.
-instance Outputable PmGrd where
-  ppr (PmCon x alt _tvs _con_dicts con_args)
-    = hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
-  ppr (PmBang x _loc) = char '!' <> ppr x
-  ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
-
-type GrdVec = [PmGrd]
-
-data Precision = Approximate | Precise
-  deriving (Eq, Show)
-
-instance Outputable Precision where
-  ppr = text . show
-
-instance Semi.Semigroup Precision where
-  Precise <> Precise = Precise
-  _       <> _       = Approximate
-
-instance Monoid Precision where
-  mempty = Precise
-  mappend = (Semi.<>)
-
---
--- * Guard tree language
---
-
--- | Means by which we identify a source construct for later pretty-printing in
--- a warning message. 'SDoc' for the equation to show, 'Located' for the
--- location.
-type SrcInfo = Located SDoc
-
--- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
--- (later digested into a 'CIRB').
-data RedSets
-  = RedSets
-  { rs_cov :: !Nablas
-  -- ^ The /Covered/ set; the set of values reaching a particular program
-  -- point.
-  , rs_div :: !Nablas
-  -- ^ The /Diverging/ set; empty if no match can lead to divergence.
-  --   If it wasn't empty, we have to turn redundancy warnings into
-  --   inaccessibility warnings for any subclauses.
-  , rs_bangs :: !(OrdList (Nablas, SrcInfo))
-  -- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points
-  -- a bang pattern in source that is redundant. See Note [Dead bang patterns].
-  }
-
--- The following two type synonyms instantiate our tree structures to guard
--- trees and annotated trees, respectively, by giving the types to attach as
--- payload.
-
--- | Used as tree payload pre-checking. The LYG guards to check.
-type Pre = [PmGrd]
-
--- | Used as tree payload post-checking. The redundancy info we elaborated.
-type Post = RedSets
-
--- | A guard tree denoting 'MatchGroup'.
-newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
-
--- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
--- GRHS.
-data PmMatch p = PmMatch { pm_pats :: !p, pm_grhss :: !(NonEmpty (PmGRHS p)) }
-
--- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
--- useful for printing out in warnings messages.
-data PmGRHS p = PmGRHS { pg_grds :: !p, pg_rhs :: !SrcInfo }
-
--- | A guard tree denoting an -XEmptyCase.
-newtype PmEmptyCase = PmEmptyCase { pe_var :: Id }
-
--- | A guard tree denoting a pattern binding.
-newtype PmPatBind p =
-  -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
-  -- rather than on the pattern bindings.
-  PmPatBind (PmGRHS p)
-
-emptyRedSets :: RedSets
--- Semigroup instance would be misleading!
-emptyRedSets = RedSets mempty mempty mempty
-
-pprSrcInfo :: SrcInfo -> SDoc
-pprSrcInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
-pprSrcInfo (L s _)                   = ppr s
-
--- | Format LYG guards as @| True <- x, let x = 42, !z@
-pprLygGuards :: [PmGrd] -> SDoc
-pprLygGuards []     = empty
-pprLygGuards (g:gs) = fsep (char '|' <+> ppr g : map ((comma <+>) . ppr) gs)
-
--- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
--- @{ <first alt>; ...; <last alt> }@
-pprLygSequence :: Outputable a => NonEmpty a -> SDoc
-pprLygSequence (NE.toList -> as) =
-  braces (space <> fsep (punctuate semi (map ppr as)) <> space)
-
-instance Outputable (PmMatchGroup Pre) where
-  ppr (PmMatchGroup matches) = pprLygSequence matches
-
-instance Outputable (PmMatch Pre) where
-  ppr (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
-    pprLygGuards grds <+> ppr grhss
-
-instance Outputable (PmGRHS Pre) where
-  ppr (PmGRHS { pg_grds = grds, pg_rhs = rhs }) =
-    pprLygGuards grds <+> text "->" <+> pprSrcInfo rhs
-
-instance Outputable (PmPatBind Pre) where
-  ppr (PmPatBind PmGRHS { pg_grds = grds, pg_rhs = bind }) =
-    ppr bind <+> pprLygGuards grds <+> text "=" <+> text "..."
-
-instance Outputable PmEmptyCase where
-  ppr (PmEmptyCase { pe_var = var }) =
-    text "<empty case on " <> ppr var <> text ">"
-
-pprRedSets :: RedSets -> SDoc
--- It's useful to change this definition for different verbosity levels in
--- printf-debugging
-pprRedSets RedSets { rs_cov = _cov, rs_div = _div, rs_bangs = _bangs }
-  = empty
-
-instance Outputable (PmMatchGroup Post) where
-  ppr (PmMatchGroup matches) = pprLygSequence matches
-
-instance Outputable (PmMatch Post) where
-  ppr (PmMatch { pm_pats = red, pm_grhss = grhss }) =
-    pprRedSets red <+> ppr grhss
-
-instance Outputable (PmGRHS Post) where
-  ppr (PmGRHS { pg_grds = red, pg_rhs = rhs }) =
-    pprRedSets red <+> text "->" <+> pprSrcInfo rhs
-
-{- Note [Dead bang patterns]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  f :: Bool -> Int
-  f True = 1
-  f !x   = 2
-
-Whenever we fall through to the second equation, we will already have evaluated
-the argument. Thus, the bang pattern serves no purpose and should be warned
-about. We call this kind of bang patterns "dead". Dead bangs are the ones
-that under no circumstances can force a thunk that wasn't already forced.
-Dead bangs are a form of redundant bangs; see below.
-
-We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
-where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
-dead. Such a dead bang is then indicated in the annotated pattern-match tree by
-a 'RedundantSrcBang' wrapping. In 'redundantAndInaccessibles', we collect
-all dead bangs to warn about.
-
-Note that we don't want to warn for a dead bang that appears on a redundant
-clause. That is because in that case, we recommend to delete the clause wholly,
-including its leading pattern match.
-
-Dead bang patterns are redundant. But there are bang patterns which are
-redundant that aren't dead, for example
-
-  f !() = 0
-
-the bang still forces the match variable, before we attempt to match on (). But
-it is redundant with the forcing done by the () match. We currently don't
-detect redundant bangs that aren't dead.
--}
-
---
--- * Desugaring source syntax to guard trees
---
-
--- | Smart constructor that eliminates trivial lets
-mkPmLetVar :: Id -> Id -> GrdVec
-mkPmLetVar x y | x == y = []
-mkPmLetVar x y          = [PmLet x (Var y)]
-
--- | ADT constructor pattern => no existentials, no local constraints
-vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
-vanillaConGrd scrut con arg_ids =
-  PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
-        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
-
--- | Creates a 'GrdVec' refining a match var of list type to a list,
--- where list fields are matched against the incoming tagged 'GrdVec's.
--- For example:
---   @mkListGrds "a" "[(x, True <- x),(y, !y)]"@
--- to
---   @"[(x:b) <- a, True <- x, (y:c) <- b, !y, [] <- c]"@
--- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match
--- variable.
-mkListGrds :: Id -> [(Id, GrdVec)] -> DsM GrdVec
--- See Note [Order of guards matter] for why we need to intertwine guards
--- on list elements.
-mkListGrds a []                  = pure [vanillaConGrd a nilDataCon []]
-mkListGrds a ((x, head_grds):xs) = do
-  b <- mkPmId (idType a)
-  tail_grds <- mkListGrds b xs
-  pure $ vanillaConGrd a consDataCon [x, b] : head_grds ++ tail_grds
-
--- | Create a 'GrdVec' refining a match variable to a 'PmLit'.
-mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
-mkPmLitGrds x (PmLit _ (PmLitString s)) = do
-  -- We desugar String literals to list literals for better overlap reasoning.
-  -- It's a little unfortunate we do this here rather than in
-  -- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and
-  -- 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much simpler
-  -- here. See Note [Representation of Strings in TmState] in
-  -- GHC.HsToCore.PmCheck.Oracle
-  vars <- traverse mkPmId (take (lengthFS s) (repeat charTy))
-  let mk_char_lit y c = mkPmLitGrds y (PmLit charTy (PmLitChar c))
-  char_grdss <- zipWithM mk_char_lit vars (unpackFS s)
-  mkListGrds x (zip vars char_grdss)
-mkPmLitGrds x lit = do
-  let grd = PmCon { pm_id = x
-                  , pm_con_con = PmAltLit lit
-                  , pm_con_tvs = []
-                  , pm_con_dicts = []
-                  , pm_con_args = [] }
-  pure [grd]
-
--- | @desugarPat _ x pat@ transforms @pat@ into a 'GrdVec', where
--- the variable representing the match is @x@.
-desugarPat :: Id -> Pat GhcTc -> DsM GrdVec
-desugarPat x pat = case pat of
-  WildPat  _ty -> pure []
-  VarPat _ y   -> pure (mkPmLetVar (unLoc y) x)
-  ParPat _ p   -> desugarLPat x p
-  LazyPat _ _  -> pure [] -- like a wildcard
-  BangPat _ p@(L l p') ->
-    -- Add the bang in front of the list, because it will happen before any
-    -- nested stuff.
-    (PmBang x pm_loc :) <$> desugarLPat x p
-      where pm_loc = Just (L l (ppr p'))
-
-  -- (x@pat)   ==>   Desugar pat with x as match var and handle impedance
-  --                 mismatch with incoming match var
-  AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> desugarLPat y p
-
-  SigPat _ p _ty -> desugarLPat x p
-
-  -- See Note [Desugar CoPats]
-  -- Generally the translation is
-  -- pat |> co   ===>   let y = x |> co, pat <- y  where y is a match var of pat
-  XPat (CoPat wrapper p _ty)
-    | isIdHsWrapper wrapper                   -> desugarPat x p
-    | WpCast co <-  wrapper, isReflexiveCo co -> desugarPat x p
-    | otherwise -> do
-        (y, grds) <- desugarPatV p
-        wrap_rhs_y <- dsHsWrapper wrapper
-        pure (PmLet y (wrap_rhs_y (Var x)) : grds)
-
-  -- (n + k)  ===>   let b = x >= k, True <- b, let n = x-k
-  NPlusKPat _pat_ty (L _ n) k1 k2 ge minus -> do
-    b <- mkPmId boolTy
-    let grd_b = vanillaConGrd b trueDataCon []
-    [ke1, ke2] <- traverse dsOverLit [unLoc k1, k2]
-    rhs_b <- dsSyntaxExpr ge    [Var x, ke1]
-    rhs_n <- dsSyntaxExpr minus [Var x, ke2]
-    pure [PmLet b rhs_b, grd_b, PmLet n rhs_n]
-
-  -- (fun -> pat)   ===>   let y = fun x, pat <- y where y is a match var of pat
-  ViewPat _arg_ty lexpr pat -> do
-    (y, grds) <- desugarLPatV pat
-    fun <- dsLExpr lexpr
-    pure $ PmLet y (App fun (Var x)) : grds
-
-  -- list
-  ListPat (ListPatTc _elem_ty Nothing) ps ->
-    desugarListPat x ps
-
-  -- overloaded list
-  ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do
-    dflags <- getDynFlags
-    case splitListTyConApp_maybe pat_ty of
-      Just _e_ty
-        | not (xopt LangExt.RebindableSyntax dflags)
-        -- Just desugar it as a regular ListPat
-        -> desugarListPat x pats
-      _ -> do
-        y <- mkPmId (mkListTy elem_ty)
-        grds <- desugarListPat y pats
-        rhs_y <- dsSyntaxExpr to_list [Var x]
-        pure $ PmLet y rhs_y : grds
-
-    -- (a) In the presence of RebindableSyntax, we don't know anything about
-    --     `toList`, we should treat `ListPat` as any other view pattern.
-    --
-    -- (b) In the absence of RebindableSyntax,
-    --     - If the pat_ty is `[a]`, then we treat the overloaded list pattern
-    --       as ordinary list pattern. Although we can give an instance
-    --       `IsList [Int]` (more specific than the default `IsList [a]`), in
-    --       practice, we almost never do that. We assume the `to_list` is
-    --       the `toList` from `instance IsList [a]`.
-    --
-    --     - Otherwise, we treat the `ListPat` as ordinary view pattern.
-    --
-    -- See #14547, especially comment#9 and comment#10.
-
-  ConPat { pat_con     = L _ con
-         , pat_args    = ps
-         , pat_con_ext = ConPatTc
-           { cpt_arg_tys = arg_tys
-           , cpt_tvs     = ex_tvs
-           , cpt_dicts   = dicts
-           }
-         } -> do
-    desugarConPatOut x con arg_tys ex_tvs dicts ps
-
-  NPat ty (L _ olit) mb_neg _ -> do
-    -- See Note [Literal short cut] in "GHC.HsToCore.Match.Literal"
-    -- We inline the Literal short cut for @ty@ here, because @ty@ is more
-    -- precise than the field of OverLitTc, which is all that dsOverLit (which
-    -- normally does the literal short cut) can look at. Also @ty@ matches the
-    -- type of the scrutinee, so info on both pattern and scrutinee (for which
-    -- short cutting in dsOverLit works properly) is overloaded iff either is.
-    dflags <- getDynFlags
-    let platform = targetPlatform dflags
-    core_expr <- case olit of
-      OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ }
-        | not rebindable
-        , Just expr <- shortCutLit platform val ty
-        -> dsExpr expr
-      _ -> dsOverLit olit
-    let lit  = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr)
-    let lit' = case mb_neg of
-          Just _  -> expectJust "failed to negate lit" (negatePmLit lit)
-          Nothing -> lit
-    mkPmLitGrds x lit'
-
-  LitPat _ lit -> do
-    core_expr <- dsLit (convertLit lit)
-    let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr)
-    mkPmLitGrds x lit
-
-  TuplePat _tys pats boxity -> do
-    (vars, grdss) <- mapAndUnzipM desugarLPatV pats
-    let tuple_con = tupleDataCon boxity (length vars)
-    pure $ vanillaConGrd x tuple_con vars : concat grdss
-
-  SumPat _ty p alt arity -> do
-    (y, grds) <- desugarLPatV p
-    let sum_con = sumDataCon alt arity
-    -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
-    pure $ vanillaConGrd x sum_con [y] : grds
-
-  SplicePat {} -> panic "Check.desugarPat: SplicePat"
-
--- | 'desugarPat', but also select and return a new match var.
-desugarPatV :: Pat GhcTc -> DsM (Id, GrdVec)
-desugarPatV pat = do
-  x <- selectMatchVar Many pat
-  grds <- desugarPat x pat
-  pure (x, grds)
-
-desugarLPat :: Id -> LPat GhcTc -> DsM GrdVec
-desugarLPat x = desugarPat x . unLoc
-
--- | 'desugarLPat', but also select and return a new match var.
-desugarLPatV :: LPat GhcTc -> DsM (Id, GrdVec)
-desugarLPatV = desugarPatV . unLoc
-
--- | @desugarListPat _ x [p1, ..., pn]@ is basically
---   @desugarConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
--- constructing the 'ConPatOut's.
-desugarListPat :: Id -> [LPat GhcTc] -> DsM GrdVec
-desugarListPat x pats = do
-  vars_and_grdss <- traverse desugarLPatV pats
-  mkListGrds x vars_and_grdss
-
--- | Desugar a constructor pattern
-desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
-                 -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec
-desugarConPatOut x con univ_tys ex_tvs dicts = \case
-    PrefixCon ps                 -> go_field_pats (zip [0..] ps)
-    InfixCon  p1 p2              -> go_field_pats (zip [0..] [p1,p2])
-    RecCon    (HsRecFields fs _) -> go_field_pats (rec_field_ps fs)
-  where
-    -- The actual argument types (instantiated)
-    arg_tys     = map scaledThing $ conLikeInstOrigArgTys con (univ_tys ++ mkTyVarTys ex_tvs)
-
-    -- Extract record field patterns tagged by field index from a list of
-    -- LHsRecField
-    rec_field_ps fs = map (tagged_pat . unLoc) fs
-      where
-        tagged_pat f = (lbl_to_index (getName (hsRecFieldId f)), hsRecFieldArg f)
-        -- Unfortunately the label info is empty when the DataCon wasn't defined
-        -- with record field labels, hence we desugar to field index.
-        orig_lbls        = map flSelector $ conLikeFieldLabels con
-        lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls
-
-    go_field_pats tagged_pats = do
-      -- The fields that appear might not be in the correct order. So
-      --   1. Do the PmCon match
-      --   2. Then pattern match on the fields in the order given by the first
-      --      field of @tagged_pats@.
-      -- See Note [Field match order for RecCon]
-
-      -- Desugar the mentioned field patterns. We're doing this first to get
-      -- the Ids for pm_con_args and bring them in order afterwards.
-      let trans_pat (n, pat) = do
-            (var, pvec) <- desugarLPatV pat
-            pure ((n, var), pvec)
-      (tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats
-
-      let get_pat_id n ty = case lookup n tagged_vars of
-            Just var -> pure var
-            Nothing  -> mkPmId ty
-
-      -- 1. the constructor pattern match itself
-      arg_ids <- zipWithM get_pat_id [0..] arg_tys
-      let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
-
-      -- 2. guards from field selector patterns
-      let arg_grds = concat arg_grdss
-
-      -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
-      pure (con_grd : arg_grds)
-
-desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre)
--- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
-desugarPatBind loc var pat =
-  PmPatBind . flip PmGRHS (L loc (ppr pat)) <$> desugarPat var pat
-
-desugarEmptyCase :: Id -> DsM PmEmptyCase
-desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
-
--- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
-desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
-               -> DsM (PmMatchGroup Pre)
-desugarMatches vars matches =
-  PmMatchGroup <$> traverse (desugarMatch vars) matches
-
--- Desugar a single match
-desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PmMatch Pre)
-desugarMatch vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
-  pats'  <- concat <$> zipWithM desugarLPat vars pats
-  grhss' <- desugarGRHSs match_loc (sep (map ppr pats)) grhss
-  -- tracePm "desugarMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
-  return PmMatch { pm_pats = pats', pm_grhss = grhss' }
-
-desugarGRHSs :: SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty (PmGRHS Pre))
-desugarGRHSs match_loc pp_pats grhss
-  = traverse (desugarLGRHS match_loc pp_pats)
-  . expectJust "desugarGRHSs"
-  . NE.nonEmpty
-  $ grhssGRHSs grhss
-
--- | Desugar a guarded right-hand side to a single 'GrdTree'
-desugarLGRHS :: SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM (PmGRHS Pre)
-desugarLGRHS match_loc pp_pats (L _loc (GRHS _ gs _)) = do
-  -- _loc points to the match separator (ie =, ->) that comes after the guards.
-  -- Hence we have to pass in the match_loc, which we use in case that the RHS
-  -- is unguarded.
-  -- 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@.
-  let rhs_info = case gs of
-        []              -> L match_loc pp_pats
-        (L grd_loc _):_ -> L grd_loc   (pp_pats <+> vbar <+> interpp'SP gs)
-  grds <- concatMapM (desugarGuard . unLoc) gs
-  pure PmGRHS { pg_grds = grds, pg_rhs = rhs_info }
-
--- | Desugar a guard statement to a 'GrdVec'
-desugarGuard :: GuardStmt GhcTc -> DsM GrdVec
-desugarGuard guard = case guard of
-  BodyStmt _   e _ _ -> desugarBoolGuard e
-  LetStmt  _   binds -> desugarLet (unLoc binds)
-  BindStmt _ p e     -> desugarBind p e
-  LastStmt        {} -> panic "desugarGuard LastStmt"
-  ParStmt         {} -> panic "desugarGuard ParStmt"
-  TransStmt       {} -> panic "desugarGuard TransStmt"
-  RecStmt         {} -> panic "desugarGuard RecStmt"
-  ApplicativeStmt {} -> panic "desugarGuard ApplicativeLastStmt"
-
--- | Desugar let-bindings
-desugarLet :: HsLocalBinds GhcTc -> DsM GrdVec
-desugarLet _binds = return []
-
--- | Desugar a pattern guard
---   @pat <- e ==>  let x = e;  <guards for pat <- x>@
-desugarBind :: LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
-desugarBind p e = dsLExpr e >>= \case
-  Var y
-    | Nothing <- isDataConId_maybe y
-    -- RHS is a variable, so that will allow us to omit the let
-    -> desugarLPat y p
-  rhs -> do
-    (x, grds) <- desugarLPatV p
-    pure (PmLet x rhs : grds)
-
--- | Desugar a boolean guard
---   @e ==>  let x = e; True <- x@
-desugarBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
-desugarBoolGuard e
-  | isJust (isTrueLHsExpr e) = return []
-    -- The formal thing to do would be to generate (True <- True)
-    -- but it is trivial to solve so instead we give back an empty
-    -- GrdVec for efficiency
-  | otherwise = dsLExpr e >>= \case
-      Var y
-        | Nothing <- isDataConId_maybe y
-        -- Omit the let by matching on y
-        -> pure [vanillaConGrd y trueDataCon []]
-      rhs -> do
-        x <- mkPmId boolTy
-        pure [PmLet x rhs, vanillaConGrd x trueDataCon []]
-
-{- Note [Field match order for RecCon]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The order for RecCon field patterns actually determines evaluation order of
-the pattern match. For example:
-
-  data T = T { a :: Char, b :: Int }
-  f :: T -> ()
-  f T{ b = 42, a = 'a' } = ()
-
-Then @f (T (error "a") (error "b"))@ errors out with "b" because it is mentioned
-first in the pattern match.
-
-This means we can't just desugar the pattern match to
-@[T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the
-right order: @[T a b <- x, 42 <- b, 'a' <- a]@.
-
-Note [Order of guards matters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Similar to Note [Field match order for RecCon], the order in which the guards
-for a pattern match appear matter. Consider a situation similar to T5117:
-
-  f (0:_)  = ()
-  f (0:[]) = ()
-
-The latter clause is clearly redundant. Yet if we desugar the second clause as
-
-  [x:xs' <- xs, [] <- xs', 0 <- x]
-
-We will say that the second clause only has an inaccessible RHS. That's because
-we force the tail of the list before comparing its head! So the correct
-translation would have been
-
-  [x:xs' <- xs, 0 <- x, [] <- xs']
-
-And we have to take in the guards on list cells into @mkListGrds@.
-
-Note [Desugar CoPats]
-~~~~~~~~~~~~~~~~~~~~~~~
-The pattern match checker did not know how to handle coerced patterns
-`CoPat` efficiently, which gave rise to #11276. The original approach
-desugared `CoPat`s:
-
-    pat |> co    ===>    x (pat <- (x |> co))
-
-Why did we do this seemingly unnecessary expansion in the first place?
-The reason is that the type of @pat |> co@ (which is the type of the value
-abstraction we match against) might be different than that of @pat@. Data
-instances such as @Sing (a :: Bool)@ are a good example of this: If we would
-just drop the coercion, we'd get a type error when matching @pat@ against its
-value abstraction, with the result being that pmIsSatisfiable decides that every
-possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
-a lot of false warnings.
-
-But we can check whether the coercion is a hole or if it is just refl, in
-which case we can drop it.
--}
-
---
--- * Coverage checking guard trees into annotated trees
---
-
--- | Pattern-match coverage check result
-data CheckResult a
-  = CheckResult
-  { cr_ret :: !a
-  -- ^ A hole for redundancy info and covered sets.
-  , cr_uncov   :: !Nablas
-  -- ^ The set of uncovered values falling out at the bottom.
-  --   (for -Wincomplete-patterns, but also important state for the algorithm)
-  , cr_approx  :: !Precision
-  -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
-  -- purpose of suggesting to crank it up in the warning message. Writer state.
-  } deriving Functor
-
-instance Outputable a => Outputable (CheckResult a) where
-  ppr (CheckResult c unc pc)
-    = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
-        [ field "ret" c <> comma
-        , field "uncov" unc])
-    where
-      ppr_precision Precise     = empty
-      ppr_precision Approximate = text "(Approximate)"
-      field name value = text name <+> equals <+> ppr value
-
--- | Lift 'addPmCts' over 'Nablas'.
-addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
-addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
-
--- | 'addPmCtsNablas' for a single 'PmCt'.
-addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
-addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
-
--- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
--- we preserve the invariant that there are no uninhabited 'Nabla's. But that
--- could change in the future, for example by implementing this function in
--- terms of @notNull <$> generateInhabitingPatterns 1 ds@.
-isInhabited :: Nablas -> DsM Bool
-isInhabited (MkNablas ds) = pure (not (null ds))
-
--- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
-newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) }
-  deriving Functor
-
--- | Composes 'CheckAction's top-to-bottom:
--- If a value falls through the resulting action, then it must fall through the
--- first action and then through the second action.
--- If a value matches the resulting action, then it either matches the
--- first action or matches the second action.
--- Basically the semantics of the LYG branching construct.
-topToBottom :: (top -> bot -> ret)
-            -> CheckAction top
-            -> CheckAction bot
-            -> CheckAction ret
-topToBottom f (CA top) (CA bot) = CA $ \inc -> do
-  t <- top inc
-  b <- bot (cr_uncov t)
-  pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
-                   , cr_uncov = cr_uncov b
-                   , cr_approx = cr_approx t Semi.<> cr_approx b }
-
-
--- | Composes 'CheckAction's left-to-right:
--- If a value falls through the resulting action, then it either falls through the
--- first action or through the second action.
--- If a value matches the resulting action, then it must match the first action
--- and then match the second action.
--- Basically the semantics of the LYG guard construct.
-leftToRight :: (RedSets -> right -> ret)
-            -> CheckAction RedSets
-            -> CheckAction right
-            -> CheckAction ret
-leftToRight f (CA left) (CA right) = CA $ \inc -> do
-  l <- left inc
-  r <- right (rs_cov (cr_ret l))
-  limit <- maxPmCheckModels <$> getDynFlags
-  let uncov = cr_uncov l Semi.<> cr_uncov r
-  -- See Note [Countering exponential blowup]
-  let (prec', uncov') = throttle limit inc uncov
-  pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
-                   , cr_uncov = uncov'
-                   , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }
-
--- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@
--- is exceeding the given @limit@ and the @old@ number of 'Nabla's.
--- See Note [Countering exponential blowup].
-throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
-throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
-  --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
-  | length new_ds > max limit (length old_ds) = (Approximate, old)
-  | otherwise                                 = (Precise,     new)
-
-checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
--- The implementation is pretty similar to
--- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
-checkSequence act (t :| [])       = (:| []) <$> act t
-checkSequence act (t1 :| (t2:ts)) =
-  topToBottom (NE.<|) (act t1) (checkSequence act (t2:|ts))
-
-checkGrd :: PmGrd -> CheckAction RedSets
-checkGrd grd = CA $ \inc -> case grd of
-  -- let x = e: Refine with x ~ e
-  PmLet x e -> do
-    matched <- addPhiCtNablas inc (PhiCoreCt x e)
-    tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
-    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
-                     , cr_uncov = mempty
-                     , cr_approx = Precise }
-  -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
-  PmBang x mb_info -> do
-    div <- addPhiCtNablas inc (PhiBotCt x)
-    matched <- addPhiCtNablas inc (PhiNotBotCt x)
-    -- See Note [Dead bang patterns]
-    -- mb_info = Just info <==> PmBang originates from bang pattern in source
-    let bangs | Just info <- mb_info = unitOL (div, info)
-              | otherwise            = NilOL
-    tracePm "check:Bang" (ppr x <+> ppr div)
-    pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
-                     , cr_uncov = mempty
-                     , cr_approx = Precise }
-  -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
-  PmCon x con tvs dicts args -> do
-    !div <- if isPmAltConMatchStrict con
-      then addPhiCtNablas inc (PhiBotCt x)
-      else pure mempty
-    !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
-    !uncov   <- addPhiCtNablas inc (PhiNotConCt x con)
-    tracePm "check:Con" $ vcat
-      [ ppr grd
-      , ppr inc
-      , hang (text "div") 2 (ppr div)
-      , hang (text "matched") 2 (ppr matched)
-      , hang (text "uncov") 2 (ppr uncov)
-      ]
-    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
-                     , cr_uncov = uncov
-                     , cr_approx = Precise }
-
-checkGrds :: [PmGrd] -> CheckAction RedSets
-checkGrds [] = CA $ \inc ->
-  pure CheckResult { cr_ret = emptyRedSets { rs_cov = inc }
-                   , cr_uncov = mempty
-                   , cr_approx = Precise }
-checkGrds (g:grds) = leftToRight merge (checkGrd g) (checkGrds grds)
-  where
-    merge ri_g ri_grds = -- This operation would /not/ form a Semigroup!
-      RedSets { rs_cov   = rs_cov ri_grds
-              , rs_div   = rs_div ri_g   Semi.<> rs_div ri_grds
-              , rs_bangs = rs_bangs ri_g Semi.<> rs_bangs ri_grds }
-
-checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
-checkMatchGroup (PmMatchGroup matches) =
-  PmMatchGroup <$> checkSequence checkMatch matches
-
-checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
-checkMatch (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
-  leftToRight PmMatch (checkGrds grds) (checkGRHSs grhss)
-
-checkGRHSs :: NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
-checkGRHSs = checkSequence checkGRHS
-
-checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
-checkGRHS (PmGRHS { pg_grds = grds, pg_rhs = rhs_info }) =
-  flip PmGRHS rhs_info <$> checkGrds grds
-
-checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
-checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
-  unc <- addPhiCtNablas inc (PhiNotBotCt var)
-  pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
-
-checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
-checkPatBind = coerce checkGRHS
-
-{- Note [Countering exponential blowup]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Precise pattern match exhaustiveness checking is necessarily exponential in
-the size of some input programs. We implement a counter-measure in the form of
-the -fmax-pmcheck-models flag, limiting the number of Nablas we check against
-each pattern by a constant.
-
-How do we do that? Consider
-
-  f True True = ()
-  f True True = ()
-
-And imagine we set our limit to 1 for the sake of the example. The first clause
-will be checked against the initial Nabla, {}. Doing so will produce an
-Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
-Also we find the first clause to cover the model {x~True,y~True}.
-
-But the Uncovered set we get out of the match is too huge! We somehow have to
-ensure not to make things worse as they are already, so we continue checking
-with a singleton Uncovered set of the initial Nabla {}. Why is this
-sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
-to forgetting that we matched against the first clause. The values represented
-by {} are a superset of those represented by its two refinements {x≁True} and
-{x~True,y≁True}.
-
-This forgetfulness becomes very apparent in the example above: By continuing
-with {} we don't detect the second clause as redundant, as it again covers the
-same non-empty subset of {}. So we don't flag everything as redundant anymore,
-but still will never flag something as redundant that isn't.
-
-For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
-and report @f _ _@ as missing, which is a superset of the actual missing
-matches. But soundness means we will never fail to report a missing match.
-
-This mechanism is implemented in 'throttle'.
-
-Guards are an extreme example in this regard, with #11195 being a particularly
-dreadful example: Since their RHS are often pretty much unique, we split on a
-variable (the one representing the RHS) that doesn't occur anywhere else in the
-program, so we don't actually get useful information out of that split!
--}
-
---
--- * Collecting long-distance information
---
-
-ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
-ldiMatchGroup (PmMatchGroup matches) = ldiMatch <$> matches
-
-ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas)
-ldiMatch (PmMatch { pm_pats = red, pm_grhss = grhss }) =
-  (rs_cov red, ldiGRHS <$> grhss)
-
-ldiGRHS :: PmGRHS Post -> Nablas
-ldiGRHS (PmGRHS { pg_grds = red }) = rs_cov red
-
---
--- * Collecting redundancy information
---
-
--- | The result of redundancy checking:
---    * RHSs classified as /C/overed, /I/naccessible and /R/edundant
---    * And redundant /B/ang patterns. See Note [Dead bang patterns].
-data CIRB
-  = CIRB
-  { cirb_cov   :: !(OrdList SrcInfo) -- ^ Covered clauses
-  , cirb_inacc :: !(OrdList SrcInfo) -- ^ Inaccessible clauses
-  , cirb_red   :: !(OrdList SrcInfo) -- ^ Redundant clauses
-  , cirb_bangs :: !(OrdList SrcInfo) -- ^ Redundant bang patterns
-  }
-
-instance Semigroup CIRB where
-  CIRB a b c d <> CIRB e f g h = CIRB (a <> e) (b <> f) (c <> g) (d <> h)
-    where (<>) = (Semi.<>)
-
-instance Monoid CIRB where
-  mempty = CIRB mempty mempty mempty mempty
-
-markAllRedundant :: CIRB -> CIRB
-markAllRedundant CIRB { cirb_cov = cov, cirb_inacc = inacc, cirb_red = red } =
-  mempty { cirb_red = cov Semi.<> inacc Semi.<> red }
-
--- See Note [Determining inaccessible clauses]
-ensureOneNotRedundant :: CIRB -> CIRB
-ensureOneNotRedundant ci = case ci of
-  CIRB { cirb_cov = NilOL, cirb_inacc = NilOL, cirb_red = ConsOL r rs }
-    -> ci { cirb_inacc = unitOL r, cirb_red = rs }
-  _ -> ci
-
--- | Only adds the redundant bangs to the @CIRB@ if there is at least one
--- non-redundant 'SrcInfo'. There is no point in remembering a redundant bang
--- if the whole match is redundant!
-addRedundantBangs :: OrdList SrcInfo -> CIRB -> CIRB
-addRedundantBangs _red_bangs cirb@CIRB { cirb_cov = NilOL, cirb_inacc = NilOL } =
-  cirb
-addRedundantBangs red_bangs  cirb =
-  cirb { cirb_bangs = cirb_bangs cirb Semi.<> red_bangs }
-
--- | Checks the 'Nablas' in a 'RedSets' for inhabitants and returns
---    1. Whether the Covered set was inhabited
---    2. Whether the Diverging set was inhabited
---    3. All source bangs whose 'Nablas' were empty, which means they are
---       redundant.
-testRedSets :: RedSets -> DsM (Bool, Bool, OrdList SrcInfo)
-testRedSets RedSets { rs_cov = cov, rs_div = div, rs_bangs = bangs } = do
-  is_covered  <- isInhabited cov
-  may_diverge <- isInhabited div
-  red_bangs   <- flip mapMaybeM (fromOL bangs) $ \(nablas, bang) -> do
-    isInhabited nablas >>= \case
-      True  -> pure Nothing
-      False -> pure (Just bang)
-  pure (is_covered, may_diverge, toOL red_bangs)
-
-cirbsMatchGroup :: PmMatchGroup Post -> DsM CIRB
-cirbsMatchGroup (PmMatchGroup matches) =
-  Semi.sconcat <$> traverse cirbsMatch matches
-
-cirbsMatch :: PmMatch Post -> DsM CIRB
-cirbsMatch PmMatch { pm_pats = red, pm_grhss = grhss } = do
-  (is_covered, may_diverge, red_bangs) <- testRedSets red
-  cirb <- cirbsGRHSs grhss
-  pure $ addRedundantBangs red_bangs
-       -- See Note [Determining inaccessible clauses]
-       $ applyWhen may_diverge ensureOneNotRedundant
-       $ applyWhen (not is_covered) markAllRedundant
-       $ cirb
-
-cirbsGRHSs :: NonEmpty (PmGRHS Post) -> DsM CIRB
-cirbsGRHSs grhss = Semi.sconcat <$> traverse cirbsGRHS grhss
-
-cirbsGRHS :: PmGRHS Post -> DsM CIRB
-cirbsGRHS PmGRHS { pg_grds = red, pg_rhs = info } = do
-  (is_covered, may_diverge, red_bangs) <- testRedSets red
-  let cirb | is_covered  = mempty { cirb_cov   = unitOL info }
-           | may_diverge = mempty { cirb_inacc = unitOL info }
-           | otherwise   = mempty { cirb_red   = unitOL info }
-  pure (addRedundantBangs red_bangs cirb)
-
-cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
-cirbsEmptyCase _ = pure mempty
-
-cirbsPatBind :: PmPatBind Post -> DsM CIRB
-cirbsPatBind = coerce cirbsGRHS
-
-{- Note [Determining inaccessible clauses]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-  f _  True = ()
-  f () True = ()
-  f _  _    = ()
-Is f's second clause redundant? The perhaps surprising answer is, no, it isn't!
-@f (error "boom") False@ will force the error with clause 2, but will return
-() if it was deleted, so clearly not redundant. Yet for now combination of
-arguments we can ever reach clause 2's RHS, so we say it has inaccessible RHS
-(as opposed to being completely redundant).
-
-We detect an inaccessible RHS simply by pretending it's redundant, until we see
--}
-
---
--- * Formatting and reporting warnings
---
-
--- | Given a function that collects 'CIRB's, this function will emit warnings
--- for a 'CheckResult'.
-formatReportWarnings :: (ann -> DsM CIRB) -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
-formatReportWarnings collect ctx vars cr@CheckResult { cr_ret = ann } = do
-  cov_info <- collect ann
-  dflags <- getDynFlags
-  reportWarnings dflags ctx vars cr{cr_ret=cov_info}
-
--- | Issue all the warnings
--- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
-reportWarnings :: DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
-reportWarnings dflags ctx@(DsMatchContext kind loc) vars
-  CheckResult { cr_ret    = CIRB { cirb_inacc = inaccessible_rhss
-                                 , cirb_red   = redundant_rhss
-                                 , cirb_bangs = redundant_bangs }
-              , cr_uncov  = uncovered
-              , cr_approx = precision }
-  = when (flag_i || flag_u || flag_b) $ do
-      unc_examples <- getNFirstUncovered vars (maxPatterns + 1) uncovered
-      let exists_r = flag_i && notNull redundant_rhss
-          exists_i = flag_i && notNull inaccessible_rhss
-          exists_u = flag_u && notNull unc_examples
-          exists_b = flag_b && notNull redundant_bangs
-          approx   = precision == Approximate
-
-      when (approx && (exists_u || exists_i)) $
-        putSrcSpanDs loc (warnDs NoReason approx_msg)
-
-      when exists_b $ forM_ redundant_bangs $ \(L l q) -> do
-        putSrcSpanDs l (warnDs (Reason Opt_WarnRedundantBangPatterns)
-                               (pprEqn q "has redundant bang"))
-
-      when exists_r $ forM_ redundant_rhss $ \(L l q) -> do
-        putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
-                               (pprEqn q "is redundant"))
-      when exists_i $ forM_ inaccessible_rhss $ \(L l q) -> do
-        putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
-                               (pprEqn q "has inaccessible right hand side"))
-
-      when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
-        pprEqns vars unc_examples
-  where
-    flag_i = overlapping dflags kind
-    flag_u = exhaustive dflags kind
-    flag_b = redundant_bang dflags
-    flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
-
-    maxPatterns = maxUncoveredPatterns dflags
-
-    -- Print a single clause (for redundant/with-inaccessible-rhs)
-    pprEqn q txt = pprContext True ctx (text txt) $ \f ->
-      f (q <+> matchSeparator kind <+> text "...")
-
-    -- Print several clauses (for uncovered clauses)
-    pprEqns vars nablas = pprContext False ctx (text "are non-exhaustive") $ \_ ->
-      case vars of -- See #11245
-           [] -> text "Guards do not cover entire pattern space"
-           _  -> let us = map (\nabla -> pprUncovered nabla vars) nablas
-                 in  hang (text "Patterns not matched:") 4
-                       (vcat (take maxPatterns us) $$ dots maxPatterns us)
-
-    approx_msg = vcat
-      [ hang
-          (text "Pattern match checker ran into -fmax-pmcheck-models="
-            <> int (maxPmCheckModels dflags)
-            <> text " limit, so")
-          2
-          (  bullet <+> text "Redundant clauses might not be reported at all"
-          $$ bullet <+> text "Redundant clauses might be reported as inaccessible"
-          $$ bullet <+> text "Patterns reported as unmatched might actually be matched")
-      , text "Increase the limit or resolve the warnings to suppress this message." ]
-
-getNFirstUncovered :: [Id] -> Int -> Nablas -> DsM [Nabla]
-getNFirstUncovered vars n (MkNablas nablas) = go n (bagToList nablas)
-  where
-    go 0 _              = pure []
-    go _ []             = pure []
-    go n (nabla:nablas) = do
-      front <- generateInhabitingPatterns vars n nabla
-      back <- go (n - length front) nablas
-      pure (front ++ back)
-
-dots :: Int -> [a] -> SDoc
-dots maxPatterns qs
-    | qs `lengthExceeds` maxPatterns = text "..."
-    | otherwise                      = empty
-
-pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
-pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
-  = vcat [text txt <+> msg,
-          sep [ text "In" <+> ppr_match <> char ':'
-              , nest 4 (rest_of_msg_fun pref)]]
-  where
-    txt | singular  = "Pattern match"
-        | otherwise = "Pattern match(es)"
-
-    (ppr_match, pref)
-        = case kind of
-             FunRhs { mc_fun = L _ fun }
-                  -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
-             _    -> (pprMatchContext kind, \ pp -> pp)
-
---
--- * Utilities
---
-
--- | All warning flags that need to run the pattern match checker.
-allPmCheckWarnings :: [WarningFlag]
-allPmCheckWarnings =
-  [ Opt_WarnIncompletePatterns
-  , Opt_WarnIncompleteUniPatterns
-  , Opt_WarnIncompletePatternsRecUpd
-  , Opt_WarnOverlappingPatterns
-  ]
-
--- | Check whether the redundancy checker should run (redundancy only)
-overlapping :: DynFlags -> HsMatchContext id -> Bool
--- See Note [Inaccessible warnings for record updates]
-overlapping _      RecUpd = False
-overlapping dflags _      = wopt Opt_WarnOverlappingPatterns dflags
-
--- | Check whether the exhaustiveness checker should run (exhaustiveness only)
-exhaustive :: DynFlags -> HsMatchContext id -> Bool
-exhaustive  dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
-
--- | Check whether unnecessary bangs should be warned about
-redundant_bang :: DynFlags -> Bool
-redundant_bang dflags = wopt Opt_WarnRedundantBangPatterns dflags
-
--- | Denotes whether an exhaustiveness check is supported, and if so,
--- via which 'WarningFlag' it's controlled.
--- Returns 'Nothing' if check is not supported.
-exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
-exhaustiveWarningFlag (FunRhs {})   = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag CaseAlt       = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag IfAlt         = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag LambdaExpr    = Just Opt_WarnIncompleteUniPatterns
-exhaustiveWarningFlag PatBindRhs    = Just Opt_WarnIncompleteUniPatterns
-exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
-exhaustiveWarningFlag ProcExpr      = Just Opt_WarnIncompleteUniPatterns
-exhaustiveWarningFlag RecUpd        = Just Opt_WarnIncompletePatternsRecUpd
-exhaustiveWarningFlag ThPatSplice   = Nothing
-exhaustiveWarningFlag PatSyn        = Nothing
-exhaustiveWarningFlag ThPatQuote    = Nothing
--- Don't warn about incomplete patterns in list comprehensions, pattern guards
--- etc. They are often *supposed* to be incomplete
-exhaustiveWarningFlag (StmtCtxt {}) = Nothing
-
--- | Check whether any part of pattern match checking is enabled for this
--- 'HsMatchContext' (does not matter whether it is the redundancy check or the
--- exhaustiveness check).
-isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
-isMatchContextPmChecked dflags origin kind
-  | isGenerated origin
-  = False
-  | otherwise
-  = overlapping dflags kind || exhaustive dflags kind
-
--- | Return True when any of the pattern match warnings ('allPmCheckWarnings')
--- are enabled, in which case we need to run the pattern match checker.
-needToRunPmCheck :: DynFlags -> Origin -> Bool
-needToRunPmCheck dflags origin
-  | isGenerated origin
-  = False
-  | otherwise
-  = notNull (filter (`wopt` dflags) allPmCheckWarnings)
-
-{- Note [Inaccessible warnings for record updates]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#12957)
-  data T a where
-    T1 :: { x :: Int } -> T Bool
-    T2 :: { x :: Int } -> T a
-    T3 :: T a
-
-  f :: T Char -> T a
-  f r = r { x = 3 }
-
-The desugarer will conservatively generate a case for T1 even though
-it's impossible:
-  f r = case r of
-          T1 x -> T1 3   -- Inaccessible branch
-          T2 x -> T2 3
-          _    -> error "Missing"
-
-We don't want to warn about the inaccessible branch because the programmer
-didn't put it there!  So we filter out the warning here.
-
-The same can happen for long distance term constraints instead of type
-constraints (#17783):
-
-  data T = A { x :: Int } | B { x :: Int }
-  f r@A{} = r { x = 3 }
-  f _     = B 0
-
-Here, the long distance info from the FunRhs match (@r ~ A x@) will make the
-clause matching on @B@ of the desugaring to @case@ redundant. It's generated
-code that we don't want to warn about.
--}
-
---
--- * Long-distance information
---
-
--- | Locally update 'dsl_nablas' with the given action, but defer evaluation
--- with 'unsafeInterleaveM' in order not to do unnecessary work.
-locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a
-locallyExtendPmNablas ext k = do
-  nablas <- getLdiNablas
-  nablas' <- unsafeInterleaveM $ ext nablas
-  updPmNablas nablas' k
-
--- | Add in-scope type constraints if the coverage checker might run and then
--- run the given action.
-addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
-addTyCs origin ev_vars m = do
-  dflags <- getDynFlags
-  applyWhen (needToRunPmCheck dflags origin)
-            (locallyExtendPmNablas $ \nablas ->
-              addPhiCtsNablas nablas (PhiTyCt . evVarPred <$> ev_vars))
-            m
-
--- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment
--- when checking a case expression:
---     case e of x { matches }
--- When checking matches we record that (x ~ e) where x is the initial
--- uncovered. All matches will have to satisfy this equality.
-addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
-addCoreScrutTmCs Nothing    _   k = k
-addCoreScrutTmCs (Just scr) [x] k =
-  flip locallyExtendPmNablas k $ \nablas ->
-    addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
-addCoreScrutTmCs _   _   _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id"
-
--- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first.
-addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
-addHsScrutTmCs Nothing    _    k = k
-addHsScrutTmCs (Just scr) vars k = do
-  scr_e <- dsLExpr scr
-  addCoreScrutTmCs (Just scr_e) vars k
-
-{- Note [Long-distance information]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  data Color = R | G | B
-  f :: Color -> Int
-  f R = …
-  f c = … (case c of
-          G -> True
-          B -> False) …
-
-Humans can make the "long-distance connection" between the outer pattern match
-and the nested case pattern match to see that the inner pattern match is
-exhaustive: @c@ can't be @R@ anymore because it was matched in the first clause
-of @f@.
-
-To achieve similar reasoning in the coverage checker, we keep track of the set
-of values that can reach a particular program point (often loosely referred to
-as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas'.
-We fill that set with Covered Nablas returned by the exported checking
-functions, which the call sites put into place with
-'GHC.HsToCore.Monad.updPmNablas'.
-Call sites also extend this set with facts from type-constraint dictionaries,
-case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
-and 'addHsScrutTmCs'.
-
-Note [Recovering from unsatisfiable pattern-matching constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following code (see #12957 and #15450):
-
-  f :: Int ~ Bool => ()
-  f = case True of { False -> () }
-
-We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
-used not to do this; in fact, it would warn that the match was /redundant/!
-This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
-coverage checker deems any matches with unsatisfiable constraint sets to be
-unreachable.
-
-We make sure to always start from an inhabited 'Nablas' by calling
-'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the
-long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty.
--}
diff --git a/compiler/GHC/HsToCore/Pmc.hs b/compiler/GHC/HsToCore/Pmc.hs
new file mode 100644
index 0000000000..d621e65c4b
--- /dev/null
+++ b/compiler/GHC/HsToCore/Pmc.hs
@@ -0,0 +1,501 @@
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE MultiWayIf                 #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE NamedFieldPuns             #-}
+{-# LANGUAGE FlexibleInstances          #-}
+
+-- | This module coverage checks pattern matches. It finds
+--
+--     * Uncovered patterns, certifying non-exhaustivity
+--     * Redundant equations
+--     * Equations with an inaccessible right-hand-side
+--
+-- The algorithm is based on the paper
+-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989)
+--
+-- There is an overview Figure 2 in there that's probably helpful.
+-- Here is an overview of how it's implemented, which follows the structure of
+-- the entry points such as 'pmcMatches':
+--
+--  1. Desugar source syntax (like 'LMatch') to guard tree variants (like
+--     'GrdMatch'), with one of the desugaring functions (like 'desugarMatch').
+--     See "GHC.HsToCore.Pmc.Desugar".
+--     Follows Section 3.1 in the paper.
+--  2. Coverage check guard trees (with a function like 'checkMatch') to get a
+--     'CheckResult'. See "GHC.HsToCore.Pmc.Check".
+--     The normalised refinement types 'Nabla' are tested for inhabitants by
+--     "GHC.HsToCore.Pmc.Solver".
+--  3. Collect redundancy information into a 'CIRB' with a function such
+--     as 'cirbsMatch'. Follows the R function from Figure 6 of the paper.
+--  4. Format and report uncovered patterns and redundant equations ('CIRB')
+--     with 'formatReportWarnings'. Basically job of the G function, plus proper
+--     pretty printing of the warnings (Section 5.4 of the paper).
+--  5. Return 'Nablas' reaching syntactic sub-components for
+--     Note [Long-distance information]. Collected by functions such as
+--     'ldiMatch'. See Section 4.1 of the paper.
+module GHC.HsToCore.Pmc (
+        -- Checking and printing
+        pmcPatBind, pmcMatches, pmcGRHSs,
+        isMatchContextPmChecked,
+
+        -- See Note [Long-distance information]
+        addTyCs, addCoreScrutTmCs, addHsScrutTmCs
+    ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils
+import GHC.HsToCore.Pmc.Desugar
+import GHC.HsToCore.Pmc.Check
+import GHC.HsToCore.Pmc.Solver
+import GHC.HsToCore.Pmc.Ppr
+import GHC.Types.Basic (Origin(..))
+import GHC.Core (CoreExpr)
+import GHC.Driver.Session
+import GHC.Hs
+import GHC.Types.Id
+import GHC.Types.SrcLoc
+import GHC.Utils.Misc
+import GHC.Utils.Outputable
+import GHC.Utils.Panic
+import GHC.Types.Var (EvVar)
+import GHC.Tc.Utils.TcType (evVarPred)
+import {-# SOURCE #-} GHC.HsToCore.Expr (dsLExpr)
+import GHC.HsToCore.Monad
+import GHC.Data.Bag
+import GHC.Data.IOEnv (unsafeInterleaveM)
+import GHC.Data.OrdList
+import GHC.Utils.Monad (mapMaybeM)
+
+import Control.Monad (when, forM_)
+import qualified Data.Semigroup as Semi
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+import Data.Coerce
+
+--
+-- * Exported entry points to the checker
+--
+
+-- | A non-empty delta that is initialised from the ambient refinement type
+-- capturing long-distance information, or the trivially habitable 'Nablas' if
+-- the former is uninhabited.
+-- See Note [Recovering from unsatisfiable pattern-matching constraints].
+getLdiNablas :: DsM Nablas
+getLdiNablas = do
+  nablas <- getPmNablas
+  isInhabited nablas >>= \case
+    True  -> pure nablas
+    False -> pure initNablas
+
+-- | Check a pattern binding (let, where) for exhaustiveness.
+pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
+-- See Note [pmcPatBind only checks PatBindRhs]
+pmcPatBind ctxt@(DsMatchContext PatBindRhs loc) var p = do
+  missing   <- getLdiNablas
+  pat_bind <- desugarPatBind loc var p
+  tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
+  result <- unCA (checkPatBind pat_bind) missing
+  tracePm "}: " (ppr (cr_uncov result))
+  formatReportWarnings cirbsPatBind ctxt [var] result
+pmcPatBind _ _ _ = pure ()
+
+-- | Exhaustive for guard matches, is used for guards in pattern bindings and
+-- in @MultiIf@ expressions. Returns the 'Nablas' covered by the RHSs.
+pmcGRHSs
+  :: HsMatchContext GhcRn         -- ^ Match context, for warning messages
+  -> GRHSs GhcTc (LHsExpr GhcTc)  -- ^ The GRHSs to check
+  -> DsM (NonEmpty Nablas)        -- ^ Covered 'Nablas' for each RHS, for long
+                                  --   distance info
+pmcGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
+  let combined_loc = foldl1 combineSrcSpans (map getLoc grhss)
+      ctxt = DsMatchContext hs_ctxt combined_loc
+  matches <- desugarGRHSs combined_loc empty guards
+  missing   <- getLdiNablas
+  tracePm "pmcGRHSs" (hang (vcat [ppr ctxt
+                                , text "Guards:"])
+                                2
+                                (pprGRHSs hs_ctxt guards $$ ppr missing))
+  result <- unCA (checkGRHSs matches) missing
+  tracePm "}: " (ppr (cr_uncov result))
+  formatReportWarnings cirbsGRHSs ctxt [] result
+  return (ldiGRHS <$> cr_ret result)
+
+-- | Check a list of syntactic 'Match'es (part of case, functions, etc.), each
+-- with a 'Pat' and one or more 'GRHSs':
+--
+-- @
+--   f x y | x == y    = 1   -- match on x and y with two guarded RHSs
+--         | otherwise = 2
+--   f _ _             = 3   -- clause with a single, un-guarded RHS
+-- @
+--
+-- Returns one non-empty 'Nablas' for 1.) each pattern of a 'Match' and 2.)
+-- each of a 'Match'es 'GRHS' for Note [Long-distance information].
+--
+-- Special case: When there are /no matches/, then the functionassumes it
+-- checks and @-XEmptyCase@ with only a single match variable.
+-- See Note [Checking EmptyCase].
+pmcMatches
+  :: DsMatchContext                  -- ^ Match context, for warnings messages
+  -> [Id]                            -- ^ Match variables, i.e. x and y above
+  -> [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
+  -- 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!
+  !missing   <- getLdiNablas
+  tracePm "pmcMatches {" $
+          hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
+               2
+               (vcat (map ppr matches) $$ ppr missing)
+  case NE.nonEmpty matches of
+    Nothing -> do
+      -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
+      let var = only vars
+      empty_case <- desugarEmptyCase var
+      result <- unCA (checkEmptyCase empty_case) missing
+      tracePm "}: " (ppr (cr_uncov result))
+      formatReportWarnings cirbsEmptyCase ctxt vars result
+      return []
+    Just matches -> do
+      matches <- desugarMatches vars matches
+      result <- unCA (checkMatchGroup matches) missing
+      tracePm "}: " (ppr (cr_uncov result))
+      formatReportWarnings cirbsMatchGroup ctxt vars result
+      return (NE.toList (ldiMatchGroup (cr_ret result)))
+
+{- Note [pmcPatBind only checks PatBindRhs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+@pmcPatBind@'s sole purpose is to check vanilla pattern bindings, like
+@x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
+But its caller is also called for individual pattern guards in a @StmtCtxt@.
+For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
+go through this function. It makes no sense to do coverage checking there:
+  * Pattern guards may well fail. Fall-through is not an unrecoverable panic,
+    but rather behavior the programmer expects, so inexhaustivity should not be
+    reported.
+  * Redundancy is already reported for the whole GRHS via one of the other
+    exported coverage checking functions. Also reporting individual redundant
+    guards is... redundant. See #17646.
+Note that we can't just omit checking of @StmtCtxt@ altogether (by adjusting
+'isMatchContextPmChecked'), because that affects the other checking functions,
+too.
+-}
+
+--
+-- * Collecting long-distance information
+--
+
+ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
+ldiMatchGroup (PmMatchGroup matches) = ldiMatch <$> matches
+
+ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas)
+ldiMatch (PmMatch { pm_pats = red, pm_grhss = grhss }) =
+  (rs_cov red, ldiGRHS <$> grhss)
+
+ldiGRHS :: PmGRHS Post -> Nablas
+ldiGRHS (PmGRHS { pg_grds = red }) = rs_cov red
+
+--
+-- * Collecting redundancy information
+--
+
+-- | The result of redundancy checking:
+--    * RHSs classified as /C/overed, /I/naccessible and /R/edundant
+--    * And redundant /B/ang patterns. See Note [Dead bang patterns].
+data CIRB
+  = CIRB
+  { cirb_cov   :: !(OrdList SrcInfo) -- ^ Covered clauses
+  , cirb_inacc :: !(OrdList SrcInfo) -- ^ Inaccessible clauses
+  , cirb_red   :: !(OrdList SrcInfo) -- ^ Redundant clauses
+  , cirb_bangs :: !(OrdList SrcInfo) -- ^ Redundant bang patterns
+  }
+
+instance Semigroup CIRB where
+  CIRB a b c d <> CIRB e f g h = CIRB (a <> e) (b <> f) (c <> g) (d <> h)
+    where (<>) = (Semi.<>)
+
+instance Monoid CIRB where
+  mempty = CIRB mempty mempty mempty mempty
+
+markAllRedundant :: CIRB -> CIRB
+markAllRedundant CIRB { cirb_cov = cov, cirb_inacc = inacc, cirb_red = red } =
+  mempty { cirb_red = cov Semi.<> inacc Semi.<> red }
+
+-- See Note [Determining inaccessible clauses]
+ensureOneNotRedundant :: CIRB -> CIRB
+ensureOneNotRedundant ci = case ci of
+  CIRB { cirb_cov = NilOL, cirb_inacc = NilOL, cirb_red = ConsOL r rs }
+    -> ci { cirb_inacc = unitOL r, cirb_red = rs }
+  _ -> ci
+
+-- | Only adds the redundant bangs to the @CIRB@ if there is at least one
+-- non-redundant 'SrcInfo'. There is no point in remembering a redundant bang
+-- if the whole match is redundant!
+addRedundantBangs :: OrdList SrcInfo -> CIRB -> CIRB
+addRedundantBangs _red_bangs cirb@CIRB { cirb_cov = NilOL, cirb_inacc = NilOL } =
+  cirb
+addRedundantBangs red_bangs  cirb =
+  cirb { cirb_bangs = cirb_bangs cirb Semi.<> red_bangs }
+
+-- | Checks the 'Nablas' in a 'RedSets' for inhabitants and returns
+--    1. Whether the Covered set was inhabited
+--    2. Whether the Diverging set was inhabited
+--    3. All source bangs whose 'Nablas' were empty, which means they are
+--       redundant.
+testRedSets :: RedSets -> DsM (Bool, Bool, OrdList SrcInfo)
+testRedSets RedSets { rs_cov = cov, rs_div = div, rs_bangs = bangs } = do
+  is_covered  <- isInhabited cov
+  may_diverge <- isInhabited div
+  red_bangs   <- flip mapMaybeM (fromOL bangs) $ \(nablas, bang) -> do
+    isInhabited nablas >>= \case
+      True  -> pure Nothing
+      False -> pure (Just bang)
+  pure (is_covered, may_diverge, toOL red_bangs)
+
+cirbsMatchGroup :: PmMatchGroup Post -> DsM CIRB
+cirbsMatchGroup (PmMatchGroup matches) =
+  Semi.sconcat <$> traverse cirbsMatch matches
+
+cirbsMatch :: PmMatch Post -> DsM CIRB
+cirbsMatch PmMatch { pm_pats = red, pm_grhss = grhss } = do
+  (is_covered, may_diverge, red_bangs) <- testRedSets red
+  cirb <- cirbsGRHSs grhss
+  pure $ addRedundantBangs red_bangs
+       -- See Note [Determining inaccessible clauses]
+       $ applyWhen may_diverge ensureOneNotRedundant
+       $ applyWhen (not is_covered) markAllRedundant
+       $ cirb
+
+cirbsGRHSs :: NonEmpty (PmGRHS Post) -> DsM CIRB
+cirbsGRHSs grhss = Semi.sconcat <$> traverse cirbsGRHS grhss
+
+cirbsGRHS :: PmGRHS Post -> DsM CIRB
+cirbsGRHS PmGRHS { pg_grds = red, pg_rhs = info } = do
+  (is_covered, may_diverge, red_bangs) <- testRedSets red
+  let cirb | is_covered  = mempty { cirb_cov   = unitOL info }
+           | may_diverge = mempty { cirb_inacc = unitOL info }
+           | otherwise   = mempty { cirb_red   = unitOL info }
+  pure (addRedundantBangs red_bangs cirb)
+
+cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
+cirbsEmptyCase _ = pure mempty
+
+cirbsPatBind :: PmPatBind Post -> DsM CIRB
+cirbsPatBind = coerce cirbsGRHS
+
+{- Note [Determining inaccessible clauses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f _  True = ()
+  f () True = ()
+  f _  _    = ()
+Is f's second clause redundant? The perhaps surprising answer is, no, it isn't!
+@f (error "boom") False@ will force the error with clause 2, but will return
+() if it was deleted, so clearly not redundant. Yet for now combination of
+arguments we can ever reach clause 2's RHS, so we say it has inaccessible RHS
+(as opposed to being completely redundant).
+
+We detect an inaccessible RHS simply by pretending it's redundant, until we see
+-}
+
+--
+-- * Formatting and reporting warnings
+--
+
+-- | Given a function that collects 'CIRB's, this function will emit warnings
+-- for a 'CheckResult'.
+formatReportWarnings :: (ann -> DsM CIRB) -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
+formatReportWarnings collect ctx vars cr@CheckResult { cr_ret = ann } = do
+  cov_info <- collect ann
+  dflags <- getDynFlags
+  reportWarnings dflags ctx vars cr{cr_ret=cov_info}
+
+-- | Issue all the warnings
+-- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
+reportWarnings :: DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
+reportWarnings dflags ctx@(DsMatchContext kind loc) vars
+  CheckResult { cr_ret    = CIRB { cirb_inacc = inaccessible_rhss
+                                 , cirb_red   = redundant_rhss
+                                 , cirb_bangs = redundant_bangs }
+              , cr_uncov  = uncovered
+              , cr_approx = precision }
+  = when (flag_i || flag_u || flag_b) $ do
+      unc_examples <- getNFirstUncovered vars (maxPatterns + 1) uncovered
+      let exists_r = flag_i && notNull redundant_rhss
+          exists_i = flag_i && notNull inaccessible_rhss
+          exists_u = flag_u && notNull unc_examples
+          exists_b = flag_b && notNull redundant_bangs
+          approx   = precision == Approximate
+
+      when (approx && (exists_u || exists_i)) $
+        putSrcSpanDs loc (warnDs NoReason approx_msg)
+
+      when exists_b $ forM_ redundant_bangs $ \(SrcInfo (L l q)) -> do
+        putSrcSpanDs l (warnDs (Reason Opt_WarnRedundantBangPatterns)
+                               (pprEqn q "has redundant bang"))
+
+      when exists_r $ forM_ redundant_rhss $ \(SrcInfo (L l q)) -> do
+        putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
+                               (pprEqn q "is redundant"))
+      when exists_i $ forM_ inaccessible_rhss $ \(SrcInfo (L l q)) -> do
+        putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
+                               (pprEqn q "has inaccessible right hand side"))
+
+      when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
+        pprEqns vars unc_examples
+  where
+    flag_i = overlapping dflags kind
+    flag_u = exhaustive dflags kind
+    flag_b = redundantBang dflags
+    flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
+
+    maxPatterns = maxUncoveredPatterns dflags
+
+    -- Print a single clause (for redundant/with-inaccessible-rhs)
+    pprEqn q txt = pprContext True ctx (text txt) $ \f ->
+      f (q <+> matchSeparator kind <+> text "...")
+
+    -- Print several clauses (for uncovered clauses)
+    pprEqns vars nablas = pprContext False ctx (text "are non-exhaustive") $ \_ ->
+      case vars of -- See #11245
+           [] -> text "Guards do not cover entire pattern space"
+           _  -> let us = map (\nabla -> pprUncovered nabla vars) nablas
+                 in  hang (text "Patterns not matched:") 4
+                       (vcat (take maxPatterns us) $$ dots maxPatterns us)
+
+    approx_msg = vcat
+      [ hang
+          (text "Pattern match checker ran into -fmax-pmcheck-models="
+            <> int (maxPmCheckModels dflags)
+            <> text " limit, so")
+          2
+          (  bullet <+> text "Redundant clauses might not be reported at all"
+          $$ bullet <+> text "Redundant clauses might be reported as inaccessible"
+          $$ bullet <+> text "Patterns reported as unmatched might actually be matched")
+      , text "Increase the limit or resolve the warnings to suppress this message." ]
+
+getNFirstUncovered :: [Id] -> Int -> Nablas -> DsM [Nabla]
+getNFirstUncovered vars n (MkNablas nablas) = go n (bagToList nablas)
+  where
+    go 0 _              = pure []
+    go _ []             = pure []
+    go n (nabla:nablas) = do
+      front <- generateInhabitingPatterns vars n nabla
+      back <- go (n - length front) nablas
+      pure (front ++ back)
+
+dots :: Int -> [a] -> SDoc
+dots maxPatterns qs
+    | qs `lengthExceeds` maxPatterns = text "..."
+    | otherwise                      = empty
+
+pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
+pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
+  = vcat [text txt <+> msg,
+          sep [ text "In" <+> ppr_match <> char ':'
+              , nest 4 (rest_of_msg_fun pref)]]
+  where
+    txt | singular  = "Pattern match"
+        | otherwise = "Pattern match(es)"
+
+    (ppr_match, pref)
+        = case kind of
+             FunRhs { mc_fun = L _ fun }
+                  -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
+             _    -> (pprMatchContext kind, \ pp -> pp)
+
+--
+-- * Adding external long-distance information
+--
+
+-- | Locally update 'dsl_nablas' with the given action, but defer evaluation
+-- with 'unsafeInterleaveM' in order not to do unnecessary work.
+locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a
+locallyExtendPmNablas ext k = do
+  nablas <- getLdiNablas
+  nablas' <- unsafeInterleaveM $ ext nablas
+  updPmNablas nablas' k
+
+-- | Add in-scope type constraints if the coverage checker might run and then
+-- run the given action.
+addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
+addTyCs origin ev_vars m = do
+  dflags <- getDynFlags
+  applyWhen (needToRunPmCheck dflags origin)
+            (locallyExtendPmNablas $ \nablas ->
+              addPhiCtsNablas nablas (PhiTyCt . evVarPred <$> ev_vars))
+            m
+
+-- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment
+-- when checking a case expression:
+--     case e of x { matches }
+-- When checking matches we record that (x ~ e) where x is the initial
+-- uncovered. All matches will have to satisfy this equality.
+addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
+addCoreScrutTmCs Nothing    _   k = k
+addCoreScrutTmCs (Just scr) [x] k =
+  flip locallyExtendPmNablas k $ \nablas ->
+    addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
+addCoreScrutTmCs _   _   _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id"
+
+-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first.
+addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
+addHsScrutTmCs Nothing    _    k = k
+addHsScrutTmCs (Just scr) vars k = do
+  scr_e <- dsLExpr scr
+  addCoreScrutTmCs (Just scr_e) vars k
+
+{- Note [Long-distance information]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data Color = R | G | B
+  f :: Color -> Int
+  f R = …
+  f c = … (case c of
+          G -> True
+          B -> False) …
+
+Humans can make the "long-distance connection" between the outer pattern match
+and the nested case pattern match to see that the inner pattern match is
+exhaustive: @c@ can't be @R@ anymore because it was matched in the first clause
+of @f@.
+
+To achieve similar reasoning in the coverage checker, we keep track of the set
+of values that can reach a particular program point (often loosely referred to
+as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas'.
+We fill that set with Covered Nablas returned by the exported checking
+functions, which the call sites put into place with
+'GHC.HsToCore.Monad.updPmNablas'.
+Call sites also extend this set with facts from type-constraint dictionaries,
+case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
+and 'addHsScrutTmCs'.
+
+Note [Recovering from unsatisfiable pattern-matching constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following code (see #12957 and #15450):
+
+  f :: Int ~ Bool => ()
+  f = case True of { False -> () }
+
+We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
+used not to do this; in fact, it would warn that the match was /redundant/!
+This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
+coverage checker deems any matches with unsatisfiable constraint sets to be
+unreachable.
+
+We make sure to always start from an inhabited 'Nablas' by calling
+'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the
+long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty.
+-}
diff --git a/compiler/GHC/HsToCore/Pmc/Check.hs b/compiler/GHC/HsToCore/Pmc/Check.hs
new file mode 100644
index 0000000000..49cf79965e
--- /dev/null
+++ b/compiler/GHC/HsToCore/Pmc/Check.hs
@@ -0,0 +1,276 @@
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE MultiWayIf                 #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE NamedFieldPuns             #-}
+{-# LANGUAGE FlexibleInstances          #-}
+
+-- | Coverage checking step of the
+-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
+--
+-- Coverage check guard trees (like @'PmMatch' 'Pre'@) to get a
+-- 'CheckResult', containing
+--
+--   1. The set of uncovered values, 'cr_uncov'
+--   2. And an annotated tree variant (like @'PmMatch' 'Post'@) that captures
+--      redundancy and inaccessibility information as 'RedSets' annotations
+--
+-- Basically the UA function from Section 5.1, which is an optimised
+-- interleaving of U and A from Section 3.2 (Figure 5).
+-- The Normalised Refinement Types 'Nablas' are maintained in
+-- "GHC.HsToCore.Pmc.Solver".
+module GHC.HsToCore.Pmc.Check (
+        CheckAction(..),
+        checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase
+    ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Monad ( DsM )
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils
+import GHC.HsToCore.Pmc.Solver
+import GHC.Driver.Session
+import GHC.Utils.Outputable
+import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Data.OrdList
+
+import qualified Data.Semigroup as Semi
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+import Data.Coerce
+
+-- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
+newtype CheckAction a = CA { unCA :: Nablas -> DsM (CheckResult a) }
+  deriving Functor
+
+-- | Composes 'CheckAction's top-to-bottom:
+-- If a value falls through the resulting action, then it must fall through the
+-- first action and then through the second action.
+-- If a value matches the resulting action, then it either matches the
+-- first action or matches the second action.
+-- Basically the semantics of the LYG branching construct.
+topToBottom :: (top -> bot -> ret)
+            -> CheckAction top
+            -> CheckAction bot
+            -> CheckAction ret
+topToBottom f (CA top) (CA bot) = CA $ \inc -> do
+  t <- top inc
+  b <- bot (cr_uncov t)
+  pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
+                   , cr_uncov = cr_uncov b
+                   , cr_approx = cr_approx t Semi.<> cr_approx b }
+
+
+-- | Composes 'CheckAction's left-to-right:
+-- If a value falls through the resulting action, then it either falls through the
+-- first action or through the second action.
+-- If a value matches the resulting action, then it must match the first action
+-- and then match the second action.
+-- Basically the semantics of the LYG guard construct.
+leftToRight :: (RedSets -> right -> ret)
+            -> CheckAction RedSets
+            -> CheckAction right
+            -> CheckAction ret
+leftToRight f (CA left) (CA right) = CA $ \inc -> do
+  l <- left inc
+  r <- right (rs_cov (cr_ret l))
+  limit <- maxPmCheckModels <$> getDynFlags
+  let uncov = cr_uncov l Semi.<> cr_uncov r
+  -- See Note [Countering exponential blowup]
+  let (prec', uncov') = throttle limit inc uncov
+  pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
+                   , cr_uncov = uncov'
+                   , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }
+
+-- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@
+-- is exceeding the given @limit@ and the @old@ number of 'Nabla's.
+-- See Note [Countering exponential blowup].
+throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
+throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
+  --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
+  | length new_ds > max limit (length old_ds) = (Approximate, old)
+  | otherwise                                 = (Precise,     new)
+
+checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
+-- The implementation is pretty similar to
+-- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
+checkSequence act (t :| [])       = (:| []) <$> act t
+checkSequence act (t1 :| (t2:ts)) =
+  topToBottom (NE.<|) (act t1) (checkSequence act (t2:|ts))
+
+emptyRedSets :: RedSets
+-- Semigroup instance would be misleading!
+emptyRedSets = RedSets mempty mempty mempty
+
+checkGrd :: PmGrd -> CheckAction RedSets
+checkGrd grd = CA $ \inc -> case grd of
+  -- let x = e: Refine with x ~ e
+  PmLet x e -> do
+    matched <- addPhiCtNablas inc (PhiCoreCt x e)
+    tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
+    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
+                     , cr_uncov = mempty
+                     , cr_approx = Precise }
+  -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
+  PmBang x mb_info -> do
+    div <- addPhiCtNablas inc (PhiBotCt x)
+    matched <- addPhiCtNablas inc (PhiNotBotCt x)
+    -- See Note [Dead bang patterns]
+    -- mb_info = Just info <==> PmBang originates from bang pattern in source
+    let bangs | Just info <- mb_info = unitOL (div, info)
+              | otherwise            = NilOL
+    tracePm "check:Bang" (ppr x <+> ppr div)
+    pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
+                     , cr_uncov = mempty
+                     , cr_approx = Precise }
+  -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
+  PmCon x con tvs dicts args -> do
+    !div <- if isPmAltConMatchStrict con
+      then addPhiCtNablas inc (PhiBotCt x)
+      else pure mempty
+    !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
+    !uncov   <- addPhiCtNablas inc (PhiNotConCt x con)
+    tracePm "check:Con" $ vcat
+      [ ppr grd
+      , ppr inc
+      , hang (text "div") 2 (ppr div)
+      , hang (text "matched") 2 (ppr matched)
+      , hang (text "uncov") 2 (ppr uncov)
+      ]
+    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
+                     , cr_uncov = uncov
+                     , cr_approx = Precise }
+
+checkGrds :: [PmGrd] -> CheckAction RedSets
+checkGrds [] = CA $ \inc ->
+  pure CheckResult { cr_ret = emptyRedSets { rs_cov = inc }
+                   , cr_uncov = mempty
+                   , cr_approx = Precise }
+checkGrds (g:grds) = leftToRight merge (checkGrd g) (checkGrds grds)
+  where
+    merge ri_g ri_grds = -- This operation would /not/ form a Semigroup!
+      RedSets { rs_cov   = rs_cov ri_grds
+              , rs_div   = rs_div ri_g   Semi.<> rs_div ri_grds
+              , rs_bangs = rs_bangs ri_g Semi.<> rs_bangs ri_grds }
+
+checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
+checkMatchGroup (PmMatchGroup matches) =
+  PmMatchGroup <$> checkSequence checkMatch matches
+
+checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
+checkMatch (PmMatch { pm_pats = GrdVec grds, pm_grhss = grhss }) =
+  leftToRight PmMatch (checkGrds grds) (checkGRHSs grhss)
+
+checkGRHSs :: NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
+checkGRHSs = checkSequence checkGRHS
+
+checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
+checkGRHS (PmGRHS { pg_grds = GrdVec grds, pg_rhs = rhs_info }) =
+  flip PmGRHS rhs_info <$> checkGrds grds
+
+checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
+-- See Note [Checking EmptyCase]
+checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
+  unc <- addPhiCtNablas inc (PhiNotBotCt var)
+  pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
+
+checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
+checkPatBind = coerce checkGRHS
+
+{- Note [Checking EmptyCase]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-XEmptyCase is useful for matching on empty data types like 'Void'. For example,
+the following is a complete match:
+
+    f :: Void -> ()
+    f x = case x of {}
+
+Really, -XEmptyCase is the only way to write a program that at the same time is
+safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
+(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
+exception into divergence (@f x = f x@).
+
+Semantically, unlike every other case expression, -XEmptyCase is strict in its
+match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
+initial Nabla and check if there are any values left to match on.
+
+Note [Dead bang patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  f :: Bool -> Int
+  f True = 1
+  f !x   = 2
+
+Whenever we fall through to the second equation, we will already have evaluated
+the argument. Thus, the bang pattern serves no purpose and should be warned
+about. We call this kind of bang patterns "dead". Dead bangs are the ones
+that under no circumstances can force a thunk that wasn't already forced.
+Dead bangs are a form of redundant bangs; see below.
+
+We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
+where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
+dead. So for a source bang, we add the refined Nabla and the source info to
+the 'RedSet's 'rs_bangs'. When collecting stuff to warn, we test that Nabla for
+inhabitants. If it's empty, we'll warn that it's redundant.
+
+Note that we don't want to warn for a dead bang that appears on a redundant
+clause. That is because in that case, we recommend to delete the clause wholly,
+including its leading pattern match.
+
+Dead bang patterns are redundant. But there are bang patterns which are
+redundant that aren't dead, for example
+
+  f !() = 0
+
+the bang still forces the match variable, before we attempt to match on (). But
+it is redundant with the forcing done by the () match. We currently don't
+detect redundant bangs that aren't dead.
+
+Note [Countering exponential blowup]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Precise pattern match exhaustiveness checking is necessarily exponential in
+the size of some input programs. We implement a counter-measure in the form of
+the -fmax-pmcheck-models flag, limiting the number of Nablas we check against
+each pattern by a constant.
+
+How do we do that? Consider
+
+  f True True = ()
+  f True True = ()
+
+And imagine we set our limit to 1 for the sake of the example. The first clause
+will be checked against the initial Nabla, {}. Doing so will produce an
+Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
+Also we find the first clause to cover the model {x~True,y~True}.
+
+But the Uncovered set we get out of the match is too huge! We somehow have to
+ensure not to make things worse as they are already, so we continue checking
+with a singleton Uncovered set of the initial Nabla {}. Why is this
+sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
+to forgetting that we matched against the first clause. The values represented
+by {} are a superset of those represented by its two refinements {x≁True} and
+{x~True,y≁True}.
+
+This forgetfulness becomes very apparent in the example above: By continuing
+with {} we don't detect the second clause as redundant, as it again covers the
+same non-empty subset of {}. So we don't flag everything as redundant anymore,
+but still will never flag something as redundant that isn't.
+
+For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
+and report @f _ _@ as missing, which is a superset of the actual missing
+matches. But soundness means we will never fail to report a missing match.
+
+This mechanism is implemented in 'throttle'.
+
+Guards are an extreme example in this regard, with #11195 being a particularly
+dreadful example: Since their RHS are often pretty much unique, we split on a
+variable (the one representing the RHS) that doesn't occur anywhere else in the
+program, so we don't actually get useful information out of that split!
+-}
diff --git a/compiler/GHC/HsToCore/Pmc/Desugar.hs b/compiler/GHC/HsToCore/Pmc/Desugar.hs
new file mode 100644
index 0000000000..07b0095dd2
--- /dev/null
+++ b/compiler/GHC/HsToCore/Pmc/Desugar.hs
@@ -0,0 +1,450 @@
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE TupleSections              #-}
+{-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE MultiWayIf                 #-}
+{-# LANGUAGE LambdaCase                 #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE NamedFieldPuns             #-}
+{-# LANGUAGE FlexibleInstances          #-}
+
+-- | Desugaring step of the
+-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
+--
+-- Desugars Haskell source syntax into guard tree variants Pm*.
+-- In terms of the paper, this module is concerned with Sections 3.1, Figure 4,
+-- in particular.
+module GHC.HsToCore.Pmc.Desugar (
+      desugarPatBind, desugarGRHSs, desugarMatches, desugarEmptyCase
+    ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils
+import GHC.Core (Expr(Var,App))
+import GHC.Data.FastString (unpackFS, lengthFS)
+import GHC.Driver.Session
+import GHC.Hs
+import GHC.Tc.Utils.Zonk (shortCutLit)
+import GHC.Types.Id
+import GHC.Core.ConLike
+import GHC.Types.Name
+import GHC.Builtin.Types
+import GHC.Types.SrcLoc
+import GHC.Utils.Outputable
+import GHC.Utils.Panic
+import GHC.Core.DataCon
+import GHC.Types.Var (EvVar)
+import GHC.Core.Coercion
+import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper)
+import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr)
+import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper)
+import GHC.HsToCore.Utils (selectMatchVar)
+import GHC.HsToCore.Match.Literal (dsLit, dsOverLit)
+import GHC.HsToCore.Monad
+import GHC.Core.TyCo.Rep
+import GHC.Core.Type
+import GHC.HsToCore.Utils       (isTrueLHsExpr)
+import GHC.Data.Maybe
+import qualified GHC.LanguageExtensions as LangExt
+import GHC.Utils.Monad (concatMapM)
+
+import Control.Monad (zipWithM)
+import Data.List (elemIndex)
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+
+-- | Smart constructor that eliminates trivial lets
+mkPmLetVar :: Id -> Id -> [PmGrd]
+mkPmLetVar x y | x == y = []
+mkPmLetVar x y          = [PmLet x (Var y)]
+
+-- | ADT constructor pattern => no existentials, no local constraints
+vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
+vanillaConGrd scrut con arg_ids =
+  PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
+        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
+
+-- | Creates a '[PmGrd]' refining a match var of list type to a list,
+-- where list fields are matched against the incoming tagged '[PmGrd]'s.
+-- For example:
+--   @mkListGrds "a" "[(x, True <- x),(y, !y)]"@
+-- to
+--   @"[(x:b) <- a, True <- x, (y:c) <- b, !y, [] <- c]"@
+-- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match
+-- variable.
+mkListGrds :: Id -> [(Id, [PmGrd])] -> DsM [PmGrd]
+-- See Note [Order of guards matter] for why we need to intertwine guards
+-- on list elements.
+mkListGrds a []                  = pure [vanillaConGrd a nilDataCon []]
+mkListGrds a ((x, head_grds):xs) = do
+  b <- mkPmId (idType a)
+  tail_grds <- mkListGrds b xs
+  pure $ vanillaConGrd a consDataCon [x, b] : head_grds ++ tail_grds
+
+-- | Create a '[PmGrd]' refining a match variable to a 'PmLit'.
+mkPmLitGrds :: Id -> PmLit -> DsM [PmGrd]
+mkPmLitGrds x (PmLit _ (PmLitString s)) = do
+  -- We desugar String literals to list literals for better overlap reasoning.
+  -- It's a little unfortunate we do this here rather than in
+  -- 'GHC.HsToCore.Pmc.Solver.trySolve' and
+  -- 'GHC.HsToCore.Pmc.Solver.addRefutableAltCon', but it's so much simpler
+  -- here. See Note [Representation of Strings in TmState] in
+  -- GHC.HsToCore.Pmc.Solver
+  vars <- traverse mkPmId (take (lengthFS s) (repeat charTy))
+  let mk_char_lit y c = mkPmLitGrds y (PmLit charTy (PmLitChar c))
+  char_grdss <- zipWithM mk_char_lit vars (unpackFS s)
+  mkListGrds x (zip vars char_grdss)
+mkPmLitGrds x lit = do
+  let grd = PmCon { pm_id = x
+                  , pm_con_con = PmAltLit lit
+                  , pm_con_tvs = []
+                  , pm_con_dicts = []
+                  , pm_con_args = [] }
+  pure [grd]
+
+-- | @desugarPat _ x pat@ transforms @pat@ into a '[PmGrd]', where
+-- the variable representing the match is @x@.
+desugarPat :: Id -> Pat GhcTc -> DsM [PmGrd]
+desugarPat x pat = case pat of
+  WildPat  _ty -> pure []
+  VarPat _ y   -> pure (mkPmLetVar (unLoc y) x)
+  ParPat _ p   -> desugarLPat x p
+  LazyPat _ _  -> pure [] -- like a wildcard
+  BangPat _ p@(L l p') ->
+    -- Add the bang in front of the list, because it will happen before any
+    -- nested stuff.
+    (PmBang x pm_loc :) <$> desugarLPat x p
+      where pm_loc = Just (SrcInfo (L l (ppr p')))
+
+  -- (x@pat)   ==>   Desugar pat with x as match var and handle impedance
+  --                 mismatch with incoming match var
+  AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> desugarLPat y p
+
+  SigPat _ p _ty -> desugarLPat x p
+
+  -- See Note [Desugar CoPats]
+  -- Generally the translation is
+  -- pat |> co   ===>   let y = x |> co, pat <- y  where y is a match var of pat
+  XPat (CoPat wrapper p _ty)
+    | isIdHsWrapper wrapper                   -> desugarPat x p
+    | WpCast co <-  wrapper, isReflexiveCo co -> desugarPat x p
+    | otherwise -> do
+        (y, grds) <- desugarPatV p
+        wrap_rhs_y <- dsHsWrapper wrapper
+        pure (PmLet y (wrap_rhs_y (Var x)) : grds)
+
+  -- (n + k)  ===>   let b = x >= k, True <- b, let n = x-k
+  NPlusKPat _pat_ty (L _ n) k1 k2 ge minus -> do
+    b <- mkPmId boolTy
+    let grd_b = vanillaConGrd b trueDataCon []
+    [ke1, ke2] <- traverse dsOverLit [unLoc k1, k2]
+    rhs_b <- dsSyntaxExpr ge    [Var x, ke1]
+    rhs_n <- dsSyntaxExpr minus [Var x, ke2]
+    pure [PmLet b rhs_b, grd_b, PmLet n rhs_n]
+
+  -- (fun -> pat)   ===>   let y = fun x, pat <- y where y is a match var of pat
+  ViewPat _arg_ty lexpr pat -> do
+    (y, grds) <- desugarLPatV pat
+    fun <- dsLExpr lexpr
+    pure $ PmLet y (App fun (Var x)) : grds
+
+  -- list
+  ListPat (ListPatTc _elem_ty Nothing) ps ->
+    desugarListPat x ps
+
+  -- overloaded list
+  ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do
+    dflags <- getDynFlags
+    case splitListTyConApp_maybe pat_ty of
+      Just _e_ty
+        | not (xopt LangExt.RebindableSyntax dflags)
+        -- Just desugar it as a regular ListPat
+        -> desugarListPat x pats
+      _ -> do
+        y <- mkPmId (mkListTy elem_ty)
+        grds <- desugarListPat y pats
+        rhs_y <- dsSyntaxExpr to_list [Var x]
+        pure $ PmLet y rhs_y : grds
+
+    -- (a) In the presence of RebindableSyntax, we don't know anything about
+    --     `toList`, we should treat `ListPat` as any other view pattern.
+    --
+    -- (b) In the absence of RebindableSyntax,
+    --     - If the pat_ty is `[a]`, then we treat the overloaded list pattern
+    --       as ordinary list pattern. Although we can give an instance
+    --       `IsList [Int]` (more specific than the default `IsList [a]`), in
+    --       practice, we almost never do that. We assume the `to_list` is
+    --       the `toList` from `instance IsList [a]`.
+    --
+    --     - Otherwise, we treat the `ListPat` as ordinary view pattern.
+    --
+    -- See #14547, especially comment#9 and comment#10.
+
+  ConPat { pat_con     = L _ con
+         , pat_args    = ps
+         , pat_con_ext = ConPatTc
+           { cpt_arg_tys = arg_tys
+           , cpt_tvs     = ex_tvs
+           , cpt_dicts   = dicts
+           }
+         } -> do
+    desugarConPatOut x con arg_tys ex_tvs dicts ps
+
+  NPat ty (L _ olit) mb_neg _ -> do
+    -- See Note [Literal short cut] in "GHC.HsToCore.Match.Literal"
+    -- We inline the Literal short cut for @ty@ here, because @ty@ is more
+    -- precise than the field of OverLitTc, which is all that dsOverLit (which
+    -- normally does the literal short cut) can look at. Also @ty@ matches the
+    -- type of the scrutinee, so info on both pattern and scrutinee (for which
+    -- short cutting in dsOverLit works properly) is overloaded iff either is.
+    dflags <- getDynFlags
+    let platform = targetPlatform dflags
+    core_expr <- case olit of
+      OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ }
+        | not rebindable
+        , Just expr <- shortCutLit platform val ty
+        -> dsExpr expr
+      _ -> dsOverLit olit
+    let lit  = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr)
+    let lit' = case mb_neg of
+          Just _  -> expectJust "failed to negate lit" (negatePmLit lit)
+          Nothing -> lit
+    mkPmLitGrds x lit'
+
+  LitPat _ lit -> do
+    core_expr <- dsLit (convertLit lit)
+    let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr)
+    mkPmLitGrds x lit
+
+  TuplePat _tys pats boxity -> do
+    (vars, grdss) <- mapAndUnzipM desugarLPatV pats
+    let tuple_con = tupleDataCon boxity (length vars)
+    pure $ vanillaConGrd x tuple_con vars : concat grdss
+
+  SumPat _ty p alt arity -> do
+    (y, grds) <- desugarLPatV p
+    let sum_con = sumDataCon alt arity
+    -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
+    pure $ vanillaConGrd x sum_con [y] : grds
+
+  SplicePat {} -> panic "Check.desugarPat: SplicePat"
+
+-- | 'desugarPat', but also select and return a new match var.
+desugarPatV :: Pat GhcTc -> DsM (Id, [PmGrd])
+desugarPatV pat = do
+  x <- selectMatchVar Many pat
+  grds <- desugarPat x pat
+  pure (x, grds)
+
+desugarLPat :: Id -> LPat GhcTc -> DsM [PmGrd]
+desugarLPat x = desugarPat x . unLoc
+
+-- | 'desugarLPat', but also select and return a new match var.
+desugarLPatV :: LPat GhcTc -> DsM (Id, [PmGrd])
+desugarLPatV = desugarPatV . unLoc
+
+-- | @desugarListPat _ x [p1, ..., pn]@ is basically
+--   @desugarConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
+-- constructing the 'ConPatOut's.
+desugarListPat :: Id -> [LPat GhcTc] -> DsM [PmGrd]
+desugarListPat x pats = do
+  vars_and_grdss <- traverse desugarLPatV pats
+  mkListGrds x vars_and_grdss
+
+-- | Desugar a constructor pattern
+desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
+                 -> [EvVar] -> HsConPatDetails GhcTc -> DsM [PmGrd]
+desugarConPatOut x con univ_tys ex_tvs dicts = \case
+    PrefixCon ps                 -> go_field_pats (zip [0..] ps)
+    InfixCon  p1 p2              -> go_field_pats (zip [0..] [p1,p2])
+    RecCon    (HsRecFields fs _) -> go_field_pats (rec_field_ps fs)
+  where
+    -- The actual argument types (instantiated)
+    arg_tys     = map scaledThing $ conLikeInstOrigArgTys con (univ_tys ++ mkTyVarTys ex_tvs)
+
+    -- Extract record field patterns tagged by field index from a list of
+    -- LHsRecField
+    rec_field_ps fs = map (tagged_pat . unLoc) fs
+      where
+        tagged_pat f = (lbl_to_index (getName (hsRecFieldId f)), hsRecFieldArg f)
+        -- Unfortunately the label info is empty when the DataCon wasn't defined
+        -- with record field labels, hence we desugar to field index.
+        orig_lbls        = map flSelector $ conLikeFieldLabels con
+        lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls
+
+    go_field_pats tagged_pats = do
+      -- The fields that appear might not be in the correct order. So
+      --   1. Do the PmCon match
+      --   2. Then pattern match on the fields in the order given by the first
+      --      field of @tagged_pats@.
+      -- See Note [Field match order for RecCon]
+
+      -- Desugar the mentioned field patterns. We're doing this first to get
+      -- the Ids for pm_con_args and bring them in order afterwards.
+      let trans_pat (n, pat) = do
+            (var, pvec) <- desugarLPatV pat
+            pure ((n, var), pvec)
+      (tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats
+
+      let get_pat_id n ty = case lookup n tagged_vars of
+            Just var -> pure var
+            Nothing  -> mkPmId ty
+
+      -- 1. the constructor pattern match itself
+      arg_ids <- zipWithM get_pat_id [0..] arg_tys
+      let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
+
+      -- 2. guards from field selector patterns
+      let arg_grds = concat arg_grdss
+
+      -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
+      pure (con_grd : arg_grds)
+
+desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre)
+-- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
+desugarPatBind loc var pat =
+  PmPatBind . flip PmGRHS (SrcInfo (L loc (ppr pat))) . GrdVec <$> desugarPat var pat
+
+desugarEmptyCase :: Id -> DsM PmEmptyCase
+desugarEmptyCase var = pure PmEmptyCase { pe_var = var }
+
+-- | Desugar the non-empty 'Match'es of a 'MatchGroup'.
+desugarMatches :: [Id] -> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
+               -> DsM (PmMatchGroup Pre)
+desugarMatches vars matches =
+  PmMatchGroup <$> traverse (desugarMatch vars) matches
+
+-- Desugar a single match
+desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PmMatch Pre)
+desugarMatch vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
+  pats'  <- concat <$> zipWithM desugarLPat vars pats
+  grhss' <- desugarGRHSs match_loc (sep (map ppr pats)) grhss
+  -- tracePm "desugarMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
+  return PmMatch { pm_pats = GrdVec pats', pm_grhss = grhss' }
+
+desugarGRHSs :: SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty (PmGRHS Pre))
+desugarGRHSs match_loc pp_pats grhss
+  = traverse (desugarLGRHS match_loc pp_pats)
+  . expectJust "desugarGRHSs"
+  . NE.nonEmpty
+  $ grhssGRHSs grhss
+
+-- | Desugar a guarded right-hand side to a single 'GrdTree'
+desugarLGRHS :: SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM (PmGRHS Pre)
+desugarLGRHS match_loc pp_pats (L _loc (GRHS _ gs _)) = do
+  -- _loc points to the match separator (ie =, ->) that comes after the guards.
+  -- Hence we have to pass in the match_loc, which we use in case that the RHS
+  -- is unguarded.
+  -- 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@.
+  let rhs_info = case gs of
+        []              -> L match_loc pp_pats
+        (L grd_loc _):_ -> L grd_loc   (pp_pats <+> vbar <+> interpp'SP gs)
+  grds <- concatMapM (desugarGuard . unLoc) gs
+  pure PmGRHS { pg_grds = GrdVec grds, pg_rhs = SrcInfo rhs_info }
+
+-- | Desugar a guard statement to a '[PmGrd]'
+desugarGuard :: GuardStmt GhcTc -> DsM [PmGrd]
+desugarGuard guard = case guard of
+  BodyStmt _   e _ _ -> desugarBoolGuard e
+  LetStmt  _   binds -> desugarLet (unLoc binds)
+  BindStmt _ p e     -> desugarBind p e
+  LastStmt        {} -> panic "desugarGuard LastStmt"
+  ParStmt         {} -> panic "desugarGuard ParStmt"
+  TransStmt       {} -> panic "desugarGuard TransStmt"
+  RecStmt         {} -> panic "desugarGuard RecStmt"
+  ApplicativeStmt {} -> panic "desugarGuard ApplicativeLastStmt"
+
+-- | Desugar let-bindings
+desugarLet :: HsLocalBinds GhcTc -> DsM [PmGrd]
+desugarLet _binds = return []
+
+-- | Desugar a pattern guard
+--   @pat <- e ==>  let x = e;  <guards for pat <- x>@
+desugarBind :: LPat GhcTc -> LHsExpr GhcTc -> DsM [PmGrd]
+desugarBind p e = dsLExpr e >>= \case
+  Var y
+    | Nothing <- isDataConId_maybe y
+    -- RHS is a variable, so that will allow us to omit the let
+    -> desugarLPat y p
+  rhs -> do
+    (x, grds) <- desugarLPatV p
+    pure (PmLet x rhs : grds)
+
+-- | Desugar a boolean guard
+--   @e ==>  let x = e; True <- x@
+desugarBoolGuard :: LHsExpr GhcTc -> DsM [PmGrd]
+desugarBoolGuard e
+  | isJust (isTrueLHsExpr e) = return []
+    -- The formal thing to do would be to generate (True <- True)
+    -- but it is trivial to solve so instead we give back an empty
+    -- [PmGrd] for efficiency
+  | otherwise = dsLExpr e >>= \case
+      Var y
+        | Nothing <- isDataConId_maybe y
+        -- Omit the let by matching on y
+        -> pure [vanillaConGrd y trueDataCon []]
+      rhs -> do
+        x <- mkPmId boolTy
+        pure [PmLet x rhs, vanillaConGrd x trueDataCon []]
+
+{- Note [Field match order for RecCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The order for RecCon field patterns actually determines evaluation order of
+the pattern match. For example:
+
+  data T = T { a :: Char, b :: Int }
+  f :: T -> ()
+  f T{ b = 42, a = 'a' } = ()
+
+Then @f (T (error "a") (error "b"))@ errors out with "b" because it is mentioned
+first in the pattern match.
+
+This means we can't just desugar the pattern match to
+@[T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the
+right order: @[T a b <- x, 42 <- b, 'a' <- a]@.
+
+Note [Order of guards matters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Similar to Note [Field match order for RecCon], the order in which the guards
+for a pattern match appear matter. Consider a situation similar to T5117:
+
+  f (0:_)  = ()
+  f (0:[]) = ()
+
+The latter clause is clearly redundant. Yet if we desugar the second clause as
+
+  [x:xs' <- xs, [] <- xs', 0 <- x]
+
+We will say that the second clause only has an inaccessible RHS. That's because
+we force the tail of the list before comparing its head! So the correct
+translation would have been
+
+  [x:xs' <- xs, 0 <- x, [] <- xs']
+
+And we have to take in the guards on list cells into @mkListGrds@.
+
+Note [Desugar CoPats]
+~~~~~~~~~~~~~~~~~~~~~~~
+The pattern match checker did not know how to handle coerced patterns
+`CoPat` efficiently, which gave rise to #11276. The original approach
+desugared `CoPat`s:
+
+    pat |> co    ===>    x (pat <- (x |> co))
+
+Why did we do this seemingly unnecessary expansion in the first place?
+The reason is that the type of @pat |> co@ (which is the type of the value
+abstraction we match against) might be different than that of @pat@. Data
+instances such as @Sing (a :: Bool)@ are a good example of this: If we would
+just drop the coercion, we'd get a type error when matching @pat@ against its
+value abstraction, with the result being that pmIsSatisfiable decides that every
+possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
+a lot of false warnings.
+
+But we can check whether the coercion is a hole or if it is just refl, in
+which case we can drop it.
+-}
diff --git a/compiler/GHC/HsToCore/PmCheck/Ppr.hs b/compiler/GHC/HsToCore/Pmc/Ppr.hs
index 94ea9d6361..ebad0757b2 100644
--- a/compiler/GHC/HsToCore/PmCheck/Ppr.hs
+++ b/compiler/GHC/HsToCore/Pmc/Ppr.hs
@@ -4,7 +4,7 @@
 
 -- | Provides factilities for pretty-printing 'Nabla's in a way appropriate for
 -- user facing pattern match warnings.
-module GHC.HsToCore.PmCheck.Ppr (
+module GHC.HsToCore.Pmc.Ppr (
         pprUncovered
     ) where
 
@@ -26,8 +26,8 @@ import GHC.Utils.Misc
 import GHC.Data.Maybe
 import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)
 
-import GHC.HsToCore.PmCheck.Types
-import GHC.HsToCore.PmCheck.Oracle
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Solver
 
 -- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
 -- components and refutable shapes associated to any mentioned variables.
@@ -93,7 +93,7 @@ Unhandled constraints that refer to HsExpr are typically ignored by the solver
 (it does not even substitute in HsExpr so they are even printed as wildcards).
 Additionally, the oracle returns a substitution if it succeeds so we apply this
 substitution to the vectors before printing them out (see function `pprOne' in
-"GHC.HsToCore.PmCheck") to be more precise.
+"GHC.HsToCore.Pmc") to be more precise.
 -}
 
 -- | Extract and assigns pretty names to constraint variables with refutable
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index fd76bcf70d..cfbe6c3b94 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -7,34 +7,41 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
 {-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns,
              MultiWayIf, ScopedTypeVariables, MagicHash #-}
 
--- | The pattern match oracle. The main export of the module are the functions
--- 'addPhiCts' for adding facts to the oracle, and 'generateInhabitingPatterns' to turn a
--- 'Nabla' into a concrete evidence for an equation.
+-- | Model refinements type as per the
+-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
+-- The main export of the module are the functions 'addPhiCtsNablas' for adding
+-- facts to the oracle, 'isInhabited' to check if a refinement type is inhabited
+-- and 'generateInhabitingPatterns' to turn a 'Nabla' into a concrete pattern
+-- for an equation.
 --
--- In terms of the [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989)
--- describing the implementation, this module is concerned with Sections 3.4, 3.6 and 3.7.
--- E.g., it represents refinement types directly as a normalised refinement type 'Nabla'.
-module GHC.HsToCore.PmCheck.Oracle (
+-- In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6
+-- and 3.7. E.g., it represents refinement types directly as a bunch of
+-- normalised refinement types 'Nabla'.
+module GHC.HsToCore.Pmc.Solver (
 
-        DsM, tracePm, mkPmId,
-        Nabla, initNablas, lookupRefuts, lookupSolution,
+        Nabla, Nablas(..), initNablas,
+        lookupRefuts, lookupSolution,
 
         PhiCt(..), PhiCts,
+        addPhiCtNablas,
+        addPhiCtsNablas,
 
-        addPhiCts,           -- Add a constraint to the oracle.
+        isInhabited,
         generateInhabitingPatterns
+
     ) where
 
 #include "HsVersions.h"
 
 import GHC.Prelude
 
-import GHC.HsToCore.PmCheck.Types
+import GHC.HsToCore.Pmc.Types
+import GHC.HsToCore.Pmc.Utils ( tracePm, mkPmId )
 
 import GHC.Driver.Session
 import GHC.Driver.Config
 import GHC.Utils.Outputable
-import GHC.Utils.Error
+import GHC.Utils.Error ( pprErrMsgBagWithLoc )
 import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Data.Bag
@@ -68,7 +75,6 @@ import GHC.Core.Type
 import GHC.Tc.Solver   (tcNormalise, tcCheckSatisfiability)
 import GHC.Core.Unify    (tcMatchTy)
 import GHC.Core.Coercion
-import GHC.Utils.Monad hiding (foldlM)
 import GHC.HsToCore.Monad hiding (foldlM)
 import GHC.Tc.Instance.Family
 import GHC.Core.FamInstEnv
@@ -82,40 +88,32 @@ import Data.Foldable (foldlM, minimumBy, toList)
 import Data.List     (sortBy, find)
 import qualified Data.List.NonEmpty as NE
 import Data.Ord      (comparing)
-import Data.Tuple    (swap)
-
-import GHC.Driver.Ppr (pprTrace)
-
--- Debugging Infrastructure
 
-tracePm :: String -> SDoc -> DsM ()
-tracePm herald doc = do
-  dflags <- getDynFlags
-  printer <- mkPrintUnqualifiedDs
-  liftIO $ dumpIfSet_dyn_printer printer dflags
-            Opt_D_dump_ec_trace "" FormatText (text herald $$ (nest 2 doc))
-{-# INLINE tracePm #-}  -- see Note [INLINE conditional tracing utilities]
+--
+-- * Main exports
+--
 
-debugOn :: () -> Bool
-debugOn _ = False
--- debugOn _ = True
+-- | Add a bunch of 'PhiCt's to all the 'Nabla's.
+-- Lifts 'addPhiCts' over many 'Nablas'.
+addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
+addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
 
-trc :: String -> SDoc -> a -> a
-trc | debugOn () = pprTrace
-    | otherwise  = \_ _ a -> a
+-- | 'addPmCtsNablas' for a single 'PmCt'.
+addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
+addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
 
-_trcM :: Monad m => String -> SDoc -> m ()
-_trcM header doc = trc header doc (return ())
+liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
+liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
 
--- | Generate a fresh `Id` of a given type
-mkPmId :: Type -> DsM Id
-mkPmId ty = getUniqueM >>= \unique ->
-  let occname = mkVarOccFS $ fsLit "pm"
-      name    = mkInternalName unique occname noSrcSpan
-  in  return (mkLocalIdOrCoVar name Many ty)
+-- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
+-- we preserve the invariant that there are no uninhabited 'Nabla's. But that
+-- could change in the future, for example by implementing this function in
+-- terms of @notNull <$> generateInhabitingPatterns 1 ds@.
+isInhabited :: Nablas -> DsM Bool
+isInhabited (MkNablas ds) = pure (not (null ds))
 
 -----------------------------------------------
--- * Caching residual COMPLETE set
+-- * Caching residual COMPLETE sets
 
 -- See Note [Implementation of COMPLETE pragmas]
 
@@ -195,7 +193,7 @@ also be defined in the module of the pragma) and do not impact recompilation
 checking (#18675).
 
 The pattern-match checker will then initialise each variable's 'VarInfo' with
-*all* imported COMPLETE sets (in 'GHC.HsToCore.PmCheck.Oracle.addCompleteMatches'),
+*all* imported COMPLETE sets (in 'GHC.HsToCore.Pmc.Solver.addCompleteMatches'),
 well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a
 COMPLETE set that is ill-typed for that match variable could never be written by
 the user! And we make sure not to report any ill-typed COMPLETE sets when
@@ -525,9 +523,6 @@ trvVarInfo f nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts = env} } x
     set_vi (a, vi') =
       (a, nabla{ nabla_tm_st = ts{ ts_facts = setEntrySDIE env (vi_id vi') vi' } })
 
-------------------------------------------------
--- * Exported utility functions querying 'Nabla'
-
 {- Note [Coverage checking Newtype matches]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Newtypes have quite peculiar match semantics compared to ordinary DataCons. In a
@@ -556,6 +551,9 @@ Handling of Newtypes is also described in the Appendix of the Lower Your Guards
 where you can find the solution in a perhaps more digestible format.
 -}
 
+------------------------------------------------
+-- * Exported utility functions querying 'Nabla'
+
 lookupRefuts :: Uniquable k => Nabla -> k -> [PmAltCon]
 -- Unfortunately we need the extra bit of polymorphism and the unfortunate
 -- duplication of lookupVarInfo here.
@@ -943,7 +941,7 @@ addCoreCt nabla x e = do
     -- @x ~ y@.
     equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
     equate_with_similar_expr x e = do
-      rep <- StateT $ \nabla -> swap <$> lift (representCoreExpr nabla e)
+      rep <- StateT $ \nabla -> lift (representCoreExpr nabla e)
       -- Note that @rep == x@ if we encountered @e@ for the first time.
       modifyT (\nabla -> addVarCt nabla x rep)
 
@@ -996,14 +994,14 @@ addCoreCt nabla x e = do
 -- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
 -- equivalent to @e'@) we encountered earlier, or a fresh identifier if
 -- there weren't any such constraints.
-representCoreExpr :: Nabla -> CoreExpr -> DsM (Nabla, Id)
+representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
 representCoreExpr nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_reps = reps } } e
-  | Just rep <- lookupCoreMap reps e = pure (nabla, rep)
+  | Just rep <- lookupCoreMap reps e = pure (rep, nabla)
   | otherwise = do
       rep <- mkPmId (exprType e)
       let reps'  = extendCoreMap reps e rep
       let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
-      pure (nabla', rep)
+      pure (rep, nabla')
 
 -- | Like 'modify', but with an effectful modifier action
 modifyT :: Monad m => (s -> m s) -> StateT s m ()
@@ -1159,9 +1157,9 @@ Note [Strict fields and variables of unlifted type]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Binders of unlifted type (and strict fields) are unlifted by construction;
 they are conceived with an implicit @≁⊥@ constraint to begin with. Hence,
-desugaring in "GHC.HsToCore.PmCheck" is entirely unconcerned by strict fields,
+desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned by strict fields,
 since the forcing happens *before* pattern matching.
-And the φ constructor constraints emitted by 'GHC.HsToCore.PmCheck.checkGrd'
+And the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd'
 have complex binding semantics (binding type constraints and unlifted fields),
 so unliftedness semantics are entirely confined to the oracle.
 
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
index a4fad5f4b3..37829b9936 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
@@ -1,43 +1,41 @@
-{-
-Author: George Karachalias <george.karachalias@cs.kuleuven.be>
-        Sebastian Graf <sgraf1337@gmail.com>
--}
-
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ApplicativeDo #-}
 
--- | Types used through-out pattern match checking. This module is mostly there
--- to be imported from "GHC.Tc.Types". The exposed API is that of
--- "GHC.HsToCore.PmCheck.Oracle" and "GHC.HsToCore.PmCheck".
-module GHC.HsToCore.PmCheck.Types (
-        -- * Representations for Literals and AltCons
-        PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
-        isPmAltConMatchStrict, pmAltConImplBangs,
+-- | Domain types used in "GHC.HsToCore.Pmc.Solver".
+-- The ultimate goal is to define 'Nabla', which models normalised refinement
+-- types from the paper
+-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
+module GHC.HsToCore.Pmc.Solver.Types (
 
-        -- ** Equality on 'PmAltCon's
-        PmEquality(..), eqPmAltCon,
+        -- * Normalised refinement types
+        BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
+        Nabla(..), Nablas(..), initNablas,
 
-        -- ** Operations on 'PmLit'
-        literalToPmLit, negatePmLit, overloadPmLit,
-        pmLitAsStringLit, coreExprAsPmLit,
+        -- ** A 'DIdEnv' where entries may be shared
+        Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
+        setIndirectSDIE, setEntrySDIE, traverseSDIE, entriesSDIE,
 
-        -- * Caching residual COMPLETE sets
+        -- ** Caching residual COMPLETE sets
         ConLikeSet, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
 
-        -- * PmAltConSet
+        -- ** Representations for Literals and AltCons
+        PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
+        isPmAltConMatchStrict, pmAltConImplBangs,
+
+        -- *** PmAltConSet
         PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
         extendPmAltConSet, pmAltConSetElems,
 
-        -- * A 'DIdEnv' where entries may be shared
-        Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
-        setIndirectSDIE, setEntrySDIE, traverseSDIE, entriesSDIE,
+        -- *** Equality on 'PmAltCon's
+        PmEquality(..), eqPmAltCon,
+
+        -- *** Operations on 'PmLit'
+        literalToPmLit, negatePmLit, overloadPmLit,
+        pmLitAsStringLit, coreExprAsPmLit
 
-        -- * The pattern match oracle
-        BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
-        Nabla(..), Nablas(..), initNablas, liftNablasM
     ) where
 
 #include "HsVersions.h"
@@ -76,6 +74,284 @@ import Data.Foldable (find)
 import Data.Ratio
 import qualified Data.Semigroup as Semi
 
+--
+-- * Normalised refinement types
+--
+
+-- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
+-- canonical (i.e. mutually compatible) term and type constraints that form the
+-- refinement type's predicate.
+data Nabla
+  = MkNabla
+  { nabla_ty_st :: !TyState
+  -- ^ Type oracle; things like a~Int
+  , nabla_tm_st :: !TmState
+  -- ^ Term oracle; things like x~Nothing
+  }
+
+-- | An initial nabla that is always satisfiable
+initNabla :: Nabla
+initNabla = MkNabla initTyState initTmState
+
+instance Outputable Nabla where
+  ppr nabla = hang (text "Nabla") 2 $ vcat [
+      -- intentionally formatted this way enable the dev to comment in only
+      -- the info she needs
+      ppr (nabla_tm_st nabla),
+      ppr (nabla_ty_st nabla)
+    ]
+
+-- | A disjunctive bag of 'Nabla's, representing a refinement type.
+newtype Nablas = MkNablas (Bag Nabla)
+
+initNablas :: Nablas
+initNablas = MkNablas (unitBag initNabla)
+
+instance Outputable Nablas where
+  ppr (MkNablas nablas) = ppr nablas
+
+instance Semigroup Nablas where
+  MkNablas l <> MkNablas r = MkNablas (l `unionBags` r)
+
+instance Monoid Nablas where
+  mempty = MkNablas emptyBag
+
+-- | The type oracle state. An 'GHC.Tc.Solver.Monad.InertSet' that we
+-- incrementally add local type constraints to, together with a sequence
+-- number that counts the number of times we extended it with new facts.
+data TyState = TySt { ty_st_n :: !Int, ty_st_inert :: !InertSet }
+
+-- | Not user-facing.
+instance Outputable TyState where
+  ppr (TySt n inert) = ppr n <+> ppr inert
+
+initTyState :: TyState
+initTyState = TySt 0 emptyInert
+
+-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
+-- entries are possibly shared when we figure out that two variables must be
+-- equal, thus represent the same set of values.
+--
+-- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
+data TmState
+  = TmSt
+  { ts_facts :: !(SharedDIdEnv VarInfo)
+  -- ^ Facts about term variables. Deterministic env, so that we generate
+  -- deterministic error messages.
+  , ts_reps  :: !(CoreMap Id)
+  -- ^ An environment for looking up whether we already encountered semantically
+  -- equivalent expressions that we want to represent by the same 'Id'
+  -- representative.
+  , ts_dirty :: !DIdSet
+  -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
+  -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
+  }
+
+-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
+-- and negative ('vi_neg') facts, like "x is not (:)".
+-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
+-- ('vi_rcm').
+--
+-- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.Pmc.Solver".
+data VarInfo
+  = VI
+  { vi_id  :: !Id
+  -- ^ The 'Id' in question. Important for adding new constraints relative to
+  -- this 'VarInfo' when we don't easily have the 'Id' available.
+
+  , 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
+  -- pattern matches involving pattern synonym
+  --    case x of { Just y -> case x of PatSyn z -> ... }
+  -- However, no more than one RealDataCon in the list, otherwise contradiction
+  -- because of generativity.
+
+  , vi_neg :: !PmAltConSet
+  -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
+  -- Example, assuming
+  --
+  -- @
+  --     data T = Leaf Int | Branch T T | Node Int T
+  -- @
+  --
+  -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
+  -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
+  -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
+  -- between 'vi_pos' and 'vi_neg'.
+
+  -- See Note [Why record both positive and negative info?]
+  -- It's worth having an actual set rather than a simple association list,
+  -- because files like Cabal's `LicenseId` define relatively huge enums
+  -- that lead to quadratic or worse behavior.
+
+  , vi_bot :: BotInfo
+  -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and
+  --   @x ≁ ⊥@ constraints. E.g.
+  --    * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@.
+  --    * 'IsBot': @x ~ ⊥@
+  --    * 'IsNotBot': @x ≁ ⊥@
+
+  , vi_rcm :: !ResidualCompleteMatches
+  -- ^ A cache of the associated COMPLETE sets. At any time a superset of
+  -- possible constructors of each COMPLETE set. So, if it's not in here, we
+  -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
+  -- to recognise completion of a COMPLETE set efficiently for large enums.
+  }
+
+data PmAltConApp
+  = PACA
+  { paca_con :: !PmAltCon
+  , paca_tvs :: ![TyVar]
+  , paca_ids :: ![Id]
+  }
+
+-- | See 'vi_bot'.
+data BotInfo
+  = IsBot
+  | IsNotBot
+  | MaybeBot
+  deriving Eq
+
+instance Outputable PmAltConApp where
+  ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
+    hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
+
+instance Outputable BotInfo where
+  ppr MaybeBot = underscore
+  ppr IsBot    = text "~⊥"
+  ppr IsNotBot = text "≁⊥"
+
+-- | Not user-facing.
+instance Outputable TmState where
+  ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
+
+-- | Not user-facing.
+instance Outputable VarInfo where
+  ppr (VI x 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_pos
+        | [] <- pos  = underscore
+        | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
+        | otherwise  = char '~' <> ppr pos
+      pp_neg
+        | isEmptyPmAltConSet neg = underscore
+        | otherwise              = char '≁' <> ppr neg
+      pp_cache
+        | RCM Nothing Nothing <- cache = underscore
+        | otherwise                    = ppr cache
+
+-- | Initial state of the term oracle.
+initTmState :: TmState
+initTmState = TmSt emptySDIE emptyCoreMap emptyDVarSet
+
+-- ** A 'DIdEnv' where entries may be shared
+
+-- | Either @Indirect x@, meaning the value is represented by that of @x@, or
+-- an @Entry@ containing containing the actual value it represents.
+data Shared a
+  = Indirect !Id
+  | Entry !a
+
+-- | A 'DIdEnv' in which entries can be shared by multiple 'Id's.
+-- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry
+-- of an Id with 'setEntrySDIE'.
+newtype SharedDIdEnv a
+  = SDIE { unSDIE :: DIdEnv (Shared a) }
+
+emptySDIE :: SharedDIdEnv a
+emptySDIE = SDIE emptyDVarEnv
+
+lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a)
+lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of
+  Nothing           -> (x, Nothing)
+  Just (Indirect y) -> lookupReprAndEntrySDIE sdie y
+  Just (Entry a)    -> (x, Just a)
+
+-- | @lookupSDIE env x@ looks up an entry for @x@, looking through all
+-- 'Indirect's until it finds a shared 'Entry'.
+lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a
+lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x)
+
+-- | Check if two variables are part of the same equivalence class.
+sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool
+sameRepresentativeSDIE sdie x y =
+  fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y)
+
+-- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby
+-- merging @x@'s equivalence class into @y@'s. This will discard all info on
+-- @x@!
+setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
+setIndirectSDIE sdie@(SDIE env) x y =
+  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y)
+
+-- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@,
+-- thereby modifying its whole equivalence class.
+setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
+setEntrySDIE sdie@(SDIE env) x a =
+  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a)
+
+entriesSDIE :: SharedDIdEnv a -> [a]
+entriesSDIE (SDIE env) = mapMaybe preview_entry (eltsUDFM env)
+  where
+    preview_entry (Entry e) = Just e
+    preview_entry _         = Nothing
+
+traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
+traverseSDIE f = fmap (SDIE . listToUDFM_Directly) . traverse g . udfmToList . unSDIE
+  where
+    g :: (Unique, Shared a) -> f (Unique, Shared b)
+    g (u, Indirect y) = pure (u,Indirect y)
+    g (u, Entry a)    = do
+        a' <- f a
+        pure (u,Entry a')
+
+instance Outputable a => Outputable (Shared a) where
+  ppr (Indirect x) = ppr x
+  ppr (Entry a)    = ppr a
+
+instance Outputable a => Outputable (SharedDIdEnv a) where
+  ppr (SDIE env) = ppr env
+
+-- | A data type that caches for the 'VarInfo' of @x@ the results of querying
+-- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
+-- which we already know @x ≁ K@ from these sets.
+--
+-- For motivation, see Section 5.3 in Lower Your Guards.
+-- See also Note [Implementation of COMPLETE pragmas]
+data ResidualCompleteMatches
+  = RCM
+  { rcm_vanilla :: !(Maybe ConLikeSet)
+  -- ^ The residual set for the vanilla COMPLETE set from the data defn.
+  -- Tracked separately from 'rcm_pragmas', because it might only be
+  -- known much later (when we have enough type information to see the 'TyCon'
+  -- of the match), or not at all even. Until that happens, it is 'Nothing'.
+  , rcm_pragmas :: !(Maybe [ConLikeSet])
+  -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
+  -- visible when compiling this module. Querying that set with
+  -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
+  -- until first needed in a 'DsM' context.
+  }
+
+getRcm :: ResidualCompleteMatches -> [ConLikeSet]
+getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
+
+isRcmInitialised :: ResidualCompleteMatches -> Bool
+isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
+
+instance Outputable ResidualCompleteMatches where
+  -- formats as "[{Nothing,Just},{P,Q}]"
+  ppr rcm = ppr (getRcm rcm)
+
+--------------------------------------------------------------------------------
+-- The rest is just providing an IR for (overloaded!) literals and AltCons that
+-- sits between Hs and Core. We need a reliable way to detect and determine
+-- equality between them, which is impossible with Hs (too expressive) and with
+-- Core (no notion of overloaded literals, and even plain 'Int' literals are
+-- actually constructor apps). Also String literals are troublesome.
+
 -- | Literals (simple and overloaded ones) for pattern match checking.
 --
 -- See Note [Undecidable Equality for PmAltCons]
@@ -230,7 +506,7 @@ pmAltConType (PmAltConLike con) arg_tys  = conLikeResTy con arg_tys
 -- | Is a match on this constructor forcing the match variable?
 -- True of data constructors, literals and pattern synonyms (#17357), but not of
 -- newtypes.
--- See Note [Coverage checking Newtype matches] in "GHC.HsToCore.PmCheck.Oracle".
+-- See Note [Coverage checking Newtype matches] in "GHC.HsToCore.Pmc.Solver".
 isPmAltConMatchStrict :: PmAltCon -> Bool
 isPmAltConMatchStrict PmAltLit{}                      = True
 isPmAltConMatchStrict (PmAltConLike PatSynCon{})      = True -- #17357
@@ -288,7 +564,7 @@ The impact of this treatment of overloaded literals is the following:
   * We have instant equality check for overloaded literals (we do not rely on
     the term oracle which is rather expensive, both in terms of performance and
     memory). This significantly improves the performance of functions `covered`
-    `uncovered` and `divergent` in "GHC.HsToCore.PmCheck" and effectively addresses
+    `uncovered` and `divergent` in "GHC.HsToCore.Pmc" and effectively addresses
     #11161.
 
   * The warnings issued are simpler.
@@ -347,23 +623,22 @@ coreExprAsPmLit e = case collectArgs e of
     --       overloaded lits anyway, so we immediately override type information
     -> literalToPmLit (exprType e) (mkLitDouble (litValue n % litValue d))
   (Var x, args)
-    -- Take care of -XRebindableSyntax. The last argument should be the (only)
-    -- integer literal, otherwise we can't really do much about it.
-    | [Lit l] <- dropWhile (not . is_lit) args
-    , is_rebound_name x fromIntegerName
+    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
+    | is_rebound_name x fromIntegerName
+    , [Lit l] <- dropWhile (not . is_lit) args
     -> literalToPmLit (literalType l) l >>= overloadPmLit (exprType e)
   (Var x, args)
-    -- Similar to fromInteger case
-    | [r] <- dropWhile (not . is_ratio) args
-    , is_rebound_name x fromRationalName
+    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
+    | is_rebound_name x fromRationalName
+    , [r] <- dropWhile (not . is_ratio) args
     -> coreExprAsPmLit r >>= overloadPmLit (exprType e)
   (Var x, args)
     | is_rebound_name x fromStringName
-    -- With -XRebindableSyntax or without: The first String argument is what we are after
+    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
     , s:_ <- filter (eqType stringTy . exprType) args
     -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
     -> coreExprAsPmLit s >>= overloadPmLit (exprType e)
-  -- These last two cases handle String literals
+  -- These last two cases handle proper String literals
   (Var x, [Type ty])
     | Just dc <- isDataConWorkId_maybe x
     , dc == nilDataCon
@@ -383,11 +658,25 @@ coreExprAsPmLit e = case collectArgs e of
       | otherwise
       = False
 
-    -- | Compares the given Id to the Name based on OccName, to detect
-    -- -XRebindableSyntax.
+    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
     is_rebound_name :: Id -> Name -> Bool
     is_rebound_name x n = getOccFS (idName x) == getOccFS n
 
+{- Note [Detecting overloaded literals with -XRebindableSyntax]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Normally, we'd find e.g. overloaded string literals by comparing the
+application head of an expression to `fromStringName`. But that doesn't work
+with -XRebindableSyntax: The `Name` of a user-provided `fromString` function is
+different to `fromStringName`, which lives in a certain module, etc.
+
+There really is no other way than to compare `OccName`s and guess which
+argument is the actual literal string (we assume it's the first argument of
+type `String`).
+
+The same applies to other overloaded literals, such as overloaded rationals
+(`fromRational`)and overloaded integer literals (`fromInteger`).
+-}
+
 instance Outputable PmLitValue where
   ppr (PmLitInt i)        = ppr i
   ppr (PmLitRat r)        = ppr (double (fromRat r)) -- good enough
@@ -420,271 +709,3 @@ instance Outputable PmAltCon where
 
 instance Outputable PmEquality where
   ppr = text . show
-
--- | A data type that caches for the 'VarInfo' of @x@ the results of querying
--- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
--- which we already know @x ≁ K@ from these sets.
---
--- For motivation, see Section 5.3 in Lower Your Guards.
--- See also Note [Implementation of COMPLETE pragmas]
-data ResidualCompleteMatches
-  = RCM
-  { rcm_vanilla :: !(Maybe ConLikeSet)
-  -- ^ The residual set for the vanilla COMPLETE set from the data defn.
-  -- Tracked separately from 'rcm_pragmas', because it might only be
-  -- known much later (when we have enough type information to see the 'TyCon'
-  -- of the match), or not at all even. Until that happens, it is 'Nothing'.
-  , rcm_pragmas :: !(Maybe [ConLikeSet])
-  -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
-  -- visible when compiling this module. Querying that set with
-  -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
-  -- until first needed in a 'DsM' context.
-  }
-
-getRcm :: ResidualCompleteMatches -> [ConLikeSet]
-getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
-
-isRcmInitialised :: ResidualCompleteMatches -> Bool
-isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
-
-instance Outputable ResidualCompleteMatches where
-  -- formats as "[{Nothing,Just},{P,Q}]"
-  ppr rcm = ppr (getRcm rcm)
-
--- | Either @Indirect x@, meaning the value is represented by that of @x@, or
--- an @Entry@ containing containing the actual value it represents.
-data Shared a
-  = Indirect Id
-  | Entry a
-
--- | A 'DIdEnv' in which entries can be shared by multiple 'Id's.
--- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry
--- of an Id with 'setEntrySDIE'.
-newtype SharedDIdEnv a
-  = SDIE { unSDIE :: DIdEnv (Shared a) }
-
-emptySDIE :: SharedDIdEnv a
-emptySDIE = SDIE emptyDVarEnv
-
-lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a)
-lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of
-  Nothing           -> (x, Nothing)
-  Just (Indirect y) -> lookupReprAndEntrySDIE sdie y
-  Just (Entry a)    -> (x, Just a)
-
--- | @lookupSDIE env x@ looks up an entry for @x@, looking through all
--- 'Indirect's until it finds a shared 'Entry'.
-lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a
-lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x)
-
--- | Check if two variables are part of the same equivalence class.
-sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool
-sameRepresentativeSDIE sdie x y =
-  fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y)
-
--- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby
--- merging @x@'s equivalence class into @y@'s. This will discard all info on
--- @x@!
-setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
-setIndirectSDIE sdie@(SDIE env) x y =
-  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y)
-
--- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@,
--- thereby modifying its whole equivalence class.
-setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
-setEntrySDIE sdie@(SDIE env) x a =
-  SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a)
-
-entriesSDIE :: SharedDIdEnv a -> [a]
-entriesSDIE (SDIE env) = mapMaybe preview_entry (eltsUDFM env)
-  where
-    preview_entry (Entry e) = Just e
-    preview_entry _         = Nothing
-
-traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
-traverseSDIE f = fmap (SDIE . listToUDFM_Directly) . traverse g . udfmToList . unSDIE
-  where
-    g :: (Unique, Shared a) -> f (Unique, Shared b)
-    g (u, Indirect y) = pure (u,Indirect y)
-    g (u, Entry a)    = do
-        a' <- f a
-        pure (u,Entry a')
-
-instance Outputable a => Outputable (Shared a) where
-  ppr (Indirect x) = ppr x
-  ppr (Entry a)    = ppr a
-
-instance Outputable a => Outputable (SharedDIdEnv a) where
-  ppr (SDIE env) = ppr env
-
--- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
--- entries are possibly shared when we figure out that two variables must be
--- equal, thus represent the same set of values.
---
--- See Note [TmState invariants] in "GHC.HsToCore.PmCheck.Oracle".
-data TmState
-  = TmSt
-  { ts_facts :: !(SharedDIdEnv VarInfo)
-  -- ^ Facts about term variables. Deterministic env, so that we generate
-  -- deterministic error messages.
-  , ts_reps  :: !(CoreMap Id)
-  -- ^ An environment for looking up whether we already encountered semantically
-  -- equivalent expressions that we want to represent by the same 'Id'
-  -- representative.
-  , ts_dirty :: !DIdSet
-  -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
-  -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
-  }
-
--- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
--- and negative ('vi_neg') facts, like "x is not (:)".
--- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
--- ('vi_rcm').
---
--- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.PmCheck.Oracle".
-data VarInfo
-  = VI
-  { vi_id  :: !Id
-  -- ^ The 'Id' in question. Important for adding new constraints relative to
-  -- this 'VarInfo' when we don't easily have the 'Id' available.
-
-  , 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
-  -- pattern matches involving pattern synonym
-  --    case x of { Just y -> case x of PatSyn z -> ... }
-  -- However, no more than one RealDataCon in the list, otherwise contradiction
-  -- because of generativity.
-
-  , vi_neg :: !PmAltConSet
-  -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
-  -- Example, assuming
-  --
-  -- @
-  --     data T = Leaf Int | Branch T T | Node Int T
-  -- @
-  --
-  -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
-  -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
-  -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
-  -- between 'vi_pos' and 'vi_neg'.
-
-  -- See Note [Why record both positive and negative info?]
-  -- It's worth having an actual set rather than a simple association list,
-  -- because files like Cabal's `LicenseId` define relatively huge enums
-  -- that lead to quadratic or worse behavior.
-
-  , vi_bot :: BotInfo
-  -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and
-  --   @x ≁ ⊥@ constraints. E.g.
-  --    * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@.
-  --    * 'IsBot': @x ~ ⊥@
-  --    * 'IsNotBot': @x ≁ ⊥@
-
-  , vi_rcm :: !ResidualCompleteMatches
-  -- ^ A cache of the associated COMPLETE sets. At any time a superset of
-  -- possible constructors of each COMPLETE set. So, if it's not in here, we
-  -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
-  -- to recognise completion of a COMPLETE set efficiently for large enums.
-  }
-
-data PmAltConApp
-  = PACA
-  { paca_con :: !PmAltCon
-  , paca_tvs :: ![TyVar]
-  , paca_ids :: ![Id]
-  }
-
--- | See 'vi_bot'.
-data BotInfo
-  = IsBot
-  | IsNotBot
-  | MaybeBot
-  deriving Eq
-
-instance Outputable PmAltConApp where
-  ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
-    hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
-
-instance Outputable BotInfo where
-  ppr MaybeBot = underscore
-  ppr IsBot    = text "~⊥"
-  ppr IsNotBot = text "≁⊥"
-
--- | Not user-facing.
-instance Outputable TmState where
-  ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
-
--- | Not user-facing.
-instance Outputable VarInfo where
-  ppr (VI x 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_pos
-        | [] <- pos  = underscore
-        | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
-        | otherwise  = char '~' <> ppr pos
-      pp_neg
-        | isEmptyPmAltConSet neg = underscore
-        | otherwise              = char '≁' <> ppr neg
-      pp_cache
-        | RCM Nothing Nothing <- cache = underscore
-        | otherwise                    = ppr cache
-
--- | Initial state of the term oracle.
-initTmState :: TmState
-initTmState = TmSt emptySDIE emptyCoreMap emptyDVarSet
-
--- | The type oracle state. An 'GHC.Tc.Solver.Monad.InsertSet' that we
--- incrementally add local type constraints to, together with a sequence
--- number that counts the number of times we extended it with new facts.
-data TyState = TySt { ty_st_n :: !Int, ty_st_inert :: !InertSet }
-
--- | Not user-facing.
-instance Outputable TyState where
-  ppr (TySt n inert) = ppr n <+> ppr inert
-
-initTyState :: TyState
-initTyState = TySt 0 emptyInert
-
--- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
--- canonical (i.e. mutually compatible) term and type constraints that form the
--- refinement type's predicate.
-data Nabla
-  = MkNabla
-  { nabla_ty_st :: !TyState
-  -- ^ Type oracle; things like a~Int
-  , nabla_tm_st :: !TmState
-  -- ^ Term oracle; things like x~Nothing
-  }
-
--- | An initial nabla that is always satisfiable
-initNabla :: Nabla
-initNabla = MkNabla initTyState initTmState
-
-instance Outputable Nabla where
-  ppr nabla = hang (text "Nabla") 2 $ vcat [
-      -- intentionally formatted this way enable the dev to comment in only
-      -- the info she needs
-      ppr (nabla_tm_st nabla),
-      ppr (nabla_ty_st nabla)
-    ]
-
--- | A disjunctive bag of 'Nabla's, representing a refinement type.
-newtype Nablas = MkNablas (Bag Nabla)
-
-initNablas :: Nablas
-initNablas = MkNablas (unitBag initNabla)
-
-instance Outputable Nablas where
-  ppr (MkNablas nablas) = ppr nablas
-
-instance Semigroup Nablas where
-  MkNablas l <> MkNablas r = MkNablas (l `unionBags` r)
-
-instance Monoid Nablas where
-  mempty = MkNablas emptyBag
-
-liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
-liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
diff --git a/compiler/GHC/HsToCore/Pmc/Types.hs b/compiler/GHC/HsToCore/Pmc/Types.hs
new file mode 100644
index 0000000000..793485ae39
--- /dev/null
+++ b/compiler/GHC/HsToCore/Pmc/Types.hs
@@ -0,0 +1,231 @@
+{-
+Author: George Karachalias <george.karachalias@cs.kuleuven.be>
+        Sebastian Graf <sgraf1337@gmail.com>
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+-- | Types used through-out pattern match checking. This module is mostly there
+-- to be imported from "GHC.HsToCore.Types". The exposed API is that of
+-- "GHC.HsToCore.Pmc".
+--
+-- These types model the paper
+-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
+module GHC.HsToCore.Pmc.Types (
+        -- * LYG syntax
+
+        -- ** Guard language
+        SrcInfo(..), PmGrd(..), GrdVec(..),
+
+        -- ** Guard tree language
+        PmMatchGroup(..), PmMatch(..), PmGRHS(..), PmPatBind(..), PmEmptyCase(..),
+
+        -- * Coverage Checking types
+        RedSets (..), Precision (..), CheckResult (..),
+
+        -- * Pre and post coverage checking synonyms
+        Pre, Post,
+
+        -- * Normalised refinement types
+        module GHC.HsToCore.Pmc.Solver.Types
+
+    ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.HsToCore.Pmc.Solver.Types
+
+import GHC.Data.OrdList
+import GHC.Types.Id
+import GHC.Types.Var (EvVar)
+import GHC.Types.SrcLoc
+import GHC.Utils.Outputable
+import GHC.Core.Type
+import GHC.Core
+
+import Data.List.NonEmpty ( NonEmpty(..) )
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Semigroup as Semi
+
+--
+-- * Guard language
+--
+
+-- | A very simple language for pattern guards. Let bindings, bang patterns,
+-- and matching variables against flat constructor patterns.
+-- The LYG guard language.
+data PmGrd
+  = -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
+    -- The @args@ are bound in this construct, the @x@ is just a use.
+    -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
+    PmCon {
+      pm_id          :: !Id,
+      pm_con_con     :: !PmAltCon,
+      pm_con_tvs     :: ![TyVar],
+      pm_con_dicts   :: ![EvVar],
+      pm_con_args    :: ![Id]
+    }
+
+    -- | @PmBang x@ corresponds to a @seq x True@ guard.
+    -- If the extra 'SrcInfo' is present, the bang guard came from a source
+    -- bang pattern, in which case we might want to report it as redundant.
+    -- See Note [Dead bang patterns] in GHC.HsToCore.Pmc.Check.
+  | PmBang {
+      pm_id   :: !Id,
+      _pm_loc :: !(Maybe SrcInfo)
+    }
+
+    -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
+    -- /binds/ @x@.
+  | PmLet {
+      pm_id        :: !Id,
+      _pm_let_expr :: !CoreExpr
+    }
+
+-- | Should not be user-facing.
+instance Outputable PmGrd where
+  ppr (PmCon x alt _tvs _con_dicts con_args)
+    = hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
+  ppr (PmBang x _loc) = char '!' <> ppr x
+  ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
+
+--
+-- * Guard tree language
+--
+
+-- | Means by which we identify a source construct for later pretty-printing in
+-- a warning message. 'SDoc' for the equation to show, 'Located' for the
+-- location.
+newtype SrcInfo = SrcInfo (Located SDoc)
+
+-- | A sequence of 'PmGrd's.
+newtype GrdVec = GrdVec [PmGrd]
+
+-- | A guard tree denoting 'MatchGroup'.
+newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
+
+-- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
+-- GRHS.
+data PmMatch p = PmMatch { pm_pats :: !p, pm_grhss :: !(NonEmpty (PmGRHS p)) }
+
+-- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
+-- useful for printing out in warnings messages.
+data PmGRHS p = PmGRHS { pg_grds :: !p, pg_rhs :: !SrcInfo }
+
+-- | A guard tree denoting an -XEmptyCase.
+newtype PmEmptyCase = PmEmptyCase { pe_var :: Id }
+
+-- | A guard tree denoting a pattern binding.
+newtype PmPatBind p =
+  -- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
+  -- rather than on the pattern bindings.
+  PmPatBind (PmGRHS p)
+
+instance Outputable SrcInfo where
+  ppr (SrcInfo (L (RealSrcSpan rss _) _)) = ppr (srcSpanStartLine rss)
+  ppr (SrcInfo (L s                   _)) = ppr s
+
+-- | Format LYG guards as @| True <- x, let x = 42, !z@
+instance Outputable GrdVec where
+  ppr (GrdVec [])     = empty
+  ppr (GrdVec (g:gs)) = fsep (char '|' <+> ppr g : map ((comma <+>) . ppr) gs)
+
+-- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
+-- @{ <first alt>; ...; <last alt> }@
+pprLygSequence :: Outputable a => NonEmpty a -> SDoc
+pprLygSequence (NE.toList -> as) =
+  braces (space <> fsep (punctuate semi (map ppr as)) <> space)
+
+instance Outputable p => Outputable (PmMatchGroup p) where
+  ppr (PmMatchGroup matches) = pprLygSequence matches
+
+instance Outputable p => Outputable (PmMatch p) where
+  ppr (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
+    ppr grds <+> ppr grhss
+
+instance Outputable p => Outputable (PmGRHS p) where
+  ppr (PmGRHS { pg_grds = grds, pg_rhs = rhs }) =
+    ppr grds <+> text "->" <+> ppr rhs
+
+instance Outputable p => Outputable (PmPatBind p) where
+  ppr (PmPatBind PmGRHS { pg_grds = grds, pg_rhs = bind }) =
+    ppr bind <+> ppr grds <+> text "=" <+> text "..."
+
+instance Outputable PmEmptyCase where
+  ppr (PmEmptyCase { pe_var = var }) =
+    text "<empty case on " <> ppr var <> text ">"
+
+data Precision = Approximate | Precise
+  deriving (Eq, Show)
+
+instance Outputable Precision where
+  ppr = text . show
+
+instance Semi.Semigroup Precision where
+  Precise <> Precise = Precise
+  _       <> _       = Approximate
+
+instance Monoid Precision where
+  mempty = Precise
+  mappend = (Semi.<>)
+
+-- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
+-- (later digested into a 'CIRB').
+data RedSets
+  = RedSets
+  { rs_cov :: !Nablas
+  -- ^ The /Covered/ set; the set of values reaching a particular program
+  -- point.
+  , rs_div :: !Nablas
+  -- ^ The /Diverging/ set; empty if no match can lead to divergence.
+  --   If it wasn't empty, we have to turn redundancy warnings into
+  --   inaccessibility warnings for any subclauses.
+  , rs_bangs :: !(OrdList (Nablas, SrcInfo))
+  -- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points
+  -- a bang pattern in source that is redundant. See Note [Dead bang patterns].
+  }
+
+instance Outputable RedSets where
+  ppr RedSets { rs_cov = _cov, rs_div = _div, rs_bangs = _bangs }
+    -- It's useful to change this definition for different verbosity levels in
+    -- printf-debugging
+    = empty
+
+-- | Pattern-match coverage check result
+data CheckResult a
+  = CheckResult
+  { cr_ret :: !a
+  -- ^ A hole for redundancy info and covered sets.
+  , cr_uncov   :: !Nablas
+  -- ^ The set of uncovered values falling out at the bottom.
+  --   (for -Wincomplete-patterns, but also important state for the algorithm)
+  , cr_approx  :: !Precision
+  -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
+  -- purpose of suggesting to crank it up in the warning message. Writer state.
+  } deriving Functor
+
+instance Outputable a => Outputable (CheckResult a) where
+  ppr (CheckResult c unc pc)
+    = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
+        [ field "ret" c <> comma
+        , field "uncov" unc])
+    where
+      ppr_precision Precise     = empty
+      ppr_precision Approximate = text "(Approximate)"
+      field name value = text name <+> equals <+> ppr value
+
+--
+-- * Pre and post coverage checking synonyms
+--
+
+-- | Used as tree payload pre-checking. The LYG guards to check.
+type Pre = GrdVec
+
+-- | Used as tree payload post-checking. The redundancy info we elaborated.
+type Post = RedSets
diff --git a/compiler/GHC/HsToCore/Pmc/Utils.hs b/compiler/GHC/HsToCore/Pmc/Utils.hs
new file mode 100644
index 0000000000..d4646bd6e8
--- /dev/null
+++ b/compiler/GHC/HsToCore/Pmc/Utils.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns,
+             MultiWayIf, ScopedTypeVariables, MagicHash #-}
+
+-- | Utility module for the pattern-match coverage checker.
+module GHC.HsToCore.Pmc.Utils (
+
+        tracePm, mkPmId,
+        allPmCheckWarnings, overlapping, exhaustive, redundantBang,
+        exhaustiveWarningFlag,
+        isMatchContextPmChecked, needToRunPmCheck
+
+    ) where
+
+#include "HsVersions.h"
+
+import GHC.Prelude
+
+import GHC.Types.Basic (Origin(..), isGenerated)
+import GHC.Driver.Session
+import GHC.Hs
+import GHC.Core.Type
+import GHC.Data.FastString
+import GHC.Data.IOEnv
+import GHC.Types.Id
+import GHC.Types.Name
+import GHC.Types.Unique.Supply
+import GHC.Types.SrcLoc
+import GHC.Utils.Error
+import GHC.Utils.Misc
+import GHC.Utils.Outputable
+import GHC.HsToCore.Monad
+
+tracePm :: String -> SDoc -> DsM ()
+tracePm herald doc = do
+  dflags <- getDynFlags
+  printer <- mkPrintUnqualifiedDs
+  liftIO $ dumpIfSet_dyn_printer printer dflags
+            Opt_D_dump_ec_trace "" FormatText (text herald $$ (nest 2 doc))
+{-# INLINE tracePm #-}  -- see Note [INLINE conditional tracing utilities]
+
+-- | Generate a fresh `Id` of a given type
+mkPmId :: Type -> DsM Id
+mkPmId ty = getUniqueM >>= \unique ->
+  let occname = mkVarOccFS $ fsLit "pm"
+      name    = mkInternalName unique occname noSrcSpan
+  in  return (mkLocalIdOrCoVar name Many ty)
+
+-- | All warning flags that need to run the pattern match checker.
+allPmCheckWarnings :: [WarningFlag]
+allPmCheckWarnings =
+  [ Opt_WarnIncompletePatterns
+  , Opt_WarnIncompleteUniPatterns
+  , Opt_WarnIncompletePatternsRecUpd
+  , Opt_WarnOverlappingPatterns
+  ]
+
+-- | Check whether the redundancy checker should run (redundancy only)
+overlapping :: DynFlags -> HsMatchContext id -> Bool
+-- See Note [Inaccessible warnings for record updates]
+overlapping _      RecUpd = False
+overlapping dflags _      = wopt Opt_WarnOverlappingPatterns dflags
+
+-- | Check whether the exhaustiveness checker should run (exhaustiveness only)
+exhaustive :: DynFlags -> HsMatchContext id -> Bool
+exhaustive  dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
+
+-- | Check whether unnecessary bangs should be warned about
+redundantBang :: DynFlags -> Bool
+redundantBang dflags = wopt Opt_WarnRedundantBangPatterns dflags
+
+-- | Denotes whether an exhaustiveness check is supported, and if so,
+-- via which 'WarningFlag' it's controlled.
+-- Returns 'Nothing' if check is not supported.
+exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
+exhaustiveWarningFlag (FunRhs {})   = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag CaseAlt       = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag IfAlt         = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag LambdaExpr    = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag PatBindRhs    = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
+exhaustiveWarningFlag ProcExpr      = Just Opt_WarnIncompleteUniPatterns
+exhaustiveWarningFlag RecUpd        = Just Opt_WarnIncompletePatternsRecUpd
+exhaustiveWarningFlag ThPatSplice   = Nothing
+exhaustiveWarningFlag PatSyn        = Nothing
+exhaustiveWarningFlag ThPatQuote    = Nothing
+-- Don't warn about incomplete patterns in list comprehensions, pattern guards
+-- etc. They are often *supposed* to be incomplete
+exhaustiveWarningFlag (StmtCtxt {}) = Nothing
+
+-- | Check whether any part of pattern match checking is enabled for this
+-- 'HsMatchContext' (does not matter whether it is the redundancy check or the
+-- exhaustiveness check).
+isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
+isMatchContextPmChecked dflags origin kind
+  | isGenerated origin
+  = False
+  | otherwise
+  = overlapping dflags kind || exhaustive dflags kind
+
+-- | Return True when any of the pattern match warnings ('allPmCheckWarnings')
+-- are enabled, in which case we need to run the pattern match checker.
+needToRunPmCheck :: DynFlags -> Origin -> Bool
+needToRunPmCheck dflags origin
+  | isGenerated origin
+  = False
+  | otherwise
+  = notNull (filter (`wopt` dflags) allPmCheckWarnings)
+
+{- Note [Inaccessible warnings for record updates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#12957)
+  data T a where
+    T1 :: { x :: Int } -> T Bool
+    T2 :: { x :: Int } -> T a
+    T3 :: T a
+
+  f :: T Char -> T a
+  f r = r { x = 3 }
+
+The desugarer will conservatively generate a case for T1 even though
+it's impossible:
+  f r = case r of
+          T1 x -> T1 3   -- Inaccessible branch
+          T2 x -> T2 3
+          _    -> error "Missing"
+
+We don't want to warn about the inaccessible branch because the programmer
+didn't put it there!  So we filter out the warning here.
+
+The same can happen for long distance term constraints instead of type
+constraints (#17783):
+
+  data T = A { x :: Int } | B { x :: Int }
+  f r@A{} = r { x = 3 }
+  f _     = B 0
+
+Here, the long distance info from the FunRhs match (@r ~ A x@) will make the
+clause matching on @B@ of the desugaring to @case@ redundant. It's generated
+code that we don't want to warn about.
+-}
diff --git a/compiler/GHC/HsToCore/Types.hs b/compiler/GHC/HsToCore/Types.hs
index d6fd94e723..64fe4498a0 100644
--- a/compiler/GHC/HsToCore/Types.hs
+++ b/compiler/GHC/HsToCore/Types.hs
@@ -14,7 +14,7 @@ import GHC.Types.SrcLoc
 import GHC.Types.Var
 import GHC.Hs (LForeignDecl, HsExpr, GhcTc)
 import GHC.Tc.Types (TcRnIf, IfGblEnv, IfLclEnv, CompleteMatches)
-import GHC.HsToCore.PmCheck.Types (Nablas)
+import GHC.HsToCore.Pmc.Types (Nablas)
 import GHC.Core (CoreExpr)
 import GHC.Core.FamInstEnv
 import GHC.Utils.Error
@@ -61,7 +61,7 @@ data DsLclEnv
   { dsl_meta    :: DsMetaEnv   -- ^ Template Haskell bindings
   , dsl_loc     :: RealSrcSpan -- ^ To put in pattern-matching error msgs
   , dsl_nablas  :: Nablas
-  -- ^ See Note [Note [Long-distance information] in "GHC.HsToCore.PmCheck".
+  -- ^ See Note [Note [Long-distance information] in "GHC.HsToCore.Pmc".
   -- The set of reaching values Nablas is augmented as we walk inwards, refined
   -- through each pattern match in turn
   }
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 2aa1189bcf..70af1b1255 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -820,7 +820,7 @@ It does *not* reduce type or data family applications or look through newtypes.
 Why is this useful? As one example, when coverage-checking an EmptyCase
 expression, it's possible that the type of the scrutinee will only reduce
 if some local equalities are solved for. See "Wrinkle: Local equalities"
-in Note [Type normalisation] in "GHC.HsToCore.PmCheck".
+in Note [Type normalisation] in "GHC.HsToCore.Pmc".
 
 To accomplish its stated goal, tcNormalise first initialises the solver monad
 with the given InertCans, then uses flattenType to simplify the desired type
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 9665b5e4e2..918c6f7629 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -307,10 +307,14 @@ Library
         GHC.Core.Stats
         GHC.Core.Make
         GHC.Core.Ppr
-        GHC.HsToCore.PmCheck.Oracle
-        GHC.HsToCore.PmCheck.Ppr
-        GHC.HsToCore.PmCheck.Types
-        GHC.HsToCore.PmCheck
+        GHC.HsToCore.Pmc
+        GHC.HsToCore.Pmc.Types
+        GHC.HsToCore.Pmc.Utils
+        GHC.HsToCore.Pmc.Desugar
+        GHC.HsToCore.Pmc.Check
+        GHC.HsToCore.Pmc.Solver.Types
+        GHC.HsToCore.Pmc.Solver
+        GHC.HsToCore.Pmc.Ppr
         GHC.HsToCore.Coverage
         GHC.HsToCore
         GHC.HsToCore.Types