path: root/compiler/GHC/HsToCore/PmCheck.hs

{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>

Pattern Matching Coverage Checking.
-}

{-# LANGUAGE CPP            #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE TupleSections  #-}
{-# LANGUAGE ViewPatterns   #-}
{-# LANGUAGE MultiWayIf     #-}
{-# LANGUAGE LambdaCase     #-}
{-# LANGUAGE NamedFieldPuns #-}

module GHC.HsToCore.PmCheck (
        -- Checking and printing
        covCheckPatBind, covCheckMatchGroup, covCheckGRHSs,
        isMatchContextPmChecked,

        -- See Note [Type and Term Equality Propagation]
        addTyCsDs, 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.Tc.Instance.Family
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.Core.TyCon
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)

import Control.Monad (when, forM_, zipWithM)
import Data.List (elemIndex)
import qualified Data.Semigroup as Semi
import Data.List.NonEmpty (NonEmpty(..))

{-
This module checks pattern matches for:
\begin{enumerate}
  \item Equations that are redundant
  \item Equations with inaccessible right-hand-side
  \item Exhaustiveness
\end{enumerate}

The algorithm is based on the paper:

  "GADTs Meet Their Match:
     Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"

    https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/gadtpm-acm.pdf

%************************************************************************
%*                                                                      *
                     Pattern Match Check Types
%*                                                                      *
%************************************************************************
-}

-- | 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.<>)

-- | Means by which we identify source location for later pretty-printing
--  in a warning message. 'SDoc' for the equation to show, 'Located' for
-- the location.
type SrcInfo = Located SDoc

-- | A representation of the desugaring to 'PmGrd's of all clauses of a
-- function definition/pattern match/etc.
data GrdTree
  = Rhs !SrcInfo
  | Guard !PmGrd !GrdTree
  -- ^ @Guard grd t@ will try to match @grd@ and on success continue to match
  -- @t@. Falls through if either match fails. Models left-to-right semantics
  -- of pattern matching.
  | Sequence ![GrdTree]
  -- ^ @Sequence (t:ts)@ matches against @t@, and then matches all
  -- fallen-through values against @Sequence ts@. Models top-to-bottom semantics
  -- of pattern matching.
  -- @Sequence []@ always fails; it is useful for Note [Checking EmptyCase].

{- 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 'checkGrdTree'. 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.
-}

-- | The digest of 'checkGrdTree', representing the annotated pattern-match
-- tree. 'extractRedundancyInfo' can figure out redundant and proper
-- inaccessible RHSs from this, as well as dead bangs.
data AnnotatedTree
  = AccessibleRhs !Deltas !SrcInfo
  -- ^ A RHS deemed accessible. The 'Deltas' is the (non-empty) set of covered
  -- values.
  | InaccessibleRhs !SrcInfo
  -- ^ A RHS deemed inaccessible; it covers no value.
  | MayDiverge !AnnotatedTree
  -- ^ Asserts that the tree may force diverging values, so not all of its
  -- clauses can be redundant.
  | SequenceAnn !Deltas ![AnnotatedTree]
  -- ^ @SequenceAnn inc ts@ mirrors @'Sequence' ts@ for preserving the
  -- skeleton of a 'GrdTree's @ts@. It also carries the set of incoming values
  -- @inc@.
  | RedundantSrcBang !SrcInfo !AnnotatedTree
  -- ^ For tracking redundant bangs. See Note [Dead bang patterns]

pprSrcInfo :: SrcInfo -> SDoc
pprSrcInfo (L (RealSrcSpan rss _) _) = ppr (srcSpanStartLine rss)
pprSrcInfo (L s _)                   = ppr s

instance Outputable GrdTree where
  ppr (Rhs info)      = text "->" <+> pprSrcInfo info
  -- Format guards as "| True <- x, let x = 42, !z"
  ppr g@Guard{} = fsep (prefix (map ppr grds)) <+> ppr t
    where
      (t, grds)                  = collect_grds g
      collect_grds (Guard grd t) = (grd :) <$> collect_grds t
      collect_grds t             = (t, [])
      prefix []                  = []
      prefix (s:sdocs)           = char '|' <+> s : map (comma <+>) sdocs
  ppr (Sequence [])   = text "<empty case>"
  ppr (Sequence ts)   = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)

instance Outputable AnnotatedTree where
  ppr (AccessibleRhs _delta info) = parens (ppr _delta) <+> pprSrcInfo info
  ppr (InaccessibleRhs info) = text "inaccessible" <+> pprSrcInfo info
  ppr (MayDiverge t)         = text "div" <+> ppr t
  ppr (SequenceAnn _ [])       = text "<empty case>"
  ppr (SequenceAnn _ ts)       = braces (space <> fsep (punctuate semi (map ppr ts)) <> space)
  ppr (RedundantSrcBang l t) = text "redundant bang" <+> pprSrcInfo l <+> ppr t

-- | Lift 'addPmCts' over 'Deltas'.
addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas deltas cts = liftDeltasM (\d -> addPmCts d cts) deltas

-- | 'addPmCtsDeltas' a single 'PmCt'.
addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas
addPmCtDeltas deltas ct = addPmCtsDeltas deltas (unitBag ct)

-- | Test if any of the 'Delta's is inhabited. Currently this is pure, because
-- we preserve the invariant that there are no uninhabited 'Delta's. But that
-- could change in the future, for example by implementing this function in
-- terms of @notNull <$> provideEvidence 1 ds@.
isInhabited :: Deltas -> DsM Bool
isInhabited (MkDeltas ds) = pure (not (null ds))

-- | Pattern-match check result
data CheckResult
  = CheckResult
  { cr_clauses :: !AnnotatedTree
  -- ^ Captures redundancy info for each clause in the original program.
  --   (for -Woverlapping-patterns)
  , cr_uncov   :: !Deltas
  -- ^ The set of uncovered values falling out at the bottom.
  --   (for -Wincomplete-patterns)
  , 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
  }

instance Outputable CheckResult where
  ppr (CheckResult c unc pc)
    = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
        [ field "clauses" c <> comma
        , field "uncov" unc])
    where
      ppr_precision Precise     = empty
      ppr_precision Approximate = text "(Approximate)"
      field name value = text name <+> equals <+> ppr value

{-
%************************************************************************
%*                                                                      *
       Entry points to the checker: covCheckPatBind and covCheckMatchGroup
%*                                                                      *
%************************************************************************
-}

-- | Check a pattern binding (let, where) for exhaustiveness.
covCheckPatBind :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
covCheckPatBind dflags ctxt@(DsMatchContext _ locn) var p = do
  -- We only ever need to run this in a context where we need exhaustivity
  -- warnings (so not in pattern guards or comprehensions, for example, because
  -- they are perfectly fine to fail).
  -- Omitting checking this flag emits redundancy warnings twice in obscure
  -- cases like #17646.
  -- Given the context in which this function is called, it will only ever do
  -- something for
  --   * PatBindRhs, -Wincomplete-uni-patterns: @let True = False@
  --   * PatBindGuards, -Wincomplete-patterns: @Just x | False = Just 42@
  missing   <- getPmDeltas
  tracePm "covCheckPatBind" (vcat [ppr ctxt, ppr var, ppr p, ppr missing])
  fam_insts <- dsGetFamInstEnvs
  grd_tree  <- mkGrdTreeRhs (L locn $ ppr p) <$> translatePat fam_insts var p
  res <- checkGrdTree grd_tree missing
  dsPmWarn dflags ctxt [var] res

-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs.
covCheckGRHSs
  :: HsMatchContext GhcRn         -- ^ Match context, for warning messages
  -> GRHSs GhcTc (LHsExpr GhcTc)  -- ^ The GRHSs to check
  -> DsM (NonEmpty Deltas)        -- ^ Covered 'Deltas' for each RHS, for long
                                  --   distance info
covCheckGRHSs hs_ctx guards@(GRHSs _ grhss _) = do
    let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
        dsMatchContext = DsMatchContext hs_ctx combinedLoc
        match = L combinedLoc $
                  Match { m_ext = noExtField
                        , m_ctxt = hs_ctx
                        , m_pats = []
                        , m_grhss = guards }
    [(_, deltas)] <- covCheckMatchGroup dsMatchContext [] [match]
    pure deltas

-- | Check a list of syntactic /match/es (part of case, functions, etc.), each
-- with a /pat/ and one or more /grhss/:
--
-- @
--   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 'Deltas' for each GRHS, representing its covered values, or the
-- incoming uncovered 'Deltas' (from 'getPmDeltas') if the GRHS is inaccessible.
-- Since there is at least one /grhs/ per /match/, the list of 'Deltas' is at
-- least as long as the list of matches.
covCheckMatchGroup
  :: DsMatchContext                  -- ^ Match context, for warnings messages
  -> [Id]                            -- ^ Match variables, i.e. x and y above
  -> [LMatch GhcTc (LHsExpr GhcTc)]  -- ^ List of matches
  -> DsM [(Deltas, NonEmpty Deltas)] -- ^ One covered 'Deltas' per RHS, for long
                                     --   distance info.
covCheckMatchGroup ctxt vars matches = do
  tracePm "covCheckMatchGroup" (hang (vcat [ppr ctxt
                               , ppr vars
                               , text "Matches:"])
                               2
                               (vcat (map ppr matches)))

  init_deltas <- getPmDeltas
  missing <- case matches of
    -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
    [] | [var] <- vars -> addPmCtDeltas init_deltas (PmNotBotCt var)
    _                  -> pure init_deltas
  fam_insts <- dsGetFamInstEnvs
  grd_tree  <- translateMatches fam_insts vars matches
  res <- checkGrdTree grd_tree missing

  dflags <- getDynFlags
  dsPmWarn dflags ctxt vars res

  return (extractRhsDeltas (cr_clauses res))

-- | Extract the 'Deltas' reaching the RHSs of the 'AnnotatedTree' for a match
-- group.
-- For 'AccessibleRhs's, this is stored in the tree node, whereas
-- 'InaccessibleRhs's fall back to the supplied original 'Deltas'.
-- See @Note [Recovering from unsatisfiable pattern-matching constraints]@.
extractRhsDeltas :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
extractRhsDeltas = go_matches
  where
    go_matches :: AnnotatedTree -> [(Deltas, NonEmpty Deltas)]
    go_matches (SequenceAnn def ts) = map (go_match def) ts -- -XEmptyCase handled here!
    go_matches t                    = pprPanic "extractRhsDeltas.go_matches" (text "Matches must start with SequenceAnn. But was" $$ ppr t)

    go_match :: Deltas -> AnnotatedTree -> (Deltas, NonEmpty Deltas)
    -- There is no -XEmptyCase at this level, only at the Matches level. So @ts@
    -- is non-empty!
    go_match def (SequenceAnn pat ts)   = (pat, foldMap1 (text "go_match: empty SequenceAnn") (go_grhss def) ts)
    go_match def (MayDiverge t)         = go_match def t
    go_match def (RedundantSrcBang _ t) = go_match def t
    -- Even if there's only a single GRHS, we wrap it in a SequenceAnn for the
    -- Deltas covered by the pattern. So the remaining cases are impossible!
    go_match _   t                    = pprPanic "extractRhsDeltas.go_match" (text "Single GRHS must be wrapped in SequenceAnn. But got " $$ ppr t)

    go_grhss :: Deltas -> AnnotatedTree -> NonEmpty Deltas
    -- There is no -XEmptyCase at this level, only at the Matches level. So @ts@
    -- is non-empty!
    go_grhss def (SequenceAnn _ ts)       = foldMap1 (text "go_grhss: empty SequenceAnn") (go_grhss def) ts
    go_grhss def (MayDiverge t)           = go_grhss def t
    go_grhss def (RedundantSrcBang _ t)   = go_grhss def t
    go_grhss _   (AccessibleRhs deltas _) = deltas :| []
    go_grhss def (InaccessibleRhs _)      = def    :| []

    foldMap1 msg _ []     = pprPanic "extractRhsDeltas.foldMap1" msg
    foldMap1 _   f (x:xs) = foldl' (\acc x -> acc Semi.<> f x) (f x) xs

{- Note [Checking EmptyCase]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-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 Delta and check if there are any values left to match on.
-}

{-
%************************************************************************
%*                                                                      *
              Transform source syntax to *our* syntax
%*                                                                      *
%************************************************************************
-}

-- -----------------------------------------------------------------------
-- * Utilities

-- | 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, seq y True, [] <- 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 translate 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]

-- -----------------------------------------------------------------------
-- * Transform (Pat Id) into GrdVec

-- | @translatePat _ x pat@ transforms @pat@ into a 'GrdVec', where
-- the variable representing the match is @x@.
translatePat :: FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
translatePat fam_insts x pat = case pat of
  WildPat  _ty -> pure []
  VarPat _ y   -> pure (mkPmLetVar (unLoc y) x)
  ParPat _ p   -> translateLPat fam_insts 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 :) <$> translateLPat fam_insts x p
    where pm_loc = Just (L l (ppr p'))

  -- (x@pat)   ==>   Translate pat with x as match var and handle impedance
  --                 mismatch with incoming match var
  AsPat _ (L _ y) p -> (mkPmLetVar y x ++) <$> translateLPat fam_insts y p

  SigPat _ p _ty -> translateLPat fam_insts x p

  -- See Note [Translate 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                   -> translatePat fam_insts x p
    | WpCast co <-  wrapper, isReflexiveCo co -> translatePat fam_insts x p
    | otherwise -> do
        (y, grds) <- translatePatV fam_insts 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) <- translateLPatV fam_insts pat
    fun <- dsLExpr lexpr
    pure $ PmLet y (App fun (Var x)) : grds

  -- list
  ListPat (ListPatTc _elem_ty Nothing) ps ->
    translateListPat fam_insts 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 translate it as a regular ListPat
        -> translateListPat fam_insts x pats
      _ -> do
        y <- mkPmId (mkListTy elem_ty)
        grds <- translateListPat fam_insts 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
    translateConPatOut fam_insts 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 (translateLPatV fam_insts) pats
    let tuple_con = tupleDataCon boxity (length vars)
    pure $ vanillaConGrd x tuple_con vars : concat grdss

  SumPat _ty p alt arity -> do
    (y, grds) <- translateLPatV fam_insts p
    let sum_con = sumDataCon alt arity
    -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
    pure $ vanillaConGrd x sum_con [y] : grds

  -- --------------------------------------------------------------------------
  -- Not supposed to happen
  SplicePat {} -> panic "Check.translatePat: SplicePat"

-- | 'translatePat', but also select and return a new match var.
translatePatV :: FamInstEnvs -> Pat GhcTc -> DsM (Id, GrdVec)
translatePatV fam_insts pat = do
  x <- selectMatchVar Many pat
  grds <- translatePat fam_insts x pat
  pure (x, grds)

translateLPat :: FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat fam_insts x = translatePat fam_insts x . unLoc

-- | 'translateLPat', but also select and return a new match var.
translateLPatV :: FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV fam_insts = translatePatV fam_insts . unLoc

-- | @translateListPat _ x [p1, ..., pn]@ is basically
--   @translateConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever
-- constructing the 'ConPatOut's.
translateListPat :: FamInstEnvs -> Id -> [LPat GhcTc] -> DsM GrdVec
translateListPat fam_insts x pats = do
  vars_and_grdss <- traverse (translateLPatV fam_insts) pats
  mkListGrds x vars_and_grdss

-- | Translate a constructor pattern
translateConPatOut :: FamInstEnvs -> Id -> ConLike -> [Type] -> [TyVar]
                   -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec
translateConPatOut fam_insts 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 translate 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 first
      -- do a PmCon match, then force according to field strictness and then
      -- force evaluation of the field patterns in the order given by
      -- the first field of @tagged_pats@.
      -- See Note [Field match order for RecCon]

      -- Translate the mentioned field patterns. We're doing this first to get
      -- the Ids for pm_con_args.
      let trans_pat (n, pat) = do
            (var, pvec) <- translateLPatV fam_insts 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. bang strict fields
      let arg_is_banged = map isBanged $ conLikeImplBangs con
          noSrcPmBang i = PmBang {pm_id = i, pm_loc = Nothing}
          bang_grds     = map noSrcPmBang (filterByList arg_is_banged arg_ids)

      -- 3. guards from field selector patterns
      let arg_grds = concat arg_grdss

      -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
      --
      -- Store the guards in exactly that order
      --      1.         2.           3.
      pure (con_grd : bang_grds ++ arg_grds)

-- | Translate a the 'Match'es of a 'MatchGroup'
translateMatches :: FamInstEnvs -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)]
                 -> DsM GrdTree
