{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}

-- | Coverage checking step of the
-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
--
-- Coverage check guard trees (like @'PmMatch' 'Pre'@) to get a
-- 'CheckResult', containing
--
--   1. The set of uncovered values, 'cr_uncov'
--   2. And an annotated tree variant (like @'PmMatch' 'Post'@) that captures
--      redundancy and inaccessibility information as 'RedSets' annotations
--
-- Basically the UA function from Section 5.1, which is an optimised
-- interleaving of U and A from Section 3.2 (Figure 5).
-- The Normalised Refinement Types 'Nablas' are maintained in
-- "GHC.HsToCore.Pmc.Solver".
module GHC.HsToCore.Pmc.Check (
        CheckAction(..),
        checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase, checkRecSel
    ) where

import GHC.Prelude

import GHC.Builtin.Names ( hasKey, considerAccessibleIdKey, trueDataConKey )
import GHC.HsToCore.Monad ( DsM )
import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Utils
import GHC.HsToCore.Pmc.Solver
import GHC.Driver.DynFlags
import GHC.Utils.Outputable
import GHC.Tc.Utils.TcType (evVarPred)
import GHC.Data.OrdList
import GHC.Data.Bag

import qualified Data.Semigroup as Semi
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Coerce
import GHC.Types.Var
import GHC.Core
import GHC.Core.Utils

-- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'.
newtype CheckAction a = CA { forall a. CheckAction a -> Nablas -> DsM (CheckResult a)
unCA :: Nablas -> DsM (CheckResult a) }
  deriving (forall a b. (a -> b) -> CheckAction a -> CheckAction b)
-> (forall a b. a -> CheckAction b -> CheckAction a)
-> Functor CheckAction
forall a b. a -> CheckAction b -> CheckAction a
forall a b. (a -> b) -> CheckAction a -> CheckAction b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b
fmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b
$c<$ :: forall a b. a -> CheckAction b -> CheckAction a
<$ :: forall a b. a -> CheckAction b -> CheckAction a
Functor

-- | Composes 'CheckAction's top-to-bottom:
-- If a value falls through the resulting action, then it must fall through the
-- first action and then through the second action.
-- If a value matches the resulting action, then it either matches the
-- first action or matches the second action.
-- Basically the semantics of the LYG branching construct.
topToBottom :: (top -> bot -> ret)
            -> CheckAction top
            -> CheckAction bot
            -> CheckAction ret
topToBottom :: forall top bot ret.
(top -> bot -> ret)
-> CheckAction top -> CheckAction bot -> CheckAction ret
topToBottom top -> bot -> ret
f (CA Nablas -> DsM (CheckResult top)
top) (CA Nablas -> DsM (CheckResult bot)
bot) = (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult ret)) -> CheckAction ret)
-> (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
  t <- Nablas -> DsM (CheckResult top)
top Nablas
inc
  b <- bot (cr_uncov t)
  pure CheckResult { cr_ret = f (cr_ret t) (cr_ret b)
                   , cr_uncov = cr_uncov b
                   , cr_approx = cr_approx t Semi.<> cr_approx b }


-- | Composes 'CheckAction's left-to-right:
-- If a value falls through the resulting action, then it either falls through the
-- first action or through the second action.
-- If a value matches the resulting action, then it must match the first action
-- and then match the second action.
-- Basically the semantics of the LYG guard construct.
leftToRight :: (RedSets -> right -> ret)
            -> CheckAction RedSets
            -> CheckAction right
            -> CheckAction ret
leftToRight :: forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> right -> ret
f (CA Nablas -> DsM (CheckResult Post)
left) (CA Nablas -> DsM (CheckResult right)
right) = (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult ret)) -> CheckAction ret)
-> (Nablas -> DsM (CheckResult ret)) -> CheckAction ret
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
  l <- Nablas -> DsM (CheckResult Post)
left Nablas
inc
  r <- right (rs_cov (cr_ret l))
  limit <- maxPmCheckModels <$> getDynFlags
  let uncov = CheckResult Post -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult Post
