{-
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,
        needToRunPmCheck, isMatchContextPmChecked,

        -- See Note [Type and Term Equality Propagation]
        addTyCsDs, addScrutTmCs, addPatTmCs
    ) where

#include "HsVersions.h"

import GhcPrelude

import GHC.HsToCore.PmCheck.Types
import GHC.HsToCore.PmCheck.Oracle
import GHC.HsToCore.PmCheck.Ppr
import BasicTypes (Origin, isGenerated)
import CoreSyn (CoreExpr, Expr(Var,App))
import FastString (unpackFS, lengthFS)
import DynFlags
import GHC.Hs
import TcHsSyn
import Id
import ConLike
import Name
import FamInst
import TysWiredIn
import SrcLoc
import Util
import Outputable
import DataCon
import TyCon
import Var (EvVar)
import Coercion
import TcEvidence
import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr, dsSyntaxExpr)
import {-# SOURCE #-} DsBinds (dsHsWrapper)
import DsUtils (selectMatchVar)
import MatchLit (dsLit, dsOverLit)
import DsMonad
import Bag
import TyCoRep
import Type
import DsUtils       (isTrueLHsExpr)
import Maybes
import qualified GHC.LanguageExtensions as LangExt

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"

    http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.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 tvs dicts args@ corresponds to a
    -- @K tvs dicts args <- x@ guard. The @tvs@ and @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]
_con_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]

-- | Each 'Delta' is proof (i.e., a model of the fact) that some values are not
-- covered by a pattern match. E.g. @f Nothing = <rhs>@ might be given an
-- uncovered set @[x :-> Just y]@ or @[x /= Nothing]@, where @x@ is the variable
-- matching against @f@'s first argument.
type Uncovered = [Delta]

-- Instead of keeping the whole sets in memory, we keep a boolean for both the
-- covered and the divergent set (we store the uncovered set though, since we
-- want to print it). For both the covered and the divergent we have:
--
--   True <=> The set is non-empty
--
-- hence:
--  C = True             ==> Useful clause (no warning)
--  C = False, D = True  ==> Clause with inaccessible RHS
--  C = False, D = False ==> Redundant clause

data Covered = Covered | NotCovered
  deriving Int -> Covered -> ShowS
[Covered] -> ShowS
Covered -> String
(Int -> Covered -> ShowS)
-> (Covered -> String) -> ([Covered] -> ShowS) -> Show Covered
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Covered] -> ShowS
$cshowList :: [Covered] -> ShowS
show :: Covered -> String
$cshow :: Covered -> String
showsPrec :: Int -> Covered -> ShowS
$cshowsPrec :: Int -> Covered -> ShowS
Show

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

-- Like the or monoid for booleans
-- Covered = True, Uncovered = False
instance Semi.Semigroup Covered where
  Covered
Covered <> :: Covered -> Covered -> Covered
<> Covered
_ = Covered
Covered
  Covered
_ <> Covered
Covered = Covered
Covered
  Covered
NotCovered <> Covered
NotCovered = Covered
NotCovered

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

data Diverged = Diverged | NotDiverged
  deriving Int -> Diverged -> ShowS
[Diverged] -> ShowS
Diverged -> String
(Int -> Diverged -> ShowS)
-> (Diverged -> String) -> ([Diverged] -> ShowS) -> Show Diverged
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Diverged] -> ShowS
$cshowList :: [Diverged] -> ShowS
show :: Diverged -> String
$cshow :: Diverged -> String
showsPrec :: Int -> Diverged -> ShowS
$cshowsPrec :: Int -> Diverged -> ShowS
Show

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

instance Semi.Semigroup Diverged where
  Diverged
Diverged <> :: Diverged -> Diverged -> Diverged
<> Diverged
_ = Diverged
Diverged
  Diverged
_ <> Diverged
Diverged = Diverged
Diverged
  Diverged
NotDiverged <> Diverged
NotDiverged = Diverged
NotDiverged

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

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
Approximate <> :: Precision -> Precision -> Precision
<> Precision
_ = Precision
Approximate
  Precision
_ <> Precision
Approximate = Precision
Approximate
  Precision
Precise <> Precision
Precise = Precision
Precise

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

-- | A triple <C,U,D> of covered, uncovered, and divergent sets.
--
-- Also stores a flag 'presultApprox' denoting whether we ran into the
-- 'maxPmCheckModels' limit for the purpose of hints in warning messages to
-- maybe increase the limit.
data PartialResult = PartialResult {
                        PartialResult -> Covered
presultCovered   :: Covered
                      , PartialResult -> Uncovered
presultUncovered :: Uncovered
                      , PartialResult -> Diverged
presultDivergent :: Diverged
                      , PartialResult -> Precision
presultApprox    :: Precision }

emptyPartialResult :: PartialResult
emptyPartialResult :: PartialResult
emptyPartialResult = PartialResult :: Covered -> Uncovered -> Diverged -> Precision -> PartialResult
PartialResult { presultUncovered :: Uncovered
presultUncovered = Uncovered
forall a. Monoid a => a
mempty
                                   , presultCovered :: Covered
presultCovered   = Covered
forall a. Monoid a => a
mempty
                                   , presultDivergent :: Diverged
presultDivergent = Diverged
forall a. Monoid a => a
mempty
                                   , presultApprox :: Precision
presultApprox    = Precision
forall a. Monoid a => a
mempty }

combinePartialResults :: PartialResult -> PartialResult -> PartialResult
combinePartialResults :: PartialResult -> PartialResult -> PartialResult
combinePartialResults (PartialResult Covered
cs1 Uncovered
vsa1 Diverged
ds1 Precision
ap1) (PartialResult Covered
cs2 Uncovered
vsa2 Diverged
ds2 Precision
ap2)
  = Covered -> Uncovered -> Diverged -> Precision -> PartialResult
PartialResult (Covered
cs1 Covered -> Covered -> Covered
forall a. Semigroup a => a -> a -> a
Semi.<> Covered
cs2)
                  (Uncovered
vsa1 Uncovered -> Uncovered -> Uncovered
forall a. Semigroup a => a -> a -> a
Semi.<> Uncovered
vsa2)
                  (Diverged
ds1 Diverged -> Diverged -> Diverged
forall a. Semigroup a => a -> a -> a
Semi.<> Diverged
ds2)
                  (Precision
ap1 Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> Precision
ap2) -- the result is approximate if either is

instance Outputable PartialResult where
  ppr :: PartialResult -> SDoc
ppr (PartialResult Covered
c Uncovered
unc Diverged
d Precision
pc)
    = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"PartialResult" SDoc -> SDoc -> SDoc
<+> Covered -> SDoc
forall a. Outputable a => a -> SDoc
ppr Covered
c SDoc -> SDoc -> SDoc
<+> Diverged -> SDoc
forall a. Outputable a => a -> SDoc
ppr Diverged
d SDoc -> SDoc -> SDoc
<+> Precision -> SDoc
forall a. Outputable a => a -> SDoc
ppr Precision
pc) Int
2 (Uncovered -> SDoc
ppr_unc Uncovered
unc)
    where
      ppr_unc :: Uncovered -> SDoc
ppr_unc = SDoc -> SDoc
braces (SDoc -> SDoc) -> (Uncovered -> SDoc) -> Uncovered -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
fsep ([SDoc] -> SDoc) -> (Uncovered -> [SDoc]) -> Uncovered -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma ([SDoc] -> [SDoc]) -> (Uncovered -> [SDoc]) -> Uncovered -> [SDoc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Delta -> SDoc) -> Uncovered -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr

instance Semi.Semigroup PartialResult where
  <> :: PartialResult -> PartialResult -> PartialResult
(<>) = PartialResult -> PartialResult -> PartialResult
combinePartialResults

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

-- | Pattern check result
--
-- * Redundant clauses
-- * Not-covered clauses (or their type, if no pattern is available)
-- * Clauses with inaccessible RHS
-- * A flag saying whether we ran into the 'maxPmCheckModels' limit for the
--   purpose of suggesting to crank it up in the warning message
--
-- More details about the classification of clauses into useful, redundant
-- and with inaccessible right hand side can be found here:
--
--     https://gitlab.haskell.org/ghc/ghc/wikis/pattern-match-check
--
data PmResult =
  PmResult {
      PmResult -> [Located [LPat GhcTc]]
pmresultRedundant    :: [Located [LPat GhcTc]]
    , PmResult -> Uncovered
pmresultUncovered    :: [Delta]
    , PmResult -> [Located [LPat GhcTc]]
pmresultInaccessible :: [Located [LPat GhcTc]]
    , PmResult -> Precision
pmresultApproximate  :: Precision }

instance Outputable PmResult where
  ppr :: PmResult -> SDoc
ppr PmResult
pmr = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"PmResult") Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
    [ String -> SDoc
text String
"pmresultRedundant" SDoc -> SDoc -> SDoc
<+> [Located [Located (Pat GhcTc)]] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (PmResult -> [Located [LPat GhcTc]]
pmresultRedundant PmResult
pmr)
    , String -> SDoc
text String
"pmresultUncovered" SDoc -> SDoc -> SDoc
<+> Uncovered -> SDoc
forall a. Outputable a => a -> SDoc
ppr (PmResult -> Uncovered
pmresultUncovered PmResult
pmr)
    , String -> SDoc
text String
"pmresultInaccessible" SDoc -> SDoc -> SDoc
<+> [Located [Located (Pat GhcTc)]] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (PmResult -> [Located [LPat GhcTc]]
pmresultInaccessible PmResult
pmr)
    , String -> SDoc
text String
"pmresultApproximate" SDoc -> SDoc -> SDoc
<+> Precision -> SDoc
forall a. Outputable a => a -> SDoc
ppr (PmResult -> Precision
pmresultApproximate PmResult
pmr)
    ]

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

