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

Pattern Matching Coverage Checking.
-}

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

module GHC.HsToCore.PmCheck (
        -- Checking and printing
        checkSingle, checkMatches, checkGuardMatches,
        isMatchContextPmChecked,

        -- See Note [Type and Term Equality Propagation]
        addTyCsDs, addScrutTmCs
    ) 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.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

{-
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 {
      PmGrd -> Id
pm_id          :: !Id,
      PmGrd -> PmAltCon
pm_con_con     :: !PmAltCon,
      PmGrd -> [Id]
pm_con_tvs     :: ![TyVar],
      PmGrd -> [Id]
pm_con_dicts   :: ![EvVar],
      PmGrd -> [Id]
pm_con_args    :: ![Id]
    }

    -- | @PmBang x@ corresponds to a @seq x True@ guard.
  | PmBang {
      pm_id          :: !Id
    }

    -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
    -- /binds/ @x@.
  | PmLet {
      pm_id        :: !Id,
      PmGrd -> CoreExpr
_pm_let_expr :: !CoreExpr
    }

-- | Should not be user-facing.
instance Outputable PmGrd where
  ppr :: PmGrd -> SDoc
ppr (PmCon Id
x PmAltCon
alt [Id]
_tvs [Id]
_con_dicts [Id]
con_args)
    = [SDoc] -> SDoc
hsep [PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
alt, [SDoc] -> SDoc
hsep ((Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
con_args), String -> SDoc
text String
"<-", Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x]
  ppr (PmBang Id
x) = Char -> SDoc
char Char
'!' SDoc -> SDoc -> SDoc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x
  ppr (PmLet Id
x CoreExpr
expr) = [SDoc] -> SDoc
hsep [String -> SDoc
text String
"let", Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x, String -> SDoc
text String
"=", CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
expr]

type GrdVec = [PmGrd]

data Precision = Approximate | Precise
  deriving (Precision -> Precision -> Bool
(Precision -> Precision -> Bool)
-> (Precision -> Precision -> Bool) -> Eq Precision
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Precision -> Precision -> Bool
$c/= :: Precision -> Precision -> Bool
== :: Precision -> Precision -> Bool
$c== :: Precision -> Precision -> Bool
Eq, Int -> Precision -> ShowS
[Precision] -> ShowS
Precision -> String
(Int -> Precision -> ShowS)
-> (Precision -> String)
-> ([Precision] -> ShowS)
-> Show Precision
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Precision] -> ShowS
$cshowList :: [Precision] -> ShowS
show :: Precision -> String
$cshow :: Precision -> String
showsPrec :: Int -> Precision -> ShowS
$cshowsPrec :: Int -> Precision -> ShowS
Show)

instance Outputable Precision where
  ppr :: Precision -> SDoc
ppr = String -> SDoc
text (String -> SDoc) -> (Precision -> String) -> Precision -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Precision -> String
forall a. Show a => a -> String
show

instance Semi.Semigroup Precision where
  Precision
Precise <> :: Precision -> Precision -> Precision
<> Precision
Precise = Precision
Precise
  Precision
_       <> Precision
_       = Precision
Approximate

instance Monoid Precision where
  mempty :: Precision
mempty = Precision
Precise
  mappend :: Precision -> Precision -> Precision
mappend = Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
(Semi.<>)

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

-- | A representation of the desugaring to 'PmGrd's of all clauses of a
-- function definition/pattern match/etc.
data GrdTree
  = Rhs !RhsInfo
  | 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 !GrdTree
  -- ^ @Sequence l r@ first matches against @l@, and then matches all
  -- fallen-through values against @r@. Models top-to-bottom semantics of
  -- pattern matching.
  | Empty
  -- ^ A @GrdTree@ that always fails. Most useful for
  -- Note [Checking EmptyCase]. A neutral element to 'Sequence'.

-- | The digest of 'checkGrdTree', representing the annotated pattern-match
-- tree. 'redundantAndInaccessibleRhss' can figure out redundant and proper
-- inaccessible RHSs from this.
data AnnotatedTree
  = AccessibleRhs !Deltas !RhsInfo
  -- ^ A RHS deemed accessible. The 'Deltas' is the (non-empty) set of covered
  -- values.
  | InaccessibleRhs !RhsInfo
  -- ^ 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 !AnnotatedTree !AnnotatedTree
  -- ^ Mirrors 'Sequence' for preserving the skeleton of a 'GrdTree's.
  | EmptyAnn
  -- ^ Mirrors 'Empty' for preserving the skeleton of a 'GrdTree's.

pprRhsInfo :: RhsInfo -> SDoc
pprRhsInfo :: RhsInfo -> SDoc
pprRhsInfo (L (RealSrcSpan RealSrcSpan
rss Maybe BufSpan
_) SDoc
_) = Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
rss)
pprRhsInfo (L SrcSpan
s SDoc
_)                   = SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
s

instance Outputable GrdTree where
  ppr :: GrdTree -> SDoc
ppr (Rhs RhsInfo
info)      = String -> SDoc
text String
"->" SDoc -> SDoc -> SDoc
<+> RhsInfo -> SDoc
pprRhsInfo RhsInfo
info
  -- Format guards as "| True <- x, let x = 42, !z"
  ppr g :: GrdTree
g@Guard{} = [SDoc] -> SDoc
fsep ([SDoc] -> [SDoc]
prefix ((PmGrd -> SDoc) -> [PmGrd] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PmGrd -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PmGrd]
grds)) SDoc -> SDoc -> SDoc
<+> GrdTree -> SDoc
forall a. Outputable a => a -> SDoc
ppr GrdTree
t
    where
      (GrdTree
t, [PmGrd]
grds)                  = GrdTree -> (GrdTree, [PmGrd])
collect_grds GrdTree
g
      collect_grds :: GrdTree -> (GrdTree, [PmGrd])
collect_grds (Guard PmGrd
grd GrdTree
t) = (PmGrd
grd PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
:) ([PmGrd] -> [PmGrd]) -> (GrdTree, [PmGrd]) -> (GrdTree, [PmGrd])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GrdTree -> (GrdTree, [PmGrd])
collect_grds GrdTree
t
      collect_grds GrdTree
t             = (GrdTree
t, [])
      prefix :: [SDoc] -> [SDoc]
prefix []                  = []
      prefix (SDoc
s:[SDoc]
sdocs)           = Char -> SDoc
char Char
'|' SDoc -> SDoc -> SDoc
<+> SDoc
s SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: (SDoc -> SDoc) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SDoc
comma SDoc -> SDoc -> SDoc
<+>) [SDoc]
sdocs
  -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
  ppr t :: GrdTree
t@Sequence{}    = SDoc -> SDoc
braces (SDoc
space SDoc -> SDoc -> SDoc
<> [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
semi (GrdTree -> [SDoc]
collect_seqs GrdTree
t)) SDoc -> SDoc -> SDoc
<> SDoc
space)
    where
      collect_seqs :: GrdTree -> [SDoc]