l Nablas -> Nablas -> Nablas
forall a. Semigroup a => a -> a -> a
Semi.<> CheckResult right -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult right
r
  -- See Note [Countering exponential blowup]
  let (prec', uncov') = throttle limit inc uncov
  pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r)
                   , cr_uncov = uncov'
                   , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r }

-- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@
-- is exceeding the given @limit@ and the @old@ number of 'Nabla's.
-- See Note [Countering exponential blowup].
throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas)
throttle Int
limit old :: Nablas
old@(MkNablas Bag Nabla
old_ds) new :: Nablas
new@(MkNablas Bag Nabla
new_ds)
  --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
  | Bag Nabla -> Int
forall a. Bag a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Nabla
new_ds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
limit (Bag Nabla -> Int
forall a. Bag a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Bag Nabla
old_ds) = (Precision
Approximate, Nablas
old)
  | Bool
otherwise                                 = (Precision
Precise,     Nablas
new)

checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
-- The implementation is pretty similar to
-- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
checkSequence :: forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence grdtree -> CheckAction anntree
act (grdtree
t :| [])       = (anntree -> [anntree] -> NonEmpty anntree
forall a. a -> [a] -> NonEmpty a
:| []) (anntree -> NonEmpty anntree)
-> CheckAction anntree -> CheckAction (NonEmpty anntree)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> grdtree -> CheckAction anntree
act grdtree
t
checkSequence grdtree -> CheckAction anntree
act (grdtree
t1 :| (grdtree
t2:[grdtree]
ts)) =
  (anntree -> NonEmpty anntree -> NonEmpty anntree)
-> CheckAction anntree
-> CheckAction (NonEmpty anntree)
-> CheckAction (NonEmpty anntree)
forall top bot ret.
(top -> bot -> ret)
-> CheckAction top -> CheckAction bot -> CheckAction ret
topToBottom anntree -> NonEmpty anntree -> NonEmpty anntree
forall a. a -> NonEmpty a -> NonEmpty a
(NE.<|) (grdtree -> CheckAction anntree
act grdtree
t1) ((grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence grdtree -> CheckAction anntree
act (grdtree
t2grdtree -> [grdtree] -> NonEmpty grdtree
forall a. a -> [a] -> NonEmpty a
:|[grdtree]
ts))

emptyRedSets :: RedSets
-- Semigroup instance would be misleading!
emptyRedSets :: Post
emptyRedSets = Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> Post
RedSets Nablas
forall a. Monoid a => a
mempty Nablas
forall a. Monoid a => a
mempty OrdList (Nablas, SrcInfo)
forall a. Monoid a => a
mempty

checkGrd :: PmGrd -> CheckAction RedSets
checkGrd :: PmGrd -> CheckAction Post
checkGrd PmGrd
grd = (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult Post)) -> CheckAction Post)
-> (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> case PmGrd
grd of
  -- let x = e: Refine with x ~ e
  PmLet Id
x CoreExpr
e -> do
    matched <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> CoreExpr -> PhiCt
PhiCoreCt Id
x CoreExpr
e)
    tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
                     , cr_uncov = mempty
                     , cr_approx = Precise }
  -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
  PmBang Id
x Maybe SrcInfo
mb_info -> do
    div <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiBotCt Id
x)
    matched <- addPhiCtNablas inc (PhiNotBotCt x)
    -- See Note [Dead bang patterns]
    -- mb_info = Just info <==> PmBang originates from bang pattern in source
    let bangs | Just SrcInfo
info <- Maybe SrcInfo
mb_info = (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo)
forall a. a -> OrdList a
unitOL (Nablas
div, SrcInfo
info)
              | Bool
otherwise            = OrdList (Nablas, SrcInfo)
forall a. OrdList a
NilOL
    tracePm "check:Bang" (ppr x <+> ppr div)
    pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
                     , cr_uncov = mempty
                     , cr_approx = Precise }
  -- See point (3) of Note [considerAccessible]
  PmCon Id