-- | Check a single pattern binding (let)
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
checkSingle DynFlags
dflags ctxt :: DsMatchContext
ctxt@(DsMatchContext HsMatchContext Name
_ SrcSpan
locn) Id
var Pat GhcTc
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 GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr Pat GhcTc
p])
  PmResult
res <- SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
checkSingle' SrcSpan
locn Id
var Pat GhcTc
p
  DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM ()
dsPmWarn DynFlags
dflags DsMatchContext
ctxt [Id
var] PmResult
res

-- | Check a single pattern binding (let)
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
checkSingle' SrcSpan
locn Id
var Pat GhcTc
p = do
  FamInstEnvs
fam_insts <- DsM FamInstEnvs
dsGetFamInstEnvs
  GrdVec
grds      <- FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
translatePat FamInstEnvs
fam_insts Id
var Pat GhcTc
p
  Delta
missing   <- DsM Delta
getPmDelta
  String -> SDoc -> DsM ()
tracePm String
"checkSingle': missing" (Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
missing)
  PartialResult Covered
cs Uncovered
us Diverged
ds Precision
pc <- GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck GrdVec
grds [] Int
1 Delta
missing
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  Uncovered
us' <- [Id] -> Int -> Uncovered -> DsM Uncovered
getNFirstUncovered [Id
var] (DynFlags -> Int
maxUncoveredPatterns DynFlags
dflags Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Uncovered
us
  let plain :: PmResult
plain = PmResult :: [Located [LPat GhcTc]]
-> Uncovered -> [Located [LPat GhcTc]] -> Precision -> PmResult
PmResult { pmresultRedundant :: [Located [LPat GhcTc]]
pmresultRedundant    = []
                       , pmresultUncovered :: Uncovered
pmresultUncovered    = Uncovered
us'
                       , pmresultInaccessible :: [Located [LPat GhcTc]]
pmresultInaccessible = []
                       , pmresultApproximate :: Precision
pmresultApproximate  = Precision
pc }
  PmResult -> DsM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PmResult -> DsM PmResult) -> PmResult -> DsM PmResult
forall a b. (a -> b) -> a -> b
$ case (Covered
cs,Diverged
ds) of
    (Covered
Covered   , Diverged
_          ) -> PmResult
plain                              -- useful
    (Covered
NotCovered, Diverged
NotDiverged) -> PmResult
plain { pmresultRedundant :: [Located [LPat GhcTc]]
pmresultRedundant = [Located [Located (Pat GhcTc)]]
[Located [LPat GhcTc]]
m    } -- redundant
    (Covered
NotCovered, Diverged
Diverged   ) -> PmResult
plain { pmresultInaccessible :: [Located [LPat GhcTc]]
pmresultInaccessible = [Located [Located (Pat GhcTc)]]
[Located [LPat GhcTc]]
m } -- inaccessible rhs
  where m :: [Located [Located (Pat GhcTc)]]
m = [SrcSpan
-> SrcSpanLess (Located [Located (Pat GhcTc)])
-> Located [Located (Pat GhcTc)]
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
locn [SrcSpan -> SrcSpanLess (Located (Pat GhcTc)) -> Located (Pat GhcTc)
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
locn SrcSpanLess (Located (Pat GhcTc))
Pat GhcTc
p]]

-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions.
checkGuardMatches :: HsMatchContext Name          -- Match context
                  -> GRHSs GhcTc (LHsExpr GhcTc)  -- Guarded RHSs
                  -> DsM ()
checkGuardMatches :: HsMatchContext Name -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM ()
checkGuardMatches HsMatchContext Name
hs_ctx guards :: GRHSs GhcTc (LHsExpr GhcTc)
guards@(GRHSs XCGRHSs GhcTc (LHsExpr GhcTc)
_ [LGRHS GhcTc (LHsExpr GhcTc)]
grhss LHsLocalBinds GhcTc
_) = do
    DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
    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 GhcTc (LHsExpr GhcTc) -> SrcSpan)
-> [LGRHS GhcTc (LHsExpr GhcTc)] -> [SrcSpan]
forall a b. (a -> b) -> [a] -> [b]
map LGRHS GhcTc (LHsExpr GhcTc) -> SrcSpan
forall a. HasSrcSpan a => a -> SrcSpan
getLoc [LGRHS GhcTc (LHsExpr GhcTc)]
grhss)
        dsMatchContext :: DsMatchContext
dsMatchContext = HsMatchContext Name -> SrcSpan -> DsMatchContext
DsMatchContext HsMatchContext Name
hs_ctx SrcSpan
combinedLoc
        match :: LMatch GhcTc (LHsExpr GhcTc)
match = SrcSpan
-> SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc))
-> LMatch GhcTc (LHsExpr GhcTc)
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
combinedLoc (SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc))
 -> LMatch GhcTc (LHsExpr GhcTc))
-> SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc))
-> LMatch GhcTc (LHsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
                  Match :: forall p body.
XCMatch p body
-> HsMatchContext (NameOrRdrName (IdP p))
-> [LPat p]
-> GRHSs p body
-> Match p body
Match { m_ext :: XCMatch GhcTc (LHsExpr GhcTc)
m_ext = XCMatch GhcTc (LHsExpr GhcTc)
NoExtField
noExtField
                        , m_ctxt :: HsMatchContext (NameOrRdrName (IdP GhcTc))
m_ctxt = HsMatchContext Name
HsMatchContext (NameOrRdrName (IdP GhcTc))
hs_ctx
                        , m_pats :: [LPat GhcTc]
m_pats = []
                        , m_grhss :: GRHSs GhcTc (LHsExpr GhcTc)
m_grhss = GRHSs GhcTc (LHsExpr GhcTc)
guards }
    DynFlags
-> DsMatchContext
-> [Id]
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM ()
checkMatches DynFlags
dflags DsMatchContext
dsMatchContext [] [LMatch GhcTc (LHsExpr GhcTc)
match]
checkGuardMatches HsMatchContext Name
_ (XGRHSs XXGRHSs GhcTc (LHsExpr GhcTc)
nec) = NoExtCon -> DsM ()
forall a. NoExtCon -> a
noExtCon XXGRHSs GhcTc (LHsExpr GhcTc)
NoExtCon
nec

-- | Check a matchgroup (case, functions, etc.)
checkMatches :: DynFlags -> DsMatchContext
             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
checkMatches :: DynFlags
-> DsMatchContext
-> [Id]
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM ()
checkMatches DynFlags
dflags DsMatchContext
ctxt [Id]
vars [LMatch GhcTc (LHsExpr GhcTc)]
matches = do
  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 GhcTc (LHsExpr GhcTc) -> SDoc)
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map LMatch GhcTc (LHsExpr GhcTc) -> SDoc
forall a. Outputable a => a -> SDoc
ppr [LMatch GhcTc (LHsExpr GhcTc)]
matches)))
  PmResult
res <- [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
checkMatches' [Id]
vars [LMatch GhcTc (LHsExpr GhcTc)]
matches
  DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM ()
dsPmWarn DynFlags
dflags DsMatchContext
ctxt [Id]
vars PmResult
res

-- | Check a matchgroup (case, functions, etc.).
checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
checkMatches' [Id]
vars [LMatch GhcTc (LHsExpr GhcTc)]
matches = do
  Delta
init_delta <- DsM Delta
getPmDelta
  Uncovered
missing <- case [LMatch GhcTc (LHsExpr GhcTc)]
matches of
    -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
    [] | [Id
var] <- [Id]
vars -> Maybe Delta -> Uncovered
forall a. Maybe a -> [a]
maybeToList (Maybe Delta -> Uncovered)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta) -> DsM Uncovered
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta -> TmCt -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addTmCt Delta
init_delta (Id -> TmCt
TmVarNonVoid Id
var)
    [LMatch GhcTc (LHsExpr GhcTc)]
_                  -> Uncovered -> DsM Uncovered
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Delta
init_delta]
  String -> SDoc -> DsM ()
tracePm String
"checkMatches': missing" (Uncovered -> SDoc
forall a. Outputable a => a -> SDoc
ppr Uncovered
missing)
  ([LMatch GhcTc (LHsExpr GhcTc)]
rs,Uncovered
us,[LMatch GhcTc (LHsExpr GhcTc)]
ds,Precision
pc) <- [LMatch GhcTc (LHsExpr GhcTc)]
-> Uncovered
-> DsM
     ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)], Precision)
go [LMatch GhcTc (LHsExpr GhcTc)]
matches Uncovered
missing
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  Uncovered
us' <- [Id] -> Int -> Uncovered -> DsM Uncovered
getNFirstUncovered [Id]
vars (DynFlags -> Int
maxUncoveredPatterns DynFlags
dflags Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Uncovered
us
  PmResult -> DsM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PmResult -> DsM PmResult) -> PmResult -> DsM PmResult
forall a b. (a -> b) -> a -> b
$ PmResult :: [Located [LPat GhcTc]]
-> Uncovered -> [Located [LPat GhcTc]] -> Precision -> PmResult
PmResult {
                pmresultRedundant :: [Located [LPat GhcTc]]
pmresultRedundant    = (LMatch GhcTc (LHsExpr GhcTc) -> Located [Located (Pat GhcTc)])
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> [Located [Located (Pat GhcTc)]]
forall a b. (a -> b) -> [a] -> [b]
map LMatch GhcTc (LHsExpr GhcTc) -> Located [Located (Pat GhcTc)]
forall id body. LMatch id body -> Located [LPat id]
hsLMatchToLPats [LMatch GhcTc (LHsExpr GhcTc)]
rs
              , pmresultUncovered :: Uncovered
pmresultUncovered    = Uncovered
us'
              , pmresultInaccessible :: [Located [LPat GhcTc]]
pmresultInaccessible = (LMatch GhcTc (LHsExpr GhcTc) -> Located [Located (Pat GhcTc)])
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> [Located [Located (Pat GhcTc)]]
forall a b. (a -> b) -> [a] -> [b]
map LMatch GhcTc (LHsExpr GhcTc) -> Located [Located (Pat GhcTc)]
forall id body. LMatch id body -> Located [LPat id]
hsLMatchToLPats [LMatch GhcTc (LHsExpr GhcTc)]
ds
              , pmresultApproximate :: Precision
pmresultApproximate  = Precision
pc }
  where
    go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
       -> DsM ( [LMatch GhcTc (LHsExpr GhcTc)]
              , Uncovered
              , [LMatch GhcTc (LHsExpr GhcTc)]
              , Precision)
    go :: [LMatch GhcTc (LHsExpr GhcTc)]
