Commit 7915afc6 authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot

Encode shape information in `PmOracle`

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.

This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).

Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149

-------------------------
Metric Decrease:
    ManyAlternatives
    T11195
-------------------------
parent b5ae3868
......@@ -25,9 +25,9 @@ module NameEnv (
emptyDNameEnv,
lookupDNameEnv,
delFromDNameEnv,
delFromDNameEnv, filterDNameEnv,
mapDNameEnv,
alterDNameEnv,
adjustDNameEnv, alterDNameEnv, extendDNameEnv,
-- ** Dependency analysis
depAnal
) where
......@@ -151,8 +151,17 @@ lookupDNameEnv = lookupUDFM
delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a
delFromDNameEnv = delFromUDFM
filterDNameEnv :: (a -> Bool) -> DNameEnv a -> DNameEnv a
filterDNameEnv = filterUDFM
mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
mapDNameEnv = mapUDFM
adjustDNameEnv :: (a -> a) -> DNameEnv a -> Name -> DNameEnv a
adjustDNameEnv = adjustUDFM
alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
alterDNameEnv = alterUDFM
extendDNameEnv :: DNameEnv a -> Name -> a -> DNameEnv a
extendDNameEnv = addToUDFM
......@@ -184,6 +184,20 @@ to get the instantiation a := ty.
This is very unlike DataCons, where univ tyvars match 1-1 the
arguments of the TyCon.
Side note: I (SG) get the impression that instantiated return types should
generate a *required* constraint for pattern synonyms, rather than a *provided*
constraint like it's the case for GADTs. For example, I'd expect these
declarations to have identical semantics:
pattern Just42 :: Maybe Int
pattern Just42 = Just 42
pattern Just'42 :: (a ~ Int) => Maybe a
pattern Just'42 = Just 42
The latter generates the proper required constraint, the former does not.
Also rather different to GADTs is the fact that Just42 doesn't have any
universally quantified type variables, whereas Just'42 or MkS above has.
Note [Pattern synonym representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -11,21 +11,28 @@ Pattern Matching Coverage Checking.
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE LambdaCase #-}
module Check (
-- Checking and printing
checkSingle, checkMatches, checkGuardMatches, isAnyPmCheckEnabled,
checkSingle, checkMatches, checkGuardMatches,
needToRunPmCheck, isMatchContextPmChecked,
-- See Note [Type and Term Equality Propagation]
genCaseTmCs1, genCaseTmCs2
addTyCsDs, addScrutTmCs, addPatTmCs
) where
#include "HsVersions.h"
import GhcPrelude
import TmOracle
import PmExpr
import PmOracle
import PmPpr
import BasicTypes (Origin, isGenerated)
import CoreSyn (CoreExpr, Expr(Var))
import CoreUtils (exprType)
import FastString (unpackFS)
import Unify( tcMatchTy )
import DynFlags
import HsSyn
......@@ -33,42 +40,37 @@ import TcHsSyn
import Id
import ConLike
import Name
import FamInstEnv
import TysPrim (tYPETyCon)
import FamInst
import TysWiredIn
import TyCon
import SrcLoc
import Util
import Outputable
import FastString
import DataCon
import PatSyn
import HscTypes (CompleteMatch(..))
import BasicTypes (Boxity(..))
import Var (EvVar)
import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr)
import MatchLit (dsLit, dsOverLit)
import DsMonad
import TcSimplify (tcCheckSatisfiability)
import TcType (isStringTy)
import Bag
import ErrUtils
import Var (EvVar)
import TyCoRep
import Type
import UniqSupply
import DsUtils (isTrueLHsExpr)
import Maybes (isJust, expectJust)
import qualified GHC.LanguageExtensions as LangExt
import Data.List (find)
import Data.Maybe (catMaybes, isJust, fromMaybe)
import Control.Monad (forM, when, forM_, zipWithM, filterM)
import Control.Monad (forM, when, forM_)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe
import Coercion
import TcEvidence
import TcSimplify (tcNormalise)
import IOEnv
import qualified Data.Semigroup as Semi
import ListT (ListT(..), fold, select)
{-
This module checks pattern matches for:
\begin{enumerate}
......@@ -91,98 +93,44 @@ The algorithm is based on the paper:
%************************************************************************
-}
-- We use the non-determinism monad to apply the algorithm to several
-- possible sets of constructors. Users can specify complete sets of
-- constructors by using COMPLETE pragmas.
-- The algorithm only picks out constructor
-- sets deep in the bowels which makes a simpler `mapM` more difficult to
-- implement. The non-determinism is only used in one place, see the ConVar
-- case in `pmCheckHd`.
data PmPat where
-- | For the arguments' meaning see 'HsPat.ConPatOut'.
PmCon :: { pm_con_con :: PmAltCon
, pm_con_arg_tys :: [Type]
, pm_con_tvs :: [TyVar]
, pm_con_args :: [PmPat] } -> PmPat
type PmM a = ListT DsM a
PmVar :: { pm_var_id :: Id } -> PmPat
liftD :: DsM a -> PmM a
liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
PmGrd :: { pm_grd_pv :: PatVec -- ^ Always has 'patVecArity' 1.
, pm_grd_expr :: CoreExpr } -> PmPat
-- (PmGrd pat expr) matches expr against pat, binding the variables in pat
-- Pick the first match complete covered match or otherwise the "best" match.
-- The best match is the one with the least uncovered clauses, ties broken
-- by the number of inaccessible clauses followed by number of redundant
-- clauses.
--
-- This is specified in the
-- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
-- users' guide. If you update the implementation of this function, make sure
-- to update that section of the users' guide as well.
getResult :: PmM PmResult -> DsM PmResult
getResult ls
= do { res <- fold ls goM (pure Nothing)
; case res of
Nothing -> panic "getResult is empty"
Just a -> return a }
where
goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
goM mpm dpm = do { pmr <- dpm
; return $ Just $ go pmr mpm }
-- Careful not to force unecessary results
go :: Maybe PmResult -> PmResult -> PmResult
go Nothing rs = rs
go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
| null us && null rs && null is = old
| otherwise =
let PmResult prov' rs' (UncoveredPatterns us') is' = new
in case compareLength us us'
`mappend` (compareLength is is')
`mappend` (compareLength rs rs')
`mappend` (compare prov prov') of
GT -> new
EQ -> new
LT -> old
go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
= panic "getResult: No inhabitation candidates"
data PatTy = PAT | VA -- Used only as a kind, to index PmPat
-- The *arity* of a PatVec [p1,..,pn] is
-- the number of p1..pn that are not Guards
data PmPat :: PatTy -> * where
PmCon :: { pm_con_con :: ConLike
, pm_con_arg_tys :: [Type]
, pm_con_tvs :: [TyVar]
, pm_con_dicts :: [EvVar]
, pm_con_args :: [PmPat t] } -> PmPat t
-- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
PmVar :: { pm_var_id :: Id } -> PmPat t
PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
PmNLit :: { pm_lit_id :: Id
, pm_lit_not :: [PmLit] } -> PmPat 'VA
PmGrd :: { pm_grd_pv :: PatVec
, pm_grd_expr :: PmExpr } -> PmPat 'PAT
-- | A fake guard pattern (True <- _) used to represent cases we cannot handle.
PmFake :: PmPat 'PAT
PmFake :: PmPat
instance Outputable (PmPat a) where
ppr = pprPmPatDebug
-- | Should not be user-facing.
instance Outputable PmPat where
ppr (PmCon alt _arg_tys _con_tvs con_args)
= cparen (notNull con_args) (hsep [ppr alt, hsep (map ppr con_args)])
ppr (PmVar vid) = ppr vid
ppr (PmGrd pv ge) = hsep (map ppr pv) <+> text "<-" <+> ppr ge
ppr PmFake = text "<PmFake>"
-- data T a where
-- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
-- or MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
type Pattern = PmPat 'PAT -- ^ Patterns
type ValAbs = PmPat 'VA -- ^ Value Abstractions
type PatVec = [Pattern] -- ^ Pattern Vectors
data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions
-- | Pattern Vectors. The *arity* of a PatVec [p1,..,pn] is
-- the number of p1..pn that are not Guards. See 'patternArity'.
type PatVec = [PmPat]
type ValVec = [Id] -- ^ Value Vector Abstractions
-- | Term and type constraints to accompany each value vector abstraction.
-- For efficiency, we store the term oracle state instead of the term
-- constraints. TODO: Do the same for the type constraints?
data Delta = MkDelta { delta_ty_cs :: Bag EvVar
, delta_tm_cs :: TmState }
type ValSetAbs = [ValVec] -- ^ Value Set Abstractions
type Uncovered = ValSetAbs
-- | 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
......@@ -199,8 +147,7 @@ data Covered = Covered | NotCovered
deriving Show
instance Outputable Covered where
ppr (Covered) = text "Covered"
ppr (NotCovered) = text "NotCovered"
ppr = text . show
-- Like the or monoid for booleans
-- Covered = True, Uncovered = False
......@@ -217,8 +164,7 @@ data Diverged = Diverged | NotDiverged
deriving Show
instance Outputable Diverged where
ppr Diverged = text "Diverged"
ppr NotDiverged = text "NotDiverged"
ppr = text . show
instance Semi.Semigroup Diverged where
Diverged <> _ = Diverged
......@@ -229,55 +175,36 @@ instance Monoid Diverged where
mempty = NotDiverged
mappend = (Semi.<>)
-- | When we learned that a given match group is complete
data Provenance =
FromBuiltin -- ^ From the original definition of the type
-- constructor.
| FromComplete -- ^ From a user-provided @COMPLETE@ pragma
deriving (Show, Eq, Ord)
instance Outputable Provenance where
ppr = text . show
instance Semi.Semigroup Provenance where
FromComplete <> _ = FromComplete
_ <> FromComplete = FromComplete
_ <> _ = FromBuiltin
instance Monoid Provenance where
mempty = FromBuiltin
mappend = (Semi.<>)
-- | A triple <C,U,D> of covered, uncovered, and divergent sets.
data PartialResult = PartialResult {
presultProvenance :: Provenance
-- keep track of provenance because we don't want
-- to warn about redundant matches if the result
-- is contaminated with a COMPLETE pragma
, presultCovered :: Covered
presultCovered :: Covered
, presultUncovered :: Uncovered
, presultDivergent :: Diverged }
instance Outputable PartialResult where
ppr (PartialResult prov c vsa d)
= text "PartialResult" <+> ppr prov <+> ppr c
<+> ppr d <+> ppr vsa
emptyPartialResult :: PartialResult
emptyPartialResult = PartialResult { presultUncovered = mempty
, presultCovered = mempty
, presultDivergent = mempty }
combinePartialResults :: PartialResult -> PartialResult -> PartialResult
combinePartialResults (PartialResult cs1 vsa1 ds1) (PartialResult cs2 vsa2 ds2)
= PartialResult (cs1 Semi.<> cs2)
(vsa1 Semi.<> vsa2)
(ds1 Semi.<> ds2)
instance Semi.Semigroup PartialResult where
(PartialResult prov1 cs1 vsa1 ds1)
<> (PartialResult prov2 cs2 vsa2 ds2)
= PartialResult (prov1 Semi.<> prov2)
(cs1 Semi.<> cs2)
(vsa1 Semi.<> vsa2)
(ds1 Semi.<> ds2)
instance Outputable PartialResult where
ppr (PartialResult c vsa d)
= hang (text "PartialResult" <+> ppr c <+> ppr d) 2 (ppr_vsa vsa)
where
ppr_vsa = braces . fsep . punctuate comma . map ppr
instance Semi.Semigroup PartialResult where
(<>) = combinePartialResults
instance Monoid PartialResult where
mempty = PartialResult mempty mempty [] mempty
mempty = emptyPartialResult
mappend = (Semi.<>)
-- newtype ChoiceOf a = ChoiceOf [a]
-- | Pattern check result
--
-- * Redundant clauses
......@@ -291,15 +218,13 @@ instance Monoid PartialResult where
--
data PmResult =
PmResult {
pmresultProvenance :: Provenance
, pmresultRedundant :: [Located [LPat GhcTc]]
pmresultRedundant :: [Located [LPat GhcTc]]
, pmresultUncovered :: UncoveredCandidates
, pmresultInaccessible :: [Located [LPat GhcTc]] }
instance Outputable PmResult where
ppr pmr = hang (text "PmResult") 2 $ vcat
[ text "pmresultProvenance" <+> ppr (pmresultProvenance pmr)
, text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
[ text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
, text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
, text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
]
......@@ -315,21 +240,13 @@ instance Outputable PmResult where
-- but we don't want to issue just a wildcard as missing. Instead, we print a
-- type annotated wildcard, so that the user knows what kind of patterns is
-- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
data UncoveredCandidates = UncoveredPatterns Uncovered
data UncoveredCandidates = UncoveredPatterns [Id] [Delta]
| TypeOfUncovered Type
instance Outputable UncoveredCandidates where
ppr (UncoveredPatterns uc) = text "UnPat" <+> ppr uc
ppr (UncoveredPatterns vva deltas) = text "UnPat" <+> ppr vva $$ ppr deltas
ppr (TypeOfUncovered ty) = text "UnTy" <+> ppr ty
-- | The empty pattern check result
emptyPmResult :: PmResult
emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
-- | Non-exhaustive empty case with unknown/trivial inhabitants
uncoveredWithTy :: Type -> PmResult
uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
{-
%************************************************************************
%* *
......@@ -341,27 +258,28 @@ uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
-- | Check a single pattern binding (let)
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
mb_pm_res <- tryM (getResult (checkSingle' locn var p))
tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
mb_pm_res <- tryM (checkSingle' locn var p)
case mb_pm_res of
Left _ -> warnPmIters dflags ctxt
Right res -> dsPmWarn dflags ctxt res
-- | Check a single pattern binding (let)
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
checkSingle' locn var p = do
liftD resetPmIterDs -- set the iter-no to zero
fam_insts <- liftD dsGetFamInstEnvs
clause <- liftD $ translatePat fam_insts p
missing <- mkInitialUncovered [var]
tracePm "checkSingle': missing" (vcat (map pprValVecDebug missing))
-- no guards
PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
let us' = UncoveredPatterns us
resetPmIterDs -- set the iter-no to zero
fam_insts <- dsGetFamInstEnvs
clause <- translatePat fam_insts p
missing <- getPmDelta
tracePm "checkSingle': missing" (ppr missing)
PartialResult cs us ds <- pmcheckI clause [] [var] 1 missing
dflags <- getDynFlags
us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us
let uc = UncoveredPatterns [var] us'
return $ case (cs,ds) of
(Covered, _ ) -> PmResult prov [] us' [] -- useful
(NotCovered, NotDiverged) -> PmResult prov m us' [] -- redundant
(NotCovered, Diverged ) -> PmResult prov [] us' m -- inaccessible rhs
(Covered, _ ) -> PmResult [] uc [] -- useful
(NotCovered, NotDiverged) -> PmResult m uc [] -- redundant
(NotCovered, Diverged ) -> PmResult [] uc m -- inaccessible rhs
where m = [cL locn [cL locn p]]
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
......@@ -385,14 +303,14 @@ checkGuardMatches _ (XGRHSs nec) = noExtCon nec
checkMatches :: DynFlags -> DsMatchContext
-> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
checkMatches dflags ctxt vars matches = do
tracePmD "checkMatches" (hang (vcat [ppr ctxt
tracePm "checkMatches" (hang (vcat [ppr ctxt
, ppr vars
, text "Matches:"])
2
(vcat (map ppr matches)))
mb_pm_res <- tryM $ getResult $ case matches of
mb_pm_res <- tryM $ case matches of
-- Check EmptyCase separately
-- See Note [Checking EmptyCase Expressions]
-- See Note [Checking EmptyCase Expressions] in PmOracle
[] | [var] <- vars -> checkEmptyCase' var
_normal_match -> checkMatches' vars matches
case mb_pm_res of
......@@ -401,42 +319,42 @@ checkMatches dflags ctxt vars matches = do
-- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
-- list of matches. For empty case expressions, use checkEmptyCase' instead.
checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
checkMatches' vars matches
| null matches = panic "checkMatches': EmptyCase"
| otherwise = do
liftD resetPmIterDs -- set the iter-no to zero
missing <- mkInitialUncovered vars
tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
(prov, rs,us,ds) <- go matches missing
resetPmIterDs -- set the iter-no to zero
missing <- getPmDelta
tracePm "checkMatches': missing" (ppr missing)
(rs,us,ds) <- go matches [missing]
dflags <- getDynFlags
us' <- getNFirstUncovered vars (maxUncoveredPatterns dflags + 1) us
let up = UncoveredPatterns vars us'
return $ PmResult {
pmresultProvenance = prov
, pmresultRedundant = map hsLMatchToLPats rs
, pmresultUncovered = UncoveredPatterns us
pmresultRedundant = map hsLMatchToLPats rs
, pmresultUncovered = up
, pmresultInaccessible = map hsLMatchToLPats ds }
where
go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
-> PmM (Provenance
, [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM ( [LMatch GhcTc (LHsExpr GhcTc)]
, Uncovered
, [LMatch GhcTc (LHsExpr GhcTc)])
go [] missing = return (mempty, [], missing, [])
go [] missing = return ([], missing, [])
go (m:ms) missing = do
tracePm "checkMatches': go" (ppr m $$ ppr missing)
fam_insts <- liftD dsGetFamInstEnvs
(clause, guards) <- liftD $ translateMatch fam_insts m
r@(PartialResult prov cs missing' ds)
<- runMany (pmcheckI clause guards) missing
tracePm "checkMatches': go" (ppr m)
fam_insts <- dsGetFamInstEnvs
(clause, guards) <- translateMatch fam_insts m
r@(PartialResult cs missing' ds)
<- runMany (pmcheckI clause guards vars (length missing)) missing
tracePm "checkMatches': go: res" (ppr r)
(ms_prov, rs, final_u, is) <- go ms missing'
let final_prov = prov `mappend` ms_prov
(rs, final_u, is) <- go ms missing'
return $ case (cs, ds) of
-- useful
(Covered, _ ) -> (final_prov, rs, final_u, is)
(Covered, _ ) -> (rs, final_u, is)
-- redundant
(NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
(NotCovered, NotDiverged) -> (m:rs, final_u,is)
-- inaccessible
(NotCovered, Diverged ) -> (final_prov, rs, final_u, m:is)
(NotCovered, Diverged ) -> (rs, final_u, m:is)
hsLMatchToLPats :: LMatch id body -> Located [LPat id]
hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
......@@ -444,472 +362,59 @@ checkMatches' vars matches
-- | Check an empty case expression. Since there are no clauses to process, we
-- only compute the uncovered set. See Note [Checking EmptyCase Expressions]
-- for details.
checkEmptyCase' :: Id -> PmM PmResult
checkEmptyCase' var = do
tm_ty_css <- pmInitialTmTyCs
mb_candidates <- inhabitationCandidates (delta_ty_cs tm_ty_css) (idType var)
case mb_candidates of
-- in "PmOracle" for details.
checkEmptyCase' :: Id -> DsM PmResult
checkEmptyCase' x = do
delta <- getPmDelta
us <- inhabitants delta (idType x) >>= \case
-- Inhabitation checking failed / the type is trivially inhabited
Left ty -> return (uncoveredWithTy ty)
-- A list of inhabitant candidates is available: Check for each
-- one for the satisfiability of the constraints it gives rise to.
Right (_, candidates) -> do
missing_m <- flip mapMaybeM candidates $
\InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
, ic_ty_cs = ty_cs
, ic_strict_arg_tys = strict_arg_tys } -> do
mb_sat <- pmIsSatisfiable tm_ty_css tm_ct ty_cs strict_arg_tys
pure $ fmap (ValVec [va]) mb_sat
return $ if null missing_m
then emptyPmResult
else PmResult FromBuiltin [] (UncoveredPatterns missing_m) []
-- | Returns 'True' if the argument 'Type' is a fully saturated application of
-- a closed type constructor.
--
-- Closed type constructors are those with a fixed right hand side, as
-- opposed to e.g. associated types. These are of particular interest for
-- pattern-match coverage checking, because GHC can exhaustively consider all
-- possible forms that values of a closed type can take on.
--
-- Note that this function is intended to be used to check types of value-level
-- patterns, so as a consequence, the 'Type' supplied as an argument to this
-- function should be of kind @Type@.
pmIsClosedType :: Type -> Bool
pmIsClosedType ty
= case splitTyConApp_maybe ty of
Just (tc, ty_args)
| is_algebraic_like tc && not (isFamilyTyCon tc)
-> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
_other -> False
where
-- This returns True for TyCons which /act like/ algebraic types.
-- (See "Type#type_classification" for what an algebraic type is.)
--
-- This is qualified with \"like\" because of a particular special
-- case: TYPE (the underlyind kind behind Type, among others). TYPE
-- is conceptually a datatype (and thus algebraic), but in practice it is
-- a primitive builtin type, so we must check for it specially.
--
-- NB: it makes sense to think of TYPE as a closed type in a value-level,
-- pattern-matching context. However, at the kind level, TYPE is certainly
-- not closed! Since this function is specifically tailor