translateMatches fam_insts vars matches =
  -- It's important that we wrap a 'Sequence' even if it only wraps a singleton.
  -- 'extractRhsDeltas' needs this to recover 'MatchGroup' structure.
  Sequence <$> traverse (translateMatch fam_insts vars) matches

-- Translate a single match
translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc)
               -> DsM GrdTree
translateMatch fam_insts vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
  pats'  <- concat <$> zipWithM (translateLPat fam_insts) vars pats
  grhss' <- translateGRHSs fam_insts match_loc (sep (map ppr pats)) grhss
  -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss'])
  return (foldr Guard grhss' pats')

mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
mkGrdTreeRhs sdoc = foldr Guard (Rhs sdoc)

translateGRHSs :: FamInstEnvs -> SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM GrdTree
translateGRHSs fam_insts match_loc pp_pats grhss =
  -- It's important that we wrap a 'Sequence' even if it only wraps a singleton.
  -- 'extractRhsDeltas' needs this to recover 'GRHSs' structure.
  Sequence <$> traverse (translateLGRHS fam_insts match_loc pp_pats) (grhssGRHSs grhss)

-- | Translate a guarded right-hand side to a single 'GrdTree'
translateLGRHS :: FamInstEnvs -> SrcSpan -> SDoc -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
translateLGRHS fam_insts match_loc pp_pats (L _loc (GRHS _ gs _)) =
  -- _loc points to the match separator (ie =, ->) that comes after the guards..
  mkGrdTreeRhs loc_sdoc <$> concatMapM (translateGuard fam_insts . unLoc) gs
    where
      loc_sdoc
        -- pp_pats is the space-separated pattern of the current Match this
        -- GRHS belongs to, so the @A B x@ part in @A B x | 0 <- x@.
        | null gs   = L match_loc pp_pats
        | otherwise = L grd_loc   (pp_pats <+> vbar <+> interpp'SP gs)
      L grd_loc _ = head gs

-- | Translate a guard statement to a 'GrdVec'
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
translateGuard fam_insts guard = case guard of
  BodyStmt _   e _ _ -> translateBoolGuard e
  LetStmt  _   binds -> translateLet (unLoc binds)
  BindStmt _ p e     -> translateBind fam_insts p e
  LastStmt        {} -> panic "translateGuard LastStmt"
  ParStmt         {} -> panic "translateGuard ParStmt"
  TransStmt       {} -> panic "translateGuard TransStmt"
  RecStmt         {} -> panic "translateGuard RecStmt"
  ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"

-- | Translate let-bindings
translateLet :: HsLocalBinds GhcTc -> DsM GrdVec
translateLet _binds = return []

-- | Translate a pattern guard
--   @pat <- e ==>  let x = e;  <guards for pat <- x>@
translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
translateBind fam_insts p e = dsLExpr e >>= \case
  Var y
    | Nothing <- isDataConId_maybe y
    -- RHS is a variable, so that will allow us to omit the let
    -> translateLPat fam_insts y p
  rhs -> do
    (x, grds) <- translateLPatV fam_insts p
    pure (PmLet x rhs : grds)

-- | Translate a boolean guard
--   @e ==>  let x = e; True <- x@
translateBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
translateBoolGuard 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 :: !Bool, b :: Char, c :: Int }
  f :: T -> ()
  f T{ c = 42, b = 'b' } = ()