-> Uncovered
-> DsM
     ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)], Precision)
go []     Uncovered
missing = ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
 [LMatch GhcTc (LHsExpr GhcTc)], Precision)
-> DsM
     ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)], Precision)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Uncovered
missing, [], Precision
Precise)
    go (LMatch GhcTc (LHsExpr GhcTc)
m:[LMatch GhcTc (LHsExpr GhcTc)]
ms) Uncovered
missing = do
      String -> SDoc -> DsM ()
tracePm String
"checkMatches': go" (LMatch GhcTc (LHsExpr GhcTc) -> SDoc
forall a. Outputable a => a -> SDoc
ppr LMatch GhcTc (LHsExpr GhcTc)
m)
      DynFlags
dflags             <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
      FamInstEnvs
fam_insts          <- DsM FamInstEnvs
dsGetFamInstEnvs
      (GrdVec
clause, [GrdVec]
guards)   <- FamInstEnvs
-> [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (GrdVec, [GrdVec])
translateMatch FamInstEnvs
fam_insts [Id]
vars LMatch GhcTc (LHsExpr GhcTc)
m
      let limit :: Int
limit                     = DynFlags -> Int
maxPmCheckModels DynFlags
dflags
          n_siblings :: Int
n_siblings                = Uncovered -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Uncovered
missing
          throttled_check :: Delta -> DsM PartialResult
throttled_check Delta
delta     =
            (Int, PartialResult) -> PartialResult
forall a b. (a, b) -> b
snd ((Int, PartialResult) -> PartialResult)
-> IOEnv (Env DsGblEnv DsLclEnv) (Int, PartialResult)
-> DsM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> (Int -> Delta -> DsM PartialResult)
-> Int
-> Delta
-> IOEnv (Env DsGblEnv DsLclEnv) (Int, PartialResult)
throttle Int
limit (GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck GrdVec
clause [GrdVec]
guards) Int
n_siblings Delta
delta

      r :: PartialResult
r@(PartialResult Covered
cs Uncovered
missing' Diverged
ds Precision
pc1) <- (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
runMany Delta -> DsM PartialResult
throttled_check Uncovered
missing

      String -> SDoc -> DsM ()
tracePm String
"checkMatches': go: res" (PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
r)
      ([LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u, [LMatch GhcTc (LHsExpr GhcTc)]
is, Precision
pc2)  <- [LMatch GhcTc (LHsExpr GhcTc)]
-> Uncovered
-> DsM
     ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)], Precision)
go [LMatch GhcTc (LHsExpr GhcTc)]
ms Uncovered
missing'
      ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
 [LMatch GhcTc (LHsExpr GhcTc)], Precision)
-> DsM
     ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)], Precision)
forall (m :: * -> *) a. Monad m => a -> m a
return (([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
  [LMatch GhcTc (LHsExpr GhcTc)], Precision)
 -> DsM
      ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
       [LMatch GhcTc (LHsExpr GhcTc)], Precision))
-> ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
    [LMatch GhcTc (LHsExpr GhcTc)], Precision)
-> DsM
     ([LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)], Precision)
forall a b. (a -> b) -> a -> b
$ case (Covered
cs, Diverged
ds) of
        -- useful
        (Covered
Covered,  Diverged
_    )        -> ([LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u,    [LMatch GhcTc (LHsExpr GhcTc)]
is, Precision
pc1 Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> Precision
pc2)
        -- redundant
        (Covered
NotCovered, Diverged
NotDiverged) -> (LMatch GhcTc (LHsExpr GhcTc)
mLMatch GhcTc (LHsExpr GhcTc)
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [LMatch GhcTc (LHsExpr GhcTc)]
forall a. a -> [a] -> [a]
:[LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u, [LMatch GhcTc (LHsExpr GhcTc)]
is, Precision
pc1 Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> Precision
pc2)
        -- inaccessible
        (Covered
NotCovered, Diverged
Diverged )   -> ([LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u, LMatch GhcTc (LHsExpr GhcTc)
mLMatch GhcTc (LHsExpr GhcTc)
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [LMatch GhcTc (LHsExpr GhcTc)]
forall a. a -> [a] -> [a]
:[LMatch GhcTc (LHsExpr GhcTc)]
is, Precision
pc1 Precision -> Precision -> Precision
forall a. Semigroup a => a -> a -> a
Semi.<> Precision
pc2)

    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
hsLMatchToLPats (LMatch id body -> Located (SrcSpanLess (LMatch id body))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
l (Match { m_pats = pats })) = SrcSpan -> SrcSpanLess (Located [LPat id]) -> Located [LPat id]
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
l [LPat id]
SrcSpanLess (Located [LPat id])
pats
    hsLMatchToLPats LMatch id body
_                                   = String -> Located [LPat id]
forall a. String -> a
panic String
"checkMatches'"

getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta]
getNFirstUncovered :: [Id] -> Int -> Uncovered -> DsM Uncovered
getNFirstUncovered [Id]
_    Int
0 Uncovered
_              = Uncovered -> DsM Uncovered
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
getNFirstUncovered [Id]
_    Int
_ []             = Uncovered -> DsM Uncovered
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
getNFirstUncovered [Id]
vars Int
n (Delta
delta:Uncovered
deltas) = do
  Uncovered
front <- [Id] -> Int -> Delta -> DsM Uncovered
provideEvidence [Id]
vars Int
n Delta
delta
  Uncovered
back <- [Id] -> Int -> Uncovered -> DsM Uncovered
getNFirstUncovered [Id]
vars (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Uncovered -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Uncovered
front) Uncovered
deltas
  Uncovered -> DsM Uncovered
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Uncovered
front Uncovered -> Uncovered -> Uncovered
forall a. [a] -> [a] -> [a]
++ Uncovered
back)

{- 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 -> GrdVec
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,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, GrdVec)] -> DsM GrdVec
mkListGrds Id
a []                  = GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
a DataCon
nilDataCon []]
mkListGrds Id
a ((Id
x, GrdVec
head_grds):[(Id, GrdVec)]
xs) = do
  Id
b <- Type -> DsM Id
mkPmId (Id -> Type
idType Id
a)
  GrdVec
tail_grds <- Id -> [(Id, GrdVec)] -> DsM GrdVec
mkListGrds Id
b [(Id, GrdVec)]
xs
  GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GrdVec -> DsM GrdVec) -> GrdVec -> DsM GrdVec
forall a b. (a -> b) -> a -> b
$ Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
a DataCon
consDataCon [Id
x, Id
b] PmGrd -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
: GrdVec
head_grds GrdVec -> GrdVec -> GrdVec
forall a. [a] -> [a] -> [a]
++ GrdVec
tail_grds

-- | Create a 'GrdVec' refining a match variable to a 'PmLit'.
mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
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 -> DsM GrdVec
mk_char_lit Id
y Char
c = Id -> PmLit -> DsM GrdVec
mkPmLitGrds Id
y (Type -> PmLitValue -> PmLit
PmLit Type
charTy (Char -> PmLitValue
PmLitChar Char
c))
  [GrdVec]
char_grdss <- (Id -> Char -> DsM GrdVec)
-> [Id] -> String -> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Id -> Char -> DsM GrdVec
mk_char_lit [Id]
vars (FastString -> String
unpackFS FastString
s)
  Id -> [(Id, GrdVec)] -> DsM GrdVec
mkListGrds Id
x ([Id] -> [GrdVec] -> [(Id, GrdVec)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
vars [GrdVec]
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 = [] }
  GrdVec -> DsM GrdVec
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 GhcTc -> DsM GrdVec
translatePat FamInstEnvs
fam_insts Id
x Pat GhcTc
pat = case Pat GhcTc
pat of
  WildPat  XWildPat GhcTc
_ty -> GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  VarPat XVarPat GhcTc
_ Located (IdP GhcTc)
y   -> GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> Id -> GrdVec
mkPmLetVar (Located Id -> SrcSpanLess (Located Id)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Located Id
Located (IdP GhcTc)
y) Id
x)
  ParPat XParPat GhcTc
_ LPat GhcTc
p   -> FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts Id
x LPat GhcTc
p
  LazyPat XLazyPat GhcTc
_ LPat GhcTc
_  -> GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] -- like a wildcard
  BangPat XBangPat GhcTc
_ LPat GhcTc
p  ->
    -- Add the bang in front of the list, because it will happen before any
    -- nested stuff.
    (Id -> PmGrd
PmBang Id
x PmGrd -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
:) (GrdVec -> GrdVec) -> DsM GrdVec -> DsM GrdVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts Id
x LPat GhcTc
p

  -- (x@pat)   ==>   Translate pat with x as match var and handle impedance
  --                 mismatch with incoming match var
  AsPat XAsPat GhcTc
_ (Located (IdP GhcTc) -> Located (SrcSpanLess (Located Id))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ SrcSpanLess (Located Id)
y) LPat GhcTc
p -> (Id -> Id -> GrdVec
mkPmLetVar SrcSpanLess (Located Id)
Id
y Id
x GrdVec -> GrdVec -> GrdVec
forall a. [a] -> [a] -> [a]
++) (GrdVec -> GrdVec) -> DsM GrdVec -> DsM GrdVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts SrcSpanLess (Located Id)
Id
y LPat GhcTc
p

  SigPat XSigPat GhcTc
