diff options
Diffstat (limited to 'compiler/deSugar/Check.hs')
| -rw-r--r-- | compiler/deSugar/Check.hs | 2316 |
1 files changed, 629 insertions, 1687 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index 602c125f67..3a1515d0cc 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -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 tailored towards pattern - -- matching, however, it's OK to label TYPE as closed. - is_algebraic_like :: TyCon -> Bool - is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon - -pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type - -> PmM (Maybe (Type, [DataCon], Type)) --- ^ Get rid of *outermost* (or toplevel) --- * type function redex --- * data family redex --- * newtypes --- --- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a --- coercion, it returns useful information for issuing pattern matching --- warnings. See Note [Type normalisation for EmptyCase] for details. --- --- NB: Normalisation can potentially change kinds, if the head of the type --- is a type family with a variable result kind. I (Richard E) can't think --- of a way to cause trouble here, though. -pmTopNormaliseType_maybe env ty_cs typ - = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs typ - -- Before proceeding, we chuck typ into the constraint solver, in case - -- solving for given equalities may reduce typ some. See - -- "Wrinkle: local equalities" in - -- Note [Type normalisation for EmptyCase]. - pure $ do typ' <- mb_typ' - ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ' - -- We need to do topNormaliseTypeX in addition to tcNormalise, - -- since topNormaliseX looks through newtypes, which - -- tcNormalise does not do. - Just (eq_src_ty ty (typ' : ty_f [ty]), tm_f [], ty) - where - -- Find the first type in the sequence of rewrites that is a data type, - -- newtype, or a data family application (not the representation tycon!). - -- This is the one that is equal (in source Haskell) to the initial type. - -- If none is found in the list, then all of them are type family - -- applications, so we simply return the last one, which is the *simplest*. - eq_src_ty :: Type -> [Type] -> Type - eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys) - - is_closed_or_data_family :: Type -> Bool - is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty - - -- For efficiency, represent both lists as difference lists. - -- comb performs the concatenation, for both lists. - comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2) - - stepper = newTypeStepper `composeSteppers` tyFamStepper - - -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into - -- a loop. If it would fall into a loop, it produces 'NS_Abort'. - newTypeStepper :: NormaliseStepper ([Type] -> [Type],[DataCon] -> [DataCon]) - newTypeStepper rec_nts tc tys - | Just (ty', _co) <- instNewTyCon_maybe tc tys - = case checkRecTc rec_nts tc of - Just rec_nts' -> let tyf = ((TyConApp tc tys):) - tmf = ((tyConSingleDataCon tc):) - in NS_Step rec_nts' ty' (tyf, tmf) - Nothing -> NS_Abort - | otherwise - = NS_Done - - tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon]) - tyFamStepper rec_nts tc tys -- Try to step a type/data family - = let (_args_co, ntys, _res_co) = normaliseTcArgs env Representational tc tys in - -- NB: It's OK to use normaliseTcArgs here instead of - -- normalise_tc_args (which takes the LiftingContext described - -- in Note [Normalising types]) because the reduceTyFamApp below - -- works only at top level. We'll never recur in this function - -- after reducing the kind of a bound tyvar. - - case reduceTyFamApp_maybe env Representational tc ntys of - Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id) - _ -> NS_Done - --- | Determine suitable constraints to use at the beginning of pattern-match --- coverage checking by consulting the sets of term and type constraints --- currently in scope. If one of these sets of constraints is unsatisfiable, --- use an empty set in its place. (See --- @Note [Recovering from unsatisfiable pattern-matching constraints]@ --- for why this is done.) -pmInitialTmTyCs :: PmM Delta -pmInitialTmTyCs = do - ty_cs <- liftD getDictsDs - tm_cs <- bagToList <$> liftD getTmCsDs - sat_ty <- tyOracle ty_cs - let initTyCs = if sat_ty then ty_cs else emptyBag - initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs) - pure $ MkDelta{ delta_tm_cs = initTmState, delta_ty_cs = initTyCs } + Left ty -> pure (TypeOfUncovered ty) + -- A list of oracle states for the different satisfiable constructors is + -- available. Turn this into a value set abstraction. + Right (va, deltas) -> pure (UncoveredPatterns [va] deltas) + pure (PmResult [] us []) + +getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta] +getNFirstUncovered _ 0 _ = pure [] +getNFirstUncovered _ _ [] = pure [] +getNFirstUncovered vars n (delta:deltas) = do + front <- provideEvidenceForEquation vars n delta + back <- getNFirstUncovered vars (n - length front) deltas + pure (front ++ back) + +-- | The maximum successive number of refinements ('refineToAltCon') we allow +-- per representative. See Note [Limit the number of refinements]. +mAX_REFINEMENTS :: Int +-- The current number is chosen so that PrelRules is still checked with +-- reasonable performance. If this is set to below 2, ds022 will start to fail. +-- Although that is probably due to the fact that we always increase the +-- refinement counter instead of just increasing it when the contraposition +-- is satisfiable (when the not taken case 'addRefutableAltCon' is +-- satisfiable, that is). That would be the first thing I'd try if we have +-- performance problems on one test while decreasing the threshold leads to +-- other tests being broken like ds022 above. +mAX_REFINEMENTS = 3 + +-- | The threshold for detecting exponential blow-up in the number of 'Delta's +-- to check introduced by guards. +tHRESHOLD_GUARD_DELTAS :: Int +tHRESHOLD_GUARD_DELTAS = 100 + +-- | Multiply the estimated number of 'Delta's to process by a constant +-- branching factor induced by a guard and return the new estimate if it +-- doesn't exceed a constant threshold. +-- See 6. in Note [Guards and Approximation]. +tryMultiplyDeltas :: Int -> Int -> Maybe Int +tryMultiplyDeltas multiplier n_delta + -- The ^2 below is intentional: We want to give up on guards with a large + -- branching factor rather quickly, still leaving room for small informative + -- ones later on. + | n_delta*multiplier^(2::Int) < tHRESHOLD_GUARD_DELTAS + = Just (n_delta*multiplier) + | otherwise + = Nothing {- -Note [Recovering from unsatisfiable pattern-matching constraints] -~~~~~~~~~~~~~~~~ -Consider the following code (see #12957 and #15450): - - f :: Int ~ Bool => () - f = case True of { False -> () } - -We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC -used not to do this; in fact, it would warn that the match was /redundant/! -This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the -coverage checker deems any matches with unsatifiable constraint sets to be -unreachable. - -We decide to better than this. When beginning coverage checking, we first -check if the constraints in scope are unsatisfiable, and if so, we start -afresh with an empty set of constraints. This way, we'll get the warnings -that we expect. --} - --- | Given a conlike's term constraints, type constraints, and strict argument --- types, check if they are satisfiable. --- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet --- Their Match paper.) --- --- For the purposes of efficiency, this takes as separate arguments the --- ambient term and type constraints (which are known beforehand to be --- satisfiable), as well as the new term and type constraints (which may not --- be satisfiable). This lets us implement two mini-optimizations: --- --- * If there are no new type constraints, then don't bother initializing --- the type oracle, since it's redundant to do so. --- * Since the new term constraint is a separate argument, we only need to --- execute one iteration of the term oracle (instead of traversing the --- entire set of term constraints). --- --- Taking strict argument types into account is something which was not --- discussed in GADTs Meet Their Match. For an explanation of what role they --- serve, see @Note [Extensions to GADTs Meet Their Match]@. -pmIsSatisfiable - :: Delta -- ^ The ambient term and type constraints - -- (known to be satisfiable). - -> TmVarCt -- ^ The new term constraint. - -> Bag EvVar -- ^ The new type constraints. - -> [Type] -- ^ The strict argument types. - -> PmM (Maybe Delta) - -- ^ @'Just' delta@ if the constraints (@delta@) are - -- satisfiable, and each strict argument type is inhabitable. - -- 'Nothing' otherwise. -pmIsSatisfiable amb_cs new_tm_c new_ty_cs strict_arg_tys = do - mb_sat <- tmTyCsAreSatisfiable amb_cs new_tm_c new_ty_cs - case mb_sat of - Nothing -> pure Nothing - Just delta -> do - -- We know that the term and type constraints are inhabitable, so now - -- check if each strict argument type is inhabitable. - all_non_void <- checkAllNonVoid initRecTc delta strict_arg_tys - pure $ if all_non_void -- Check if each strict argument type - -- is inhabitable - then Just delta - else Nothing - --- | Like 'pmIsSatisfiable', but only checks if term and type constraints are --- satisfiable, and doesn't bother checking anything related to strict argument --- types. -tmTyCsAreSatisfiable - :: Delta -- ^ The ambient term and type constraints - -- (known to be satisfiable). - -> TmVarCt -- ^ The new term constraint. - -> Bag EvVar -- ^ The new type constraints. - -> PmM (Maybe Delta) - -- ^ @'Just' delta@ if the constraints (@delta@) are - -- satisfiable. 'Nothing' otherwise. -tmTyCsAreSatisfiable - (MkDelta{ delta_tm_cs = amb_tm_cs, delta_ty_cs = amb_ty_cs }) - new_tm_c new_ty_cs = do - let ty_cs = new_ty_cs `unionBags` amb_ty_cs - sat_ty <- if isEmptyBag new_ty_cs - then pure True - else tyOracle ty_cs - pure $ case (sat_ty, solveOneEq amb_tm_cs new_tm_c) of - (True, Just term_cs) -> Just $ MkDelta{ delta_ty_cs = ty_cs - , delta_tm_cs = term_cs } - _unsat -> Nothing - --- | Implements two performance optimizations, as described in the --- \"Strict argument type constraints\" section of --- @Note [Extensions to GADTs Meet Their Match]@. -checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool -checkAllNonVoid rec_ts amb_cs strict_arg_tys = do - fam_insts <- liftD dsGetFamInstEnvs - let definitely_inhabited = - definitelyInhabitedType fam_insts (delta_ty_cs amb_cs) - tys_to_check <- filterOutM definitely_inhabited strict_arg_tys - let rec_max_bound | tys_to_check `lengthExceeds` 1 - = 1 - | otherwise - = defaultRecTcMaxBound - rec_ts' = setRecTcMaxBound rec_max_bound rec_ts - allM (nonVoid rec_ts' amb_cs) tys_to_check - --- | Checks if a strict argument type of a conlike is inhabitable by a --- terminating value (i.e, an 'InhabitationCandidate'). --- See @Note [Extensions to GADTs Meet Their Match]@. -nonVoid - :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit. - -> Delta -- ^ The ambient term/type constraints (known to be - -- satisfiable). - -> Type -- ^ The strict argument type. - -> PmM Bool -- ^ 'True' if the strict argument type might be inhabited by - -- a terminating value (i.e., an 'InhabitationCandidate'). - -- 'False' if it is definitely uninhabitable by anything - -- (except bottom). -nonVoid rec_ts amb_cs strict_arg_ty = do - mb_cands <- inhabitationCandidates (delta_ty_cs amb_cs) strict_arg_ty - case mb_cands of - Right (tc, cands) - | Just rec_ts' <- checkRecTc rec_ts tc - -> anyM (cand_is_inhabitable rec_ts' amb_cs) cands - -- A strict argument type is inhabitable by a terminating value if - -- at least one InhabitationCandidate is inhabitable. - _ -> pure True - -- Either the type is trivially inhabited or we have exceeded the - -- recursion depth for some TyCon (so bail out and conservatively - -- claim the type is inhabited). - where - -- Checks if an InhabitationCandidate for a strict argument type: - -- - -- (1) Has satisfiable term and type constraints. - -- (2) Has 'nonVoid' strict argument types (we bail out of this - -- check if recursion is detected). - -- - -- See Note [Extensions to GADTs Meet Their Match] - cand_is_inhabitable :: RecTcChecker -> Delta - -> InhabitationCandidate -> PmM Bool - cand_is_inhabitable rec_ts amb_cs - (InhabitationCandidate{ ic_tm_ct = new_term_c - , ic_ty_cs = new_ty_cs - , ic_strict_arg_tys = new_strict_arg_tys }) = do - mb_sat <- tmTyCsAreSatisfiable amb_cs new_term_c new_ty_cs - case mb_sat of - Nothing -> pure False - Just new_delta -> do - checkAllNonVoid rec_ts new_delta new_strict_arg_tys - --- | @'definitelyInhabitedType' ty@ returns 'True' if @ty@ has at least one --- constructor @C@ such that: --- --- 1. @C@ has no equality constraints. --- 2. @C@ has no strict argument types. --- --- See the \"Strict argument type constraints\" section of --- @Note [Extensions to GADTs Meet Their Match]@. -definitelyInhabitedType :: FamInstEnvs -> Bag EvVar -> Type -> PmM Bool -definitelyInhabitedType env ty_cs ty = do - mb_res <- pmTopNormaliseType_maybe env ty_cs ty - pure $ case mb_res of - Just (_, cons, _) -> any meets_criteria cons - Nothing -> False - where - meets_criteria :: DataCon -> Bool - meets_criteria con = - null (dataConEqSpec con) && -- (1) - null (dataConImplBangs con) -- (2) - -{- Note [Type normalisation for EmptyCase] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -EmptyCase is an exception for pattern matching, since it is strict. This means -that it boils down to checking whether the type of the scrutinee is inhabited. -Function pmTopNormaliseType_maybe gets rid of the outermost type function/data -family redex and newtypes, in search of an algebraic type constructor, which is -easier to check for inhabitation. - -It returns 3 results instead of one, because there are 2 subtle points: -1. Newtypes are isomorphic to the underlying type in core but not in the source - language, -2. The representational data family tycon is used internally but should not be - shown to the user - -Hence, if pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty), -then - (a) src_ty is the rewritten type which we can show to the user. That is, the - type we get if we rewrite type families but not data families or - newtypes. - (b) dcs is the list of data constructors "skipped", every time we normalise a - newtype to its core representation, we keep track of the source data - constructor. - (c) core_ty is the rewritten type. That is, - pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty) - implies - topNormaliseType_maybe env ty = Just (co, core_ty) - for some coercion co. - -To see how all cases come into play, consider the following example: - - data family T a :: * - data instance T Int = T1 | T2 Bool - -- Which gives rise to FC: - -- data T a - -- data R:TInt = T1 | T2 Bool - -- axiom ax_ti : T Int ~R R:TInt - - newtype G1 = MkG1 (T Int) - newtype G2 = MkG2 G1 - - type instance F Int = F Char - type instance F Char = G2 - -In this case pmTopNormaliseType_maybe env ty_cs (F Int) results in - - Just (G2, [MkG2,MkG1], R:TInt) - -Which means that in source Haskell: - - G2 is equivalent to F Int (in contrast, G1 isn't). - - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int). - ------ --- Wrinkle: Local equalities ------ - -Given the following type family: - - type family F a - type instance F Int = Void - -Should the following program (from #14813) be considered exhaustive? - - f :: (i ~ Int) => F i -> a - f x = case x of {} - -You might think "of course, since `x` is obviously of type Void". But the -idType of `x` is technically F i, not Void, so if we pass F i to -inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive. -In order to avoid this pitfall, we need to normalise the type passed to -pmTopNormaliseType_maybe, using the constraint solver to solve for any local -equalities (such as i ~ Int) that may be in scope. --} - --- | Generate all 'InhabitationCandidate's for a given type. The result is --- either @'Left' ty@, if the type cannot be reduced to a closed algebraic type --- (or if it's one trivially inhabited, like 'Int'), or @'Right' candidates@, --- if it can. In this case, the candidates are the signature of the tycon, each --- one accompanied by the term- and type- constraints it gives rise to. --- See also Note [Checking EmptyCase Expressions] -inhabitationCandidates :: Bag EvVar -> Type - -> PmM (Either Type (TyCon, [InhabitationCandidate])) -inhabitationCandidates ty_cs ty = do - fam_insts <- liftD dsGetFamInstEnvs - mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty - case mb_norm_res of - Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs - Nothing -> alts_to_check ty ty [] - where - -- All these types are trivially inhabited - trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon - , intTyCon, wordTyCon, word8TyCon ] - - -- Note: At the moment we leave all the typing and constraint fields of - -- PmCon empty, since we know that they are not gonna be used. Is the - -- right-thing-to-do to actually create them, even if they are never used? - build_tm :: ValAbs -> [DataCon] -> ValAbs - build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e]) - - -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe - alts_to_check :: Type -> Type -> [DataCon] - -> PmM (Either Type (TyCon, [InhabitationCandidate])) - alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of - Just (tc, tc_args) - | tc `elem` trivially_inhabited - -> case dcs of - [] -> return (Left src_ty) - (_:_) -> do var <- liftD $ mkPmId core_ty - let va = build_tm (PmVar var) dcs - return $ Right (tc, [InhabitationCandidate - { ic_val_abs = va, ic_tm_ct = mkIdEq var - , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }]) - - | pmIsClosedType core_ty && not (isAbstractTyCon tc) - -- Don't consider abstract tycons since we don't know what their - -- constructors are, which makes the results of coverage checking - -- them extremely misleading. - -> liftD $ do - var <- mkPmId core_ty -- it would be wrong to unify x - alts <- mapM (mkOneConFull var tc_args . RealDataCon) (tyConDataCons tc) - return $ Right - (tc, [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs} - | alt <- alts ]) - -- For other types conservatively assume that they are inhabited. - _other -> return (Left src_ty) - -{- Note [Checking EmptyCase Expressions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Empty case expressions are strict on the scrutinee. That is, `case x of {}` -will force argument `x`. Hence, `checkMatches` is not sufficient for checking -empty cases, because it assumes that the match is not strict (which is true -for all other cases, apart from EmptyCase). This gave rise to #10746. Instead, -we do the following: - -1. We normalise the outermost type family redex, data family redex or newtype, - using pmTopNormaliseType_maybe (in types/FamInstEnv.hs). This computes 3 - things: - (a) A normalised type src_ty, which is equal to the type of the scrutinee in - source Haskell (does not normalise newtypes or data families) - (b) The actual normalised type core_ty, which coincides with the result - topNormaliseType_maybe. This type is not necessarily equal to the input - type in source Haskell. And this is precicely the reason we compute (a) - and (c): the reasoning happens with the underlying types, but both the - patterns and types we print should respect newtypes and also show the - family type constructors and not the representation constructors. - - (c) A list of all newtype data constructors dcs, each one corresponding to a - newtype rewrite performed in (b). - - For an example see also Note [Type normalisation for EmptyCase] - in types/FamInstEnv.hs. - -2. Function checkEmptyCase' performs the check: - - If core_ty is not an algebraic type, then we cannot check for - inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming - that the type is inhabited. - - If core_ty is an algebraic type, then we unfold the scrutinee to all - possible constructor patterns, using inhabitationCandidates, and then - check each one for constraint satisfiability, same as we for normal - pattern match checking. - %************************************************************************ %* * Transform source syntax to *our* syntax @@ -920,14 +425,14 @@ we do the following: -- ----------------------------------------------------------------------- -- * Utilities -nullaryConPattern :: ConLike -> Pattern +nullaryConPattern :: ConLike -> PmPat -- Nullary data constructor and nullary type constructor nullaryConPattern con = - PmCon { pm_con_con = con, pm_con_arg_tys = [] - , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] } + PmCon { pm_con_con = (PmAltConLike con), pm_con_arg_tys = [] + , pm_con_tvs = [], pm_con_args = [] } {-# INLINE nullaryConPattern #-} -truePattern :: Pattern +truePattern :: PmPat truePattern = nullaryConPattern (RealDataCon trueDataCon) {-# INLINE truePattern #-} @@ -937,35 +442,54 @@ mkCanFailPmPat ty = do var <- mkPmVar ty return [var, PmFake] -vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern +vanillaConPattern :: ConLike -> [Type] -> PatVec -> PmPat -- ADT constructor pattern => no existentials, no local constraints vanillaConPattern con arg_tys args = - PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys - , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args } + PmCon { pm_con_con = PmAltConLike con, pm_con_arg_tys = arg_tys + , pm_con_tvs = [], pm_con_args = args } {-# INLINE vanillaConPattern #-} -- | Create an empty list pattern of a given type -nilPattern :: Type -> Pattern +nilPattern :: Type -> PmPat nilPattern ty = - PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty] - , pm_con_tvs = [], pm_con_dicts = [] - , pm_con_args = [] } + PmCon { pm_con_con = PmAltConLike (RealDataCon nilDataCon) + , pm_con_arg_tys = [ty], pm_con_tvs = [], pm_con_args = [] } {-# INLINE nilPattern #-} mkListPatVec :: Type -> PatVec -> PatVec -> PatVec -mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon +mkListPatVec ty xs ys = [PmCon { pm_con_con = PmAltConLike (RealDataCon consDataCon) , pm_con_arg_tys = [ty] - , pm_con_tvs = [], pm_con_dicts = [] + , pm_con_tvs = [] , pm_con_args = xs++ys }] {-# INLINE mkListPatVec #-} --- | Create a (non-overloaded) literal pattern -mkLitPattern :: HsLit GhcTc -> Pattern -mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit } -{-# INLINE mkLitPattern #-} +-- | Create a literal pattern +mkPmLitPattern :: PmLit -> PatVec +mkPmLitPattern lit@(PmLit _ val) + -- We translate String literals to list literals for better overlap reasoning. + -- It's a little unfortunate we do this here rather than in + -- 'PmOracle.trySolve' and 'PmOracle.addRefutableAltCon', but it's so much + -- simpler here. + -- See Note [Representation of Strings in TmState] in PmOracle + | PmLitString s <- val + , let mk_char_lit c = mkPmLitPattern (PmLit charTy (PmLitChar c)) + = foldr (\c p -> mkListPatVec charTy (mk_char_lit c) p) + [nilPattern charTy] + (unpackFS s) + | otherwise + = [PmCon { pm_con_con = PmAltLit lit + , pm_con_arg_tys = [] + , pm_con_tvs = [] + , pm_con_args = [] }] +{-# INLINE mkPmLitPattern #-} -- ----------------------------------------------------------------------- --- * Transform (Pat Id) into of (PmPat Id) +-- * Transform (Pat Id) into [PmPat] +-- The arity of the [PmPat] is always 1, but it may be a combination +-- of a vanilla pattern and a guard pattern. +-- Example: view pattern (f y -> Just x) +-- becomes [PmVar z, PmGrd [PmPat (Just x), f y]] +-- where z is fresh translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec translatePat fam_insts pat = case pat of @@ -977,12 +501,10 @@ translatePat fam_insts pat = case pat of -- ignore strictness annotations for now BangPat _ p -> translatePat fam_insts (unLoc p) - AsPat _ lid p -> do - -- Note [Translating As Patterns] - ps <- translatePat fam_insts (unLoc p) - let [e] = map vaToPmExpr (coercePatVec ps) - g = PmGrd [PmVar (unLoc lid)] e - return (ps ++ [g]) + -- (x@pat) ===> x (pat <- x) + AsPat _ (dL->L _ x) p -> do + pat <- translatePat fam_insts (unLoc p) + pure [PmVar x, PmGrd pat (Var x)] SigPat _ p _ty -> translatePat fam_insts (unLoc p) @@ -991,10 +513,10 @@ translatePat fam_insts pat = case pat of | isIdHsWrapper wrapper -> translatePat fam_insts p | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p | otherwise -> do - ps <- translatePat fam_insts p + ps <- translatePat fam_insts p (xp,xe) <- mkPmId2Forms ty g <- mkGuard ps (mkHsWrap wrapper (unLoc xe)) - return [xp,g] + pure [xp,g] -- (n + k) ===> x (True <- x >= k) (n <- x-k) NPlusKPat ty (dL->L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty @@ -1008,20 +530,20 @@ translatePat fam_insts pat = case pat of True -> do (xp,xe) <- mkPmId2Forms arg_ty g <- mkGuard ps (HsApp noExtField lexpr xe) - return [xp,g] + return [xp, g] False -> mkCanFailPmPat arg_ty -- list ListPat (ListPatTc ty Nothing) ps -> do - foldr (mkListPatVec ty) [nilPattern ty] - <$> translatePatVec fam_insts (map unLoc ps) + pv <- translatePatVec fam_insts (map unLoc ps) + return (foldr (mkListPatVec ty) [nilPattern ty] pv) -- overloaded list ListPat (ListPatTc _elem_ty (Just (pat_ty, _to_list))) lpats -> do dflags <- getDynFlags if xopt LangExt.RebindableSyntax dflags - then mkCanFailPmPat pat_ty - else case splitListTyConApp_maybe pat_ty of + then mkCanFailPmPat pat_ty + else case splitListTyConApp_maybe pat_ty of Just e_ty -> translatePat fam_insts (ListPat (ListPatTc e_ty Nothing) lpats) Nothing -> mkCanFailPmPat pat_ty @@ -1046,43 +568,50 @@ translatePat fam_insts pat = case pat of ConPatOut { pat_con = (dL->L _ con) , pat_arg_tys = arg_tys , pat_tvs = ex_tvs - , pat_dicts = dicts , pat_args = ps } -> do - groups <- allCompleteMatches con arg_tys + let ty = conLikeResTy con arg_tys + groups <- allCompleteMatches ty case groups of - [] -> mkCanFailPmPat (conLikeResTy con arg_tys) + [] -> mkCanFailPmPat ty _ -> do args <- translateConPatVec fam_insts arg_tys ex_tvs con ps - return [PmCon { pm_con_con = con + return [PmCon { pm_con_con = PmAltConLike con , pm_con_arg_tys = arg_tys , pm_con_tvs = ex_tvs - , pm_con_dicts = dicts , pm_con_args = args }] - -- See Note [Translate Overloaded Literal for Exhaustiveness Checking] - NPat _ (dL->L _ olit) mb_neg _ - | OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit - , isStringTy ty -> - foldr (mkListPatVec charTy) [nilPattern charTy] <$> - translatePatVec fam_insts - (map (LitPat noExtField . HsChar src) (unpackFS s)) - | otherwise -> return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) olit }] - - -- See Note [Translate Overloaded Literal for Exhaustiveness Checking] - LitPat _ lit - | HsString src s <- lit -> - foldr (mkListPatVec charTy) [nilPattern charTy] <$> - translatePatVec fam_insts - (map (LitPat noExtField . HsChar src) (unpackFS s)) - | otherwise -> return [mkLitPattern lit] + NPat ty (dL->L _ olit) mb_neg _ -> 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. + dflags <- getDynFlags + core_expr <- case olit of + OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ } + | not rebindable + , Just expr <- shortCutLit dflags val ty + -> dsExpr expr + _ -> dsOverLit olit + let lit = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr) + let lit' = case mb_neg of + Just _ -> expectJust "failed to negate lit" (negatePmLit lit) + Nothing -> lit + return (mkPmLitPattern lit') + + LitPat _ lit -> do + core_expr <- dsLit (convertLit lit) + let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr) + return (mkPmLitPattern lit) TuplePat tys ps boxity -> do tidy_ps <- translatePatVec fam_insts (map unLoc ps) let tuple_con = RealDataCon (tupleDataCon boxity (length ps)) tys' = case boxity of - Boxed -> tys - -- See Note [Unboxed tuple RuntimeRep vars] in TyCon - Unboxed -> map getRuntimeRep tys ++ tys + Boxed -> tys + -- See Note [Unboxed tuple RuntimeRep vars] in TyCon + Unboxed -> map getRuntimeRep tys ++ tys return [vanillaConPattern tuple_con tys' (concat tidy_ps)] SumPat ty p alt arity -> do @@ -1097,91 +626,6 @@ translatePat fam_insts pat = case pat of SplicePat {} -> panic "Check.translatePat: SplicePat" XPat {} -> panic "Check.translatePat: XPat" -{- Note [Translate Overloaded Literal for Exhaustiveness Checking] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The translation of @NPat@ in exhaustiveness checker is a bit different -from translation in pattern matcher. - - * In pattern matcher (see `tidyNPat' in deSugar/MatchLit.hs), we - translate integral literals to HsIntPrim or HsWordPrim and translate - overloaded strings to HsString. - - * In exhaustiveness checker, in `genCaseTmCs1/genCaseTmCs2`, we use - `lhsExprToPmExpr` to generate uncovered set. In `hsExprToPmExpr`, - however we generate `PmOLit` for HsOverLit, rather than refine - `HsOverLit` inside `NPat` to HsIntPrim/HsWordPrim. If we do - the same thing in `translatePat` as in `tidyNPat`, the exhaustiveness - checker will fail to match the literals patterns correctly. See - #14546. - - In Note [Undecidable Equality for Overloaded Literals], we say: "treat - overloaded literals that look different as different", but previously we - didn't do such things. - - Now, we translate the literal value to match and the literal patterns - consistently: - - * For integral literals, we parse both the integral literal value and - the patterns as OverLit HsIntegral. For example: - - case 0::Int of - 0 -> putStrLn "A" - 1 -> putStrLn "B" - _ -> putStrLn "C" - - When checking the exhaustiveness of pattern matching, we translate the 0 - in value position as PmOLit, but translate the 0 and 1 in pattern position - as PmSLit. The inconsistency leads to the failure of eqPmLit to detect the - equality and report warning of "Pattern match is redundant" on pattern 0, - as reported in #14546. In this patch we remove the specialization of - OverLit patterns, and keep the overloaded number literal in pattern as it - is to maintain the consistency. We know nothing about the `fromInteger` - method (see Note [Undecidable Equality for Overloaded Literals]). Now we - can capture the exhaustiveness of pattern 0 and the redundancy of pattern - 1 and _. - - * For string literals, we parse the string literals as HsString. When - OverloadedStrings is enabled, it further be turned as HsOverLit HsIsString. - For example: - - case "foo" of - "foo" -> putStrLn "A" - "bar" -> putStrLn "B" - "baz" -> putStrLn "C" - - Previously, the overloaded string values are translated to PmOLit and the - non-overloaded string values are translated to PmSLit. However the string - patterns, both overloaded and non-overloaded, are translated to list of - characters. The inconsistency leads to wrong warnings about redundant and - non-exhaustive pattern matching warnings, as reported in #14546. - - In order to catch the redundant pattern in following case: - - case "foo" of - ('f':_) -> putStrLn "A" - "bar" -> putStrLn "B" - - in this patch, we translate non-overloaded string literals, both in value - position and pattern position, as list of characters. For overloaded string - literals, we only translate it to list of characters only when it's type - is stringTy, since we know nothing about the toString methods. But we know - that if two overloaded strings are syntax equal, then they are equal. Then - if it's type is not stringTy, we just translate it to PmOLit. We can still - capture the exhaustiveness of pattern "foo" and the redundancy of pattern - "bar" and "baz" in the following code: - - {-# LANGUAGE OverloadedStrings #-} - main = do - case "foo" of - "foo" -> putStrLn "A" - "bar" -> putStrLn "B" - "baz" -> putStrLn "C" - - We must ensure that doing the same translation to literal values and patterns - in `translatePat` and `hsExprToPmExpr`. The previous inconsistent work led to - #14546. --} - -- | Translate a list of patterns (Note: each pattern is translated -- to a pattern vector but we do not concatenate the results). translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec] @@ -1189,7 +633,8 @@ translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats -- | Translate a constructor pattern translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar] - -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec + -> ConLike -> HsConPatDetails GhcTc + -> DsM PatVec translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps) = concat <$> translatePatVec fam_insts (map unLoc ps) translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2) @@ -1221,7 +666,7 @@ translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _)) let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ] guards = map (\(name,pvec) -> case lookup name zipped of - Just x -> PmGrd pvec (PmExprVar (idName x)) + Just x -> PmGrd pvec (Var x) Nothing -> panic "translateConPatVec: lookup") translated_pats @@ -1245,19 +690,20 @@ translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _)) -- Translate a single match translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc) - -> DsM (PatVec,[PatVec]) -translateMatch fam_insts (dL->L _ (Match { m_pats = lpats, m_grhss = grhss })) = - do - pats' <- concat <$> translatePatVec fam_insts pats - guards' <- mapM (translateGuards fam_insts) guards - return (pats', guards') - where - extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc] - extractGuards (dL->L _ (GRHS _ gs _)) = map unLoc gs - extractGuards _ = panic "translateMatch" - - pats = map unLoc lpats - guards = map extractGuards (grhssGRHSs grhss) + -> DsM (PatVec, [PatVec]) +translateMatch fam_insts (dL->L _ (Match { m_pats = lpats, m_grhss = grhss })) + = do + pats' <- concat <$> translatePatVec fam_insts pats + guards' <- mapM (translateGuards fam_insts) guards + -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards']) + return (pats', guards') + where + extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc] + extractGuards (dL->L _ (GRHS _ gs _)) = map unLoc gs + extractGuards _ = panic "translateMatch" + + pats = map unLoc lpats + guards = map extractGuards (grhssGRHSs grhss) translateMatch _ _ = panic "translateMatch" -- ----------------------------------------------------------------------- @@ -1265,35 +711,11 @@ translateMatch _ _ = panic "translateMatch" -- | Translate a list of guard statements to a pattern vector translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec -translateGuards fam_insts guards = do - all_guards <- concat <$> mapM (translateGuard fam_insts) guards - let - shouldKeep :: Pattern -> DsM Bool - shouldKeep p - | PmVar {} <- p = pure True - | PmCon {} <- p = (&&) - <$> singleMatchConstructor (pm_con_con p) (pm_con_arg_tys p) - <*> allM shouldKeep (pm_con_args p) - shouldKeep (PmGrd pv e) - | isNotPmExprOther e = pure True -- expensive but we want it - | otherwise = allM shouldKeep pv - shouldKeep _other_pat = pure False -- let the rest.. - - all_handled <- allM shouldKeep all_guards - -- It should have been @pure all_guards@ but it is too expressive. - -- Since the term oracle does not handle all constraints we generate, - -- we (hackily) replace all constraints the oracle cannot handle with a - -- single one (we need to know if there is a possibility of failure). - -- See Note [Guards and Approximation] for all guard-related approximations - -- we implement. - if all_handled - then pure all_guards - else do - kept <- filterM shouldKeep all_guards - pure (PmFake : kept) +translateGuards fam_insts guards = + concat <$> mapM (translateGuard fam_insts) guards -- | Check whether a pattern can fail to match -cantFailPattern :: Pattern -> DsM Bool +cantFailPattern :: PmPat -> DsM Bool cantFailPattern PmVar {} = pure True cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps} = (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps @@ -1395,11 +817,10 @@ below is the *right thing to do*: The case with literals is a bit different. a literal @l@ should be translated to @x (True <- x == from l)@. Since we want to have better warnings for overloaded literals as it is a very common feature, we treat them differently. -They are mainly covered in Note [Undecidable Equality for Overloaded Literals] -in PmExpr. +They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmExpr. 4. N+K Patterns & Pattern Synonyms -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +---------------------------------- An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@. Since the only pattern of the three that causes failure is guard @(n <- x-k)@, and has two possible outcomes. Hence, there is no benefit in using a dummy and @@ -1418,18 +839,85 @@ Additionally, top-level guard translation (performed by @translateGuards@) replaces guards that cannot be reasoned about (like the ones we described in 1-4) with a single @PmFake@ to record the possibility of failure to match. +6. Combinatorial explosion +-------------------------- +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. +Long story short: At each point we estimate the number of Deltas we possibly +have to check in the same manner as the current Delta. If we hit a guard that +splits the current Delta k-fold, we check whether this split would get us beyond +a certain threshold ('tryMultiplyDeltas') and continue to check the other guards +with the original Delta. + +Note [Limit the number of refinements] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In PrelRules, we have a huge case with relatively deep matches on pattern +synonyms. Since we allow multiple compatible solutions in the oracle +(i.e. @x ~ [I# y, 42]@), and every pattern synonym is compatible according to +'eqPmAltCon' with every other (no generativity as with DataCons), what would +usually result in a ConVar split where only one branch is satisfiable results +in a blow-up of Deltas. Here's an example: + case x of + A (A _) -> () + B (B _) -> () + ... +By the time we hit the first clause's RHS, we have split the initial Delta twice +and handled the {x~A y, y ~ A z} case, leaving {x/~A} and {x~A y, y/~A} models +for the second clause to check. + +Now consider what happens if A=Left, B=Right. We get x~B y' from the match, +which contradicts with {x~A y, y/~A}, because A and B are incompatible due to +the generative nature of DataCons. This leaves only {x/~A} for checking B's +clause, which ultimately leaves {x/~[A,B]} and {x~B y', y'/~B} uncovered. +Resulting in three models to check for the next clause. That's only linear +growth in the number of models for each clause. + +Consider A and B were arbitrary pattern synonyms instead. We still get x~B y' +from the match, but this no longer refutes {x~A y, y/~A}, because we don't +assume generativity for pattern synonyms. Ergo, @eqPmAltCon A B == Nothing@ +and we get to check the second clause's inner match with {x~B y', x/~A} and +{x~[A y,B y'], y/~A}, splitting both in turn. That makes 4 instead of 3 deltas. +If we keep on doing this, we see that in the nth clause we'd have O(2^n) models +to check instead of just O(n) as above! + +Clearly we have to put a stop to this. So we count in the oracle the number of +times we refined x to some constructor. If the number of splits exceeds the +'mAX_REFINEMENTS', we check the next clause using the original Delta rather +than the union of Deltas arising from the ConVar split. + +If for the above example we had mAX_REFINEMENTS=1, then in the second clause +we would still check the inner match with {x~B y', x/~A} and {x~[A y,B y'], y/~A} +but *discard* the two Deltas arising from splitting {x~[A y,B y'], y/~A}, +checking the next clause with {x~A y, y/~A} instead of its two refinements. +In addition to {x~B y', y'~B z', x/~A} (which arose from the other split) and +{x/~[A,B]} that makes 3 models for the third equation, so linear :). + 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 <- (e |> co)) + pat |> co ===> x (pat <- (x |> co)) -Instead, we now check whether the coercion is a hole or if it is just refl, in -which case we can drop it. Unfortunately, data families generate useful -coercions so guards are still generated in these cases and checking data -families is not really efficient. +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. %************************************************************************ %* * @@ -1443,31 +931,15 @@ families is not really efficient. -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern -pmPatType :: PmPat p -> Type +pmPatType :: PmPat -> Type pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys }) - = conLikeResTy con tys + = pmAltConType con tys pmPatType (PmVar { pm_var_id = x }) = idType x -pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l -pmPatType (PmNLit { pm_lit_id = x }) = idType x pmPatType (PmGrd { pm_grd_pv = pv }) = ASSERT(patVecArity pv == 1) (pmPatType p) where Just p = find ((==1) . patternArity) pv pmPatType PmFake = pmPatType truePattern --- | Information about a conlike that is relevant to coverage checking. --- It is called an \"inhabitation candidate\" since it is a value which may --- possibly inhabit some type, but only if its term constraint ('ic_tm_ct') --- and type constraints ('ic_ty_cs') are permitting, and if all of its strict --- argument types ('ic_strict_arg_tys') are inhabitable. --- See @Note [Extensions to GADTs Meet Their Match]@. -data InhabitationCandidate = - InhabitationCandidate - { ic_val_abs :: ValAbs - , ic_tm_ct :: TmVarCt - , ic_ty_cs :: Bag EvVar - , ic_strict_arg_tys :: [Type] - } - {- Note [Extensions to GADTs Meet Their Match] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1476,275 +948,45 @@ 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. ------ --- Strict argument type constraints ------ - -In the ConVar case of clause processing, each conlike K traditionally -generates two different forms of constraints: - -* A term constraint (e.g., x ~ K y1 ... yn) -* Type constraints from the conlike's context (e.g., if K has type - forall bs. Q => s1 .. sn -> T tys, then Q would be its type constraints) - -As it turns out, these alone are not enough to detect a certain class of -unreachable code. Consider the following example (adapted from #15305): - - data K = K1 | K2 !Void - - f :: K -> () - f K1 = () - -Even though `f` doesn't match on `K2`, `f` is exhaustive in its patterns. Why? -Because it's impossible to construct a terminating value of type `K` using the -`K2` constructor, and thus it's impossible for `f` to ever successfully match -on `K2`. - -The reason is because `K2`'s field of type `Void` is //strict//. Because there -are no terminating values of type `Void`, any attempt to construct something -using `K2` will immediately loop infinitely or throw an exception due to the -strictness annotation. (If the field were not strict, then `f` could match on, -say, `K2 undefined` or `K2 (let x = x in x)`.) - -Since neither the term nor type constraints mentioned above take strict -argument types into account, we make use of the `nonVoid` function to -determine whether a strict type is inhabitable by a terminating value or not. - -`nonVoid ty` returns True when either: -1. `ty` has at least one InhabitationCandidate for which both its term and type - constraints are satifiable, and `nonVoid` returns `True` for all of the - strict argument types in that InhabitationCandidate. -2. We're unsure if it's inhabited by a terminating value. - -`nonVoid ty` returns False when `ty` is definitely uninhabited by anything -(except bottom). Some examples: - -* `nonVoid Void` returns False, since Void has no InhabitationCandidates. - (This is what lets us discard the `K2` constructor in the earlier example.) -* `nonVoid (Int :~: Int)` returns True, since it has an InhabitationCandidate - (through the Refl constructor), and its term constraint (x ~ Refl) and - type constraint (Int ~ Int) are satisfiable. -* `nonVoid (Int :~: Bool)` returns False. Although it has an - InhabitationCandidate (by way of Refl), its type constraint (Int ~ Bool) is - not satisfiable. -* Given the following definition of `MyVoid`: - - data MyVoid = MkMyVoid !Void - - `nonVoid MyVoid` returns False. The InhabitationCandidate for the MkMyVoid - constructor contains Void as a strict argument type, and since `nonVoid Void` - returns False, that InhabitationCandidate is discarded, leaving no others. - -* Performance considerations - -We must be careful when recursively calling `nonVoid` on the strict argument -types of an InhabitationCandidate, because doing so naïvely can cause GHC to -fall into an infinite loop. Consider the following example: - - data Abyss = MkAbyss !Abyss - - stareIntoTheAbyss :: Abyss -> a - stareIntoTheAbyss x = case x of {} - -In principle, stareIntoTheAbyss is exhaustive, since there is no way to -construct a terminating value using MkAbyss. However, both the term and type -constraints for MkAbyss are satisfiable, so the only way one could determine -that MkAbyss is unreachable is to check if `nonVoid Abyss` returns False. -There is only one InhabitationCandidate for Abyss—MkAbyss—and both its term -and type constraints are satisfiable, so we'd need to check if `nonVoid Abyss` -returns False... and now we've entered an infinite loop! - -To avoid this sort of conundrum, `nonVoid` uses a simple test to detect the -presence of recursive types (through `checkRecTc`), and if recursion is -detected, we bail out and conservatively assume that the type is inhabited by -some terminating value. This avoids infinite loops at the expense of making -the coverage checker incomplete with respect to functions like -stareIntoTheAbyss above. Then again, the same problem occurs with recursive -newtypes, like in the following code: - - newtype Chasm = MkChasm Chasm - - gazeIntoTheChasm :: Chasm -> a - gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive - -So this limitation is somewhat understandable. - -Note that even with this recursion detection, there is still a possibility that -`nonVoid` can run in exponential time. Consider the following data type: - - data T = MkT !T !T !T - -If we call `nonVoid` on each of its fields, that will require us to once again -check if `MkT` is inhabitable in each of those three fields, which in turn will -require us to check if `MkT` is inhabitable again... As you can see, the -branching factor adds up quickly, and if the recursion depth limit is, say, -100, then `nonVoid T` will effectively take forever. - -To mitigate this, we check the branching factor every time we are about to call -`nonVoid` on a list of strict argument types. If the branching factor exceeds 1 -(i.e., if there is potential for exponential runtime), then we limit the -maximum recursion depth to 1 to mitigate the problem. If the branching factor -is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay -to stick with a larger maximum recursion depth. - -Another microoptimization applies to data types like this one: - - data S a = ![a] !T - -Even though there is a strict field of type [a], it's quite silly to call -nonVoid on it, since it's "obvious" that it is inhabitable. To make this -intuition formal, we say that a type is definitely inhabitable (DI) if: - - * It has at least one constructor C such that: - 1. C has no equality constraints (since they might be unsatisfiable) - 2. C has no strict argument types (since they might be uninhabitable) - -It's relatively cheap to cheap if a type is DI, so before we call `nonVoid` -on a list of strict argument types, we filter out all of the DI ones. +* Value abstractions are severely simplified to the point where they are just + variables. The information about the PmExpr 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 PmOracle. +* Efficient handling of literal splitting, large enumerations and accurate + redundancy warnings for `COMPLETE` groups through the oracle. -} -instance Outputable InhabitationCandidate where - ppr (InhabitationCandidate { ic_val_abs = va, ic_tm_ct = tm_ct - , ic_ty_cs = ty_cs - , ic_strict_arg_tys = strict_arg_tys }) = - text "InhabitationCandidate" <+> - vcat [ text "ic_val_abs =" <+> ppr va - , text "ic_tm_ct =" <+> ppr tm_ct - , text "ic_ty_cs =" <+> ppr ty_cs - , text "ic_strict_arg_tys =" <+> ppr strict_arg_tys ] - --- | Generate an 'InhabitationCandidate' for a given conlike (generate --- fresh variables of the appropriate type for arguments) -mkOneConFull :: Id -> [Type] -> ConLike -> DsM InhabitationCandidate --- * 'con' K is a conlike of algebraic data type 'T tys' - --- * 'tc_args' are the type arguments of the 'con's TyCon T --- --- * 'x' is the variable for which we encode an equality constraint --- in the term oracle --- --- After instantiating the universal tyvars of K to tc_args we get --- K @tys :: forall bs. Q => s1 .. sn -> T tys --- --- Suppose y1 is a strict field. Then we get --- Results: ic_val_abs: K (y1::s1) .. (yn::sn) --- ic_tm_ct: x ~ K y1..yn --- ic_ty_cs: Q --- ic_strict_arg_tys: [s1] -mkOneConFull x tc_args con = do - let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, _con_res_ty) - = conLikeFullSig con - arg_is_banged = map isBanged $ conLikeImplBangs con - subst1 = zipTvSubst univ_tvs tc_args - - (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM - - -- Field types - let arg_tys' = substTys subst arg_tys - -- Fresh term variables (VAs) as arguments to the constructor - arguments <- mapM mkPmVar arg_tys' - -- All constraints bound by the constructor (alpha-renamed) - let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas) - evvars <- mapM (nameType "pm") theta_cs - let con_abs = PmCon { pm_con_con = con - , pm_con_arg_tys = tc_args - , pm_con_tvs = ex_tvs' - , pm_con_dicts = evvars - , pm_con_args = arguments } - strict_arg_tys = filterByList arg_is_banged arg_tys' - return $ InhabitationCandidate - { ic_val_abs = con_abs - , ic_tm_ct = TVC x (vaToPmExpr con_abs) - , ic_ty_cs = listToBag evvars - , ic_strict_arg_tys = strict_arg_tys - } - -- ---------------------------------------------------------------------------- -- * More smart constructors and fresh variable generation -- | Create a guard pattern -mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern -mkGuard pv e = do - res <- allM cantFailPattern pv - let expr = hsExprToPmExpr e - tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr]) - if | res -> pure (PmGrd pv expr) - | PmExprOther {} <- expr -> pure PmFake - | otherwise -> pure (PmGrd pv expr) - --- | Create a term equality of the form: `(x ~ lit)` -mkPosEq :: Id -> PmLit -> TmVarCt -mkPosEq x l = TVC x (PmExprLit l) -{-# INLINE mkPosEq #-} - --- | Create a term equality of the form: `(x ~ x)` --- (always discharged by the term oracle) -mkIdEq :: Id -> TmVarCt -mkIdEq x = TVC x (PmExprVar (idName x)) -{-# INLINE mkIdEq #-} +mkGuard :: PatVec -> HsExpr GhcTc -> DsM PmPat +mkGuard pv e = PmGrd pv <$> dsExpr e -- | Generate a variable pattern of a given type -mkPmVar :: Type -> DsM (PmPat p) +mkPmVar :: Type -> DsM PmPat mkPmVar ty = PmVar <$> mkPmId ty -{-# INLINE mkPmVar #-} -- | Generate many variable patterns, given a list of types mkPmVars :: [Type] -> DsM PatVec mkPmVars tys = mapM mkPmVar tys -{-# INLINE mkPmVars #-} - --- | Generate a fresh `Id` of a given type -mkPmId :: Type -> DsM Id -mkPmId ty = getUniqueM >>= \unique -> - let occname = mkVarOccFS $ fsLit "$pm" - name = mkInternalName unique occname noSrcSpan - in return (mkLocalId name ty) -- | Generate a fresh term variable of a given and return it in two forms: -- * A variable pattern -- * A variable expression -mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc) +mkPmId2Forms :: Type -> DsM (PmPat, LHsExpr GhcTc) mkPmId2Forms ty = do x <- mkPmId ty return (PmVar x, noLoc (HsVar noExtField (noLoc x))) --- ---------------------------------------------------------------------------- --- * Converting between Value Abstractions, Patterns and PmExpr - --- | Convert a value abstraction an expression -vaToPmExpr :: ValAbs -> PmExpr -vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps }) - = PmExprCon c (map vaToPmExpr ps) -vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x) -vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l -vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x) - --- | Convert a pattern vector to a list of value abstractions by dropping the --- guards (See Note [Translating As Patterns]) -coercePatVec :: PatVec -> [ValAbs] -coercePatVec pv = concatMap coercePmPat pv - --- | Convert a pattern to a list of value abstractions (will be either an empty --- list if the pattern is a guard pattern, or a singleton list in all other --- cases) by dropping the guards (See Note [Translating As Patterns]) -coercePmPat :: Pattern -> [ValAbs] -coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }] -coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }] -coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys - , pm_con_tvs = tvs, pm_con_dicts = dicts - , pm_con_args = args }) - = [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys - , pm_con_tvs = tvs, pm_con_dicts = dicts - , pm_con_args = coercePatVec args }] -coercePmPat (PmGrd {}) = [] -- drop the guards -coercePmPat PmFake = [] -- drop the guards - --- | Check whether a 'ConLike' has the /single match/ property, i.e. whether +-- | Check whether a 'PmAltCon' has the /single match/ property, i.e. whether -- it is the only possible match in the given context. See also -- 'allCompleteMatches' and Note [Single match constructors]. -singleMatchConstructor :: ConLike -> [Type] -> DsM Bool -singleMatchConstructor cl tys = - any (isSingleton . snd) <$> allCompleteMatches cl tys +singleMatchConstructor :: PmAltCon -> [Type] -> DsM Bool +singleMatchConstructor PmAltLit{} _ = pure False +singleMatchConstructor (PmAltConLike cl) tys = + any isSingleton <$> allCompleteMatches (conLikeResTy cl tys) {- Note [Single match constructors] @@ -1771,42 +1013,46 @@ the single-match property. We currently don't (can't) check this in the translation step. See #15753 for why this yields surprising results. -} --- | For a given conlike, finds all the sets of patterns which could --- be relevant to that conlike by consulting the result type. +-- | For a given type, finds all the COMPLETE sets of conlikes that inhabit it. +-- +-- Note that for a data family instance, this must be the *representation* type. +-- e.g. data instance T (a,b) = T1 a b +-- leads to +-- data TPair a b = T1 a b -- The "representation" type +-- It is TPair a b, not T (a, b), that is given to allCompleteMatches -- -- These come from two places. -- 1. From data constructors defined with the result type constructor. -- 2. From `COMPLETE` pragmas which have the same type as the result -- type constructor. Note that we only use `COMPLETE` pragmas -- *all* of whose pattern types match. See #14135 -allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])] -allCompleteMatches cl tys = do - let fam = case cl of - RealDataCon dc -> - [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))] - PatSynCon _ -> [] - ty = conLikeResTy cl tys - pragmas <- case splitTyConApp_maybe ty of - Just (tc, _) -> dsGetCompleteMatches tc - Nothing -> return [] - let fams cm = (FromComplete,) <$> - mapM dsLookupConLike (completeMatchConLikes cm) - from_pragma <- filter (\(_,m) -> isValidCompleteMatch ty m) <$> - mapM fams pragmas - let final_groups = fam ++ from_pragma - return final_groups - where - -- Check that all the pattern synonym return types in a `COMPLETE` - -- pragma subsume the type we're matching. - -- See Note [Filtering out non-matching COMPLETE sets] - isValidCompleteMatch :: Type -> [ConLike] -> Bool - isValidCompleteMatch ty = all go - where - go (RealDataCon {}) = True - go (PatSynCon psc) = isJust $ flip tcMatchTy ty $ patSynResTy - $ patSynSig psc - - patSynResTy (_, _, _, _, _, res_ty) = res_ty +allCompleteMatches :: Type -> DsM [[ConLike]] +allCompleteMatches ty = case splitTyConApp_maybe ty of + Nothing -> pure [] -- NB: We don't know any COMPLETE set, as opposed to [[]] + Just (tc, tc_args) -> do + -- Look into the representation type of a data family instance, too. + env <- dsGetFamInstEnvs + let (tc', _tc_args', _co) = tcLookupDataFamInst env tc tc_args + let mb_rdcs = map RealDataCon <$> tyConDataCons_maybe tc' + let maybe_to_list = maybe [] (:[]) + let rdcs = maybe_to_list mb_rdcs + -- NB: tc, because COMPLETE sets are associated with the parent data family + -- TyCon + pragmas <- dsGetCompleteMatches tc + let fams = mapM dsLookupConLike . completeMatchConLikes + pscs <- mapM fams pragmas + let candidates = rdcs ++ pscs + -- Check that all the pattern synonym return types in a `COMPLETE` + -- pragma subsume the type we're matching. + -- See Note [Filtering out non-matching COMPLETE sets] + pure (filter (isValidCompleteMatch ty) candidates) + where + isValidCompleteMatch :: Type -> [ConLike] -> Bool + isValidCompleteMatch ty = all p + where + p (RealDataCon _) = True + p (PatSynCon ps) = isJust (tcMatchTy (projResTy (patSynSig ps)) ty) + projResTy (_, _, _, _, _, res_ty) = res_ty {- Note [Filtering out non-matching COMPLETE sets] @@ -1858,37 +1104,24 @@ OK. Consider this example (from #14059): 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. --} --- ----------------------------------------------------------------------- --- * Types and constraints +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 -newEvVar :: Name -> Type -> EvVar -newEvVar name ty = mkLocalId name ty + pattern Just42 :: Maybe Int + pattern Just42 = Just 42 -nameType :: String -> Type -> DsM EvVar -nameType name ty = do - unique <- getUniqueM - let occname = mkVarOccFS (fsLit (name++"_"++show unique)) - idname = mkInternalName unique occname noSrcSpan - return (newEvVar idname ty) +But fail to filter out the equivalent -{- -%************************************************************************ -%* * - The type oracle -%* * -%************************************************************************ --} + pattern Just'42 :: (a ~ Int) => Maybe a + pattern Just'42 = Just 42 --- | Check whether a set of type constraints is satisfiable. -tyOracle :: Bag EvVar -> PmM Bool -tyOracle evs - = liftD $ - do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs - ; case res of - Just sat -> return sat - Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) } +Which seems fine as far as tcMatchTy is concerned, but it raises a few eye +brows. +-} {- %************************************************************************ @@ -1907,8 +1140,9 @@ patVecArity :: PatVec -> PmArity patVecArity = sum . map patternArity -- | Compute the arity of a pattern -patternArity :: Pattern -> PmArity +patternArity :: PmPat -> PmArity patternArity (PmGrd {}) = 0 +patternArity PmFake = 0 patternArity _other_pat = 1 {- @@ -1920,416 +1154,152 @@ patternArity _other_pat = 1 Main functions are: -* mkInitialUncovered :: [Id] -> PmM Uncovered - - Generates the initial uncovered set. Term and type constraints in scope - are checked, if they are inconsistent, the set is empty, otherwise, the - set contains only a vector of variables with the constraints in scope. - -* pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult +* pmcheck :: PatVec -> [PatVec] -> ValVec -> Delta -> DsM PartialResult - Checks redundancy, coverage and inaccessibility, using auxilary functions - `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is - common in all three checks (see paper) and calls `pmcheckGuards` when the - whole clause is checked, or `pmcheckHd` when the pattern vector does not - start with a guard. + 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 -> PmM PartialResult +* pmcheckGuards :: [PatVec] -> ValVec -> Delta -> DsM PartialResult Processes the guards. - -* pmcheckHd :: Pattern -> PatVec -> [PatVec] - -> ValAbs -> ValVec -> PmM PartialResult - - Worker: This function implements functions `covered`, `uncovered` and - `divergent` from the paper at once. 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. -} -- | Lift a pattern matching action from a single value vector abstration to a --- value set abstraction, but calling it on every vector and the combining the +-- value set abstraction, but calling it on every vector and combining the -- results. -runMany :: (ValVec -> PmM PartialResult) -> (Uncovered -> PmM PartialResult) -runMany _ [] = return mempty -runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms - --- | Generate the initial uncovered set. It initializes the --- delta with all term and type constraints in scope. -mkInitialUncovered :: [Id] -> PmM Uncovered -mkInitialUncovered vars = do - delta <- pmInitialTmTyCs - let patterns = map PmVar vars - return [ValVec patterns delta] +runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult +runMany _ [] = return emptyPartialResult +runMany pm (m:ms) = do + res <- pm m + combinePartialResults res <$> runMany pm ms -- | Increase the counter for elapsed algorithm iterations, check that the -- limit is not exceeded and call `pmcheck` -pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult -pmcheckI ps guards vva = do - n <- liftD incrCheckPmIterDs - tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps - $$ hang (text "guards:") 2 (vcat (map pprPatVec guards)) - $$ pprValVecDebug vva) - res <- pmcheck ps guards vva +pmcheckI :: PatVec -> [PatVec] -> ValVec -> Int -> Delta -> DsM PartialResult +pmcheckI ps guards vva n delta = do + m <- incrCheckPmIterDs + tracePm "pmCheck" (ppr m <> colon + $$ hang (text "patterns:") 2 (ppr ps) + $$ hang (text "guards:") 2 (ppr guards) + $$ ppr vva + $$ ppr delta) + res <- pmcheck ps guards vva n delta tracePm "pmCheckResult:" (ppr res) return res {-# INLINE pmcheckI #-} -- | Increase the counter for elapsed algorithm iterations, check that the -- limit is not exceeded and call `pmcheckGuards` -pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult -pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva +pmcheckGuardsI :: [PatVec] -> Int -> Delta -> DsM PartialResult +pmcheckGuardsI gvs n delta = incrCheckPmIterDs >> pmcheckGuards gvs n delta {-# INLINE pmcheckGuardsI #-} --- | Increase the counter for elapsed algorithm iterations, check that the --- limit is not exceeded and call `pmcheckHd` -pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec - -> PmM PartialResult -pmcheckHdI p ps guards va vva = do - n <- liftD incrCheckPmIterDs - tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p - $$ pprPatVec ps - $$ hang (text "guards:") 2 (vcat (map pprPatVec guards)) - $$ pprPmPatDebug va - $$ pprValVecDebug vva) - - res <- pmcheckHd p ps guards va vva - tracePm "pmCheckHdI: res" (ppr res) - return res -{-# INLINE pmcheckHdI #-} +-- | Check the list of mutually exclusive guards +pmcheckGuards :: [PatVec] -> Int -> Delta -> DsM PartialResult +pmcheckGuards [] _ delta = return (usimple delta) +pmcheckGuards (gv:gvs) n delta = do + (PartialResult cs unc ds) <- pmcheckI gv [] [] n delta + let (n', unc') + -- See 6. in Note [Guards and Approximation] + | Just n' <- tryMultiplyDeltas (length unc) n = (n', unc) + | otherwise = (n, [delta]) + (PartialResult css uncs dss) <- runMany (pmcheckGuardsI gvs n') unc' + return $ PartialResult (cs `mappend` css) + uncs + (ds `mappend` dss) -- | Matching function: Check simultaneously a clause (takes separately the -- patterns and the list of guards) for exhaustiveness, redundancy and -- inaccessibility. -pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult -pmcheck [] guards vva@(ValVec [] _) +pmcheck + :: PatVec -- ^ Patterns of the clause + -> [PatVec] -- ^ (Possibly multiple) guards of the clause + -> ValVec -- ^ The value vector abstraction to match against + -> Int -- ^ Estimate on the number of similar 'Delta's to handle. + -- See 6. in Note [Guards and Approximation] + -> Delta -- ^ Oracle state giving meaning to the identifiers in the ValVec + -> DsM PartialResult +pmcheck [] guards [] n delta | null guards = return $ mempty { presultCovered = Covered } - | otherwise = pmcheckGuardsI guards vva + | otherwise = pmcheckGuardsI guards n delta -- Guard -pmcheck (PmFake : ps) guards vva = +pmcheck (PmFake : ps) guards vva n delta = -- short-circuit if the guard pattern is useless. -- we just have two possible outcomes: fail here or match and recurse -- none of the two contains any useful information about the failure -- though. So just have these two cases but do not do all the boilerplate - forces . mkCons vva <$> pmcheckI ps guards vva -pmcheck (p : ps) guards (ValVec vas delta) - | PmGrd { pm_grd_pv = pv, pm_grd_expr = e } <- p - = do - y <- liftD $ mkPmId (pmPatType p) - let tm_state = extendSubst y e (delta_tm_cs delta) - delta' = delta { delta_tm_cs = tm_state } - utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta') - -pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons" -pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil" - -pmcheck (p:ps) guards (ValVec (va:vva) delta) - = pmcheckHdI p ps guards va (ValVec vva delta) - --- | Check the list of guards -pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult -pmcheckGuards [] vva = return (usimple [vva]) -pmcheckGuards (gv:gvs) vva = do - (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva - (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa - return $ PartialResult (prov1 `mappend` prov2) - (cs `mappend` css) - vsas - (ds `mappend` dss) - --- | Worker function: Implements all cases described in the paper for all three --- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard` --- cases which are handled by `pmcheck` -pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec - -> PmM PartialResult - --- Var -pmcheckHd (PmVar x) ps guards va (ValVec vva delta) - | Just tm_state <- solveOneEq (delta_tm_cs delta) (TVC x (vaToPmExpr va)) - = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state})) - | otherwise = return mempty - --- ConCon -pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1 - , pm_con_args = args1})) ps guards - (va@(PmCon { pm_con_con = c2, pm_con_tvs = ex_tvs2 - , pm_con_args = args2})) (ValVec vva delta) - | c1 /= c2 = - return (usimple [ValVec (va:vva) delta]) - | otherwise = do - let to_evvar tv1 tv2 = nameType "pmConCon" $ - mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2) - mb_to_evvar tv1 tv2 - -- If we have identical constructors but different existential - -- tyvars, then generate extra equality constraints to ensure the - -- existential tyvars. - -- See Note [Coverage checking and existential tyvars]. - | tv1 == tv2 = pure Nothing - | otherwise = Just <$> to_evvar tv1 tv2 - evvars <- (listToBag . catMaybes) <$> - ASSERT(ex_tvs1 `equalLength` ex_tvs2) - liftD (zipWithM mb_to_evvar ex_tvs1 ex_tvs2) - let delta' = delta { delta_ty_cs = evvars `unionBags` delta_ty_cs delta } - kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p) - <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta') - --- LitLit -pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva = - case eqPmLit l1 l2 of - True -> ucon va <$> pmcheckI ps guards vva - False -> return $ ucon va (usimple [vva]) + -- TODO: I don't think this should mkCons delta, rather than just replace the + -- presultUncovered by [delta] completely. Note that the uncovered set + -- returned from the recursive call can only be a refinement of the + -- original delta. + forces . mkCons delta <$> pmcheckI ps guards vva n delta +pmcheck (p@PmGrd { pm_grd_pv = pv, pm_grd_expr = e } : ps) guards vva n delta = do + tracePm "PmGrd: pmPatType" (vcat [ppr p, ppr (pmPatType p)]) + x <- mkPmId (exprType e) + delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e + pmcheckI (pv ++ ps) guards (x : vva) n delta' + +-- Var: Add x :-> y to the oracle and recurse +pmcheck (PmVar x : ps) guards (y : vva) n delta = do + delta' <- expectJust "x is fresh" <$> addTmCt delta (TmVarVar x y) + pmcheckI ps guards vva n delta' -- ConVar -pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys })) - ps guards - (PmVar x) (ValVec vva delta) = do - (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys) - - cons_cs <- mapM (liftD . mkOneConFull x tys) complete_match - - inst_vsa <- flip mapMaybeM cons_cs $ - \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 delta tm_ct ty_cs strict_arg_tys - pure $ fmap (ValVec (va:vva)) mb_sat - - set_provenance prov . - force_if (canDiverge (idName x) (delta_tm_cs delta)) <$> - runMany (pmcheckI (p:ps) guards) inst_vsa - --- LitVar -pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta) - = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$> - mkUnion non_matched <$> - case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of - Just tm_state -> pmcheckHdI p ps guards (PmLit l) $ - ValVec vva (delta {delta_tm_cs = tm_state}) - Nothing -> return mempty - where - -- See Note [Refutable shapes] in TmOracle - us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l) - = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })] - | otherwise = [] - - non_matched = usimple us - --- LitNLit -pmcheckHd (p@(PmLit l)) ps guards - (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta) - | all (not . eqPmLit l) lits - , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l) - -- Both guards check the same so it would be sufficient to have only - -- the second one. Nevertheless, it is much cheaper to check whether - -- the literal is in the list so we check it first, to avoid calling - -- the term oracle (`solveOneEq`) if possible - = mkUnion non_matched <$> - pmcheckHdI p ps guards (PmLit l) - (ValVec vva (delta { delta_tm_cs = tm_state })) - | otherwise = return non_matched - where - -- See Note [Refutable shapes] in TmOracle - us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l) - = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })] - | otherwise = [] - - non_matched = usimple us - --- ---------------------------------------------------------------------------- --- The following three can happen only in cases like #322 where constructors --- and overloaded literals appear in the same match. The general strategy is --- to replace the literal (positive/negative) by a variable and recurse. The --- fact that the variable is equal to the literal is recorded in `delta` so --- no information is lost - --- LitCon -pmcheckHd p@PmLit{} ps guards va@PmCon{} (ValVec vva delta) - = do y <- liftD $ mkPmId (pmPatType va) - -- Analogous to the ConVar case, we have to case split the value - -- abstraction on possible literals. We do so by introducing a fresh - -- variable that is equated to the constructor. LitVar will then take - -- care of the case split by resorting to NLit. - let tm_state = extendSubst y (vaToPmExpr va) (delta_tm_cs delta) - delta' = delta { delta_tm_cs = tm_state } - pmcheckHdI p ps guards (PmVar y) (ValVec vva delta') - --- ConLit -pmcheckHd p@PmCon{} ps guards (PmLit l) (ValVec vva delta) - = do y <- liftD $ mkPmId (pmPatType p) - -- This desugars to the ConVar case by introducing a fresh variable that - -- is equated to the literal via a constraint. ConVar will then properly - -- case split on all possible constructors. - let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta) - delta' = delta { delta_tm_cs = tm_state } - pmcheckHdI p ps guards (PmVar y) (ValVec vva delta') - --- ConNLit -pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva - = pmcheckHdI p ps guards (PmVar x) vva - --- Impossible: handled by pmcheck -pmcheckHd PmFake _ _ _ _ = panic "pmcheckHd: Fake" -pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard" - -{- -Note [Coverage checking and existential tyvars] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -GHC's implementation of the pattern-match coverage algorithm (as described in -the GADTs Meet Their Match paper) must take some care to emit enough type -constraints when handling data constructors with exisentially quantified type -variables. To better explain what the challenge is, consider a constructor K -of the form: - - K @e_1 ... @e_m ev_1 ... ev_v ty_1 ... ty_n :: T u_1 ... u_p - -Where: - -* e_1, ..., e_m are the existentially bound type variables. -* ev_1, ..., ev_v are evidence variables, which may inhabit a dictionary type - (e.g., Eq) or an equality constraint (e.g., e_1 ~ Int). -* ty_1, ..., ty_n are the types of K's fields. -* T u_1 ... u_p is the return type, where T is the data type constructor, and - u_1, ..., u_p are the universally quantified type variables. - -In the ConVar case, the coverage algorithm will have in hand the constructor -K as well as a list of type arguments [t_1, ..., t_n] to substitute T's -universally quantified type variables u_1, ..., u_n for. It's crucial to take -these in as arguments, as it is non-trivial to derive them just from the result -type of a pattern synonym and the ambient type of the match (#11336, #17112). -The type checker already did the hard work, so we should just make use of it. - -The presence of existentially quantified type variables adds a significant -wrinkle. We always grab e_1, ..., e_m from the definition of K to begin with, -but we don't want them to appear in the final PmCon, because then -calling (mkOneConFull K) for other pattern variables might reuse the same -existential tyvars, which is certainly wrong. - -Previously, GHC's solution to this wrinkle was to always create fresh names -for the existential tyvars and put them into the PmCon. This works well for -many cases, but it can break down if you nest GADT pattern matches in just -the right way. For instance, consider the following program: - - data App f a where - App :: f a -> App f (Maybe a) - - data Ty a where - TBool :: Ty Bool - TInt :: Ty Int - - data T f a where - C :: T Ty (Maybe Bool) - - foo :: T f a -> App f a -> () - foo C (App TBool) = () - -foo is a total program, but with the previous approach to handling existential -tyvars, GHC would mark foo's patterns as non-exhaustive. - -When foo is desugared to Core, it looks roughly like so: - - foo @f @a (C co1 _co2) (App @a1 _co3 (TBool |> co1)) = () - -(Where `a1` is an existential tyvar.) - -That, in turn, is processed by the coverage checker to become: - - foo @f @a (C co1 _co2) (App @a1 _co3 (pmvar123 :: f a1)) - | TBool <- pmvar123 |> co1 - = () - -Note that the type of pmvar123 is `f a1`—this will be important later. - -Now, we proceed with coverage-checking as usual. When we come to the -ConVar case for App, we create a fresh variable `a2` to represent its -existential tyvar. At this point, we have the equality constraints -`(a ~ Maybe a2, a ~ Maybe Bool, f ~ Ty)` in scope. - -However, when we check the guard, it will use the type of pmvar123, which is -`f a1`. Thus, when considering if pmvar123 can match the constructor TInt, -it will generate the constraint `a1 ~ Int`. This means our final set of -equality constraints would be: - - f ~ Ty - a ~ Maybe Bool - a ~ Maybe a2 - a1 ~ Int - -Which is satisfiable! Freshening the existential tyvar `a` to `a2` doomed us, -because GHC is unable to relate `a2` to `a1`, which really should be the same -tyvar. - -Luckily, we can avoid this pitfall. Recall that the ConVar case was where we -generated a PmCon with too-fresh existentials. But after ConVar, we have the -ConCon case, which considers whether each constructor of a particular data type -can be matched on in a particular spot. - -In the case of App, when we get to the ConCon case, we will compare our -original App PmCon (from the source program) to the App PmCon created from the -ConVar case. In the former PmCon, we have `a1` in hand, which is exactly the -existential tyvar we want! Thus, we can force `a1` to be the same as `a2` here -by emitting an additional `a1 ~ a2` constraint. Now our final set of equality -constraints will be: - - f ~ Ty - a ~ Maybe Bool - a ~ Maybe a2 - a1 ~ Int - a1 ~ a2 - -Which is unsatisfiable, as we desired, since we now have that -Int ~ a1 ~ a2 ~ Bool. - -In general, App might have more than one constructor, in which case we -couldn't reuse the existential tyvar for App for a different constructor. This -means that we can only use this trick in ConCon when the constructors are the -same. But this is fine, since this is the only scenario where this situation -arises in the first place! --} +pmcheck (p@PmCon{ pm_con_con = con, pm_con_args = args + , pm_con_arg_tys = arg_tys, pm_con_tvs = ex_tvs } : ps) + guards (x : vva) n delta = do + -- E.g f (K p q) = <rhs> + -- <next equation> + -- Split the value vector into two value vectors: + -- * one for <rhs>, binding x to (K p q) + -- * one for <next equation>, recording that x is /not/ (K _ _) + + -- Stuff for <rhs> + pr_pos <- refineToAltCon delta x con arg_tys ex_tvs >>= \case + Nothing -> pure mempty + Just (delta', arg_vas) -> + pmcheckI (args ++ ps) guards (arg_vas ++ vva) n delta' + + -- Stuff for <next equation> + -- The var is forced regardless of whether @con@ was satisfiable + let pr_pos' = forceIfCanDiverge delta x pr_pos + pr_neg <- addRefutableAltCon delta x con >>= \case + Nothing -> pure mempty + Just delta' -> pure (usimple delta') + + tracePm "ConVar" (vcat [ppr p, ppr x, ppr pr_pos', ppr pr_neg]) + + -- Combine both into a single PartialResult + let pr = mkUnion pr_pos' pr_neg + case (presultUncovered pr_pos', presultUncovered pr_neg) of + ([], _) -> pure pr + (_, []) -> pure pr + -- See Note [Limit the number of refinements] + _ | lookupNumberOfRefinements delta x < mAX_REFINEMENTS + -> pure pr + | otherwise -> pure pr{ presultUncovered = [delta] } + +pmcheck [] _ (_:_) _ _ = panic "pmcheck: nil-cons" +pmcheck (_:_) _ [] _ _ = panic "pmcheck: cons-nil" -- ---------------------------------------------------------------------------- -- * Utilities for main checking -updateVsa :: (ValSetAbs -> ValSetAbs) -> (PartialResult -> PartialResult) -updateVsa f p@(PartialResult { presultUncovered = old }) +updateUncovered :: (Uncovered -> Uncovered) -> (PartialResult -> PartialResult) +updateUncovered f p@(PartialResult { presultUncovered = old }) = p { presultUncovered = f old } --- | Initialise with default values for covering and divergent information. -usimple :: ValSetAbs -> PartialResult -usimple vsa = mempty { presultUncovered = vsa } - --- | Take the tail of all value vector abstractions in the uncovered set -utail :: PartialResult -> PartialResult -utail = updateVsa upd - where upd vsa = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ] - --- | Prepend a value abstraction to all value vector abstractions in the --- uncovered set -ucon :: ValAbs -> PartialResult -> PartialResult -ucon va = updateVsa upd - where - upd vsa = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ] - --- | Given a data constructor of arity `a` and an uncovered set containing --- value vector abstractions of length `(a+n)`, pass the first `n` value --- abstractions to the constructor (Hence, the resulting value vector --- abstractions will have length `n+1`) -kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar] - -> PartialResult -> PartialResult -kcon con arg_tys ex_tvs dicts - = let n = conLikeArity con - upd vsa = - [ ValVec (va:vva) delta - | ValVec vva' delta <- vsa - , let (args, vva) = splitAt n vva' - , let va = PmCon { pm_con_con = con - , pm_con_arg_tys = arg_tys - , pm_con_tvs = ex_tvs - , pm_con_dicts = dicts - , pm_con_args = args } ] - in updateVsa upd +-- | Initialise with default values for covering and divergent information and +-- a singleton uncovered set. +usimple :: Delta -> PartialResult +usimple delta = mempty { presultUncovered = [delta] } -- | Get the union of two covered, uncovered and divergent value set -- abstractions. Since the covered and divergent sets are represented by a @@ -2339,21 +1309,19 @@ kcon con arg_tys ex_tvs dicts mkUnion :: PartialResult -> PartialResult -> PartialResult mkUnion = mappend --- | Add a value vector abstraction to a value set abstraction (uncovered). -mkCons :: ValVec -> PartialResult -> PartialResult -mkCons vva = updateVsa (vva:) +-- | Add a model to the uncovered set. +mkCons :: Delta -> PartialResult -> PartialResult +mkCons model = updateUncovered (model:) -- | Set the divergent set to not empty forces :: PartialResult -> PartialResult forces pres = pres { presultDivergent = Diverged } --- | Set the divergent set to non-empty if the flag is `True` -force_if :: Bool -> PartialResult -> PartialResult -force_if True pres = forces pres -force_if False pres = pres - -set_provenance :: Provenance -> PartialResult -> PartialResult -set_provenance prov pr = pr { presultProvenance = prov } +-- | Set the divergent set to non-empty if the variable has not been forced yet +forceIfCanDiverge :: Delta -> Id -> PartialResult -> PartialResult +forceIfCanDiverge delta x + | canDiverge delta x = forces + | otherwise = id -- ---------------------------------------------------------------------------- -- * Propagation of term constraints inwards when checking nested matches @@ -2362,7 +1330,7 @@ set_provenance prov pr = pr { presultProvenance = prov } ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 `addTmCsDs' in PmMonad that store in the environment type and +`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' @@ -2384,80 +1352,88 @@ f x = case x of (_:_) -> True [] -> False -- can't happen -Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating +Functions `addScrutTmCs' and `addPatTmCs' are responsible for generating these constraints. -} --- | Generate equalities when checking a case expression: --- case x of { p1 -> e1; ... pn -> en } --- When we go deeper to check e.g. e1 we record two equalities: --- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn) --- and (x ~ p1). -genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee - -> [Pat GhcTc] -- LHS (should have length 1) - -> [Id] -- MatchVars (should have length 1) - -> DsM (Bag TmVarCt) -genCaseTmCs2 Nothing _ _ = return emptyBag -genCaseTmCs2 (Just scr) [p] [var] = do - fam_insts <- dsGetFamInstEnvs - [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p - let scr_e = lhsExprToPmExpr scr - return $ listToBag [(TVC var e), (TVC var scr_e)] -genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase" - --- | Generate a simple equality when checking a case expression: --- case x of { matches } --- When checking matches we record that (x ~ y) where y is the initial +locallyExtendPmDelta :: (Delta -> DsM (Maybe Delta)) -> DsM a -> DsM a +locallyExtendPmDelta ext k = getPmDelta >>= ext >>= \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. + Nothing -> k + Just delta' -> updPmDelta delta' k + +-- | Add in-scope type constraints +addTyCsDs :: Bag EvVar -> DsM a -> DsM a +addTyCsDs ev_vars = + locallyExtendPmDelta (\delta -> addTypeEvidence delta 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. -genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag TmVarCt -genCaseTmCs1 Nothing _ = emptyBag -genCaseTmCs1 (Just scr) [var] = unitBag (TVC var (lhsExprToPmExpr scr)) -genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase" - -{- Note [Literals in PmPat] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Instead of translating a literal to a variable accompanied with a guard, we -treat them like constructor patterns. The following example from -"./libraries/base/GHC/IO/Encoding.hs" shows why: - -mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding -mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of - "UTF8" -> return $ UTF8.mkUTF8 cfm - "UTF16" -> return $ UTF16.mkUTF16 cfm - "UTF16LE" -> return $ UTF16.mkUTF16le cfm - ... - -Each clause gets translated to a list of variables with an equal number of -guards. For every guard we generate two cases (equals True/equals False) which -means that we generate 2^n cases to feed the oracle with, where n is the sum of -the length of all strings that appear in the patterns. For this particular -example this means over 2^40 cases. Instead, by representing them like with -constructor we get the following: - 1. We exploit the common prefix with our representation of VSAs - 2. We prune immediately non-reachable cases - (e.g. False == (x == "U"), True == (x == "U")) - -Note [Translating As Patterns] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Instead of translating x@p as: x (p <- x) -we instead translate it as: p (x <- coercePattern p) -for performance reasons. For example: - - f x@True = 1 - f y@False = 2 - -Gives the following with the first translation: - - x |> {x == False, x == y, y == True} - -If we use the second translation we get an empty set, independently of the -oracle. Since the pattern `p' may contain guard patterns though, it cannot be -used as an expression. That's why we call `coercePatVec' to drop the guard and -`vaToPmExpr' to transform the value abstraction to an expression in the -guard pattern (value abstractions are a subset of expressions). We keep the -guards in the first pattern `p' though. +addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a +addScrutTmCs Nothing _ k = k +addScrutTmCs (Just scr) [x] k = do + scr_e <- dsLExpr scr + locallyExtendPmDelta (\delta -> addVarCoreCt delta x scr_e) k +addScrutTmCs _ _ _ = panic "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 +-- Morally, this computes an approximation of the Covered set for p1 +-- (which pmcheck currently discards). TODO: Re-use pmcheck instead of calling +-- out to awkard addVarPatVecCt. +addPatTmCs ps xs k = do + fam_insts <- dsGetFamInstEnvs + pv <- concat <$> translatePatVec fam_insts ps + locallyExtendPmDelta (\delta -> addVarPatVecCt delta xs pv) k + +-- ---------------------------------------------------------------------------- +-- * Converting between Value Abstractions, Patterns and PmExpr +-- | Add a constraint equating a variable to a 'PatVec'. Picks out the single +-- 'PmPat' of arity 1 and equates x to it. Returns the original Delta if that +-- fails. Otherwise it returns Nothing when the resulting Delta would be +-- unsatisfiable, or @Just delta'@ when the extended @delta'@ is still possibly +-- satisfiable. +addVarPatVecCt :: Delta -> [Id] -> PatVec -> DsM (Maybe Delta) +-- This is just a simple version of pmcheck to compute the Covered Delta +-- (which pmcheck doesn't even attempt to keep). +-- Also PmGrd, although having pattern arity 0, really stores important info. +-- For example, as-patterns desugar to a plain variable match and an associated +-- PmGrd for the RHS of the @. We don't currently look into that PmGrd and I'm +-- not willing to duplicate any more of pmcheck. +addVarPatVecCt delta (x:xs) (pat:pv) + | patternArity pat == 1 -- PmVar or PmCon + = runMaybeT $ do + delta' <- MaybeT (addVarPatCt delta x pat) + MaybeT (addVarPatVecCt delta' xs pv) + | otherwise -- PmGrd or PmFake + = addVarPatVecCt delta (x:xs) pv +addVarPatVecCt delta [] pv = ASSERT( patVecArity pv == 0 ) pure (Just delta) +addVarPatVecCt _ (_:_) [] = panic "More match vars than patterns" + +-- | Convert a pattern to a 'PmExpr' (will be either 'Nothing' if the pattern is +-- a guard pattern, or 'Just' an expression in all other cases) by dropping the +-- guards +addVarPatCt :: Delta -> Id -> PmPat -> DsM (Maybe Delta) +addVarPatCt delta x (PmVar { pm_var_id = y }) = addTmCt delta (TmVarVar x y) +addVarPatCt delta x (PmCon { pm_con_con = con, pm_con_args = args }) = runMaybeT $ do + arg_ids <- traverse (lift . mkPmId . pmPatType) args + delta' <- foldlM (\delta (y, arg) -> MaybeT (addVarPatCt delta y arg)) delta (zip arg_ids args) + MaybeT (addTmCt delta' (TmVarCon x con arg_ids)) +addVarPatCt delta _ _pat = ASSERT( patternArity _pat == 0 ) pure (Just delta) +{- %************************************************************************ %* * Pretty printing of exhaustiveness/redundancy check warnings @@ -2465,32 +1441,34 @@ guards in the first pattern `p' though. %************************************************************************ -} --- | Check whether any part of pattern match checking is enabled (does not --- matter whether it is the redundancy check or the exhaustiveness check). -isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool -isAnyPmCheckEnabled dflags (DsMatchContext kind _loc) +-- | Check whether any part of pattern match checking is enabled for this +-- 'HsMatchContext' (does not matter whether it is the redundancy check or the +-- exhaustiveness check). +isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool +isMatchContextPmChecked dflags origin kind + | isGenerated origin + = False + | otherwise = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind -instance Outputable ValVec where - ppr (ValVec vva delta) - = let (subst, refuts) = wrapUpTmState (delta_tm_cs delta) - vector = substInValAbs subst vva - in pprUncovered (vector, refuts) - --- | Apply a term substitution to a value vector abstraction. All VAs are --- transformed to PmExpr (used only before pretty printing). -substInValAbs :: TmVarCtEnv -> [ValAbs] -> [PmExpr] -substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr) +-- | Return True when any of the pattern match warnings ('allPmCheckWarnings') +-- are enabled, in which case we need to run the pattern match checker. +needToRunPmCheck :: DynFlags -> Origin -> Bool +needToRunPmCheck dflags origin + | isGenerated origin + = False + | otherwise + = notNull (filter (`wopt` dflags) allPmCheckWarnings) -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility) dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM () dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result = when (flag_i || flag_u) $ do - let exists_r = flag_i && notNull redundant && onlyBuiltin - exists_i = flag_i && notNull inaccessible && onlyBuiltin && not is_rec_upd + let exists_r = flag_i && notNull redundant + exists_i = flag_i && notNull inaccessible && not is_rec_upd exists_u = flag_u && (case uncovered of - TypeOfUncovered _ -> True - UncoveredPatterns u -> notNull u) + TypeOfUncovered _ -> True + UncoveredPatterns _ unc -> notNull unc) when exists_r $ forM_ redundant $ \(dL->L l q) -> do putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns) @@ -2500,12 +1478,11 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result (pprEqn q "has inaccessible right hand side")) when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $ case uncovered of - TypeOfUncovered ty -> warnEmptyCase ty - UncoveredPatterns candidates -> pprEqns candidates + TypeOfUncovered ty -> warnEmptyCase ty + UncoveredPatterns vars unc -> pprEqns vars unc where PmResult - { pmresultProvenance = prov - , pmresultRedundant = redundant + { pmresultRedundant = redundant , pmresultUncovered = uncovered , pmresultInaccessible = inaccessible } = pm_result @@ -2516,8 +1493,6 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result is_rec_upd = case kind of { RecUpd -> True; _ -> False } -- See Note [Inaccessible warnings for record updates] - onlyBuiltin = prov == FromBuiltin - maxPatterns = maxUncoveredPatterns dflags -- Print a single clause (for redundant/with-inaccessible-rhs) @@ -2525,14 +1500,12 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result f (pprPats kind (map unLoc q)) -- Print several clauses (for uncovered clauses) - pprEqns qs = pprContext False ctx (text "are non-exhaustive") $ \_ -> - case qs of -- See #11245 - [ValVec [] _] - -> text "Guards do not cover entire pattern space" - _missing -> let us = map ppr qs - in hang (text "Patterns not matched:") 4 - (vcat (take maxPatterns us) - $$ dots maxPatterns us) + pprEqns vars deltas = pprContext False ctx (text "are non-exhaustive") $ \_ -> + case vars of -- See #11245 + [] -> text "Guards do not cover entire pattern space" + _ -> let us = map (\delta -> pprUncovered delta vars) deltas + in hang (text "Patterns not matched:") 4 + (vcat (take maxPatterns us) $$ dots maxPatterns us) -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for -- which we only know the type and have no inhabitants at hand) @@ -2583,6 +1556,15 @@ dots maxPatterns qs | qs `lengthExceeds` maxPatterns = text "..." | otherwise = empty +-- | All warning flags that need to run the pattern match checker. +allPmCheckWarnings :: [WarningFlag] +allPmCheckWarnings = + [ Opt_WarnIncompletePatterns + , Opt_WarnIncompleteUniPatterns + , Opt_WarnIncompletePatternsRecUpd + , Opt_WarnOverlappingPatterns + ] + -- | Check whether the exhaustiveness checker should run (exhaustiveness only) exhaustive :: DynFlags -> HsMatchContext id -> Bool exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag @@ -2626,43 +1608,3 @@ pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc pprPats kind pats = sep [sep (map ppr pats), matchSeparator kind, text "..."] - --- Debugging Infrastructre - -tracePm :: String -> SDoc -> PmM () -tracePm herald doc = liftD $ tracePmD herald doc - - -tracePmD :: String -> SDoc -> DsM () -tracePmD herald doc = do - dflags <- getDynFlags - printer <- mkPrintUnqualifiedDs - liftIO $ dumpIfSet_dyn_printer printer dflags - Opt_D_dump_ec_trace (text herald $$ (nest 2 doc)) - - -pprPmPatDebug :: PmPat a -> SDoc -pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args) - = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)] -pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid -pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li -pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl -pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv) - <+> ppr ge -pprPmPatDebug PmFake = text "PmFake" - -pprPatVec :: PatVec -> SDoc -pprPatVec ps = hang (text "Pattern:") 2 - (brackets $ sep - $ punctuate (comma <> char '\n') (map pprPmPatDebug ps)) - -pprValAbs :: [ValAbs] -> SDoc -pprValAbs ps = hang (text "ValAbs:") 2 - (brackets $ sep - $ punctuate (comma) (map pprPmPatDebug ps)) - -pprValVecDebug :: ValVec -> SDoc -pprValVecDebug (ValVec vas _d) = text "ValVec" <+> - parens (pprValAbs vas) - -- <not a haddock> $$ ppr (delta_tm_cs _d) - -- <not a haddock> $$ ppr (delta_ty_cs _d) |