diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/basicTypes/NameEnv.hs | 13 | ||||
| -rw-r--r-- | compiler/basicTypes/PatSyn.hs | 14 | ||||
| -rw-r--r-- | compiler/deSugar/Check.hs | 2316 | ||||
| -rw-r--r-- | compiler/deSugar/DsBinds.hs | 16 | ||||
| -rw-r--r-- | compiler/deSugar/DsGRHSs.hs | 19 | ||||
| -rw-r--r-- | compiler/deSugar/DsMonad.hs | 33 | ||||
| -rw-r--r-- | compiler/deSugar/ExtractDocs.hs | 2 | ||||
| -rw-r--r-- | compiler/deSugar/Match.hs | 33 | ||||
| -rw-r--r-- | compiler/deSugar/PmExpr.hs | 450 | ||||
| -rw-r--r-- | compiler/deSugar/PmOracle.hs | 1872 | ||||
| -rw-r--r-- | compiler/deSugar/PmOracle.hs-boot | 7 | ||||
| -rw-r--r-- | compiler/deSugar/PmPpr.hs | 254 | ||||
| -rw-r--r-- | compiler/deSugar/TmOracle.hs | 362 | ||||
| -rw-r--r-- | compiler/ghc.cabal.in | 3 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 9 | ||||
| -rw-r--r-- | compiler/typecheck/TcSimplify.hs | 2 | ||||
| -rw-r--r-- | compiler/utils/Binary.hs | 1 | ||||
| -rw-r--r-- | compiler/utils/ListSetOps.hs | 9 | ||||
| -rw-r--r-- | compiler/utils/ListT.hs | 79 | ||||
| -rw-r--r-- | compiler/utils/Outputable.hs | 2 | ||||
| -rw-r--r-- | compiler/utils/Util.hs | 15 |
21 files changed, 3008 insertions, 2503 deletions
diff --git a/compiler/basicTypes/NameEnv.hs b/compiler/basicTypes/NameEnv.hs index 0b1cf435bc..5f6bdc5846 100644 --- a/compiler/basicTypes/NameEnv.hs +++ b/compiler/basicTypes/NameEnv.hs @@ -25,9 +25,9 @@ module NameEnv ( emptyDNameEnv, lookupDNameEnv, - delFromDNameEnv, + delFromDNameEnv, filterDNameEnv, mapDNameEnv, - alterDNameEnv, + adjustDNameEnv, alterDNameEnv, extendDNameEnv, -- ** Dependency analysis depAnal ) where @@ -151,8 +151,17 @@ lookupDNameEnv = lookupUDFM delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a delFromDNameEnv = delFromUDFM +filterDNameEnv :: (a -> Bool) -> DNameEnv a -> DNameEnv a +filterDNameEnv = filterUDFM + mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b mapDNameEnv = mapUDFM +adjustDNameEnv :: (a -> a) -> DNameEnv a -> Name -> DNameEnv a +adjustDNameEnv = adjustUDFM + alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a alterDNameEnv = alterUDFM + +extendDNameEnv :: DNameEnv a -> Name -> a -> DNameEnv a +extendDNameEnv = addToUDFM diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs index 008a0771fa..14a05b3258 100644 --- a/compiler/basicTypes/PatSyn.hs +++ b/compiler/basicTypes/PatSyn.hs @@ -184,6 +184,20 @@ to get the instantiation a := ty. This is very unlike DataCons, where univ tyvars match 1-1 the arguments of the TyCon. +Side note: I (SG) get the impression that instantiated return types should +generate a *required* constraint for pattern synonyms, rather than a *provided* +constraint like it's the case for GADTs. For example, I'd expect these +declarations to have identical semantics: + + pattern Just42 :: Maybe Int + pattern Just42 = Just 42 + + pattern Just'42 :: (a ~ Int) => Maybe a + pattern Just'42 = Just 42 + +The latter generates the proper required constraint, the former does not. +Also rather different to GADTs is the fact that Just42 doesn't have any +universally quantified type variables, whereas Just'42 or MkS above has. Note [Pattern synonym representation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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) diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index 4a6a463b2d..cea7f3215b 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -29,7 +29,7 @@ import {-# SOURCE #-} Match( matchWrapper ) import DsMonad import DsGRHSs import DsUtils -import Check ( checkGuardMatches ) +import Check ( needToRunPmCheck, addTyCsDs, checkGuardMatches ) import HsSyn -- lots of things import CoreSyn -- lots of things @@ -186,11 +186,15 @@ dsHsBind dflags (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts , abs_exports = exports , abs_ev_binds = ev_binds , abs_binds = binds, abs_sig = has_sig }) - = do { ds_binds <- addDictsDs (listToBag dicts) $ - dsLHsBinds binds - -- addDictsDs: push type constraints deeper - -- for inner pattern match check - -- See Check, Note [Type and Term Equality Propagation] + = do { ds_binds <- applyWhen (needToRunPmCheck dflags FromSource) + -- FromSource might not be accurate, but at worst + -- we do superfluous calls to the pattern match + -- oracle. + -- addTyCsDs: push type constraints deeper + -- for inner pattern match check + -- See Check, Note [Type and Term Equality Propagation] + (addTyCsDs (listToBag dicts)) + (dsLHsBinds binds) ; ds_ev_binds <- dsTcEvBinds_s ev_binds diff --git a/compiler/deSugar/DsGRHSs.hs b/compiler/deSugar/DsGRHSs.hs index 5adc661388..b0d35d0b2a 100644 --- a/compiler/deSugar/DsGRHSs.hs +++ b/compiler/deSugar/DsGRHSs.hs @@ -23,7 +23,9 @@ import MkCore import CoreSyn import CoreUtils (bindNonRec) -import Check (genCaseTmCs2) +import BasicTypes (Origin(FromSource)) +import DynFlags +import Check (needToRunPmCheck, addTyCsDs, addPatTmCs, addScrutTmCs) import DsMonad import DsUtils import Type ( Type ) @@ -122,11 +124,16 @@ matchGuards (BindStmt _ pat bind_rhs _ _ : stmts) ctx rhs rhs_ty = do let upat = unLoc pat dicts = collectEvVarsPat upat match_var <- selectMatchVar upat - tm_cs <- genCaseTmCs2 (Just bind_rhs) [upat] [match_var] - match_result <- addDictsDs dicts $ - addTmCsDs tm_cs $ - -- See Note [Type and Term Equality Propagation] in Check - matchGuards stmts ctx rhs rhs_ty + + dflags <- getDynFlags + match_result <- + -- See Note [Type and Term Equality Propagation] in Check + applyWhen (needToRunPmCheck dflags FromSource) + -- FromSource might not be accurate, but at worst + -- we do superfluous calls to the pattern match + -- oracle. + (addTyCsDs dicts . addScrutTmCs (Just bind_rhs) [match_var] . addPatTmCs [upat] [match_var]) + (matchGuards stmts ctx rhs rhs_ty) core_rhs <- dsLExpr bind_rhs match_result' <- matchSinglePatVar match_var (StmtCtxt ctx) pat rhs_ty match_result diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs index 9534b4e20b..d937b3b134 100644 --- a/compiler/deSugar/DsMonad.hs +++ b/compiler/deSugar/DsMonad.hs @@ -29,8 +29,8 @@ module DsMonad ( DsMetaEnv, DsMetaVal(..), dsGetMetaEnv, dsLookupMetaEnv, dsExtendMetaEnv, - -- Getting and setting EvVars and term constraints in local environment - getDictsDs, addDictsDs, getTmCsDs, addTmCsDs, + -- Getting and setting pattern match oracle states + getPmDelta, updPmDelta, -- Iterations for pm checking incrCheckPmIterDs, resetPmIterDs, dsGetCompleteMatches, @@ -70,7 +70,7 @@ import BasicTypes ( Origin ) import DataCon import ConLike import TyCon -import PmExpr +import {-# SOURCE #-} PmOracle import Id import Module import Outputable @@ -82,7 +82,6 @@ import NameEnv import DynFlags import ErrUtils import FastString -import Var (EvVar) import UniqFM ( lookupWithDefaultUFM ) import Literal ( mkLitString ) import CostCentreState @@ -285,8 +284,7 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var pmvar cc_st_var } lcl_env = DsLclEnv { dsl_meta = emptyNameEnv , dsl_loc = real_span - , dsl_dicts = emptyBag - , dsl_tm_cs = emptyBag + , dsl_delta = initDelta , dsl_pm_iter = pmvar } in (gbl_env, lcl_env) @@ -386,23 +384,14 @@ the @SrcSpan@ being carried around. getGhcModeDs :: DsM GhcMode getGhcModeDs = getDynFlags >>= return . ghcMode --- | Get in-scope type constraints (pm check) -getDictsDs :: DsM (Bag EvVar) -getDictsDs = do { env <- getLclEnv; return (dsl_dicts env) } +-- | Get the current pattern match oracle state. See 'dsl_delta'. +getPmDelta :: DsM Delta +getPmDelta = do { env <- getLclEnv; return (dsl_delta env) } --- | Add in-scope type constraints (pm check) -addDictsDs :: Bag EvVar -> DsM a -> DsM a -addDictsDs ev_vars - = updLclEnv (\env -> env { dsl_dicts = unionBags ev_vars (dsl_dicts env) }) - --- | Get in-scope term constraints (pm check) -getTmCsDs :: DsM (Bag TmVarCt) -getTmCsDs = do { env <- getLclEnv; return (dsl_tm_cs env) } - --- | Add in-scope term constraints (pm check) -addTmCsDs :: Bag TmVarCt -> DsM a -> DsM a -addTmCsDs tm_cs - = updLclEnv (\env -> env { dsl_tm_cs = unionBags tm_cs (dsl_tm_cs env) }) +-- | Set the pattern match oracle state within the scope of the given action. +-- See 'dsl_delta'. +updPmDelta :: Delta -> DsM a -> DsM a +updPmDelta delta = updLclEnv (\env -> env { dsl_delta = delta }) -- | Increase the counter for elapsed pattern match check iterations. -- If the current counter is already over the limit, fail diff --git a/compiler/deSugar/ExtractDocs.hs b/compiler/deSugar/ExtractDocs.hs index ce5299443b..4d7f115074 100644 --- a/compiler/deSugar/ExtractDocs.hs +++ b/compiler/deSugar/ExtractDocs.hs @@ -289,7 +289,7 @@ ungroup group_ = mkDecls (typesigs . hs_valds) (SigD noExtField) group_ ++ mkDecls (valbinds . hs_valds) (ValD noExtField) group_ where - typesigs (XValBindsLR (NValBinds _ sigs)) = filter (isUserSig . unLoc) sigs + typesigs (XValBindsLR (NValBinds _ sig)) = filter (isUserSig . unLoc) sig typesigs ValBinds{} = error "expected XValBindsLR" valbinds (XValBindsLR (NValBinds binds _)) = diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs index 921b829fb9..a0576494a0 100644 --- a/compiler/deSugar/Match.hs +++ b/compiler/deSugar/Match.hs @@ -690,7 +690,13 @@ Call @match@ with all of this information! matchWrapper :: HsMatchContext Name -- ^ For shadowing warning messages - -> Maybe (LHsExpr GhcTc) -- ^ Scrutinee, if we check a case expr + -> Maybe (LHsExpr GhcTc) -- ^ Scrutinee. (Just scrut) for a case expr + -- case scrut of { p1 -> e1 ... } + -- (and in this case the MatchGroup will + -- have all singleton patterns) + -- Nothing for a function definition + -- f p1 q1 = ... -- No "scrutinee" + -- f p2 q2 = ... -- in this case -> MatchGroup GhcTc (LHsExpr GhcTc) -- ^ Matches being desugared -> DsM ([Id], CoreExpr) -- ^ Results (usually passed to 'match') @@ -730,25 +736,30 @@ matchWrapper ctxt mb_scr (MG { mg_alts = (dL->L _ matches) ; eqns_info <- mapM (mk_eqn_info new_vars) matches - -- pattern match check warnings - ; unless (isGenerated origin) $ - when (isAnyPmCheckEnabled dflags (DsMatchContext ctxt locn)) $ - addTmCsDs (genCaseTmCs1 mb_scr new_vars) $ - -- See Note [Type and Term Equality Propagation] - checkMatches dflags (DsMatchContext ctxt locn) new_vars matches + -- Pattern match check warnings for /this match-group/ + ; when (isMatchContextPmChecked dflags origin ctxt) $ + addScrutTmCs mb_scr new_vars $ + -- See Note [Type and Term Equality Propagation] + checkMatches dflags (DsMatchContext ctxt locn) new_vars matches ; result_expr <- handleWarnings $ matchEquations ctxt new_vars eqns_info rhs_ty ; return (new_vars, result_expr) } where + -- Called once per equation in the match, or alternative in the case mk_eqn_info vars (dL->L _ (Match { m_pats = pats, m_grhss = grhss })) = do { dflags <- getDynFlags ; let upats = map (unLoc . decideBangHood dflags) pats dicts = collectEvVarsPats upats - ; tm_cs <- genCaseTmCs2 mb_scr upats vars - ; match_result <- addDictsDs dicts $ -- See Note [Type and Term Equality Propagation] - addTmCsDs tm_cs $ -- See Note [Type and Term Equality Propagation] - dsGRHSs ctxt grhss rhs_ty + + ; match_result <- + -- Extend the environment with knowledge about + -- the matches before desguaring the RHS + -- See Note [Type and Term Equality Propagation] + applyWhen (needToRunPmCheck dflags origin) + (addTyCsDs dicts . addScrutTmCs mb_scr vars . addPatTmCs upats vars) + (dsGRHSs ctxt grhss rhs_ty) + ; return (EqnInfo { eqn_pats = upats , eqn_orig = FromSource , eqn_rhs = match_result }) } diff --git a/compiler/deSugar/PmExpr.hs b/compiler/deSugar/PmExpr.hs index 3697dd8cc1..f83c63e4fd 100644 --- a/compiler/deSugar/PmExpr.hs +++ b/compiler/deSugar/PmExpr.hs @@ -6,29 +6,38 @@ Haskell expressions (as used by the pattern matching checker) and utilities. {-# LANGUAGE CPP #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} module PmExpr ( - PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), - eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr + PmLit(..), PmLitValue(..), PmAltCon(..), + pmAltConType, PmEquality(..), eqPmAltCon, + pmLitType, literalToPmLit, negatePmLit, overloadPmLit, + pmLitAsStringLit, coreExprAsPmLit ) where #include "HsVersions.h" import GhcPrelude -import BasicTypes (SourceText) -import FastString (FastString, unpackFS) -import HsSyn +import Util +import FastString import Id import Name import DataCon import ConLike -import TcEvidence (isErasableHsWrapper) -import TcType (isStringTy) -import TysWiredIn import Outputable -import SrcLoc +import Maybes +import Type +import TyCon +import Literal +import CoreSyn +import CoreUtils (exprType) +import PrelNames +import TysWiredIn +import TysPrim + +import Numeric (fromRat) +import Data.Foldable (find) +import Data.Ratio {- %************************************************************************ @@ -38,52 +47,135 @@ import SrcLoc %************************************************************************ -} -{- Note [PmExprOther in PmExpr] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Since there is no plan to extend the (currently pretty naive) term oracle in -the near future, instead of playing with the verbose (HsExpr Id), we lift it to -PmExpr. All expressions the term oracle does not handle are wrapped by the -constructor PmExprOther. Note that we do not perform substitution in -PmExprOther. Because of this, we do not even print PmExprOther, since they may -refer to variables that are otherwise substituted away. --} - -- ---------------------------------------------------------------------------- -- ** Types --- | Lifted expressions for pattern match checking. -data PmExpr = PmExprVar Name - | PmExprCon ConLike [PmExpr] - | PmExprLit PmLit - | PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr] - - -mkPmExprData :: DataCon -> [PmExpr] -> PmExpr -mkPmExprData dc args = PmExprCon (RealDataCon dc) args - -- | Literals (simple and overloaded ones) for pattern match checking. -data PmLit = PmSLit (HsLit GhcTc) -- simple - | PmOLit Bool {- is it negated? -} (HsOverLit GhcTc) -- overloaded - --- | Equality between literals for pattern match checking. -eqPmLit :: PmLit -> PmLit -> Bool -eqPmLit (PmSLit l1) (PmSLit l2) = l1 == l2 -eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2 - -- See Note [Undecidable Equality for Overloaded Literals] -eqPmLit _ _ = False - --- | Represents a match against a literal. We mostly use it to to encode shapes --- for a variable that immediately lead to a refutation. -- --- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'. -newtype PmAltCon = PmAltLit PmLit - deriving Outputable - +-- See Note [Undecidable Equality for PmAltCons] +data PmLit = PmLit + { pm_lit_ty :: Type + , pm_lit_val :: PmLitValue } + +data PmLitValue + = PmLitInt Integer + | PmLitRat Rational + | PmLitChar Char + -- We won't actually see PmLitString in the oracle since we desugar strings to + -- lists + | PmLitString FastString + | PmLitOverInt Int {- How often Negated? -} Integer + | PmLitOverRat Int {- How often Negated? -} Rational + | PmLitOverString FastString + +-- | Undecidable semantic equality result. +-- See Note [Undecidable Equality for PmAltCons] +data PmEquality + = Equal + | Disjoint + | PossiblyOverlap + deriving (Eq, Show) + +-- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@. +decEquality :: Bool -> PmEquality +decEquality True = Equal +decEquality False = Disjoint + +-- | Undecidable equality for values represented by 'PmLit's. +-- See Note [Undecidable Equality for PmAltCons] +-- +-- * @Just True@ ==> Surely equal +-- * @Just False@ ==> Surely different (non-overlapping, even!) +-- * @Nothing@ ==> Equality relation undecidable +eqPmLit :: PmLit -> PmLit -> PmEquality +eqPmLit (PmLit t1 v1) (PmLit t2 v2) + -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined + | not (t1 `eqType` t2) = Disjoint + | otherwise = go v1 v2 + where + go (PmLitInt i1) (PmLitInt i2) = decEquality (i1 == i2) + go (PmLitRat r1) (PmLitRat r2) = decEquality (r1 == r2) + go (PmLitChar c1) (PmLitChar c2) = decEquality (c1 == c2) + go (PmLitString s1) (PmLitString s2) = decEquality (s1 == s2) + go (PmLitOverInt n1 i1) (PmLitOverInt n2 i2) + | n1 == n2 && i1 == i2 = Equal + go (PmLitOverRat n1 r1) (PmLitOverRat n2 r2) + | n1 == n2 && r1 == r2 = Equal + go (PmLitOverString s1) (PmLitOverString s2) + | s1 == s2 = Equal + go _ _ = PossiblyOverlap + +-- | Syntactic equality. +instance Eq PmLit where + a == b = eqPmLit a b == Equal + +-- | Type of a 'PmLit' +pmLitType :: PmLit -> Type +pmLitType (PmLit ty _) = ty + +-- | Type of a 'PmAltCon' +pmAltConType :: PmAltCon -> [Type] -> Type +pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit +pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys + +-- | Undecidable equality for values represented by 'ConLike's. +-- See Note [Undecidable Equality for PmAltCons]. +-- 'PatSynCon's aren't enforced to be generative, so two syntactically different +-- 'PatSynCon's might match the exact same values. Without looking into and +-- reasoning about the pattern synonym's definition, we can't decide if their +-- sets of matched values is different. +-- +-- * @Just True@ ==> Surely equal +-- * @Just False@ ==> Surely different (non-overlapping, even!) +-- * @Nothing@ ==> Equality relation undecidable +eqConLike :: ConLike -> ConLike -> PmEquality +eqConLike (RealDataCon dc1) (RealDataCon dc2) = decEquality (dc1 == dc2) +eqConLike (PatSynCon psc1) (PatSynCon psc2) + | psc1 == psc2 + = Equal +eqConLike _ _ = PossiblyOverlap + +-- | Represents the head of a match against a 'ConLike' or literal. +-- Really similar to 'CoreSyn.AltCon'. +data PmAltCon = PmAltConLike ConLike + | PmAltLit PmLit + +-- | We can't in general decide whether two 'PmAltCon's match the same set of +-- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a +-- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'. +-- See Note [Undecidable Equality for PmAltCons]. +-- +-- * @Just True@ ==> Surely equal +-- * @Just False@ ==> Surely different (non-overlapping, even!) +-- * @Nothing@ ==> Equality relation undecidable +-- +-- Examples (omitting some constructor wrapping): +-- +-- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is +-- decidable +-- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is +-- decidable +-- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality +-- is undecidable +-- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is +-- undecidable +-- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit +-- comparisons are undecidable without reasoning about the wrapped @Int#@ +-- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume +-- reflexivity for overloaded literals +-- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity +-- for Pattern Synonyms +eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality +eqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = eqConLike cl1 cl2 +eqPmAltCon (PmAltLit l1) (PmAltLit l2) = eqPmLit l1 l2 +eqPmAltCon _ _ = PossiblyOverlap + +-- | Syntactic equality. instance Eq PmAltCon where - PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2 + a == b = eqPmAltCon a b == Equal -{- Note [Undecidable Equality for Overloaded Literals] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Undecidable Equality for PmAltCons] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Equality on overloaded literals is undecidable in the general case. Consider the following example: @@ -96,25 +188,19 @@ the following example: f 1 = () -- Clause A f 2 = () -- Clause B -Clause B is redundant but to detect this, we should be able to solve the -constraint: False ~ (fromInteger 2 ~ fromInteger 1) which means that we -have to look through function `fromInteger`, whose implementation could +Clause B is redundant but to detect this, we must decide the constraint: +@fromInteger 2 ~ fromInteger 1@ which means that we +have to look through function @fromInteger@, whose implementation could be anything. This poses difficulties for: 1. The expressive power of the check. We cannot expect a reasonable implementation of pattern matching to detect - that fromInteger 2 ~ fromInteger 1 is True, unless we unfold function + that @fromInteger 2 ~ fromInteger 1@ is True, unless we unfold function fromInteger. This puts termination at risk and is undecidable in the general case. -2. Performance. - Having an unresolved constraint False ~ (fromInteger 2 ~ fromInteger 1) - lying around could become expensive really fast. Ticket #11161 illustrates - how heavy use of overloaded literals can generate plenty of those - constraints, effectively undermining the term oracle's performance. - -3. Error nessages/Warnings. - What should our message for `f` above be? A reasonable approach would be +2. Error messages/Warnings. + What should our message for @f@ above be? A reasonable approach would be to issue: Pattern matches are (potentially) redundant: @@ -122,8 +208,13 @@ be anything. This poses difficulties for: but seems to complex and confusing for the user. -We choose to treat overloaded literals that look different as different. The -impact of this is the following: +We choose to equate only obviously equal overloaded literals, in all other cases +we signal undecidability by returning Nothing from 'eqPmAltCons'. We do +better for non-overloaded literals, because we know their fromInteger/fromString +implementation is actually injective, allowing us to simplify the constraint +@fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable. + +The impact of this treatment of overloaded literals is the following: * Redundancy checking is rather conservative, since it cannot see that clause B above is redundant. @@ -136,120 +227,100 @@ impact of this is the following: * The warnings issued are simpler. - * We do not play on the safe side, strictly speaking. The assumption that - 1 /= 2 makes the redundancy check more conservative but at the same time - makes its dual (exhaustiveness check) unsafe. This we can live with, mainly - for two reasons: - 1. At the moment we do not use the results of the check during compilation - where this would be a disaster (could result in runtime errors even if - our function was deemed exhaustive). - 2. Pattern matcing on literals can never be considered exhaustive unless we - have a catch-all clause. Hence, this assumption affects mainly the - appearance of the warnings and is, in practice safe. +Similar reasoning applies to pattern synonyms: In contrast to data constructors, +which are generative, constraints like F a ~ G b for two different pattern +synonyms F and G aren't immediately unsatisfiable. We assume F a ~ F a, though. -} --- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e@. -data TmVarCt = TVC !Id !PmExpr +literalToPmLit :: Type -> Literal -> Maybe PmLit +literalToPmLit ty l = PmLit ty <$> go l + where + go (LitChar c) = Just (PmLitChar c) + go (LitFloat r) = Just (PmLitRat r) + go (LitDouble r) = Just (PmLitRat r) + go (LitString s) = Just (PmLitString (mkFastStringByteString s)) + go (LitNumber _ i _) = Just (PmLitInt i) + go _ = Nothing + +negatePmLit :: PmLit -> Maybe PmLit +negatePmLit (PmLit ty v) = PmLit ty <$> go v + where + go (PmLitInt i) = Just (PmLitInt (-i)) + go (PmLitRat r) = Just (PmLitRat (-r)) + go (PmLitOverInt n i) = Just (PmLitOverInt (n+1) i) + go (PmLitOverRat n r) = Just (PmLitOverRat (n+1) r) + go _ = Nothing + +overloadPmLit :: Type -> PmLit -> Maybe PmLit +overloadPmLit ty (PmLit _ v) = PmLit ty <$> go v + where + go (PmLitInt i) = Just (PmLitOverInt 0 i) + go (PmLitRat r) = Just (PmLitOverRat 0 r) + go (PmLitString s) + | ty `eqType` stringTy = Just v + | otherwise = Just (PmLitOverString s) + go _ = Nothing -instance Outputable TmVarCt where - ppr (TVC x e) = ppr x <+> char '~' <+> ppr e +pmLitAsStringLit :: PmLit -> Maybe FastString +pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s +pmLitAsStringLit _ = Nothing -- ---------------------------------------------------------------------------- -- ** Predicates on PmExpr --- | Check if an expression is lifted or not -isNotPmExprOther :: PmExpr -> Bool -isNotPmExprOther (PmExprOther _) = False -isNotPmExprOther _expr = True - -- ----------------------------------------------------------------------- -- ** Lift source expressions (HsExpr Id) to PmExpr -lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr -lhsExprToPmExpr (dL->L _ e) = hsExprToPmExpr e - -hsExprToPmExpr :: HsExpr GhcTc -> PmExpr - --- Translating HsVar to flexible meta variables in the unification problem is --- morally wrong, but it does the right thing for now. --- In contrast to the situation in pattern matches, HsVars in expression syntax --- are object language variables, most similar to rigid variables with an --- unknown solution. The correct way would be to handle them through PmExprOther --- and identify syntactically equal occurrences by the same rigid meta variable, --- but we can't compare the wrapped HsExpr for equality. Hence we are stuck with --- this hack. -hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x)) - --- Translating HsConLikeOut to a flexible meta variable is misleading. --- For an example why, consider `consAreRigid` in --- `testsuite/tests/pmcheck/should_compile/PmExprVars.hs`. --- hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName c) - --- Desugar literal strings as a list of characters. For other literal values, --- keep it as it is. --- See `translatePat` in Check.hs (the `NPat` and `LitPat` case), and --- Note [Translate Overloaded Literal for Exhaustiveness Checking]. -hsExprToPmExpr (HsOverLit _ olit) - | OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit, isStringTy ty - = stringExprToList src s - | otherwise = PmExprLit (PmOLit False olit) -hsExprToPmExpr (HsLit _ lit) - | HsString src s <- lit - = stringExprToList src s - | otherwise = PmExprLit (PmSLit lit) - -hsExprToPmExpr e@(NegApp _ (dL->L _ neg_expr) _) - | PmExprLit (PmOLit False olit) <- hsExprToPmExpr neg_expr - -- NB: DON'T simply @(NegApp (NegApp olit))@ as @x@. when extension - -- @RebindableSyntax@ enabled, (-(-x)) may not equals to x. - = PmExprLit (PmOLit True olit) - | otherwise = PmExprOther e - -hsExprToPmExpr (HsPar _ (dL->L _ e)) = hsExprToPmExpr e - -hsExprToPmExpr e@(ExplicitTuple _ ps boxity) - | all tupArgPresent ps = mkPmExprData tuple_con tuple_args - | otherwise = PmExprOther e - where - tuple_con = tupleDataCon boxity (length ps) - tuple_args = [ lhsExprToPmExpr e | (dL->L _ (Present _ e)) <- ps ] - -hsExprToPmExpr e@(ExplicitList _ mb_ol elems) - | Nothing <- mb_ol = foldr cons nil (map lhsExprToPmExpr elems) - | otherwise = PmExprOther e {- overloaded list: No PmExprApp -} - where - cons x xs = mkPmExprData consDataCon [x,xs] - nil = mkPmExprData nilDataCon [] - --- we want this but we would have to make everything monadic :/ --- ./compiler/deSugar/DsMonad.hs:397:dsLookupDataCon :: Name -> DsM DataCon --- --- hsExprToPmExpr (RecordCon c _ binds) = do --- con <- dsLookupDataCon (unLoc c) --- args <- mapM lhsExprToPmExpr (hsRecFieldsArgs binds) --- return (PmExprCon con args) -hsExprToPmExpr e@(RecordCon {}) = PmExprOther e - -hsExprToPmExpr (HsTick _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsBinTick _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsTickPragma _ _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsSCC _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (HsCoreAnn _ _ _ e) = lhsExprToPmExpr e -hsExprToPmExpr (ExprWithTySig _ e _) = lhsExprToPmExpr e -hsExprToPmExpr (HsWrap _ w e) - -- A dictionary application spoils e and we have no choice but to return an - -- PmExprOther. Same thing for other stuff that can't erased in the - -- compilation process. Otherwise this bites in - -- teststuite/tests/pmcheck/should_compile/PmExprVars.hs. - | isErasableHsWrapper w = hsExprToPmExpr e -hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle - -stringExprToList :: SourceText -> FastString -> PmExpr -stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s)) +coreExprAsPmLit :: CoreExpr -> Maybe PmLit +-- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined +coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e +coreExprAsPmLit (Lit l) = literalToPmLit (literalType l) l +coreExprAsPmLit e = case collectArgs e of + (Var x, [Lit l]) + | Just dc <- isDataConWorkId_maybe x + , dc `elem` [intDataCon, wordDataCon, charDataCon, floatDataCon, doubleDataCon] + -> literalToPmLit (exprType e) l + (Var x, [_ty, Lit n, Lit d]) + | Just dc <- isDataConWorkId_maybe x + , dataConName dc == ratioDataConName + -- HACK: just assume we have a literal double. This case only occurs for + -- overloaded lits anyway, so we immediately override type information + -> literalToPmLit (exprType e) (mkLitDouble (litValue n % litValue d)) + (Var x, args) + -- Take care of -XRebindableSyntax. The last argument should be the (only) + -- integer literal, otherwise we can't really do much about it. + | [Lit l] <- dropWhile (not . is_lit) args + -- getOccFS because of -XRebindableSyntax + , getOccFS (idName x) == getOccFS fromIntegerName + -> literalToPmLit (literalType l) l >>= overloadPmLit (exprType e) + (Var x, args) + -- Similar to fromInteger case + | [r] <- dropWhile (not . is_ratio) args + , getOccFS (idName x) == getOccFS fromRationalName + -> coreExprAsPmLit r >>= overloadPmLit (exprType e) + (Var x, [Type _ty, _dict, s]) + | idName x == fromStringName + -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings + -> coreExprAsPmLit s >>= overloadPmLit (exprType e) + -- These last two cases handle String literals + (Var x, [Type ty]) + | Just dc <- isDataConWorkId_maybe x + , dc == nilDataCon + , ty `eqType` charTy + -> literalToPmLit stringTy (mkLitString "") + (Var x, [Lit l]) + | idName x `elem` [unpackCStringName, unpackCStringUtf8Name] + -> literalToPmLit stringTy l + _ -> Nothing where - cons x xs = mkPmExprData consDataCon [x,xs] - nil = mkPmExprData nilDataCon [] - charToPmExpr c = PmExprLit (PmSLit (HsChar src c)) + is_lit Lit{} = True + is_lit _ = False + is_ratio (Type _) = False + is_ratio r + | Just (tc, _) <- splitTyConApp_maybe (exprType r) + = tyConName tc == ratioTyConName + | otherwise + = False {- %************************************************************************ @@ -259,22 +330,35 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s)) %************************************************************************ -} -instance Outputable PmLit where - ppr (PmSLit l) = pmPprHsLit l - ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l +instance Outputable PmLitValue where + ppr (PmLitInt i) = ppr i + ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough + ppr (PmLitChar c) = pprHsChar c + ppr (PmLitString s) = pprHsString s + ppr (PmLitOverInt n i) = minuses n (ppr i) + ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r))) + ppr (PmLitOverString s) = pprHsString s + +-- Take care of negated literals +minuses :: Int -> SDoc -> SDoc +minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n -instance Outputable PmExpr where - ppr = go (0 :: Int) +instance Outputable PmLit where + ppr (PmLit ty v) = ppr v <> suffix where - go _ (PmExprLit l) = ppr l - go _ (PmExprVar v) = ppr v - go _ (PmExprOther e) = angleBrackets (ppr e) - go _ (PmExprCon (RealDataCon dc) args) - | isTupleDataCon dc = parens $ comma_sep $ map ppr args - | dc == consDataCon = brackets $ comma_sep $ map ppr (list_cells args) - where - comma_sep = fsep . punctuate comma - list_cells (hd:tl) = hd : list_cells tl - list_cells _ = [] - go prec (PmExprCon cl args) - = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args)) + -- Some ad-hoc hackery for displaying proper lit suffixes based on type + tbl = [ (intPrimTy, primIntSuffix) + , (int64PrimTy, primInt64Suffix) + , (wordPrimTy, primWordSuffix) + , (word64PrimTy, primWord64Suffix) + , (charPrimTy, primCharSuffix) + , (floatPrimTy, primFloatSuffix) + , (doublePrimTy, primDoubleSuffix) ] + suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl) + +instance Outputable PmAltCon where + ppr (PmAltConLike cl) = ppr cl + ppr (PmAltLit l) = ppr l + +instance Outputable PmEquality where + ppr = text . show diff --git a/compiler/deSugar/PmOracle.hs b/compiler/deSugar/PmOracle.hs new file mode 100644 index 0000000000..93c4d1d959 --- /dev/null +++ b/compiler/deSugar/PmOracle.hs @@ -0,0 +1,1872 @@ +{- +Authors: George Karachalias <george.karachalias@cs.kuleuven.be> + Sebastian Graf <sgraf1337@gmail.com> + Ryan Scott <ryan.gl.scott@gmail.com> +-} + +{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-} + +-- | The pattern match oracle. The main export of the module are the functions +-- 'addTmCt', 'refineToAltCon' and 'addRefutableAltCon' for adding +-- facts to the oracle, and 'provideEvidenceForEquation' to turn a 'Delta' into +-- a concrete evidence for an equation. +module PmOracle ( + + DsM, tracePm, mkPmId, + Delta, initDelta, canDiverge, lookupRefuts, lookupSolution, + lookupNumberOfRefinements, + + TmCt(..), + inhabitants, + addTypeEvidence, -- Add type equalities + addRefutableAltCon, -- Add a negative term equality + addTmCt, -- Add a positive term equality x ~ e + addVarCoreCt, -- Add a positive term equality x ~ core_expr + refineToAltCon, -- Add a positive refinement x ~ K _ _ + tmOracle, -- Add multiple positive term equalities + provideEvidenceForEquation, + ) where + +#include "HsVersions.h" + +import GhcPrelude + +import PmExpr + +import DynFlags +import Outputable +import ErrUtils +import Util +import Bag +import UniqDSet +import Unique +import Id +import VarEnv +import UniqDFM +import Var (EvVar) +import Name +import CoreSyn +import CoreOpt (exprIsConApp_maybe) +import CoreUtils (exprType) +import MkCore (mkListExpr, mkCharExpr) +import UniqSupply +import FastString +import SrcLoc +import ListSetOps (unionLists) +import Maybes +import ConLike +import DataCon +import PatSyn +import TyCon +import TysWiredIn +import TysPrim (tYPETyCon) +import TyCoRep +import Type +import TcSimplify (tcNormalise, tcCheckSatisfiability) +import Unify (tcMatchTy) +import TcRnTypes (pprEvVarWithType, completeMatchConLikes) +import Coercion +import MonadUtils hiding (foldlM) +import DsMonad hiding (foldlM) +import FamInst +import FamInstEnv + +import Control.Monad (zipWithM, guard, mzero) +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.State.Strict +import Data.Bifunctor (second) +import Data.Foldable (foldlM) +import Data.List (find) +import Data.List.NonEmpty (NonEmpty (..)) +import qualified Data.List.NonEmpty as NonEmpty +import qualified Data.Semigroup as Semigroup + +-- Debugging Infrastructre + +tracePm :: String -> SDoc -> DsM () +tracePm herald doc = do + dflags <- getDynFlags + printer <- mkPrintUnqualifiedDs + liftIO $ dumpIfSet_dyn_printer printer dflags + Opt_D_dump_ec_trace (text herald $$ (nest 2 doc)) + +-- | 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) + +----------------------------------------------- +-- * Caching possible matches of a COMPLETE set + +type ConLikeSet = UniqDSet ConLike + +-- | A data type caching the results of 'completeMatchConLikes' with support for +-- deletion of contructors that were already matched on. +data PossibleMatches + = PM TyCon (NonEmpty ConLikeSet) + -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma + -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE + -- set at all, for which we have 'NoPM' + | NoPM + -- ^ No COMPLETE set for this type (yet). Think of overloaded literals. + +instance Outputable PossibleMatches where + ppr (PM _tc cs) = ppr (NonEmpty.toList cs) + ppr NoPM = text "<NoPM>" + +initIM :: Type -> DsM (Maybe PossibleMatches) +initIM ty = case splitTyConApp_maybe ty of + Nothing -> pure Nothing + 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 rdcs = maybeToList 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 + pure (PM tc . fmap mkUniqDSet <$> NonEmpty.nonEmpty (rdcs ++ pscs)) + +markMatched :: ConLike -> PossibleMatches -> PossibleMatches +markMatched con (PM tc ms) = PM tc (fmap (`delOneFromUniqDSet` con) ms) +markMatched _ NoPM = NoPM + +-- | Satisfiability decisions as a data type. The @proof@ can carry a witness +-- for satisfiability and might even be instantiated to 'Data.Void.Void' to +-- degenerate into a semi-decision predicate. +data Satisfiability proof + = Unsatisfiable + | PossiblySatisfiable + | Satisfiable !proof + +maybeSatisfiable :: Maybe a -> Satisfiability a +maybeSatisfiable (Just a) = Satisfiable a +maybeSatisfiable Nothing = Unsatisfiable + +-- | Tries to return one of the possible 'ConLike's from one of the COMPLETE +-- sets. If the 'PossibleMatches' was inhabited before (cf. 'ensureInhabited') +-- this 'ConLike' is evidence for that assurance. +getUnmatchedConstructor :: PossibleMatches -> Satisfiability ConLike +getUnmatchedConstructor NoPM = PossiblySatisfiable +getUnmatchedConstructor (PM _tc ms) + = maybeSatisfiable $ NonEmpty.head <$> traverse pick_one_conlike ms + where + pick_one_conlike cs = case uniqDSetToList cs of + [] -> Nothing + (cl:_) -> Just cl + +--------------------------------------------------- +-- * Instantiating constructors, types and evidence + +newEvVar :: Name -> Type -> EvVar +newEvVar name ty = mkLocalId name ty + +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) + +-- | Instantiate a 'ConLike' given its universal type arguments. Instantiates +-- existential and term binders with fresh variables of appropriate type. +-- Also returns instantiated evidence variables from the match and the types of +-- strict constructor fields. +mkOneConFull :: [Type] -> ConLike -> DsM ([Id], [EvVar], [Type], [TyVar]) +-- * 'con' K is a ConLike +-- - In the case of DataCons and most PatSynCons, these +-- are associated with a particular TyCon T +-- - But there are PatSynCons for this is not the case! See #11336, #17112 +-- +-- * 'arg_tys' tys are the types K's universally quantified type +-- variables should be instantiated to. +-- - For DataCons and most PatSyns these are the arguments of their TyCon +-- - For cases like in #11336, #17112, the univ_ts include those variables +-- from the view pattern, so tys will have to come from the type checker. +-- They can't easily be recovered from the result type. +-- +-- After instantiating the universal tyvars of K to tys we get +-- K @tys :: forall bs. Q => s1 .. sn -> T tys +-- Note that if K is a PatSynCon, depending on arg_tys, T might not necessarily +-- be a concrete TyCon. +-- +-- Suppose y1 is a strict field. Then we get +-- Results: [y1,..,yn] +-- Q +-- [s1] +-- [e1,..,en] +mkOneConFull arg_tys con = do + let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , field_tys, _con_res_ty) + = conLikeFullSig con + -- pprTrace "mkOneConFull" (ppr con $$ ppr arg_tys $$ ppr univ_tvs $$ ppr _con_res_ty) (return ()) + -- Substitute universals for type arguments + let subst_univ = zipTvSubst univ_tvs arg_tys + -- Instantiate fresh existentials as arguments to the contructor + (subst, ex_tvs') <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM + let field_tys' = substTys subst field_tys + -- Instantiate fresh term variables (VAs) as arguments to the constructor + vars <- mapM mkPmId field_tys' + -- All constraints bound by the constructor (alpha-renamed), these are added + -- to the type oracle + let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas) + theta_ev_vars <- mapM (nameType "pm") theta_cs + -- Figure out the types of strict constructor fields + let arg_is_banged = map isBanged $ conLikeImplBangs con + strict_arg_tys = filterByList arg_is_banged field_tys' + return (vars, theta_ev_vars, strict_arg_tys, ex_tvs') + +equateTyVars :: [TyVar] -> [TyVar] -> DsM [EvVar] +equateTyVars ex_tvs1 ex_tvs2 + = ASSERT(ex_tvs1 `equalLength` ex_tvs2) + catMaybes <$> zipWithM mb_to_evvar ex_tvs1 ex_tvs2 + where + mb_to_evvar tv1 tv2 + | tv1 == tv2 = pure Nothing + | otherwise = Just <$> to_evvar tv1 tv2 + to_evvar tv1 tv2 = nameType "pmConCon" $ + mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2) + +------------------------- +-- * Pattern match oracle + + +-- | Term and type constraints to accompany each value vector abstraction. +-- For efficiency, we store the term oracle state instead of the term +-- constraints. +data Delta = MkDelta { delta_ty_cs :: Bag EvVar -- Type oracle; things like a~Int + , delta_tm_cs :: TmState } -- Term oracle; things like x~Nothing + +-- | An initial delta that is always satisfiable +initDelta :: Delta +initDelta = MkDelta emptyBag initTmState + +instance Outputable Delta where + ppr delta = vcat [ + -- intentionally formatted this way enable the dev to comment in only + -- the info she needs + ppr (delta_tm_cs delta), + ppr (pprEvVarWithType <$> delta_ty_cs delta) + --ppr (delta_ty_cs delta) + ] + + +{- 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. +-} + +------------------------------------- +-- * Composable satisfiability checks + +-- | Given a 'Delta', check if it is compatible with new facts encoded in this +-- this check. If so, return 'Just' a potentially extended 'Delta'. Return +-- 'Nothing' if unsatisfiable. +-- +-- There are three essential SatisfiabilityChecks: +-- 1. 'tmIsSatisfiable', adding term oracle facts +-- 2. 'tyIsSatisfiable', adding type oracle facts +-- 3. 'tysAreNonVoid', checks if the given types have an inhabitant +-- Functions like 'pmIsSatisfiable', 'nonVoid' and 'testInhabited' plug these +-- together as they see fit. +newtype SatisfiabilityCheck = SC (Delta -> DsM (Maybe Delta)) + +-- | Check the given 'Delta' for satisfiability by the the given +-- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Delta' if +-- successful, and 'Nothing' otherwise. +runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta) +runSatisfiabilityCheck delta (SC chk) = chk delta + +-- | Allowing easy composition of 'SatisfiabilityCheck's. +instance Semigroup SatisfiabilityCheck where + -- This is @a >=> b@ from MaybeT DsM + SC a <> SC b = SC c + where + c delta = a delta >>= \case + Nothing -> pure Nothing + Just delta' -> b delta' + +instance Monoid SatisfiabilityCheck where + -- We only need this because of mconcat (which we use in place of sconcat, + -- which requires NonEmpty lists as argument, making all call sites ugly) + mempty = SC (pure . Just) + +------------------------------- +-- * Oracle transition function + +-- | 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.) +-- +-- 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 [Strict argument type constraints]@. +pmIsSatisfiable + :: Delta -- ^ The ambient term and type constraints + -- (known to be satisfiable). + -> Bag TmCt -- ^ The new term constraints. + -> Bag EvVar -- ^ The new type constraints. + -> [Type] -- ^ The strict argument types. + -> DsM (Maybe Delta) + -- ^ @'Just' delta@ if the constraints (@delta@) are + -- satisfiable, and each strict argument type is inhabitable. + -- 'Nothing' otherwise. +pmIsSatisfiable amb_cs new_tm_cs new_ty_cs strict_arg_tys = + -- The order is important here! Check the new type constraints before we check + -- whether strict argument types are inhabited given those constraints. + runSatisfiabilityCheck amb_cs $ mconcat + [ tyIsSatisfiable True new_ty_cs + , tmIsSatisfiable new_tm_cs + , tysAreNonVoid initRecTc strict_arg_tys + ] + +----------------------- +-- * Type normalisation + +-- | The return value of 'pmTopNormaliseType' +data TopNormaliseTypeResult + = NoChange Type + -- ^ 'tcNormalise' failed to simplify the type and 'topNormaliseTypeX' was + -- unable to reduce the outermost type application, so the type came out + -- unchanged. + | NormalisedByConstraints Type + -- ^ 'tcNormalise' was able to simplify the type with some local constraint + -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type + -- redex. + | HadRedexes Type [(Type, DataCon)] Type + -- ^ 'tcNormalise' may or may not been able to simplify the type, but + -- 'topNormaliseTypeX' made progress either way and got rid of at least one + -- outermost type or data family redex or newtype. + -- The first field is the last type that was reduced solely through type + -- family applications (possibly just the 'tcNormalise'd type). This is the + -- one that is equal (in source Haskell) to the initial type. + -- The third field is the type that we get when also looking through data + -- family applications and newtypes. This would be the representation type in + -- Core (modulo casts). + -- The second field is the list of Newtype 'DataCon's that we looked through + -- in the chain of reduction steps between the Source type and the Core type. + -- We also keep the type of the DataCon application, so that we don't have to + -- reconstruct it in inhabitationCandidates.build_newtype. + +-- | Just give me the potentially normalised source type, unchanged or not! +normalisedSourceType :: TopNormaliseTypeResult -> Type +normalisedSourceType (NoChange ty) = ty +normalisedSourceType (NormalisedByConstraints ty) = ty +normalisedSourceType (HadRedexes ty _ _) = ty + +instance Outputable TopNormaliseTypeResult where + ppr (NoChange ty) = text "NoChange" <+> ppr ty + ppr (NormalisedByConstraints ty) = text "NormalisedByConstraints" <+> ppr ty + ppr (HadRedexes src_ty ds core_ty) = text "HadRedexes" <+> braces fields + where + fields = fsep (punctuate comma [ text "src_ty =" <+> ppr src_ty + , text "newtype_dcs =" <+> ppr ds + , text "core_ty =" <+> ppr core_ty ]) + +pmTopNormaliseType :: Bag EvVar -> Type -> DsM TopNormaliseTypeResult +-- ^ Get rid of *outermost* (or toplevel) +-- * type function redex +-- * data family redex +-- * newtypes +-- +-- Behaves 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. +-- It also initially 'tcNormalise's the type with the bag of local constraints. +-- +-- See 'TopNormaliseTypeResult' for the meaning of the return value. +-- +-- 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 ty_cs typ + = do env <- dsGetFamInstEnvs + -- 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]. + (_, mb_typ') <- initTcDsForSolver $ tcNormalise ty_cs typ + -- If tcNormalise didn't manage to simplify the type, continue anyway. + -- We might be able to reduce type applications nonetheless! + let typ' = fromMaybe typ mb_typ' + -- Now we look with topNormaliseTypeX through type and data family + -- applications and newtypes, which tcNormalise does not do. + -- See also 'TopNormaliseTypeResult'. + pure $ case topNormaliseTypeX (stepper env) comb typ' of + Nothing + | Nothing <- mb_typ' -> NoChange typ + | otherwise -> NormalisedByConstraints typ' + Just ((ty_f,tm_f), ty) -> HadRedexes src_ty newtype_dcs core_ty + where + src_ty = eq_src_ty ty (typ' : ty_f [ty]) + newtype_dcs = tm_f [] + core_ty = 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 env = newTypeStepper `composeSteppers` tyFamStepper env + + -- 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],[(Type, DataCon)] -> [(Type, DataCon)]) + newTypeStepper rec_nts tc tys + | Just (ty', _co) <- instNewTyCon_maybe tc tys + , let orig_ty = TyConApp tc tys + = case checkRecTc rec_nts tc of + Just rec_nts' -> let tyf = (orig_ty:) + tmf = ((orig_ty, tyConSingleDataCon tc):) + in NS_Step rec_nts' ty' (tyf, tmf) + Nothing -> NS_Abort + | otherwise + = NS_Done + + tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a) + tyFamStepper env 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 + +-- | 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 + +{- 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 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 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 newtype constructors "skipped", every time we normalise + a newtype to its core representation, we keep track of the source data + constructor and the type we unwrap. + (c) core_ty is the rewritten type. That is, + pmTopNormaliseType 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 env ty_cs (F Int) results in + + Just (G2, [(G2,MkG2),(G1,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, using the constraint solver to solve for any local +equalities (such as i ~ Int) that may be in scope. +-} + +---------------- +-- * Type oracle + +-- | Check whether a set of type constraints is satisfiable. +tyOracle :: Bag EvVar -> DsM Bool +tyOracle evs + = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs + ; case res of + Just sat -> return sat + Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) } + +-- | A 'SatisfiabilityCheck' based on new type-level constraints. +-- Returns a new 'Delta' if the new constraints are compatible with existing +-- ones. Doesn't bother calling out to the type oracle if the bag of new type +-- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle +-- for emptiness if the first argument is 'True'. +tyIsSatisfiable :: Bool -> Bag EvVar -> SatisfiabilityCheck +tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> do + tracePm "tyIsSatisfiable" (ppr (fmap pprEvVarWithType new_ty_cs)) + let ty_cs = new_ty_cs `unionBags` delta_ty_cs delta + let delta' = delta{ delta_ty_cs = ty_cs } + if isEmptyBag new_ty_cs + then pure (Just delta) + else tyOracle ty_cs >>= \case + False -> pure Nothing + True + | recheck_complete_sets -> ensureAllPossibleMatchesInhabited delta' + | otherwise -> pure (Just delta') + + +{- ********************************************************************* +* * + SharedIdEnv + DIdEnv with sharing +* * +********************************************************************* -} + +-- | Either @Indirect x@, meaning the value is represented by that of @x@, or +-- an @Entry@ containing containing the actual value it represents. +data Shared a + = Indirect Id + | Entry a + +-- | A 'DIdEnv' in which entries can be shared by multiple 'Id's. +-- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry +-- of an Id with 'setEntrySDIE'. +newtype SharedDIdEnv a + = SDIE { unSDIE :: DIdEnv (Shared a) } + +emptySDIE :: SharedDIdEnv a +emptySDIE = SDIE emptyDVarEnv + +lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a) +lookupReprAndEntrySDIE sdie@(SDIE env) x = case lookupDVarEnv env x of + Nothing -> (x, Nothing) + Just (Indirect y) -> lookupReprAndEntrySDIE sdie y + Just (Entry a) -> (x, Just a) + +-- | @lookupSDIE env x@ looks up an entry for @x@, looking through all +-- 'Indirect's until it finds a shared 'Entry'. +lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a +lookupSDIE sdie x = snd (lookupReprAndEntrySDIE sdie x) + +-- | Check if two variables are part of the same equivalence class. +sameRepresentative :: SharedDIdEnv a -> Id -> Id -> Bool +sameRepresentative sdie x y = + fst (lookupReprAndEntrySDIE sdie x) == fst (lookupReprAndEntrySDIE sdie y) + +-- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby +-- merging @x@'s equivalence class into @y@'s. This will discard all info on +-- @x@! +setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a +setIndirectSDIE sdie@(SDIE env) x y = + SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Indirect y) + +-- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@, +-- thereby modifying its whole equivalence class. +setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a +setEntrySDIE sdie@(SDIE env) x a = + SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a) + +traverseSharedIdEnv :: Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b) +traverseSharedIdEnv f = fmap (SDIE . listToUDFM) . traverse g . udfmToList . unSDIE + where + g (u, Indirect y) = pure (u,Indirect y) + g (u, Entry a) = (u,) . Entry <$> f a + +instance Outputable a => Outputable (Shared a) where + ppr (Indirect x) = ppr x + ppr (Entry a) = ppr a + +instance Outputable a => Outputable (SharedDIdEnv a) where + ppr (SDIE env) = ppr env + + +{- ********************************************************************* +* * + TmState + What we know about terms +* * +********************************************************************* -} + +-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These +-- entries are possibly shared when we figure out that two variables must be +-- equal, thus represent the same set of values. +-- +-- See Note [TmState invariants]. +newtype TmState = TS (SharedDIdEnv VarInfo) + -- Deterministic so that we generate deterministic error messages + +-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@, +-- and negative ('vi_neg') facts, like "x is not (:)". +-- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set +-- ('vi_cache') and the number of times each variable was refined +-- ('vi_n_refines'). +-- +-- Subject to Note [The Pos/Neg invariant]. +data VarInfo + = VI + { vi_ty :: !Type + -- ^ The type of the variable. Important for rejecting possible GADT + -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@). + + , vi_pos :: [(PmAltCon, [Id])] + -- ^ Positive info: 'PmExprCon's it is (i.e. @x ~ [Just y, PatSyn z]@), all + -- at the same time (i.e. conjunctive). We need a list because of nested + -- pattern matches involving pattern synonym + -- case x of { Just y -> case x of PatSyn z -> ... } + -- However, no more than one RealDataCon in the list, otherwise contradiction + -- because of generativity. + + , vi_neg :: ![PmAltCon] + -- ^ Negative info: A list of 'PmAltCon's that it cannot match. + -- Example, assuming + -- + -- @ + -- data T = Leaf Int | Branch T T | Node Int T + -- @ + -- + -- then @x /~ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@, + -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos', + -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing + -- between 'vi_pos' and 'vi_neg'. + + -- See Note [Why record both positive and negative info?] + + , vi_cache :: !PossibleMatches + -- ^ A cache of the associated COMPLETE sets. At any time a superset of + -- possible constructors of each COMPLETE set. So, if it's not in here, we + -- can't possibly match on it. Complementary to 'vi_neg'. We still need it + -- to recognise completion of a COMPLETE set efficiently for large enums. + + , vi_n_refines :: !Int + -- ^ Purely for Check performance reasons. The number of times this + -- representative was refined ('refineToAltCon') in the Check's ConVar split. + -- Sadly, we can't store this info in the Check module, as it's tightly coupled + -- to the particular 'Delta' and also is per *representative*, not per + -- syntactic variable. Note that this number does not always correspond to the + -- length of solutions: 'addVarConCt' might add a solution without + -- incurring the potential exponential blowup by ConVar. + } + +{- Note [The Pos/Neg invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos', +any entry in 'vi_neg' must be incomparable to C (return Nothing) according to +'eqPmAltCons'. Those entries that are comparable either lead to a refutation +or are redudant. Examples: +* @x ~ Just y@, @x /~ [Just]@. 'eqPmAltCon' returns @Equal@, so refute. +* @x ~ Nothing@, @x /~ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative + info is redundant and should be discarded. +* @x ~ I# y@, @x /~ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal. + We keep this info in order to be able to refute a redundant match on i.e. 4 + later on. + +This carries over to pattern synonyms and overloaded literals. Say, we have + pattern Just42 = Just 42 + case Just42 of x + Nothing -> () + Just _ -> () +Even though we had a solution for the value abstraction called x here in form +of a PatSynCon (Just42,[]), this solution is incomparable to both Nothing and +Just. Hence we retain the info in vi_neg, which eventually allows us to detect +the complete pattern match. + +The Pos/Neg invariant extends to vi_cache, which stores essentially positive +information. We make sure that vi_neg and vi_cache never overlap. This isn't +strictly necessary since vi_cache is just a cache, so doesn't need to be +accurate: Every suggestion of a possible ConLike from vi_cache might be +refutable by the type oracle anyway. But it helps to maintain sanity while +debugging traces. + +Note [Why record both positive and negative info?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +You might think that knowing positive info (like x ~ Just y) would render +negative info irrelevant, but not so because of pattern synonyms. E.g we might +know that x cannot match (Foo 4), where pattern Foo p = Just p + +Also overloaded literals themselves behave like pattern synonyms. E.g if +postively we know that (x ~ I# y), we might also negatively want to record that +x does not match 45 f 45 = e2 f (I# 22#) = e3 f 45 = e4 -- +Overlapped + +Note [TmState invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~ +The term oracle state is never obviously (i.e., without consulting the type +oracle) contradictory. This implies a few invariants: +* Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute. + This is implied by the Note [Pos/Neg invariant]. +* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_cache to + detect this, but we could just compare whole COMPLETE sets to vi_neg every + time, if it weren't for performance. + +Maintaining these invariants in 'addVarVarCt' (the core of the term oracle) and +'addRefutableAltCon' is subtle. +* Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate'). + - (COMPLETE) If we had @x /~ True@ and @y /~ False@, then we get + @x /~ [True,False]@. This is vacuous by matter of comparing to the vanilla + COMPLETE set, so should refute. + - (Pos/Neg) If we had @x /~ True@ and @y ~ True@, we have to refute. +* Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addVarConCt') + - (Neg) If we had @x /~ K@, refute. + - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to + 'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute. + - (Refine) If we had @x /~ K zs@, unify each y with each z in turn. +* Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addRefutableAltCon') + - (Refut) If we have @x ~ K ys@, refute. + - (Redundant) If we have @x ~ K2@ and @eqPmAltCon K K2 == Disjoint@ + (ex. Just and Nothing), the info is redundant and can be + discarded. + - (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get + @x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the vanilla + COMPLETE set, so should refute. + +Note that merging VarInfo in equate can be done by calling out to 'addVarConCt' and +'addRefutableAltCon' for each of the facts individually. + +Note [Representation of Strings in TmState] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Instead of treating regular String literals as a PmLits, we treat it as a list +of characters in the oracle for better overlap reasoning. The following example +shows why: + + f :: String -> () + f ('f':_) = () + f "foo" = () + f _ = () + +The second case is redundant, and we like to warn about it. Therefore either +the oracle will have to do some smart conversion between the list and literal +representation or treat is as the list it really is at runtime. + +The "smart conversion" has the advantage of leveraging the more compact literal +representation wherever possible, but is really nasty to get right with negative +equalities: Just think of how to encode @x /= "foo"@. +The "list" option is far simpler, but incurs some overhead in representation and +warning messages (which can be alleviated by someone with enough dedication). +-} + +-- | Not user-facing. +instance Outputable TmState where + ppr (TS state) = ppr state + +-- | Not user-facing. +instance Outputable VarInfo where + ppr (VI ty pos neg cache n) + = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache, ppr n])) + +-- | Initial state of the oracle. +initTmState :: TmState +initTmState = TS emptySDIE + +-- | A 'SatisfiabilityCheck' based on new term-level constraints. +-- Returns a new 'Delta' if the new constraints are compatible with existing +-- ones. +tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck +tmIsSatisfiable new_tm_cs = SC $ \delta -> tmOracle delta new_tm_cs + +-- | External interface to the term oracle. +tmOracle :: Foldable f => Delta -> f TmCt -> DsM (Maybe Delta) +tmOracle delta = runMaybeT . foldlM go delta + where + go delta ct = MaybeT (addTmCt delta ct) + +----------------------- +-- * Looking up VarInfo + +emptyVarInfo :: Id -> VarInfo +emptyVarInfo x = VI (idType x) [] [] NoPM 0 + +lookupVarInfo :: TmState -> Id -> VarInfo +-- (lookupVarInfo tms x) tells what we know about 'x' +lookupVarInfo (TS env) x = fromMaybe (emptyVarInfo x) (lookupSDIE env x) + +initPossibleMatches :: Bag EvVar -> VarInfo -> DsM VarInfo +initPossibleMatches ty_cs vi@VI{ vi_ty = ty, vi_cache = NoPM } = do + -- New evidence might lead to refined info on ty, in turn leading to discovery + -- of a COMPLETE set. + res <- pmTopNormaliseType ty_cs ty + let ty' = normalisedSourceType res + mb_pm <- initIM ty' + -- tracePm "initPossibleMatches" (ppr vi $$ ppr ty' $$ ppr res $$ ppr mb_pm) + case mb_pm of + Nothing -> pure vi + Just pm -> pure vi{ vi_ty = ty', vi_cache = pm } +initPossibleMatches _ vi = pure vi + +-- | @initLookupVarInfo ts x@ looks up the 'VarInfo' for @x@ in @ts@ and tries +-- to initialise the 'vi_cache' component if it was 'NoPM' through +-- 'initPossibleMatches'. +initLookupVarInfo :: Delta -> Id -> DsM VarInfo +initLookupVarInfo MkDelta{ delta_tm_cs = ts, delta_ty_cs = ty_cs } x + = initPossibleMatches ty_cs (lookupVarInfo ts x) + +------------------------------------------------ +-- * Exported utility functions querying 'Delta' + +-- | Check whether a constraint (x ~ BOT) can succeed, +-- given the resulting state of the term oracle. +canDiverge :: Delta -> Id -> Bool +canDiverge MkDelta{ delta_tm_cs = ts } x + -- If the variable seems not evaluated, there is a possibility for + -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found + -- a solution (i.e. some equivalent literal or constructor) for it yet. + -- Even if we don't have a solution yet, it might be involved in a negative + -- constraint, in which case we must already have evaluated it earlier. + | VI _ [] [] _ _ <- lookupVarInfo ts x + = True + -- Variable x is already in WHNF or we know some refutable shape, so the + -- constraint is non-satisfiable + | otherwise = False + +lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon] +-- Unfortunately we need the extra bit of polymorphism and the unfortunate +-- duplication of lookupVarInfo here. +lookupRefuts MkDelta{ delta_tm_cs = ts@(TS (SDIE env)) } k = + case lookupUDFM env k of + Nothing -> [] + Just (Indirect y) -> vi_neg (lookupVarInfo ts y) + Just (Entry vi) -> vi_neg vi + +isDataConSolution :: (PmAltCon, [Id]) -> Bool +isDataConSolution (PmAltConLike (RealDataCon _), _) = True +isDataConSolution _ = False + +-- @lookupSolution delta x@ picks a single solution ('vi_pos') of @x@ from +-- possibly many, preferring 'RealDataCon' solutions whenever possible. +lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id]) +lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_cs delta) x) of + [] -> Nothing + pos + | Just sol <- find isDataConSolution pos -> Just sol + | otherwise -> Just (head pos) + +-- | @lookupNumberOfRefinements delta x@ Looks up how many times we have refined +-- ('refineToAltCon') @x@ for some 'PmAltCon' to arrive at @delta@. This number +-- is always less or equal to @length (lookupSolution delta x)@! +lookupNumberOfRefinements :: Delta -> Id -> Int +lookupNumberOfRefinements delta x + = vi_n_refines (lookupVarInfo (delta_tm_cs delta) x) + +------------------------------- +-- * Adding facts to the oracle + +-- | A term constraint. Either equates two variables or a variable with a +-- 'PmAltCon' application. +data TmCt + = TmVarVar !Id !Id + | TmVarCon !Id !PmAltCon ![Id] + +instance Outputable TmCt where + ppr (TmVarVar x y) = ppr x <+> char '~' <+> ppr y + ppr (TmVarCon x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args) + +-- | Add type equalities to 'Delta'. +addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta) +addTypeEvidence delta dicts + = runSatisfiabilityCheck delta (tyIsSatisfiable True dicts) + +-- | Tries to equate two representatives in 'Delta'. +-- See Note [TmState invariants]. +addTmCt :: Delta -> TmCt -> DsM (Maybe Delta) +addTmCt delta ct = runMaybeT $ case ct of + TmVarVar x y -> addVarVarCt delta (x, y) + TmVarCon x con args -> addVarConCt delta x con args + +-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the +-- 'Delta' and return @Nothing@ if that leads to a contradiction. +-- See Note [TmState invariants]. +addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta) +addRefutableAltCon delta@MkDelta{ delta_tm_cs = TS env } x nalt = runMaybeT $ do + vi@(VI _ pos neg pm _) <- lift (initLookupVarInfo delta x) + -- 1. Bail out quickly when nalt contradicts a solution + let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal + guard (not (any (contradicts nalt) pos)) + -- 2. Only record the new fact when it's not already implied by one of the + -- solutions + let implies nalt (cl, _args) = eqPmAltCon cl nalt == Disjoint + let neg' + | any (implies nalt) pos = neg + -- See Note [Completeness checking with required Thetas] + | hasRequiredTheta nalt = neg + | otherwise = unionLists neg [nalt] + let vi_ext = vi{ vi_neg = neg' } + -- 3. Make sure there's at least one other possible constructor + vi' <- case nalt of + PmAltConLike cl + -> MaybeT (ensureInhabited delta vi_ext{ vi_cache = markMatched cl pm }) + _ -> pure vi_ext + pure delta{ delta_tm_cs = TS (setEntrySDIE env x vi') } + +hasRequiredTheta :: PmAltCon -> Bool +hasRequiredTheta (PmAltConLike cl) = notNull req_theta + where + (_,_,_,_,req_theta,_,_) = conLikeFullSig cl +hasRequiredTheta _ = False + +{- Note [Completeness checking with required Thetas] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the situation in #11224 + + import Text.Read (readMaybe) + pattern PRead :: Read a => () => a -> String + pattern PRead x <- (readMaybe -> Just x) + f :: String -> Int + f (PRead x) = x + f (PRead xs) = length xs + f _ = 0 + +Is the first match exhaustive on the PRead synonym? Should the second line thus +deemed redundant? The answer is, of course, No! The required theta is like a +hidden parameter which must be supplied at the pattern match site, so PRead +is much more like a view pattern (where behavior depends on the particular value +passed in). +The simple solution here is to forget in 'addRefutableAltCon' that we matched +on synonyms with a required Theta like @PRead@, so that subsequent matches on +the same constructor are never flagged as redundant. The consequence is that +we no longer detect the actually redundant match in + + g :: String -> Int + g (PRead x) = x + g (PRead y) = y -- redundant! + g _ = 0 + +But that's a small price to pay, compared to the proper solution here involving +storing required arguments along with the PmAltConLike in 'vi_neg'. +-} + +-- | Guess the universal argument types of a ConLike from an instantiation of +-- its result type. Rather easy for DataCons, but not so much for PatSynCons. +-- See Note [Pattern synonym result type] in PatSyn.hs. +guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type] +guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon _) = do + (tc, tc_args) <- splitTyConApp_maybe res_ty + -- Consider data families: In case of a DataCon, we need to translate to + -- the representation TyCon. For PatSyns, they are relative to the data + -- family TyCon, so we don't need to translate them. + let (_, tc_args', _) = tcLookupDataFamInst env tc tc_args + Just tc_args' +guessConLikeUnivTyArgsFromResTy _ res_ty (PatSynCon ps) = do + -- We were successful if we managed to instantiate *every* univ_tv of con. + -- This is difficult and bound to fail in some cases, see + -- Note [Pattern synonym result type] in PatSyn.hs. So we just try our best + -- here and be sure to return an instantiation when we can substitute every + -- universally quantified type variable. + -- We *could* instantiate all the other univ_tvs just to fresh variables, I + -- suppose, but that means we get weird field types for which we don't know + -- anything. So we prefer to keep it simple here. + let (univ_tvs,_,_,_,_,con_res_ty) = patSynSig ps + subst <- tcMatchTy con_res_ty res_ty + traverse (lookupTyVar subst) univ_tvs + +ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo) + -- Returns (Just vi) guarantees that at least one member + -- of each ConLike in the COMPLETE set satisfies the oracle + -- + -- Internally uses and updates the ConLikeSets in vi_cache. + -- + -- NB: Does /not/ filter each ConLikeSet with the oracle; members may + -- remain that do not statisfy it. This lazy approach just + -- avoids doing unnecessary work. +ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This would be much less tedious with lenses + where + set_cache vi cache = vi { vi_cache = cache } + + test NoPM = pure (Just NoPM) + test (PM tc ms) = runMaybeT (PM tc <$> traverse one_set ms) + + one_set cs = find_one_inh cs (uniqDSetToList cs) + + find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet + -- (find_one_inh cs cls) iterates over cls, deleting from cs + -- any uninhabited elements of cls. Stop (returning Just cs) + -- when you see an inhabited element; return Nothing if all + -- are uninhabited + find_one_inh _ [] = mzero + find_one_inh cs (con:cons) = lift (inh_test con) >>= \case + True -> pure cs + False -> find_one_inh (delOneFromUniqDSet cs con) cons + + inh_test :: ConLike -> DsM Bool + -- @inh_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly + -- be of form @K _ _ _@. Returning True is always sound. + -- + -- It's like 'DataCon.dataConCannotMatch', but more clever because it takes + -- the facts in Delta into account. + inh_test con = do + env <- dsGetFamInstEnvs + case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of + Nothing -> pure True -- be conservative about this + Just arg_tys -> do + (_vars, ev_vars, strict_arg_tys, _ex_tyvars) <- mkOneConFull arg_tys con + -- No need to run the term oracle compared to pmIsSatisfiable + fmap isJust <$> runSatisfiabilityCheck delta $ mconcat + -- Important to pass False to tyIsSatisfiable here, so that we won't + -- recursively call ensureAllPossibleMatchesInhabited, leading to an + -- endless recursion. + [ tyIsSatisfiable False (listToBag ev_vars) + , tysAreNonVoid initRecTc strict_arg_tys + ] + +-- | Checks if every 'VarInfo' in the term oracle has still an inhabited +-- 'vi_cache', considering the current type information in 'Delta'. +-- This check is necessary after having matched on a GADT con to weed out +-- impossible matches. +ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta) +ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_cs = TS env } + = runMaybeT (set_tm_cs_env delta <$> traverseSharedIdEnv go env) + where + set_tm_cs_env delta env = delta{ delta_tm_cs = TS env } + go vi = MaybeT (ensureInhabited delta vi) + +-- | @refineToAltCon delta x con arg_tys ex_tyvars@ instantiates @con@ at +-- @arg_tys@ with fresh variables (equating existentials to @ex_tyvars@). +-- It adds a new term equality equating @x@ is to the resulting 'PmExprCon' and +-- new type equalities arising from GADT matches. +-- If successful, returns the new @delta@ and the fresh term variables, or +-- @Nothing@ otherwise. +refineToAltCon :: Delta -> Id -> PmAltCon -> [Type] -> [TyVar] -> DsM (Maybe (Delta, [Id])) +refineToAltCon delta x l@PmAltLit{} _arg_tys _ex_tvs1 = runMaybeT $ do + delta' <- addVarConCt delta x l [] + pure (markRefined delta' x, []) +refineToAltCon delta x alt@(PmAltConLike con) arg_tys ex_tvs1 = do + -- The plan for ConLikes: + -- Suppose K :: forall a b y z. (y,b) -> z -> T a b + -- where the y,z are the existentials + -- @refineToAltCon delta x K [ex1, ex2]@ extends delta with the + -- positive information x :-> K y' z' p q, for some fresh y', z', p, q. + -- This is done by mkOneConFull. + -- We return the fresh [p,q] args, and bind the existentials [y',z'] to + -- [ex1, ex2]. + -- Return Nothing if such a match is contradictory with delta. + + (arg_vars, theta_ev_vars, strict_arg_tys, ex_tvs2) <- mkOneConFull arg_tys con + + -- 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]. + ex_ev_vars <- equateTyVars ex_tvs1 ex_tvs2 + + let new_ty_cs = listToBag theta_ev_vars `unionBags` listToBag ex_ev_vars + let new_tm_cs = unitBag (TmVarCon x alt arg_vars) + + -- Now check satifiability + mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys + tracePm "refineToAltCon" (vcat [ ppr x + , ppr new_tm_cs + , ppr new_ty_cs + , ppr strict_arg_tys + , ppr delta + , ppr mb_delta ]) + case mb_delta of + Nothing -> pure Nothing + Just delta' -> pure (Just (markRefined delta' x, arg_vars)) + +-- | This is the only place that actualy increments 'vi_n_refines'. +markRefined :: Delta -> Id -> Delta +markRefined delta@MkDelta{ delta_tm_cs = ts@(TS env) } x + = delta{ delta_tm_cs = TS env' } + where + vi = lookupVarInfo ts x + env' = setEntrySDIE env x vi{ vi_n_refines = vi_n_refines vi + 1 } + +{- +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! +-} + +-------------------------------------- +-- * Term oracle unification procedure + +-- | Try to unify two 'Id's and record the gained knowledge in 'Delta'. +-- +-- Returns @Nothing@ when there's a contradiction. Returns @Just delta@ +-- when the constraint was compatible with prior facts, in which case @delta@ +-- has integrated the knowledge from the equality constraint. +-- +-- See Note [TmState invariants]. +addVarVarCt :: Delta -> (Id, Id) -> MaybeT DsM Delta +addVarVarCt delta@MkDelta{ delta_tm_cs = TS env } (x, y) + -- It's important that we never @equate@ two variables of the same equivalence + -- class, otherwise we might get cyclic substitutions. + -- Cf. 'extendSubstAndSolve' and + -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@. + | sameRepresentative env x y = pure delta + | otherwise = equate delta x y + +-- | @equate ts@(TS env) x y@ merges the equivalence classes of @x@ and @y@ by +-- adding an indirection to the environment. +-- Makes sure that the positive and negative facts of @x@ and @y@ are +-- compatible. +-- Preconditions: @not (sameRepresentative env x y)@ +-- +-- See Note [TmState invariants]. +equate :: Delta -> Id -> Id -> MaybeT DsM Delta +equate delta@MkDelta{ delta_tm_cs = TS env } x y + = ASSERT( not (sameRepresentative env x y) ) + case (lookupSDIE env x, lookupSDIE env y) of + (Nothing, _) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env x y) }) + (_, Nothing) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env y x) }) + -- Merge the info we have for x into the info for y + (Just vi_x, Just vi_y) -> do + -- This assert will probably trigger at some point... + -- We should decide how to break the tie + MASSERT2( vi_ty vi_x `eqType` vi_ty vi_y, text "Not same type" ) + -- First assume that x and y are in the same equivalence class + let env_ind = setIndirectSDIE env x y + -- Then sum up the refinement counters + let vi_y' = vi_y{ vi_n_refines = vi_n_refines vi_x + vi_n_refines vi_y } + let env_refs = setEntrySDIE env_ind y vi_y' + let delta_refs = delta{ delta_tm_cs = TS env_refs } + -- and then gradually merge every positive fact we have on x into y + let add_fact delta (cl, args) = addVarConCt delta y cl args + delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x) + -- Do the same for negative info + let add_refut delta nalt = MaybeT (addRefutableAltCon delta y nalt) + delta_neg <- foldlM add_refut delta_pos (vi_neg vi_x) + -- vi_cache will be updated in addRefutableAltCon, so we are good to + -- go! + pure delta_neg + +-- | @addVarConCt x alt args ts@ extends the substitution with a mapping @x: -> +-- PmExprCon alt args@ if compatible with refutable shapes of @x@ and its +-- solution, reject (@Nothing@) otherwise. +-- +-- See Note [TmState invariants]. +addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta +addVarConCt delta@MkDelta{ delta_tm_cs = TS env } x alt args = do + VI ty pos neg cache n <- lift (initLookupVarInfo delta x) + -- First try to refute with a negative fact + guard (all ((/= Equal) . eqPmAltCon alt) neg) + -- Then see if any of the other solutions (remember: each of them is an + -- additional refinement of the possible values x could take) indicate a + -- contradiction + guard (all ((/= Disjoint) . eqPmAltCon alt . fst) pos) + -- Now we should be good! Add (alt, args) as a possible solution, or refine an + -- existing one + case find ((== Equal) . eqPmAltCon alt . fst) pos of + Just (_, other_args) -> do + foldlM addVarVarCt delta (zip args other_args) + Nothing -> do + -- Filter out redundant negative facts (those that compare Just False to + -- the new solution) + let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg + let pos' = (alt,args):pos + pure delta{ delta_tm_cs = TS (setEntrySDIE env x (VI ty pos' neg' cache n))} + +---------------------------------------- +-- * Enumerating inhabitation candidates + +-- | 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 constraints ('ic_tm_cs') +-- and type constraints ('ic_ty_cs') are permitting, and if all of its strict +-- argument types ('ic_strict_arg_tys') are inhabitable. +-- See @Note [Strict argument type constraints]@. +data InhabitationCandidate = + InhabitationCandidate + { ic_tm_cs :: Bag TmCt + , ic_ty_cs :: Bag EvVar + , ic_strict_arg_tys :: [Type] + } + +instance Outputable InhabitationCandidate where + ppr (InhabitationCandidate tm_cs ty_cs strict_arg_tys) = + text "InhabitationCandidate" <+> + vcat [ text "ic_tm_cs =" <+> ppr tm_cs + , text "ic_ty_cs =" <+> ppr ty_cs + , text "ic_strict_arg_tys =" <+> ppr strict_arg_tys ] + +mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate +-- Precondition: idType x is a TyConApp, so that tyConAppArgs in here is safe. +mkInhabitationCandidate x dc = do + let cl = RealDataCon dc + let tc_args = tyConAppArgs (idType x) + (arg_vars, ev_vars, strict_arg_tys, _ex_tyvars) <- mkOneConFull tc_args cl + pure InhabitationCandidate + { ic_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars) + , ic_ty_cs = listToBag ev_vars + , ic_strict_arg_tys = strict_arg_tys + } + +-- | 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 :: Delta -> Type + -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) +inhabitationCandidates MkDelta{ delta_ty_cs = ty_cs } ty = do + pmTopNormaliseType ty_cs ty >>= \case + NoChange _ -> alts_to_check ty ty [] + NormalisedByConstraints ty' -> alts_to_check ty' ty' [] + HadRedexes src_ty dcs core_ty -> alts_to_check src_ty core_ty dcs + where + -- All these types are trivially inhabited + trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon + , intTyCon, wordTyCon, word8TyCon ] + + build_newtype :: (Type, DataCon) -> Id -> DsM (Id, TmCt) + build_newtype (ty, dc) x = do + -- ty is the type of @dc x@. It's a @dataConTyCon dc@ application. + y <- mkPmId ty + pure (y, TmVarCon y (PmAltConLike (RealDataCon dc)) [x]) + + build_newtypes :: Id -> [(Type, DataCon)] -> DsM (Id, [TmCt]) + build_newtypes x = foldrM (\dc (x, cts) -> go dc x cts) (x, []) + where + go dc x cts = second (:cts) <$> build_newtype dc x + + -- Inhabitation candidates, using the result of pmTopNormaliseType + alts_to_check :: Type -> Type -> [(Type, DataCon)] + -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) + alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of + Just (tc, _) + | tc `elem` trivially_inhabited + -> case dcs of + [] -> return (Left src_ty) + (_:_) -> do inner <- mkPmId core_ty + (outer, new_tm_cts) <- build_newtypes inner dcs + return $ Right (tc, outer, [InhabitationCandidate + { ic_tm_cs = listToBag new_tm_cts + , 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. + -> do + inner <- mkPmId core_ty -- it would be wrong to unify inner + alts <- mapM (mkInhabitationCandidate inner) (tyConDataCons tc) + (outer, new_tm_cts) <- build_newtypes inner dcs + let wrap_dcs alt = alt{ ic_tm_cs = listToBag new_tm_cts `unionBags` ic_tm_cs alt} + return $ Right (tc, outer, map wrap_dcs alts) + -- For other types conservatively assume that they are inhabited. + _other -> return (Left src_ty) + +inhabitants :: Delta -> Type -> DsM (Either Type (Id, [Delta])) +inhabitants delta ty = inhabitationCandidates delta ty >>= \case + Left ty' -> pure (Left ty') + Right (_, va, candidates) -> do + deltas <- flip mapMaybeM candidates $ + \InhabitationCandidate{ ic_tm_cs = tm_cs + , ic_ty_cs = ty_cs + , ic_strict_arg_tys = strict_arg_tys } -> do + pmIsSatisfiable delta tm_cs ty_cs strict_arg_tys + pure (Right (va, deltas)) + +---------------------------- +-- * Detecting vacuous types + +{- 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 (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 Check.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 do for normal + pattern match checking. +-} + +-- | A 'SatisfiabilityCheck' based on "NonVoid ty" constraints, e.g. Will +-- check if the @strict_arg_tys@ are actually all inhabited. +-- Returns the old 'Delta' if all the types are non-void according to 'Delta'. +tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck +tysAreNonVoid rec_env strict_arg_tys = SC $ \delta -> do + all_non_void <- checkAllNonVoid rec_env delta strict_arg_tys + -- Check if each strict argument type is inhabitable + pure $ if all_non_void + then Just delta + else Nothing + +-- | Implements two performance optimizations, as described in +-- @Note [Strict argument type constraints]@. +checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool +checkAllNonVoid rec_ts amb_cs strict_arg_tys = do + let definitely_inhabited = definitelyInhabitedType (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 [Strict argument type constraints]@. +nonVoid + :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit. + -> Delta -- ^ The ambient term/type constraints (known to be + -- satisfiable). + -> Type -- ^ The strict argument type. + -> DsM 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 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 [Strict argument type constraints] + cand_is_inhabitable :: RecTcChecker -> Delta + -> InhabitationCandidate -> DsM Bool + cand_is_inhabitable rec_ts amb_cs + (InhabitationCandidate{ ic_tm_cs = new_tm_cs + , ic_ty_cs = new_ty_cs + , ic_strict_arg_tys = new_strict_arg_tys }) = + fmap isJust $ runSatisfiabilityCheck amb_cs $ mconcat + [ tyIsSatisfiable False new_ty_cs + , tmIsSatisfiable new_tm_cs + , tysAreNonVoid rec_ts 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 @Note [Strict argument type constraints]@. +definitelyInhabitedType :: Bag EvVar -> Type -> DsM Bool +definitelyInhabitedType ty_cs ty = do + res <- pmTopNormaliseType ty_cs ty + pure $ case res of + HadRedexes _ cons _ -> any meets_criteria cons + _ -> False + where + meets_criteria :: (Type, DataCon) -> Bool + meets_criteria (_, con) = + null (dataConEqSpec con) && -- (1) + null (dataConImplBangs con) -- (2) + +{- Note [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 check 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. +-} + +-------------------------------------------- +-- * Providing positive evidence for a Delta + +-- | @provideEvidenceForEquation vs n delta@ returns a list of +-- at most @n@ (but perhaps empty) refinements of @delta@ that instantiate +-- @vs@ to compatible constructor applications or wildcards. +-- Negative information is only retained if literals are involved or when +-- for recursive GADTs. +provideEvidenceForEquation :: [Id] -> Int -> Delta -> DsM [Delta] +provideEvidenceForEquation = go init_ts + where + -- Choosing 1 here will not be enough for RedBlack, but any other bound + -- might potentially lead to combinatorial explosion, so we are extremely + -- cautious and pick 2 here. + init_ts = setRecTcMaxBound 2 initRecTc + go _ _ 0 _ = pure [] + go _ [] _ delta = pure [delta] + go rec_ts (x:xs) n delta = do + VI ty pos neg pm _ <- initLookupVarInfo delta x + case pos of + _:_ -> do + -- All solutions must be valid at once. Try to find candidates for their + -- fields. Example: + -- f x@(Just _) True = case x of SomePatSyn _ -> () + -- after this clause, we want to report that + -- * @f Nothing _@ is uncovered + -- * @f x False@ is uncovered + -- where @x@ will have two possibly compatible solutions, @Just y@ for + -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@ + -- and @z@ that is valid at the same time. These constitute arg_vas below. + let arg_vas = concatMap (\(_cl, args) -> args) pos + go rec_ts (arg_vas ++ xs) n delta + [] + -- First the simple case where we don't need to query the oracles + | isVanillaDataType ty + -- So no type info unleashed in pattern match + , null neg + -- No term-level info either + || notNull [ l | PmAltLit l <- neg ] + -- ... or there are literals involved, in which case we don't want + -- to split on possible constructors + -> go rec_ts xs n delta + [] -> do + -- We have to pick one of the available constructors and try it + -- It's important that each of the ConLikeSets in pm is still inhabited, + -- so that it doesn't matter from which we pick. + -- I think we implicitly uphold that invariant, but not too sure + case getUnmatchedConstructor pm of + Unsatisfiable -> pure [] + -- No COMPLETE sets available, so we can assume it's inhabited + PossiblySatisfiable -> go rec_ts xs n delta + Satisfiable cl + | Just rec_ts' <- checkRecTc rec_ts (fst (splitTyConApp ty)) + -> split_at_con rec_ts' delta n x xs cl + | otherwise + -- We ran out of fuel; just conservatively assume that this is + -- inhabited. + -> go rec_ts xs n delta + + -- | @split_at_con _ delta _ x _ con@ splits the given delta into two + -- models: One where we assume x is con and one where we assume it can't be + -- con. Really similar to the ConVar case in Check, only that we don't + -- really have a pattern driving the split. + split_at_con + :: RecTcChecker -- ^ Detects when we split the same TyCon too often + -> Delta -- ^ The model we like to refine to the split + -> Int -- ^ The number of equations still to produce + -> Id -> [Id] -- ^ Head and tail of the value abstractions + -> ConLike -- ^ The ConLike over which to split + -> DsM [Delta] + split_at_con rec_ts delta n x xs cl = do + -- This will be really similar to the ConVar case + let (_,ex_tvs,_,_,_,_,_) = conLikeFullSig cl + -- we might need to freshen ex_tvs. Not sure + -- We may need to reduce type famlies/synonyms in x's type first + res <- pmTopNormaliseType (delta_ty_cs delta) (idType x) + let res_ty = normalisedSourceType res + env <- dsGetFamInstEnvs + case guessConLikeUnivTyArgsFromResTy env res_ty cl of + Nothing -> pure [delta] -- We can't split this one, so assume it's inhabited + Just arg_tys -> do + ev_pos <- refineToAltCon delta x (PmAltConLike cl) arg_tys ex_tvs >>= \case + Nothing -> pure [] + Just (delta', arg_vas) -> + go rec_ts (arg_vas ++ xs) n delta' + + -- Only n' more equations to go... + let n' = n - length ev_pos + ev_neg <- addRefutableAltCon delta x (PmAltConLike cl) >>= \case + Nothing -> pure [] + Just delta' -> go rec_ts (x:xs) n' delta' + + -- Actually there was no need to split if we see that both branches + -- were inhabited and we had no negative information on the variable! + -- So only refine delta if we find that one branch was indeed + -- uninhabited. + let neg = lookupRefuts delta x + case (ev_pos, ev_neg) of + ([], _) -> pure ev_neg + (_, []) -> pure ev_pos + _ | null neg -> pure [delta] + | otherwise -> pure (ev_pos ++ ev_neg) + +-- | Checks if every data con of the type 'isVanillaDataCon'. +isVanillaDataType :: Type -> Bool +isVanillaDataType ty = fromMaybe False $ do + (tc, _) <- splitTyConApp_maybe ty + dcs <- tyConDataCons_maybe tc + pure (all isVanillaDataCon dcs) + +-- Most of our actions thread around a delta from one computation to the next, +-- thereby potentially failing. This is expressed in the following Monad: +-- type PmM a = StateT Delta (MaybeT DsM) a + +-- | Records that a variable @x@ is equal to a 'CoreExpr' @e@. +addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta) +addVarCoreCt delta x e = runMaybeT (execStateT (core_expr x e) delta) + where + -- | Takes apart a 'CoreExpr' and tries to extract as much information about + -- literals and constructor applications as possible. + core_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) () + -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon + core_expr x (Cast e _co) = core_expr x e + core_expr x (Tick _t e) = core_expr x e + core_expr x e + | Just (pmLitAsStringLit -> Just s) <- coreExprAsPmLit e + , expr_ty `eqType` stringTy + -- See Note [Representation of Strings in TmState] + = case unpackFS s of + -- We need this special case to break a loop with coreExprAsPmLit + -- Otherwise we alternate endlessly between [] and "" + [] -> data_con_app x nilDataCon [] + s' -> core_expr x (mkListExpr charTy (map mkCharExpr s')) + | Just lit <- coreExprAsPmLit e + = pm_lit x lit + | Just (_in_scope, _empty_floats@[], dc, _arg_tys, args) + <- exprIsConApp_maybe empty_in_scope e + = do { arg_ids <- traverse bind_expr args + ; data_con_app x dc arg_ids } + -- TODO: Think about how to recognize PatSyns + | Var y <- e, not (isDataConWorkId x) + = modifyT (\delta -> addVarVarCt delta (x, y)) + | otherwise + -- TODO: Use a CoreMap to identify the CoreExpr with a unique representant + = pure () + where + empty_in_scope = (emptyInScopeSet, const NoUnfolding) + expr_ty = exprType e + + bind_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id + bind_expr e = do + x <- lift (lift (mkPmId (exprType e))) + core_expr x e + pure x + + data_con_app :: Id -> DataCon -> [Id] -> StateT Delta (MaybeT DsM) () + data_con_app x dc args = pm_alt_con_app x (PmAltConLike (RealDataCon dc)) args + + pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) () + pm_lit x lit = pm_alt_con_app x (PmAltLit lit) [] + + -- | Adds the given constructor application as a solution for @x@. + pm_alt_con_app :: Id -> PmAltCon -> [Id] -> StateT Delta (MaybeT DsM) () + pm_alt_con_app x con args = modifyT $ \delta -> addVarConCt delta x con args + +-- | Like 'modify', but with an effectful modifier action +modifyT :: Monad m => (s -> m s) -> StateT s m () +modifyT f = StateT $ fmap ((,) ()) . f diff --git a/compiler/deSugar/PmOracle.hs-boot b/compiler/deSugar/PmOracle.hs-boot new file mode 100644 index 0000000000..e099fe78a6 --- /dev/null +++ b/compiler/deSugar/PmOracle.hs-boot @@ -0,0 +1,7 @@ +module PmOracle where + +import GhcPrelude () + +data Delta + +initDelta :: Delta diff --git a/compiler/deSugar/PmPpr.hs b/compiler/deSugar/PmPpr.hs index 06b60a6806..bee38ed46b 100644 --- a/compiler/deSugar/PmPpr.hs +++ b/compiler/deSugar/PmPpr.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, ViewPatterns #-} -- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for -- user facing pattern match warnings. @@ -10,20 +10,20 @@ module PmPpr ( import GhcPrelude -import Name -import NameEnv -import NameSet +import Id +import VarEnv import UniqDFM -import UniqSet import ConLike import DataCon import TysWiredIn import Outputable -import Control.Monad.Trans.State.Strict -import Maybes +import Control.Monad.Trans.RWS.CPS import Util +import Maybes +import Data.List.NonEmpty (NonEmpty, nonEmpty, toList) -import TmOracle +import PmExpr +import PmOracle -- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its -- components and refutable shapes associated to any mentioned variables. @@ -35,22 +35,31 @@ import TmOracle -- where p is not one of {3, 4} -- q is not one of {0, 5} -- @ -pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc -pprUncovered (expr_vec, refuts) - | null cs = fsep vec -- there are no literal constraints - | otherwise = hang (fsep vec) 4 $ - text "where" <+> vcat (map pprRefutableShapes cs) +-- +-- When the set of refutable shapes contains more than 3 elements, the +-- additional elements are indicated by "...". +pprUncovered :: Delta -> [Id] -> SDoc +pprUncovered delta vas + | isNullUDFM refuts = fsep vec -- there are no refutations + | otherwise = hang (fsep vec) 4 $ + text "where" <+> vcat (map (pprRefutableShapes . snd) (udfmToList refuts)) where - sdoc_vec = mapM pprPmExprWithParens expr_vec - (vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts) + ppr_action = mapM (pprPmExprVar 2) vas + (vec, renamings) = runPmPpr delta ppr_action + refuts = prettifyRefuts delta renamings -- | Output refutable shapes of a variable in the form of @var is not one of {2, --- Nothing, 3}@. +-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is +-- indicated by an ellipsis. pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc pprRefutableShapes (var, alts) - = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts) + = var <+> text "is not one of" <+> format_alts alts where - ppr_alt (PmAltLit lit) = ppr lit + format_alts = braces . fsep . punctuate comma . shorten . map ppr_alt + shorten (a:b:c:_:_) = a:b:c:[text "..."] + shorten xs = xs + ppr_alt (PmAltConLike cl) = ppr cl + ppr_alt (PmAltLit lit) = ppr lit {- 1. Literals ~~~~~~~~~~~~~~ @@ -78,114 +87,115 @@ substitution to the vectors before printing them out (see function `pprOne' in Check.hs) to be more precise. -} --- | A 'PmRefutEnv' with pretty names for the occuring variables. -type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon]) - --- | Assigns pretty names to constraint variables in the domain of the given --- 'PmRefutEnv'. -prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv -prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList +-- | Extract and assigns pretty names to constraint variables with refutable +-- shapes. +prettifyRefuts :: Delta -> DIdEnv SDoc -> DIdEnv (SDoc, [PmAltCon]) +prettifyRefuts delta = listToUDFM . map attach_refuts . udfmToList where - rename new (old, lits) = (old, (new, lits)) - -- Try nice names p,q,r,s,t before using the (ugly) t_i - nameList :: [SDoc] - nameList = map text ["p","q","r","s","t"] ++ - [ text ('t':show u) | u <- [(0 :: Int)..] ] - -type PmPprM a = State (PrettyPmRefutEnv, NameSet) a --- (the first part of the state is read only. make it a reader?) - -runPmPpr :: PmPprM a -> PrettyPmRefutEnv -> (a, [(SDoc,[PmAltCon])]) -runPmPpr m lit_env = (result, mapMaybe is_used (udfmToList lit_env)) - where - (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet) - - is_used (k,v) - | elemUniqSet_Directly k used = Just v - | otherwise = Nothing - -addUsed :: Name -> PmPprM () -addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x)) - -checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated -checkNegation x = do - negated <- gets fst - return $ case lookupDNameEnv negated x of - Just (new, _) -> Just new - Nothing -> Nothing - --- | Pretty print a pmexpr, but remember to prettify the names of the variables + attach_refuts (u, sdoc) = (u, (sdoc, lookupRefuts delta u)) + + +type PmPprM a = RWS Delta () (DIdEnv SDoc, [SDoc]) a + +-- Try nice names p,q,r,s,t before using the (ugly) t_i +nameList :: [SDoc] +nameList = map text ["p","q","r","s","t"] ++ + [ text ('t':show u) | u <- [(0 :: Int)..] ] + +runPmPpr :: Delta -> PmPprM a -> (a, DIdEnv SDoc) +runPmPpr delta m = case runRWS m delta (emptyDVarEnv, nameList) of + (a, (renamings, _), _) -> (a, renamings) + +-- | Allocates a new, clean name for the given 'Id' if it doesn't already have +-- one. +getCleanName :: Id -> PmPprM SDoc +getCleanName x = do + (renamings, name_supply) <- get + let (clean_name:name_supply') = name_supply + case lookupDVarEnv renamings x of + Just nm -> pure nm + Nothing -> do + put (extendDVarEnv renamings x clean_name, name_supply') + pure clean_name + +checkRefuts :: Id -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached +checkRefuts x = do + delta <- ask + case lookupRefuts delta x of + [] -> pure Nothing -- Will just be a wildcard later on + _ -> Just <$> getCleanName x + +-- | Pretty print a variable, but remember to prettify the names of the variables -- that refer to neg-literals. The ones that cannot be shown are printed as -- underscores. -pprPmExpr :: PmExpr -> PmPprM SDoc -pprPmExpr (PmExprVar x) = do - mb_name <- checkNegation x - case mb_name of - Just name -> addUsed x >> return name - Nothing -> return underscore -pprPmExpr (PmExprCon con args) = pprPmExprCon con args -pprPmExpr (PmExprLit l) = return (ppr l) -pprPmExpr (PmExprOther _) = return underscore -- don't show - -needsParens :: PmExpr -> Bool -needsParens (PmExprVar {}) = False -needsParens (PmExprLit l) = isNegatedPmLit l -needsParens (PmExprOther {}) = False -- will become a wildcard -needsParens (PmExprCon (RealDataCon c) es) - | isTupleDataCon c - || isConsDataCon c || null es = False - | otherwise = True -needsParens (PmExprCon (PatSynCon _) es) = not (null es) - -pprPmExprWithParens :: PmExpr -> PmPprM SDoc -pprPmExprWithParens expr - | needsParens expr = parens <$> pprPmExpr expr - | otherwise = pprPmExpr expr - -pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc -pprPmExprCon (RealDataCon con) args - | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args - | isConsDataCon con = pretty_list - where - mkTuple :: [SDoc] -> SDoc - mkTuple = parens . fsep . punctuate comma - - -- lazily, to be used in the list case only - pretty_list :: PmPprM SDoc - pretty_list = case isNilPmExpr (last list) of - True -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list) - False -> parens . hcat . punctuate colon <$> mapM pprPmExpr list - - list = list_elements args - - list_elements [x,y] - | PmExprCon c es <- y, RealDataCon nilDataCon == c - = ASSERT(null es) [x,y] - | PmExprCon c es <- y, RealDataCon consDataCon == c - = x : list_elements es - | otherwise = [x,y] - list_elements list = pprPanic "list_elements:" (ppr list) -pprPmExprCon cl args +pprPmExprVar :: Int -> Id -> PmPprM SDoc +pprPmExprVar prec x = do + delta <- ask + case lookupSolution delta x of + Just (alt, args) -> pprPmExprCon prec alt args + Nothing -> fromMaybe underscore <$> checkRefuts x + +pprPmExprCon :: Int -> PmAltCon -> [Id] -> PmPprM SDoc +pprPmExprCon _prec (PmAltLit l) _ = pure (ppr l) +pprPmExprCon prec (PmAltConLike cl) args = do + delta <- ask + pprConLike delta prec cl args + +pprConLike :: Delta -> Int -> ConLike -> [Id] -> PmPprM SDoc +pprConLike delta _prec cl args + | Just pm_expr_list <- pmExprAsList delta (PmAltConLike cl) args + = case pm_expr_list of + NilTerminated list -> + brackets . fsep . punctuate comma <$> mapM (pprPmExprVar 0) list + WcVarTerminated pref x -> + parens . fcat . punctuate colon <$> mapM (pprPmExprVar 0) (toList pref ++ [x]) +pprConLike _delta _prec (RealDataCon con) args + | isUnboxedTupleCon con + , let hash_parens doc = text "(#" <+> doc <+> text "#)" + = hash_parens . fsep . punctuate comma <$> mapM (pprPmExprVar 0) args + | isTupleDataCon con + = parens . fsep . punctuate comma <$> mapM (pprPmExprVar 0) args +pprConLike _delta prec cl args | conLikeIsInfix cl = case args of - [x, y] -> do x' <- pprPmExprWithParens x - y' <- pprPmExprWithParens y - return (x' <+> ppr cl <+> y') + [x, y] -> do x' <- pprPmExprVar 1 x + y' <- pprPmExprVar 1 y + return (cparen (prec > 0) (x' <+> ppr cl <+> y')) -- can it be infix but have more than two arguments? list -> pprPanic "pprPmExprCon:" (ppr list) | null args = return (ppr cl) - | otherwise = do args' <- mapM pprPmExprWithParens args - return (fsep (ppr cl : args')) - --- | Check whether a literal is negated -isNegatedPmLit :: PmLit -> Bool -isNegatedPmLit (PmOLit b _) = b -isNegatedPmLit _other_lit = False - --- | Check whether a PmExpr is syntactically e -isNilPmExpr :: PmExpr -> Bool -isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon -isNilPmExpr _other_expr = False - --- | Check if a DataCon is (:). -isConsDataCon :: DataCon -> Bool -isConsDataCon con = consDataCon == con + | otherwise = do args' <- mapM (pprPmExprVar 2) args + return (cparen (prec > 1) (fsep (ppr cl : args'))) + +-- | The result of 'pmExprAsList'. +data PmExprList + = NilTerminated [Id] + | WcVarTerminated (NonEmpty Id) Id + +-- | Extract a list of 'PmExpr's out of a sequence of cons cells, optionally +-- terminated by a wildcard variable instead of @[]@. Some examples: +-- +-- * @pmExprAsList (1:2:[]) == Just ('NilTerminated' [1,2])@, a regular, +-- @[]@-terminated list. Should be pretty-printed as @[1,2]@. +-- * @pmExprAsList (1:2:x) == Just ('WcVarTerminated' [1,2] x)@, a list prefix +-- ending in a wildcard variable x (of list type). Should be pretty-printed as +-- (1:2:_). +-- * @pmExprAsList [] == Just ('NilTerminated' [])@ +pmExprAsList :: Delta -> PmAltCon -> [Id] -> Maybe PmExprList +pmExprAsList delta = go_con [] + where + go_var rev_pref x + | Just (alt, args) <- lookupSolution delta x + = go_con rev_pref alt args + go_var rev_pref x + | Just pref <- nonEmpty (reverse rev_pref) + = Just (WcVarTerminated pref x) + go_var _ _ + = Nothing + + go_con rev_pref (PmAltConLike (RealDataCon c)) es + | c == nilDataCon + = ASSERT( null es ) Just (NilTerminated (reverse rev_pref)) + | c == consDataCon + = ASSERT( length es == 2 ) go_var (es !! 0 : rev_pref) (es !! 1) + go_con _ _ _ + = Nothing diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs deleted file mode 100644 index db3ce6d770..0000000000 --- a/compiler/deSugar/TmOracle.hs +++ /dev/null @@ -1,362 +0,0 @@ -{- -Author: George Karachalias <george.karachalias@cs.kuleuven.be> --} - -{-# LANGUAGE CPP, MultiWayIf #-} - --- | The term equality oracle. The main export of the module are the functions --- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'. --- --- If you are looking for an oracle that can solve type-level constraints, look --- at 'TcSimplify.tcCheckSatisfiability'. -module TmOracle ( - - -- re-exported from PmExpr - PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), TmVarCtEnv, - PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr, - - -- the term oracle - tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq, - extendSubst, canDiverge, isRigid, - addSolveRefutableAltCon, lookupRefutableAltCons, - - -- misc. - exprDeepLookup, pmLitType - ) where - -#include "HsVersions.h" - -import GhcPrelude - -import PmExpr - -import Util -import Id -import Name -import Type -import HsLit -import TcHsSyn -import MonadUtils -import ListSetOps (insertNoDup, unionLists) -import Maybes -import Outputable -import NameEnv -import UniqFM -import UniqDFM - -{- -%************************************************************************ -%* * - The term equality oracle -%* * -%************************************************************************ --} - --- | Pretty much a @['TmVarCt']@ association list where the domain is 'Name' --- instead of 'Id'. This is the type of 'tm_pos', where we store solutions for --- rigid pattern match variables. -type TmVarCtEnv = NameEnv PmExpr - --- | An environment assigning shapes to variables that immediately lead to a --- refutation. So, if this maps @x :-> [3]@, then trying to solve a 'TmVarCt' --- like @x ~ 3@ immediately leads to a contradiction. --- Determinism is important since we use this for warning messages in --- 'PmPpr.pprUncovered'. We don't do the same for 'TmVarCtEnv', so that is a plain --- 'NameEnv'. --- --- See also Note [Refutable shapes] in TmOracle. -type PmRefutEnv = DNameEnv [PmAltCon] - --- | The state of the term oracle. Tracks all term-level facts of the form "x is --- @True@" ('tm_pos') and "x is not @5@" ('tm_neg'). --- --- Subject to Note [The Pos/Neg invariant]. -data TmState = TmS - { tm_pos :: !TmVarCtEnv - -- ^ A substitution with solutions we extend with every step and return as a - -- result. The substitution is in /triangular form/: It might map @x@ to @y@ - -- where @y@ itself occurs in the domain of 'tm_pos', rendering lookup - -- non-idempotent. This means that 'varDeepLookup' potentially has to walk - -- along a chain of var-to-var mappings until we find the solution but has the - -- advantage that when we update the solution for @y@ above, we automatically - -- update the solution for @x@ in a union-find-like fashion. - -- Invariant: Only maps to other variables ('PmExprVar') or to WHNFs - -- ('PmExprLit', 'PmExprCon'). Ergo, never maps to a 'PmExprOther'. - , tm_neg :: !PmRefutEnv - -- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely - -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal - -- 3 or 4. Should we later solve @x@ to a variable @y@ - -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of - -- @y@. See also Note [The Pos/Neg invariant]. - } - -{- Note [The Pos/Neg invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Invariant: In any 'TmState', The domains of 'tm_pos' and 'tm_neg' are disjoint. - -For example, it would make no sense to say both - tm_pos = [...x :-> 3 ...] - tm_neg = [...x :-> [4,42]... ] -The positive information is strictly more informative than the negative. - -Suppose we are adding the (positive) fact @x :-> e@ to 'tm_pos'. Then we must -delete any binding for @x@ from 'tm_neg', to uphold the invariant. - -But there is more! Suppose we are adding @x :-> y@ to 'tm_pos', and 'tm_neg' -contains @x :-> cs, y :-> ds@. Then we want to update 'tm_neg' to -@y :-> (cs ++ ds)@, to make use of the negative information we have about @x@. --} - -instance Outputable TmState where - ppr state = braces (fsep (punctuate comma (pos ++ neg))) - where - pos = map pos_eq (nonDetUFMToList (tm_pos state)) - neg = map neg_eq (udfmToList (tm_neg state)) - pos_eq (l, r) = ppr l <+> char '~' <+> ppr r - neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r - --- | Initial state of the oracle. -initialTmState :: TmState -initialTmState = TmS emptyNameEnv emptyDNameEnv - --- | Wrap up the term oracle's state once solving is complete. Return the --- flattened 'tm_pos' and 'tm_neg'. -wrapUpTmState :: TmState -> (TmVarCtEnv, PmRefutEnv) -wrapUpTmState solver_state - = (flattenTmVarCtEnv (tm_pos solver_state), tm_neg solver_state) - --- | Flatten the triangular subsitution. -flattenTmVarCtEnv :: TmVarCtEnv -> TmVarCtEnv -flattenTmVarCtEnv env = mapNameEnv (exprDeepLookup env) env - --- | Check whether a constraint (x ~ BOT) can succeed, --- given the resulting state of the term oracle. -canDiverge :: Name -> TmState -> Bool -canDiverge x TmS{ tm_pos = pos, tm_neg = neg } - -- If the variable seems not evaluated, there is a possibility for - -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found - -- a solution (i.e. some equivalent literal or constructor) for it yet. - | (_, PmExprVar y) <- varDeepLookup pos x -- seems not forced - -- Even if we don't have a solution yet, it might be involved in a negative - -- constraint, in which case we must already have evaluated it earlier. - , Nothing <- lookupDNameEnv neg y - = True - -- Variable x is already in WHNF or we know some refutable shape, so the - -- constraint is non-satisfiable - | otherwise = False - --- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that --- @x@ and @e@ are completely substituted before! -isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool -isRefutable x e env - = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x - --- | Solve an equality (top-level). -solveOneEq :: TmState -> TmVarCt -> Maybe TmState -solveOneEq solver_env (TVC x e) = unify solver_env (PmExprVar (idName x), e) - -exprToAlt :: PmExpr -> Maybe PmAltCon -exprToAlt (PmExprLit l) = Just (PmAltLit l) -exprToAlt _ = Nothing - --- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the --- 'TmState' and return @Nothing@ if that leads to a contradiction. -addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState -addSolveRefutableAltCon original@TmS{ tm_pos = pos, tm_neg = neg } x nalt - = case exprToAlt e of - -- We have to take care to preserve Note [The Pos/Neg invariant] - Nothing -> Just extended -- Not solved yet - Just alt -- We have a solution - | alt == nalt -> Nothing -- ... which is contradictory - | otherwise -> Just original -- ... which is compatible, rendering the - where -- refutation redundant - (y, e) = varDeepLookup pos (idName x) - extended = original { tm_neg = neg' } - neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y - --- | When updating 'tm_neg', we want to delete any 'null' entries. This adapter --- intends to provide a suitable interface for 'alterDNameEnv'. -delNulls :: ([a] -> [a]) -> Maybe [a] -> Maybe [a] -delNulls f mb_entry - | ret@(_:_) <- f (fromMaybe [] mb_entry) = Just ret - | otherwise = Nothing - --- | Return all 'PmAltCon' shapes that are impossible for 'Id' to take, i.e. --- would immediately lead to a refutation by the term oracle. -lookupRefutableAltCons :: Id -> TmState -> [PmAltCon] -lookupRefutableAltCons x TmS { tm_neg = neg } - = fromMaybe [] (lookupDNameEnv neg (idName x)) - --- | Is the given variable /rigid/ (i.e., we have a solution for it) or --- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A --- semantically helpful alias for 'lookupNameEnv'. -isRigid :: TmState -> Name -> Maybe PmExpr -isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x - --- | @isFlexible tms = isNothing . 'isRigid' tms@ -isFlexible :: TmState -> Name -> Bool -isFlexible tms = isNothing . isRigid tms - --- | Try to unify two 'PmExpr's and record the gained knowledge in the --- 'TmState'. --- --- Returns @Nothing@ when there's a contradiction. Returns @Just tms@ --- when the constraint was compatible with prior facts, in which case @tms@ has --- integrated the knowledge from the equality constraint. -unify :: TmState -> (PmExpr, PmExpr) -> Maybe TmState -unify tms eq@(e1, e2) = case eq of - -- We cannot do a thing about these cases - (PmExprOther _,_) -> boring - (_,PmExprOther _) -> boring - - (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of - -- See Note [Undecidable Equality for Overloaded Literals] - True -> boring - False -> unsat - - (PmExprCon c1 ts1, PmExprCon c2 ts2) - | c1 == c2 -> foldlM unify tms (zip ts1 ts2) - | otherwise -> unsat - - (PmExprVar x, PmExprVar y) - | x == y -> boring - - -- It's important to handle both rigid cases first, otherwise we get cyclic - -- substitutions. Cf. 'extendSubstAndSolve' and - -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@. - (PmExprVar x, _) - | Just e1' <- isRigid tms x -> unify tms (e1', e2) - (_, PmExprVar y) - | Just e2' <- isRigid tms y -> unify tms (e1, e2') - (PmExprVar x, PmExprVar y) -> Just (equate x y tms) - (PmExprVar x, _) -> trySolve x e2 tms - (_, PmExprVar y) -> trySolve y e1 tms - - _ -> WARN( True, text "unify: Catch all" <+> ppr eq) - boring -- I HATE CATCH-ALLS - where - boring = Just tms - unsat = Nothing - --- | Merges the equivalence classes of @x@ and @y@ by extending the substitution --- with @x :-> y@. --- Preconditions: @x /= y@ and both @x@ and @y@ are flexible (cf. --- 'isFlexible'/'isRigid'). -equate :: Name -> Name -> TmState -> TmState -equate x y tms@TmS{ tm_pos = pos, tm_neg = neg } - = ASSERT( x /= y ) - ASSERT( isFlexible tms x ) - ASSERT( isFlexible tms y ) - tms' - where - pos' = extendNameEnv pos x (PmExprVar y) - -- Be careful to uphold Note [The Pos/Neg invariant] by merging the refuts - -- of x into those of y - nalts = fromMaybe [] (lookupDNameEnv neg x) - neg' = alterDNameEnv (delNulls (unionLists nalts)) neg y - `delFromDNameEnv` x - tms' = TmS { tm_pos = pos', tm_neg = neg' } - --- | Extend the substitution with a mapping @x: -> e@ if compatible with --- refutable shapes of @x@ and its solution, reject (@Nothing@) otherwise. --- --- Precondition: @x@ is flexible (cf. 'isFlexible'/'isRigid'). --- Precondition: @e@ is a 'PmExprCon' or 'PmExprLit' -trySolve:: Name -> PmExpr -> TmState -> Maybe TmState -trySolve x e _tms@TmS{ tm_pos = pos, tm_neg = neg } - | ASSERT( isFlexible _tms x ) - ASSERT( _is_whnf e ) - isRefutable x e neg - = Nothing - | otherwise - = Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x)) - where - _is_whnf PmExprCon{} = True - _is_whnf PmExprLit{} = True - _is_whnf _ = False - --- | When we know that a variable is fresh, we do not actually have to --- check whether anything changes, we know that nothing does. Hence, --- @extendSubst@ simply extends the substitution, unlike what --- 'extendSubstAndSolve' does. -extendSubst :: Id -> PmExpr -> TmState -> TmState -extendSubst y e solver_state@TmS{ tm_pos = pos } - | isNotPmExprOther simpl_e - = solver_state { tm_pos = extendNameEnv pos x simpl_e } - | otherwise = solver_state - where - x = idName y - simpl_e = exprDeepLookup pos e - --- | Apply an (un-flattened) substitution to a variable and return its --- representative in the triangular substitution @env@ and the completely --- substituted expression. The latter may just be the representative wrapped --- with 'PmExprVar' if we haven't found a solution for it yet. -varDeepLookup :: TmVarCtEnv -> Name -> (Name, PmExpr) -varDeepLookup env x = case lookupNameEnv env x of - Just (PmExprVar y) -> varDeepLookup env y - Just e -> (x, exprDeepLookup env e) -- go deeper - Nothing -> (x, PmExprVar x) -- terminal -{-# INLINE varDeepLookup #-} - --- | Apply an (un-flattened) substitution to an expression. -exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr -exprDeepLookup env (PmExprVar x) = snd (varDeepLookup env x) -exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es) -exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther - --- | External interface to the term oracle. -tmOracle :: TmState -> [TmVarCt] -> Maybe TmState -tmOracle tm_state eqs = foldlM solveOneEq tm_state eqs - --- | Type of a PmLit -pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :( -pmLitType (PmSLit lit) = hsLitType lit -pmLitType (PmOLit _ lit) = overLitType lit - -{- Note [Refutable shapes] -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Consider a pattern match like - - foo x - | 0 <- x = 42 - | 0 <- x = 43 - | 1 <- x = 44 - | otherwise = 45 - -This will result in the following initial matching problem: - - PatVec: x (0 <- x) - ValVec: $tm_y - -Where the first line is the pattern vector and the second line is the value -vector abstraction. When we handle the first pattern guard in Check, it will be -desugared to a match of the form - - PatVec: x 0 - ValVec: $tm_y x - -In LitVar, this will split the value vector abstraction for `x` into a positive -`PmLit 0` and a negative `PmLit x [0]` value abstraction. While the former is -immediately matched against the pattern vector, the latter (vector value -abstraction `~[0] $tm_y`) is completely uncovered by the clause. - -`pmcheck` proceeds by *discarding* the the value vector abstraction involving -the guard to accomodate for the desugaring. But this also discards the valuable -information that `x` certainly is not the literal 0! Consequently, we wouldn't -be able to report the second clause as redundant. - -That's a typical example of why we need the term oracle, and in this specific -case, the ability to encode that `x` certainly is not the literal 0. Now the -term oracle can immediately refute the constraint `x ~ 0` generated by the -second clause and report the clause as redundant. After the third clause, the -set of such *refutable* literals is again extended to `[0, 1]`. - -In general, we want to store a set of refutable shapes (`PmAltCon`) for each -variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will -add such a refutable mapping to the `PmRefutEnv` in the term oracles state and -check if causes any immediate contradiction. Whenever we record a solution in -the substitution via `extendSubstAndSolve`, the refutable environment is checked -for any matching refutable `PmAltCon`. --} diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index 7946e233c4..884006b487 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -336,7 +336,7 @@ Library PprCore PmExpr PmPpr - TmOracle + PmOracle Check Coverage Desugar @@ -572,7 +572,6 @@ Library IOEnv Json ListSetOps - ListT Maybes MonadUtils OrdList diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 5d56d33d53..0a2db75a2d 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -167,7 +167,7 @@ import TcType import Annotations import InstEnv import FamInstEnv -import PmExpr +import {-# SOURCE #-} PmOracle (Delta) import IOEnv import RdrName import Name @@ -390,10 +390,9 @@ data DsLclEnv = DsLclEnv { dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs -- See Note [Note [Type and Term Equality Propagation] in Check.hs - -- These two fields are augmented as we walk inwards, - -- through each patttern match in turn - dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching - dsl_tm_cs :: Bag TmVarCt, -- Constraints form term-level pattern matching + -- The oracle state Delta is augmented as we walk inwards, + -- through each pattern match in turn + dsl_delta :: Delta, dsl_pm_iter :: IORef Int -- Number of iterations for pmcheck so far -- We fail if this gets too big diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 48c7305669..18f2c505d9 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -688,6 +688,8 @@ constraints or to decide if a particular set of constraints is satisfiable, the purpose of tcNormalise is to take a type, plus some local constraints, and normalise the type as much as possible with respect to those constraints. +It does *not* reduce type or data family applications or look through newtypes. + Why is this useful? As one example, when coverage-checking an EmptyCase expression, it's possible that the type of the scrutinee will only reduce if some local equalities are solved for. See "Wrinkle: Local equalities" diff --git a/compiler/utils/Binary.hs b/compiler/utils/Binary.hs index 7a3b7a1472..164549fe58 100644 --- a/compiler/utils/Binary.hs +++ b/compiler/utils/Binary.hs @@ -935,7 +935,6 @@ putTypeRep bh (Fun arg res) = do put_ bh (3 :: Word8) putTypeRep bh arg putTypeRep bh res -putTypeRep _ _ = fail "Binary.putTypeRep: Impossible" getSomeTypeRep :: BinHandle -> IO SomeTypeRep getSomeTypeRep bh = do diff --git a/compiler/utils/ListSetOps.hs b/compiler/utils/ListSetOps.hs index 8078d5603e..a8b717df00 100644 --- a/compiler/utils/ListSetOps.hs +++ b/compiler/utils/ListSetOps.hs @@ -14,7 +14,7 @@ module ListSetOps ( Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing, -- Duplicate handling - hasNoDups, removeDups, findDupsEq, insertNoDup, + hasNoDups, removeDups, findDupsEq, equivClasses, -- Indexing @@ -178,10 +178,3 @@ findDupsEq _ [] = [] findDupsEq eq (x:xs) | null eq_xs = findDupsEq eq xs | otherwise = (x :| eq_xs) : findDupsEq eq neq_xs where (eq_xs, neq_xs) = partition (eq x) xs - --- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only --- when an equal element couldn't be found in @xs@. -insertNoDup :: (Eq a) => a -> [a] -> [a] -insertNoDup x set - | elem x set = set - | otherwise = x:set diff --git a/compiler/utils/ListT.hs b/compiler/utils/ListT.hs deleted file mode 100644 index 66e52ed9f4..0000000000 --- a/compiler/utils/ListT.hs +++ /dev/null @@ -1,79 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} - -------------------------------------------------------------------------- --- | --- Module : Control.Monad.Logic --- Copyright : (c) Dan Doel --- License : BSD3 --- --- Maintainer : dan.doel@gmail.com --- Stability : experimental --- Portability : non-portable (multi-parameter type classes) --- --- A backtracking, logic programming monad. --- --- Adapted from the paper --- /Backtracking, Interleaving, and Terminating --- Monad Transformers/, by --- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry --- (<http://www.cs.rutgers.edu/~ccshan/logicprog/ListT-icfp2005.pdf>). -------------------------------------------------------------------------- - -module ListT ( - ListT(..), - runListT, - select, - fold - ) where - -import GhcPrelude - -import Control.Applicative - -import Control.Monad -import Control.Monad.Fail as MonadFail - -------------------------------------------------------------------------- --- | A monad transformer for performing backtracking computations --- layered over another monad 'm' -newtype ListT m a = - ListT { unListT :: forall r. (a -> m r -> m r) -> m r -> m r } - deriving (Functor) - -select :: Monad m => [a] -> ListT m a -select xs = foldr (<|>) mzero (map pure xs) - -fold :: ListT m a -> (a -> m r -> m r) -> m r -> m r -fold = runListT - -------------------------------------------------------------------------- --- | Runs a ListT computation with the specified initial success and --- failure continuations. -runListT :: ListT m a -> (a -> m r -> m r) -> m r -> m r -runListT = unListT - -instance Applicative (ListT f) where - pure a = ListT $ \sk fk -> sk a fk - f <*> a = ListT $ \sk fk -> unListT f (\g fk' -> unListT a (sk . g) fk') fk - -instance Alternative (ListT f) where - empty = ListT $ \_ fk -> fk - f1 <|> f2 = ListT $ \sk fk -> unListT f1 sk (unListT f2 sk fk) - -instance Monad (ListT m) where - m >>= f = ListT $ \sk fk -> unListT m (\a fk' -> unListT (f a) sk fk') fk -#if !MIN_VERSION_base(4,13,0) - fail = MonadFail.fail -#endif - -instance MonadFail.MonadFail (ListT m) where - fail _ = ListT $ \_ fk -> fk - -instance MonadPlus (ListT m) where - mzero = ListT $ \_ fk -> fk - m1 `mplus` m2 = ListT $ \sk fk -> unListT m1 sk (unListT m2 sk fk) diff --git a/compiler/utils/Outputable.hs b/compiler/utils/Outputable.hs index a5306faaa4..cd3e2a5f5b 100644 --- a/compiler/utils/Outputable.hs +++ b/compiler/utils/Outputable.hs @@ -1205,7 +1205,7 @@ pprTraceM str doc = pprTrace str doc (pure ()) -- | @pprTraceWith desc f x@ is equivalent to @pprTrace desc (f x) x@. -- This allows you to print details from the returned value as well as from -- ambient variables. -pprTraceWith :: Outputable a => String -> (a -> SDoc) -> a -> a +pprTraceWith :: String -> (a -> SDoc) -> a -> a pprTraceWith desc f x = pprTrace desc (f x) x -- | @pprTraceIt desc x@ is equivalent to @pprTrace desc (ppr x) x@ diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs index 51812cca75..d6cea5ca8d 100644 --- a/compiler/utils/Util.hs +++ b/compiler/utils/Util.hs @@ -14,6 +14,9 @@ module Util ( ghciTablesNextToCode, isWindowsHost, isDarwinHost, + -- * Miscellaneous higher-order functions + applyWhen, nTimes, + -- * General list processing zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal, zipLazy, stretchZipWith, zipWithAndUnzip, zipAndUnzip, @@ -57,9 +60,6 @@ module Util ( takeList, dropList, splitAtList, split, dropTail, capitalise, - -- * For loop - nTimes, - -- * Sorting sortWith, minWith, nubSort, ordNub, @@ -222,12 +222,17 @@ isDarwinHost = False {- ************************************************************************ * * -\subsection{A for loop} +\subsection{Miscellaneous higher-order functions} * * ************************************************************************ -} --- | Compose a function with itself n times. (nth rather than twice) +-- | Apply a function iff some condition is met. +applyWhen :: Bool -> (a -> a) -> a -> a +applyWhen True f x = f x +applyWhen _ _ x = x + +-- | A for loop: Compose a function with itself n times. (nth rather than twice) nTimes :: Int -> (a -> a) -> (a -> a) nTimes 0 _ = id nTimes 1 f = f |