_ LPat GhcTc
p LHsSigWcType (NoGhcTc GhcTc)
_ty -> FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts Id
x LPat GhcTc
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
  CoPat XCoPat GhcTc
_ HsWrapper
wrapper Pat GhcTc
p Type
_ty
    | HsWrapper -> Bool
isIdHsWrapper HsWrapper
wrapper                   -> FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
translatePat FamInstEnvs
fam_insts Id
x Pat GhcTc
p
    | WpCast TcCoercionR
co <-  HsWrapper
wrapper, TcCoercionR -> Bool
isReflexiveCo TcCoercionR
co -> FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
translatePat FamInstEnvs
fam_insts Id
x Pat GhcTc
p
    | Bool
otherwise -> do
        (Id
y, GrdVec
grds) <- FamInstEnvs -> Pat GhcTc -> DsM (Id, GrdVec)
translatePatV FamInstEnvs
fam_insts Pat GhcTc
p
        CoreExpr -> CoreExpr
wrap_rhs_y <- HsWrapper -> DsM (CoreExpr -> CoreExpr)
dsHsWrapper HsWrapper
wrapper
        GrdVec -> DsM GrdVec
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 -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
: GrdVec
grds)

  -- (n + k)  ===>   let b = x >= k, True <- b, let n = x-k
  NPlusKPat XNPlusKPat GhcTc
_pat_ty (Located (IdP GhcTc) -> Located (SrcSpanLess (Located Id))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ SrcSpanLess (Located Id)
n) Located (HsOverLit GhcTc)
k1 HsOverLit GhcTc
k2 SyntaxExpr GhcTc
ge SyntaxExpr GhcTc
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 GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr)
-> [HsOverLit GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [CoreExpr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse HsOverLit GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsOverLit [Located (HsOverLit GhcTc)
-> SrcSpanLess (Located (HsOverLit GhcTc))
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Located (HsOverLit GhcTc)
k1, HsOverLit GhcTc
k2]
    CoreExpr
rhs_b <- SyntaxExpr GhcTc
-> [CoreExpr] -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsSyntaxExpr SyntaxExpr GhcTc
ge    [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x, CoreExpr
ke1]
    CoreExpr
rhs_n <- SyntaxExpr GhcTc
-> [CoreExpr] -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsSyntaxExpr SyntaxExpr GhcTc
minus [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x, CoreExpr
ke2]
    GrdVec -> DsM GrdVec
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 SrcSpanLess (Located Id)
Id
n CoreExpr
rhs_n]

  -- (fun -> pat)   ===>   let y = fun x, pat <- y where y is a match var of pat
  ViewPat XViewPat GhcTc
_arg_ty LHsExpr GhcTc
lexpr LPat GhcTc
pat -> do
    (Id
y, GrdVec
grds) <- FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV FamInstEnvs
fam_insts LPat GhcTc
pat
    CoreExpr
fun <- LHsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr GhcTc
lexpr
    GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GrdVec -> DsM GrdVec) -> GrdVec -> DsM GrdVec
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 -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
: GrdVec
grds

  -- list
  ListPat (ListPatTc _elem_ty Nothing) [LPat GhcTc]
ps ->
    FamInstEnvs -> Id -> [LPat GhcTc] -> DsM GrdVec
translateListPat FamInstEnvs
fam_insts Id
x [LPat GhcTc]
ps

  -- overloaded list
  ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) [LPat GhcTc]
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 GhcTc] -> DsM GrdVec
translateListPat FamInstEnvs
fam_insts Id
x [LPat GhcTc]
pats
      Maybe Type
_ -> do
        Id
y <- Type -> DsM Id
mkPmId (Type -> Type
mkListTy Type
elem_ty)
        GrdVec
grds <- FamInstEnvs -> Id -> [LPat GhcTc] -> DsM GrdVec
translateListPat FamInstEnvs
fam_insts Id
y [LPat GhcTc]
pats
        CoreExpr
rhs_y <- SyntaxExpr GhcTc
-> [CoreExpr] -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsSyntaxExpr SyntaxExpr GhcTc
to_list [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x]
        GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GrdVec -> DsM GrdVec) -> GrdVec -> DsM GrdVec
forall a b. (a -> b) -> a -> b
$ Id -> CoreExpr -> PmGrd
PmLet Id
y CoreExpr
rhs_y PmGrd -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
: GrdVec
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.

  ConPatOut { pat_con :: forall p. Pat p -> Located ConLike
pat_con     = (Located ConLike -> Located (SrcSpanLess (Located ConLike))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ SrcSpanLess (Located ConLike)
con)
            , pat_arg_tys :: forall p. Pat p -> [Type]
pat_arg_tys = [Type]
arg_tys
            , pat_tvs :: forall p. Pat p -> [Id]
pat_tvs     = [Id]
ex_tvs
            , pat_dicts :: forall p. Pat p -> [Id]
pat_dicts   = [Id]
dicts
            , pat_args :: forall p. Pat p -> HsConPatDetails p
pat_args    = HsConPatDetails GhcTc
ps } -> do
    FamInstEnvs
-> Id
-> ConLike
-> [Type]
-> [Id]
-> [Id]
-> HsConPatDetails GhcTc
-> DsM GrdVec
translateConPatOut FamInstEnvs
fam_insts Id
x SrcSpanLess (Located ConLike)
ConLike
con [Type]
arg_tys [Id]
ex_tvs [Id]
dicts HsConPatDetails GhcTc
ps

  NPat XNPat GhcTc
ty (Located (HsOverLit GhcTc)
-> Located (SrcSpanLess (Located (HsOverLit GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ SrcSpanLess (Located (HsOverLit GhcTc))
olit) Maybe (SyntaxExpr GhcTc)
mb_neg SyntaxExpr GhcTc
_ -> do
    -- See Note [Literal short cut] in MatchLit.hs
    -- 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
    CoreExpr
core_expr <- case SrcSpanLess (Located (HsOverLit GhcTc))
olit of
      OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ }
        | Bool -> Bool
not Bool
rebindable
        , Just HsExpr GhcTc
expr <- DynFlags -> OverLitVal -> Type -> Maybe (HsExpr GhcTc)
shortCutLit DynFlags
dflags OverLitVal
val Type
XNPat GhcTc
ty
        -> HsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsExpr HsExpr GhcTc
expr
      SrcSpanLess (Located (HsOverLit GhcTc))
_ -> HsOverLit GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsOverLit SrcSpanLess (Located (HsOverLit GhcTc))
HsOverLit GhcTc
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 GhcTc)
mb_neg of
          Just SyntaxExpr GhcTc
_  -> 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 GhcTc)
Nothing -> PmLit
lit
    Id -> PmLit -> DsM GrdVec
mkPmLitGrds Id
x PmLit
lit'

  LitPat XLitPat GhcTc
_ HsLit GhcTc
lit -> do
    CoreExpr
core_expr <- HsLit GhcRn -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLit (HsLit GhcTc -> HsLit GhcRn
forall a b. ConvertIdX a b => HsLit a -> HsLit b
convertLit HsLit GhcTc
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 -> DsM GrdVec
mkPmLitGrds Id
x PmLit
lit

  TuplePat XTuplePat GhcTc
_tys [LPat GhcTc]
pats Boxity
boxity -> do
    ([Id]
vars, [GrdVec]
grdss) <- (Located (Pat GhcTc) -> DsM (Id, GrdVec))
-> [Located (Pat GhcTc)]
-> IOEnv (Env DsGblEnv DsLclEnv) ([Id], [GrdVec])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV FamInstEnvs
fam_insts) [Located (Pat GhcTc)]
[LPat GhcTc]
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)
    GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GrdVec -> DsM GrdVec) -> GrdVec -> DsM GrdVec
forall a b. (a -> b) -> a -> b
$ Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd Id
x DataCon
tuple_con [Id]
vars PmGrd -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
: [GrdVec] -> GrdVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [GrdVec]
grdss

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

  -- --------------------------------------------------------------------------
  -- Not supposed to happen
  ConPatIn  {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"Check.translatePat: ConPatIn"
  SplicePat {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"Check.translatePat: SplicePat"
  XPat      XXPat GhcTc
n  -> NoExtCon -> DsM GrdVec
forall a. NoExtCon -> a
noExtCon XXPat GhcTc
NoExtCon
n

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

translateLPat :: FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat :: FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts Id
x = FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
translatePat FamInstEnvs
fam_insts Id
x (Pat GhcTc -> DsM GrdVec)
-> (Located (Pat GhcTc) -> Pat GhcTc)
-> Located (Pat GhcTc)
-> DsM GrdVec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (Pat GhcTc) -> Pat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc

-- | 'translateLPat', but also select and return a new match var.
translateLPatV :: FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV :: FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV FamInstEnvs
fam_insts = FamInstEnvs -> Pat GhcTc -> DsM (Id, GrdVec)
translatePatV FamInstEnvs
fam_insts (Pat GhcTc -> DsM (Id, GrdVec))
-> (Located (Pat GhcTc) -> Pat GhcTc)
-> Located (Pat GhcTc)
-> DsM (Id, GrdVec)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (Pat GhcTc) -> Pat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
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 GhcTc] -> DsM GrdVec
translateListPat FamInstEnvs
fam_insts Id
x [LPat GhcTc]
pats = do
  [(Id, GrdVec)]
vars_and_grdss <- (Located (Pat GhcTc) -> DsM (Id, GrdVec))
-> [Located (Pat GhcTc)]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Id, GrdVec)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV FamInstEnvs
fam_insts) [Located (Pat GhcTc)]
[LPat GhcTc]
pats
  Id -> [(Id, GrdVec)] -> DsM GrdVec