Then
  * @f (T (error "a") (error "b") (error "c"))@ errors out with "a" because of
    the strict field.
  * @f (T True        (error "b") (error "c"))@ errors out with "c" because it
    is mentioned frist in the pattern match.

This means we can't just desugar the pattern match to the PatVec
@[T !_ 'b' 42]@. Instead we have to generate variable matches that have
strictness according to the field declarations and afterwards force them in the
right order. As a result, we get the PatVec @[T !_ b c, 42 <- c, 'b' <- b]@.

Of course, when the labels occur in the order they are defined, we can just use
the simpler desugaring.

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 translate 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 [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 Deltas 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 Delta, {}. 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 Delta {}. Why is this
sound (wrt. notion of the GADTs Meet their Match paper)? 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!

Note [Translate CoPats]
~~~~~~~~~~~~~~~~~~~~~~~
The pattern match checker did not know how to handle coerced patterns `CoPat`
efficiently, which gave rise to #11276. The original approach translated
`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.

%************************************************************************
%*                                                                      *
                 Utilities for Pattern Match Checking
%*                                                                      *
%************************************************************************
-}

-- ----------------------------------------------------------------------------
-- * Basic utilities

{-
Note [Extensions to GADTs Meet Their Match]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The GADTs Meet Their Match paper presents the formalism that GHC's coverage
checker adheres to. Since the paper's publication, there have been some
additional features added to the coverage checker which are not described in
the paper. This Note serves as a reference for these new features.

* Value abstractions are severely simplified to the point where they are just
  variables. The information about the shape of a variable is encoded in
  the oracle state 'Delta' instead.
* Handling of uninhabited fields like `!Void`.
  See Note [Strict argument type constraints] in GHC.HsToCore.PmCheck.Oracle.
* Efficient handling of literal splitting, large enumerations and accurate
  redundancy warnings for `COMPLETE` groups through the oracle.

Note [Filtering out non-matching COMPLETE sets]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Currently, conlikes in a COMPLETE set are simply grouped by the
type constructor heading the return type. This is nice and simple, but it does
mean that there are scenarios when a COMPLETE set might be incompatible with
the type of a scrutinee. For instance, consider (from #14135):

  data Foo a = Foo1 a | Foo2 a

  pattern MyFoo2 :: Int -> Foo Int
  pattern MyFoo2 i = Foo2 i

  {-# COMPLETE Foo1, MyFoo2 #-}

  f :: Foo a -> a
  f (Foo1 x) = x

`f` has an incomplete pattern-match, so when choosing which constructors to
report as unmatched in a warning, GHC must choose between the original set of
data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe
that GHC shouldn't even consider the COMPLETE set as a possibility: the return
type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since
there's no substitution `s` such that s(Foo Int) = Foo a.

To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern
synonym constructor's return type matches the type of the scrutinee, and if one
doesn't, then we remove the whole COMPLETE set from consideration.

One might wonder why GHC only checks /pattern synonym/ constructors, and not
/data/ constructors as well. The reason is because that the type of a
GADT constructor very well may not match the type of a scrutinee, and that's
OK. Consider this example (from #14059):

  data SBool (z :: Bool) where
    SFalse :: SBool False
    STrue  :: SBool True

  pattern STooGoodToBeTrue :: forall (z :: Bool). ()
                           => z ~ True
                           => SBool z
  pattern STooGoodToBeTrue = STrue
  {-# COMPLETE SFalse, STooGoodToBeTrue #-}

  wobble :: SBool z -> Bool
  wobble STooGoodToBeTrue = True

In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse
should be matched against, even though its type, SBool False, does not match
the scrutinee type, SBool z.

SG: Another angle at this is that the implied constraints when we instantiate
universal type variables in the return type of a GADT will lead to *provided*
thetas, whereas when we instantiate the return type of a pattern synonym that
corresponds to a *required* theta. See Note [Pattern synonym result type] in
PatSyn. Note how isValidCompleteMatches will successfully filter out

    pattern Just42 :: Maybe Int
    pattern Just42 = Just 42

But fail to filter out the equivalent

    pattern Just'42 :: (a ~ Int) => Maybe a
    pattern Just'42 = Just 42

Which seems fine as far as tcMatchTy is concerned, but it raises a few eye
brows.
-}

{-
%************************************************************************
%*                                                                      *
            Heart of the algorithm: checkGrdTree
%*                                                                      *
%************************************************************************
-}

-- | @throttle limit old new@ returns @old@ if the number of 'Delta's in @new@
-- is exceeding the given @limit@ and the @old@ number of 'Delta's.
-- See Note [Countering exponential blowup].
throttle :: Int -> Deltas -> Deltas -> (Precision, Deltas)
throttle limit old@(MkDeltas old_ds) new@(MkDeltas 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)

-- | Matching on a newtype doesn't force anything.
-- See Note [Divergence of Newtype matches] in "GHC.HsToCore.PmCheck.Oracle".
conMatchForces :: PmAltCon -> Bool
conMatchForces (PmAltConLike (RealDataCon dc))
  | isNewTyCon (dataConTyCon dc) = False
conMatchForces _                 = True

-- | Makes sure that we only wrap a single 'MayDiverge' around an
-- 'AnnotatedTree', purely for esthetic reasons.
mayDiverge :: AnnotatedTree -> AnnotatedTree
mayDiverge a@(MayDiverge _) = a
mayDiverge a                = MayDiverge a

-- | Computes two things:
--
--   * The set of uncovered values not matched by any of the clauses of the
--     'GrdTree'. Note that 'PmCon' guards are the only way in which values
--     fall through from one 'Many' branch to the next.
--   * An 'AnnotatedTree' that contains divergence and inaccessibility info
--     for all clauses. Will be fed to 'extractRedundancyInfo' for
--     presenting redundant and proper innaccessible RHSs, as well as dead
--     bangs to the user.
checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
-- RHS: Check that it covers something and wrap Inaccessible if not
checkGrdTree' (Rhs sdoc) deltas = do
  is_covered <- isInhabited deltas
  let clauses
        | is_covered = AccessibleRhs deltas sdoc
        | otherwise  = InaccessibleRhs sdoc
  pure CheckResult
    { cr_clauses = clauses
    , cr_uncov   = MkDeltas emptyBag
    , cr_approx  = Precise }
-- let x = e: Refine with x ~ e
checkGrdTree' (Guard (PmLet x e) tree) deltas = do
  deltas' <- addPmCtDeltas deltas (PmCoreCt x e)
  checkGrdTree' tree deltas'
-- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
checkGrdTree' (Guard (PmBang x src_bang_info) tree) deltas = do
  has_diverged <- addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
  deltas' <- addPmCtDeltas deltas (PmNotBotCt x)
  res <- checkGrdTree' tree deltas'
  let clauses
        | not has_diverged
        , Just info <- src_bang_info
        = RedundantSrcBang info (cr_clauses res)
        | has_diverged
        = mayDiverge (cr_clauses res)
        | otherwise -- won't diverge and it wasn't a source bang
        = cr_clauses res

  pure res{ cr_clauses = clauses }

-- Con: Diverge on x ~ ⊥, fall through on x /~ K and refine with x ~ K ys
--      and type info
checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
  has_diverged <-
    if conMatchForces con
      then addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
      else pure False
  unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
  deltas' <- addPmCtsDeltas deltas $
    listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con tvs args
  -- tracePm "checkGrdTree:Con" (ppr deltas $$ ppr x $$ ppr con $$ ppr dicts $$ ppr deltas')
  CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
  limit <- maxPmCheckModels <$> getDynFlags
  let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
  pure CheckResult
    { cr_clauses = applyWhen has_diverged mayDiverge tree'
    , cr_uncov = unc'
    , cr_approx = prec Semi.<> prec' }
-- Sequence: Thread residual uncovered sets from equation to equation
checkGrdTree' (Sequence ts) init_unc = go [] init_unc Precise ts
  where
    -- | Accumulates a CheckResult. Its type is more like
    -- @CheckResult -> [GrdTree] -> CheckResult@, but cr_clauses is a single
    -- 'AnnotatedTree', not a list thereof. Hence 3 parameters to thread the
    -- fields.
    go :: [AnnotatedTree] -> Deltas -> Precision -> [GrdTree] -> DsM CheckResult
    -- No cases left: Fall through for all values
    go ts' unc prec [] = pure CheckResult
                          { cr_clauses = SequenceAnn init_unc (reverse ts')
                          , cr_uncov = unc
                          , cr_approx = prec }
    go ts' unc prec (t:ts) = do
      CheckResult t' unc_1 prec_t <- checkGrdTree' t unc
      go (t':ts') unc_1 (prec_t Semi.<> prec) ts

-- | Print diagnostic info and actually call 'checkGrdTree''.
checkGrdTree :: GrdTree -> Deltas -> DsM CheckResult
checkGrdTree guards deltas = do
  tracePm "checkGrdTree {" $ vcat [ ppr guards
                                  , ppr deltas ]
  res <- checkGrdTree' guards deltas
  tracePm "checkGrdTree }:" (ppr res) -- braces are easier to match by tooling
  return res

-- ----------------------------------------------------------------------------
-- * Propagation of term constraints inwards when checking nested matches

{- Note [Type and Term Equality Propagation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking a match it would be great to have all type and term information
available so we can get more precise results. For this reason we have functions
`addDictsDs' and `addTmVarCsDs' in GHC.HsToCore.Monad that store in the
environment type and term constraints (respectively) as we go deeper.

The type constraints we propagate inwards are collected by `collectEvVarsPats'
in GHC.Hs.Pat. This handles bug #4139 ( see example
  https://gitlab.haskell.org/ghc/ghc/snippets/672 )
where this is needed.

For term equalities we do less, we just generate equalities for HsCase. For
example we accurately give 2 redundancy warnings for the marked cases:

f :: [a] -> Bool
f x = case x of

  []    -> case x of        -- brings (x ~ []) in scope
             []    -> True
             (_:_) -> False -- can't happen

  (_:_) -> case x of        -- brings (x ~ (_:_)) in scope
             (_:_) -> True
             []    -> False -- can't happen

Functions `add*ScrutTmCs' is responsible for generating
these constraints.
-}

