[Git][ghc/ghc][wip/pmcheck-ncon] 2 commits: TmOracle: Replace negative term equalities by refutable PmAltCons
Sebastian Graf
gitlab at gitlab.haskell.org
Mon May 27 15:13:13 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-ncon at Glasgow Haskell Compiler / GHC
Commits:
20611ad8 by Sebastian Graf at 2019-05-27T07:45:21Z
TmOracle: Replace negative term equalities by refutable PmAltCons
The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".
This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5" or "x can no longer be Just y,
for any y". We encode this knowledge in a `PmRefutEnv`, mapping a set of
newly introduced `PmAltCon`s (literals and `ConLike`s) to eac variable
denoting above inequalities.
So, say we have `x ≁ Just ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ Just 5`. The entry in the refutable
environment will immediately lead to a contradiction.
This machinery renders the whole `PmExprEq` business unnecessary,
getting rid of a lot of (mostly dead) code.
Note that the `PmAltConLike` case is currently unnecessary: The `ConVar`
case will just split the value set abstraction for each possible
constructor instead of encoding negative equalites. This is bound to
change in a follow-up patch. If we began to use `PmAltConLike`, we'd
even profit from nicer error messages as is currently the case for
negative literal equalities.
See the Note [Refutable shapes] in TmOracle for a place to start.
- - - - -
5a263c0a by Sebastian Graf at 2019-05-27T15:12:50Z
Add `PmNCons` to `Check` for correct warnings in the presence of `COMPLETE` groups
Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).
The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.
The `getResult` function would then pick the outcome according to
metrics defined in accordance to the user's guide. But crucially, it
lacked knowledge about the order in which affected clauses appear,
leading to the surprising behavior in #13363.
The introduction of an `PmNCons` variant in `PmPat` fixes this: Instead
of committing to a particular `COMPLETE` group in the `ConVar` case,
we now split off the matching constructor incrementally and record the
newly covered case in `PmNCons`.
After all clauses have been processed this way, we filter out any value
vector abstractions from the uncovered set involving `PmNCons` whose set
of covered constructors completely overlap a `COMPLETE` set.
- - - - -
14 changed files:
- compiler/basicTypes/NameEnv.hs
- compiler/deSugar/Check.hs
- compiler/deSugar/PmExpr.hs
- + compiler/deSugar/PmPpr.hs
- compiler/deSugar/TmOracle.hs
- compiler/ghc.cabal.in
- compiler/utils/ListSetOps.hs
- compiler/utils/Outputable.hs
- libraries/binary
- + testsuite/tests/pmcheck/complete_sigs/T13363a.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
- + testsuite/tests/pmcheck/complete_sigs/T13363b.hs
- + testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
- testsuite/tests/pmcheck/complete_sigs/all.T
Changes:
=====================================
compiler/basicTypes/NameEnv.hs
=====================================
@@ -25,6 +25,7 @@ module NameEnv (
emptyDNameEnv,
lookupDNameEnv,
+ delFromDNameEnv,
mapDNameEnv,
alterDNameEnv,
-- ** Dependency analysis
@@ -147,6 +148,9 @@ emptyDNameEnv = emptyUDFM
lookupDNameEnv :: DNameEnv a -> Name -> Maybe a
lookupDNameEnv = lookupUDFM
+delFromDNameEnv :: DNameEnv a -> Name -> DNameEnv a
+delFromDNameEnv = delFromUDFM
+
mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
mapDNameEnv = mapUDFM
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -25,6 +25,7 @@ module Check (
import GhcPrelude
import TmOracle
+import PmPpr
import Unify( tcMatchTy )
import DynFlags
import HsSyn
@@ -54,20 +55,19 @@ import TyCoRep
import Type
import UniqSupply
import DsUtils (isTrueLHsExpr)
-import Maybes (expectJust)
+import Maybes (MaybeT (..), 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, foldM, when, guard, forM_, zipWithM, filterM)
+import Control.Monad.Trans.Class (lift)
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}
@@ -90,72 +90,33 @@ 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`.
-
-type PmM a = ListT DsM a
-
-liftD :: DsM a -> PmM a
-liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
+type PmM = DsM
--- 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
+-- | Used only as a kind, to index PmPat
+data PatTy = PAT | VA
-- The *arity* of a PatVec [p1,..,pn] is
-- the number of p1..pn that are not Guards
data PmPat :: PatTy -> * where
+ -- | For the arguments' meaning see 'HsPat.ConPatOut'.
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]
+ -- | See Note [Literals in PmPat]
+ PmLit :: { pm_lit_lit :: PmLit } -> PmPat t
+ -- | Literal values the wrapped 'Id' cannot take on.
+ -- See Note [PmNLit and PmNCon].
PmNLit :: { pm_lit_id :: Id
, pm_lit_not :: [PmLit] } -> PmPat 'VA
+ -- | Top-level 'ConLike's the wrapped 'Id' cannot take on.
+ -- See Note [PmNLit and PmNCon].
+ PmNCon :: { pm_con_id :: Id
+ , pm_con_grps :: [[ConLike]]
+ , pm_con_not :: [ConLike] } -> 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.
@@ -198,8 +159,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
@@ -216,8 +176,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
@@ -228,51 +187,26 @@ 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.<>)
-
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
+ ppr (PartialResult c vsa d)
+ = text "PartialResult" <+> ppr c <+> ppr d <+> ppr vsa
instance Semi.Semigroup PartialResult where
- (PartialResult prov1 cs1 vsa1 ds1)
- <> (PartialResult prov2 cs2 vsa2 ds2)
- = PartialResult (prov1 Semi.<> prov2)
- (cs1 Semi.<> cs2)
+ (PartialResult cs1 vsa1 ds1)
+ <> (PartialResult cs2 vsa2 ds2)
+ = PartialResult (cs1 Semi.<> cs2)
(vsa1 Semi.<> vsa2)
(ds1 Semi.<> ds2)
instance Monoid PartialResult where
- mempty = PartialResult mempty mempty [] mempty
+ mempty = PartialResult mempty [] mempty
mappend = (Semi.<>)
-- newtype ChoiceOf a = ChoiceOf [a]
@@ -290,15 +224,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)
]
@@ -323,11 +255,11 @@ instance Outputable UncoveredCandidates where
-- | The empty pattern check result
emptyPmResult :: PmResult
-emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
+emptyPmResult = PmResult [] (UncoveredPatterns []) []
-- | Non-exhaustive empty case with unknown/trivial inhabitants
uncoveredWithTy :: Type -> PmResult
-uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
+uncoveredWithTy ty = PmResult [] (TypeOfUncovered ty) []
{-
%************************************************************************
@@ -340,8 +272,8 @@ 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
@@ -349,25 +281,25 @@ checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
-- | Check a single pattern binding (let)
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
checkSingle' locn var p = do
- liftD resetPmIterDs -- set the iter-no to zero
- fam_insts <- liftD dsGetFamInstEnvs
- clause <- liftD $ translatePat fam_insts p
+ resetPmIterDs -- set the iter-no to zero
+ fam_insts <- dsGetFamInstEnvs
+ clause <- 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
+ PartialResult cs us ds <- runMany (pmcheckI clause []) missing
+ us' <- UncoveredPatterns <$> normaliseUncovered 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 [] us' [] -- useful
+ (NotCovered, NotDiverged) -> PmResult m us' [] -- redundant
+ (NotCovered, Diverged ) -> PmResult [] us' m -- inaccessible rhs
where m = [cL locn [cL locn p]]
-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions.
checkGuardMatches :: HsMatchContext Name -- Match context
-> GRHSs GhcTc (LHsExpr GhcTc) -- Guarded RHSs
- -> DsM ()
+ -> PmM ()
checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
dflags <- getDynFlags
let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
@@ -382,14 +314,14 @@ checkGuardMatches _ (XGRHSs _) = panic "checkGuardMatches"
-- | Check a matchgroup (case, functions, etc.)
checkMatches :: DynFlags -> DsMatchContext
- -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
+ -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM ()
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]
[] | [var] <- vars -> checkEmptyCase' var
@@ -404,38 +336,36 @@ checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
checkMatches' vars matches
| null matches = panic "checkMatches': EmptyCase"
| otherwise = do
- liftD resetPmIterDs -- set the iter-no to zero
+ resetPmIterDs -- set the iter-no to zero
missing <- mkInitialUncovered vars
tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
- (prov, rs,us,ds) <- go matches missing
+ (rs,us,ds) <- go matches missing
+ us' <- normaliseUncovered us
return $ PmResult {
- pmresultProvenance = prov
- , pmresultRedundant = map hsLMatchToLPats rs
- , pmresultUncovered = UncoveredPatterns us
+ pmresultRedundant = map hsLMatchToLPats rs
+ , pmresultUncovered = UncoveredPatterns us'
, pmresultInaccessible = map hsLMatchToLPats ds }
where
go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
- -> PmM (Provenance
- , [LMatch GhcTc (LHsExpr GhcTc)]
+ -> PmM ( [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)
+ fam_insts <- dsGetFamInstEnvs
+ (clause, guards) <- translateMatch fam_insts m
+ r@(PartialResult cs missing' ds)
<- runMany (pmcheckI clause guards) 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
@@ -463,7 +393,7 @@ checkEmptyCase' var = do
pure $ fmap (ValVec [va]) mb_sat
return $ if null missing_m
then emptyPmResult
- else PmResult FromBuiltin [] (UncoveredPatterns missing_m) []
+ else PmResult [] (UncoveredPatterns missing_m) []
-- | Returns 'True' if the argument 'Type' is a fully saturated application of
-- a closed type constructor.
@@ -514,7 +444,7 @@ pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> 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
+ = do (_, mb_typ') <- 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
@@ -577,8 +507,8 @@ pmTopNormaliseType_maybe env ty_cs typ
-- for why this is done.)
pmInitialTmTyCs :: PmM Delta
pmInitialTmTyCs = do
- ty_cs <- liftD getDictsDs
- tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
+ ty_cs <- getDictsDs
+ tm_cs <- map toComplex . bagToList <$> getTmCsDs
sat_ty <- tyOracle ty_cs
let initTyCs = if sat_ty then ty_cs else emptyBag
initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -669,12 +599,40 @@ tmTyCsAreSatisfiable
, delta_tm_cs = term_cs }
_unsat -> Nothing
+-- | This weeds out patterns with 'PmNCon's where at least one COMPLETE set is
+-- rendered vacuous by equality constraints.
+normaliseUncovered :: Uncovered -> PmM Uncovered
+normaliseUncovered us = do
+ let allM p = foldM (\b a -> if b then p a else pure False) True
+ anyM p = foldM (\b a -> if b then pure True else p a) False
+ valvec_inhabited p (ValVec vva delta) = allM (valabs_inhabited (p delta)) vva
+ valabs_inhabited p v = case v :: ValAbs of
+ -- TODO: There's no easy way to call allCompleteMatches only from
+ -- knowing x's idType. Maybe this doesn't matter.
+ -- PmVar x -> var_inh (p x) []
+ PmNCon x grps ncons -> var_inh (p x) grps ncons
+ _ -> pure True
+ var_inh p groups ncons =
+ allM (anyM p . filter (`notElem` ncons)) groups
+
+ -- We'll first do a cheap sweep without consulting the oracles
+ let cheap_inh_test _ _ _ = pure True
+ us1 <- filterM (valvec_inhabited cheap_inh_test) us
+ -- Then we'll do another pass trying to weed out the rest with (in)equalities
+ let actual_inh_test delta x con = do
+ ic <- mkOneConFull x con
+ tracePm "nrm" (ppr con <+> ppr x <+> ppr (delta_tm_cs delta))
+ isJust <$> pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+ us2 <- filterM (valvec_inhabited actual_inh_test) us1
+ tracePm "normaliseUncovered" (vcat (map pprValVecDebug us2))
+ pure us2
+
-- | 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
+ fam_insts <- dsGetFamInstEnvs
let definitely_inhabited =
definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
@@ -831,7 +789,7 @@ equalities (such as i ~ Int) that may be in scope.
inhabitationCandidates :: Bag EvVar -> Type
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates ty_cs ty = do
- fam_insts <- liftD dsGetFamInstEnvs
+ fam_insts <- 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
@@ -855,7 +813,7 @@ inhabitationCandidates ty_cs ty = do
| tc `elem` trivially_inhabited
-> case dcs of
[] -> return (Left src_ty)
- (_:_) -> do var <- liftD $ mkPmId core_ty
+ (_:_) -> do var <- mkPmId core_ty
let va = build_tm (PmVar var) dcs
return $ Right (tc, [InhabitationCandidate
{ ic_val_abs = va, ic_tm_ct = mkIdEq var
@@ -865,7 +823,7 @@ inhabitationCandidates ty_cs ty = do
-- 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
+ -> do
var <- mkPmId core_ty -- it would be wrong to unify x
alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
return $ Right
@@ -931,7 +889,7 @@ truePattern = nullaryConPattern (RealDataCon trueDataCon)
{-# INLINE truePattern #-}
-- | Generate a `canFail` pattern vector of a specific type
-mkCanFailPmPat :: Type -> DsM PatVec
+mkCanFailPmPat :: Type -> PmM PatVec
mkCanFailPmPat ty = do
var <- mkPmVar ty
return [var, PmFake]
@@ -966,7 +924,7 @@ mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
-- -----------------------------------------------------------------------
-- * Transform (Pat Id) into of (PmPat Id)
-translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
+translatePat :: FamInstEnvs -> Pat GhcTc -> PmM PatVec
translatePat fam_insts pat = case pat of
WildPat ty -> mkPmVars [ty]
VarPat _ id -> return [PmVar (unLoc id)]
@@ -1178,12 +1136,12 @@ from translation in pattern matcher.
-- | 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]
+translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> PmM [PatVec]
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 -> PmM 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)
@@ -1239,11 +1197,12 @@ translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
-- Translate a single match
translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
- -> DsM (PatVec,[PatVec])
+ -> PmM (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]
@@ -1258,11 +1217,11 @@ translateMatch _ _ = panic "translateMatch"
-- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
-- | Translate a list of guard statements to a pattern vector
-translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
+translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> PmM PatVec
translateGuards fam_insts guards = do
all_guards <- concat <$> mapM (translateGuard fam_insts) guards
let
- shouldKeep :: Pattern -> DsM Bool
+ shouldKeep :: Pattern -> PmM Bool
shouldKeep p
| PmVar {} <- p = pure True
| PmCon {} <- p = (&&)
@@ -1287,7 +1246,7 @@ translateGuards fam_insts guards = do
pure (PmFake : kept)
-- | Check whether a pattern can fail to match
-cantFailPattern :: Pattern -> DsM Bool
+cantFailPattern :: Pattern -> PmM 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
@@ -1295,7 +1254,7 @@ cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
cantFailPattern _ = pure False
-- | Translate a guard statement to Pattern
-translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
+translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> PmM PatVec
translateGuard fam_insts guard = case guard of
BodyStmt _ e _ _ -> translateBoolGuard e
LetStmt _ binds -> translateLet (unLoc binds)
@@ -1308,18 +1267,18 @@ translateGuard fam_insts guard = case guard of
XStmtLR {} -> panic "translateGuard RecStmt"
-- | Translate let-bindings
-translateLet :: HsLocalBinds GhcTc -> DsM PatVec
+translateLet :: HsLocalBinds GhcTc -> PmM PatVec
translateLet _binds = return []
-- | Translate a pattern guard
-translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
+translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> PmM PatVec
translateBind fam_insts (dL->L _ p) e = do
ps <- translatePat fam_insts p
g <- mkGuard ps (unLoc e)
return [g]
-- | Translate a boolean guard
-translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
+translateBoolGuard :: LHsExpr GhcTc -> PmM PatVec
translateBoolGuard e
| isJust (isTrueLHsExpr e) = return []
-- The formal thing to do would be to generate (True <- True)
@@ -1420,10 +1379,17 @@ efficiently, which gave rise to #11276. The original approach translated
pat |> co ===> x (pat <- (e |> 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 at . 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.
%************************************************************************
%* *
@@ -1440,6 +1406,7 @@ families is not really efficient.
pmPatType :: PmPat p -> Type
pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
= conLikeResTy con tys
+pmPatType (PmNCon { pm_con_id = x }) = idType x
pmPatType (PmVar { pm_var_id = x }) = idType x
pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
pmPatType (PmNLit { pm_lit_id = x }) = idType x
@@ -1470,10 +1437,13 @@ 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
------
+* Handling of uninhabited fields like `!Void`.
+ See Note [Strict argument type constraints]
+* Efficient handling of literal splitting, large enumerations and accurate
+ redundancy warnings for `COMPLETE` groups. See Note [PmNLit and PmNCon]
+Note [Strict argument type constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the ConVar case of clause processing, each conlike K traditionally
generates two different forms of constraints:
@@ -1593,8 +1563,43 @@ intuition formal, we say that a type is definitely inhabitable (DI) if:
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`
+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.
+
+Note [PmNLit and PmNCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+TLDR:
+* 'PmNLit' is an efficient encoding of literals we already matched on.
+ Important for checking redundancy without blowing up the term oracle.
+* 'PmNCon' is an efficient encoding of all constructors we already matched on.
+ Important for proper redundancy and completeness checks while being more
+ efficient than the `ConVar` split in GADTs Meet Their Match.
+
+GADTs Meet Their Match handled literals by desugaring to guard expressions,
+effectively encoding the knowledge in the term oracle. As it turned out, this
+doesn't scale (#11303, cf. Note [Literals in PmPat]), so we adopted an approach
+that encodes negative information about literals as a 'PmNLit', which encodes
+literal values the carried variable may no longer take on.
+
+The counterpart for constructor values is 'PmNCon', where we associate
+with a variable the topmost 'ConLike's it surely can't be. This is in contrast
+to GADTs Meet Their Match, where instead the `ConVar` case would split the value
+vector abstraction on all possible constructors from a `COMPLETE` group.
+In fact, we used to do just that, but committing to a particular `COMPLETE`
+group in `ConVar`, even nondeterministically, led to misleading redundancy
+warnings (#13363).
+Apart from that, splitting on huge enumerations in the presence of a catch-all
+case is a huge waste of resources.
+
+Note that since we have pattern guards, the term oracle must also be able to
+cope with negative equations involving literals and constructors, cf.
+Note [Refutable shapes] in TmOracle. Since we don't want to put too much strain
+on the term oracle with repeated coverage checks against all `COMPLETE` groups,
+we only do so once at the end in 'normaliseUncovered'.
+
+Peter Sestoft was probably the first to describe positive and negative
+information about terms in this manner in ML Pattern Match Compilation and
+Partial Evaluation.
-}
instance Outputable InhabitationCandidate where
@@ -1609,7 +1614,7 @@ instance Outputable InhabitationCandidate where
-- | Generate an 'InhabitationCandidate' for a given conlike (generate
-- fresh variables of the appropriate type for arguments)
-mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
+mkOneConFull :: Id -> ConLike -> PmM InhabitationCandidate
-- * x :: T tys, where T is an algebraic data type
-- NB: in the case of a data family, T is the *representation* TyCon
-- e.g. data instance T (a,b) = T1 a b
@@ -1663,23 +1668,18 @@ mkOneConFull x con = do
-- * More smart constructors and fresh variable generation
-- | Create a guard pattern
-mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern
+mkGuard :: PatVec -> HsExpr GhcTc -> PmM Pattern
mkGuard pv e = do
res <- allM cantFailPattern pv
let expr = hsExprToPmExpr e
- tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
+ tracePm "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: `(False ~ (x ~ lit))`
-mkNegEq :: Id -> PmLit -> ComplexEq
-mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
-{-# INLINE mkNegEq #-}
-
--- | Create a term equality of the form: `(x ~ lit)`
-mkPosEq :: Id -> PmLit -> ComplexEq
-mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
+-- | Create a term equality of the form: `(x ~ e)`
+mkPosEq :: Id -> PmExpr -> ComplexEq
+mkPosEq x e = (PmExprVar (idName x), e)
{-# INLINE mkPosEq #-}
-- | Create a term equality of the form: `(x ~ x)`
@@ -1690,17 +1690,17 @@ mkIdEq x = (PmExprVar name, PmExprVar name)
{-# INLINE mkIdEq #-}
-- | Generate a variable pattern of a given type
-mkPmVar :: Type -> DsM (PmPat p)
+mkPmVar :: Type -> PmM (PmPat p)
mkPmVar ty = PmVar <$> mkPmId ty
{-# INLINE mkPmVar #-}
-- | Generate many variable patterns, given a list of types
-mkPmVars :: [Type] -> DsM PatVec
+mkPmVars :: [Type] -> PmM PatVec
mkPmVars tys = mapM mkPmVar tys
{-# INLINE mkPmVars #-}
-- | Generate a fresh `Id` of a given type
-mkPmId :: Type -> DsM Id
+mkPmId :: Type -> PmM Id
mkPmId ty = getUniqueM >>= \unique ->
let occname = mkVarOccFS $ fsLit "$pm"
name = mkInternalName unique occname noSrcSpan
@@ -1709,7 +1709,7 @@ mkPmId ty = getUniqueM >>= \unique ->
-- | 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 -> PmM (Pattern, LHsExpr GhcTc)
mkPmId2Forms ty = do
x <- mkPmId ty
return (PmVar x, noLoc (HsVar noExt (noLoc x)))
@@ -1721,6 +1721,7 @@ mkPmId2Forms ty = do
vaToPmExpr :: ValAbs -> PmExpr
vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
= PmExprCon c (map vaToPmExpr ps)
+vaToPmExpr (PmNCon { pm_con_id = x }) = PmExprVar (idName x)
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)
@@ -1748,9 +1749,9 @@ coercePmPat PmFake = [] -- drop the guards
-- | Check whether a 'ConLike' 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 :: ConLike -> [Type] -> PmM Bool
singleMatchConstructor cl tys =
- any (isSingleton . snd) <$> allCompleteMatches cl tys
+ any isSingleton <$> allCompleteMatches cl tys
{-
Note [Single match constructors]
@@ -1785,20 +1786,18 @@ translation step. See #15753 for why this yields surprising results.
-- 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 :: ConLike -> [Type] -> DsM [[ConLike]]
allCompleteMatches cl tys = do
let fam = case cl of
RealDataCon dc ->
- [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
+ [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 fams cm = mapM dsLookupConLike (completeMatchConLikes cm)
+ from_pragma <- filter (isValidCompleteMatch ty) <$> mapM fams pragmas
let final_groups = fam ++ from_pragma
return final_groups
where
@@ -1890,8 +1889,7 @@ nameType name ty = do
-- | Check whether a set of type constraints is satisfiable.
tyOracle :: Bag EvVar -> PmM Bool
tyOracle evs
- = liftD $
- do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
+ = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
; case res of
Just sat -> return sat
Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
@@ -1973,7 +1971,7 @@ mkInitialUncovered vars = do
-- limit is not exceeded and call `pmcheck`
pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI ps guards vva = do
- n <- liftD incrCheckPmIterDs
+ n <- incrCheckPmIterDs
tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
$$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
$$ pprValVecDebug vva)
@@ -1985,7 +1983,7 @@ pmcheckI ps guards vva = do
-- | 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 gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva
{-# INLINE pmcheckGuardsI #-}
-- | Increase the counter for elapsed algorithm iterations, check that the
@@ -1993,7 +1991,7 @@ pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
-> PmM PartialResult
pmcheckHdI p ps guards va vva = do
- n <- liftD incrCheckPmIterDs
+ n <- incrCheckPmIterDs
tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
$$ pprPatVec ps
$$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
@@ -2023,10 +2021,13 @@ pmcheck (PmFake : 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)
+ tracePm "PmGrd: pmPatType" (hcat [ppr p, ppr (pmPatType p)])
+ y <- 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')
+ pr <- pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
+ us <- normaliseUncovered (presultUncovered pr)
+ pure $ utail pr { presultUncovered = us }
pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
@@ -2038,10 +2039,9 @@ pmcheck (p:ps) guards (ValVec (va:vva) delta)
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)
+ (PartialResult cs vsa ds) <- pmcheckI gv [] vva
+ (PartialResult css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
+ return $ PartialResult (cs `mappend` css)
vsas
(ds `mappend` dss)
@@ -2077,7 +2077,7 @@ pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
| otherwise = Just <$> to_evvar tv1 tv2
evvars <- (listToBag . catMaybes) <$>
ASSERT(ex_tvs1 `equalLength` ex_tvs2)
- liftD (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
+ (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')
@@ -2089,44 +2089,53 @@ pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
False -> return $ ucon va (usimple [vva])
-- 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) 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
+pmcheckHd p at PmCon{} ps guards (PmVar x) vva@(ValVec _ delta) = do
+ groups <- allCompleteMatches (pm_con_con p) (pm_con_arg_tys p)
+ force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
+ pmcheckHd p ps guards (PmNCon x groups []) vva
+
+-- ConNCon
+pmcheckHd p at PmCon{} ps guards va at PmNCon{} (ValVec vva delta) = do
+ -- Split the value vector into two value vectors: One representing the current
+ -- constructor, the other representing everything but the current constructor
+ -- (and the already known impossible constructors).
+ let con = pm_con_con p
+ let x = pm_con_id va
+ let grps = pm_con_grps va
+ let ncons = pm_con_not va
+
+ -- For the value vector of the current constructor, we directly recurse into
+ -- checking the the current case, so we get back a PartialResult
+ ic <- mkOneConFull x con
+ pr_con <- fmap (fromMaybe mempty) $ runMaybeT $ do
+ guard (con `notElem` ncons)
+ delta' <- MaybeT $ pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+ lift $ tracePm "success" (ppr (delta_tm_cs delta))
+ lift $ pmcheckHdI p ps guards (ic_val_abs ic) (ValVec vva delta')
+
+ let ncons' = con : ncons
+ let us_incomplete
+ | let nalt = PmAltConLike (pm_con_con p) (pm_con_arg_tys p)
+ , Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x nalt
+ = [ValVec (PmNCon x grps ncons' : vva) (delta { delta_tm_cs = tm_state })]
+ | otherwise = []
+ us_incomplete' <- normaliseUncovered us_incomplete
+ tracePm "ConNCon" (vcat [ppr p, ppr x, ppr ncons', ppr pr_con, ppr us_incomplete, ppr us_incomplete'])
+
+ -- Combine both into a single PartialResult
+ let pr_combined = mkUnion pr_con (usimple us_incomplete')
+ pure pr_combined
-- LitVar
-pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
+pmcheckHd p at PmLit{} ps guards (PmVar x) vva@(ValVec _ 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
- us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
- = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
- | otherwise = []
-
- non_matched = usimple us
+ pmcheckHd p ps guards (PmNLit x []) vva
-- 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)
+ , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x (PmExprLit 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
@@ -2136,7 +2145,8 @@ pmcheckHd (p@(PmLit l)) ps guards
(ValVec vva (delta { delta_tm_cs = tm_state }))
| otherwise = return non_matched
where
- us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
+ -- 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 = []
@@ -2151,7 +2161,7 @@ pmcheckHd (p@(PmLit l)) ps guards
-- LitCon
pmcheckHd p at PmLit{} ps guards va at PmCon{} (ValVec vva delta)
- = do y <- liftD $ mkPmId (pmPatType va)
+ = do y <- 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
@@ -2162,7 +2172,7 @@ pmcheckHd p at PmLit{} ps guards va at PmCon{} (ValVec vva delta)
-- ConLit
pmcheckHd p at PmCon{} ps guards (PmLit l) (ValVec vva delta)
- = do y <- liftD $ mkPmId (pmPatType p)
+ = do y <- 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.
@@ -2174,6 +2184,10 @@ pmcheckHd p at PmCon{} ps guards (PmLit l) (ValVec vva delta)
pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
= pmcheckHdI p ps guards (PmVar x) vva
+-- LitNCon
+pmcheckHd (p@(PmLit {})) ps guards (PmNCon { pm_con_id = x }) vva
+ = pmcheckHdI p ps guards (PmVar x) vva
+
-- Impossible: handled by pmcheck
pmcheckHd PmFake _ _ _ _ = panic "pmcheckHd: Fake"
pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
@@ -2357,9 +2371,6 @@ 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 }
-
-- ----------------------------------------------------------------------------
-- * Propagation of term constraints inwards when checking nested matches
@@ -2367,7 +2378,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 `addTmCsDs' 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'
@@ -2478,27 +2489,21 @@ isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
instance Outputable ValVec where
ppr (ValVec vva delta)
- = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
- vector = substInValAbs subst vva
- in ppr_uncovered (vector, residual_eqs)
+ = 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 :: PmVarEnv -> [ValAbs] -> [PmExpr]
substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
--- | Wrap up the term oracle's state once solving is complete. Drop any
--- information about unhandled constraints (involving HsExprs) and flatten
--- (height 1) the substitution.
-wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
-wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
-
-- | 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)
@@ -2515,8 +2520,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
UncoveredPatterns candidates -> pprEqns candidates
where
PmResult
- { pmresultProvenance = prov
- , pmresultRedundant = redundant
+ { pmresultRedundant = redundant
, pmresultUncovered = uncovered
, pmresultInaccessible = inaccessible } = pm_result
@@ -2527,15 +2531,14 @@ 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)
- pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
+ pprEqn q txt = pprContext True ctx (text txt) $ \f ->
+ f (pprPats kind (map unLoc q))
-- Print several clauses (for uncovered clauses)
- pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+ pprEqns qs = pprContext False ctx (text "are non-exhaustive") $ \_ ->
case qs of -- See #11245
[ValVec [] _]
-> text "Guards do not cover entire pattern space"
@@ -2546,7 +2549,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
-- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
-- which we only know the type and have no inhabitants at hand)
- warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
+ warnEmptyCase ty = pprContext False ctx (text "are non-exhaustive") $ \_ ->
hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
{- Note [Inaccessible warnings for record updates]
@@ -2618,8 +2621,8 @@ exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete pat
-- incomplete
-- True <==> singular
-pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
-pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
+pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
+pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
= vcat [text txt <+> msg,
sep [ text "In" <+> ppr_match <> char ':'
, nest 4 (rest_of_msg_fun pref)]]
@@ -2633,26 +2636,10 @@ pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
-> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
_ -> (pprMatchContext kind, \ pp -> pp)
-ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
-ppr_pats kind pats
+pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
+pprPats kind pats
= sep [sep (map ppr pats), matchSeparator kind, text "..."]
-ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
-ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
-
-ppr_constraint :: (SDoc,[PmLit]) -> SDoc
-ppr_constraint (var, lits) = var <+> text "is not one of"
- <+> braces (pprWithCommas ppr lits)
-
-ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
-ppr_uncovered (expr_vec, complex)
- | null cs = fsep vec -- there are no literal constraints
- | otherwise = hang (fsep vec) 4 $
- text "where" <+> vcat (map ppr_constraint cs)
- where
- sdoc_vec = mapM pprPmExprWithParens expr_vec
- (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
-
{- Note [Representation of Term Equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the paper, term constraints always take the form (x ~ e). Of course, a more
@@ -2717,11 +2704,7 @@ involved.
-- Debugging Infrastructre
tracePm :: String -> SDoc -> PmM ()
-tracePm herald doc = liftD $ tracePmD herald doc
-
-
-tracePmD :: String -> SDoc -> DsM ()
-tracePmD herald doc = do
+tracePm herald doc = do
dflags <- getDynFlags
printer <- mkPrintUnqualifiedDs
liftIO $ dumpIfSet_dyn_printer printer dflags
@@ -2731,6 +2714,8 @@ tracePmD herald doc = do
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 (PmNCon x _ sets)
+ = hsep [text "PmNCon", ppr x, ppr sets]
pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
@@ -2751,3 +2736,5 @@ pprValAbs ps = hang (text "ValAbs:") 2
pprValVecDebug :: ValVec -> SDoc
pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
parens (pprValAbs vas)
+ $$ (ppr (delta_tm_cs _d))
+ -- $$ (ppr (delta_ty_cs _d))
=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -8,10 +8,9 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE ViewPatterns #-}
module PmExpr (
- PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
- truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
- lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
- pprPmExprWithParens, runPmPprM
+ PmExpr(..), PmLit(..), PmAltCon(..), SimpleEq, ComplexEq, toComplex,
+ eqPmLit, pmExprToAlt, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
+ substComplexEq
) where
#include "HsVersions.h"
@@ -23,19 +22,14 @@ import FastString (FastString, unpackFS)
import HsSyn
import Id
import Name
-import NameSet
import DataCon
import ConLike
-import TcType (isStringTy)
+import TcType (Type, isStringTy)
import TysWiredIn
import Outputable
import Util
import SrcLoc
-import Data.Maybe (mapMaybe)
-import Data.List (groupBy, sortBy, nubBy)
-import Control.Monad.Trans.State.Lazy
-
{-
%************************************************************************
%* *
@@ -61,7 +55,6 @@ refer to variables that are otherwise substituted away.
data PmExpr = PmExprVar Name
| PmExprCon ConLike [PmExpr]
| PmExprLit PmLit
- | PmExprEq PmExpr PmExpr -- Syntactic equality
| PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr]
@@ -79,6 +72,30 @@ 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 'ConLike' or 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'.
+data PmAltCon = PmAltConLike ConLike [Type]
+ -- ^ The types are the argument types of the 'ConLike' application
+ | PmAltLit PmLit
+
+-- | This instance won't compare the argument types of the 'ConLike', as we
+-- carry them for recovering COMPLETE match groups only. The 'PmRefutEnv' below
+-- should never have different 'PmAltConLike's with the same 'ConLike' for the
+-- same variable. See Note [Refutable shapes] in TmOracle.
+instance Eq PmAltCon where
+ PmAltConLike cl1 _ == PmAltConLike cl2 _ = cl1 == cl2
+ PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+ _ == _ = False
+
+pmExprToAlt :: PmExpr -> Maybe PmAltCon
+-- Note how this deliberately chooses bogus argument types for PmAltConLike.
+-- This is only safe for doing lookup in a 'PmRefutEnv'!
+pmExprToAlt (PmExprCon cl _) = Just (PmAltConLike cl [])
+pmExprToAlt (PmExprLit l) = Just (PmAltLit l)
+pmExprToAlt _ = Nothing
+
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
@@ -145,9 +162,6 @@ impact of this is the following:
appearance of the warnings and is, in practice safe.
-}
-nubPmLit :: [PmLit] -> [PmLit]
-nubPmLit = nubBy eqPmLit
-
-- | Term equalities
type SimpleEq = (Id, PmExpr) -- We always use this orientation
type ComplexEq = (PmExpr, PmExpr)
@@ -156,14 +170,6 @@ type ComplexEq = (PmExpr, PmExpr)
toComplex :: SimpleEq -> ComplexEq
toComplex (x,e) = (PmExprVar (idName x), e)
--- | Expression `True'
-truePmExpr :: PmExpr
-truePmExpr = mkPmExprData trueDataCon []
-
--- | Expression `False'
-falsePmExpr :: PmExpr
-falsePmExpr = mkPmExprData falseDataCon []
-
-- ----------------------------------------------------------------------------
-- ** Predicates on PmExpr
@@ -172,38 +178,6 @@ isNotPmExprOther :: PmExpr -> Bool
isNotPmExprOther (PmExprOther _) = False
isNotPmExprOther _expr = True
--- | Check whether a literal is negated
-isNegatedPmLit :: PmLit -> Bool
-isNegatedPmLit (PmOLit b _) = b
-isNegatedPmLit _other_lit = False
-
--- | Check whether a PmExpr is syntactically equal to term `True'.
-isTruePmExpr :: PmExpr -> Bool
-isTruePmExpr (PmExprCon c []) = c == RealDataCon trueDataCon
-isTruePmExpr _other_expr = False
-
--- | Check whether a PmExpr is syntactically equal to term `False'.
-isFalsePmExpr :: PmExpr -> Bool
-isFalsePmExpr (PmExprCon c []) = c == RealDataCon falseDataCon
-isFalsePmExpr _other_expr = False
-
--- | Check whether a PmExpr is syntactically e
-isNilPmExpr :: PmExpr -> Bool
-isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
-isNilPmExpr _other_expr = False
-
--- | Check whether a PmExpr is syntactically equal to (x == y).
--- Since (==) is overloaded and can have an arbitrary implementation, we use
--- the PmExprEq constructor to represent only equalities with non-overloaded
--- literals where it coincides with a syntactic equality check.
-isPmExprEq :: PmExpr -> Maybe (PmExpr, PmExpr)
-isPmExprEq (PmExprEq e1 e2) = Just (e1,e2)
-isPmExprEq _other_expr = Nothing
-
--- | Check if a DataCon is (:).
-isConsDataCon :: DataCon -> Bool
-isConsDataCon con = consDataCon == con
-
-- ----------------------------------------------------------------------------
-- ** Substitution in PmExpr
@@ -216,9 +190,6 @@ substPmExpr x e1 e =
| otherwise -> (e, False)
PmExprCon c ps -> let (ps', bs) = mapAndUnzip (substPmExpr x e1) ps
in (PmExprCon c ps', or bs)
- PmExprEq ex ey -> let (ex', bx) = substPmExpr x e1 ex
- (ey', by) = substPmExpr x e1 ey
- in (PmExprEq ex' ey', bx || by)
_other_expr -> (e, False) -- The rest are terminals (We silently ignore
-- Other). See Note [PmExprOther in PmExpr]
@@ -312,155 +283,26 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s))
%************************************************************************
-}
-{- 1. Literals
-~~~~~~~~~~~~~~
-Starting with a function definition like:
-
- f :: Int -> Bool
- f 5 = True
- f 6 = True
-
-The uncovered set looks like:
- { var |> False == (var == 5), False == (var == 6) }
-
-Yet, we would like to print this nicely as follows:
- x , where x not one of {5,6}
-
-Function `filterComplex' takes the set of residual constraints and packs
-together the negative constraints that refer to the same variable so we can do
-just this. Since these variables will be shown to the programmer, we also give
-them better names (t1, t2, ..), hence the SDoc in PmNegLitCt.
-
-2. Residual Constraints
-~~~~~~~~~~~~~~~~~~~~~~~
-Unhandled constraints that refer to HsExpr are typically ignored by the solver
-(it does not even substitute in HsExpr so they are even printed as wildcards).
-Additionally, the oracle returns a substitution if it succeeds so we apply this
-substitution to the vectors before printing them out (see function `pprOne' in
-Check.hs) to be more precice.
--}
-
--- -----------------------------------------------------------------------------
--- ** Transform residual constraints in appropriate form for pretty printing
-
-type PmNegLitCt = (Name, (SDoc, [PmLit]))
-
-filterComplex :: [ComplexEq] -> [PmNegLitCt]
-filterComplex = zipWith rename nameList . map mkGroup
- . groupBy name . sortBy order . mapMaybe isNegLitCs
- where
- order x y = compare (fst x) (fst y)
- name x y = fst x == fst y
- mkGroup l = (fst (head l), nubPmLit $ map snd l)
- rename new (old, lits) = (old, (new, lits))
-
- isNegLitCs (e1,e2)
- | isFalsePmExpr e1, Just (x,y) <- isPmExprEq e2 = isNegLitCs' x y
- | isFalsePmExpr e2, Just (x,y) <- isPmExprEq e1 = isNegLitCs' x y
- | otherwise = Nothing
-
- isNegLitCs' (PmExprVar x) (PmExprLit l) = Just (x, l)
- isNegLitCs' (PmExprLit l) (PmExprVar x) = Just (x, l)
- isNegLitCs' _ _ = Nothing
-
- -- 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)..] ]
-
--- ----------------------------------------------------------------------------
-
-runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])])
-runPmPprM m lit_env = (result, mapMaybe is_used lit_env)
- where
- (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
-
- is_used (x,(name, lits))
- | elemNameSet x used = Just (name, lits)
- | otherwise = Nothing
-
-type PmPprM a = State ([PmNegLitCt], NameSet) a
--- (the first part of the state is read only. make it a reader?)
-
-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 lookup x negated of
- Just (new, _) -> Just new
- Nothing -> Nothing
-
--- | Pretty print a pmexpr, 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 (PmExprEq _ _) = return underscore -- don't show
-pprPmExpr (PmExprOther _) = return underscore -- don't show
-
-needsParens :: PmExpr -> Bool
-needsParens (PmExprVar {}) = False
-needsParens (PmExprLit l) = isNegatedPmLit l
-needsParens (PmExprEq {}) = False -- will become a wildcard
-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
- | conLikeIsInfix cl = case args of
- [x, y] -> do x' <- pprPmExprWithParens x
- y' <- pprPmExprWithParens y
- return (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'))
-
instance Outputable PmLit where
ppr (PmSLit l) = pmPprHsLit l
ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
--- not really useful for pmexprs per se
instance Outputable PmExpr where
- ppr e = fst $ runPmPprM (pprPmExpr e) []
+ ppr = go (0 :: Int)
+ 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))
+
+instance Outputable PmAltCon where
+ ppr (PmAltConLike cl tys) = ppr cl <+> char '@' <> ppr tys
+ ppr (PmAltLit l) = ppr l
=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -0,0 +1,192 @@
+{-# LANGUAGE CPP #-}
+
+-- | Provides factilities for pretty-printing 'PmExpr's in a way approriate for
+-- user facing pattern match warnings.
+module PmPpr (
+ pprUncovered
+ ) where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import Name
+import NameEnv
+import NameSet
+import UniqDFM
+import UniqSet
+import ConLike
+import DataCon
+import TysWiredIn
+import Outputable
+import Control.Monad.Trans.State.Strict
+import Maybes
+import Util
+
+import TmOracle
+
+-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
+-- components and refutable shapes associated to any mentioned variables.
+--
+-- Example for @([Just p, q], [p :-> [3,4], q :-> [0,5]]):
+--
+-- @
+-- (Just p) q
+-- 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)
+ where
+ sdoc_vec = mapM pprPmExprWithParens expr_vec
+ (vec,cs) = runPmPpr sdoc_vec (prettifyRefuts refuts)
+
+-- | Output refutable shapes of a variable in the form of @var is not one of {2,
+-- Nothing, 3}@.
+pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
+pprRefutableShapes (var, alts)
+ = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts)
+ where
+ ppr_alt (PmAltLit lit) = ppr lit
+ ppr_alt (PmAltConLike cl _) = ppr cl
+
+{- 1. Literals
+~~~~~~~~~~~~~~
+Starting with a function definition like:
+
+ f :: Int -> Bool
+ f 5 = True
+ f 6 = True
+
+The uncovered set looks like:
+ { var |> var /= 5, var /= 6 }
+
+Yet, we would like to print this nicely as follows:
+ x , where x not one of {5,6}
+
+Since these variables will be shown to the programmer, we give them better names
+(t1, t2, ..) in 'prettifyRefuts', hence the SDoc in 'PrettyPmRefutEnv'.
+
+2. Residual Constraints
+~~~~~~~~~~~~~~~~~~~~~~~
+Unhandled constraints that refer to HsExpr are typically ignored by the solver
+(it does not even substitute in HsExpr so they are even printed as wildcards).
+Additionally, the oracle returns a substitution if it succeeds so we apply this
+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
+ 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
+-- 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
+ | conLikeIsInfix cl = case args of
+ [x, y] -> do x' <- pprPmExprWithParens x
+ y' <- pprPmExprWithParens y
+ return (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
=====================================
compiler/deSugar/TmOracle.hs
=====================================
@@ -1,20 +1,24 @@
{-
Author: George Karachalias <george.karachalias at cs.kuleuven.be>
-
-The term equality oracle. The main export of the module is function `tmOracle'.
-}
{-# 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(..), SimpleEq, ComplexEq, PmVarEnv, falsePmExpr,
- eqPmLit, filterComplex, isNotPmExprOther, runPmPprM, lhsExprToPmExpr,
- hsExprToPmExpr, pprPmExprWithParens,
+ PmExpr(..), PmLit(..), PmAltCon(..), SimpleEq, ComplexEq, PmVarEnv,
+ PmRefutEnv, eqPmLit, pmExprToAlt, isNotPmExprOther, lhsExprToPmExpr,
+ hsExprToPmExpr,
-- the term oracle
- tmOracle, TmState, initialTmState, solveOneEq, extendSubst, canDiverge,
+ tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq, extendSubst, canDiverge,
+ addSolveRefutableAltCon, lookupRefutableAltCons,
-- misc.
toComplex, exprDeepLookup, pmLitType, flattenPmVarEnv
@@ -28,15 +32,18 @@ import PmExpr
import Id
import Name
+import NameEnv
+import UniqFM
+import UniqDFM
import Type
import HsLit
import TcHsSyn
import MonadUtils
+import ListSetOps (insertNoDup, unionLists)
import Util
+import Maybes
import Outputable
-import NameEnv
-
{-
%************************************************************************
%* *
@@ -48,23 +55,87 @@ import NameEnv
-- | The type of substitutions.
type PmVarEnv = NameEnv PmExpr
--- | The environment of the oracle contains
--- 1. A Bool (are there any constraints we cannot handle? (PmExprOther)).
--- 2. A substitution we extend with every step and return as a result.
-type TmOracleEnv = (Bool, PmVarEnv)
+-- | An environment assigning shapes to variables that immediately lead to a
+-- refutation. So, if this maps @x :-> [Just]@, then trying to solve a
+-- 'ComplexEq' like @x ~ Just False@ 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 'PmVarEnv', 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 we know,
+-- giving special treatment to constraints of the form "x is @True@" ('tm_pos')
+-- and "x is not @5@" ('tm_neg').
+data TmState = TmS
+ { tm_facts :: ![ComplexEq]
+ -- ^ Complex equalities we may assume to hold. We have not (yet) brought them
+ -- into a form leading to a contradiction or a 'SimpleEq'. Otherwise, we would
+ -- store the 'SimpleEq' as a solution in the 'tm_pos' env, where it could be
+ -- used to simplify other equations. All 'ComplexEq's are fully substituted
+ -- according to (i.e., fixed-points under) 'tm_pos'.
+ , tm_pos :: !PmVarEnv
+ -- ^ A substitution with solutions we extend with every step and return as a
+ -- result. Think of it as any 'ComplexEq' from 'tm_facts' we managed to
+ -- bring into the form of a 'SimpleEq'.
+ -- Contrary to 'tm_facts', 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.
+ , tm_neg :: !PmRefutEnv
+ -- ^ maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely
+ -- 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 at . Should we later solve @x@ to a variable
+ -- @y@ ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into
+ -- those of @y at .
+ }
+
+instance Outputable TmState where
+ ppr state = braces (fsep (punctuate comma (facts ++ pos ++ neg)))
+ where
+ facts = map pos_eq (tm_facts state)
+ 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. Drop any
+-- information about non-simple constraints and flatten (height 1) the
+-- substitution.
+wrapUpTmState :: TmState -> (PmVarEnv, PmRefutEnv)
+wrapUpTmState solver_state
+ = (flattenPmVarEnv (tm_pos solver_state), tm_neg solver_state)
+
+-- | Flatten the triangular subsitution.
+flattenPmVarEnv :: PmVarEnv -> PmVarEnv
+flattenPmVarEnv 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 (standby, (_unhandled, env))
+canDiverge x TmS{ tm_pos = pos, tm_facts = facts }
-- If the variable seems not evaluated, there is a possibility for
- -- constraint x ~ BOT to be satisfiable.
- | PmExprVar y <- varDeepLookup env x -- seems not forced
+ -- 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
-- If it is involved (directly or indirectly) in any equality in the
-- worklist, we can assume that it is already indirectly evaluated,
-- as a side-effect of equality checking. If not, then we can assume
-- that the constraint is satisfiable.
- = not $ any (isForcedByEq x) standby || any (isForcedByEq y) standby
+ = not $ any (isForcedByEq x) facts || any (isForcedByEq y) facts
-- Variable x is already in WHNF so the constraint is non-satisfiable
| otherwise = False
@@ -78,27 +149,47 @@ varIn x e = case e of
PmExprVar y -> x == y
PmExprCon _ es -> any (x `varIn`) es
PmExprLit _ -> False
- PmExprEq e1 e2 -> (x `varIn` e1) || (x `varIn` e2)
PmExprOther _ -> False
--- | Flatten the DAG (Could be improved in terms of performance.).
-flattenPmVarEnv :: PmVarEnv -> PmVarEnv
-flattenPmVarEnv env = mapNameEnv (exprDeepLookup env) env
-
--- | The state of the term oracle (includes complex constraints that cannot
--- progress unless we get more information).
-type TmState = ([ComplexEq], TmOracleEnv)
-
--- | Initial state of the oracle.
-initialTmState :: TmState
-initialTmState = ([], (False, emptyNameEnv))
+-- | 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 <$> pmExprToAlt e <*> lookupDNameEnv env x
-- | Solve a complex equality (top-level).
solveOneEq :: TmState -> ComplexEq -> Maybe TmState
-solveOneEq solver_env@(_,(_,env)) complex
- = solveComplexEq solver_env -- do the actual *merging* with existing state
- $ simplifyComplexEq -- simplify as much as you can
- $ applySubstComplexEq env complex -- replace everything we already know
+solveOneEq solver_env at TmS{ tm_pos = pos } complex
+ = solveComplexEq solver_env -- do the actual *merging* with existing state
+ $ applySubstComplexEq pos complex -- replace everything we already know
+
+-- | 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 at TmS{ tm_pos = pos, tm_neg = neg } x nalt
+ = case pmExprToAlt e of
+ 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))
-- | Solve a complex equality.
-- Nothing => definitely unsatisfiable
@@ -106,10 +197,10 @@ solveOneEq solver_env@(_,(_,env)) complex
-- it to the tmstate; the result may or may not be
-- satisfiable
solveComplexEq :: TmState -> ComplexEq -> Maybe TmState
-solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
+solveComplexEq solver_state eq@(e1, e2) = {-pprTraceWith "solveComplexEq" (\mb_sat -> ppr eq $$ ppr mb_sat) $-} case eq of
-- We cannot do a thing about these cases
- (PmExprOther _,_) -> Just (standby, (True, env))
- (_,PmExprOther _) -> Just (standby, (True, env))
+ (PmExprOther _,_) -> Just solver_state
+ (_,PmExprOther _) -> Just solver_state
(PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
-- See Note [Undecidable Equality for Overloaded Literals]
@@ -119,12 +210,6 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
(PmExprCon c1 ts1, PmExprCon c2 ts2)
| c1 == c2 -> foldlM solveComplexEq solver_state (zip ts1 ts2)
| otherwise -> Nothing
- (PmExprCon _ [], PmExprEq t1 t2)
- | isTruePmExpr e1 -> solveComplexEq solver_state (t1, t2)
- | isFalsePmExpr e1 -> Just (eq:standby, (unhandled, env))
- (PmExprEq t1 t2, PmExprCon _ [])
- | isTruePmExpr e2 -> solveComplexEq solver_state (t1, t2)
- | isFalsePmExpr e2 -> Just (eq:standby, (unhandled, env))
(PmExprVar x, PmExprVar y)
| x == y -> Just solver_state
@@ -133,110 +218,68 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
(PmExprVar x, _) -> extendSubstAndSolve x e2 solver_state
(_, PmExprVar x) -> extendSubstAndSolve x e1 solver_state
- (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
-
_ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
- Just (standby, (True, env)) -- I HATE CATCH-ALLS
+ Just solver_state -- I HATE CATCH-ALLS
-- | Extend the substitution and solve the (possibly updated) constraints.
extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
-extendSubstAndSolve x e (standby, (unhandled, env))
- = foldlM solveComplexEq new_incr_state (map simplifyComplexEq changed)
+extendSubstAndSolve x e TmS{ tm_facts = facts, tm_pos = pos, tm_neg = neg }
+ | isRefutable x e' neg -- NB: e'
+ = Nothing
+ | otherwise
+ = foldlM solveComplexEq new_incr_state changed
where
-- Apply the substitution to the worklist and partition them to the ones
-- that had some progress and the rest. Then, recurse over the ones that
-- had some progress. Careful about performance:
-- See Note [Representation of Term Equalities] in deSugar/Check.hs
- (changed, unchanged) = partitionWith (substComplexEq x e) standby
- new_incr_state = (unchanged, (unhandled, extendNameEnv env x e))
+ (changed, unchanged) = partitionWith (substComplexEq x e) facts
+ new_pos = extendNameEnv pos x e
+ -- When e is a @PmExprVar y@, we have to check @y@'s solution for
+ -- refutability instead. Afterwards, we have to merge @x@'s refutable shapes
+ -- to @y@'s. Actually, e == e' because it has been fully substituted before,
+ -- but better be safe.
+ (y, e') = varDeepLookup new_pos x
+ new_neg | x == y = neg
+ | otherwise = case lookupDNameEnv neg x of
+ Nothing -> neg
+ Just nalts ->
+ alterDNameEnv (delNulls (unionLists nalts)) neg y
+ `delFromDNameEnv` x
+ new_incr_state = TmS unchanged new_pos new_neg
-- | 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 (standby, (unhandled, env))
+extendSubst y e solver_state at TmS{ tm_pos = pos }
| isNotPmExprOther simpl_e
- = (standby, (unhandled, extendNameEnv env x simpl_e))
- | otherwise = (standby, (True, env))
+ = solver_state { tm_pos = extendNameEnv pos x simpl_e }
+ | otherwise = solver_state
where
x = idName y
- simpl_e = fst $ simplifyPmExpr $ exprDeepLookup env e
-
--- | Simplify a complex equality.
-simplifyComplexEq :: ComplexEq -> ComplexEq
-simplifyComplexEq (e1, e2) = (fst $ simplifyPmExpr e1, fst $ simplifyPmExpr e2)
-
--- | Simplify an expression. The boolean indicates if there has been any
--- simplification or if the operation was a no-op.
-simplifyPmExpr :: PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyPmExpr e = case e of
- PmExprCon c ts -> case mapAndUnzip simplifyPmExpr ts of
- (ts', bs) -> (PmExprCon c ts', or bs)
- PmExprEq t1 t2 -> simplifyEqExpr t1 t2
- _other_expr -> (e, False) -- the others are terminals
-
--- | Simplify an equality expression. The equality is given in parts.
-simplifyEqExpr :: PmExpr -> PmExpr -> (PmExpr, Bool)
--- See Note [Deep equalities]
-simplifyEqExpr e1 e2 = case (e1, e2) of
- -- Varables
- (PmExprVar x, PmExprVar y)
- | x == y -> (truePmExpr, True)
-
- -- Literals
- (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
- -- See Note [Undecidable Equality for Overloaded Literals]
- True -> (truePmExpr, True)
- False -> (falsePmExpr, True)
-
- -- Can potentially be simplified
- (PmExprEq {}, _) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
- ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
- ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
- ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
- (_, PmExprEq {}) -> case (simplifyPmExpr e1, simplifyPmExpr e2) of
- ((e1', True ), (e2', _ )) -> simplifyEqExpr e1' e2'
- ((e1', _ ), (e2', True )) -> simplifyEqExpr e1' e2'
- ((e1', False), (e2', False)) -> (PmExprEq e1' e2', False) -- cannot progress
-
- -- Constructors
- (PmExprCon c1 ts1, PmExprCon c2 ts2)
- | c1 == c2 ->
- let (ts1', bs1) = mapAndUnzip simplifyPmExpr ts1
- (ts2', bs2) = mapAndUnzip simplifyPmExpr ts2
- (tss, _bss) = zipWithAndUnzip simplifyEqExpr ts1' ts2'
- worst_case = PmExprEq (PmExprCon c1 ts1') (PmExprCon c2 ts2')
- in if | not (or bs1 || or bs2) -> (worst_case, False) -- no progress
- | all isTruePmExpr tss -> (truePmExpr, True)
- | any isFalsePmExpr tss -> (falsePmExpr, True)
- | otherwise -> (worst_case, False)
- | otherwise -> (falsePmExpr, True)
-
- -- We cannot do anything about the rest..
- _other_equality -> (original, False)
-
- where
- original = PmExprEq e1 e2 -- reconstruct equality
+ simpl_e = exprDeepLookup pos e
-- | Apply an (un-flattened) substitution to a simple equality.
applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq
applySubstComplexEq env (e1,e2) = (exprDeepLookup env e1, exprDeepLookup env e2)
--- | Apply an (un-flattened) substitution to a variable.
-varDeepLookup :: PmVarEnv -> Name -> PmExpr
-varDeepLookup env x
- | Just e <- lookupNameEnv env x = exprDeepLookup env e -- go deeper
- | otherwise = PmExprVar x -- terminal
+-- | 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 :: PmVarEnv -> 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 :: PmVarEnv -> PmExpr -> PmExpr
-exprDeepLookup env (PmExprVar x) = varDeepLookup env x
+exprDeepLookup env (PmExprVar x) = snd (varDeepLookup env x)
exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
-exprDeepLookup env (PmExprEq e1 e2) = PmExprEq (exprDeepLookup env e1)
- (exprDeepLookup env e2)
exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
-- | External interface to the term oracle.
@@ -248,18 +291,57 @@ pmLitType :: PmLit -> Type -- should be in PmExpr but gives cyclic imports :(
pmLitType (PmSLit lit) = hsLitType lit
pmLitType (PmOLit _ lit) = overLitType lit
-{- Note [Deep equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Solving nested equalities is the most difficult part. The general strategy
-is the following:
+{- Note [Refutable shapes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
- * Equalities of the form (True ~ (e1 ~ e2)) are transformed to just
- (e1 ~ e2) and then treated recursively.
+Consider a pattern match like
- * Equalities of the form (False ~ (e1 ~ e2)) cannot be analyzed unless
- we know more about the inner equality (e1 ~ e2). That's exactly what
- `simplifyEqExpr' tries to do: It takes e1 and e2 and either returns
- truePmExpr, falsePmExpr or (e1' ~ e2') in case it is uncertain. Note
- that it is not e but rather e', since it may perform some
- simplifications deeper.
--}
+ 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`. This extends to
+`ConLike`s, where all value arguments are universally quantified implicitly.
+So, if the `PmRefutEnv` contains an entry for `x` with `Just [Bool]`, then this
+corresponds to the fact that `forall y. x ≁ Just @Bool y`.
+
+`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`.
+
+Note that `PmAltConLike` carries a list of type arguments. This purely for the
+purpose of being able to reconstruct all other constructors of the matching
+group the `ConLike` is part of through calling `allCompleteMatches` in Check.
+-}
\ No newline at end of file
=====================================
compiler/ghc.cabal.in
=====================================
@@ -324,6 +324,7 @@ Library
MkCore
PprCore
PmExpr
+ PmPpr
TmOracle
Check
Coverage
=====================================
compiler/utils/ListSetOps.hs
=====================================
@@ -14,7 +14,7 @@ module ListSetOps (
Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
-- Duplicate handling
- hasNoDups, removeDups, findDupsEq,
+ hasNoDups, removeDups, findDupsEq, insertNoDup,
equivClasses,
-- Indexing
@@ -169,3 +169,10 @@ 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 at .
+insertNoDup :: (Eq a) => a -> [a] -> [a]
+insertNoDup x set
+ | Nothing <- find (== x) set = x:set
+ | otherwise = set
=====================================
compiler/utils/Outputable.hs
=====================================
@@ -81,8 +81,8 @@ module Outputable (
-- * Error handling and debugging utilities
pprPanic, pprSorry, assertPprPanic, pprPgmError,
- pprTrace, pprTraceDebug, pprTraceIt, warnPprTrace, pprSTrace,
- pprTraceException, pprTraceM,
+ pprTrace, pprTraceDebug, pprTraceWith, pprTraceIt, warnPprTrace,
+ pprSTrace, pprTraceException, pprTraceM,
trace, pgmError, panic, sorry, assertPanic,
pprDebugAndThen, callStackDoc,
) where
@@ -1196,9 +1196,15 @@ pprTrace str doc x
pprTraceM :: Applicative f => String -> SDoc -> f ()
pprTraceM str doc = pprTrace str doc (pure ())
+-- | @pprTraceWith desc f x@ is equivalent to @pprTrace desc (f x) x at .
+-- 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 desc f x = pprTrace desc (f x) x
+
-- | @pprTraceIt desc x@ is equivalent to @pprTrace desc (ppr x) x@
pprTraceIt :: Outputable a => String -> a -> a
-pprTraceIt desc x = pprTrace desc (ppr x) x
+pprTraceIt desc x = pprTraceWith desc ppr x
-- | @pprTraceException desc x action@ runs action, printing a message
-- if it throws an exception.
=====================================
libraries/binary
=====================================
@@ -1 +1 @@
-Subproject commit 94855814e2e4f7a0f191ffa5b4c98ee0147e3174
+Subproject commit e707cab7cb61bebd311632fd46d508ef2f524c6e
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363a.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data Boolean = F | T
+ deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F = 0
+catchAll TooGoodToBeTrue = 1
+catchAll _ = error "impossible"
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
=====================================
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363a.hs:15:1: warning: [-Woverlapping-patterns]
+ Pattern match is redundant
+ In an equation for `catchAll': catchAll _ = ...
+ |
+14 | catchAll _ = error "impossible"
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363b.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data T = A | B | C
+ deriving Eq
+
+pattern BC :: T
+pattern BC = C
+
+{-# COMPLETE A, BC #-}
+
+f A = 1
+f B = 2
+f BC = 3
+f _ = error "impossible"
=====================================
testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
=====================================
@@ -0,0 +1,7 @@
+
+testsuite/tests/pmcheck/complete_sigs/T13363b.hs:16:1: warning: [-Woverlapping-patterns]
+ Pattern match is redundant
+ In an equation for `f': f _ = ...
+ |
+16 | f _ = error "impossible"
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^
=====================================
testsuite/tests/pmcheck/complete_sigs/all.T
=====================================
@@ -15,3 +15,5 @@ test('completesig14', normal, compile, [''])
test('completesig15', normal, compile_fail, [''])
test('T14059a', normal, compile, [''])
test('T14253', expect_broken(14253), compile, [''])
+test('T13363a', normal, compile, ['-Wall'])
+test('T13363b', normal, compile, ['-Wall'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/2fadc36bebf74aa83a165750f04cb02d7d1a2fc8...5a263c0a996877762d9153df5ddba59ef2bcdf03
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/2fadc36bebf74aa83a165750f04cb02d7d1a2fc8...5a263c0a996877762d9153df5ddba59ef2bcdf03
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20190527/afe5e206/attachment-0001.html>
More information about the ghc-commits
mailing list