mkListGrds Id
x [(Id, GrdVec)]
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 GhcTc
-> DsM GrdVec
translateConPatOut FamInstEnvs
fam_insts Id
x ConLike
con [Type]
univ_tys [Id]
ex_tvs [Id]
dicts = \case
    PrefixCon [LPat GhcTc]
ps                 -> [(Int, Located (Pat GhcTc))] -> DsM GrdVec
go_field_pats ([Int] -> [Located (Pat GhcTc)] -> [(Int, Located (Pat GhcTc))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Located (Pat GhcTc)]
[LPat GhcTc]
ps)
    InfixCon  LPat GhcTc
p1 LPat GhcTc
p2              -> [(Int, Located (Pat GhcTc))] -> DsM GrdVec
go_field_pats ([Int] -> [Located (Pat GhcTc)] -> [(Int, Located (Pat GhcTc))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Located (Pat GhcTc)
LPat GhcTc
p1,Located (Pat GhcTc)
LPat GhcTc
p2])
    RecCon    (HsRecFields [LHsRecField GhcTc (LPat GhcTc)]
fs Maybe (Located Int)
_) -> [(Int, Located (Pat GhcTc))] -> DsM GrdVec
go_field_pats ([LHsRecField GhcTc (Located (Pat GhcTc))]
-> [(Int, Located (Pat GhcTc))]
rec_field_ps [LHsRecField GhcTc (Located (Pat GhcTc))]
[LHsRecField GhcTc (LPat GhcTc)]
fs)
  where
    -- The actual argument types (instantiated)
    arg_tys :: [Type]
arg_tys     = ConLike -> [Type] -> [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 :: [LHsRecField GhcTc (Located (Pat GhcTc))]
-> [(Int, Located (Pat GhcTc))]
rec_field_ps [LHsRecField GhcTc (Located (Pat GhcTc))]
fs = (LHsRecField GhcTc (Located (Pat GhcTc))
 -> (Int, Located (Pat GhcTc)))
-> [LHsRecField GhcTc (Located (Pat GhcTc))]
-> [(Int, Located (Pat GhcTc))]
forall a b. (a -> b) -> [a] -> [b]
map (HsRecField GhcTc (Located (Pat GhcTc))
-> (Int, Located (Pat GhcTc))
tagged_pat (HsRecField GhcTc (Located (Pat GhcTc))
 -> (Int, Located (Pat GhcTc)))
-> (LHsRecField GhcTc (Located (Pat GhcTc))
    -> HsRecField GhcTc (Located (Pat GhcTc)))
-> LHsRecField GhcTc (Located (Pat GhcTc))
-> (Int, Located (Pat GhcTc))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHsRecField GhcTc (Located (Pat GhcTc))
-> HsRecField GhcTc (Located (Pat GhcTc))
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) [LHsRecField GhcTc (Located (Pat GhcTc))]
fs
      where
        tagged_pat :: HsRecField GhcTc (Located (Pat GhcTc))
-> (Int, Located (Pat GhcTc))
tagged_pat HsRecField GhcTc (Located (Pat GhcTc))
f = (Name -> Int
lbl_to_index (Located Id -> Name
forall a. NamedThing a => a -> Name
getName (HsRecField GhcTc (Located (Pat GhcTc)) -> Located Id
forall arg. HsRecField GhcTc arg -> Located Id
hsRecFieldId HsRecField GhcTc (Located (Pat GhcTc))
f)), HsRecField GhcTc (Located (Pat GhcTc)) -> Located (Pat GhcTc)
forall id arg. HsRecField' id arg -> arg
hsRecFieldArg HsRecField GhcTc (Located (Pat GhcTc))
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 GhcTc))] -> DsM GrdVec
go_field_pats [(Int, Located (Pat GhcTc))]
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 GhcTc))
-> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), GrdVec)
trans_pat (Int
n, Located (Pat GhcTc)
pat) = do
            (Id
var, GrdVec
pvec) <- FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV FamInstEnvs
fam_insts Located (Pat GhcTc)
LPat GhcTc
pat
            ((Int, Id), GrdVec)
-> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), GrdVec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Int
n, Id
var), GrdVec
pvec)
      ([(Int, Id)]
tagged_vars, [GrdVec]
arg_grdss) <- ((Int, Located (Pat GhcTc))
 -> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), GrdVec))
-> [(Int, Located (Pat GhcTc))]
-> IOEnv (Env DsGblEnv DsLclEnv) ([(Int, Id)], [GrdVec])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Int, Located (Pat GhcTc))
-> IOEnv (Env DsGblEnv DsLclEnv) ((Int, Id), GrdVec)
trans_pat [(Int, Located (Pat GhcTc))]
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 :: GrdVec
bang_grds     = (Id -> PmGrd) -> [Id] -> GrdVec
forall a b. (a -> b) -> [a] -> [b]
map Id -> PmGrd
PmBang   ([Id] -> GrdVec) -> [Id] -> GrdVec
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 :: GrdVec
arg_grds = [GrdVec] -> GrdVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [GrdVec]
arg_grdss

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

-- Translate a single match
translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc)
               -> DsM (GrdVec, [GrdVec])
translateMatch :: FamInstEnvs
-> [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (GrdVec, [GrdVec])
translateMatch FamInstEnvs
fam_insts [Id]
vars (LMatch GhcTc (LHsExpr GhcTc)
-> Located (SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ (Match { m_pats = pats, m_grhss = grhss }))
  = do
      GrdVec
pats'   <- [GrdVec] -> GrdVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([GrdVec] -> GrdVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec] -> DsM GrdVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id -> Located (Pat GhcTc) -> DsM GrdVec)
-> [Id]
-> [Located (Pat GhcTc)]
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts) [Id]
vars [Located (Pat GhcTc)]
[LPat GhcTc]
pats
      [GrdVec]
guards' <- ([GuardStmt GhcTc] -> DsM GrdVec)
-> [[GuardStmt GhcTc]] -> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs -> [GuardStmt GhcTc] -> DsM GrdVec
translateGuards FamInstEnvs
fam_insts) [[GuardStmt GhcTc]]
guards
      -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards'])
      (GrdVec, [GrdVec]) -> DsM (GrdVec, [GrdVec])