-- | Locally update 'dsl_deltas' with the given action, but defer evaluation
-- with 'unsafeInterleaveM' in order not to do unnecessary work.
locallyExtendPmDelta :: (Deltas -> DsM Deltas) -> DsM a -> DsM a
locallyExtendPmDelta ext k = do
  deltas <- getPmDeltas
  deltas' <- unsafeInterleaveM $ do
    deltas' <- ext deltas
    inh <- isInhabited deltas'
    -- If adding a constraint would lead to a contradiction, don't add it.
    -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@
    -- for why this is done.
    if inh
      then pure deltas'
      else pure deltas
  updPmDeltas deltas' k

-- | Add in-scope type constraints if the coverage checker might run and then
-- run the given action.
addTyCsDs :: Origin -> Bag EvVar -> DsM a -> DsM a
addTyCsDs origin ev_vars m = do
  dflags <- getDynFlags
  applyWhen (needToRunPmCheck dflags origin)
            (locallyExtendPmDelta (\deltas -> addPmCtsDeltas deltas (PmTyCt . 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 locallyExtendPmDelta k $ \deltas ->
    addPmCtsDeltas deltas (unitBag (PmCoreCt 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

{-
%************************************************************************
%*                                                                      *
      Pretty printing of exhaustiveness/redundancy check warnings
%*                                                                      *
%************************************************************************
-}

-- | 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)

-- | A type for organising information to be used in warnings.
data RedundancyInfo
  = RedundancyInfo
  { redundant_rhss    :: ![SrcInfo]
  , inaccessible_rhss :: ![SrcInfo]
  , redundant_bangs   :: ![Located SDoc]
  }

extractRedundancyInfo :: AnnotatedTree -> RedundancyInfo
extractRedundancyInfo tree =
  RedundancyInfo { redundant_rhss    = fromOL ol_red
                 , inaccessible_rhss = fromOL ol_inacc
                 , redundant_bangs   = fromOL ol_bangs }
  where
    (_ol_acc, ol_inacc, ol_red, ol_bangs) = go tree
    -- | Collects
    --    1. accessible RHSs
    --    2. proper inaccessible RHSs (so we can't delete them)
    --    3. hypothetically redundant RHSs (so not only inaccessible, but we can
    --       even safely delete the equation without altering semantics)
    --    4. 'Dead' bangs from the source, collected to be warned about
    -- See Note [Determining inaccessible clauses]
    -- See Note [Dead bang patterns]
    go :: AnnotatedTree -> (OrdList SrcInfo, OrdList SrcInfo, OrdList SrcInfo, OrdList SrcInfo)
    go (AccessibleRhs _ info) = (unitOL info, nilOL, nilOL      , nilOL)
    go (InaccessibleRhs info) = (nilOL,       nilOL, unitOL info, nilOL) -- presumably redundant
    go (MayDiverge t)         = case go t of
      -- See Note [Determining inaccessible clauses]
      (acc, inacc, red, bs)
        | isNilOL acc && isNilOL inacc -> (nilOL, red, nilOL, bs)
      res                              -> res
    go (SequenceAnn _ ts)     = foldMap go ts
    go (RedundantSrcBang l t) = case go t of
      -- See Note [Dead bang patterns]
      res@(acc, inacc, _, _)
        | isNilOL acc, isNilOL inacc -> res
        | otherwise                  -> (nilOL, nilOL, nilOL, unitOL l) Semi.<> res

{- 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
that it's part of a sub-tree in the pattern match that forces some argument
(which corresponds to wrapping the 'AnnotatedTree' in 'MayDiverge'). Then we
turn all supposedly redundant RHSs into inaccessible ones.

But as it turns out (@g@ from #17465) this is too conservative:
  g () | False = ()
       | otherwise = ()
g's first clause has an inaccessible RHS, but it's also safe to delete. So it's
redundant, really! But by just turning all redundant child clauses into
inaccessible ones, we report the first clause as inaccessible.

Clearly, it is enough if we say that we only degrade if *not all* of the child
clauses are redundant. As long as there is at least one clause which we announce
not to be redundant, the guard prefix responsible for the 'MayDiverge' will
survive. Hence we check for that in 'extractRedundancyInfo'.
-}

-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
dsPmWarn dflags ctx@(DsMatchContext kind loc) vars result
  = 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
    CheckResult
      { cr_clauses = clauses
      , cr_uncov   = uncovered
      , cr_approx  = precision } = result
    RedundancyInfo{redundant_rhss, inaccessible_rhss, redundant_bangs}
      = extractRedundancyInfo clauses

    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 deltas = pprContext False ctx (text "are non-exhaustive") $ \_ ->
      case vars of -- See #11245
           [] -> text "Guards do not cover entire pattern space"
           _  -> let us = map (\delta -> pprUncovered delta vars) deltas
                 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 -> Deltas -> DsM [Delta]
getNFirstUncovered vars n (MkDeltas deltas) = go n (bagToList deltas)
  where
    go 0 _              = pure []
    go _ []             = pure []
    go n (delta:deltas) = do
      front <- provideEvidence vars n delta
      back <- go (n - length front) deltas
      pure (front ++ back)

{- 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.
-}

dots :: Int -> [a] -> SDoc
dots maxPatterns qs
    | qs `lengthExceeds` maxPatterns = text "..."
    | otherwise                      = empty

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

-- True <==> singular
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)