x (PmAltConLike ConLike
con) [Id]
_ [Id]
_ [Id]
_
    | Id
x Id -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
considerAccessibleIdKey
    , ConLike
con ConLike -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
trueDataConKey
    -> CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = Post
emptyRedSets { rs_cov = initNablas }
                        , cr_uncov :: Nablas
cr_uncov = Nablas
forall a. Monoid a => a
mempty
                        , cr_approx :: Precision
cr_approx = Precision
Precise }
  -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
  PmCon Id
x PmAltCon
con [Id]
tvs [Id]
dicts [Id]
args -> do
    !div <- if PmAltCon -> Bool
isPmAltConMatchStrict PmAltCon
con
      then Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiBotCt Id
x)
      else Nablas -> DsM Nablas
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nablas
forall a. Monoid a => a
mempty
    !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
    !uncov   <- addPhiCtNablas inc (PhiNotConCt x con)
    tracePm "check:Con" $ vcat
      [ ppr grd
      , ppr inc
      , hang (text "div") 2 (ppr div)
      , hang (text "matched") 2 (ppr matched)
      , hang (text "uncov") 2 (ppr uncov)
      ]
    pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
                     , cr_uncov = uncov
                     , cr_approx = Precise }

checkGrds :: [PmGrd] -> CheckAction RedSets
checkGrds :: [PmGrd] -> CheckAction Post
checkGrds [] = (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult Post)) -> CheckAction Post)
-> (Nablas -> DsM (CheckResult Post)) -> CheckAction Post
forall a b. (a -> b) -> a -> b
$ \Nablas
inc ->
  CheckResult Post -> DsM (CheckResult Post)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CheckResult { cr_ret :: Post
cr_ret = Post
emptyRedSets { rs_cov = inc }
                   , cr_uncov :: Nablas
cr_uncov = Nablas
forall a. Monoid a => a
mempty
                   , cr_approx :: Precision
cr_approx = Precision
Precise }
checkGrds (PmGrd
g:[PmGrd]
grds) = (Post -> Post -> Post)
-> CheckAction Post -> CheckAction Post -> CheckAction Post
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> Post -> Post
merge (PmGrd -> CheckAction Post
checkGrd PmGrd
g) ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
grds)
  where
    merge :: Post -> Post -> Post
merge Post
ri_g Post
ri_grds = -- This operation would /not/ form a Semigroup!
      RedSets { rs_cov :: Nablas
rs_cov   = Post -> Nablas
rs_cov Post
ri_grds
              , rs_div :: Nablas
rs_div   = Post -> Nablas
rs_div Post
ri_g   Nablas -> Nablas -> Nablas
forall a. Semigroup a => a -> a -> a
Semi.<> Post -> Nablas
rs_div Post
ri_grds
              , rs_bangs :: OrdList (Nablas, SrcInfo)
rs_bangs = Post -> OrdList (Nablas, SrcInfo)
rs_bangs Post
ri_g OrdList (Nablas, SrcInfo)
-> OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo)
forall a. Semigroup a => a -> a -> a
Semi.<> Post -> OrdList (Nablas, SrcInfo)
rs_bangs Post
ri_grds }

checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
checkMatchGroup (PmMatchGroup NonEmpty (PmMatch Pre)
matches) =
  NonEmpty (PmMatch Post) -> PmMatchGroup Post
forall p. NonEmpty (PmMatch p) -> PmMatchGroup p
PmMatchGroup (NonEmpty (PmMatch Post) -> PmMatchGroup Post)
-> CheckAction (NonEmpty (PmMatch Post))
-> CheckAction (PmMatchGroup Post)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmMatch Pre -> CheckAction (PmMatch Post))
-> NonEmpty (PmMatch Pre) -> CheckAction (NonEmpty (PmMatch Post))
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch NonEmpty (PmMatch Pre)
matches

checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post)
checkMatch (PmMatch { pm_pats :: forall p. PmMatch p -> p
pm_pats = GrdVec [PmGrd]
grds, pm_grhss :: forall p. PmMatch p -> PmGRHSs p
pm_grhss = PmGRHSs Pre
grhss }) =
  (Post -> PmGRHSs Post -> PmMatch Post)
-> CheckAction Post
-> CheckAction (PmGRHSs Post)
-> CheckAction (PmMatch Post)
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> PmGRHSs Post -> PmMatch Post
forall p. p -> PmGRHSs p -> PmMatch p
PmMatch ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
grds) (PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs PmGRHSs Pre
grhss)

checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs (PmGRHSs { pgs_lcls :: forall p. PmGRHSs p -> p
pgs_lcls = GrdVec [PmGrd]
lcls, pgs_grhss :: forall p. PmGRHSs p -> NonEmpty (PmGRHS p)
pgs_grhss = NonEmpty (PmGRHS Pre)
grhss }) =
  (Post -> NonEmpty (PmGRHS Post) -> PmGRHSs Post)
-> CheckAction Post
-> CheckAction (NonEmpty (PmGRHS Post))
-> CheckAction (PmGRHSs Post)
forall right ret.
(Post -> right -> ret)
-> CheckAction Post -> CheckAction right -> CheckAction ret
leftToRight Post -> NonEmpty (PmGRHS Post) -> PmGRHSs Post
forall p. p -> NonEmpty (PmGRHS p) -> PmGRHSs p
PmGRHSs ([PmGrd] -> CheckAction Post
checkGrds [PmGrd]
lcls) ((PmGRHS Pre -> CheckAction (PmGRHS Post))
-> NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post))
forall grdtree anntree.
(grdtree -> CheckAction anntree)
-> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
checkSequence PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS NonEmpty (PmGRHS Pre)
grhss)

checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS (PmGRHS { pg_grds :: forall p. PmGRHS p -> p
pg_grds = GrdVec [PmGrd]
grds, pg_rhs :: forall p. PmGRHS p -> SrcInfo
pg_rhs = SrcInfo
rhs_info }) =
  (Post -> SrcInfo -> PmGRHS Post) -> SrcInfo -> Post -> PmGRHS Post
forall a b c. (a -> b -> c) -> b -> a -> c
flip Post -> SrcInfo -> PmGRHS Post
forall p. p -> SrcInfo -> PmGRHS p
PmGRHS SrcInfo
rhs_info (Post -> PmGRHS Post)
-> CheckAction Post -> CheckAction (PmGRHS Post)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PmGrd] -> CheckAction Post
checkGrds [PmGrd]
grds

checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
-- See Note [Checking EmptyCase]
checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
checkEmptyCase pe :: PmEmptyCase
pe@(PmEmptyCase { pe_var :: PmEmptyCase -> Id
pe_var = Id
var }) = (Nablas -> DsM (CheckResult PmEmptyCase))
-> CheckAction PmEmptyCase
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult PmEmptyCase))
 -> CheckAction PmEmptyCase)
-> (Nablas -> DsM (CheckResult PmEmptyCase))
-> CheckAction PmEmptyCase
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
  unc <- Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
inc (Id -> PhiCt
PhiNotBotCt Id
var)
  pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }

checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post)
checkPatBind = (PmGRHS Pre -> CheckAction (PmGRHS Post))
-> PmPatBind Pre -> CheckAction (PmPatBind Post)
forall a b. Coercible a b => a -> b
coerce PmGRHS Pre -> CheckAction (PmGRHS Post)
checkGRHS

checkRecSel :: PmRecSel () -> CheckAction (PmRecSel Id)
-- See Note [Detecting incomplete record selectors] in GHC.HsToCore.Pmc
checkRecSel :: PmRecSel () -> CheckAction (PmRecSel Id)
checkRecSel pr :: PmRecSel ()
pr@(PmRecSel { pr_arg :: forall v. PmRecSel v -> CoreExpr
pr_arg = CoreExpr
arg, pr_cons :: forall v. PmRecSel v -> [ConLike]
pr_cons = [ConLike]
cons }) = (Nablas -> DsM (CheckResult (PmRecSel Id)))
-> CheckAction (PmRecSel Id)
forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a
CA ((Nablas -> DsM (CheckResult (PmRecSel Id)))
 -> CheckAction (PmRecSel Id))
