[Git][ghc/ghc][master] 2 commits: PmCheck - Comments only: Replace /~ by ≁
Marge Bot
gitlab at gitlab.haskell.org
Tue Sep 22 09:38:44 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
6fe8a0c7 by Sebastian Graf at 2020-09-22T05:38:35-04:00
PmCheck - Comments only: Replace /~ by ≁
- - - - -
e9501547 by Sebastian Graf at 2020-09-22T05:38:35-04: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` (now called
`generateInhabitingPatterns`) 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` (now called
`inhabitationTest`) 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 generateInhabitingPatterns]`
why we still have tests (1) and (2).
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
`generateInhabitingPatterns` does more work to suggest the minimal
COMPLETE set.
Metric Decrease:
T17836
T17836b
- - - - -
11 changed files:
- 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
- + testsuite/tests/pmcheck/should_compile/T18249.hs
- + testsuite/tests/pmcheck/should_compile/T18249.stderr
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Hs/Expr.hs
=====================================
@@ -1347,8 +1347,10 @@ hsExprNeedsParens p = go
ExpansionExpr (HsExpanded a _) -> hsExprNeedsParens p a
| GhcRn <- ghcPass @p
= case x of HsExpanded a _ -> hsExprNeedsParens p a
+#if __GLASGOW_HASKELL__ <= 900
| otherwise
= True
+#endif
-- | @'parenthesizeHsExpr' p e@ checks if @'hsExprNeedsParens' p e@ is true,
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -221,7 +221,7 @@ safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
exception into divergence (@f x = f x@).
Semantically, unlike every other case expression, -XEmptyCase is strict in its
-match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the
+match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the
initial Nabla and check if there are any values left to match on.
-}
@@ -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 <$> generateInhabitingPatterns 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 /~ ⊥
+ -- 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
+ -- 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)
@@ -1048,7 +1011,7 @@ How do we do that? Consider
And imagine we set our limit to 1 for the sake of the example. The first clause
will be checked against the initial Nabla, {}. Doing so will produce an
-Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}.
+Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}.
Also we find the first clause to cover the model {x~True,y~True}.
But the Uncovered set we get out of the match is too huge! We somehow have to
@@ -1056,8 +1019,8 @@ ensure not to make things worse as they are already, so we continue checking
with a singleton Uncovered set of the initial Nabla {}. Why is this
sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts
to forgetting that we matched against the first clause. The values represented
-by {} are a superset of those represented by its two refinements {x/~True} and
-{x~True,y/~True}.
+by {} are a superset of those represented by its two refinements {x≁True} and
+{x~True,y≁True}.
This forgetfulness becomes very apparent in the example above: By continuing
with {} we don't detect the second clause as redundant, as it again covers the
@@ -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 <- generateInhabitingPatterns 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
@@ -416,7 +417,7 @@ instance Outputable PmEquality where
-- | A data type that caches for the 'VarInfo' of @x@ the results of querying
-- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
--- which we already know @x /~ K@ from these sets.
+-- which we already know @x ≁ K@ from these sets.
--
-- For motivation, see Section 5.3 in Lower Your Guards.
-- See also Note [Implementation of COMPLETE pragmas]
@@ -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
@@ -552,7 +558,7 @@ data VarInfo
-- data T = Leaf Int | Branch T T | Node Int T
-- @
--
- -- then @x /~ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
+ -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
-- and hence can only match @Branch at . Is orthogonal to anything from 'vi_pos',
-- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
-- between 'vi_pos' and 'vi_neg'.
@@ -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,9 @@ instance OutputableBndrId id => Outputable (HsExprArg id) where
ppr (HsEPar _) = text "HsEPar"
ppr (HsEWrap w) = case ghcPass @id of
GhcTc -> text "HsEWrap" <+> ppr w
+#if __GLASGOW_HASKELL__ <= 900
_ -> empty
+#endif
type family XExprTypeArg id where
XExprTypeArg 'Parsed = NoExtField
=====================================
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/-/compare/416bd50e58b23ad70813b18a913ca77a3ab6e936...e9501547a8be6af97bcbf38a7ed66dadf02ea27b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/416bd50e58b23ad70813b18a913ca77a3ab6e936...e9501547a8be6af97bcbf38a7ed66dadf02ea27b
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/20200922/4e7dda3e/attachment-0001.html>
More information about the ghc-commits
mailing list