collect_seqs (Sequence GrdTree
l GrdTree
r) = GrdTree -> [SDoc]
collect_seqs GrdTree
l [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ GrdTree -> [SDoc]
collect_seqs GrdTree
r
      collect_seqs GrdTree
t              = [GrdTree -> SDoc
forall a. Outputable a => a -> SDoc
ppr GrdTree
t]
  ppr GrdTree
Empty          = String -> SDoc
text String
"<empty case>"

instance Outputable AnnotatedTree where
  ppr :: AnnotatedTree -> SDoc
ppr (AccessibleRhs Deltas
_ RhsInfo
info) = RhsInfo -> SDoc
pprRhsInfo RhsInfo
info
  ppr (InaccessibleRhs RhsInfo
info) = String -> SDoc
text String
"inaccessible" SDoc -> SDoc -> SDoc
<+> RhsInfo -> SDoc
pprRhsInfo RhsInfo
info
  ppr (MayDiverge AnnotatedTree
t)         = String -> SDoc
text String
"div" SDoc -> SDoc -> SDoc
<+> AnnotatedTree -> SDoc
forall a. Outputable a => a -> SDoc
ppr AnnotatedTree
t
    -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
  ppr t :: AnnotatedTree
t@SequenceAnn{}        = SDoc -> SDoc
braces (SDoc
space SDoc -> SDoc -> SDoc
<> [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
semi (AnnotatedTree -> [SDoc]
collect_seqs AnnotatedTree
t)) SDoc -> SDoc -> SDoc
<> SDoc
space)
    where
      collect_seqs :: AnnotatedTree -> [SDoc]
collect_seqs (SequenceAnn AnnotatedTree
l AnnotatedTree
r) = AnnotatedTree -> [SDoc]
collect_seqs AnnotatedTree
l [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ AnnotatedTree -> [SDoc]
collect_seqs AnnotatedTree
r
      collect_seqs AnnotatedTree
t                 = [AnnotatedTree -> SDoc
forall a. Outputable a => a -> SDoc
ppr AnnotatedTree
t]
  ppr AnnotatedTree
EmptyAnn               = String -> SDoc
text String
"<empty case>"

-- | Lift 'addPmCts' over 'Deltas'.
addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas Deltas
deltas PmCts
cts = (Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> Deltas -> DsM Deltas
forall (m :: * -> *).
Monad m =>
(Delta -> m (Maybe Delta)) -> Deltas -> m Deltas
liftDeltasM (\Delta
d -> Delta -> PmCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addPmCts Delta
d PmCts
cts) Deltas
deltas

-- | 'addPmCtsDeltas' a single 'PmCt'.
addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas
addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
deltas PmCt
ct = Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas Deltas
deltas (PmCt -> PmCts
forall a. a -> Bag a
unitBag PmCt
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 :: Deltas -> DsM Bool
isInhabited (MkDeltas Bag Delta
ds) = Bool -> DsM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool
not (Bag Delta -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Bag Delta
ds))

-- | Pattern-match check result
data CheckResult
  = CheckResult
  { CheckResult -> AnnotatedTree
cr_clauses :: !AnnotatedTree
  -- ^ Captures redundancy info for each clause in the original program.
  --   (for -Woverlapping-patterns)
  , CheckResult -> Deltas
cr_uncov   :: !Deltas
  -- ^ The set of uncovered values falling out at the bottom.
  --   (for -Wincomplete-patterns)
  , CheckResult -> Precision
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 -> SDoc
ppr (CheckResult AnnotatedTree
c Deltas
unc Precision
pc)
    = String -> SDoc
text String
"CheckResult" SDoc -> SDoc -> SDoc
<+> Precision -> SDoc
ppr_precision Precision
pc SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
fsep
        [ String -> AnnotatedTree -> SDoc
forall {a}. Outputable a => String -> a -> SDoc
field String
"clauses" AnnotatedTree
c SDoc -> SDoc -> SDoc
<> SDoc
comma
        , String -> Deltas -> SDoc
forall {a}. Outputable a => String -> a -> SDoc
field String
"uncov" Deltas
unc])
    where
      ppr_precision :: Precision -> SDoc
ppr_precision Precision
Precise     = SDoc
empty
      ppr_precision Precision
Approximate = String -> SDoc
text String
"(Approximate)"
      field :: String -> a -> SDoc
field String
name a
value = String -> SDoc
text String
name SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
value

{-
%************************************************************************
%*                                                                      *
       Entry points to the checker: checkSingle and checkMatches
%*                                                                      *
%************************************************************************
-}

-- | Check a single pattern binding (let) for exhaustiveness.
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
checkSingle :: DynFlags
-> DsMatchContext -> Id -> Pat (GhcPass 'Typechecked) -> DsM ()
checkSingle DynFlags
dflags ctxt :: DsMatchContext
ctxt@(DsMatchContext HsMatchContext GhcRn
kind SrcSpan
locn) Id
var Pat (GhcPass 'Typechecked)
p = do
  String -> SDoc -> DsM ()
tracePm String
"checkSingle" ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt, Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
var, Pat (GhcPass 'Typechecked) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Pat (GhcPass 'Typechecked)
p])
  -- 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.
  Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> HsMatchContext GhcRn -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext GhcRn
kind) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ do
    -- TODO: This could probably call checkMatches, like checkGuardMatches.
    Deltas
missing   <- DsM Deltas
getPmDeltas
    String -> SDoc -> DsM ()
tracePm String
"checkSingle: missing" (Deltas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Deltas
missing)
    FamInstEnvs
fam_insts <- DsM FamInstEnvs
dsGetFamInstEnvs
    GrdTree
grd_tree  <- RhsInfo -> [PmGrd] -> GrdTree
mkGrdTreeRhs (SrcSpan -> SDoc -> RhsInfo
forall l e. l -> e -> GenLocated l e
L SrcSpan
locn (SDoc -> RhsInfo) -> SDoc -> RhsInfo
forall a b. (a -> b) -> a -> b
$ Pat (GhcPass 'Typechecked) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Pat (GhcPass 'Typechecked)
p) ([PmGrd] -> GrdTree)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> Id
-> Pat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translatePat FamInstEnvs
fam_insts Id
var Pat (GhcPass 'Typechecked)
p
    CheckResult
res <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree GrdTree
grd_tree Deltas
missing
    DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
dsPmWarn DynFlags
dflags DsMatchContext
ctxt [Id
var] CheckResult
res

-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions. Returns the 'Deltas' covered by the RHSs.
checkGuardMatches
  :: HsMatchContext GhcRn         -- ^ Match context, for warning messages
  -> GRHSs GhcTc (LHsExpr GhcTc)  -- ^ The GRHSs to check
  -> DsM [Deltas]                 -- ^ Covered 'Deltas' for each RHS, for long
                                  --   distance info
checkGuardMatches :: HsMatchContext GhcRn
-> GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> DsM [Deltas]
checkGuardMatches HsMatchContext GhcRn
hs_ctx guards :: GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
guards@(GRHSs XCGRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
_ [LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
grhss LHsLocalBinds (GhcPass 'Typechecked)
_) = do
    let combinedLoc :: SrcSpan
combinedLoc = (SrcSpan -> SrcSpan -> SrcSpan) -> [SrcSpan] -> SrcSpan
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SrcSpan -> SrcSpan -> SrcSpan
combineSrcSpans ((LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
 -> SrcSpan)
-> [LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
-> [SrcSpan]
forall a b. (a -> b) -> [a] -> [b]
map LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> SrcSpan
forall l e. GenLocated l e -> l
getLoc [LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
grhss)
        dsMatchContext :: DsMatchContext
dsMatchContext = HsMatchContext GhcRn -> SrcSpan -> DsMatchContext
DsMatchContext HsMatchContext GhcRn
hs_ctx SrcSpan
combinedLoc
        match :: LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
match = SrcSpan
-> Match (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
forall l e. l -> e -> GenLocated l e
L SrcSpan
combinedLoc (Match (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
 -> LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked)))
-> Match (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
forall a b. (a -> b) -> a -> b
$
                  Match :: forall p body.
XCMatch p body
-> HsMatchContext (NoGhcTc p)
-> [LPat p]
-> GRHSs p body
-> Match p body
Match { m_ext :: XCMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
m_ext = NoExtField
XCMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
noExtField
                        , m_ctxt :: HsMatchContext (NoGhcTc (GhcPass 'Typechecked))
m_ctxt = HsMatchContext GhcRn
HsMatchContext (NoGhcTc (GhcPass 'Typechecked))
hs_ctx
                        , m_pats :: [LPat (GhcPass 'Typechecked)]
m_pats = []
                        , m_grhss :: GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
m_grhss = GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
guards }
    DsMatchContext
-> [Id]
-> [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
-> DsM [Deltas]
checkMatches DsMatchContext
dsMatchContext [] [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
match]

-- | 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.
checkMatches
  :: DsMatchContext                  -- ^ Match context, for warnings messages
  -> [Id]                            -- ^ Match variables, i.e. x and y above
  -> [LMatch GhcTc (LHsExpr GhcTc)]  -- ^ List of matches
  -> DsM [Deltas]                    -- ^ One covered 'Deltas' per RHS, for long
                                     --   distance info.
checkMatches :: DsMatchContext
-> [Id]
-> [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
-> DsM [Deltas]
checkMatches DsMatchContext
ctxt [Id]
vars [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
matches = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  String -> SDoc -> DsM ()
tracePm String
"checkMatches" (SDoc -> Int -> SDoc -> SDoc
hang ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt
                               , [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
vars
                               , String -> SDoc
text String
"Matches:"])
                               Int
2
                               ([SDoc] -> SDoc
vcat ((LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
 -> SDoc)
-> [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
-> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
matches)))

  Deltas
init_deltas <- DsM Deltas
getPmDeltas
  Deltas
missing <- case [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
matches of
    -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
    [] | [Id
var] <- [Id]
vars -> Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
init_deltas (Id -> PmCt
PmNotBotCt Id
var)
    [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
_                  -> Deltas -> DsM Deltas
forall (f :: * -> *) a. Applicative f => a -> f a
pure Deltas
init_deltas
  FamInstEnvs
fam_insts <- DsM FamInstEnvs
dsGetFamInstEnvs
  GrdTree
grd_tree  <- [PmGrd] -> [GrdTree] -> GrdTree
mkGrdTreeMany [] ([GrdTree] -> GrdTree)
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdTree]
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
 -> IOEnv (Env DsGblEnv DsLclEnv) GrdTree)
-> [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdTree]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs
-> [Id]
-> LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
translateMatch FamInstEnvs
fam_insts [Id]
vars) [LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
matches
  CheckResult
res <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree GrdTree
grd_tree Deltas
missing

  DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
dsPmWarn DynFlags
dflags DsMatchContext
ctxt [Id]
vars CheckResult
res

  [Deltas] -> DsM [Deltas]
forall (m :: * -> *) a. Monad m => a -> m a
return (Deltas -> AnnotatedTree -> [Deltas]
extractRhsDeltas Deltas
init_deltas (CheckResult -> AnnotatedTree
cr_clauses CheckResult
res))

-- | Extract the 'Deltas' reaching the RHSs of the 'AnnotatedTree'.
-- For 'AccessibleRhs's, this is stored in the tree node, whereas
-- 'InaccessibleRhs's fall back to the supplied original 'Deltas'.
-- See @Note [Recovering from unsatisfiable pattern-matching constraints]@.
extractRhsDeltas :: Deltas -> AnnotatedTree -> [Deltas]
extractRhsDeltas :: Deltas -> AnnotatedTree -> [Deltas]
extractRhsDeltas Deltas
orig_deltas = OrdList Deltas -> [Deltas]
forall a. OrdList a -> [a]
fromOL (OrdList Deltas -> [Deltas])
-> (AnnotatedTree -> OrdList Deltas) -> AnnotatedTree -> [Deltas]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotatedTree -> OrdList Deltas
go
  where
    go :: AnnotatedTree -> OrdList Deltas
go (AccessibleRhs Deltas
deltas RhsInfo
_) = Deltas -> OrdList Deltas
forall a. a -> OrdList a
unitOL Deltas
deltas
    go (InaccessibleRhs RhsInfo
_)      = Deltas -> OrdList Deltas
forall a. a -> OrdList a
unitOL Deltas
orig_deltas
    go (MayDiverge AnnotatedTree
t)           = AnnotatedTree -> OrdList Deltas
go AnnotatedTree
t
    go (SequenceAnn AnnotatedTree
l AnnotatedTree
r)        = AnnotatedTree -> OrdList Deltas
go AnnotatedTree
l OrdList Deltas -> OrdList Deltas -> OrdList Deltas
forall a. Semigroup a => a -> a -> a
Semi.<> AnnotatedTree -> OrdList Deltas
go AnnotatedTree
r
    go AnnotatedTree
EmptyAnn                 = OrdList Deltas
forall a. OrdList a
nilOL

{- 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 :: Id -> Id -> [PmGrd]
mkPmLetVar Id
x Id
y | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
y = []
mkPmLetVar Id
x Id
y          = [Id -> CoreExpr -> PmGrd
PmLet Id
x (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
y)]

-- | ADT constructor pattern => no existentials, no local constraints
vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
scrut DataCon
con [Id]
arg_ids =
  PmCon :: Id -> PmAltCon -> [Id] -> [Id] -> [Id] -> PmGrd
PmCon { pm_id :: Id
pm_id = Id
scrut, pm_con_con :: PmAltCon
pm_con_con = ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
con)
        , pm_con_tvs :: [Id]
pm_con_tvs = [], pm_con_dicts :: [Id]
pm_con_dicts = [], pm_con_args :: [Id]
pm_con_args = [Id]
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 :: Id -> [(Id, [PmGrd])] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkListGrds Id
a []                  = [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
a DataCon
nilDataCon []]
mkListGrds Id
a ((Id
x, [PmGrd]
head_grds):[(Id, [PmGrd])]
xs) = do
  Id
b <- Type -> DsM Id
mkPmId (Id -> Type
idType Id
a)
  [PmGrd]
tail_grds <- Id -> [(Id, [PmGrd])] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkListGrds Id
b [(Id, [PmGrd])]
xs
  [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a b. (a -> b) -> a -> b
$ Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
a DataCon
consDataCon [Id
x, Id
b] PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
head_grds [PmGrd] -> [PmGrd] -> [PmGrd]
forall a. [a] -> [a] -> [a]
++ [PmGrd]
tail_grds

-- | Create a 'GrdVec' refining a match variable to a 'PmLit'.
mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
mkPmLitGrds :: Id -> PmLit -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkPmLitGrds Id
x (PmLit Type
_ (PmLitString FastString
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
  [Id]
vars <- (Type -> DsM Id) -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [Id]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type -> DsM Id
mkPmId (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
take (FastString -> Int
lengthFS FastString
s) (Type -> [Type]
forall a. a -> [a]
repeat Type
charTy))
  let mk_char_lit :: Id -> Char -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mk_char_lit Id
y Char
c = Id -> PmLit -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkPmLitGrds Id
y (Type -> PmLitValue -> PmLit
PmLit Type
charTy (Char -> PmLitValue
PmLitChar Char
c))
  [[PmGrd]]
char_grdss <- (Id -> Char -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [Id] -> String -> IOEnv (Env DsGblEnv DsLclEnv) [[PmGrd]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Id -> Char -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mk_char_lit [Id]
vars (FastString -> String
unpackFS FastString
s)
  Id -> [(Id, [PmGrd])] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkListGrds Id
x ([Id] -> [[PmGrd]] -> [(Id, [PmGrd])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
vars [[PmGrd]]
char_grdss)
mkPmLitGrds Id
x PmLit
lit = do
  let grd :: PmGrd
grd = PmCon :: Id -> PmAltCon -> [Id] -> [Id] -> [Id] -> PmGrd
PmCon { pm_id :: Id
pm_id = Id
x
                  , pm_con_con :: PmAltCon
pm_con_con = PmLit -> PmAltCon
PmAltLit PmLit
lit
                  , pm_con_tvs :: [Id]
pm_con_tvs = []
                  , pm_con_dicts :: [Id]
pm_con_dicts = []
                  , pm_con_args :: [Id]
pm_con_args = [] }
  [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [PmGrd
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 :: FamInstEnvs
-> Id
-> Pat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translatePat FamInstEnvs
fam_insts Id
x Pat (GhcPass 'Typechecked)
pat = case Pat (GhcPass 'Typechecked)
pat of
  WildPat  XWildPat (GhcPass 'Typechecked)
_ty -> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  VarPat XVarPat (GhcPass 'Typechecked)
_ Located (IdP (GhcPass 'Typechecked))
y   -> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> Id -> [PmGrd]
mkPmLetVar (Located Id -> Id
forall l e. GenLocated l e -> e
unLoc Located Id
Located (IdP (GhcPass 'Typechecked))
y) Id
x)
  ParPat XParPat (GhcPass 'Typechecked)
_ LPat (GhcPass 'Typechecked)
p   -> FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts Id
x LPat (GhcPass 'Typechecked)
p
  LazyPat XLazyPat (GhcPass 'Typechecked)
_ LPat (GhcPass 'Typechecked)
_  -> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] -- like a wildcard
  BangPat XBangPat (GhcPass 'Typechecked)
_ LPat (GhcPass 'Typechecked)
p  ->
    -- Add the bang in front of the list, because it will happen before any
    -- nested stuff.
    (Id -> PmGrd
PmBang Id
x PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
:) ([PmGrd] -> [PmGrd])
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts Id
x LPat (GhcPass 'Typechecked)
p

  -- (x@pat)   ==>   Translate pat with x as match var and handle impedance
  --                 mismatch with incoming match var
  AsPat XAsPat (GhcPass 'Typechecked)
_ (L SrcSpan
_ IdP (GhcPass 'Typechecked)
y) LPat (GhcPass 'Typechecked)
p -> (Id -> Id -> [PmGrd]
mkPmLetVar Id
IdP (GhcPass 'Typechecked)
y Id
x [PmGrd] -> [PmGrd] -> [PmGrd]
forall a. [a] -> [a] -> [a]
++) ([PmGrd] -> [PmGrd])
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts Id
IdP (GhcPass 'Typechecked)
y LPat (GhcPass 'Typechecked)
p

  SigPat XSigPat (GhcPass 'Typechecked)
_ LPat (GhcPass 'Typechecked)
p HsPatSigType (NoGhcTc (GhcPass 'Typechecked))
_ty -> FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts Id
x LPat (GhcPass 'Typechecked)
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 HsWrapper
wrapper Pat (GhcPass 'Typechecked)
p Type
_ty)
    | HsWrapper -> Bool
isIdHsWrapper HsWrapper
wrapper                   -> FamInstEnvs
-> Id
-> Pat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translatePat FamInstEnvs
fam_insts Id
x Pat (GhcPass 'Typechecked)
p
    | WpCast TcCoercionR
co <-  HsWrapper
wrapper, TcCoercionR -> Bool
isReflexiveCo TcCoercionR
co -> FamInstEnvs
-> Id
-> Pat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translatePat FamInstEnvs
fam_insts Id
x Pat (GhcPass 'Typechecked)
p
    | Bool
otherwise -> do
        (Id
y, [PmGrd]
grds) <- FamInstEnvs -> Pat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translatePatV FamInstEnvs
fam_insts Pat (GhcPass 'Typechecked)
p
        CoreExpr -> CoreExpr
wrap_rhs_y <- HsWrapper -> DsM (CoreExpr -> CoreExpr)
dsHsWrapper HsWrapper
wrapper
        [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> CoreExpr -> PmGrd
PmLet Id
y (CoreExpr -> CoreExpr
wrap_rhs_y (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x)) PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
grds)

  -- (n + k)  ===>   let b = x >= k, True <- b, let n = x-k
  NPlusKPat XNPlusKPat (GhcPass 'Typechecked)
_pat_ty (L SrcSpan
_ IdP (GhcPass 'Typechecked)
n) Located (HsOverLit (GhcPass 'Typechecked))
k1 HsOverLit (GhcPass 'Typechecked)
k2 SyntaxExpr (GhcPass 'Typechecked)
ge SyntaxExpr (GhcPass 'Typechecked)
minus -> do
    Id
b <- Type -> DsM Id
mkPmId Type
boolTy
    let grd_b :: PmGrd
grd_b = Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
b DataCon
trueDataCon []
    [CoreExpr
ke1, CoreExpr
ke2] <- (HsOverLit (GhcPass 'Typechecked)
 -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr)
-> [HsOverLit (GhcPass 'Typechecked)]
-> IOEnv (Env DsGblEnv DsLclEnv) [CoreExpr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse HsOverLit (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsOverLit [Located (HsOverLit (GhcPass 'Typechecked))
-> HsOverLit (GhcPass 'Typechecked)
forall l e. GenLocated l e -> e
unLoc Located (HsOverLit (GhcPass 'Typechecked))
k1, HsOverLit (GhcPass 'Typechecked)
k2]
    CoreExpr
rhs_b <- SyntaxExpr (GhcPass 'Typechecked)
-> [CoreExpr] -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsSyntaxExpr SyntaxExpr (GhcPass 'Typechecked)
ge    [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x, CoreExpr
ke1]
    CoreExpr
rhs_n <- SyntaxExpr (GhcPass 'Typechecked)
-> [CoreExpr] -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsSyntaxExpr SyntaxExpr (GhcPass 'Typechecked)
minus [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x, CoreExpr
ke2]
    [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Id -> CoreExpr -> PmGrd
PmLet Id
b CoreExpr
rhs_b, PmGrd
grd_b, Id -> CoreExpr -> PmGrd
PmLet Id
IdP (GhcPass 'Typechecked)
n CoreExpr
rhs_n]

  -- (fun -> pat)   ===>   let y = fun x, pat <- y where y is a match var of pat
  ViewPat XViewPat (GhcPass 'Typechecked)
_arg_ty LHsExpr (GhcPass 'Typechecked)
lexpr LPat (GhcPass 'Typechecked)
pat -> do
    (Id
y, [PmGrd]
grds) <- FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts LPat (GhcPass 'Typechecked)
pat
    CoreExpr
fun <- LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr (GhcPass 'Typechecked)
lexpr
    [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a b. (a -> b) -> a -> b
$ Id -> CoreExpr -> PmGrd
PmLet Id
y (CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App CoreExpr
fun (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x)) PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
grds

  -- list
  ListPat (ListPatTc Type
_elem_ty Maybe (Type, SyntaxExpr (GhcPass 'Typechecked))
Nothing) [LPat (GhcPass 'Typechecked)]
ps ->
    FamInstEnvs
-> Id
-> [LPat (GhcPass 'Typechecked)]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateListPat FamInstEnvs
fam_insts Id
x [LPat (GhcPass 'Typechecked)]
ps

  -- overloaded list
  ListPat (ListPatTc Type
elem_ty (Just (Type
pat_ty, SyntaxExpr (GhcPass 'Typechecked)
to_list))) [LPat (GhcPass 'Typechecked)]
pats -> do
    DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
    case Type -> Maybe Type
splitListTyConApp_maybe Type
pat_ty of
      Just Type
_e_ty
        | Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.RebindableSyntax DynFlags
dflags)
        -- Just translate it as a regular ListPat
        -> FamInstEnvs
-> Id
-> [LPat (GhcPass 'Typechecked)]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateListPat FamInstEnvs
fam_insts Id
x [LPat (GhcPass 'Typechecked)]
pats
      Maybe Type
_ -> do
        Id
y <- Type -> DsM Id
mkPmId (Type -> Type
mkListTy Type
elem_ty)
        [PmGrd]
grds <- FamInstEnvs
-> Id
-> [LPat (GhcPass 'Typechecked)]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateListPat FamInstEnvs
fam_insts Id
y [LPat (GhcPass 'Typechecked)]
pats
        CoreExpr
rhs_y <- SyntaxExpr (GhcPass 'Typechecked)
-> [CoreExpr] -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsSyntaxExpr SyntaxExpr (GhcPass 'Typechecked)
to_list [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x]
        [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a b. (a -> b) -> a -> b
$ Id -> CoreExpr -> PmGrd
PmLet Id
y CoreExpr
rhs_y PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
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 :: forall p. Pat p -> Located (ConLikeP p)
pat_con     = L SrcSpan
_ ConLikeP (GhcPass 'Typechecked)
con
         , pat_args :: forall p. Pat p -> HsConPatDetails p
pat_args    = HsConPatDetails (GhcPass 'Typechecked)
ps
         , pat_con_ext :: forall p. Pat p -> XConPat p
pat_con_ext = ConPatTc
           { cpt_arg_tys :: ConPatTc -> [Type]
cpt_arg_tys = [Type]
arg_tys
           , cpt_tvs :: ConPatTc -> [Id]
cpt_tvs     = [Id]
ex_tvs
           , cpt_dicts :: ConPatTc -> [Id]
cpt_dicts   = [Id]
dicts
           }
         } -> do
    FamInstEnvs
-> Id
-> ConLike
-> [Type]
-> [Id]
-> [Id]
-> HsConPatDetails (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateConPatOut FamInstEnvs
fam_insts Id
x ConLike
ConLikeP (GhcPass 'Typechecked)
con [Type]
arg_tys [Id]
ex_tvs [Id]
dicts HsConPatDetails (GhcPass 'Typechecked)
ps

  NPat XNPat (GhcPass 'Typechecked)
ty (L SrcSpan
_ HsOverLit (GhcPass 'Typechecked)
olit) Maybe (SyntaxExpr (GhcPass 'Typechecked))
mb_neg SyntaxExpr (GhcPass 'Typechecked)
_ -> 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.
    DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
    let platform :: Platform
platform = DynFlags -> Platform
targetPlatform DynFlags
dflags
    CoreExpr
core_expr <- case HsOverLit (GhcPass 'Typechecked)
olit of
      OverLit{ ol_val :: forall p. HsOverLit p -> OverLitVal
ol_val = OverLitVal
val, ol_ext :: forall p. HsOverLit p -> XOverLit p
ol_ext = OverLitTc Bool
rebindable Type
_ }
        | Bool -> Bool
not Bool
rebindable
        , Just HsExpr (GhcPass 'Typechecked)
expr <- Platform
-> OverLitVal -> Type -> Maybe (HsExpr (GhcPass 'Typechecked))
shortCutLit Platform
platform OverLitVal
val Type
XNPat (GhcPass 'Typechecked)
ty
        -> HsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsExpr HsExpr (GhcPass 'Typechecked)
expr
      HsOverLit (GhcPass 'Typechecked)
_ -> HsOverLit (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsOverLit HsOverLit (GhcPass 'Typechecked)
olit
    let lit :: PmLit
lit  = String -> Maybe PmLit -> PmLit
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"failed to detect OverLit" (CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
core_expr)
    let lit' :: PmLit
lit' = case Maybe (SyntaxExpr (GhcPass 'Typechecked))
mb_neg of
          Just SyntaxExpr (GhcPass 'Typechecked)
_  -> String -> Maybe PmLit -> PmLit
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"failed to negate lit" (PmLit -> Maybe PmLit
negatePmLit PmLit
lit)
          Maybe (SyntaxExpr (GhcPass 'Typechecked))
Nothing -> PmLit
lit
    Id -> PmLit -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkPmLitGrds Id
x PmLit
lit'

  LitPat XLitPat (GhcPass 'Typechecked)
_ HsLit (GhcPass 'Typechecked)
lit -> do
    CoreExpr
core_expr <- HsLit GhcRn -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLit (HsLit (GhcPass 'Typechecked) -> HsLit GhcRn
forall (p1 :: Pass) (p2 :: Pass).
HsLit (GhcPass p1) -> HsLit (GhcPass p2)
convertLit HsLit (GhcPass 'Typechecked)
lit)
    let lit :: PmLit
lit = String -> Maybe PmLit -> PmLit
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"failed to detect Lit" (CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
core_expr)
    Id -> PmLit -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkPmLitGrds Id
x PmLit
lit

  TuplePat XTuplePat (GhcPass 'Typechecked)
_tys [LPat (GhcPass 'Typechecked)]
pats Boxity
boxity -> do
    ([Id]
vars, [[PmGrd]]
grdss) <- (Located (Pat (GhcPass 'Typechecked)) -> DsM (Id, [PmGrd]))
-> [Located (Pat (GhcPass 'Typechecked))]
-> IOEnv (Env DsGblEnv DsLclEnv) ([Id], [[PmGrd]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts) [Located (Pat (GhcPass 'Typechecked))]
[LPat (GhcPass 'Typechecked)]
pats
    let tuple_con :: DataCon
tuple_con = Boxity -> Int -> DataCon
tupleDataCon Boxity
boxity ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
vars)
    [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a b. (a -> b) -> a -> b
$ Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
x DataCon
tuple_con [Id]
vars PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [[PmGrd]] -> [PmGrd]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PmGrd]]
grdss

  SumPat XSumPat (GhcPass 'Typechecked)
_ty LPat (GhcPass 'Typechecked)
p Int
alt Int
arity -> do
    (Id
y, [PmGrd]
grds) <- FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts LPat (GhcPass 'Typechecked)
p
    let sum_con :: DataCon
sum_con = Int -> Int -> DataCon
sumDataCon Int
alt Int
arity
    -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
    [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a b. (a -> b) -> a -> b
$ Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
x DataCon
sum_con [Id
y] PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
grds

  -- --------------------------------------------------------------------------
  -- Not supposed to happen
  SplicePat {} -> String -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a. String -> a
panic String
"Check.translatePat: SplicePat"

-- | 'translatePat', but also select and return a new match var.
translatePatV :: FamInstEnvs -> Pat GhcTc -> DsM (Id, GrdVec)
translatePatV :: FamInstEnvs -> Pat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translatePatV FamInstEnvs
fam_insts Pat (GhcPass 'Typechecked)
pat = do
  Id
x <- Type -> Pat (GhcPass 'Typechecked) -> DsM Id
selectMatchVar Type
Many Pat (GhcPass 'Typechecked)
pat
  [PmGrd]
grds <- FamInstEnvs
-> Id
-> Pat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translatePat FamInstEnvs
fam_insts Id
x Pat (GhcPass 'Typechecked)
pat
  (Id, [PmGrd]) -> DsM (Id, [PmGrd])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
x, [PmGrd]
grds)

translateLPat :: FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat :: FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts Id
x = FamInstEnvs
-> Id
-> Pat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translatePat FamInstEnvs
fam_insts Id
x (Pat (GhcPass 'Typechecked)
 -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> (Located (Pat (GhcPass 'Typechecked))
    -> Pat (GhcPass 'Typechecked))
-> Located (Pat (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (Pat (GhcPass 'Typechecked)) -> Pat (GhcPass 'Typechecked)
forall l e. GenLocated l e -> e
unLoc

-- | 'translateLPat', but also select and return a new match var.
translateLPatV :: FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV :: FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts = FamInstEnvs -> Pat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translatePatV FamInstEnvs
fam_insts (Pat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd]))
-> (Located (Pat (GhcPass 'Typechecked))
    -> Pat (GhcPass 'Typechecked))
-> Located (Pat (GhcPass 'Typechecked))
-> DsM (Id, [PmGrd])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (Pat (GhcPass 'Typechecked)) -> Pat (GhcPass 'Typechecked)
forall l e. GenLocated l e -> e
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 :: FamInstEnvs
-> Id
-> [LPat (GhcPass 'Typechecked)]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateListPat FamInstEnvs
fam_insts Id
x [LPat (GhcPass 'Typechecked)]
pats = do
  [(Id, [PmGrd])]
vars_and_grdss <- (Located (Pat (GhcPass 'Typechecked)) -> DsM (Id, [PmGrd]))
-> [Located (Pat (GhcPass 'Typechecked))]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Id, [PmGrd])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts) [Located (Pat (GhcPass 'Typechecked))]
[LPat (GhcPass 'Typechecked)]
pats
  Id -> [(Id, [PmGrd])] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
mkListGrds Id
x [(Id, [PmGrd])]
vars_and_grdss

-- | Translate a constructor pattern
translateConPatOut :: FamInstEnvs -> Id -> ConLike -> [Type] -> [TyVar]
                   -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec
translateConPatOut :: FamInstEnvs
-> Id
-> ConLike
-> [Type]
-> [Id]
-> [Id]
-> HsConPatDetails (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateConPatOut FamInstEnvs
fam_insts Id
x ConLike
con [Type]
univ_tys [Id]
ex_tvs [Id]
dicts = \case
    PrefixCon [LPat (GhcPass 'Typechecked)]
ps                 -> [(Int, Located (Pat (GhcPass 'Typechecked)))]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
go_field_pats ([Int]
-> [Located (Pat (GhcPass 'Typechecked))]
-> [(Int, Located (Pat (GhcPass 'Typechecked)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Located (Pat (GhcPass 'Typechecked))]
[LPat (GhcPass 'Typechecked)]
ps)
    InfixCon  LPat (GhcPass 'Typechecked)
p1 LPat (GhcPass 'Typechecked)
p2              -> [(Int, Located (Pat (GhcPass 'Typechecked)))]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
go_field_pats ([Int]
-> [Located (Pat (GhcPass 'Typechecked))]
-> [(Int, Located (Pat (GhcPass 'Typechecked)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Located (Pat (GhcPass 'Typechecked))
LPat (GhcPass 'Typechecked)
p1,Located (Pat (GhcPass 'Typechecked))
LPat (GhcPass 'Typechecked)
p2])
    RecCon    (HsRecFields [LHsRecField (GhcPass 'Typechecked) (LPat (GhcPass 'Typechecked))]
fs Maybe (Located Int)
_) -> [(Int, Located (Pat (GhcPass 'Typechecked)))]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
go_field_pats ([GenLocated
   SrcSpan
   (HsRecField
      (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))]
-> [(Int, Located (Pat (GhcPass 'Typechecked)))]
rec_field_ps [GenLocated
   SrcSpan
   (HsRecField
      (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))]
[LHsRecField (GhcPass 'Typechecked) (LPat (GhcPass 'Typechecked))]
fs)
  where
    -- The actual argument types (instantiated)
    arg_tys :: [Type]
arg_tys     = (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing ([Scaled Type] -> [Type]) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ ConLike -> [Type] -> [Scaled Type]
conLikeInstOrigArgTys ConLike
con ([Type]
univ_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Id] -> [Type]
mkTyVarTys [Id]
ex_tvs)

    -- Extract record field patterns tagged by field index from a list of
    -- LHsRecField
    rec_field_ps :: [GenLocated
   SrcSpan
   (HsRecField
      (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))]
-> [(Int, Located (Pat (GhcPass 'Typechecked)))]
rec_field_ps [GenLocated
   SrcSpan
   (HsRecField
      (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))]
fs = (GenLocated
   SrcSpan
   (HsRecField
      (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))
 -> (Int, Located (Pat (GhcPass 'Typechecked))))
-> [GenLocated
      SrcSpan
      (HsRecField
         (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))]
-> [(Int, Located (Pat (GhcPass 'Typechecked)))]
forall a b. (a -> b) -> [a] -> [b]
map (HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
-> (Int, Located (Pat (GhcPass 'Typechecked)))
tagged_pat (HsRecField
   (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
 -> (Int, Located (Pat (GhcPass 'Typechecked))))
-> (GenLocated
      SrcSpan
      (HsRecField
         (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))
    -> HsRecField
         (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))
-> GenLocated
     SrcSpan
     (HsRecField
        (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))
-> (Int, Located (Pat (GhcPass 'Typechecked)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenLocated
  SrcSpan
  (HsRecField
     (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))
-> HsRecField
     (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
forall l e. GenLocated l e -> e
unLoc) [GenLocated
   SrcSpan
   (HsRecField
      (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked))))]
fs
      where
        tagged_pat :: HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
-> (Int, Located (Pat (GhcPass 'Typechecked)))
tagged_pat HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
f = (Name -> Int
lbl_to_index (Located Id -> Name
forall a. NamedThing a => a -> Name
getName (HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
-> Located Id
forall arg. HsRecField (GhcPass 'Typechecked) arg -> Located Id
hsRecFieldId HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
f)), HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
-> Located (Pat (GhcPass 'Typechecked))
forall id arg. HsRecField' id arg -> arg
hsRecFieldArg HsRecField
  (GhcPass 'Typechecked) (Located (Pat (GhcPass 'Typechecked)))
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 :: [Name]
orig_lbls        = (FieldLbl Name -> Name) -> [FieldLbl Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FieldLbl Name -> Name
forall a. FieldLbl a -> a
flSelector ([FieldLbl Name] -> [Name]) -> [FieldLbl Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ ConLike -> [FieldLbl Name]
conLikeFieldLabels ConLike
con
        lbl_to_index :: Name -> Int
lbl_to_index Name
lbl = String -> Maybe Int -> Int
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"lbl_to_index" (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Name
lbl [Name]
orig_lbls

    go_field_pats :: [(Int, Located (Pat (GhcPass 'Typechecked)))]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
go_field_pats [(Int, Located (Pat (GhcPass 'Typechecked)))]
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 :: (Int, Located (Pat (GhcPass 'Typechecked)))
-> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), [PmGrd])
trans_pat (Int
n, Located (Pat (GhcPass 'Typechecked))
pat) = do
            (Id
var, [PmGrd]
pvec) <- FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts Located (Pat (GhcPass 'Typechecked))
LPat (GhcPass 'Typechecked)
pat
            ((Int, Id), [PmGrd])
-> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), [PmGrd])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Int
n, Id
var), [PmGrd]
pvec)
      ([(Int, Id)]
tagged_vars, [[PmGrd]]
arg_grdss) <- ((Int, Located (Pat (GhcPass 'Typechecked)))
 -> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), [PmGrd]))
-> [(Int, Located (Pat (GhcPass 'Typechecked)))]
-> IOEnv (Env DsGblEnv DsLclEnv) ([(Int, Id)], [[PmGrd]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Int, Located (Pat (GhcPass 'Typechecked)))
-> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), [PmGrd])
trans_pat [(Int, Located (Pat (GhcPass 'Typechecked)))]
tagged_pats

      let get_pat_id :: Int -> Type -> DsM Id
get_pat_id Int
n Type
ty = case Int -> [(Int, Id)] -> Maybe Id
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
n [(Int, Id)]
tagged_vars of
            Just Id
var -> Id -> DsM Id
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
var
            Maybe Id
Nothing  -> Type -> DsM Id
mkPmId Type
ty

      -- 1. the constructor pattern match itself
      [Id]
arg_ids <- (Int -> Type -> DsM Id)
-> [Int] -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> Type -> DsM Id
get_pat_id [Int
0..] [Type]
arg_tys
      let con_grd :: PmGrd
con_grd = Id -> PmAltCon -> [Id] -> [Id] -> [Id] -> PmGrd
PmCon Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
con) [Id]
ex_tvs [Id]
dicts [Id]
arg_ids

      -- 2. bang strict fields
      let arg_is_banged :: [Bool]
arg_is_banged = (HsImplBang -> Bool) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map HsImplBang -> Bool
isBanged ([HsImplBang] -> [Bool]) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> a -> b
$ ConLike -> [HsImplBang]
conLikeImplBangs ConLike
con
          bang_grds :: [PmGrd]
bang_grds     = (Id -> PmGrd) -> [Id] -> [PmGrd]
forall a b. (a -> b) -> [a] -> [b]
map Id -> PmGrd
PmBang   ([Id] -> [PmGrd]) -> [Id] -> [PmGrd]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Id] -> [Id]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
arg_is_banged [Id]
arg_ids

      -- 3. guards from field selector patterns
      let arg_grds :: [PmGrd]
arg_grds = [[PmGrd]] -> [PmGrd]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PmGrd]]
arg_grdss

      -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
      --
      -- Store the guards in exactly that order
      --      1.         2.           3.
      [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PmGrd
con_grd PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
bang_grds [PmGrd] -> [PmGrd] -> [PmGrd]
forall a. [a] -> [a] -> [a]
++ [PmGrd]
arg_grds)

mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
mkGrdTreeRhs :: RhsInfo -> [PmGrd] -> GrdTree
mkGrdTreeRhs RhsInfo
sdoc = (PmGrd -> GrdTree -> GrdTree) -> GrdTree -> [PmGrd] -> GrdTree
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PmGrd -> GrdTree -> GrdTree
Guard (RhsInfo -> GrdTree
Rhs RhsInfo
sdoc)

mkGrdTreeMany :: GrdVec -> [GrdTree] -> GrdTree
mkGrdTreeMany :: [PmGrd] -> [GrdTree] -> GrdTree
mkGrdTreeMany [PmGrd]
_    []    = GrdTree
Empty
mkGrdTreeMany [PmGrd]
grds [GrdTree]
trees = (PmGrd -> GrdTree -> GrdTree) -> GrdTree -> [PmGrd] -> GrdTree
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PmGrd -> GrdTree -> GrdTree
Guard ((GrdTree -> GrdTree -> GrdTree) -> [GrdTree] -> GrdTree
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 GrdTree -> GrdTree -> GrdTree
Sequence [GrdTree]
trees) [PmGrd]
grds

-- Translate a single match
translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc)
               -> DsM GrdTree
translateMatch :: FamInstEnvs
-> [Id]
-> LMatch (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
translateMatch FamInstEnvs
fam_insts [Id]
vars (L SrcSpan
match_loc (Match { m_pats :: forall p body. Match p body -> [LPat p]
m_pats = [LPat (GhcPass 'Typechecked)]
pats, m_grhss :: forall p body. Match p body -> GRHSs p body
m_grhss = GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
grhss })) = do
  [PmGrd]
pats'   <- [[PmGrd]] -> [PmGrd]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PmGrd]] -> [PmGrd])
-> IOEnv (Env DsGblEnv DsLclEnv) [[PmGrd]]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id
 -> Located (Pat (GhcPass 'Typechecked))
 -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [Id]
-> [Located (Pat (GhcPass 'Typechecked))]
-> IOEnv (Env DsGblEnv DsLclEnv) [[PmGrd]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts) [Id]
vars [Located (Pat (GhcPass 'Typechecked))]
[LPat (GhcPass 'Typechecked)]
pats
  [GrdTree]
grhss' <- (LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
 -> IOEnv (Env DsGblEnv DsLclEnv) GrdTree)
-> [LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdTree]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs
-> SrcSpan
-> [LPat (GhcPass 'Typechecked)]
-> LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
translateLGRHS FamInstEnvs
fam_insts SrcSpan
match_loc [LPat (GhcPass 'Typechecked)]
pats) (GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> [LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))]
forall p body. GRHSs p body -> [LGRHS p body]
grhssGRHSs GRHSs (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
grhss)
  -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss, ppr grhss'])
  GrdTree -> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
forall (m :: * -> *) a. Monad m => a -> m a
return ([PmGrd] -> [GrdTree] -> GrdTree
mkGrdTreeMany [PmGrd]
pats' [GrdTree]
grhss')

-- -----------------------------------------------------------------------
-- * Transform source guards (GuardStmt Id) to simpler PmGrds

-- | Translate a guarded right-hand side to a single 'GrdTree'
translateLGRHS :: FamInstEnvs -> SrcSpan -> [LPat GhcTc] -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
translateLGRHS :: FamInstEnvs
-> SrcSpan
-> [LPat (GhcPass 'Typechecked)]
-> LGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
translateLGRHS FamInstEnvs
fam_insts SrcSpan
match_loc [LPat (GhcPass 'Typechecked)]
pats (L SrcSpan
_loc (GRHS XCGRHS (GhcPass 'Typechecked) (LHsExpr (GhcPass 'Typechecked))
_ [GuardLStmt (GhcPass 'Typechecked)]
gs LHsExpr (GhcPass 'Typechecked)
_)) =
  -- _loc apparently points to the match separator that comes after the guards..
  RhsInfo -> [PmGrd] -> GrdTree
mkGrdTreeRhs RhsInfo
loc_sdoc ([PmGrd] -> GrdTree)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
-> IOEnv (Env DsGblEnv DsLclEnv) GrdTree
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GuardLStmt (GhcPass 'Typechecked)
 -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [GuardLStmt (GhcPass 'Typechecked)]
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (FamInstEnvs
-> StmtLR
     (GhcPass 'Typechecked)
     (GhcPass 'Typechecked)
     (LHsExpr (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateGuard FamInstEnvs
fam_insts (StmtLR
   (GhcPass 'Typechecked)
   (GhcPass 'Typechecked)
   (LHsExpr (GhcPass 'Typechecked))
 -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> (GuardLStmt (GhcPass 'Typechecked)
    -> StmtLR
         (GhcPass 'Typechecked)
         (GhcPass 'Typechecked)
         (LHsExpr (GhcPass 'Typechecked)))
-> GuardLStmt (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GuardLStmt (GhcPass 'Typechecked)
-> StmtLR
     (GhcPass 'Typechecked)
     (GhcPass 'Typechecked)
     (LHsExpr (GhcPass 'Typechecked))
forall l e. GenLocated l e -> e
unLoc) [GuardLStmt (GhcPass 'Typechecked)]
gs
    where
      loc_sdoc :: RhsInfo
loc_sdoc
        | [GuardLStmt (GhcPass 'Typechecked)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GuardLStmt (GhcPass 'Typechecked)]
gs   = SrcSpan -> SDoc -> RhsInfo
forall l e. l -> e -> GenLocated l e
L SrcSpan
match_loc ([SDoc] -> SDoc
sep ((Located (Pat (GhcPass 'Typechecked)) -> SDoc)
-> [Located (Pat (GhcPass 'Typechecked))] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Located (Pat (GhcPass 'Typechecked)) -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Located (Pat (GhcPass 'Typechecked))]
[LPat (GhcPass 'Typechecked)]
pats))
        | Bool
otherwise = SrcSpan -> SDoc -> RhsInfo
forall l e. l -> e -> GenLocated l e
L SrcSpan
grd_loc   ([SDoc] -> SDoc
sep ((Located (Pat (GhcPass 'Typechecked)) -> SDoc)
-> [Located (Pat (GhcPass 'Typechecked))] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Located (Pat (GhcPass 'Typechecked)) -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Located (Pat (GhcPass 'Typechecked))]
[LPat (GhcPass 'Typechecked)]
pats) SDoc -> SDoc -> SDoc
<+> SDoc
vbar SDoc -> SDoc -> SDoc
<+> [GuardLStmt (GhcPass 'Typechecked)] -> SDoc
forall a. Outputable a => [a] -> SDoc
interpp'SP [GuardLStmt (GhcPass 'Typechecked)]
gs)
      L SrcSpan
grd_loc StmtLR
  (GhcPass 'Typechecked)
  (GhcPass 'Typechecked)
  (LHsExpr (GhcPass 'Typechecked))
_ = [GuardLStmt (GhcPass 'Typechecked)]
-> GuardLStmt (GhcPass 'Typechecked)
forall a. [a] -> a
head [GuardLStmt (GhcPass 'Typechecked)]
gs

-- | Translate a guard statement to a 'GrdVec'
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
translateGuard :: FamInstEnvs
-> StmtLR
     (GhcPass 'Typechecked)
     (GhcPass 'Typechecked)
     (LHsExpr (GhcPass 'Typechecked))
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateGuard FamInstEnvs
fam_insts StmtLR
  (GhcPass 'Typechecked)
  (GhcPass 'Typechecked)
  (LHsExpr (GhcPass 'Typechecked))
guard = case StmtLR
  (GhcPass 'Typechecked)
  (GhcPass 'Typechecked)
  (LHsExpr (GhcPass 'Typechecked))
guard of
  BodyStmt XBodyStmt
  (GhcPass 'Typechecked)
  (GhcPass 'Typechecked)
  (LHsExpr (GhcPass 'Typechecked))
_   LHsExpr (GhcPass 'Typechecked)
e SyntaxExpr (GhcPass 'Typechecked)
_ SyntaxExpr (GhcPass 'Typechecked)
_ -> LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateBoolGuard LHsExpr (GhcPass 'Typechecked)
e
  LetStmt  XLetStmt
  (GhcPass 'Typechecked)
  (GhcPass 'Typechecked)
  (LHsExpr (GhcPass 'Typechecked))
_   LHsLocalBinds (GhcPass 'Typechecked)
binds -> HsLocalBinds (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLet (LHsLocalBinds (GhcPass 'Typechecked)
-> HsLocalBinds (GhcPass 'Typechecked)
forall l e. GenLocated l e -> e
unLoc LHsLocalBinds (GhcPass 'Typechecked)
binds)
  BindStmt XBindStmt
  (GhcPass 'Typechecked)
  (GhcPass 'Typechecked)
  (LHsExpr (GhcPass 'Typechecked))
_ LPat (GhcPass 'Typechecked)
p LHsExpr (GhcPass 'Typechecked)
e     -> FamInstEnvs
-> LPat (GhcPass 'Typechecked)
-> LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateBind FamInstEnvs
fam_insts LPat (GhcPass 'Typechecked)
p LHsExpr (GhcPass 'Typechecked)
e
  LastStmt        {} -> String -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a. String -> a
panic String
"translateGuard LastStmt"
  ParStmt         {} -> String -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a. String -> a
panic String
"translateGuard ParStmt"
  TransStmt       {} -> String -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a. String -> a
panic String
"translateGuard TransStmt"
  RecStmt         {} -> String -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a. String -> a
panic String
"translateGuard RecStmt"
  ApplicativeStmt {} -> String -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a. String -> a
panic String
"translateGuard ApplicativeLastStmt"

-- | Translate let-bindings
translateLet :: HsLocalBinds GhcTc -> DsM GrdVec
translateLet :: HsLocalBinds (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLet HsLocalBinds (GhcPass 'Typechecked)
_binds = [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Translate a pattern guard
--   @pat <- e ==>  let x = e;  <guards for pat <- x>@
translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
translateBind :: FamInstEnvs
-> LPat (GhcPass 'Typechecked)
-> LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateBind FamInstEnvs
fam_insts LPat (GhcPass 'Typechecked)
p LHsExpr (GhcPass 'Typechecked)
e = LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr (GhcPass 'Typechecked)
e IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
-> (CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Var Id
y
    | Maybe DataCon
Nothing <- Id -> Maybe DataCon
isDataConId_maybe Id
y
    -- RHS is a variable, so that will allow us to omit the let
    -> FamInstEnvs
-> Id
-> LPat (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateLPat FamInstEnvs
fam_insts Id
y LPat (GhcPass 'Typechecked)
p
  CoreExpr
rhs -> do
    (Id
x, [PmGrd]
grds) <- FamInstEnvs -> LPat (GhcPass 'Typechecked) -> DsM (Id, [PmGrd])
translateLPatV FamInstEnvs
fam_insts LPat (GhcPass 'Typechecked)
p
    [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> CoreExpr -> PmGrd
PmLet Id
x CoreExpr
rhs PmGrd -> [PmGrd] -> [PmGrd]
forall a. a -> [a] -> [a]
: [PmGrd]
grds)

-- | Translate a boolean guard
--   @e ==>  let x = e; True <- x@
translateBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
translateBoolGuard :: LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
translateBoolGuard LHsExpr (GhcPass 'Typechecked)
e
  | Maybe (CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr) -> Bool
forall a. Maybe a -> Bool
isJust (LHsExpr (GhcPass 'Typechecked)
-> Maybe (CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr)
isTrueLHsExpr LHsExpr (GhcPass 'Typechecked)
e) = [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (m :: * -> *) a. Monad m => a -> m a
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
  | Bool
otherwise = LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr (GhcPass 'Typechecked)
e IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
-> (CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Var Id
y
        | Maybe DataCon
Nothing <- Id -> Maybe DataCon
isDataConId_maybe Id
y
        -- Omit the let by matching on y
        -> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
y DataCon
trueDataCon []]
      CoreExpr
rhs -> do
        Id
x <- Type -> DsM Id
mkPmId Type
boolTy
        [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd])
-> [PmGrd] -> IOEnv (Env DsGblEnv DsLclEnv) [PmGrd]
forall a b. (a -> b) -> a -> b
$ [Id -> CoreExpr -> PmGrd
PmLet Id
x CoreExpr
rhs, Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
x DataCon
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 :: Int -> Deltas -> Deltas -> (Precision, Deltas)
throttle Int
limit old :: Deltas
old@(MkDeltas Bag Delta
old_ds) new :: Deltas
new@(MkDeltas Bag Delta
new_ds)
  --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
  | Bag Delta -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Delta
new_ds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
limit (Bag Delta -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Delta
old_ds) = (Precision
Approximate, Deltas
old)
  | Bool
otherwise                                 = (Precision
Precise,     Deltas
new)

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

-- | Makes sure that we only wrap a single 'MayDiverge' around an
-- 'AnnotatedTree', purely for esthetic reasons.
mayDiverge :: AnnotatedTree -> AnnotatedTree
mayDiverge :: AnnotatedTree -> AnnotatedTree
mayDiverge a :: AnnotatedTree
a@(MayDiverge AnnotatedTree
_) = AnnotatedTree
a
mayDiverge AnnotatedTree
a                = AnnotatedTree -> AnnotatedTree
MayDiverge AnnotatedTree
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 'redundantAndInaccessibleRhss' for
--     presenting redundant and proper innaccessible RHSs to the user.
checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
-- RHS: Check that it covers something and wrap Inaccessible if not
checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' (Rhs RhsInfo
sdoc) Deltas
deltas = do
  Bool
is_covered <- Deltas -> DsM Bool
isInhabited Deltas
deltas
  let clauses :: AnnotatedTree
clauses
        | Bool
is_covered = Deltas -> RhsInfo -> AnnotatedTree
AccessibleRhs Deltas
deltas RhsInfo
sdoc
        | Bool
otherwise  = RhsInfo -> AnnotatedTree
InaccessibleRhs RhsInfo
sdoc
  CheckResult -> DsM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: AnnotatedTree -> Deltas -> Precision -> CheckResult
CheckResult
    { cr_clauses :: AnnotatedTree
cr_clauses = AnnotatedTree
clauses
    , cr_uncov :: Deltas
cr_uncov   = Bag Delta -> Deltas
MkDeltas Bag Delta
forall a. Bag a
emptyBag
    , cr_approx :: Precision
cr_approx  = Precision
Precise }
-- let x = e: Refine with x ~ e
checkGrdTree' (Guard (PmLet Id
x CoreExpr
e) GrdTree
tree) Deltas
deltas = do
  Deltas
deltas' <- Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
deltas (Id -> CoreExpr -> PmCt
PmCoreCt Id
x CoreExpr
e)
  GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' GrdTree
tree Deltas
deltas'
-- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
checkGrdTree' (Guard (PmBang Id
x) GrdTree
tree) Deltas
deltas = do
  Bool
has_diverged <- Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
deltas (Id -> PmCt
PmBotCt Id
x) DsM Deltas -> (Deltas -> DsM Bool) -> DsM Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Deltas -> DsM Bool
isInhabited
  Deltas
deltas' <- Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
deltas (Id -> PmCt
PmNotBotCt Id
x)
  CheckResult
res <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' GrdTree
tree Deltas
deltas'
  CheckResult -> DsM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult
res{ cr_clauses :: AnnotatedTree
cr_clauses = Bool
-> (AnnotatedTree -> AnnotatedTree)
-> AnnotatedTree
-> AnnotatedTree
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
has_diverged AnnotatedTree -> AnnotatedTree
mayDiverge (CheckResult -> AnnotatedTree
cr_clauses CheckResult
res) }
-- Con: Diverge on x ~ ⊥, fall through on x /~ K and refine with x ~ K ys
--      and type info
checkGrdTree' (Guard (PmCon Id
x PmAltCon
con [Id]
tvs [Id]
dicts [Id]
args) GrdTree
tree) Deltas
deltas = do
  Bool
has_diverged <-
    if PmAltCon -> Bool
conMatchForces PmAltCon
con
      then Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
deltas (Id -> PmCt
PmBotCt Id
x) DsM Deltas -> (Deltas -> DsM Bool) -> DsM Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Deltas -> DsM Bool
isInhabited
      else Bool -> DsM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  Deltas
unc_this <- Deltas -> PmCt -> DsM Deltas
addPmCtDeltas Deltas
deltas (Id -> PmAltCon -> PmCt
PmNotConCt Id
x PmAltCon
con)
  Deltas
deltas' <- Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas Deltas
deltas (PmCts -> DsM Deltas) -> PmCts -> DsM Deltas
forall a b. (a -> b) -> a -> b
$
    [PmCt] -> PmCts
forall a. [a] -> Bag a
listToBag (Type -> PmCt
PmTyCt (Type -> PmCt) -> (Id -> Type) -> Id -> PmCt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
evVarPred (Id -> PmCt) -> [Id] -> [PmCt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Id]
dicts) PmCts -> PmCt -> PmCts
forall a. Bag a -> a -> Bag a
`snocBag` Id -> PmAltCon -> [Id] -> [Id] -> PmCt
PmConCt Id
x PmAltCon
con [Id]
tvs [Id]
args
  CheckResult AnnotatedTree
tree' Deltas
unc_inner Precision
prec <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' GrdTree
tree Deltas
deltas'
  Int
limit <- DynFlags -> Int
maxPmCheckModels (DynFlags -> Int)
-> IOEnv (Env DsGblEnv DsLclEnv) DynFlags
-> IOEnv (Env DsGblEnv DsLclEnv) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let (Precision
prec', Deltas
unc') = Int -> Deltas -> Deltas -> (Precision, Deltas)
throttle Int
limit Deltas
deltas (Deltas
unc_this Deltas -> Deltas -> Deltas
forall a. Semigroup a => a -> a -> a
Semi.<> Deltas
unc_inner)
  CheckResult -> DsM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: AnnotatedTree -> Deltas -> Precision -> CheckResult
CheckResult
    { cr_clauses :: AnnotatedTree
cr_clauses = Bool
-> (AnnotatedTree -> AnnotatedTree)
-> AnnotatedTree
-> AnnotatedTree
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
has_diverged AnnotatedTree -> AnnotatedTree
mayDiverge AnnotatedTree
tree'
    , cr_uncov :: Deltas
cr_uncov = Deltas
unc'
    , cr_approx :: Precision
cr_approx = Precision
prec Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> Precision
prec' }
-- Sequence: Thread residual uncovered sets from equation to equation
checkGrdTree' (Sequence GrdTree
l GrdTree
r) Deltas
unc_0 = do
  CheckResult AnnotatedTree
l' Deltas
unc_1 Precision
prec_l <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' GrdTree
l Deltas
unc_0
  CheckResult AnnotatedTree
r' Deltas
unc_2 Precision
prec_r <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' GrdTree
r Deltas
unc_1
  CheckResult -> DsM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: AnnotatedTree -> Deltas -> Precision -> CheckResult
CheckResult
    { cr_clauses :: AnnotatedTree
cr_clauses = AnnotatedTree -> AnnotatedTree -> AnnotatedTree
SequenceAnn AnnotatedTree
l' AnnotatedTree
r'
    , cr_uncov :: Deltas
cr_uncov = Deltas
unc_2
    , cr_approx :: Precision
cr_approx = Precision
prec_l Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> Precision
prec_r }
-- Empty: Fall through for all values
checkGrdTree' GrdTree
Empty Deltas
unc = do
  CheckResult -> DsM CheckResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult :: AnnotatedTree -> Deltas -> Precision -> CheckResult
CheckResult
    { cr_clauses :: AnnotatedTree
cr_clauses = AnnotatedTree
EmptyAnn
    , cr_uncov :: Deltas
cr_uncov = Deltas
unc
    , cr_approx :: Precision
cr_approx = Precision
Precise }

-- | Print diagnostic info and actually call 'checkGrdTree''.
checkGrdTree :: GrdTree -> Deltas -> DsM CheckResult
checkGrdTree :: GrdTree -> Deltas -> DsM CheckResult
checkGrdTree GrdTree
guards Deltas
deltas = do
  String -> SDoc -> DsM ()
tracePm String
"checkGrdTree {" (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat [ GrdTree -> SDoc
forall a. Outputable a => a -> SDoc
ppr GrdTree
guards
                                  , Deltas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Deltas
deltas ]
  CheckResult
res <- GrdTree -> Deltas -> DsM CheckResult
checkGrdTree' GrdTree
guards Deltas
deltas
  String -> SDoc -> DsM ()
tracePm String
"checkGrdTree }:" (CheckResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr CheckResult
res) -- braces are easier to match by tooling
  CheckResult -> DsM CheckResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckResult
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 `addScrutTmCs' 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 :: forall a. (Deltas -> DsM Deltas) -> DsM a -> DsM a
locallyExtendPmDelta Deltas -> DsM Deltas
ext DsM a
k = do
  Deltas
deltas <- DsM Deltas
getPmDeltas
  Deltas
deltas' <- DsM Deltas -> DsM Deltas
forall env a. IOEnv env a -> IOEnv env a
unsafeInterleaveM (DsM Deltas -> DsM Deltas) -> DsM Deltas -> DsM Deltas
forall a b. (a -> b) -> a -> b
$ do
    Deltas
deltas' <- Deltas -> DsM Deltas
ext Deltas
deltas
    Bool
inh <- Deltas -> DsM Bool
isInhabited Deltas
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 Bool
inh
      then Deltas -> DsM Deltas
forall (f :: * -> *) a. Applicative f => a -> f a
pure Deltas
deltas'
      else Deltas -> DsM Deltas
forall (f :: * -> *) a. Applicative f => a -> f a
pure Deltas
deltas
  Deltas -> DsM a -> DsM a
forall a. Deltas -> DsM a -> DsM a
updPmDeltas Deltas
deltas' DsM a
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 :: forall a. Origin -> Bag Id -> DsM a -> DsM a
addTyCsDs Origin
origin Bag Id
ev_vars DsM a
m = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  Bool -> (DsM a -> DsM a) -> DsM a -> DsM a
forall a. Bool -> (a -> a) -> a -> a
applyWhen (DynFlags -> Origin -> Bool
needToRunPmCheck DynFlags
dflags Origin
origin)
            ((Deltas -> DsM Deltas) -> DsM a -> DsM a
forall a. (Deltas -> DsM Deltas) -> DsM a -> DsM a
locallyExtendPmDelta (\Deltas
deltas -> Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas Deltas
deltas (Type -> PmCt
PmTyCt (Type -> PmCt) -> (Id -> Type) -> Id -> PmCt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
evVarPred (Id -> PmCt) -> Bag Id -> PmCts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bag Id
ev_vars)))
            DsM a
m

-- | Add equalities for the 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.
addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
addScrutTmCs :: forall a.
Maybe (LHsExpr (GhcPass 'Typechecked)) -> [Id] -> DsM a -> DsM a
addScrutTmCs Maybe (LHsExpr (GhcPass 'Typechecked))
Nothing    [Id]
_   DsM a
k = DsM a
k
addScrutTmCs (Just LHsExpr (GhcPass 'Typechecked)
scr) [Id
x] DsM a
k = do
  CoreExpr
scr_e <- LHsExpr (GhcPass 'Typechecked)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr (GhcPass 'Typechecked)
scr
  (Deltas -> DsM Deltas) -> DsM a -> DsM a
forall a. (Deltas -> DsM Deltas) -> DsM a -> DsM a
locallyExtendPmDelta (\Deltas
deltas -> Deltas -> PmCts -> DsM Deltas
addPmCtsDeltas Deltas
deltas (PmCt -> PmCts
forall a. a -> Bag a
unitBag (Id -> CoreExpr -> PmCt
PmCoreCt Id
x CoreExpr
scr_e))) DsM a
k
addScrutTmCs Maybe (LHsExpr (GhcPass 'Typechecked))
_   [Id]
_   DsM a
_ = String -> DsM a
forall a. String -> a
panic String
"addScrutTmCs: HsCase with more than one case binder"

{-
%************************************************************************
%*                                                                      *
      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 :: forall id. DynFlags -> Origin -> HsMatchContext id -> Bool
isMatchContextPmChecked DynFlags
dflags Origin
origin HsMatchContext id
kind
  | Origin -> Bool
isGenerated Origin
origin
  = Bool
False
  | Bool
otherwise
  = WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnOverlappingPatterns DynFlags
dflags Bool -> Bool -> Bool
|| DynFlags -> HsMatchContext id -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext id
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 :: DynFlags -> Origin -> Bool
needToRunPmCheck DynFlags
dflags Origin
origin
  | Origin -> Bool
isGenerated Origin
origin
  = Bool
False
  | Bool
otherwise
  = [WarningFlag] -> Bool
forall a. [a] -> Bool
notNull ((WarningFlag -> Bool) -> [WarningFlag] -> [WarningFlag]
forall a. (a -> Bool) -> [a] -> [a]
filter (WarningFlag -> DynFlags -> Bool
`wopt` DynFlags
dflags) [WarningFlag]
allPmCheckWarnings)

redundantAndInaccessibleRhss :: AnnotatedTree -> ([RhsInfo], [RhsInfo])
redundantAndInaccessibleRhss :: AnnotatedTree -> ([RhsInfo], [RhsInfo])
redundantAndInaccessibleRhss AnnotatedTree
tree = (OrdList RhsInfo -> [RhsInfo]
forall a. OrdList a -> [a]
fromOL OrdList RhsInfo
ol_red, OrdList RhsInfo -> [RhsInfo]
forall a. OrdList a -> [a]
fromOL OrdList RhsInfo
ol_inacc)
  where
    (OrdList RhsInfo
_ol_acc, OrdList RhsInfo
ol_inacc, OrdList RhsInfo
ol_red) = AnnotatedTree
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
go AnnotatedTree
tree
    -- | Collects RHSs which are
    --    1. accessible
    --    2. proper inaccessible (so we can't delete them)
    --    3. hypothetically redundant (so not only inaccessible RHS, but we can
    --       even safely delete the equation without altering semantics)
    -- See Note [Determining inaccessible clauses]
    go :: AnnotatedTree -> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
    go :: AnnotatedTree
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
go (AccessibleRhs Deltas
_ RhsInfo
info) = (RhsInfo -> OrdList RhsInfo
forall a. a -> OrdList a
unitOL RhsInfo
info, OrdList RhsInfo
forall a. OrdList a
nilOL, OrdList RhsInfo
forall a. OrdList a
nilOL)
    go (InaccessibleRhs RhsInfo
info) = (OrdList RhsInfo
forall a. OrdList a
nilOL,       OrdList RhsInfo
forall a. OrdList a
nilOL, RhsInfo -> OrdList RhsInfo
forall a. a -> OrdList a
unitOL RhsInfo
info) -- presumably redundant
    go (MayDiverge AnnotatedTree
t)         = case AnnotatedTree
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
go AnnotatedTree
t of
      -- See Note [Determining inaccessible clauses]
      (OrdList RhsInfo
acc, OrdList RhsInfo
inacc, OrdList RhsInfo
red)
        | OrdList RhsInfo -> Bool
forall a. OrdList a -> Bool
isNilOL OrdList RhsInfo
acc Bool -> Bool -> Bool
&& OrdList RhsInfo -> Bool
forall a. OrdList a -> Bool
isNilOL OrdList RhsInfo
inacc -> (OrdList RhsInfo
forall a. OrdList a
nilOL, OrdList RhsInfo
red, OrdList RhsInfo
forall a. OrdList a
nilOL)
      (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
res                              -> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
res
    go (SequenceAnn AnnotatedTree
l AnnotatedTree
r)      = AnnotatedTree
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
go AnnotatedTree
l (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
forall a. Semigroup a => a -> a -> a
Semi.<> AnnotatedTree
-> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
go AnnotatedTree
r
    go AnnotatedTree
EmptyAnn               = (OrdList RhsInfo
forall a. OrdList a
nilOL,       OrdList RhsInfo
forall a. OrdList a
nilOL, OrdList RhsInfo
forall a. OrdList a
nilOL)

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

-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
dsPmWarn DynFlags
dflags ctx :: DsMatchContext
ctx@(DsMatchContext HsMatchContext GhcRn
kind SrcSpan
loc) [Id]
vars CheckResult
result
  = Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
flag_i Bool -> Bool -> Bool
|| Bool
flag_u) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ do
      [Delta]
unc_examples <- [Id] -> Int -> Deltas -> DsM [Delta]
getNFirstUncovered [Id]
vars (Int
maxPatterns Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Deltas
uncovered
      let exists_r :: Bool
exists_r = Bool
flag_i Bool -> Bool -> Bool
&& [RhsInfo] -> Bool
forall a. [a] -> Bool
notNull [RhsInfo]
redundant
          exists_i :: Bool
exists_i = Bool
flag_i Bool -> Bool -> Bool
&& [RhsInfo] -> Bool
forall a. [a] -> Bool
notNull [RhsInfo]
inaccessible
          exists_u :: Bool
exists_u = Bool
flag_u Bool -> Bool -> Bool
&& [Delta] -> Bool
forall a. [a] -> Bool
notNull [Delta]
unc_examples
          approx :: Bool
approx   = Precision
precision Precision -> Precision -> Bool
forall a. Eq a => a -> a -> Bool
== Precision
Approximate

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
approx Bool -> Bool -> Bool
&& (Bool
exists_u Bool -> Bool -> Bool
|| Bool
exists_i)) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
loc (WarnReason -> SDoc -> DsM ()
warnDs WarnReason
NoReason SDoc
approx_msg)

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_r (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ [RhsInfo] -> (RhsInfo -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RhsInfo]
redundant ((RhsInfo -> DsM ()) -> DsM ()) -> (RhsInfo -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(L SrcSpan
l SDoc
q) -> do
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (WarnReason -> SDoc -> DsM ()
warnDs (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnOverlappingPatterns)
                               (SDoc -> String -> SDoc
pprEqn SDoc
q String
"is redundant"))
      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_i (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ [RhsInfo] -> (RhsInfo -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [RhsInfo]
inaccessible ((RhsInfo -> DsM ()) -> DsM ()) -> (RhsInfo -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(L SrcSpan
l SDoc
q) -> do
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (WarnReason -> SDoc -> DsM ()
warnDs (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnOverlappingPatterns)
                               (SDoc -> String -> SDoc
pprEqn SDoc
q String
"has inaccessible right hand side"))

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_u (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
loc (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ WarnReason -> SDoc -> DsM ()
warnDs WarnReason
flag_u_reason (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$
        [Id] -> [Delta] -> SDoc
pprEqns [Id]
vars [Delta]
unc_examples
  where
    CheckResult
      { cr_clauses :: CheckResult -> AnnotatedTree
cr_clauses = AnnotatedTree
clauses
      , cr_uncov :: CheckResult -> Deltas
cr_uncov   = Deltas
uncovered
      , cr_approx :: CheckResult -> Precision
cr_approx  = Precision
precision } = CheckResult
result
    ([RhsInfo]
redundant, [RhsInfo]
inaccessible) = AnnotatedTree -> ([RhsInfo], [RhsInfo])
redundantAndInaccessibleRhss AnnotatedTree
clauses

    flag_i :: Bool
flag_i = DynFlags -> HsMatchContext GhcRn -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
overlapping DynFlags
dflags HsMatchContext GhcRn
kind
    flag_u :: Bool
flag_u = DynFlags -> HsMatchContext GhcRn -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext GhcRn
kind
    flag_u_reason :: WarnReason
flag_u_reason = WarnReason
-> (WarningFlag -> WarnReason) -> Maybe WarningFlag -> WarnReason
forall b a. b -> (a -> b) -> Maybe a -> b
maybe WarnReason
NoReason WarningFlag -> WarnReason
Reason (HsMatchContext GhcRn -> Maybe WarningFlag
forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag HsMatchContext GhcRn
kind)

    maxPatterns :: Int
maxPatterns = DynFlags -> Int
maxUncoveredPatterns DynFlags
dflags

    -- Print a single clause (for redundant/with-inaccessible-rhs)
    pprEqn :: SDoc -> String -> SDoc
pprEqn SDoc
q String
txt = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext Bool
True DsMatchContext
ctx (String -> SDoc
text String
txt) (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \SDoc -> SDoc
f ->
      SDoc -> SDoc
f (SDoc
q SDoc -> SDoc -> SDoc
<+> HsMatchContext GhcRn -> SDoc
forall p. HsMatchContext p -> SDoc
matchSeparator HsMatchContext GhcRn
kind SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"...")

    -- Print several clauses (for uncovered clauses)
    pprEqns :: [Id] -> [Delta] -> SDoc
pprEqns [Id]
vars [Delta]
deltas = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext Bool
False DsMatchContext
ctx (String -> SDoc
text String
"are non-exhaustive") (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \SDoc -> SDoc
_ ->
      case [Id]
vars of -- See #11245
           [] -> String -> SDoc
text String
"Guards do not cover entire pattern space"
           [Id]
_  -> let us :: [SDoc]
us = (Delta -> SDoc) -> [Delta] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (\Delta
delta -> Delta -> [Id] -> SDoc
pprUncovered Delta
delta [Id]
vars) [Delta]
deltas
                 in  SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Patterns not matched:") Int
4
                       ([SDoc] -> SDoc
vcat (Int -> [SDoc] -> [SDoc]
forall a. Int -> [a] -> [a]
take Int
maxPatterns [SDoc]
us) SDoc -> SDoc -> SDoc
$$ Int -> [SDoc] -> SDoc
forall a. Int -> [a] -> SDoc
dots Int
maxPatterns [SDoc]
us)

    approx_msg :: SDoc
approx_msg = [SDoc] -> SDoc
vcat
      [ SDoc -> Int -> SDoc -> SDoc
hang
          (String -> SDoc
text String
"Pattern match checker ran into -fmax-pmcheck-models="
            SDoc -> SDoc -> SDoc
<> Int -> SDoc
int (DynFlags -> Int
maxPmCheckModels DynFlags
dflags)
            SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
" limit, so")
          Int
2
          (  SDoc
bullet SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Redundant clauses might not be reported at all"
          SDoc -> SDoc -> SDoc
$$ SDoc
bullet SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Redundant clauses might be reported as inaccessible"
          SDoc -> SDoc -> SDoc
$$ SDoc
bullet SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Patterns reported as unmatched might actually be matched")
      , String -> SDoc
text String
"Increase the limit or resolve the warnings to suppress this message." ]

getNFirstUncovered :: [Id] -> Int -> Deltas -> DsM [Delta]
getNFirstUncovered :: [Id] -> Int -> Deltas -> DsM [Delta]
getNFirstUncovered [Id]
vars Int
n (MkDeltas Bag Delta
deltas) = Int -> [Delta] -> DsM [Delta]
go Int
n (Bag Delta -> [Delta]
forall a. Bag a -> [a]
bagToList Bag Delta
deltas)
  where
    go :: Int -> [Delta] -> DsM [Delta]
go Int
0 [Delta]
_              = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go Int
_ []             = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go Int
n (Delta
delta:[Delta]
deltas) = do
      [Delta]
front <- [Id] -> Int -> Delta -> DsM [Delta]
provideEvidence [Id]
vars Int
n Delta
delta
      [Delta]
back <- Int -> [Delta] -> DsM [Delta]
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Delta] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Delta]
front) [Delta]
deltas
      [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Delta]
front [Delta] -> [Delta] -> [Delta]
forall a. [a] -> [a] -> [a]
++ [Delta]
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 :: forall a. Int -> [a] -> SDoc
dots Int
maxPatterns [a]
qs
    | [a]
qs [a] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
maxPatterns = String -> SDoc
text String
"..."
    | Bool
otherwise                      = SDoc
empty

-- | All warning flags that need to run the pattern match checker.
allPmCheckWarnings :: [WarningFlag]
allPmCheckWarnings :: [WarningFlag]
allPmCheckWarnings =
  [ WarningFlag
Opt_WarnIncompletePatterns
  , WarningFlag
Opt_WarnIncompleteUniPatterns
  , WarningFlag
Opt_WarnIncompletePatternsRecUpd
  , WarningFlag
Opt_WarnOverlappingPatterns
  ]

-- | Check whether the redundancy checker should run (redundancy only)
overlapping :: DynFlags -> HsMatchContext id -> Bool
-- See Note [Inaccessible warnings for record updates]
overlapping :: forall id. DynFlags -> HsMatchContext id -> Bool
overlapping DynFlags
_      HsMatchContext id
RecUpd = Bool
False
overlapping DynFlags
dflags HsMatchContext id
_      = WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnOverlappingPatterns DynFlags
dflags

-- | Check whether the exhaustiveness checker should run (exhaustiveness only)
exhaustive :: DynFlags -> HsMatchContext id -> Bool
exhaustive :: forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive  DynFlags
dflags = Bool -> (WarningFlag -> Bool) -> Maybe WarningFlag -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (WarningFlag -> DynFlags -> Bool
`wopt` DynFlags
dflags) (Maybe WarningFlag -> Bool)
-> (HsMatchContext id -> Maybe WarningFlag)
-> HsMatchContext id
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsMatchContext id -> Maybe WarningFlag
forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag

-- | 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 :: forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag (FunRhs {})   = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag HsMatchContext id
CaseAlt       = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag HsMatchContext id
IfAlt         = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag HsMatchContext id
LambdaExpr    = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompleteUniPatterns
exhaustiveWarningFlag HsMatchContext id
PatBindRhs    = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompleteUniPatterns
exhaustiveWarningFlag HsMatchContext id
PatBindGuards = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag HsMatchContext id
ProcExpr      = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompleteUniPatterns
exhaustiveWarningFlag HsMatchContext id
RecUpd        = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatternsRecUpd
exhaustiveWarningFlag HsMatchContext id
ThPatSplice   = Maybe WarningFlag
forall a. Maybe a
Nothing
exhaustiveWarningFlag HsMatchContext id
PatSyn        = Maybe WarningFlag
forall a. Maybe a
Nothing
exhaustiveWarningFlag HsMatchContext id
ThPatQuote    = Maybe WarningFlag
forall a. Maybe a
Nothing
exhaustiveWarningFlag (StmtCtxt {}) = Maybe WarningFlag
forall a. Maybe a
Nothing -- Don't warn about incomplete patterns
                                       -- in list comprehensions, pattern guards
                                       -- etc. They are often *supposed* to be
                                       -- incomplete

-- True <==> singular
pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext Bool
singular (DsMatchContext HsMatchContext GhcRn
kind SrcSpan
_loc) SDoc
msg (SDoc -> SDoc) -> SDoc
rest_of_msg_fun
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
txt SDoc -> SDoc -> SDoc
<+> SDoc
msg,
          [SDoc] -> SDoc
sep [ String -> SDoc
text String
"In" SDoc -> SDoc -> SDoc
<+> SDoc
ppr_match SDoc -> SDoc -> SDoc
<> Char -> SDoc
char Char
':'
              , Int -> SDoc -> SDoc
nest Int
4 ((SDoc -> SDoc) -> SDoc
rest_of_msg_fun SDoc -> SDoc
pref)]]
  where
    txt :: String
txt | Bool
singular  = String
"Pattern match"
        | Bool
otherwise = String
"Pattern match(es)"

    (SDoc
ppr_match, SDoc -> SDoc
pref)
        = case HsMatchContext GhcRn
kind of
             FunRhs { mc_fun :: forall p. HsMatchContext p -> LIdP p
mc_fun = L SrcSpan
_ IdP GhcRn
fun }
                  -> (HsMatchContext GhcRn -> SDoc
forall p. Outputable (IdP p) => HsMatchContext p -> SDoc
pprMatchContext HsMatchContext GhcRn
kind, \ SDoc
pp -> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
IdP GhcRn
fun SDoc -> SDoc -> SDoc
<+> SDoc
pp)
             HsMatchContext GhcRn
_    -> (HsMatchContext GhcRn -> SDoc
forall p. Outputable (IdP p) => HsMatchContext p -> SDoc
pprMatchContext HsMatchContext GhcRn
kind, \ SDoc
pp -> SDoc
pp)