forall (m :: * -> *) a. Monad m => a -> m a
return (GrdVec
pats', [GrdVec]
guards')
      where
        extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
        extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
extractGuards (LGRHS GhcTc (LHsExpr GhcTc)
-> Located (SrcSpanLess (LGRHS GhcTc (LHsExpr GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ (GRHS _ gs _)) = (GuardLStmt GhcTc -> GuardStmt GhcTc)
-> [GuardLStmt GhcTc] -> [GuardStmt GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map GuardLStmt GhcTc -> GuardStmt GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [GuardLStmt GhcTc]
gs
        extractGuards LGRHS GhcTc (LHsExpr GhcTc)
_                       = String -> [GuardStmt GhcTc]
forall a. String -> a
panic String
"translateMatch"

        guards :: [[GuardStmt GhcTc]]
guards = (LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc])
-> [LGRHS GhcTc (LHsExpr GhcTc)] -> [[GuardStmt GhcTc]]
forall a b. (a -> b) -> [a] -> [b]
map LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
extractGuards (GRHSs GhcTc (LHsExpr GhcTc) -> [LGRHS GhcTc (LHsExpr GhcTc)]
forall p body. GRHSs p body -> [LGRHS p body]
grhssGRHSs GRHSs GhcTc (LHsExpr GhcTc)
grhss)
translateMatch FamInstEnvs
_ [Id]
_ LMatch GhcTc (LHsExpr GhcTc)
_ = String -> DsM (GrdVec, [GrdVec])
forall a. String -> a
panic String
"translateMatch"

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

-- | Translate a list of guard statements to a 'GrdVec'
translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM GrdVec
translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM GrdVec
translateGuards FamInstEnvs
fam_insts [GuardStmt GhcTc]
guards =
  [GrdVec] -> GrdVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([GrdVec] -> GrdVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec] -> DsM GrdVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GuardStmt GhcTc -> DsM GrdVec)
-> [GuardStmt GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
translateGuard FamInstEnvs
fam_insts) [GuardStmt GhcTc]
guards

-- | Translate a guard statement to a 'GrdVec'
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
translateGuard FamInstEnvs
fam_insts GuardStmt GhcTc
guard = case GuardStmt GhcTc
guard of
  BodyStmt XBodyStmt GhcTc GhcTc (LHsExpr GhcTc)
_   LHsExpr GhcTc
e SyntaxExpr GhcTc
_ SyntaxExpr GhcTc
_ -> LHsExpr GhcTc -> DsM GrdVec
translateBoolGuard LHsExpr GhcTc
e
  LetStmt  XLetStmt GhcTc GhcTc (LHsExpr GhcTc)
_   LHsLocalBinds GhcTc
binds -> HsLocalBinds GhcTc -> DsM GrdVec
translateLet (LHsLocalBinds GhcTc -> SrcSpanLess (LHsLocalBinds GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsLocalBinds GhcTc
binds)
  BindStmt XBindStmt GhcTc GhcTc (LHsExpr GhcTc)
_ LPat GhcTc
p LHsExpr GhcTc
e SyntaxExpr GhcTc
_ SyntaxExpr GhcTc
_ -> FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec
translateBind FamInstEnvs
fam_insts LPat GhcTc
p LHsExpr GhcTc
e
  LastStmt        {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"translateGuard LastStmt"
  ParStmt         {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"translateGuard ParStmt"
  TransStmt       {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"translateGuard TransStmt"
  RecStmt         {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"translateGuard RecStmt"
  ApplicativeStmt {} -> String -> DsM GrdVec
forall a. String -> a
panic String
"translateGuard ApplicativeLastStmt"
  XStmtLR XXStmtLR GhcTc GhcTc (LHsExpr GhcTc)
nec        -> NoExtCon -> DsM GrdVec
forall a. NoExtCon -> a
noExtCon XXStmtLR GhcTc GhcTc (LHsExpr GhcTc)
NoExtCon
nec

-- | Translate let-bindings
translateLet :: HsLocalBinds GhcTc -> DsM GrdVec
translateLet :: HsLocalBinds GhcTc -> DsM GrdVec
translateLet HsLocalBinds GhcTc
_binds = GrdVec -> DsM GrdVec
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 GhcTc -> LHsExpr GhcTc -> DsM GrdVec
translateBind FamInstEnvs
fam_insts LPat GhcTc
p LHsExpr GhcTc
e = LHsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr GhcTc
e IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
-> (CoreExpr -> DsM GrdVec) -> DsM GrdVec
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 GhcTc -> DsM GrdVec
translateLPat FamInstEnvs
fam_insts Id
y LPat GhcTc
p
  CoreExpr
rhs -> do
    (Id
x, GrdVec
grds) <- FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec)
translateLPatV FamInstEnvs
fam_insts LPat GhcTc
p
    GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> CoreExpr -> PmGrd
PmLet Id
x CoreExpr
rhs PmGrd -> GrdVec -> GrdVec
forall a. a -> [a] -> [a]
: GrdVec
grds)

-- | Translate a boolean guard
--   @e ==>  let x = e; True <- x@
translateBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
translateBoolGuard :: LHsExpr GhcTc -> DsM GrdVec
translateBoolGuard LHsExpr GhcTc
e
  | Maybe (CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr) -> Bool
forall a. Maybe a -> Bool
isJust (LHsExpr GhcTc
-> Maybe (CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr)
isTrueLHsExpr LHsExpr GhcTc
e) = GrdVec -> DsM GrdVec
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 GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr GhcTc
e IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
-> (CoreExpr -> DsM GrdVec) -> DsM GrdVec
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
        -> GrdVec -> DsM GrdVec
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
        GrdVec -> DsM GrdVec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GrdVec -> DsM GrdVec) -> GrdVec -> DsM GrdVec
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 the higher-order function 'throttle'.

Note [Combinatorial explosion in guards]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Function with many clauses and deeply nested guards like in #11195 tend to
overwhelm the checker because they lead to exponential splitting behavior.
See the comments on #11195 on refinement trees. Every guard refines the
disjunction of Deltas by another split. This no different than the ConVar case,
but in stark contrast we mostly don't get any useful information out of that
split! Hence splitting k-fold just means having k-fold more work. The problem
exacerbates for larger k, because it gets even more unlikely that we can handle
all of the arising Deltas better than just continue working on the original
Delta.

We simply apply the same mechanism as in Note [Countering exponential blowup].
But we don't want to forget about actually useful info from pattern match
clauses just because we had one clause with many guards. So we set the limit for
guards much lower.

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: Function pmCheck
%*                                                                      *
%************************************************************************

Main functions are:

* pmCheck :: PatVec -> [PatVec] -> ValVec -> Delta -> DsM PartialResult

  This function implements functions `covered`, `uncovered` and
  `divergent` from the paper at once. Calls out to the auxilary function
  `pmCheckGuards` for handling (possibly multiple) guarded RHSs when the whole
  clause is checked. Slightly different from the paper because it does not even
  produce the covered and uncovered sets. Since we only care about whether a
  clause covers SOMETHING or if it may forces ANY argument, we only store a
  boolean in both cases, for efficiency.

* pmCheckGuards :: [PatVec] -> ValVec -> Delta -> DsM PartialResult

  Processes the guards.
-}

-- | @throttle limit f n delta@ executes the pattern match action @f@ but
-- replaces the 'Uncovered' set by @[delta]@ if not doing so would lead to
-- too many Deltas to check.
--
-- See Note [Countering exponential blowup] and
-- Note [Combinatorial explosion in guards]
--
-- How many is "too many"? @throttle@ assumes that the pattern match action
-- will be executed against @n@ similar other Deltas, its "siblings". Now, by
-- observing the branching factor (i.e. the number of children) of executing
-- the action, we can estimate how many Deltas there would be in the next
-- generation. If we find that this number exceeds @limit@, we do
-- "birth control": We simply don't allow a branching factor of more than 1.
-- Otherwise we just return the singleton set of the original @delta@.
-- This amounts to forgetting about the refined facts we got from running the
-- action.
throttle :: Int -> (Int -> Delta -> DsM PartialResult) -> Int -> Delta -> DsM (Int, PartialResult)
throttle :: Int
-> (Int -> Delta -> DsM PartialResult)
-> Int
-> Delta
-> IOEnv (Env DsGblEnv DsLclEnv) (Int, PartialResult)
throttle Int
limit Int -> Delta -> DsM PartialResult
f Int
n_siblings Delta
delta = do
  PartialResult
res <- Int -> Delta -> DsM PartialResult
f Int
n_siblings Delta
delta
  let n_own_children :: Int
n_own_children = Uncovered -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PartialResult -> Uncovered
presultUncovered PartialResult
res)
  let n_next_gen :: Int
n_next_gen = Int
n_siblings Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n_own_children
  -- Birth control!
  if Int
n_next_gen Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
limit Bool -> Bool -> Bool
|| Int
n_own_children Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
    then (Int, PartialResult)
-> IOEnv (Env DsGblEnv DsLclEnv) (Int, PartialResult)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
n_next_gen, PartialResult
res)
    else (Int, PartialResult)
-> IOEnv (Env DsGblEnv DsLclEnv) (Int, PartialResult)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
n_siblings, PartialResult
res { presultUncovered :: Uncovered
presultUncovered = [Delta
delta], presultApprox :: Precision
presultApprox = Precision
Approximate })

-- | Map a pattern matching action processing a single 'Delta' over a
-- 'Uncovered' set and return the combined 'PartialResult's.
runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
runMany Delta -> DsM PartialResult
f Uncovered
unc = [PartialResult] -> PartialResult
forall a. Monoid a => [a] -> a
mconcat ([PartialResult] -> PartialResult)
-> IOEnv (Env DsGblEnv DsLclEnv) [PartialResult]
-> DsM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Delta -> DsM PartialResult)
-> Uncovered -> IOEnv (Env DsGblEnv DsLclEnv) [PartialResult]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Delta -> DsM PartialResult
f Uncovered
unc

-- | Print diagnostic info and actually call 'pmCheck''.
pmCheck :: GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck :: GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck GrdVec
ps [GrdVec]
guards Int
n Delta
delta = do
  String -> SDoc -> DsM ()
tracePm String
"pmCheck {" (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat [ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<> SDoc
colon
                           , SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"patterns:") Int
2 (GrdVec -> SDoc
forall a. Outputable a => a -> SDoc
ppr GrdVec
ps)
                           , SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"guards:") Int
2 ([GrdVec] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [GrdVec]
guards)
                           , Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta ]
  PartialResult
res <- GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck' GrdVec
ps [GrdVec]
guards Int
n Delta
delta
  String -> SDoc -> DsM ()
tracePm String
"}:" (PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
res) -- braces are easier to match by tooling
  PartialResult -> DsM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
res

-- | Lifts 'pmCheck' over a 'DsM (Maybe Delta)'.
pmCheckM :: GrdVec -> [GrdVec] -> Int -> DsM (Maybe Delta) -> DsM PartialResult
pmCheckM :: GrdVec
-> [GrdVec]
-> Int
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> DsM PartialResult
pmCheckM GrdVec
ps [GrdVec]
guards Int
n IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
m_mb_delta = IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
m_mb_delta IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> (Maybe Delta -> DsM PartialResult) -> DsM PartialResult
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Maybe Delta
Nothing    -> PartialResult -> DsM PartialResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure PartialResult
forall a. Monoid a => a
mempty
  Just Delta
delta -> GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck GrdVec
ps [GrdVec]
guards Int
n Delta
delta

