[Git][ghc/ghc][wip/pmcheck-ncon] Add `PmNCons` to `Check` for correct warnings in the presence of `COMPLETE` groups
Sebastian Graf
gitlab at gitlab.haskell.org
Fri Jun 14 14:25:45 UTC 2019
Sebastian Graf pushed to branch wip/pmcheck-ncon at Glasgow Haskell Compiler / GHC
Commits:
e99f15d2 by Sebastian Graf at 2019-06-14T14:25:22Z
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.
- - - - -
21 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/Binary.hs
- compiler/utils/ListSetOps.hs
- − compiler/utils/ListT.hs
- docs/users_guide/glasgow_exts.rst
- + testsuite/tests/perf/compiler/ManyAlternatives.hs
- + 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
- testsuite/tests/pmcheck/should_compile/all.T
- + testsuite/tests/pmcheck/should_compile/pmc008.hs
- + testsuite/tests/pmcheck/should_compile/pmc009.hs
- + testsuite/tests/pmcheck/should_compile/pmc010.hs
- + testsuite/tests/pmcheck/should_compile/pmc011.hs
Changes:
=====================================
compiler/basicTypes/NameEnv.hs
=====================================
@@ -27,7 +27,7 @@ module NameEnv (
lookupDNameEnv,
delFromDNameEnv,
mapDNameEnv,
- alterDNameEnv,
+ alterDNameEnv, extendDNameEnv_C,
-- ** Dependency analysis
depAnal
) where
@@ -156,3 +156,6 @@ mapDNameEnv = mapUDFM
alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
alterDNameEnv = alterUDFM
+
+extendDNameEnv_C :: (a -> a -> a) -> DNameEnv a -> Name -> a -> DNameEnv a
+extendDNameEnv_C = addToUDFM_C
=====================================
compiler/deSugar/Check.hs
=====================================
@@ -24,6 +24,7 @@ module Check (
import GhcPrelude
+import PmExpr
import TmOracle
import PmPpr
import Unify( tcMatchTy )
@@ -56,20 +57,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.List (find, (\\))
import Data.Maybe (catMaybes, isJust, fromMaybe)
-import Control.Monad (forM, when, forM_, zipWithM, filterM)
+import Control.Monad (forM, 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}
@@ -92,79 +92,38 @@ 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
+type PmM = DsM
-liftD :: DsM a -> PmM a
-liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
-
--- 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]
- PmNLit :: { pm_lit_id :: Id
- , pm_lit_not :: [PmLit] } -> PmPat 'VA
- PmGrd :: { pm_grd_pv :: PatVec
+ -- | See Note [Literals in PmPat]
+ PmLit :: { pm_lit_lit :: PmLit } -> PmPat t
+ PmGrd :: { pm_grd_pv :: PatVec -- ^ Always has 'patVecArity' 1.
, pm_grd_expr :: PmExpr } -> PmPat 'PAT
-- | A fake guard pattern (True <- _) used to represent cases we cannot handle.
PmFake :: PmPat 'PAT
+-- | Should not face a user.
instance Outputable (PmPat a) where
- ppr = pprPmPatDebug
+ ppr (PmCon cc _arg_tys _con_tvs con_args)
+ = hsep [ppr cc, hsep (map ppr con_args)]
+ -- the @ is to differentiate (flexible) variables from rigid constructors and
+ -- literals
+ ppr (PmVar vid) = ppr vid
+ ppr (PmLit li) = ppr li
+ ppr (PmGrd pv ge) = hsep (map ppr pv) <+> text "<-" <+> ppr ge
+ ppr PmFake = text "<PmFake>"
-- data T a where
-- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
@@ -185,6 +144,18 @@ data Delta = MkDelta { delta_ty_cs :: Bag EvVar
type ValSetAbs = [ValVec] -- ^ Value Set Abstractions
type Uncovered = ValSetAbs
+-- | Should not face a user. See 'pprValVecSubstituted' for that.
+instance Outputable ValVec where
+ ppr (ValVec vva delta) = ppr_set vva <+> text "|>" <+> ppr_delta delta
+ where
+ ppr_set = braces . fsep . punctuate comma . map ppr
+ ppr_delta _d = hcat [
+ -- intentionally formatted this way enable the dev to comment in only
+ -- the info she needs
+ ppr (delta_tm_cs delta),
+ ppr (delta_ty_cs delta)
+ ]
+
-- Instead of keeping the whole sets in memory, we keep a boolean for both the
-- covered and the divergent set (we store the uncovered set though, since we
-- want to print it). For both the covered and the divergent we have:
@@ -200,8 +171,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
@@ -218,8 +188,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
@@ -230,51 +199,27 @@ 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)
+ = hang (text "PartialResult" <+> ppr c <+> ppr d) 2 (ppr_vsa vsa)
+ where
+ ppr_vsa = braces . fsep . punctuate comma . map ppr
instance Semi.Semigroup PartialResult where
- (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]
@@ -292,15 +237,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)
]
@@ -325,11 +268,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) []
{-
%************************************************************************
@@ -342,8 +285,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
@@ -351,25 +294,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))
+ tracePm "checkSingle': missing" (vcat (map ppr 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 normaliseValVec 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)
@@ -384,14 +327,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
@@ -406,38 +349,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
+ tracePm "checkMatches': missing" (vcat (map ppr missing))
+ (rs,us,ds) <- go matches missing
+ us' <- normaliseUncovered normaliseValVec 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
@@ -465,7 +406,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.
@@ -516,7 +457,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
@@ -579,8 +520,8 @@ pmTopNormaliseType_maybe env ty_cs typ
-- for why this is done.)
pmInitialTmTyCs :: PmM Delta
pmInitialTmTyCs = do
- ty_cs <- liftD getDictsDs
- tm_cs <- bagToList <$> liftD getTmCsDs
+ ty_cs <- getDictsDs
+ tm_cs <- bagToList <$> getTmCsDs
sat_ty <- tyOracle ty_cs
let initTyCs = if sat_ty then ty_cs else emptyBag
initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
@@ -671,12 +612,100 @@ tmTyCsAreSatisfiable
, delta_tm_cs = term_cs }
_unsat -> Nothing
+-- | Tests whether the 'Id' can inhabit the given 'ConLike' in the context
+-- expressed by the 'Delta'.
+type InhabitationTest = Delta -> Id -> ConLike -> PmM Bool
+
+-- | An 'InhabitationTest' consulting 'mkOneSatisfiableConFull'. Precise, but
+-- expensive.
+isConSatisfiable :: InhabitationTest
+isConSatisfiable delta x con = do
+ tracePm "conInhabitsId" (ppr con <+> ppr x <+> ppr (delta_tm_cs delta))
+ isJust <$> mkOneSatisfiableConFull delta x con
+
+-- | Cheap 'InhabitationTest', always returning @True at .
+cheapInhabitationTest :: InhabitationTest
+cheapInhabitationTest _ _ _ = pure True
+
+normaliseValAbs :: InhabitationTest -> Delta -> ValAbs -> PmM (Maybe (Delta, ValAbs))
+normaliseValAbs is_con_inh delta = runMaybeT . go_va delta
+ where
+ go_va :: Delta -> ValAbs -> MaybeT PmM (Delta, ValAbs)
+ go_va delta pm at PmCon{ pm_con_args = args } = do
+ (delta', args') <- mapAccumLM go_va delta args
+ pure (delta', pm { pm_con_args = args' })
+ go_va delta va@(PmVar x)
+ | let (ty, pacs) = lookupRefutableAltCons (delta_tm_cs delta) x
+ -- TODO: Even if ncons is empty, we might have a complete match ('Void',
+ -- constraints). Figure out how to the complete matches solely from
+ -- @ty at .
+ , ncons@(cl:_) <- [ cl | PmAltConLike cl <- pacs ] = do
+ grps <- lift (allCompleteMatches cl ty)
+ let is_grp_inh = filterM (lift . is_con_inh delta x) . (\\ ncons)
+ incomplete_grps <- traverse is_grp_inh grps
+ -- If all cons of any COMPLETE set are matched, the ValAbs is vacuous.
+ lift $ tracePm "normaliseValAbs" (ppr x <+> ppr (idType x) <+> ppr grps <+> ppr incomplete_grps)
+ guard (all notNull incomplete_grps)
+ -- If there's a unique singleton incomplete group, turn it into a
+ -- @PmCon@ for better readability of warning messages.
+ case incomplete_grps of
+ [[con]] -> do
+ -- We don't want to simplify to a @PmCon@ (which won't normalise
+ -- any further) when @p@ is just the 'cheapInhabitationTest'.
+ -- Thus, we have to assert satisfiability here, even if the
+ -- expensive 'isConSatisfiable' already did so. Also, we have to
+ -- store the constraints in @delta at .
+ (delta', ic) <- MaybeT $ mkOneSatisfiableConFull delta x con
+ lift $ tracePm "normaliseValAbs2" (ppr x <+> ppr (idType x) <+> ppr (ic_val_abs ic))
+ pure (delta', ic_val_abs ic)
+ _ -> pure (delta, va)
+ go_va delta va = pure (delta, va)
+
+-- | Something that normalises a 'ValVec' by consulting the given
+-- 'InhabitationTest' to weed out vacuous 'ValAbs'.
+-- See also 'normaliseValVecHead' and 'normaliseValVec'.
+type ValVecNormaliser = InhabitationTest -> ValVec -> PmM (Maybe ValVec)
+
+-- | A 'ValVecNormaliser' that normalises all components of a 'ValVec'. This is
+-- the 'ValVecNormaliser' to choose once at the end.
+normaliseValVec :: ValVecNormaliser
+normaliseValVec test (ValVec vva delta) = runMaybeT $ do
+ (delta', vva') <- mapAccumLM ((MaybeT .) . normaliseValAbs test) delta vva
+ pure (ValVec vva' delta')
+
+-- | A 'ValVecNormaliser' that only tries to normalise the head of each
+-- 'ValVec'. This is mandatory for pattern guards, where we call 'utail' on the
+-- temporarily extended 'ValVec', hence there's no way to delay this check.
+-- Of course we could 'normaliseValVec' instead, but that's unnecessarily
+-- expensive.
+normaliseValVecHead :: ValVecNormaliser
+normaliseValVecHead _ vva@(ValVec [] _) = pure (Just vva)
+normaliseValVecHead test (ValVec (va:vva) delta) = runMaybeT $ do
+ (delta', va') <- MaybeT (normaliseValAbs test delta va)
+ pure (ValVec (va':vva) delta')
+
+-- | This weeds out 'ValVec's with 'PmVar's where at least one COMPLETE set is
+-- rendered vacuous by equality constraints, by calling out the given
+-- 'ValVecNormaliser' with different 'InhabitationTest's.
+--
+-- This is quite costly due to the many oracle queries, so we only call this at
+-- the last possible moment. I.e., with 'normaliseValVecHead' when leaving a
+-- pattern guard and with 'normaliseValVec' on the final uncovered set.
+normaliseUncovered :: ValVecNormaliser -> Uncovered -> PmM Uncovered
+normaliseUncovered normalise_val_vec us = do
+ -- We'll first do a cheap sweep without consulting the oracles
+ us1 <- mapMaybeM (normalise_val_vec cheapInhabitationTest) us
+ -- Then we'll do another pass trying to weed out the rest with (in)equalities
+ us2 <- mapMaybeM (normalise_val_vec isConSatisfiable) us1
+ tracePm "normaliseUncovered" (vcat (map ppr 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
@@ -833,7 +862,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
@@ -847,7 +876,7 @@ inhabitationCandidates ty_cs ty = do
-- PmCon empty, since we know that they are not gonna be used. Is the
-- right-thing-to-do to actually create them, even if they are never used?
build_tm :: ValAbs -> [DataCon] -> ValAbs
- build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e])
+ build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [e])
-- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
alts_to_check :: Type -> Type -> [DataCon]
@@ -857,7 +886,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
@@ -867,7 +896,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
@@ -925,7 +954,7 @@ nullaryConPattern :: ConLike -> Pattern
-- Nullary data constructor and nullary type constructor
nullaryConPattern con =
PmCon { pm_con_con = con, pm_con_arg_tys = []
- , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
+ , pm_con_tvs = [], pm_con_args = [] }
{-# INLINE nullaryConPattern #-}
truePattern :: Pattern
@@ -933,7 +962,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]
@@ -942,21 +971,20 @@ vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
-- ADT constructor pattern => no existentials, no local constraints
vanillaConPattern con arg_tys args =
PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
- , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
+ , pm_con_tvs = [], pm_con_args = args }
{-# INLINE vanillaConPattern #-}
-- | Create an empty list pattern of a given type
nilPattern :: Type -> Pattern
nilPattern ty =
PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
- , pm_con_tvs = [], pm_con_dicts = []
- , pm_con_args = [] }
+ , pm_con_tvs = [], pm_con_args = [] }
{-# INLINE nilPattern #-}
mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
, pm_con_arg_tys = [ty]
- , pm_con_tvs = [], pm_con_dicts = []
+ , pm_con_tvs = []
, pm_con_args = xs++ys }]
{-# INLINE mkListPatVec #-}
@@ -968,7 +996,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)]
@@ -1047,17 +1075,16 @@ translatePat fam_insts pat = case pat of
ConPatOut { pat_con = (dL->L _ con)
, pat_arg_tys = arg_tys
, pat_tvs = ex_tvs
- , pat_dicts = dicts
, pat_args = ps } -> do
- groups <- allCompleteMatches con arg_tys
+ let ty = conLikeResTy con arg_tys
+ groups <- allCompleteMatches con ty
case groups of
- [] -> mkCanFailPmPat (conLikeResTy con arg_tys)
+ [] -> mkCanFailPmPat ty
_ -> do
args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
return [PmCon { pm_con_con = con
, pm_con_arg_tys = arg_tys
, pm_con_tvs = ex_tvs
- , pm_con_dicts = dicts
, pm_con_args = args }]
-- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
@@ -1185,12 +1212,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)
@@ -1246,11 +1273,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]
@@ -1265,11 +1293,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 = (&&)
@@ -1294,7 +1322,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
@@ -1302,7 +1330,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)
@@ -1315,18 +1343,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)
@@ -1427,10 +1455,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.
%************************************************************************
%* *
@@ -1449,7 +1484,6 @@ pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
= conLikeResTy con tys
pmPatType (PmVar { pm_var_id = x }) = idType x
pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
-pmPatType (PmNLit { pm_lit_id = x }) = idType x
pmPatType (PmGrd { pm_grd_pv = pv })
= ASSERT(patVecArity pv == 1) (pmPatType p)
where Just p = find ((==1) . patternArity) pv
@@ -1477,10 +1511,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:
@@ -1600,8 +1637,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
@@ -1616,7 +1688,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
@@ -1656,7 +1728,6 @@ mkOneConFull x con = do
let con_abs = PmCon { pm_con_con = con
, pm_con_arg_tys = tc_args
, pm_con_tvs = ex_tvs'
- , pm_con_dicts = evvars
, pm_con_args = arguments }
strict_arg_tys = filterByList arg_is_banged arg_tys'
return $ InhabitationCandidate
@@ -1666,24 +1737,45 @@ mkOneConFull x con = do
, ic_strict_arg_tys = strict_arg_tys
}
+-- | 'mkOneConFull' and immediately check whether the resulting
+-- 'InhabitationCandidat' @ic@ is inhabited by consulting 'pmIsSatisfiable'.
+-- Return @Just ic@ if it is.
+mkOneSatisfiableConFull :: Delta -> Id -> ConLike -> PmM (Maybe (Delta, InhabitationCandidate))
+mkOneSatisfiableConFull delta x con = do
+ -- mkOneConFull doesn't cope with type families, so we have to normalise
+ -- x's result type first and introduce an auxiliary binding.
+ fam_insts <- dsGetFamInstEnvs
+ mb_res_ty <- pmTopNormaliseType_maybe fam_insts (delta_ty_cs delta) (idType x)
+ let res_ty = fromMaybe (idType x) (fstOf3 <$> mb_res_ty)
+ (y, delta') <- mkIdCoercion x res_ty delta
+ tracePm "coercing" (ppr x <+> ppr (idType x) <+> ppr y <+> ppr res_ty)
+ ic <- mkOneConFull y con
+ tracePm "mkOneSatisfiableConFull" (ppr x <+> ppr y $$ ppr ic $$ ppr (delta_tm_cs delta'))
+ ((,ic) <$>) <$> pmIsSatisfiable delta' (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+
-- ----------------------------------------------------------------------------
-- * More smart constructors and fresh variable generation
+-- | Introduce a new 'Id' that has the given type and is in the same equivalence
+-- class as the argument.
+mkIdCoercion :: Id -> Type -> Delta -> PmM (Id, Delta)
+mkIdCoercion x ty delta
+ | eqType (idType x) ty = pure (x, delta) -- no need to introduce anything new
+ | otherwise = do
+ y <- mkPmId ty
+ let e = PmExprVar (idName x)
+ pure (y, delta { delta_tm_cs = extendSubst y e (delta_tm_cs delta) })
+
-- | 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: `(x ~ lit)`
-mkPosEq :: Id -> PmLit -> TmVarCt
-mkPosEq x l = TVC x (PmExprLit l)
-{-# INLINE mkPosEq #-}
-
-- | Create a term equality of the form: `(x ~ x)`
-- (always discharged by the term oracle)
mkIdEq :: Id -> TmVarCt
@@ -1691,17 +1783,17 @@ mkIdEq x = TVC x (PmExprVar (idName x))
{-# 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
@@ -1710,7 +1802,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,10 +1813,9 @@ mkPmId2Forms ty = do
-- | Convert a value abstraction an expression
vaToPmExpr :: ValAbs -> PmExpr
vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
- = PmExprCon c (map vaToPmExpr ps)
+ = PmExprCon (PmAltConLike c) (map vaToPmExpr ps)
vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
-vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
-vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
+vaToPmExpr (PmLit { pm_lit_lit = l }) = mkPmExprLit l
-- | Convert a pattern vector to a list of value abstractions by dropping the
-- guards (See Note [Translating As Patterns])
@@ -1738,20 +1829,18 @@ coercePmPat :: Pattern -> [ValAbs]
coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
- , pm_con_tvs = tvs, pm_con_dicts = dicts
- , pm_con_args = args })
+ , pm_con_tvs = tvs, pm_con_args = args })
= [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
- , pm_con_tvs = tvs, pm_con_dicts = dicts
- , pm_con_args = coercePatVec args }]
+ , pm_con_tvs = tvs, pm_con_args = coercePatVec args }]
coercePmPat (PmGrd {}) = [] -- drop the guards
coercePmPat PmFake = [] -- drop the guards
-- | Check whether a 'ConLike' has the /single match/ property, i.e. whether
-- 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 (conLikeResTy cl tys)
{-
Note [Single match constructors]
@@ -1786,20 +1875,17 @@ 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 cl tys = do
+allCompleteMatches :: ConLike -> Type -> DsM [[ConLike]]
+allCompleteMatches cl ty = 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
@@ -1891,8 +1977,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) }
@@ -1974,10 +2059,11 @@ mkInitialUncovered vars = do
-- limit is not exceeded and call `pmcheck`
pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI ps guards vva = do
- n <- liftD incrCheckPmIterDs
- tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
- $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
- $$ pprValVecDebug vva)
+ n <- incrCheckPmIterDs
+ tracePm "pmCheck" (ppr n <> colon
+ $$ hang (text "patterns:") 2 (ppr ps)
+ $$ hang (text "guards:") 2 (ppr guards)
+ $$ ppr vva)
res <- pmcheck ps guards vva
tracePm "pmCheckResult:" (ppr res)
return res
@@ -1986,7 +2072,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
@@ -1994,12 +2080,12 @@ 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
- tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
- $$ pprPatVec ps
- $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
- $$ pprPmPatDebug va
- $$ pprValVecDebug vva)
+ n <- incrCheckPmIterDs
+ tracePm "pmCheckHdI" (ppr n <> colon <+> ppr p
+ $$ hang (text "patterns:") 2 (ppr ps)
+ $$ hang (text "guards:") 2 (ppr guards)
+ $$ ppr va
+ $$ ppr vva)
res <- pmcheckHd p ps guards va vva
tracePm "pmCheckHdI: res" (ppr res)
@@ -2024,10 +2110,15 @@ 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')
+ -- The heads of the ValVecs in the uncovered set might be vacuous, so
+ -- normalise them
+ us <- normaliseUncovered normaliseValVecHead (presultUncovered pr)
+ pure $ utail pr { presultUncovered = us }
pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
@@ -2039,10 +2130,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)
@@ -2053,10 +2143,14 @@ pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
-> PmM PartialResult
-- Var
-pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
- | Just tm_state <- solveOneEq (delta_tm_cs delta) (TVC x (vaToPmExpr va))
- = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
- | otherwise = return mempty
+pmcheckHd (PmVar x) ps guards va (ValVec vva delta) =
+ case solveOneEq (delta_tm_cs delta) (TVC x (vaToPmExpr va)) of
+ Nothing -> return mempty
+ Just tm_state -> do
+ res <- normaliseValAbs isConSatisfiable (delta {delta_tm_cs = tm_state}) va
+ case res of
+ Nothing -> return mempty
+ Just (delta', va') -> ucon va' <$> pmcheckI ps guards (ValVec vva delta')
-- ConCon
pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
@@ -2077,72 +2171,52 @@ 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)
+ kcon c1 (pm_con_arg_tys p) (pm_con_tvs p)
<$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta')
-- LitLit
-pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
- case eqPmLit l1 l2 of
- True -> ucon va <$> pmcheckI ps guards vva
- False -> return $ ucon va (usimple [vva])
+pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva
+ | l1 == l2 = ucon va <$> pmcheckI ps guards vva
+ | otherwise = 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 vas 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
+
+ -- 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
+ mb_delta' <- pmIsSatisfiable delta (ic_tm_ct ic) (ic_ty_cs ic) (ic_strict_arg_tys ic)
+ pr_pos <- case mb_delta' of
+ Nothing -> pure mempty
+ Just delta' -> do
+ tracePm "success" (ppr (delta_tm_cs delta))
+ pmcheckHdI p ps guards (ic_val_abs ic) (ValVec vas delta')
+
+ let pr_neg = mkUnmatched x (PmAltConLike con) vva
+ tracePm "ConVar" (vcat [ppr p, ppr x, ppr pr_pos, ppr pr_neg])
+
+ -- Combine both into a single PartialResult
+ let pr = mkUnion pr_pos pr_neg
+ pure (forceIfCanDiverge x (delta_tm_cs delta) pr)
-- LitVar
-pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
- = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
- mkUnion non_matched <$>
- case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
- Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
- ValVec vva (delta {delta_tm_cs = tm_state})
- Nothing -> return mempty
- where
- -- See Note [Refutable shapes] in TmOracle
- us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
- = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
- | otherwise = []
+pmcheckHd p@(PmLit l) ps guards (PmVar x) vva@(ValVec vas delta) = do
+ pr_pos <- case solveOneEq (delta_tm_cs delta) (TVC x (mkPmExprLit l)) of
+ Nothing -> pure mempty
+ Just tms -> pmcheckHdI p ps guards (PmLit l) vva'
+ where
+ vva'= ValVec vas (delta { delta_tm_cs = tms })
- non_matched = usimple us
-
--- LitNLit
-pmcheckHd (p@(PmLit l)) ps guards
- (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
- | all (not . eqPmLit l) lits
- , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
- -- Both guards check the same so it would be sufficient to have only
- -- the second one. Nevertheless, it is much cheaper to check whether
- -- the literal is in the list so we check it first, to avoid calling
- -- the term oracle (`solveOneEq`) if possible
- = mkUnion non_matched <$>
- pmcheckHdI p ps guards (PmLit l)
- (ValVec vva (delta { delta_tm_cs = tm_state }))
- | otherwise = return non_matched
- where
- -- See Note [Refutable shapes] in TmOracle
- us | Just tm_state <- addSolveRefutableAltCon (delta_tm_cs delta) x (PmAltLit l)
- = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
- | otherwise = []
+ let pr_neg = mkUnmatched x (PmAltLit l) vva
- non_matched = usimple us
+ let pr = mkUnion pr_pos pr_neg
+ pure (forceIfCanDiverge x (delta_tm_cs delta) pr)
-- ----------------------------------------------------------------------------
-- The following three can happen only in cases like #322 where constructors
@@ -2153,7 +2227,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
@@ -2164,18 +2238,14 @@ 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.
- let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
+ let tm_state = extendSubst y (mkPmExprLit l) (delta_tm_cs delta)
delta' = delta { delta_tm_cs = tm_state }
pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
--- ConNLit
-pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
- = pmcheckHdI p ps guards (PmVar x) vva
-
-- Impossible: handled by pmcheck
pmcheckHd PmFake _ _ _ _ = panic "pmcheckHd: Fake"
pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
@@ -2323,9 +2393,8 @@ ucon va = updateVsa upd
-- value vector abstractions of length `(a+n)`, pass the first `n` value
-- abstractions to the constructor (Hence, the resulting value vector
-- abstractions will have length `n+1`)
-kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
- -> PartialResult -> PartialResult
-kcon con arg_tys ex_tvs dicts
+kcon :: ConLike -> [Type] -> [TyVar] -> PartialResult -> PartialResult
+kcon con arg_tys ex_tvs
= let n = conLikeArity con
upd vsa =
[ ValVec (va:vva) delta
@@ -2334,7 +2403,6 @@ kcon con arg_tys ex_tvs dicts
, let va = PmCon { pm_con_con = con
, pm_con_arg_tys = arg_tys
, pm_con_tvs = ex_tvs
- , pm_con_dicts = dicts
, pm_con_args = args } ]
in updateVsa upd
@@ -2354,13 +2422,19 @@ mkCons vva = updateVsa (vva:)
forces :: PartialResult -> PartialResult
forces pres = pres { presultDivergent = Diverged }
--- | Set the divergent set to non-empty if the flag is `True`
-force_if :: Bool -> PartialResult -> PartialResult
-force_if True pres = forces pres
-force_if False pres = pres
+-- | Set the divergent set to non-empty if the variable has not been forced yet
+forceIfCanDiverge :: Id -> TmState -> PartialResult -> PartialResult
+forceIfCanDiverge x tms
+ | canDiverge (idName x) tms = forces
+ | otherwise = id
-set_provenance :: Provenance -> PartialResult -> PartialResult
-set_provenance prov pr = pr { presultProvenance = prov }
+mkUnmatched :: Id -> PmAltCon -> ValVec -> PartialResult
+mkUnmatched x nalt (ValVec vva delta) = usimple us
+ where
+ -- See Note [Refutable shapes] in TmOracle
+ us | Just tms <- tryAddRefutableAltCon (delta_tm_cs delta) x nalt
+ = [ValVec (PmVar x : vva) (delta { delta_tm_cs = tms })]
+ | otherwise = []
-- ----------------------------------------------------------------------------
-- * Propagation of term constraints inwards when checking nested matches
@@ -2369,7 +2443,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,11 +2552,11 @@ isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
= wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
-instance Outputable ValVec where
- ppr (ValVec vva delta)
- = let (subst, refuts) = wrapUpTmState (delta_tm_cs delta)
- vector = substInValAbs subst vva
- in pprUncovered (vector, refuts)
+pprValVecSubstituted :: ValVec -> SDoc
+pprValVecSubstituted (ValVec vva delta) = pprUncovered (vector, refuts)
+ where
+ (subst, refuts) = wrapUpTmState (delta_tm_cs delta)
+ vector = substInValAbs subst vva
-- | Apply a term substitution to a value vector abstraction. All VAs are
-- transformed to PmExpr (used only before pretty printing).
@@ -2493,8 +2567,8 @@ substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
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)
@@ -2511,8 +2585,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
@@ -2523,8 +2596,6 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
is_rec_upd = case kind of { RecUpd -> True; _ -> False }
-- See Note [Inaccessible warnings for record updates]
- onlyBuiltin = prov == FromBuiltin
-
maxPatterns = maxUncoveredPatterns dflags
-- Print a single clause (for redundant/with-inaccessible-rhs)
@@ -2536,7 +2607,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
case qs of -- See #11245
[ValVec [] _]
-> text "Guards do not cover entire pattern space"
- _missing -> let us = map ppr qs
+ _missing -> let us = map pprValVecSubstituted qs
in hang (text "Patterns not matched:") 4
(vcat (take maxPatterns us)
$$ dots maxPatterns us)
@@ -2637,39 +2708,8 @@ pprPats kind pats
-- 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
Opt_D_dump_ec_trace (text herald $$ (nest 2 doc))
-
-
-pprPmPatDebug :: PmPat a -> SDoc
-pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
- = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
-pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
-pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
-pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
-pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv)
- <+> ppr ge
-pprPmPatDebug PmFake = text "PmFake"
-
-pprPatVec :: PatVec -> SDoc
-pprPatVec ps = hang (text "Pattern:") 2
- (brackets $ sep
- $ punctuate (comma <> char '\n') (map pprPmPatDebug ps))
-
-pprValAbs :: [ValAbs] -> SDoc
-pprValAbs ps = hang (text "ValAbs:") 2
- (brackets $ sep
- $ punctuate (comma) (map pprPmPatDebug ps))
-
-pprValVecDebug :: ValVec -> SDoc
-pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
- parens (pprValAbs vas)
- -- <not a haddock> $$ ppr (delta_tm_cs _d)
- -- <not a haddock> $$ ppr (delta_ty_cs _d)
=====================================
compiler/deSugar/PmExpr.hs
=====================================
@@ -9,14 +9,15 @@ Haskell expressions (as used by the pattern matching checker) and utilities.
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module PmExpr (
- PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..),
- eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr
+ PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), isNotPmExprOther,
+ lhsExprToPmExpr, hsExprToPmExpr, mkPmExprLit, pmExprAsList
) where
#include "HsVersions.h"
import GhcPrelude
+import Util
import BasicTypes (SourceText)
import FastString (FastString, unpackFS)
import HsSyn
@@ -29,6 +30,7 @@ import TcType (isStringTy)
import TysWiredIn
import Outputable
import SrcLoc
+import Data.Bifunctor (first)
{-
%************************************************************************
@@ -53,34 +55,29 @@ refer to variables that are otherwise substituted away.
-- | Lifted expressions for pattern match checking.
data PmExpr = PmExprVar Name
- | PmExprCon ConLike [PmExpr]
- | PmExprLit PmLit
+ | PmExprCon PmAltCon [PmExpr]
| PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr]
-
-mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
-mkPmExprData dc args = PmExprCon (RealDataCon dc) args
-
-- | Literals (simple and overloaded ones) for pattern match checking.
+--
+-- See Note [Undecidable Equality for Overloaded Literals]
data PmLit = PmSLit (HsLit GhcTc) -- simple
| PmOLit Bool {- is it negated? -} (HsOverLit GhcTc) -- overloaded
+ deriving Eq
--- | Equality between literals for pattern match checking.
-eqPmLit :: PmLit -> PmLit -> Bool
-eqPmLit (PmSLit l1) (PmSLit l2) = l1 == l2
-eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
- -- See Note [Undecidable Equality for Overloaded Literals]
-eqPmLit _ _ = False
-
--- | Represents a match against a literal. We mostly use it to to encode shapes
--- for a variable that immediately lead to a refutation.
+-- | 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'.
-newtype PmAltCon = PmAltLit PmLit
- deriving Outputable
+data PmAltCon = PmAltConLike ConLike
+ | PmAltLit PmLit
+ deriving Eq
+
+mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
+mkPmExprData dc args = PmExprCon (PmAltConLike (RealDataCon dc)) args
-instance Eq PmAltCon where
- PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
+mkPmExprLit :: PmLit -> PmExpr
+mkPmExprLit l = PmExprCon (PmAltLit l) []
{- Note [Undecidable Equality for Overloaded Literals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -192,17 +189,17 @@ hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x))
hsExprToPmExpr (HsOverLit _ olit)
| OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit, isStringTy ty
= stringExprToList src s
- | otherwise = PmExprLit (PmOLit False olit)
+ | otherwise = PmExprCon (PmAltLit (PmOLit False olit)) []
hsExprToPmExpr (HsLit _ lit)
| HsString src s <- lit
= stringExprToList src s
- | otherwise = PmExprLit (PmSLit lit)
+ | otherwise = PmExprCon (PmAltLit (PmSLit lit)) []
hsExprToPmExpr e@(NegApp _ (dL->L _ neg_expr) _)
- | PmExprLit (PmOLit False olit) <- hsExprToPmExpr neg_expr
+ | PmExprCon (PmAltLit (PmOLit False olit)) _ <- hsExprToPmExpr neg_expr
-- NB: DON'T simply @(NegApp (NegApp olit))@ as @x at . when extension
-- @RebindableSyntax@ enabled, (-(-x)) may not equals to x.
- = PmExprLit (PmOLit True olit)
+ = PmExprCon (PmAltLit (PmOLit False olit)) []
| otherwise = PmExprOther e
hsExprToPmExpr (HsPar _ (dL->L _ e)) = hsExprToPmExpr e
@@ -249,7 +246,35 @@ stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s))
where
cons x xs = mkPmExprData consDataCon [x,xs]
nil = mkPmExprData nilDataCon []
- charToPmExpr c = PmExprLit (PmSLit (HsChar src c))
+ charToPmExpr c = PmExprCon (PmAltLit (PmSLit (HsChar src c))) []
+
+-- | Return @Just@ a 'DataCon' application or @Nothing@, otherwise.
+pmExprToDataConApp :: PmExpr -> Maybe (DataCon, [PmExpr])
+pmExprToDataConApp (PmExprCon (PmAltConLike (RealDataCon c)) es) = Just (c, es)
+pmExprToDataConApp _ = Nothing
+
+-- | Extract a list of 'PmExpr's out of a sequence of cons cells, optionally
+-- terminated by a wildcard variable instead of @[]@.
+--
+-- So, @pmExprAsList (a:b:[]) == Just ([a,b], Nothing)@ is a @[]@ terminated,
+-- while @pmExprAsList (a:b:c) == Just ([a,b], Just c)@ signifies a list prefix
+-- @[a,b]++@ with an unspecified suffix represented by @c at . The prefix shall
+-- never be empty if a suffix is returned (we don't consider that a list).
+-- Returns @Nothing@ in all other cases.
+pmExprAsList :: PmExpr -> Maybe ([PmExpr], Maybe Name)
+pmExprAsList = go False
+ where
+ go allow_id_suffix (PmExprVar x)
+ -- We only allow an Id suffix when we are sure the prefix is not empty
+ | allow_id_suffix
+ = Just ([], Just x)
+ go _ (pmExprToDataConApp -> Just (c, es))
+ | c == nilDataCon
+ = ASSERT( null es ) Just ([], Nothing)
+ | c == consDataCon
+ = ASSERT( length es == 2 ) first (es !! 0 :) <$> go True (es !! 1)
+ go _ _
+ = Nothing
{-
%************************************************************************
@@ -263,18 +288,19 @@ instance Outputable PmLit where
ppr (PmSLit l) = pmPprHsLit l
ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
+instance Outputable PmAltCon where
+ ppr (PmAltConLike cl) = ppr cl
+ ppr (PmAltLit l) = ppr l
+
instance Outputable PmExpr where
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 _ (PmExprVar v) = ppr v
+ go _ (PmExprOther e) = angleBrackets (ppr e)
+ go _ (pmExprAsList -> Just (list, suff)) = case suff of
+ Nothing -> brackets $ fsep $ punctuate comma $ map ppr list
+ Just x -> parens $ fcat $ punctuate colon $ map ppr list ++ [ppr x]
+ go _ (pmExprToDataConApp -> Just (dc, args))
+ | isTupleDataCon dc = parens $ fsep $ punctuate comma $ map ppr args
go prec (PmExprCon cl args)
- = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args))
+ = cparen (notNull args && prec > 0) (hsep (ppr cl:map (go 1) args))
=====================================
compiler/deSugar/PmPpr.hs
=====================================
@@ -21,8 +21,8 @@ import TysWiredIn
import Outputable
import Control.Monad.Trans.State.Strict
import Maybes
-import Util
+import PmExpr
import TmOracle
-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
@@ -35,6 +35,9 @@ import TmOracle
-- where p is not one of {3, 4}
-- q is not one of {0, 5}
-- @
+--
+-- When the set of refutable shapes contains more than 3 elements, the
+-- additional elements are indicated by "...".
pprUncovered :: ([PmExpr], PmRefutEnv) -> SDoc
pprUncovered (expr_vec, refuts)
| null cs = fsep vec -- there are no literal constraints
@@ -45,12 +48,17 @@ pprUncovered (expr_vec, refuts)
(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}@.
+-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is
+-- indicated by an ellipsis.
pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
pprRefutableShapes (var, alts)
- = var <+> text "is not one of" <+> braces (pprWithCommas ppr_alt alts)
+ = var <+> text "is not one of" <+> format_alts alts
where
- ppr_alt (PmAltLit lit) = ppr lit
+ format_alts = braces . fsep . punctuate comma . shorten . map ppr_alt
+ shorten (a:b:c:_:_) = a:b:c:[text "..."]
+ shorten xs = xs
+ ppr_alt (PmAltConLike cl) = ppr cl
+ ppr_alt (PmAltLit lit) = ppr lit
{- 1. Literals
~~~~~~~~~~~~~~
@@ -86,7 +94,7 @@ type PrettyPmRefutEnv = DNameEnv (SDoc, [PmAltCon])
prettifyRefuts :: PmRefutEnv -> PrettyPmRefutEnv
prettifyRefuts = listToUDFM . zipWith rename nameList . udfmToList
where
- rename new (old, lits) = (old, (new, lits))
+ rename new (old, (_ty, 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"] ++
@@ -124,48 +132,35 @@ pprPmExpr (PmExprVar x) = do
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)
+needsParens (PmExprVar {}) = False
+needsParens (PmExprOther {}) = False -- will become a wildcard
+needsParens (PmExprCon (PmAltLit l) _) = isNegatedPmLit l
+needsParens (PmExprCon (PmAltConLike (RealDataCon c)) _)
+ | isTupleDataCon c || isConsDataCon c = False
+needsParens (PmExprCon _ 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
+pprPmExprCon :: PmAltCon -> [PmExpr] -> PmPprM SDoc
+pprPmExprCon (PmAltConLike cl) args = pprConLike cl args
+pprPmExprCon (PmAltLit l) _ = pure (ppr l)
+
+pprConLike :: ConLike -> [PmExpr] -> PmPprM SDoc
+pprConLike cl args
+ | Just (list, suff) <- pmExprAsList (PmExprCon (PmAltConLike cl) args)
+ = case suff of
+ Nothing -> brackets . fsep . punctuate comma <$> mapM pprPmExpr list
+ Just x -> parens . fcat . punctuate colon <$> mapM pprPmExpr (list ++ [PmExprVar x])
+pprConLike (RealDataCon con) args
+ | isTupleDataCon con
+ = parens . fsep . punctuate comma <$> mapM pprPmExpr args
+pprConLike cl args
| conLikeIsInfix cl = case args of
[x, y] -> do x' <- pprPmExprWithParens x
y' <- pprPmExprWithParens y
@@ -181,11 +176,6 @@ 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
=====================================
@@ -5,20 +5,16 @@ Author: George Karachalias <george.karachalias at cs.kuleuven.be>
{-# LANGUAGE CPP, MultiWayIf #-}
-- | The term equality oracle. The main export of the module are the functions
--- 'tmOracle', 'solveOneEq' and 'addSolveRefutableAltCon'.
+-- 'tmOracle', 'solveOneEq' and 'tryAddRefutableAltCon'.
--
-- If you are looking for an oracle that can solve type-level constraints, look
-- at 'TcSimplify.tcCheckSatisfiability'.
module TmOracle (
- -- re-exported from PmExpr
- PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..), TmVarCtEnv,
- PmRefutEnv, eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr,
-
-- the term oracle
- tmOracle, TmState, initialTmState, wrapUpTmState, solveOneEq,
- extendSubst, canDiverge, isRigid,
- addSolveRefutableAltCon, lookupRefutableAltCons,
+ tmOracle, TmVarCtEnv, PmRefutEnv, TmState, initialTmState,
+ wrapUpTmState, solveOneEq, extendSubst, canDiverge, isRigid,
+ tryAddRefutableAltCon, lookupRefutableAltCons,
-- misc.
exprDeepLookup, pmLitType
@@ -33,16 +29,16 @@ import PmExpr
import Util
import Id
import Name
+import NameEnv
+import UniqFM
+import UniqDFM
import Type
import HsLit
import TcHsSyn
import MonadUtils
-import ListSetOps (insertNoDup, unionLists)
+import ListSetOps (unionLists)
import Maybes
import Outputable
-import NameEnv
-import UniqFM
-import UniqDFM
{-
%************************************************************************
@@ -58,14 +54,16 @@ import UniqDFM
type TmVarCtEnv = NameEnv PmExpr
-- | An environment assigning shapes to variables that immediately lead to a
--- refutation. So, if this maps @x :-> [3]@, then trying to solve a 'TmVarCt'
--- like @x ~ 3@ immediately leads to a contradiction.
+-- refutation. So, if this maps @x :-> [Just]@, then trying to solve a
+-- 'TmVarCt' like @x ~ Just False@ immediately leads to a contradiction.
+-- Additionally, this stores the 'Type' from which to draw 'ConLike's from.
+--
-- Determinism is important since we use this for warning messages in
-- 'PmPpr.pprUncovered'. We don't do the same for 'TmVarCtEnv', so that is a plain
-- 'NameEnv'.
--
-- See also Note [Refutable shapes] in TmOracle.
-type PmRefutEnv = DNameEnv [PmAltCon]
+type PmRefutEnv = DNameEnv (Type, [PmAltCon])
-- | The state of the term oracle. Tracks all term-level facts of the form "x is
-- @True@" ('tm_pos') and "x is not @5@" ('tm_neg').
@@ -81,13 +79,19 @@ data TmState = TmS
-- advantage that when we update the solution for @y@ above, we automatically
-- update the solution for @x@ in a union-find-like fashion.
-- Invariant: Only maps to other variables ('PmExprVar') or to WHNFs
- -- ('PmExprLit', 'PmExprCon'). Ergo, never maps to a 'PmExprOther'.
+ -- ('PmExprCon'). Ergo, never maps to a 'PmExprOther'.
, tm_neg :: !PmRefutEnv
-- ^ Maps each variable @x@ to a list of 'PmAltCon's that @x@ definitely
- -- cannot match. Example, @x :-> [3, 4]@ means that @x@ cannot match a literal
- -- 3 or 4. Should we later solve @x@ to a variable @y@
- -- ('extendSubstAndSolve'), we merge the refutable shapes of @x@ into those of
- -- @y at . See also Note [The Pos/Neg invariant].
+ -- 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 . See also Note [The Pos/Neg invariant].
}
{- Note [The Pos/Neg invariant]
@@ -113,7 +117,7 @@ instance Outputable TmState where
pos = map pos_eq (nonDetUFMToList (tm_pos state))
neg = map neg_eq (udfmToList (tm_neg state))
pos_eq (l, r) = ppr l <+> char '~' <+> ppr r
- neg_eq (l, r) = ppr l <+> char '≁' <+> ppr r
+ neg_eq (l, r) = ppr l <+> text "/~" <+> ppr r
-- | Initial state of the oracle.
initialTmState :: TmState
@@ -148,21 +152,23 @@ canDiverge x TmS{ tm_pos = pos, tm_neg = neg }
-- | Check whether the equality @x ~ e@ leads to a refutation. Make sure that
-- @x@ and @e@ are completely substituted before!
isRefutable :: Name -> PmExpr -> PmRefutEnv -> Bool
-isRefutable x e env
- = fromMaybe False $ elem <$> exprToAlt e <*> lookupDNameEnv env x
+isRefutable x e env = fromMaybe False $ do
+ alt <- exprToAlt e
+ (_, nalts) <- lookupDNameEnv env x
+ pure (elem alt nalts)
-- | Solve an equality (top-level).
solveOneEq :: TmState -> TmVarCt -> Maybe TmState
solveOneEq solver_env (TVC x e) = unify solver_env (PmExprVar (idName x), e)
exprToAlt :: PmExpr -> Maybe PmAltCon
-exprToAlt (PmExprLit l) = Just (PmAltLit l)
-exprToAlt _ = Nothing
+exprToAlt (PmExprCon c _) = Just c
+exprToAlt _ = Nothing
-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
-- 'TmState' and return @Nothing@ if that leads to a contradiction.
-addSolveRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
-addSolveRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
+tryAddRefutableAltCon :: TmState -> Id -> PmAltCon -> Maybe TmState
+tryAddRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
= case exprToAlt e of
-- We have to take care to preserve Note [The Pos/Neg invariant]
Nothing -> Just extended -- Not solved yet
@@ -172,20 +178,24 @@ addSolveRefutableAltCon original at TmS{ tm_pos = pos, tm_neg = neg } x nalt
where -- refutation redundant
(y, e) = varDeepLookup pos (idName x)
extended = original { tm_neg = neg' }
- neg' = alterDNameEnv (delNulls (insertNoDup nalt)) neg y
+ neg' = extendDNameEnv_C combineRefutEntries neg y (idType x, [nalt])
--- | 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
+-- | Combines two entries in a 'PmRefutEnv' by merging the set of refutable
+-- 'PmAltCon's.
+combineRefutEntries :: (Type, [PmAltCon]) -> (Type, [PmAltCon]) -> (Type, [PmAltCon])
+combineRefutEntries (old_ty, old_nalts) (new_ty, new_nalts)
+ = ASSERT( eqType old_ty new_ty ) (old_ty, unionLists old_nalts new_nalts)
-- | 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))
+--
+-- Note that because of Note [The Pos/Neg invariant], this will return an empty
+-- list of alt cons for 'Id's which already have a solution.
+lookupRefutableAltCons :: TmState -> Id -> (Type, [PmAltCon])
+lookupRefutableAltCons _tms at TmS{ tm_pos = pos, tm_neg = neg } x
+ = fromMaybe (idType x, []) (lookupDNameEnv neg y)
+ where
+ (y, _e) = varDeepLookup pos (idName x)
-- | Is the given variable /rigid/ (i.e., we have a solution for it) or
-- /flexible/ (i.e., no solution)? Returns the solution if /rigid/. A
@@ -197,6 +207,11 @@ isRigid TmS{ tm_pos = pos } x = lookupNameEnv pos x
isFlexible :: TmState -> Name -> Bool
isFlexible tms = isNothing . isRigid tms
+-- | Is this a solution for a variable, i.e., something in WHNF?
+isSolution :: PmExpr -> Bool
+isSolution PmExprCon{} = True
+isSolution _ = False
+
-- | Try to unify two 'PmExpr's and record the gained knowledge in the
-- 'TmState'.
--
@@ -209,12 +224,8 @@ unify tms eq@(e1, e2) = case eq of
(PmExprOther _,_) -> boring
(_,PmExprOther _) -> boring
- (PmExprLit l1, PmExprLit l2) -> case eqPmLit l1 l2 of
- -- See Note [Undecidable Equality for Overloaded Literals]
- True -> boring
- False -> unsat
-
(PmExprCon c1 ts1, PmExprCon c2 ts2)
+ -- See Note [Undecidable Equality for Overloaded Literals]
| c1 == c2 -> foldlM unify tms (zip ts1 ts2)
| otherwise -> unsat
@@ -231,9 +242,6 @@ unify tms eq@(e1, e2) = case eq of
(PmExprVar x, PmExprVar y) -> Just (equate x y tms)
(PmExprVar x, _) -> trySolve x e2 tms
(_, PmExprVar y) -> trySolve y e1 tms
-
- _ -> WARN( True, text "unify: Catch all" <+> ppr eq)
- boring -- I HATE CATCH-ALLS
where
boring = Just tms
unsat = Nothing
@@ -252,28 +260,25 @@ equate x y tms at TmS{ tm_pos = pos, tm_neg = neg }
pos' = extendNameEnv pos x (PmExprVar y)
-- Be careful to uphold Note [The Pos/Neg invariant] by merging the refuts
-- of x into those of y
- nalts = fromMaybe [] (lookupDNameEnv neg x)
- neg' = alterDNameEnv (delNulls (unionLists nalts)) neg y
- `delFromDNameEnv` x
+ neg' = case lookupDNameEnv neg x of
+ Nothing -> neg
+ Just entry -> extendDNameEnv_C combineRefutEntries neg y entry
+ `delFromDNameEnv` x
tms' = TmS { tm_pos = pos', tm_neg = neg' }
-- | Extend the substitution with a mapping @x: -> e@ if compatible with
-- refutable shapes of @x@ and its solution, reject (@Nothing@) otherwise.
--
-- Precondition: @x@ is flexible (cf. 'isFlexible'/'isRigid').
--- Precondition: @e@ is a 'PmExprCon' or 'PmExprLit'
+-- Precondition: @e@ is a solution, i.e., 'PmExprCon' (cf. 'isSolution').
trySolve:: Name -> PmExpr -> TmState -> Maybe TmState
trySolve x e _tms at TmS{ tm_pos = pos, tm_neg = neg }
| ASSERT( isFlexible _tms x )
- ASSERT( _is_whnf e )
+ ASSERT( isSolution e )
isRefutable x e neg
= Nothing
| otherwise
= Just (TmS (extendNameEnv pos x e) (delFromDNameEnv neg x))
- where
- _is_whnf PmExprCon{} = True
- _is_whnf PmExprLit{} = True
- _is_whnf _ = False
-- | When we know that a variable is fresh, we do not actually have to
-- check whether anything changes, we know that nothing does. Hence,
@@ -303,7 +308,7 @@ varDeepLookup env x = case lookupNameEnv env x of
exprDeepLookup :: TmVarCtEnv -> PmExpr -> PmExpr
exprDeepLookup env (PmExprVar x) = snd (varDeepLookup env x)
exprDeepLookup env (PmExprCon c es) = PmExprCon c (map (exprDeepLookup env) es)
-exprDeepLookup _ other_expr = other_expr -- PmExprLit, PmExprOther
+exprDeepLookup _ e at PmExprOther{} = e
-- | External interface to the term oracle.
tmOracle :: TmState -> [TmVarCt] -> Maybe TmState
@@ -354,9 +359,17 @@ second clause and report the clause as redundant. After the third clause, the
set of such *refutable* literals is again extended to `[0, 1]`.
In general, we want to store a set of refutable shapes (`PmAltCon`) for each
-variable. That's the purpose of the `PmRefutEnv`. `addSolveRefutableAltCon` will
-add such a refutable mapping to the `PmRefutEnv` in the term oracles state and
-check if causes any immediate contradiction. Whenever we record a solution in
-the substitution via `extendSubstAndSolve`, the refutable environment is checked
-for any matching refutable `PmAltCon`.
+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`.
+
+`tryAddRefutableAltCon` will add such a refutable mapping to the `PmRefutEnv`
+in the term oracles state and check if it 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.
-}
=====================================
compiler/ghc.cabal.in
=====================================
@@ -568,7 +568,6 @@ Library
IOEnv
Json
ListSetOps
- ListT
Maybes
MonadUtils
OrdList
=====================================
compiler/utils/Binary.hs
=====================================
@@ -724,7 +724,6 @@ putTypeRep bh (Fun arg res) = do
put_ bh (3 :: Word8)
putTypeRep bh arg
putTypeRep bh res
-putTypeRep _ _ = fail "Binary.putTypeRep: Impossible"
getSomeTypeRep :: BinHandle -> IO SomeTypeRep
getSomeTypeRep bh = do
=====================================
compiler/utils/ListSetOps.hs
=====================================
@@ -14,7 +14,7 @@ module ListSetOps (
Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing,
-- Duplicate handling
- hasNoDups, removeDups, findDupsEq, insertNoDup,
+ hasNoDups, removeDups, findDupsEq,
equivClasses,
-- Indexing
@@ -169,10 +169,3 @@ findDupsEq _ [] = []
findDupsEq eq (x:xs) | null eq_xs = findDupsEq eq xs
| otherwise = (x :| eq_xs) : findDupsEq eq neq_xs
where (eq_xs, neq_xs) = partition (eq x) xs
-
--- | \( O(n) \). @'insertNoDup' x xs@ treats @xs@ as a set, inserting @x@ only
--- when an equal element couldn't be found in @xs at .
-insertNoDup :: (Eq a) => a -> [a] -> [a]
-insertNoDup x set
- | elem x set = set
- | otherwise = x:set
=====================================
compiler/utils/ListT.hs deleted
=====================================
@@ -1,79 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-
--------------------------------------------------------------------------
--- |
--- Module : Control.Monad.Logic
--- Copyright : (c) Dan Doel
--- License : BSD3
---
--- Maintainer : dan.doel at gmail.com
--- Stability : experimental
--- Portability : non-portable (multi-parameter type classes)
---
--- A backtracking, logic programming monad.
---
--- Adapted from the paper
--- /Backtracking, Interleaving, and Terminating
--- Monad Transformers/, by
--- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry
--- (<http://www.cs.rutgers.edu/~ccshan/logicprog/ListT-icfp2005.pdf>).
--------------------------------------------------------------------------
-
-module ListT (
- ListT(..),
- runListT,
- select,
- fold
- ) where
-
-import GhcPrelude
-
-import Control.Applicative
-
-import Control.Monad
-import Control.Monad.Fail as MonadFail
-
--------------------------------------------------------------------------
--- | A monad transformer for performing backtracking computations
--- layered over another monad 'm'
-newtype ListT m a =
- ListT { unListT :: forall r. (a -> m r -> m r) -> m r -> m r }
- deriving (Functor)
-
-select :: Monad m => [a] -> ListT m a
-select xs = foldr (<|>) mzero (map pure xs)
-
-fold :: ListT m a -> (a -> m r -> m r) -> m r -> m r
-fold = runListT
-
--------------------------------------------------------------------------
--- | Runs a ListT computation with the specified initial success and
--- failure continuations.
-runListT :: ListT m a -> (a -> m r -> m r) -> m r -> m r
-runListT = unListT
-
-instance Applicative (ListT f) where
- pure a = ListT $ \sk fk -> sk a fk
- f <*> a = ListT $ \sk fk -> unListT f (\g fk' -> unListT a (sk . g) fk') fk
-
-instance Alternative (ListT f) where
- empty = ListT $ \_ fk -> fk
- f1 <|> f2 = ListT $ \sk fk -> unListT f1 sk (unListT f2 sk fk)
-
-instance Monad (ListT m) where
- m >>= f = ListT $ \sk fk -> unListT m (\a fk' -> unListT (f a) sk fk') fk
-#if !MIN_VERSION_base(4,13,0)
- fail = MonadFail.fail
-#endif
-
-instance MonadFail.MonadFail (ListT m) where
- fail _ = ListT $ \_ fk -> fk
-
-instance MonadPlus (ListT m) where
- mzero = ListT $ \_ fk -> fk
- m1 `mplus` m2 = ListT $ \sk fk -> unListT m1 sk (unListT m2 sk fk)
=====================================
docs/users_guide/glasgow_exts.rst
=====================================
@@ -15420,49 +15420,6 @@ the user must provide a type signature. ::
foo :: [a] -> Int
foo T = 5
-.. _multiple-complete-pragmas:
-
-Disambiguating between multiple ``COMPLETE`` pragmas
-----------------------------------------------------
-
-What should happen if there are multiple ``COMPLETE`` sets that apply to a
-single set of patterns? Consider this example: ::
-
- data T = MkT1 | MkT2 | MkT2Internal
- {-# COMPLETE MkT1, MkT2 #-}
- {-# COMPLETE MkT1, MkT2Internal #-}
-
- f :: T -> Bool
- f MkT1 = True
- f MkT2 = False
-
-Which ``COMPLETE`` pragma should be used when checking the coverage of the
-patterns in ``f``? If we pick the ``COMPLETE`` set that covers ``MkT1`` and
-``MkT2``, then ``f`` is exhaustive, but if we pick the other ``COMPLETE`` set
-that covers ``MkT1`` and ``MkT2Internal``, then ``f`` is *not* exhaustive,
-since it fails to match ``MkT2Internal``. An intuitive way to solve this
-dilemma is to recognize that picking the former ``COMPLETE`` set produces the
-fewest number of uncovered pattern clauses, and thus is the better choice.
-
-GHC disambiguates between multiple ``COMPLETE`` sets based on this rationale.
-To make things more formal, when the pattern-match checker requests a set of
-constructors for some data type constructor ``T``, the checker returns:
-
-* The original set of data constructors for ``T``
-* Any ``COMPLETE`` sets of type ``T``
-
-GHC then checks for pattern coverage using each of these sets. If any of these
-sets passes the pattern coverage checker with no warnings, then we are done. If
-each set produces at least one warning, then GHC must pick one of the sets of
-warnings depending on how good the results are. The results are prioritized in
-this order:
-
-1. Fewest uncovered clauses
-2. Fewest redundant clauses
-3. Fewest inaccessible clauses
-4. Whether the match comes from the original set of data constructors or from a
- ``COMPLETE`` pragma (prioritizing the former over the latter)
-
.. _overlap-pragma:
``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas
=====================================
testsuite/tests/perf/compiler/ManyAlternatives.hs
=====================================
@@ -0,0 +1,2005 @@
+module ManyAlternatives where
+
+data A1000 = A0
+ | A0001
+ | A0002
+ | A0003
+ | A0004
+ | A0005
+ | A0006
+ | A0007
+ | A0008
+ | A0009
+ | A0010
+ | A0011
+ | A0012
+ | A0013
+ | A0014
+ | A0015
+ | A0016
+ | A0017
+ | A0018
+ | A0019
+ | A0020
+ | A0021
+ | A0022
+ | A0023
+ | A0024
+ | A0025
+ | A0026
+ | A0027
+ | A0028
+ | A0029
+ | A0030
+ | A0031
+ | A0032
+ | A0033
+ | A0034
+ | A0035
+ | A0036
+ | A0037
+ | A0038
+ | A0039
+ | A0040
+ | A0041
+ | A0042
+ | A0043
+ | A0044
+ | A0045
+ | A0046
+ | A0047
+ | A0048
+ | A0049
+ | A0050
+ | A0051
+ | A0052
+ | A0053
+ | A0054
+ | A0055
+ | A0056
+ | A0057
+ | A0058
+ | A0059
+ | A0060
+ | A0061
+ | A0062
+ | A0063
+ | A0064
+ | A0065
+ | A0066
+ | A0067
+ | A0068
+ | A0069
+ | A0070
+ | A0071
+ | A0072
+ | A0073
+ | A0074
+ | A0075
+ | A0076
+ | A0077
+ | A0078
+ | A0079
+ | A0080
+ | A0081
+ | A0082
+ | A0083
+ | A0084
+ | A0085
+ | A0086
+ | A0087
+ | A0088
+ | A0089
+ | A0090
+ | A0091
+ | A0092
+ | A0093
+ | A0094
+ | A0095
+ | A0096
+ | A0097
+ | A0098
+ | A0099
+ | A0100
+ | A0101
+ | A0102
+ | A0103
+ | A0104
+ | A0105
+ | A0106
+ | A0107
+ | A0108
+ | A0109
+ | A0110
+ | A0111
+ | A0112
+ | A0113
+ | A0114
+ | A0115
+ | A0116
+ | A0117
+ | A0118
+ | A0119
+ | A0120
+ | A0121
+ | A0122
+ | A0123
+ | A0124
+ | A0125
+ | A0126
+ | A0127
+ | A0128
+ | A0129
+ | A0130
+ | A0131
+ | A0132
+ | A0133
+ | A0134
+ | A0135
+ | A0136
+ | A0137
+ | A0138
+ | A0139
+ | A0140
+ | A0141
+ | A0142
+ | A0143
+ | A0144
+ | A0145
+ | A0146
+ | A0147
+ | A0148
+ | A0149
+ | A0150
+ | A0151
+ | A0152
+ | A0153
+ | A0154
+ | A0155
+ | A0156
+ | A0157
+ | A0158
+ | A0159
+ | A0160
+ | A0161
+ | A0162
+ | A0163
+ | A0164
+ | A0165
+ | A0166
+ | A0167
+ | A0168
+ | A0169
+ | A0170
+ | A0171
+ | A0172
+ | A0173
+ | A0174
+ | A0175
+ | A0176
+ | A0177
+ | A0178
+ | A0179
+ | A0180
+ | A0181
+ | A0182
+ | A0183
+ | A0184
+ | A0185
+ | A0186
+ | A0187
+ | A0188
+ | A0189
+ | A0190
+ | A0191
+ | A0192
+ | A0193
+ | A0194
+ | A0195
+ | A0196
+ | A0197
+ | A0198
+ | A0199
+ | A0200
+ | A0201
+ | A0202
+ | A0203
+ | A0204
+ | A0205
+ | A0206
+ | A0207
+ | A0208
+ | A0209
+ | A0210
+ | A0211
+ | A0212
+ | A0213
+ | A0214
+ | A0215
+ | A0216
+ | A0217
+ | A0218
+ | A0219
+ | A0220
+ | A0221
+ | A0222
+ | A0223
+ | A0224
+ | A0225
+ | A0226
+ | A0227
+ | A0228
+ | A0229
+ | A0230
+ | A0231
+ | A0232
+ | A0233
+ | A0234
+ | A0235
+ | A0236
+ | A0237
+ | A0238
+ | A0239
+ | A0240
+ | A0241
+ | A0242
+ | A0243
+ | A0244
+ | A0245
+ | A0246
+ | A0247
+ | A0248
+ | A0249
+ | A0250
+ | A0251
+ | A0252
+ | A0253
+ | A0254
+ | A0255
+ | A0256
+ | A0257
+ | A0258
+ | A0259
+ | A0260
+ | A0261
+ | A0262
+ | A0263
+ | A0264
+ | A0265
+ | A0266
+ | A0267
+ | A0268
+ | A0269
+ | A0270
+ | A0271
+ | A0272
+ | A0273
+ | A0274
+ | A0275
+ | A0276
+ | A0277
+ | A0278
+ | A0279
+ | A0280
+ | A0281
+ | A0282
+ | A0283
+ | A0284
+ | A0285
+ | A0286
+ | A0287
+ | A0288
+ | A0289
+ | A0290
+ | A0291
+ | A0292
+ | A0293
+ | A0294
+ | A0295
+ | A0296
+ | A0297
+ | A0298
+ | A0299
+ | A0300
+ | A0301
+ | A0302
+ | A0303
+ | A0304
+ | A0305
+ | A0306
+ | A0307
+ | A0308
+ | A0309
+ | A0310
+ | A0311
+ | A0312
+ | A0313
+ | A0314
+ | A0315
+ | A0316
+ | A0317
+ | A0318
+ | A0319
+ | A0320
+ | A0321
+ | A0322
+ | A0323
+ | A0324
+ | A0325
+ | A0326
+ | A0327
+ | A0328
+ | A0329
+ | A0330
+ | A0331
+ | A0332
+ | A0333
+ | A0334
+ | A0335
+ | A0336
+ | A0337
+ | A0338
+ | A0339
+ | A0340
+ | A0341
+ | A0342
+ | A0343
+ | A0344
+ | A0345
+ | A0346
+ | A0347
+ | A0348
+ | A0349
+ | A0350
+ | A0351
+ | A0352
+ | A0353
+ | A0354
+ | A0355
+ | A0356
+ | A0357
+ | A0358
+ | A0359
+ | A0360
+ | A0361
+ | A0362
+ | A0363
+ | A0364
+ | A0365
+ | A0366
+ | A0367
+ | A0368
+ | A0369
+ | A0370
+ | A0371
+ | A0372
+ | A0373
+ | A0374
+ | A0375
+ | A0376
+ | A0377
+ | A0378
+ | A0379
+ | A0380
+ | A0381
+ | A0382
+ | A0383
+ | A0384
+ | A0385
+ | A0386
+ | A0387
+ | A0388
+ | A0389
+ | A0390
+ | A0391
+ | A0392
+ | A0393
+ | A0394
+ | A0395
+ | A0396
+ | A0397
+ | A0398
+ | A0399
+ | A0400
+ | A0401
+ | A0402
+ | A0403
+ | A0404
+ | A0405
+ | A0406
+ | A0407
+ | A0408
+ | A0409
+ | A0410
+ | A0411
+ | A0412
+ | A0413
+ | A0414
+ | A0415
+ | A0416
+ | A0417
+ | A0418
+ | A0419
+ | A0420
+ | A0421
+ | A0422
+ | A0423
+ | A0424
+ | A0425
+ | A0426
+ | A0427
+ | A0428
+ | A0429
+ | A0430
+ | A0431
+ | A0432
+ | A0433
+ | A0434
+ | A0435
+ | A0436
+ | A0437
+ | A0438
+ | A0439
+ | A0440
+ | A0441
+ | A0442
+ | A0443
+ | A0444
+ | A0445
+ | A0446
+ | A0447
+ | A0448
+ | A0449
+ | A0450
+ | A0451
+ | A0452
+ | A0453
+ | A0454
+ | A0455
+ | A0456
+ | A0457
+ | A0458
+ | A0459
+ | A0460
+ | A0461
+ | A0462
+ | A0463
+ | A0464
+ | A0465
+ | A0466
+ | A0467
+ | A0468
+ | A0469
+ | A0470
+ | A0471
+ | A0472
+ | A0473
+ | A0474
+ | A0475
+ | A0476
+ | A0477
+ | A0478
+ | A0479
+ | A0480
+ | A0481
+ | A0482
+ | A0483
+ | A0484
+ | A0485
+ | A0486
+ | A0487
+ | A0488
+ | A0489
+ | A0490
+ | A0491
+ | A0492
+ | A0493
+ | A0494
+ | A0495
+ | A0496
+ | A0497
+ | A0498
+ | A0499
+ | A0500
+ | A0501
+ | A0502
+ | A0503
+ | A0504
+ | A0505
+ | A0506
+ | A0507
+ | A0508
+ | A0509
+ | A0510
+ | A0511
+ | A0512
+ | A0513
+ | A0514
+ | A0515
+ | A0516
+ | A0517
+ | A0518
+ | A0519
+ | A0520
+ | A0521
+ | A0522
+ | A0523
+ | A0524
+ | A0525
+ | A0526
+ | A0527
+ | A0528
+ | A0529
+ | A0530
+ | A0531
+ | A0532
+ | A0533
+ | A0534
+ | A0535
+ | A0536
+ | A0537
+ | A0538
+ | A0539
+ | A0540
+ | A0541
+ | A0542
+ | A0543
+ | A0544
+ | A0545
+ | A0546
+ | A0547
+ | A0548
+ | A0549
+ | A0550
+ | A0551
+ | A0552
+ | A0553
+ | A0554
+ | A0555
+ | A0556
+ | A0557
+ | A0558
+ | A0559
+ | A0560
+ | A0561
+ | A0562
+ | A0563
+ | A0564
+ | A0565
+ | A0566
+ | A0567
+ | A0568
+ | A0569
+ | A0570
+ | A0571
+ | A0572
+ | A0573
+ | A0574
+ | A0575
+ | A0576
+ | A0577
+ | A0578
+ | A0579
+ | A0580
+ | A0581
+ | A0582
+ | A0583
+ | A0584
+ | A0585
+ | A0586
+ | A0587
+ | A0588
+ | A0589
+ | A0590
+ | A0591
+ | A0592
+ | A0593
+ | A0594
+ | A0595
+ | A0596
+ | A0597
+ | A0598
+ | A0599
+ | A0600
+ | A0601
+ | A0602
+ | A0603
+ | A0604
+ | A0605
+ | A0606
+ | A0607
+ | A0608
+ | A0609
+ | A0610
+ | A0611
+ | A0612
+ | A0613
+ | A0614
+ | A0615
+ | A0616
+ | A0617
+ | A0618
+ | A0619
+ | A0620
+ | A0621
+ | A0622
+ | A0623
+ | A0624
+ | A0625
+ | A0626
+ | A0627
+ | A0628
+ | A0629
+ | A0630
+ | A0631
+ | A0632
+ | A0633
+ | A0634
+ | A0635
+ | A0636
+ | A0637
+ | A0638
+ | A0639
+ | A0640
+ | A0641
+ | A0642
+ | A0643
+ | A0644
+ | A0645
+ | A0646
+ | A0647
+ | A0648
+ | A0649
+ | A0650
+ | A0651
+ | A0652
+ | A0653
+ | A0654
+ | A0655
+ | A0656
+ | A0657
+ | A0658
+ | A0659
+ | A0660
+ | A0661
+ | A0662
+ | A0663
+ | A0664
+ | A0665
+ | A0666
+ | A0667
+ | A0668
+ | A0669
+ | A0670
+ | A0671
+ | A0672
+ | A0673
+ | A0674
+ | A0675
+ | A0676
+ | A0677
+ | A0678
+ | A0679
+ | A0680
+ | A0681
+ | A0682
+ | A0683
+ | A0684
+ | A0685
+ | A0686
+ | A0687
+ | A0688
+ | A0689
+ | A0690
+ | A0691
+ | A0692
+ | A0693
+ | A0694
+ | A0695
+ | A0696
+ | A0697
+ | A0698
+ | A0699
+ | A0700
+ | A0701
+ | A0702
+ | A0703
+ | A0704
+ | A0705
+ | A0706
+ | A0707
+ | A0708
+ | A0709
+ | A0710
+ | A0711
+ | A0712
+ | A0713
+ | A0714
+ | A0715
+ | A0716
+ | A0717
+ | A0718
+ | A0719
+ | A0720
+ | A0721
+ | A0722
+ | A0723
+ | A0724
+ | A0725
+ | A0726
+ | A0727
+ | A0728
+ | A0729
+ | A0730
+ | A0731
+ | A0732
+ | A0733
+ | A0734
+ | A0735
+ | A0736
+ | A0737
+ | A0738
+ | A0739
+ | A0740
+ | A0741
+ | A0742
+ | A0743
+ | A0744
+ | A0745
+ | A0746
+ | A0747
+ | A0748
+ | A0749
+ | A0750
+ | A0751
+ | A0752
+ | A0753
+ | A0754
+ | A0755
+ | A0756
+ | A0757
+ | A0758
+ | A0759
+ | A0760
+ | A0761
+ | A0762
+ | A0763
+ | A0764
+ | A0765
+ | A0766
+ | A0767
+ | A0768
+ | A0769
+ | A0770
+ | A0771
+ | A0772
+ | A0773
+ | A0774
+ | A0775
+ | A0776
+ | A0777
+ | A0778
+ | A0779
+ | A0780
+ | A0781
+ | A0782
+ | A0783
+ | A0784
+ | A0785
+ | A0786
+ | A0787
+ | A0788
+ | A0789
+ | A0790
+ | A0791
+ | A0792
+ | A0793
+ | A0794
+ | A0795
+ | A0796
+ | A0797
+ | A0798
+ | A0799
+ | A0800
+ | A0801
+ | A0802
+ | A0803
+ | A0804
+ | A0805
+ | A0806
+ | A0807
+ | A0808
+ | A0809
+ | A0810
+ | A0811
+ | A0812
+ | A0813
+ | A0814
+ | A0815
+ | A0816
+ | A0817
+ | A0818
+ | A0819
+ | A0820
+ | A0821
+ | A0822
+ | A0823
+ | A0824
+ | A0825
+ | A0826
+ | A0827
+ | A0828
+ | A0829
+ | A0830
+ | A0831
+ | A0832
+ | A0833
+ | A0834
+ | A0835
+ | A0836
+ | A0837
+ | A0838
+ | A0839
+ | A0840
+ | A0841
+ | A0842
+ | A0843
+ | A0844
+ | A0845
+ | A0846
+ | A0847
+ | A0848
+ | A0849
+ | A0850
+ | A0851
+ | A0852
+ | A0853
+ | A0854
+ | A0855
+ | A0856
+ | A0857
+ | A0858
+ | A0859
+ | A0860
+ | A0861
+ | A0862
+ | A0863
+ | A0864
+ | A0865
+ | A0866
+ | A0867
+ | A0868
+ | A0869
+ | A0870
+ | A0871
+ | A0872
+ | A0873
+ | A0874
+ | A0875
+ | A0876
+ | A0877
+ | A0878
+ | A0879
+ | A0880
+ | A0881
+ | A0882
+ | A0883
+ | A0884
+ | A0885
+ | A0886
+ | A0887
+ | A0888
+ | A0889
+ | A0890
+ | A0891
+ | A0892
+ | A0893
+ | A0894
+ | A0895
+ | A0896
+ | A0897
+ | A0898
+ | A0899
+ | A0900
+ | A0901
+ | A0902
+ | A0903
+ | A0904
+ | A0905
+ | A0906
+ | A0907
+ | A0908
+ | A0909
+ | A0910
+ | A0911
+ | A0912
+ | A0913
+ | A0914
+ | A0915
+ | A0916
+ | A0917
+ | A0918
+ | A0919
+ | A0920
+ | A0921
+ | A0922
+ | A0923
+ | A0924
+ | A0925
+ | A0926
+ | A0927
+ | A0928
+ | A0929
+ | A0930
+ | A0931
+ | A0932
+ | A0933
+ | A0934
+ | A0935
+ | A0936
+ | A0937
+ | A0938
+ | A0939
+ | A0940
+ | A0941
+ | A0942
+ | A0943
+ | A0944
+ | A0945
+ | A0946
+ | A0947
+ | A0948
+ | A0949
+ | A0950
+ | A0951
+ | A0952
+ | A0953
+ | A0954
+ | A0955
+ | A0956
+ | A0957
+ | A0958
+ | A0959
+ | A0960
+ | A0961
+ | A0962
+ | A0963
+ | A0964
+ | A0965
+ | A0966
+ | A0967
+ | A0968
+ | A0969
+ | A0970
+ | A0971
+ | A0972
+ | A0973
+ | A0974
+ | A0975
+ | A0976
+ | A0977
+ | A0978
+ | A0979
+ | A0980
+ | A0981
+ | A0982
+ | A0983
+ | A0984
+ | A0985
+ | A0986
+ | A0987
+ | A0988
+ | A0989
+ | A0990
+ | A0991
+ | A0992
+ | A0993
+ | A0994
+ | A0995
+ | A0996
+ | A0997
+ | A0998
+ | A0999
+ | A1000
+
+f :: A1000 -> Int
+f A0001 = 1990001
+f A0002 = 1990002
+f A0003 = 1990003
+f A0004 = 1990004
+f A0005 = 1990005
+f A0006 = 1990006
+f A0007 = 1990007
+f A0008 = 1990008
+f A0009 = 1990009
+f A0010 = 1990010
+f A0011 = 1990011
+f A0012 = 1990012
+f A0013 = 1990013
+f A0014 = 1990014
+f A0015 = 1990015
+f A0016 = 1990016
+f A0017 = 1990017
+f A0018 = 1990018
+f A0019 = 1990019
+f A0020 = 1990020
+f A0021 = 1990021
+f A0022 = 1990022
+f A0023 = 1990023
+f A0024 = 1990024
+f A0025 = 1990025
+f A0026 = 1990026
+f A0027 = 1990027
+f A0028 = 1990028
+f A0029 = 1990029
+f A0030 = 1990030
+f A0031 = 1990031
+f A0032 = 1990032
+f A0033 = 1990033
+f A0034 = 1990034
+f A0035 = 1990035
+f A0036 = 1990036
+f A0037 = 1990037
+f A0038 = 1990038
+f A0039 = 1990039
+f A0040 = 1990040
+f A0041 = 1990041
+f A0042 = 1990042
+f A0043 = 1990043
+f A0044 = 1990044
+f A0045 = 1990045
+f A0046 = 1990046
+f A0047 = 1990047
+f A0048 = 1990048
+f A0049 = 1990049
+f A0050 = 1990050
+f A0051 = 1990051
+f A0052 = 1990052
+f A0053 = 1990053
+f A0054 = 1990054
+f A0055 = 1990055
+f A0056 = 1990056
+f A0057 = 1990057
+f A0058 = 1990058
+f A0059 = 1990059
+f A0060 = 1990060
+f A0061 = 1990061
+f A0062 = 1990062
+f A0063 = 1990063
+f A0064 = 1990064
+f A0065 = 1990065
+f A0066 = 1990066
+f A0067 = 1990067
+f A0068 = 1990068
+f A0069 = 1990069
+f A0070 = 1990070
+f A0071 = 1990071
+f A0072 = 1990072
+f A0073 = 1990073
+f A0074 = 1990074
+f A0075 = 1990075
+f A0076 = 1990076
+f A0077 = 1990077
+f A0078 = 1990078
+f A0079 = 1990079
+f A0080 = 1990080
+f A0081 = 1990081
+f A0082 = 1990082
+f A0083 = 1990083
+f A0084 = 1990084
+f A0085 = 1990085
+f A0086 = 1990086
+f A0087 = 1990087
+f A0088 = 1990088
+f A0089 = 1990089
+f A0090 = 1990090
+f A0091 = 1990091
+f A0092 = 1990092
+f A0093 = 1990093
+f A0094 = 1990094
+f A0095 = 1990095
+f A0096 = 1990096
+f A0097 = 1990097
+f A0098 = 1990098
+f A0099 = 1990099
+f A0100 = 1990100
+f A0101 = 1990101
+f A0102 = 1990102
+f A0103 = 1990103
+f A0104 = 1990104
+f A0105 = 1990105
+f A0106 = 1990106
+f A0107 = 1990107
+f A0108 = 1990108
+f A0109 = 1990109
+f A0110 = 1990110
+f A0111 = 1990111
+f A0112 = 1990112
+f A0113 = 1990113
+f A0114 = 1990114
+f A0115 = 1990115
+f A0116 = 1990116
+f A0117 = 1990117
+f A0118 = 1990118
+f A0119 = 1990119
+f A0120 = 1990120
+f A0121 = 1990121
+f A0122 = 1990122
+f A0123 = 1990123
+f A0124 = 1990124
+f A0125 = 1990125
+f A0126 = 1990126
+f A0127 = 1990127
+f A0128 = 1990128
+f A0129 = 1990129
+f A0130 = 1990130
+f A0131 = 1990131
+f A0132 = 1990132
+f A0133 = 1990133
+f A0134 = 1990134
+f A0135 = 1990135
+f A0136 = 1990136
+f A0137 = 1990137
+f A0138 = 1990138
+f A0139 = 1990139
+f A0140 = 1990140
+f A0141 = 1990141
+f A0142 = 1990142
+f A0143 = 1990143
+f A0144 = 1990144
+f A0145 = 1990145
+f A0146 = 1990146
+f A0147 = 1990147
+f A0148 = 1990148
+f A0149 = 1990149
+f A0150 = 1990150
+f A0151 = 1990151
+f A0152 = 1990152
+f A0153 = 1990153
+f A0154 = 1990154
+f A0155 = 1990155
+f A0156 = 1990156
+f A0157 = 1990157
+f A0158 = 1990158
+f A0159 = 1990159
+f A0160 = 1990160
+f A0161 = 1990161
+f A0162 = 1990162
+f A0163 = 1990163
+f A0164 = 1990164
+f A0165 = 1990165
+f A0166 = 1990166
+f A0167 = 1990167
+f A0168 = 1990168
+f A0169 = 1990169
+f A0170 = 1990170
+f A0171 = 1990171
+f A0172 = 1990172
+f A0173 = 1990173
+f A0174 = 1990174
+f A0175 = 1990175
+f A0176 = 1990176
+f A0177 = 1990177
+f A0178 = 1990178
+f A0179 = 1990179
+f A0180 = 1990180
+f A0181 = 1990181
+f A0182 = 1990182
+f A0183 = 1990183
+f A0184 = 1990184
+f A0185 = 1990185
+f A0186 = 1990186
+f A0187 = 1990187
+f A0188 = 1990188
+f A0189 = 1990189
+f A0190 = 1990190
+f A0191 = 1990191
+f A0192 = 1990192
+f A0193 = 1990193
+f A0194 = 1990194
+f A0195 = 1990195
+f A0196 = 1990196
+f A0197 = 1990197
+f A0198 = 1990198
+f A0199 = 1990199
+f A0200 = 1990200
+f A0201 = 1990201
+f A0202 = 1990202
+f A0203 = 1990203
+f A0204 = 1990204
+f A0205 = 1990205
+f A0206 = 1990206
+f A0207 = 1990207
+f A0208 = 1990208
+f A0209 = 1990209
+f A0210 = 1990210
+f A0211 = 1990211
+f A0212 = 1990212
+f A0213 = 1990213
+f A0214 = 1990214
+f A0215 = 1990215
+f A0216 = 1990216
+f A0217 = 1990217
+f A0218 = 1990218
+f A0219 = 1990219
+f A0220 = 1990220
+f A0221 = 1990221
+f A0222 = 1990222
+f A0223 = 1990223
+f A0224 = 1990224
+f A0225 = 1990225
+f A0226 = 1990226
+f A0227 = 1990227
+f A0228 = 1990228
+f A0229 = 1990229
+f A0230 = 1990230
+f A0231 = 1990231
+f A0232 = 1990232
+f A0233 = 1990233
+f A0234 = 1990234
+f A0235 = 1990235
+f A0236 = 1990236
+f A0237 = 1990237
+f A0238 = 1990238
+f A0239 = 1990239
+f A0240 = 1990240
+f A0241 = 1990241
+f A0242 = 1990242
+f A0243 = 1990243
+f A0244 = 1990244
+f A0245 = 1990245
+f A0246 = 1990246
+f A0247 = 1990247
+f A0248 = 1990248
+f A0249 = 1990249
+f A0250 = 1990250
+f A0251 = 1990251
+f A0252 = 1990252
+f A0253 = 1990253
+f A0254 = 1990254
+f A0255 = 1990255
+f A0256 = 1990256
+f A0257 = 1990257
+f A0258 = 1990258
+f A0259 = 1990259
+f A0260 = 1990260
+f A0261 = 1990261
+f A0262 = 1990262
+f A0263 = 1990263
+f A0264 = 1990264
+f A0265 = 1990265
+f A0266 = 1990266
+f A0267 = 1990267
+f A0268 = 1990268
+f A0269 = 1990269
+f A0270 = 1990270
+f A0271 = 1990271
+f A0272 = 1990272
+f A0273 = 1990273
+f A0274 = 1990274
+f A0275 = 1990275
+f A0276 = 1990276
+f A0277 = 1990277
+f A0278 = 1990278
+f A0279 = 1990279
+f A0280 = 1990280
+f A0281 = 1990281
+f A0282 = 1990282
+f A0283 = 1990283
+f A0284 = 1990284
+f A0285 = 1990285
+f A0286 = 1990286
+f A0287 = 1990287
+f A0288 = 1990288
+f A0289 = 1990289
+f A0290 = 1990290
+f A0291 = 1990291
+f A0292 = 1990292
+f A0293 = 1990293
+f A0294 = 1990294
+f A0295 = 1990295
+f A0296 = 1990296
+f A0297 = 1990297
+f A0298 = 1990298
+f A0299 = 1990299
+f A0300 = 1990300
+f A0301 = 1990301
+f A0302 = 1990302
+f A0303 = 1990303
+f A0304 = 1990304
+f A0305 = 1990305
+f A0306 = 1990306
+f A0307 = 1990307
+f A0308 = 1990308
+f A0309 = 1990309
+f A0310 = 1990310
+f A0311 = 1990311
+f A0312 = 1990312
+f A0313 = 1990313
+f A0314 = 1990314
+f A0315 = 1990315
+f A0316 = 1990316
+f A0317 = 1990317
+f A0318 = 1990318
+f A0319 = 1990319
+f A0320 = 1990320
+f A0321 = 1990321
+f A0322 = 1990322
+f A0323 = 1990323
+f A0324 = 1990324
+f A0325 = 1990325
+f A0326 = 1990326
+f A0327 = 1990327
+f A0328 = 1990328
+f A0329 = 1990329
+f A0330 = 1990330
+f A0331 = 1990331
+f A0332 = 1990332
+f A0333 = 1990333
+f A0334 = 1990334
+f A0335 = 1990335
+f A0336 = 1990336
+f A0337 = 1990337
+f A0338 = 1990338
+f A0339 = 1990339
+f A0340 = 1990340
+f A0341 = 1990341
+f A0342 = 1990342
+f A0343 = 1990343
+f A0344 = 1990344
+f A0345 = 1990345
+f A0346 = 1990346
+f A0347 = 1990347
+f A0348 = 1990348
+f A0349 = 1990349
+f A0350 = 1990350
+f A0351 = 1990351
+f A0352 = 1990352
+f A0353 = 1990353
+f A0354 = 1990354
+f A0355 = 1990355
+f A0356 = 1990356
+f A0357 = 1990357
+f A0358 = 1990358
+f A0359 = 1990359
+f A0360 = 1990360
+f A0361 = 1990361
+f A0362 = 1990362
+f A0363 = 1990363
+f A0364 = 1990364
+f A0365 = 1990365
+f A0366 = 1990366
+f A0367 = 1990367
+f A0368 = 1990368
+f A0369 = 1990369
+f A0370 = 1990370
+f A0371 = 1990371
+f A0372 = 1990372
+f A0373 = 1990373
+f A0374 = 1990374
+f A0375 = 1990375
+f A0376 = 1990376
+f A0377 = 1990377
+f A0378 = 1990378
+f A0379 = 1990379
+f A0380 = 1990380
+f A0381 = 1990381
+f A0382 = 1990382
+f A0383 = 1990383
+f A0384 = 1990384
+f A0385 = 1990385
+f A0386 = 1990386
+f A0387 = 1990387
+f A0388 = 1990388
+f A0389 = 1990389
+f A0390 = 1990390
+f A0391 = 1990391
+f A0392 = 1990392
+f A0393 = 1990393
+f A0394 = 1990394
+f A0395 = 1990395
+f A0396 = 1990396
+f A0397 = 1990397
+f A0398 = 1990398
+f A0399 = 1990399
+f A0400 = 1990400
+f A0401 = 1990401
+f A0402 = 1990402
+f A0403 = 1990403
+f A0404 = 1990404
+f A0405 = 1990405
+f A0406 = 1990406
+f A0407 = 1990407
+f A0408 = 1990408
+f A0409 = 1990409
+f A0410 = 1990410
+f A0411 = 1990411
+f A0412 = 1990412
+f A0413 = 1990413
+f A0414 = 1990414
+f A0415 = 1990415
+f A0416 = 1990416
+f A0417 = 1990417
+f A0418 = 1990418
+f A0419 = 1990419
+f A0420 = 1990420
+f A0421 = 1990421
+f A0422 = 1990422
+f A0423 = 1990423
+f A0424 = 1990424
+f A0425 = 1990425
+f A0426 = 1990426
+f A0427 = 1990427
+f A0428 = 1990428
+f A0429 = 1990429
+f A0430 = 1990430
+f A0431 = 1990431
+f A0432 = 1990432
+f A0433 = 1990433
+f A0434 = 1990434
+f A0435 = 1990435
+f A0436 = 1990436
+f A0437 = 1990437
+f A0438 = 1990438
+f A0439 = 1990439
+f A0440 = 1990440
+f A0441 = 1990441
+f A0442 = 1990442
+f A0443 = 1990443
+f A0444 = 1990444
+f A0445 = 1990445
+f A0446 = 1990446
+f A0447 = 1990447
+f A0448 = 1990448
+f A0449 = 1990449
+f A0450 = 1990450
+f A0451 = 1990451
+f A0452 = 1990452
+f A0453 = 1990453
+f A0454 = 1990454
+f A0455 = 1990455
+f A0456 = 1990456
+f A0457 = 1990457
+f A0458 = 1990458
+f A0459 = 1990459
+f A0460 = 1990460
+f A0461 = 1990461
+f A0462 = 1990462
+f A0463 = 1990463
+f A0464 = 1990464
+f A0465 = 1990465
+f A0466 = 1990466
+f A0467 = 1990467
+f A0468 = 1990468
+f A0469 = 1990469
+f A0470 = 1990470
+f A0471 = 1990471
+f A0472 = 1990472
+f A0473 = 1990473
+f A0474 = 1990474
+f A0475 = 1990475
+f A0476 = 1990476
+f A0477 = 1990477
+f A0478 = 1990478
+f A0479 = 1990479
+f A0480 = 1990480
+f A0481 = 1990481
+f A0482 = 1990482
+f A0483 = 1990483
+f A0484 = 1990484
+f A0485 = 1990485
+f A0486 = 1990486
+f A0487 = 1990487
+f A0488 = 1990488
+f A0489 = 1990489
+f A0490 = 1990490
+f A0491 = 1990491
+f A0492 = 1990492
+f A0493 = 1990493
+f A0494 = 1990494
+f A0495 = 1990495
+f A0496 = 1990496
+f A0497 = 1990497
+f A0498 = 1990498
+f A0499 = 1990499
+f A0500 = 1990500
+f A0501 = 1990501
+f A0502 = 1990502
+f A0503 = 1990503
+f A0504 = 1990504
+f A0505 = 1990505
+f A0506 = 1990506
+f A0507 = 1990507
+f A0508 = 1990508
+f A0509 = 1990509
+f A0510 = 1990510
+f A0511 = 1990511
+f A0512 = 1990512
+f A0513 = 1990513
+f A0514 = 1990514
+f A0515 = 1990515
+f A0516 = 1990516
+f A0517 = 1990517
+f A0518 = 1990518
+f A0519 = 1990519
+f A0520 = 1990520
+f A0521 = 1990521
+f A0522 = 1990522
+f A0523 = 1990523
+f A0524 = 1990524
+f A0525 = 1990525
+f A0526 = 1990526
+f A0527 = 1990527
+f A0528 = 1990528
+f A0529 = 1990529
+f A0530 = 1990530
+f A0531 = 1990531
+f A0532 = 1990532
+f A0533 = 1990533
+f A0534 = 1990534
+f A0535 = 1990535
+f A0536 = 1990536
+f A0537 = 1990537
+f A0538 = 1990538
+f A0539 = 1990539
+f A0540 = 1990540
+f A0541 = 1990541
+f A0542 = 1990542
+f A0543 = 1990543
+f A0544 = 1990544
+f A0545 = 1990545
+f A0546 = 1990546
+f A0547 = 1990547
+f A0548 = 1990548
+f A0549 = 1990549
+f A0550 = 1990550
+f A0551 = 1990551
+f A0552 = 1990552
+f A0553 = 1990553
+f A0554 = 1990554
+f A0555 = 1990555
+f A0556 = 1990556
+f A0557 = 1990557
+f A0558 = 1990558
+f A0559 = 1990559
+f A0560 = 1990560
+f A0561 = 1990561
+f A0562 = 1990562
+f A0563 = 1990563
+f A0564 = 1990564
+f A0565 = 1990565
+f A0566 = 1990566
+f A0567 = 1990567
+f A0568 = 1990568
+f A0569 = 1990569
+f A0570 = 1990570
+f A0571 = 1990571
+f A0572 = 1990572
+f A0573 = 1990573
+f A0574 = 1990574
+f A0575 = 1990575
+f A0576 = 1990576
+f A0577 = 1990577
+f A0578 = 1990578
+f A0579 = 1990579
+f A0580 = 1990580
+f A0581 = 1990581
+f A0582 = 1990582
+f A0583 = 1990583
+f A0584 = 1990584
+f A0585 = 1990585
+f A0586 = 1990586
+f A0587 = 1990587
+f A0588 = 1990588
+f A0589 = 1990589
+f A0590 = 1990590
+f A0591 = 1990591
+f A0592 = 1990592
+f A0593 = 1990593
+f A0594 = 1990594
+f A0595 = 1990595
+f A0596 = 1990596
+f A0597 = 1990597
+f A0598 = 1990598
+f A0599 = 1990599
+f A0600 = 1990600
+f A0601 = 1990601
+f A0602 = 1990602
+f A0603 = 1990603
+f A0604 = 1990604
+f A0605 = 1990605
+f A0606 = 1990606
+f A0607 = 1990607
+f A0608 = 1990608
+f A0609 = 1990609
+f A0610 = 1990610
+f A0611 = 1990611
+f A0612 = 1990612
+f A0613 = 1990613
+f A0614 = 1990614
+f A0615 = 1990615
+f A0616 = 1990616
+f A0617 = 1990617
+f A0618 = 1990618
+f A0619 = 1990619
+f A0620 = 1990620
+f A0621 = 1990621
+f A0622 = 1990622
+f A0623 = 1990623
+f A0624 = 1990624
+f A0625 = 1990625
+f A0626 = 1990626
+f A0627 = 1990627
+f A0628 = 1990628
+f A0629 = 1990629
+f A0630 = 1990630
+f A0631 = 1990631
+f A0632 = 1990632
+f A0633 = 1990633
+f A0634 = 1990634
+f A0635 = 1990635
+f A0636 = 1990636
+f A0637 = 1990637
+f A0638 = 1990638
+f A0639 = 1990639
+f A0640 = 1990640
+f A0641 = 1990641
+f A0642 = 1990642
+f A0643 = 1990643
+f A0644 = 1990644
+f A0645 = 1990645
+f A0646 = 1990646
+f A0647 = 1990647
+f A0648 = 1990648
+f A0649 = 1990649
+f A0650 = 1990650
+f A0651 = 1990651
+f A0652 = 1990652
+f A0653 = 1990653
+f A0654 = 1990654
+f A0655 = 1990655
+f A0656 = 1990656
+f A0657 = 1990657
+f A0658 = 1990658
+f A0659 = 1990659
+f A0660 = 1990660
+f A0661 = 1990661
+f A0662 = 1990662
+f A0663 = 1990663
+f A0664 = 1990664
+f A0665 = 1990665
+f A0666 = 1990666
+f A0667 = 1990667
+f A0668 = 1990668
+f A0669 = 1990669
+f A0670 = 1990670
+f A0671 = 1990671
+f A0672 = 1990672
+f A0673 = 1990673
+f A0674 = 1990674
+f A0675 = 1990675
+f A0676 = 1990676
+f A0677 = 1990677
+f A0678 = 1990678
+f A0679 = 1990679
+f A0680 = 1990680
+f A0681 = 1990681
+f A0682 = 1990682
+f A0683 = 1990683
+f A0684 = 1990684
+f A0685 = 1990685
+f A0686 = 1990686
+f A0687 = 1990687
+f A0688 = 1990688
+f A0689 = 1990689
+f A0690 = 1990690
+f A0691 = 1990691
+f A0692 = 1990692
+f A0693 = 1990693
+f A0694 = 1990694
+f A0695 = 1990695
+f A0696 = 1990696
+f A0697 = 1990697
+f A0698 = 1990698
+f A0699 = 1990699
+f A0700 = 1990700
+f A0701 = 1990701
+f A0702 = 1990702
+f A0703 = 1990703
+f A0704 = 1990704
+f A0705 = 1990705
+f A0706 = 1990706
+f A0707 = 1990707
+f A0708 = 1990708
+f A0709 = 1990709
+f A0710 = 1990710
+f A0711 = 1990711
+f A0712 = 1990712
+f A0713 = 1990713
+f A0714 = 1990714
+f A0715 = 1990715
+f A0716 = 1990716
+f A0717 = 1990717
+f A0718 = 1990718
+f A0719 = 1990719
+f A0720 = 1990720
+f A0721 = 1990721
+f A0722 = 1990722
+f A0723 = 1990723
+f A0724 = 1990724
+f A0725 = 1990725
+f A0726 = 1990726
+f A0727 = 1990727
+f A0728 = 1990728
+f A0729 = 1990729
+f A0730 = 1990730
+f A0731 = 1990731
+f A0732 = 1990732
+f A0733 = 1990733
+f A0734 = 1990734
+f A0735 = 1990735
+f A0736 = 1990736
+f A0737 = 1990737
+f A0738 = 1990738
+f A0739 = 1990739
+f A0740 = 1990740
+f A0741 = 1990741
+f A0742 = 1990742
+f A0743 = 1990743
+f A0744 = 1990744
+f A0745 = 1990745
+f A0746 = 1990746
+f A0747 = 1990747
+f A0748 = 1990748
+f A0749 = 1990749
+f A0750 = 1990750
+f A0751 = 1990751
+f A0752 = 1990752
+f A0753 = 1990753
+f A0754 = 1990754
+f A0755 = 1990755
+f A0756 = 1990756
+f A0757 = 1990757
+f A0758 = 1990758
+f A0759 = 1990759
+f A0760 = 1990760
+f A0761 = 1990761
+f A0762 = 1990762
+f A0763 = 1990763
+f A0764 = 1990764
+f A0765 = 1990765
+f A0766 = 1990766
+f A0767 = 1990767
+f A0768 = 1990768
+f A0769 = 1990769
+f A0770 = 1990770
+f A0771 = 1990771
+f A0772 = 1990772
+f A0773 = 1990773
+f A0774 = 1990774
+f A0775 = 1990775
+f A0776 = 1990776
+f A0777 = 1990777
+f A0778 = 1990778
+f A0779 = 1990779
+f A0780 = 1990780
+f A0781 = 1990781
+f A0782 = 1990782
+f A0783 = 1990783
+f A0784 = 1990784
+f A0785 = 1990785
+f A0786 = 1990786
+f A0787 = 1990787
+f A0788 = 1990788
+f A0789 = 1990789
+f A0790 = 1990790
+f A0791 = 1990791
+f A0792 = 1990792
+f A0793 = 1990793
+f A0794 = 1990794
+f A0795 = 1990795
+f A0796 = 1990796
+f A0797 = 1990797
+f A0798 = 1990798
+f A0799 = 1990799
+f A0800 = 1990800
+f A0801 = 1990801
+f A0802 = 1990802
+f A0803 = 1990803
+f A0804 = 1990804
+f A0805 = 1990805
+f A0806 = 1990806
+f A0807 = 1990807
+f A0808 = 1990808
+f A0809 = 1990809
+f A0810 = 1990810
+f A0811 = 1990811
+f A0812 = 1990812
+f A0813 = 1990813
+f A0814 = 1990814
+f A0815 = 1990815
+f A0816 = 1990816
+f A0817 = 1990817
+f A0818 = 1990818
+f A0819 = 1990819
+f A0820 = 1990820
+f A0821 = 1990821
+f A0822 = 1990822
+f A0823 = 1990823
+f A0824 = 1990824
+f A0825 = 1990825
+f A0826 = 1990826
+f A0827 = 1990827
+f A0828 = 1990828
+f A0829 = 1990829
+f A0830 = 1990830
+f A0831 = 1990831
+f A0832 = 1990832
+f A0833 = 1990833
+f A0834 = 1990834
+f A0835 = 1990835
+f A0836 = 1990836
+f A0837 = 1990837
+f A0838 = 1990838
+f A0839 = 1990839
+f A0840 = 1990840
+f A0841 = 1990841
+f A0842 = 1990842
+f A0843 = 1990843
+f A0844 = 1990844
+f A0845 = 1990845
+f A0846 = 1990846
+f A0847 = 1990847
+f A0848 = 1990848
+f A0849 = 1990849
+f A0850 = 1990850
+f A0851 = 1990851
+f A0852 = 1990852
+f A0853 = 1990853
+f A0854 = 1990854
+f A0855 = 1990855
+f A0856 = 1990856
+f A0857 = 1990857
+f A0858 = 1990858
+f A0859 = 1990859
+f A0860 = 1990860
+f A0861 = 1990861
+f A0862 = 1990862
+f A0863 = 1990863
+f A0864 = 1990864
+f A0865 = 1990865
+f A0866 = 1990866
+f A0867 = 1990867
+f A0868 = 1990868
+f A0869 = 1990869
+f A0870 = 1990870
+f A0871 = 1990871
+f A0872 = 1990872
+f A0873 = 1990873
+f A0874 = 1990874
+f A0875 = 1990875
+f A0876 = 1990876
+f A0877 = 1990877
+f A0878 = 1990878
+f A0879 = 1990879
+f A0880 = 1990880
+f A0881 = 1990881
+f A0882 = 1990882
+f A0883 = 1990883
+f A0884 = 1990884
+f A0885 = 1990885
+f A0886 = 1990886
+f A0887 = 1990887
+f A0888 = 1990888
+f A0889 = 1990889
+f A0890 = 1990890
+f A0891 = 1990891
+f A0892 = 1990892
+f A0893 = 1990893
+f A0894 = 1990894
+f A0895 = 1990895
+f A0896 = 1990896
+f A0897 = 1990897
+f A0898 = 1990898
+f A0899 = 1990899
+f A0900 = 1990900
+f A0901 = 1990901
+f A0902 = 1990902
+f A0903 = 1990903
+f A0904 = 1990904
+f A0905 = 1990905
+f A0906 = 1990906
+f A0907 = 1990907
+f A0908 = 1990908
+f A0909 = 1990909
+f A0910 = 1990910
+f A0911 = 1990911
+f A0912 = 1990912
+f A0913 = 1990913
+f A0914 = 1990914
+f A0915 = 1990915
+f A0916 = 1990916
+f A0917 = 1990917
+f A0918 = 1990918
+f A0919 = 1990919
+f A0920 = 1990920
+f A0921 = 1990921
+f A0922 = 1990922
+f A0923 = 1990923
+f A0924 = 1990924
+f A0925 = 1990925
+f A0926 = 1990926
+f A0927 = 1990927
+f A0928 = 1990928
+f A0929 = 1990929
+f A0930 = 1990930
+f A0931 = 1990931
+f A0932 = 1990932
+f A0933 = 1990933
+f A0934 = 1990934
+f A0935 = 1990935
+f A0936 = 1990936
+f A0937 = 1990937
+f A0938 = 1990938
+f A0939 = 1990939
+f A0940 = 1990940
+f A0941 = 1990941
+f A0942 = 1990942
+f A0943 = 1990943
+f A0944 = 1990944
+f A0945 = 1990945
+f A0946 = 1990946
+f A0947 = 1990947
+f A0948 = 1990948
+f A0949 = 1990949
+f A0950 = 1990950
+f A0951 = 1990951
+f A0952 = 1990952
+f A0953 = 1990953
+f A0954 = 1990954
+f A0955 = 1990955
+f A0956 = 1990956
+f A0957 = 1990957
+f A0958 = 1990958
+f A0959 = 1990959
+f A0960 = 1990960
+f A0961 = 1990961
+f A0962 = 1990962
+f A0963 = 1990963
+f A0964 = 1990964
+f A0965 = 1990965
+f A0966 = 1990966
+f A0967 = 1990967
+f A0968 = 1990968
+f A0969 = 1990969
+f A0970 = 1990970
+f A0971 = 1990971
+f A0972 = 1990972
+f A0973 = 1990973
+f A0974 = 1990974
+f A0975 = 1990975
+f A0976 = 1990976
+f A0977 = 1990977
+f A0978 = 1990978
+f A0979 = 1990979
+f A0980 = 1990980
+f A0981 = 1990981
+f A0982 = 1990982
+f A0983 = 1990983
+f A0984 = 1990984
+f A0985 = 1990985
+f A0986 = 1990986
+f A0987 = 1990987
+f A0988 = 1990988
+f A0989 = 1990989
+f A0990 = 1990990
+f A0991 = 1990991
+f A0992 = 1990992
+f A0993 = 1990993
+f A0994 = 1990994
+f A0995 = 1990995
+f A0996 = 1990996
+f A0997 = 1990997
+f A0998 = 1990998
+f A0999 = 1990999
+f A1000 = 1991000
=====================================
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
=====================================
@@ -14,4 +14,6 @@ test('completesig13', normal, compile, [''])
test('completesig14', normal, compile, [''])
test('completesig15', normal, compile_fail, [''])
test('T14059a', normal, compile, [''])
-test('T14253', expect_broken(14253), compile, [''])
+test('T14253', normal, compile, [''])
+test('T13363a', normal, compile, ['-Wall'])
+test('T13363b', normal, compile, ['-Wall'])
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -92,6 +92,14 @@ test('pmc006', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('pmc007', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc008', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc009', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc010', [], compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc011', reqlib('ghc'), compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T11245', [], compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T12949', [], compile, ['-fwarn-overlapping-patterns'])
=====================================
testsuite/tests/pmcheck/should_compile/pmc008.hs
=====================================
@@ -0,0 +1,9 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
+
+module PMC008 where
+
+-- complete match, but because of the guard, the information that `x` is not
+-- `Just` has to flow through the term oracle.
+foo :: Maybe Int -> Int
+foo x | Just y <- x = y
+foo Nothing = 43
=====================================
testsuite/tests/pmcheck/should_compile/pmc009.hs
=====================================
@@ -0,0 +1,7 @@
+module Lib where
+
+data D = A | B
+
+f :: D -> D -> D
+f A A = A
+f B B = B
=====================================
testsuite/tests/pmcheck/should_compile/pmc010.hs
=====================================
@@ -0,0 +1,9 @@
+module Lib where
+
+data D = A | B | C | D
+
+f :: D -> D -> D
+f A A = A
+f B B = B
+f C C = C
+f D D = D
=====================================
testsuite/tests/pmcheck/should_compile/pmc011.hs
=====================================
@@ -0,0 +1,12 @@
+module HsUtils where
+import HsBinds
+import SrcLoc
+
+
+-- | We have to be careful to normalise @SrcSpanLess (LHsBind)@ to
+-- @LHsBindLR l r@ before passing the representative of @unLoc bind@ on to
+-- @mkOneConFull@, otherwise this triggers a panic in @zipTvSubst at .
+addPatSynSelector:: LHsBind p -> [a]
+addPatSynSelector bind
+ | PatSynBind _ _ <- unLoc bind
+ = []
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/e99f15d289bf44ad4c8cecaa266d2ec56c5512bd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/e99f15d289bf44ad4c8cecaa266d2ec56c5512bd
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/20190614/cdca2de7/attachment-0001.html>
More information about the ghc-commits
mailing list