[Git][ghc/ghc][wip/T18249] PmCheck: Rewrite inhabitation test
Sebastian Graf
gitlab at gitlab.haskell.org
Fri Sep 18 13:54:58 UTC 2020
Sebastian Graf pushed to branch wip/T18249 at Glasgow Haskell Compiler / GHC
Commits:
fd453290 by Sebastian Graf at 2020-09-18T15:54:08+02:00
PmCheck: Rewrite inhabitation test
We used to produce inhabitants of a pattern-match refinement type Nabla
in the checker in at least two different and mostly redundant ways:
1. There was `provideEvidence` which is used by `GHC.HsToCore.PmCheck`
to produce non-exhaustive patterns, which produces inhabitants of a
Nabla as a sub-refinement type where all match variables are
instantiated.
2. There also was `ensure{,All}Inhabited` which worked slightly
different, but was whenever new type constraints or negative term
constraints were added. See below why `provideEvidence` and
`ensureAllInhabited` can't be the same function, the main reason
being performance.
3. And last but not least there was the `nonVoid` test, which tested
that a given type was inhabited. We did use this for strict fields
and -XEmptyCase in the past.
The overlap of (3) with (2) was always a major pet peeve of mine. The
latter was quite efficient and proven to work for recursive data types,
etc, but could not handle negative constraints well (e.g. we often want
to know if a *refined* type is empty, such as `{ x:[a] | x /= [] }`).
Lower Your Guards suggested that we could get by with just one, by
replacing both functions with `inhabitationTest` in this patch.
That was only possible by implementing the structure of φ constraints
as in the paper, namely the semantics of φ constructor constraints.
This has a number of benefits:
a. Proper handling of unlifted types and strict fields, fixing #18249,
without any code duplication between
`GHC.HsToCore.PmCheck.Oracle.instCon` (was `mkOneConFull`) and
`GHC.HsToCore.PmCheck.checkGrd`.
b. `instCon` can perform the `nonVoid` test (3) simply by emitting
unliftedness constraints for strict fields.
c. `nonVoid` (3) is thus simply expressed by a call to
`inhabitationTest`.
d. Similarly, `ensureAllInhabited` (2), which we called after adding
type info, now can similarly be expressed as the fuel-based
`inhabitationTest`.
See the new `Note [Why inhabitationTest doesn't call generateInhabitants]`
why we still have to stick to "test" (1).
Fixes #18249 and brings nice metric decreases for `T17836` (-76%) and
`T17836b` (-46%), as well as `T18478` (-8%) at the cost of a few very
minor regressions (< +2%), potentially due to the fact that
`generateInhabitants` is more careful at suggesting the minimal COMPLETE
set.
Metric Decrease:
T17836
T17836b
- - - - -
14 changed files:
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Ppr.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- − compiler/GHC/HsToCore/PmCheck/Types.hs-boot
- compiler/GHC/HsToCore/Types.hs
- compiler/GHC/Tc/Gen/Expr.hs
- + compiler/GHC/Types/Unique/FuelTank.hs
- compiler/ghc.cabal.in
- + testsuite/tests/pmcheck/should_compile/T18249.hs
- + testsuite/tests/pmcheck/should_compile/T18249.stderr
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -161,6 +161,7 @@ import GHC.Types.Basic
import GHC.Types.ForeignCall
import GHC.Types.Name
import GHC.Types.Name.Env
+import GHC.Types.Unique.FuelTank
import GHC.Core.Coercion.Axiom
import GHC.Builtin.Names
import GHC.Data.Maybe
@@ -2747,13 +2748,11 @@ good to be able to unwrap multiple layers.
The function that manages all this is checkRecTc.
-}
-data RecTcChecker = RC !Int (NameEnv Int)
- -- The upper bound, and the number of times
- -- we have encountered each TyCon
+newtype RecTcChecker = RC (FuelTank TyCon)
-- | Initialise a 'RecTcChecker' with 'defaultRecTcMaxBound'.
initRecTc :: RecTcChecker
-initRecTc = RC defaultRecTcMaxBound emptyNameEnv
+initRecTc = RC (initFuelTank defaultRecTcMaxBound)
-- | The default upper bound (100) for the number of times a 'RecTcChecker' is
-- allowed to encounter each 'TyCon'.
@@ -2764,18 +2763,14 @@ defaultRecTcMaxBound = 100
-- | Change the upper bound for the number of times a 'RecTcChecker' is allowed
-- to encounter each 'TyCon'.
setRecTcMaxBound :: Int -> RecTcChecker -> RecTcChecker
-setRecTcMaxBound new_bound (RC _old_bound rec_nts) = RC new_bound rec_nts
+setRecTcMaxBound new_bound (RC tank) = RC (setFuel new_bound tank)
checkRecTc :: RecTcChecker -> TyCon -> Maybe RecTcChecker
-- Nothing => Recursion detected
-- Just rec_tcs => Keep going
-checkRecTc (RC bound rec_nts) tc
- = case lookupNameEnv rec_nts tc_name of
- Just n | n >= bound -> Nothing
- | otherwise -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
- Nothing -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
- where
- tc_name = tyConName tc
+checkRecTc (RC tank) tc = case burnFuel tank tc of
+ OutOfFuel -> Nothing
+ FuelLeft tank' -> Just (RC tank')
-- | Returns whether or not this 'TyCon' is definite, or a hole
-- that may be filled in at some later point. See Note [Skolem abstract data]
=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -1347,8 +1347,11 @@ hsExprNeedsParens p = go
ExpansionExpr (HsExpanded a _) -> hsExprNeedsParens p a
| GhcRn <- ghcPass @p
= case x of HsExpanded a _ -> hsExprNeedsParens p a
+-- TODO: Bump to 900
+#if __GLASGOW_HASKELL__ <= 810
| otherwise
= True
+#endif
-- | @'parenthesizeHsExpr' p e@ checks if @'hsExprNeedsParens' p e@ is true,
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -781,28 +781,6 @@ This means we can't just desugar the pattern match to
@[T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the
right order: @[T a b <- x, 42 <- b, 'a' <- a]@.
-Note [Strict fields and fields of unlifted type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-How do strict fields play into Note [Field match order for RecCon]? Answer:
-They don't. Desugaring is entirely unconcerned by strict fields; the forcing
-happens *before* pattern matching. But for each strict (or more generally,
-unlifted) field @s@ we have to add @s ≁ ⊥@ constraints when we check the PmCon
-guard in 'checkGrd'. Strict fields are devoid of ⊥ by construction, there's
-nothing that a bang pattern would act on. Example from #18341:
-
- data T = MkT !Int
- f :: T -> ()
- f (MkT _) | False = () -- inaccessible
- f (MkT !_) | False = () -- redundant, not only inaccessible!
- f _ = ()
-
-The second clause desugars to @MkT n <- x, !n at . When coverage checked, the
-'PmCon' @MkT n <- x@ refines the set of values that reach the bang pattern with
-the constraints @x ~ MkT n, n ≁ ⊥@ (this list is computed by 'pmConCts').
-Checking the 'PmBang' @!n@ will then try to add the constraint @n ~ ⊥@ to this
-set to get the diverging set, which is found to be empty. Hence the whole
-clause is detected as redundant, as expected.
-
Note [Order of guards matters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Similar to Note [Field match order for RecCon], the order in which the guards
@@ -872,17 +850,17 @@ instance Outputable a => Outputable (CheckResult a) where
field name value = text name <+> equals <+> ppr value
-- | Lift 'addPmCts' over 'Nablas'.
-addPmCtsNablas :: Nablas -> PmCts -> DsM Nablas
-addPmCtsNablas nablas cts = liftNablasM (\d -> addPmCts d cts) nablas
+addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
+addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
-- | 'addPmCtsNablas' for a single 'PmCt'.
-addPmCtNablas :: Nablas -> PmCt -> DsM Nablas
-addPmCtNablas nablas ct = addPmCtsNablas nablas (unitBag ct)
+addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
+addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
-- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
-- we preserve the invariant that there are no uninhabited 'Nabla's. But that
-- could change in the future, for example by implementing this function in
--- terms of @notNull <$> provideEvidence 1 ds at .
+-- terms of @notNull <$> generateInhabitants 1 ds at .
isInhabited :: Nablas -> DsM Bool
isInhabited (MkNablas ds) = pure (not (null ds))
@@ -938,26 +916,6 @@ throttle limit old@(MkNablas old_ds) new@(MkNablas new_ds)
| length new_ds > max limit (length old_ds) = (Approximate, old)
| otherwise = (Precise, new)
--- | The 'PmCts' arising from a successful 'PmCon' match @T gammas as ys <- x at .
--- These include
---
--- * @gammas@: Constraints arising from the bound evidence vars
--- * @y ≁ ⊥@ constraints for each unlifted field (including strict fields)
--- @y@ in @ys@
--- * The constructor constraint itself: @x ~ T as ys at .
---
--- See Note [Strict fields and fields of unlifted type].
-pmConCts :: Id -> PmAltCon -> [TyVar] -> [EvVar] -> [Id] -> PmCts
-pmConCts x con tvs dicts args = gammas `unionBags` unlifted `snocBag` con_ct
- where
- gammas = listToBag $ map (PmTyCt . evVarPred) dicts
- con_ct = PmConCt x con tvs args
- unlifted = listToBag [ PmNotBotCt arg
- | (arg, bang) <-
- zipEqual "pmConCts" args (pmAltConImplBangs con)
- , isBanged bang || isUnliftedType (idType arg)
- ]
-
checkSequence :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree)
-- The implementation is pretty similar to
-- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@
@@ -969,32 +927,37 @@ checkGrd :: PmGrd -> CheckAction RedSets
checkGrd grd = CA $ \inc -> case grd of
-- let x = e: Refine with x ~ e
PmLet x e -> do
- matched <- addPmCtNablas inc (PmCoreCt x e)
- -- tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
+ matched <- addPhiCtNablas inc (PhiCoreCt x e)
+ tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
, cr_uncov = mempty
, cr_approx = Precise }
-- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥
PmBang x mb_info -> do
- div <- addPmCtNablas inc (PmBotCt x)
- matched <- addPmCtNablas inc (PmNotBotCt x)
+ div <- addPhiCtNablas inc (PhiBotCt x)
+ matched <- addPhiCtNablas inc (PhiNotBotCt x)
-- See Note [Dead bang patterns]
-- mb_info = Just info <==> PmBang originates from bang pattern in source
let bangs | Just info <- mb_info = unitOL (div, info)
| otherwise = NilOL
- -- tracePm "check:Bang" (ppr x <+> ppr div)
+ tracePm "check:Bang" (ppr x <+> ppr div)
pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs }
, cr_uncov = mempty
, cr_approx = Precise }
-- Con: Fall through on x ≁ K and refine with x ~ K ys and type info
PmCon x con tvs dicts args -> do
!div <- if isPmAltConMatchStrict con
- then addPmCtNablas inc (PmBotCt x)
+ then addPhiCtNablas inc (PhiBotCt x)
else pure mempty
- let con_cts = pmConCts x con tvs dicts args
- !matched <- addPmCtsNablas inc con_cts
- !uncov <- addPmCtNablas inc (PmNotConCt x con)
- -- tracePm "checkGrd:Con" (ppr inc $$ ppr grd $$ ppr con_cts $$ ppr matched)
+ !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args)
+ !uncov <- addPhiCtNablas inc (PhiNotConCt x con)
+ tracePm "check:Con" $ vcat
+ [ ppr grd
+ , ppr inc
+ , hang (text "div") 2 (ppr div)
+ , hang (text "matched") 2 (ppr matched)
+ , hang (text "uncov") 2 (ppr uncov)
+ ]
pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
, cr_uncov = uncov
, cr_approx = Precise }
@@ -1028,7 +991,7 @@ checkGRHS (PmGRHS { pg_grds = grds, pg_rhs = rhs_info }) =
checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase
checkEmptyCase pe@(PmEmptyCase { pe_var = var }) = CA $ \inc -> do
- unc <- addPmCtNablas inc (PmNotBotCt var)
+ unc <- addPhiCtNablas inc (PhiNotBotCt var)
pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty }
checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post)
@@ -1275,7 +1238,7 @@ getNFirstUncovered vars n (MkNablas nablas) = go n (bagToList nablas)
go 0 _ = pure []
go _ [] = pure []
go n (nabla:nablas) = do
- front <- provideEvidence vars n nabla
+ front <- generateInhabitants vars n nabla
back <- go (n - length front) nablas
pure (front ++ back)
@@ -1415,7 +1378,8 @@ addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
addTyCs origin ev_vars m = do
dflags <- getDynFlags
applyWhen (needToRunPmCheck dflags origin)
- (locallyExtendPmNablas (\nablas -> addPmCtsNablas nablas (PmTyCt . evVarPred <$> ev_vars)))
+ (locallyExtendPmNablas $ \nablas ->
+ addPhiCtsNablas nablas (PhiTyCt . evVarPred <$> ev_vars))
m
-- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment
@@ -1427,7 +1391,7 @@ addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs Nothing _ k = k
addCoreScrutTmCs (Just scr) [x] k =
flip locallyExtendPmNablas k $ \nablas ->
- addPmCtsNablas nablas (unitBag (PmCoreCt x scr))
+ addPhiCtsNablas nablas (unitBag (PhiCoreCt x scr))
addCoreScrutTmCs _ _ _ = panic "addCoreScrutTmCs: scrutinee, but more than one match id"
-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first.
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
The diff for this file was not included because it is too large.
=====================================
compiler/GHC/HsToCore/PmCheck/Ppr.hs
=====================================
@@ -146,8 +146,8 @@ pprPmVar :: PprPrec -> Id -> PmPprM SDoc
pprPmVar prec x = do
nabla <- ask
case lookupSolution nabla x of
- Just (alt, _tvs, args) -> pprPmAltCon prec alt args
- Nothing -> fromMaybe typed_wildcard <$> checkRefuts x
+ Just (PACA alt _tvs args) -> pprPmAltCon prec alt args
+ Nothing -> fromMaybe typed_wildcard <$> checkRefuts x
where
-- if we have no info about the parameter and would just print a
-- wildcard, also show its type.
@@ -206,7 +206,7 @@ pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList
pmExprAsList nabla = go_con []
where
go_var rev_pref x
- | Just (alt, _tvs, args) <- lookupSolution nabla x
+ | Just (PACA alt _tvs args) <- lookupSolution nabla x
= go_con rev_pref alt args
go_var rev_pref x
| Just pref <- nonEmpty (reverse rev_pref)
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs
=====================================
@@ -25,7 +25,7 @@ module GHC.HsToCore.PmCheck.Types (
pmLitAsStringLit, coreExprAsPmLit,
-- * Caching residual COMPLETE sets
- ConLikeSet, ResidualCompleteMatches(..), getRcm,
+ ConLikeSet, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
-- * PmAltConSet
PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
@@ -33,11 +33,11 @@ module GHC.HsToCore.PmCheck.Types (
-- * A 'DIdEnv' where entries may be shared
Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
- setIndirectSDIE, setEntrySDIE, traverseSDIE,
+ setIndirectSDIE, setEntrySDIE, traverseSDIE, entriesSDIE,
-- * The pattern match oracle
- BotInfo(..), VarInfo(..), TmState(..), TyState(..), Nabla(..),
- Nablas(..), initNablas, liftNablasM
+ BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
+ Nabla(..), Nablas(..), initNablas, liftNablasM
) where
#include "HsVersions.h"
@@ -49,6 +49,7 @@ import GHC.Data.Bag
import GHC.Data.FastString
import GHC.Types.Id
import GHC.Types.Var.Env
+import GHC.Types.Var.Set
import GHC.Types.Unique.DSet
import GHC.Types.Unique.DFM
import GHC.Types.Name
@@ -437,6 +438,9 @@ data ResidualCompleteMatches
getRcm :: ResidualCompleteMatches -> [ConLikeSet]
getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
+isRcmInitialised :: ResidualCompleteMatches -> Bool
+isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
+
instance Outputable ResidualCompleteMatches where
-- formats as "[{Nothing,Just},{P,Q}]"
ppr rcm = ppr (getRcm rcm)
@@ -485,6 +489,12 @@ setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE sdie@(SDIE env) x a =
SDIE $ extendDVarEnv env (fst (lookupReprAndEntrySDIE sdie x)) (Entry a)
+entriesSDIE :: SharedDIdEnv a -> [a]
+entriesSDIE (SDIE env) = mapMaybe preview_entry (eltsUDFM env)
+ where
+ preview_entry (Entry e) = Just e
+ preview_entry _ = Nothing
+
traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
traverseSDIE f = fmap (SDIE . listToUDFM_Directly) . traverse g . udfmToList . unSDIE
where
@@ -501,13 +511,6 @@ instance Outputable a => Outputable (Shared a) where
instance Outputable a => Outputable (SharedDIdEnv a) where
ppr (SDIE env) = ppr env
--- | See 'vi_bot'.
-data BotInfo
- = IsBot
- | IsNotBot
- | MaybeBot
- deriving Eq
-
-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
-- entries are possibly shared when we figure out that two variables must be
-- equal, thus represent the same set of values.
@@ -522,6 +525,9 @@ data TmState
-- ^ An environment for looking up whether we already encountered semantically
-- equivalent expressions that we want to represent by the same 'Id'
-- representative.
+ , ts_dirty :: !DIdSet
+ -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
+ -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
}
-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
@@ -532,11 +538,11 @@ data TmState
-- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.PmCheck.Oracle".
data VarInfo
= VI
- { vi_ty :: !Type
- -- ^ The type of the variable. Important for rejecting possible GADT
- -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).
+ { vi_id :: !Id
+ -- ^ The 'Id' in question. Important for adding new constraints relative to
+ -- this 'VarInfo' when we don't easily have the 'Id' available.
- , vi_pos :: ![(PmAltCon, [TyVar], [Id])]
+ , vi_pos :: ![PmAltConApp]
-- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
-- at the same time (i.e. conjunctive). We need a list because of nested
-- pattern matches involving pattern synonym
@@ -576,40 +582,76 @@ data VarInfo
-- to recognise completion of a COMPLETE set efficiently for large enums.
}
+data PmAltConApp
+ = PACA
+ { paca_con :: !PmAltCon
+ , paca_tvs :: ![TyVar]
+ , paca_ids :: ![Id]
+ }
+
+-- | See 'vi_bot'.
+data BotInfo
+ = IsBot
+ | IsNotBot
+ | MaybeBot
+ deriving Eq
+
+instance Outputable PmAltConApp where
+ ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
+ hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
+
instance Outputable BotInfo where
- ppr MaybeBot = empty
+ ppr MaybeBot = underscore
ppr IsBot = text "~⊥"
ppr IsNotBot = text "≁⊥"
-- | Not user-facing.
instance Outputable TmState where
- ppr (TmSt state reps) = ppr state $$ ppr reps
+ ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
-- | Not user-facing.
instance Outputable VarInfo where
- ppr (VI ty pos neg bot cache)
- = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr bot, ppr cache]))
+ ppr (VI x pos neg bot cache)
+ = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache]))
+ where
+ pp_x = ppr x <> dcolon <> ppr (idType x)
+ pp_pos
+ | [] <- pos = underscore
+ | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
+ | otherwise = char '~' <> ppr pos
+ pp_neg
+ | isEmptyPmAltConSet neg = underscore
+ | otherwise = char '≁' <> ppr neg
+ pp_cache
+ | RCM Nothing Nothing <- cache = underscore
+ | otherwise = ppr cache
-- | Initial state of the term oracle.
initTmState :: TmState
-initTmState = TmSt emptySDIE emptyCoreMap
+initTmState = TmSt emptySDIE emptyCoreMap emptyDVarSet
--- | The type oracle state. A poor man's 'GHC.Tc.Solver.Monad.InsertSet': The invariant is
--- that all constraints in there are mutually compatible.
-newtype TyState = TySt InertSet
+-- | The type oracle state. An 'GHC.Tc.Solver.Monad.InsertSet' that we
+-- incrementally add local type constraints to, together with a sequence
+-- number that counts the number of times we extended it with new facts.
+data TyState = TySt { ty_st_n :: !Int, ty_st_inert :: !InertSet }
-- | Not user-facing.
instance Outputable TyState where
- ppr (TySt inert) = ppr inert
+ ppr (TySt n inert) = ppr n <+> ppr inert
initTyState :: TyState
-initTyState = TySt emptyInert
+initTyState = TySt 0 emptyInert
-- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
-- canonical (i.e. mutually compatible) term and type constraints that form the
-- refinement type's predicate.
-data Nabla = MkNabla { nabla_ty_st :: TyState -- Type oracle; things like a~Int
- , nabla_tm_st :: TmState } -- Term oracle; things like x~Nothing
+data Nabla
+ = MkNabla
+ { nabla_ty_st :: !TyState
+ -- ^ Type oracle; things like a~Int
+ , nabla_tm_st :: !TmState
+ -- ^ Term oracle; things like x~Nothing
+ }
-- | An initial nabla that is always satisfiable
initNabla :: Nabla
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs-boot deleted
=====================================
@@ -1,9 +0,0 @@
-module GHC.HsToCore.PmCheck.Types where
-
-import GHC.Data.Bag
-
-data Nabla
-
-newtype Nablas = MkNablas (Bag Nabla)
-
-initNablas :: Nablas
=====================================
compiler/GHC/HsToCore/Types.hs
=====================================
@@ -14,7 +14,7 @@ import GHC.Types.SrcLoc
import GHC.Types.Var
import GHC.Hs (LForeignDecl, HsExpr, GhcTc)
import GHC.Tc.Types (TcRnIf, IfGblEnv, IfLclEnv, CompleteMatches)
-import {-# SOURCE #-} GHC.HsToCore.PmCheck.Types (Nablas)
+import GHC.HsToCore.PmCheck.Types (Nablas)
import GHC.Core (CoreExpr)
import GHC.Core.FamInstEnv
import GHC.Utils.Error
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -1229,7 +1229,10 @@ instance OutputableBndrId id => Outputable (HsExprArg id) where
ppr (HsEPar _) = text "HsEPar"
ppr (HsEWrap w) = case ghcPass @id of
GhcTc -> text "HsEWrap" <+> ppr w
+-- TODO: Bump to 900
+#if __GLASGOW_HASKELL__ <= 810
_ -> empty
+#endif
type family XExprTypeArg id where
XExprTypeArg 'Parsed = NoExtField
=====================================
compiler/GHC/Types/Unique/FuelTank.hs
=====================================
@@ -0,0 +1,41 @@
+-- | Model fuel consumption to detect recursive use of a 'Uniqable' thing.
+module GHC.Types.Unique.FuelTank
+ ( FuelTank, initFuelTank, setFuel, burnFuel, FuelBurntResult(..)
+ ) where
+
+import GHC.Prelude
+
+import GHC.Types.Unique
+import GHC.Types.Unique.FM
+import GHC.Utils.Outputable
+
+data FuelTank uniq
+ = FT
+ { init_fuel :: !Int -- ^ The upper bound of encounters
+ , encounters :: !(UniqFM uniq Int) -- ^ Number of times we have seen a 'u'
+ }
+
+-- | Initialise a 'FuelTank' with the given amount of /fuel/, an upper bound
+-- for how often a given uniquable thing may be encountered.
+initFuelTank :: Int -> FuelTank uniq
+initFuelTank fuel = FT { init_fuel = fuel, encounters = emptyUFM }
+
+-- | Change the upper bound for the number of times a 'FuelTank' is allowed
+-- to encounter each 'TyCon'.
+setFuel :: Int -> FuelTank uniq -> FuelTank uniq
+setFuel new_fuel tank = tank { init_fuel = new_fuel }
+
+data FuelBurntResult uniq
+ = OutOfFuel
+ | FuelLeft !(FuelTank uniq)
+
+-- | Burns one fuel in the 'FuelTank' for the given uniq thing. Returns
+-- 'OutOfFuel' when all fuel was burned and @'FuelLeft' tank@ when there's
+-- still fuel left in the new @tank at .
+burnFuel :: Uniquable uniq => FuelTank uniq -> uniq -> FuelBurntResult uniq
+burnFuel (FT init_fuel encounters) u = case lookupUFM encounters u of
+ Just fuel_used | fuel_used >= init_fuel -> OutOfFuel
+ _ -> FuelLeft (FT init_fuel (addToUFM_C (+) encounters u 1))
+
+instance Outputable (FuelTank u) where
+ ppr (FT init_fuel encounters) = ppr (init_fuel, encounters)
=====================================
compiler/ghc.cabal.in
=====================================
@@ -565,6 +565,7 @@ Library
GHC.Types.Unique.DFM
GHC.Types.Unique.DSet
GHC.Types.Unique.FM
+ GHC.Types.Unique.FuelTank
GHC.Types.Unique.Set
GHC.Utils.Misc
GHC.Cmm.Dataflow
=====================================
testsuite/tests/pmcheck/should_compile/T18249.hs
=====================================
@@ -0,0 +1,36 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+module T18249 where
+
+import GHC.Exts
+
+f :: Int# -> Int
+-- redundant, not just inaccessible!
+f !_ | False = 1
+f _ = 2
+
+newtype UVoid :: TYPE 'UnliftedRep where
+ UVoid :: UVoid -> UVoid
+
+g :: UVoid -> Int
+-- redundant in a weird way:
+-- there's no way to actually write this function.
+-- Inhabitation testing currently doesn't find that UVoid is empty,
+-- but we should be able to detect the bang as redundant.
+g !_ = 1
+
+h :: (# (), () #) -> Int
+-- redundant, not just inaccessible!
+h (# _, _ #) | False = 1
+h _ = 2
+
+i :: Int -> Int
+i !_ | False = 1
+i (I# !_) | False = 2
+i _ = 3
+
=====================================
testsuite/tests/pmcheck/should_compile/T18249.stderr
=====================================
@@ -0,0 +1,20 @@
+
+T18249.hs:14:8: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘f’: f !_ | False = ...
+
+T18249.hs:25:4: warning: [-Wredundant-bang-patterns]
+ Pattern match has redundant bang
+ In an equation for ‘g’: g _ = ...
+
+T18249.hs:29:16: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘h’: h (# _, _ #) | False = ...
+
+T18249.hs:33:13: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘i’: i !_ | False = ...
+
+T18249.hs:34:13: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
+ In an equation for ‘i’: i (I# !_) | False = ...
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -134,6 +134,8 @@ test('T17977b', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18049', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T18249', normal, compile,
+ ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns -Wredundant-bang-patterns'])
test('T18273', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T18341', normal, compile,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fd4532902aec86f8bff6321fd7672ad467bec6cc
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fd4532902aec86f8bff6321fd7672ad467bec6cc
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/20200918/82b020b2/attachment-0001.html>
More information about the ghc-commits
mailing list