-- | Check the list of mutually exclusive guards
pmCheckGuards :: [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheckGuards :: [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheckGuards []       Int
_ Delta
delta = PartialResult -> DsM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta -> PartialResult
usimple Delta
delta)
pmCheckGuards (GrdVec
gv:[GrdVec]
gvs) Int
n Delta
delta = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let limit :: Int
limit = DynFlags -> Int
maxPmCheckModels DynFlags
dflags Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
5
  (Int
n', PartialResult Covered
cs Uncovered
unc Diverged
ds Precision
pc) <- Int
-> (Int -> Delta -> DsM PartialResult)
-> Int
-> Delta
-> IOEnv (Env DsGblEnv DsLclEnv) (Int, PartialResult)
throttle Int
limit (GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck GrdVec
gv []) Int
n Delta
delta
  (PartialResult Covered
css Uncovered
uncs Diverged
dss Precision
pcs) <- (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
runMany ([GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheckGuards [GrdVec]
gvs Int
n') Uncovered
unc
  PartialResult -> DsM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PartialResult -> DsM PartialResult)
-> PartialResult -> DsM PartialResult
forall a b. (a -> b) -> a -> b
$ Covered -> Uncovered -> Diverged -> Precision -> PartialResult
PartialResult (Covered
cs Covered -> Covered -> Covered
forall a. Monoid a => a -> a -> a
`mappend` Covered
css)
                         Uncovered
uncs
                         (Diverged
ds Diverged -> Diverged -> Diverged
forall a. Monoid a => a -> a -> a
`mappend` Diverged
dss)
                         (Precision
pc Precision -> Precision -> Precision
forall a. Monoid a => a -> a -> a
`mappend` Precision
pcs)

-- | Matching function: Check simultaneously a clause (takes separately the
-- patterns and the list of guards) for exhaustiveness, redundancy and
-- inaccessibility.
pmCheck'
  :: GrdVec   -- ^ Patterns of the clause
  -> [GrdVec] -- ^ (Possibly multiple) guards of the clause
  -> Int      -- ^ Estimate on the number of similar 'Delta's to handle.
              --   See 6. in Note [Countering exponential blowup]
  -> Delta    -- ^ Oracle state giving meaning to the identifiers in the ValVec
  -> DsM PartialResult
pmCheck' :: GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck' [] [GrdVec]
guards Int
n Delta
delta
  | [GrdVec] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [GrdVec]
guards = PartialResult -> DsM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PartialResult -> DsM PartialResult)
-> PartialResult -> DsM PartialResult
forall a b. (a -> b) -> a -> b
$ PartialResult
forall a. Monoid a => a
mempty { presultCovered :: Covered
presultCovered = Covered
Covered }
  | Bool
otherwise   = [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheckGuards [GrdVec]
guards Int
n Delta
delta

-- let x = e: Add x ~ e to the oracle
pmCheck' (PmLet { pm_id :: PmGrd -> Id
pm_id = Id
x, pm_let_expr :: PmGrd -> CoreExpr
pm_let_expr = CoreExpr
e } : GrdVec
ps) [GrdVec]
guards Int
n Delta
delta = do
  String -> SDoc -> DsM ()
tracePm String
"PmLet" ([SDoc] -> SDoc
vcat [Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x, CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e])
  -- x is fresh because it's bound by the let
  Delta
delta' <- String -> Maybe Delta -> Delta
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"x is fresh" (Maybe Delta -> Delta)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta) -> DsM Delta
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta
-> Id -> CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addVarCoreCt Delta
delta Id
x CoreExpr
e
  GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
pmCheck GrdVec
ps [GrdVec]
guards Int
n Delta
delta'

-- Bang x: Add x /~ _|_ to the oracle
pmCheck' (PmBang Id
x : GrdVec
ps) [GrdVec]
guards Int
n Delta
delta = do
  String -> SDoc -> DsM ()
tracePm String
"PmBang" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x)
  PartialResult
pr <- GrdVec
-> [GrdVec]
-> Int
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> DsM PartialResult
pmCheckM GrdVec
ps [GrdVec]
guards Int
n (Delta -> TmCt -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addTmCt Delta
delta (Id -> TmCt
TmVarNonVoid Id
x))
  PartialResult -> DsM PartialResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> Id -> PartialResult -> PartialResult
forceIfCanDiverge Delta
delta Id
x PartialResult
pr)

-- Con: Add x ~ K ys to the Covered set and x /~ K to the Uncovered set
pmCheck' (PmGrd
p : GrdVec
ps) [GrdVec]
guards Int
n Delta
delta
  | PmCon{ pm_id :: PmGrd -> Id
pm_id = Id
x, pm_con_con :: PmGrd -> PmAltCon
pm_con_con = PmAltCon
con, pm_con_args :: PmGrd -> [Id]
pm_con_args = [Id]
args
         , pm_con_dicts :: PmGrd -> [Id]
pm_con_dicts = [Id]
dicts } <- PmGrd
p = do
  -- E.g   f (K p q) = <rhs>
  --       <next equation>
  -- Split delta into two refinements:
  --    * one for <rhs>, binding x to (K p q)
  --    * one for <next equation>, recording that x is /not/ (K _ _)

  -- Stuff for <rhs>
  PartialResult
pr_pos <- GrdVec
-> [GrdVec]
-> Int
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> DsM PartialResult
pmCheckM GrdVec
ps [GrdVec]
guards Int
n (Delta
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addPmConCts Delta
delta Id
x PmAltCon
con [Id]
dicts [Id]
args)

  -- The var is forced regardless of whether @con@ was satisfiable
  -- See Note [Divergence of Newtype matches]
  let pr_pos' :: PartialResult
pr_pos' = Delta -> Id -> PmAltCon -> PartialResult -> PartialResult
addConMatchStrictness Delta
delta Id
x PmAltCon
con PartialResult
pr_pos

  -- Stuff for <next equation>
  PartialResult
pr_neg <- Delta
-> Id -> PmAltCon -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addRefutableAltCon Delta
delta Id
x PmAltCon
con IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> (Maybe Delta -> DsM PartialResult) -> DsM PartialResult
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe Delta
Nothing     -> PartialResult -> DsM PartialResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure PartialResult
forall a. Monoid a => a
mempty
    Just Delta
delta' -> PartialResult -> DsM PartialResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> PartialResult
usimple Delta
delta')

  String -> SDoc -> DsM ()
tracePm String
"PmCon" ([SDoc] -> SDoc
vcat [PmGrd -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmGrd
p, Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x, PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
pr_pos', PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
pr_neg])

  -- Combine both into a single PartialResult
  let pr :: PartialResult
pr = PartialResult -> PartialResult -> PartialResult
mkUnion PartialResult
pr_pos' PartialResult
pr_neg
  PartialResult -> DsM PartialResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure PartialResult
pr

addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM (Maybe Delta)
addPmConCts :: Delta
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addPmConCts Delta
delta Id
x PmAltCon
con [Id]
dicts [Id]
fields = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
 -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ do
  Delta
delta_ty    <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall a b. (a -> b) -> a -> b
$ Delta -> Bag Id -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addTypeEvidence Delta
delta ([Id] -> Bag Id
forall a. [a] -> Bag a
listToBag [Id]
dicts)
  Delta
delta_tm_ty <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall a b. (a -> b) -> a -> b
$ Delta -> TmCt -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addTmCt Delta
delta_ty (Id -> PmAltCon -> [Id] -> TmCt
TmVarCon Id
x PmAltCon
con [Id]
fields)
  Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta_tm_ty

-- ----------------------------------------------------------------------------
-- * Utilities for main checking

-- | Initialise with default values for covering and divergent information and
-- a singleton uncovered set.
usimple :: Delta -> PartialResult
usimple :: Delta -> PartialResult
usimple Delta
delta = PartialResult
forall a. Monoid a => a
mempty { presultUncovered :: Uncovered
presultUncovered = [Delta
delta] }

-- | Get the union of two covered, uncovered and divergent value set
-- abstractions. Since the covered and divergent sets are represented by a
-- boolean, union means computing the logical or (at least one of the two is
-- non-empty).

mkUnion :: PartialResult -> PartialResult -> PartialResult
mkUnion :: PartialResult -> PartialResult -> PartialResult
mkUnion = PartialResult -> PartialResult -> PartialResult
forall a. Monoid a => a -> a -> a
mappend

-- | Set the divergent set to not empty
forces :: PartialResult -> PartialResult
forces :: PartialResult -> PartialResult
forces PartialResult
pres = PartialResult
pres { presultDivergent :: Diverged
presultDivergent = Diverged
Diverged }

-- | Set the divergent set to non-empty if the variable has not been forced yet
forceIfCanDiverge :: Delta -> Id -> PartialResult -> PartialResult
forceIfCanDiverge :: Delta -> Id -> PartialResult -> PartialResult
forceIfCanDiverge Delta
delta Id
x
  | Delta -> Id -> Bool
canDiverge Delta
delta Id
x = PartialResult -> PartialResult
forces
  | Bool
otherwise          = PartialResult -> PartialResult
forall a. a -> a
id

-- | 'forceIfCanDiverge' if the 'PmAltCon' was not a Newtype.
-- See Note [Divergence of Newtype matches].
addConMatchStrictness :: Delta -> Id -> PmAltCon -> PartialResult -> PartialResult
addConMatchStrictness :: Delta -> Id -> PmAltCon -> PartialResult -> PartialResult
addConMatchStrictness Delta
_     Id
_ (PmAltConLike (RealDataCon DataCon
dc)) PartialResult
res
  | TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc) = PartialResult
res
addConMatchStrictness Delta
delta Id
x PmAltCon
_ PartialResult
res = Delta -> Id -> PartialResult -> PartialResult
forceIfCanDiverge Delta
delta Id
x PartialResult
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 DsMonad 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' and `addPatTmCs' are responsible for generating
these constraints.
-}