-> (Nablas -> DsM (CheckResult (PmRecSel Id)))
-> CheckAction (PmRecSel Id)
forall a b. (a -> b) -> a -> b
$ \Nablas
inc -> do
  arg_id <- case CoreExpr
arg of
           Var Id
arg_id -> Id -> IOEnv (Env DsGblEnv DsLclEnv) Id
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Id
arg_id
           CoreExpr
_ -> PredType -> IOEnv (Env DsGblEnv DsLclEnv) Id
mkPmId (PredType -> IOEnv (Env DsGblEnv DsLclEnv) Id)
-> PredType -> IOEnv (Env DsGblEnv DsLclEnv) Id
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CoreExpr -> PredType
CoreExpr -> PredType
exprType CoreExpr
arg

  let con_cts = (ConLike -> PhiCt) -> [ConLike] -> [PhiCt]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> PmAltCon -> PhiCt
PhiNotConCt Id
arg_id (PmAltCon -> PhiCt) -> (ConLike -> PmAltCon) -> ConLike -> PhiCt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConLike -> PmAltCon
PmAltConLike) [ConLike]
cons
      arg_ct  = Id -> CoreExpr -> PhiCt
PhiCoreCt Id
arg_id CoreExpr
arg
      phi_cts = [PhiCt] -> Bag PhiCt
forall a. [a] -> Bag a
listToBag (PhiCt
arg_ct PhiCt -> [PhiCt] -> [PhiCt]
forall a. a -> [a] -> [a]
: [PhiCt]
con_cts)
  unc <- addPhiCtsNablas inc phi_cts
  pure CheckResult { cr_ret = pr{ pr_arg_var = arg_id }, cr_uncov = unc, cr_approx = mempty }