locallyExtendPmDelta :: (Delta -> DsM (Maybe Delta)) -> DsM a -> DsM a
locallyExtendPmDelta :: (Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
locallyExtendPmDelta Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
ext DsM a
k = DsM Delta
getPmDelta DsM Delta
-> (Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
ext IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> (Maybe Delta -> DsM a) -> DsM a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  -- 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.
  Maybe Delta
Nothing     -> DsM a
k
  Just Delta
delta' -> Delta -> DsM a -> DsM a
forall a. Delta -> DsM a -> DsM a
updPmDelta Delta
delta' DsM a
k

-- | Add in-scope type constraints
addTyCsDs :: Bag EvVar -> DsM a -> DsM a
addTyCsDs :: Bag Id -> DsM a -> DsM a
addTyCsDs Bag Id
ev_vars =
  (Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
forall a.
(Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
locallyExtendPmDelta (\Delta
delta -> Delta -> Bag Id -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addTypeEvidence Delta
delta Bag Id
ev_vars)

-- | 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 :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
addScrutTmCs Maybe (LHsExpr GhcTc)
Nothing    [Id]
_   DsM a
k = DsM a
k
addScrutTmCs (Just LHsExpr GhcTc
scr) [Id
x] DsM a
k = do
  CoreExpr
scr_e <- LHsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr LHsExpr GhcTc
scr
  (Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
forall a.
(Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
locallyExtendPmDelta (\Delta
delta -> Delta
-> Id -> CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addVarCoreCt Delta
delta Id
x CoreExpr
scr_e) DsM a
k
addScrutTmCs Maybe (LHsExpr GhcTc)
_   [Id]
_   DsM a
_ = String -> DsM a
forall a. String -> a
panic String
"addScrutTmCs: HsCase with more than one case binder"

-- | Add equalities to the local 'DsM' environment when checking the RHS of a
-- case expression:
--     case e of x { p1 -> e1; ... pn -> en }
-- When we go deeper to check e.g. e1 we record (x ~ p1).
addPatTmCs :: [Pat GhcTc]           -- LHS       (should have length 1)
           -> [Id]                  -- MatchVars (should have length 1)
           -> DsM a
           -> DsM a
-- Computes an approximation of the Covered set for p1 (which pmCheck currently
-- discards).
addPatTmCs :: [Pat GhcTc] -> [Id] -> DsM a -> DsM a
addPatTmCs [Pat GhcTc]
ps [Id]
xs DsM a
k = do
  FamInstEnvs
fam_insts <- DsM FamInstEnvs
dsGetFamInstEnvs
  GrdVec
grds <- [GrdVec] -> GrdVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([GrdVec] -> GrdVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec] -> DsM GrdVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id -> Pat GhcTc -> DsM GrdVec)
-> [Id] -> [Pat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [GrdVec]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec
translatePat FamInstEnvs
fam_insts) [Id]
xs [Pat GhcTc]
ps
  (Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
forall a.
(Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> DsM a -> DsM a
locallyExtendPmDelta (\Delta
delta -> GrdVec -> Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
computeCovered GrdVec
grds Delta
delta) DsM a
k

-- | A dead simple version of 'pmCheck' that only computes the Covered set.
-- So it only cares about collecting positive info.
-- We use it to collect info from a pattern when we check its RHS.
-- See 'addPatTmCs'.
computeCovered :: GrdVec -> Delta -> DsM (Maybe Delta)
-- The duplication with 'pmCheck' is really unfortunate, but it's simpler than
-- separating out the common cases with 'pmCheck', because that would make the
-- ConVar case harder to understand.
computeCovered :: GrdVec -> Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
computeCovered [] Delta
delta = Maybe Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta)
computeCovered (PmLet { pm_id :: PmGrd -> Id
pm_id = Id
x, pm_let_expr :: PmGrd -> CoreExpr
pm_let_expr = CoreExpr
e } : GrdVec
ps) Delta
delta = do
  Delta
delta' <- String -> Maybe Delta -> Delta
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"x is fresh" (Maybe Delta -> Delta)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta) -> DsM Delta
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta
-> Id -> CoreExpr -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addVarCoreCt Delta
delta Id
x CoreExpr
e
  GrdVec -> Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
computeCovered GrdVec
ps Delta
delta'
computeCovered (PmBang{} : GrdVec
ps) Delta
delta = do
  GrdVec -> Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
computeCovered GrdVec
ps Delta
delta
computeCovered (PmGrd
p : GrdVec
ps) Delta
delta
  | PmCon{ pm_id :: PmGrd -> Id
pm_id = Id
x, pm_con_con :: PmGrd -> PmAltCon
pm_con_con = PmAltCon
con, pm_con_args :: PmGrd -> [Id]
pm_con_args = [Id]
args
         , pm_con_dicts :: PmGrd -> [Id]
pm_con_dicts = [Id]
dicts } <- PmGrd
p
  = Delta
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
addPmConCts Delta
delta Id
x PmAltCon
con [Id]
dicts [Id]
args IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
-> (Maybe Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta))
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe Delta
Nothing     -> Maybe Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Delta
forall a. Maybe a
Nothing
      Just Delta
delta' -> GrdVec -> Delta -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Delta)
computeCovered GrdVec
ps Delta
delta'

{-
%************************************************************************
%*                                                                      *
      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 :: 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)

-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM ()
dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM ()
dsPmWarn DynFlags
dflags ctx :: DsMatchContext
ctx@(DsMatchContext HsMatchContext Name
kind SrcSpan
loc) [Id]
vars PmResult
pm_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
      let exists_r :: Bool
exists_r = Bool
flag_i Bool -> Bool -> Bool
&& [Located [Located (Pat GhcTc)]] -> Bool
forall a. [a] -> Bool
notNull [Located [Located (Pat GhcTc)]]
[Located [LPat GhcTc]]
redundant
          exists_i :: Bool
exists_i = Bool
flag_i Bool -> Bool -> Bool
&& [Located [Located (Pat GhcTc)]] -> Bool
forall a. [a] -> Bool
notNull [Located [Located (Pat GhcTc)]]
[Located [LPat GhcTc]]
inaccessible Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
is_rec_upd
          exists_u :: Bool
exists_u = Bool
flag_u Bool -> Bool -> Bool
&& Uncovered -> Bool
forall a. [a] -> Bool
notNull Uncovered
uncovered
          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
$ [Located [Located (Pat GhcTc)]]
-> (Located [Located (Pat GhcTc)] -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Located [Located (Pat GhcTc)]]
[Located [LPat GhcTc]]
redundant ((Located [Located (Pat GhcTc)] -> DsM ()) -> DsM ())
-> (Located [Located (Pat GhcTc)] -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(Located [Located (Pat GhcTc)]
-> Located (SrcSpanLess (Located [Located (Pat GhcTc)]))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
l SrcSpanLess (Located [Located (Pat GhcTc)])
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)
                               ([Located (Pat GhcTc)] -> String -> SDoc
pprEqn [Located (Pat GhcTc)]
SrcSpanLess (Located [Located (Pat GhcTc)])
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
$ [Located [Located (Pat GhcTc)]]
-> (Located [Located (Pat GhcTc)] -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Located [Located (Pat GhcTc)]]
[Located [LPat GhcTc]]
inaccessible ((Located [Located (Pat GhcTc)] -> DsM ()) -> DsM ())
-> (Located [Located (Pat GhcTc)] -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(Located [Located (Pat GhcTc)]
-> Located (SrcSpanLess (Located [Located (Pat GhcTc)]))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
l SrcSpanLess (Located [Located (Pat GhcTc)])
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)
                               ([Located (Pat GhcTc)] -> String -> SDoc
pprEqn [Located (Pat GhcTc)]
SrcSpanLess (Located [Located (Pat GhcTc)])
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] -> Uncovered -> SDoc
pprEqns [Id]
vars Uncovered
uncovered
  where
    PmResult
      { pmresultRedundant :: PmResult -> [Located [LPat GhcTc]]
pmresultRedundant = [Located [LPat GhcTc]]
redundant
      , pmresultUncovered :: PmResult -> Uncovered
pmresultUncovered = Uncovered
uncovered
      , pmresultInaccessible :: PmResult -> [Located [LPat GhcTc]]
pmresultInaccessible = [Located [LPat GhcTc]]
inaccessible
      , pmresultApproximate :: PmResult -> Precision
pmresultApproximate = Precision
precision } = PmResult
pm_result

    flag_i :: Bool
flag_i = WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnOverlappingPatterns DynFlags
dflags
    flag_u :: Bool
flag_u = DynFlags -> HsMatchContext Name -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext Name
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 Name -> Maybe WarningFlag
forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag HsMatchContext Name
kind)

    is_rec_upd :: Bool
is_rec_upd = case HsMatchContext Name
kind of { HsMatchContext Name
RecUpd -> Bool
True; HsMatchContext Name
_ -> Bool
False }
       -- See Note [Inaccessible warnings for record updates]

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

    -- Print a single clause (for redundant/with-inaccessible-rhs)
    pprEqn :: [Located (Pat GhcTc)] -> String -> SDoc
pprEqn [Located (Pat GhcTc)]
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 (HsMatchContext Name -> [Pat GhcTc] -> SDoc
pprPats HsMatchContext Name
kind ((Located (Pat GhcTc) -> Pat GhcTc)
-> [Located (Pat GhcTc)] -> [Pat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map Located (Pat GhcTc) -> Pat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [Located (Pat GhcTc)]
q))

    -- Print several clauses (for uncovered clauses)
    pprEqns :: [Id] -> Uncovered -> SDoc
pprEqns [Id]
vars Uncovered
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) -> Uncovered -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (\Delta
delta -> Delta -> [Id] -> SDoc
pprUncovered Delta
delta [Id]
vars) Uncovered
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." ]

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

dots :: Int -> [a] -> SDoc
dots :: 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 exhaustiveness checker should run (exhaustiveness only)
exhaustive :: DynFlags -> HsMatchContext id -> Bool
exhaustive :: 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 :: 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 Name
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 Name
kind of
             FunRhs { mc_fun :: forall id. HsMatchContext id -> Located id
mc_fun = (Located Name -> Located (SrcSpanLess (Located Name))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L SrcSpan
_ SrcSpanLess (Located Name)
fun) }
                  -> (HsMatchContext Name -> SDoc
forall id.
(Outputable (NameOrRdrName id), Outputable id) =>
HsMatchContext id -> SDoc
pprMatchContext HsMatchContext Name
kind, \ SDoc
pp -> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
SrcSpanLess (Located Name)
fun SDoc -> SDoc -> SDoc
<+> SDoc
pp)
             HsMatchContext Name
_    -> (HsMatchContext Name -> SDoc
forall id.
(Outputable (NameOrRdrName id), Outputable id) =>
HsMatchContext id -> SDoc
pprMatchContext HsMatchContext Name
kind, \ SDoc
pp -> SDoc
pp)

pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
pprPats HsMatchContext Name
kind [Pat GhcTc]
pats
  = [SDoc] -> SDoc
sep [[SDoc] -> SDoc
sep ((Pat GhcTc -> SDoc) -> [Pat GhcTc] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Pat GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Pat GhcTc]
pats), HsMatchContext Name -> SDoc
forall id. HsMatchContext id -> SDoc
matchSeparator HsMatchContext Name
kind, String -> SDoc
text String
"..."]