{- Note [Checking EmptyCase]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-XEmptyCase is useful for matching on empty data types like 'Void'. For example,
the following is a complete match:

    f :: Void -> ()
    f x = case x of {}

Really, -XEmptyCase is the only way to write a program that at the same time is
safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
exception into divergence (@f x = f x@).

Semantically, unlike every other case expression, -XEmptyCase is strict in its
match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
initial Nabla and check if there are any values left to match on.

Note [Dead bang patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  f :: Bool -> Int
  f True = 1
  f !x   = 2

Whenever we fall through to the second equation, we will already have evaluated
the argument. Thus, the bang pattern serves no purpose and should be warned
about. We call this kind of bang patterns "dead". Dead bangs are the ones
that under no circumstances can force a thunk that wasn't already forced.
Dead bangs are a form of redundant bangs; see below.

We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable
where the PmBang appears in 'checkGrd'. If not, then clearly the bang is
dead. So for a source bang, we add the refined Nabla and the source info to
the 'RedSet's 'rs_bangs'. When collecting stuff to warn, we test that Nabla for
inhabitants. If it's empty, we'll warn that it's redundant.

Note that we don't want to warn for a dead bang that appears on a redundant
clause. That is because in that case, we recommend to delete the clause wholly,
including its leading pattern match.

Dead bang patterns are redundant. But there are bang patterns which are
redundant that aren't dead, for example

  f !() = 0

the bang still forces the match variable, before we attempt to match on (). But
it is redundant with the forcing done by the () match. We currently don't
detect redundant bangs that aren't dead.

Note [Countering exponential blowup]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Precise pattern match exhaustiveness checking is necessarily exponential in
the size of some input programs. We implement a counter-measure in the form of
the -fmax-pmcheck-models flag, limiting the number of Nablas we check against
each pattern by a constant.

How do we do that? Consider

  f True True = ()
  f True True = ()

And imagine we set our limit to 1 for the sake of the example. The first clause
will be checked against the initial Nabla, {}. Doing so will produce an
Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
Also we find the first clause to cover the model {x~True,y~True}.

But the Uncovered set we get out of the match is too huge! We somehow have to
ensure not to make things worse as they are already, so we continue checking
with a singleton Uncovered set of the initial Nabla {}. Why is this
sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
to forgetting that we matched against the first clause. The values represented
by {} are a superset of those represented by its two refinements {x≁True} and
{x~True,y≁True}.

This forgetfulness becomes very apparent in the example above: By continuing
with {} we don't detect the second clause as redundant, as it again covers the
same non-empty subset of {}. So we don't flag everything as redundant anymore,
but still will never flag something as redundant that isn't.

For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
and report @f _ _@ as missing, which is a superset of the actual missing
matches. But soundness means we will never fail to report a missing match.

This mechanism is implemented in 'throttle'.

Guards are an extreme example in this regard, with #11195 being a particularly
dreadful example: Since their RHS are often pretty much unique, we split on a
variable (the one representing the RHS) that doesn't occur anywhere else in the
program, so we don't actually get useful information out of that split!

Note [considerAccessible]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (T18610)

  f :: Bool -> Int
  f x = case (x, x) of
    (True,  True)  -> 1
    (False, False) -> 2
    (True,  False) -> 3 -- Warning: Redundant

The third case is detected as redundant. But it may be the intent of the
programmer to keep the dead code, in order for it not to bitrot or to support
debugging scenarios. But there is no way to communicate that to the
pattern-match checker! The only way is to deactivate pattern-match checking
whole-sale, which is quite annoying. Hence, we define in "GHC.Exts":

  considerAccessible = True

'considerAccessible' is treated specially by the pattern-match checker in that a
guard with it as the scrutinee expression will keep its parent clause alive:

  g :: Bool -> Int
  g x = case (x, x) of
    (True,  True)  -> 1
    (False, False) -> 2
    (True,  False) | GHC.Exts.considerAccessible -> 3 -- No warning

The key bits of the implementation are:

  1. Its definition is recognised as known-key (see "GHC.Builtin.Names").
  2. After "GHC.HsToCore.Pmc.Desugar", the guard will end up as a 'PmCon', where
     the match var is the known-key 'considerAccessible' and the constructor
     against which it matches is 'True'.
  3. We recognise the 'PmCon' in 'GHC.HsToCore.Check.checkGrd' and inflate the
     incoming set of values for all guards downstream to the unconstrained
     'initNablas' set, e.g. /all/ values.
     (The set of values that falls through that particular guard is empty, as
     matching 'considerAccessible' against 'True' can't fail.)

Note that 'considerAccessible' breaks the invariant that incoming sets of values
reaching syntactic children are subsets of that of the syntactic ancestor:
A whole match, like that of the third clause of the example, might have no
incoming value, but its single RHS has incoming values because of (3).

That means the 'is_covered' flag computed in 'GHC.HsToCore.Pmc.cirbsMatch'
is irrelevant and should not be used to flag all children as redundant (which is
what we used to do).

We achieve great benefits with a very simple implementation.
There are caveats, though:

  (A) Putting potentially failing guards /after/ the
      'considerAccessible' guard might lead to weird check results, e.g.,

        h :: Bool -> Int
        h x = case (x, x) of
          (True,  True)  -> 1
          (False, False) -> 2
          (True,  False) | GHC.Exts.considerAccessible, False <- x -> 3
          -- Warning: Not matched: (_, _)

      That *is* fixable, although we would pay with a much more complicated
      implementation.
  (B) If the programmer puts a 'considerAccessible' marker on an accessible
      clause, the checker doesn't warn about it. E.g.,

        f :: Bool -> Int
        f True | considerAccessible = 0
        f False = 1

      will not emit any warning whatsoever. We could implement code that warns
      here, but it wouldn't be as simple as it is now.
-}