[Git][ghc/ghc][wip/T18341] Fix the regression in T12227
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Aug 31 16:21:34 UTC 2020
Sebastian Graf pushed to branch wip/T18341 at Glasgow Haskell Compiler / GHC
Commits:
d399d072 by Sebastian Graf at 2020-08-31T18:20:16+02:00
Fix the regression in T12227
By
* Making constructor constraints `x <- K y` strict in `x` again
* Bringing back `initPossibleMatches` in `addNotConCt`
- - - - -
2 changed files:
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
Changes:
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -152,10 +152,14 @@ covCheckMatches
-> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and
-- GRHS, for long distance info.
covCheckMatches ctxt vars matches = do
- missing <- getPmNablas
- tracePm "covCheckMatches {" (hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
- 2
- (vcat (map ppr matches) $$ ppr missing))
+ -- We have to force @missing@ before printing out the trace message,
+ -- otherwise we get interleaved output from the solver. This function
+ -- should be strict in @missing@ anyway!
+ !missing <- getPmNablas
+ tracePm "covCheckMatches {" $
+ hang (vcat [ppr ctxt, ppr vars, text "Matches:"])
+ 2
+ (vcat (map ppr matches) $$ ppr missing)
case NE.nonEmpty matches of
Nothing -> do
-- This must be an -XEmptyCase. See Note [Checking EmptyCase]
@@ -419,29 +423,27 @@ mkPmLetVar x y | x == y = []
mkPmLetVar x y = [PmLet x (Var y)]
-- | ADT constructor pattern => no existentials, no local constraints
-vanillaConGrds :: Id -> DataCon -> [Id] -> GrdVec
-vanillaConGrds scrut con arg_ids =
- [ PmBang scrut Nothing
- , PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
- , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
- ]
+vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
+vanillaConGrd scrut con arg_ids =
+ PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
+ , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
-- | Creates a 'GrdVec' refining a match var of list type to a list,
-- where list fields are matched against the incoming tagged 'GrdVec's.
-- For example:
-- @mkListGrds "a" "[(x, True <- x),(y, !y)]"@
-- to
--- @"[!a, (x:b) <- a, !x, True <- x, !b, (y:c) <- b, !y, !c, [] <- c]"@
+-- @"[(x:b) <- a, True <- x, (y:c) <- b, !y, [] <- c]"@
-- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match
-- variable.
mkListGrds :: Id -> [(Id, GrdVec)] -> DsM GrdVec
-- See Note [Order of guards matter] for why we need to intertwine guards
-- on list elements.
-mkListGrds a [] = pure (vanillaConGrds a nilDataCon [])
+mkListGrds a [] = pure [vanillaConGrd a nilDataCon []]
mkListGrds a ((x, head_grds):xs) = do
b <- mkPmId (idType a)
tail_grds <- mkListGrds b xs
- pure $ vanillaConGrds a consDataCon [x, b] ++ head_grds ++ tail_grds
+ pure $ vanillaConGrd a consDataCon [x, b] : head_grds ++ tail_grds
-- | Create a 'GrdVec' refining a match variable to a 'PmLit'.
mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
@@ -457,13 +459,12 @@ mkPmLitGrds x (PmLit _ (PmLitString s)) = do
char_grdss <- zipWithM mk_char_lit vars (unpackFS s)
mkListGrds x (zip vars char_grdss)
mkPmLitGrds x lit = do
- let con = PmAltLit lit
- grd = PmCon { pm_id = x
+ let grd = PmCon { pm_id = x
, pm_con_con = PmAltLit lit
, pm_con_tvs = []
, pm_con_dicts = []
, pm_con_args = [] }
- pure (conMatchStrictGrds con x ++ [grd])
+ pure [grd]
-- | @desugarPat _ x pat@ transforms @pat@ into a 'GrdVec', where
-- the variable representing the match is @x at .
@@ -499,11 +500,11 @@ desugarPat x pat = case pat of
-- (n + k) ===> let b = x >= k, True <- b, let n = x-k
NPlusKPat _pat_ty (L _ n) k1 k2 ge minus -> do
b <- mkPmId boolTy
- let grd_b = vanillaConGrds b trueDataCon []
+ let grd_b = vanillaConGrd b trueDataCon []
[ke1, ke2] <- traverse dsOverLit [unLoc k1, k2]
rhs_b <- dsSyntaxExpr ge [Var x, ke1]
rhs_n <- dsSyntaxExpr minus [Var x, ke2]
- pure $ PmLet b rhs_b : grd_b ++ [PmLet n rhs_n]
+ pure [PmLet b rhs_b, grd_b, PmLet n rhs_n]
-- (fun -> pat) ===> let y = fun x, pat <- y where y is a match var of pat
ViewPat _arg_ty lexpr pat -> do
@@ -582,13 +583,13 @@ desugarPat x pat = case pat of
TuplePat _tys pats boxity -> do
(vars, grdss) <- mapAndUnzipM desugarLPatV pats
let tuple_con = tupleDataCon boxity (length vars)
- pure $ vanillaConGrds x tuple_con vars ++ concat grdss
+ pure $ vanillaConGrd x tuple_con vars : concat grdss
SumPat _ty p alt arity -> do
(y, grds) <- desugarLPatV p
let sum_con = sumDataCon alt arity
-- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
- pure $ vanillaConGrds x sum_con [y] ++ grds
+ pure $ vanillaConGrd x sum_con [y] : grds
SplicePat {} -> panic "Check.desugarPat: SplicePat"
@@ -614,11 +615,6 @@ desugarListPat x pats = do
vars_and_grdss <- traverse desugarLPatV pats
mkListGrds x vars_and_grdss
-conMatchStrictGrds :: PmAltCon -> Id -> GrdVec
-conMatchStrictGrds con x
- | isPmAltConMatchStrict con = [PmBang x Nothing]
- | otherwise = []
-
-- | Desugar a constructor pattern
desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
-> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec
@@ -642,33 +638,31 @@ desugarConPatOut x con univ_tys ex_tvs dicts = \case
go_field_pats tagged_pats = do
-- The fields that appear might not be in the correct order. So
- -- 1. Add a bang that forces the match var if 'isPmAltConMatchStrict'.
- -- 2. Do the PmCon match
- -- 3. Then pattern match on the fields in the order given by the first
+ -- 1. Do the PmCon match
+ -- 2. Then pattern match on the fields in the order given by the first
-- field of @tagged_pats at .
-- See Note [Field match order for RecCon]
-- Desugar the mentioned field patterns. We're doing this first to get
- -- the Ids for pm_con_args.
+ -- the Ids for pm_con_args and bring them in order afterwards.
let trans_pat (n, pat) = do
(var, pvec) <- desugarLPatV pat
pure ((n, var), pvec)
(tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats
- let alt_con = PmAltConLike con
- get_pat_id n ty = case lookup n tagged_vars of
+ let get_pat_id n ty = case lookup n tagged_vars of
Just var -> pure var
Nothing -> mkPmId ty
- -- the constructor pattern match itself
+ -- 1. the constructor pattern match itself
arg_ids <- zipWithM get_pat_id [0..] arg_tys
- let con_grd = PmCon x alt_con ex_tvs dicts arg_ids
+ let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
- -- guards from field selector patterns
+ -- 2. guards from field selector patterns
let arg_grds = concat arg_grdss
-- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids)
- pure (conMatchStrictGrds alt_con x ++ con_grd : arg_grds)
+ pure (con_grd : arg_grds)
desugarPatBind :: SrcSpan -> Id -> Pat GhcTc -> DsM GrdPatBind
-- See 'GrdPatBind' for how this simply repurposes GrdGRHS.
@@ -753,10 +747,10 @@ desugarBoolGuard e
Var y
| Nothing <- isDataConId_maybe y
-- Omit the let by matching on y
- -> pure (vanillaConGrds y trueDataCon [])
+ -> pure [vanillaConGrd y trueDataCon []]
rhs -> do
x <- mkPmId boolTy
- pure $ PmLet x rhs : vanillaConGrds x trueDataCon []
+ pure [PmLet x rhs, vanillaConGrd x trueDataCon []]
{- Note [Field match order for RecCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -768,13 +762,11 @@ the pattern match. For example:
f T{ b = 42, a = 'a' } = ()
Then @f (T (error "a") (error "b"))@ errors out with "b" because it is mentioned
-frist in the pattern match.
+first in the pattern match.
This means we can't just desugar the pattern match to
-@[!x, T a b <- x, 'a' <- a, 42 <- b]@. Instead we have to force them in the
-right order: @[!x, T a b <- x, 42 <- b, 'a' <- a]@.
-Note the preceding bang guards on the match var: They are necessary for DataCons
-as PmCon guards match lazily.
+@[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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -983,11 +975,14 @@ checkGrd grd = CA $ \inc -> case grd of
, 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)
+ else pure mempty
let con_cts = pmConCts x con tvs dicts args
- matched <- addPmCtsNablas inc con_cts
- uncov <- addPmCtNablas inc (PmNotConCt x con)
+ !matched <- addPmCtsNablas inc con_cts
+ !uncov <- addPmCtNablas inc (PmNotConCt x con)
-- tracePm "checkGrd:Con" (ppr inc $$ ppr grd $$ ppr con_cts $$ ppr matched)
- pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched }
+ pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div }
, cr_uncov = uncov
, cr_approx = Precise }
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -903,7 +903,11 @@ addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
addNotConCt _ _ (PmAltConLike (RealDataCon dc))
| isNewDataCon dc = mzero -- (4) in Note [Coverage checking Newtype matches]
addNotConCt nabla at MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do
- let vi@(VI _ pos neg _ pm) = lookupVarInfo ts x
+ -- For good performance, it's important to initPossibleMatches here.
+ -- Otherwise we can't mark nalt as matched later on, incurring unnecessary
+ -- inhabitation tests for nalt.
+ vi@(VI _ pos neg _ pm) <- lift $ initPossibleMatches (nabla_ty_st nabla)
+ (lookupVarInfo ts x)
-- 1. Bail out quickly when nalt contradicts a solution
let contradicts nalt (cl, _tvs, _args) = eqPmAltCon cl nalt == Equal
guard (not (any (contradicts nalt) pos))
@@ -915,11 +919,12 @@ addNotConCt nabla at MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do
-- See Note [Completeness checking with required Thetas]
| hasRequiredTheta nalt = neg
| otherwise = extendPmAltConSet neg nalt
- let vi1 = vi{ vi_neg = neg' }
+ MASSERT( isPmAltConMatchStrict nalt )
+ let vi1 = vi{ vi_neg = neg', vi_bot = IsNotBot }
-- 3. Make sure there's at least one other possible constructor
vi2 <- case nalt of
PmAltConLike cl
- -> MaybeT (ensureInhabited nabla vi1{ vi_cache = markMatched cl pm })
+ -> ensureInhabited nabla vi1{ vi_cache = markMatched cl pm }
_ -> pure vi1
pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env x vi2) reps }
@@ -993,30 +998,30 @@ addNotBotCt nabla at MkNabla{ nabla_tm_st = TmSt env reps } x = do
IsBot -> mzero -- There was x ~ ⊥. Contradiction!
IsNotBot -> pure nabla -- There already is x /~ ⊥. Nothing left to do
MaybeBot -> do -- We add x /~ ⊥ and test if x is still inhabited
- vi <- MaybeT $ ensureInhabited nabla vi{ vi_bot = IsNotBot }
+ vi <- ensureInhabited nabla vi{ vi_bot = IsNotBot }
pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env y vi) reps}
-ensureInhabited :: Nabla -> VarInfo -> DsM (Maybe VarInfo)
- -- Returns (Just vi) if at least one member of each ConLike in the COMPLETE
- -- set satisfies the oracle
- --
- -- Internally uses and updates the ConLikeSets in vi_cache.
- --
- -- NB: Does /not/ filter each ConLikeSet with the oracle; members may
- -- remain that do not statisfy it. This lazy approach just
- -- avoids doing unnecessary work.
+-- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE
+-- set satisfies the oracle
+--
+-- Internally uses and updates the ConLikeSets in vi_cache.
+--
+-- NB: Does /not/ filter each ConLikeSet with the oracle; members may
+-- remain that do not statisfy it. This lazy approach just
+-- avoids doing unnecessary work.
+ensureInhabited :: Nabla -> VarInfo -> MaybeT DsM VarInfo
ensureInhabited nabla vi = case vi_bot vi of
- MaybeBot -> pure (Just vi) -- The |-Bot rule from the paper
- IsBot -> pure (Just vi)
- IsNotBot -> initPossibleMatches (nabla_ty_st nabla) vi >>= inst_complete_sets
+ MaybeBot -> pure vi -- The |-Bot rule from the paper
+ IsBot -> pure vi
+ IsNotBot -> lift (initPossibleMatches (nabla_ty_st nabla) vi) >>= inst_complete_sets
where
-- | This is the |-Inst rule from the paper (section 4.5). Tries to
-- find an inhabitant in every complete set by instantiating with one their
-- constructors. If there is any complete set where we can't find an
-- inhabitant, the whole thing is uninhabited.
- inst_complete_sets :: VarInfo -> DsM (Maybe VarInfo)
- inst_complete_sets vi at VI{ vi_cache = NoPM } = pure (Just vi)
- inst_complete_sets vi at VI{ vi_cache = PM ms } = runMaybeT $ do
+ inst_complete_sets :: VarInfo -> MaybeT DsM VarInfo
+ inst_complete_sets vi at VI{ vi_cache = NoPM } = pure vi
+ inst_complete_sets vi at VI{ vi_cache = PM ms } = do
ms <- traverse (\cs -> inst_complete_set vi cs (uniqDSetToList cs)) ms
pure vi{ vi_cache = PM ms }
@@ -1061,8 +1066,7 @@ ensureAllInhabited nabla at MkNabla{ nabla_tm_st = TmSt env reps }
= runMaybeT (set_tm_cs_env nabla <$> traverseSDIE go env)
where
set_tm_cs_env nabla env = nabla{ nabla_tm_st = TmSt env reps }
- go vi = MaybeT $
- initPossibleMatches (nabla_ty_st nabla) vi >>= ensureInhabited nabla
+ go vi = ensureInhabited nabla vi
--------------------------------------
-- * Term oracle unification procedure
@@ -1144,17 +1148,18 @@ addConCt nabla at MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x alt tvs args = do
MaybeT $ addPmCts nabla (listToBag ty_cts `unionBags` listToBag tm_cts)
Nothing -> do
let pos' = (alt, tvs, args):pos
- let nabla' = nabla{ nabla_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg bot cache)) reps}
+ let nabla_with bot = nabla{ nabla_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg bot cache)) reps}
-- In case of a newtype constructor, we have to make sure that x ~ ⊥ and
-- x /~ ⊥ constraints now apply to the wrapped thing, as 'lookupVarInfoNT'
-- looks through newtype constructors.
case (alt, args) of
(PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
case bot of
- MaybeBot -> pure nabla'
- IsBot -> addBotCt nabla' y
- IsNotBot -> addNotBotCt nabla' y
- _ -> pure nabla'
+ MaybeBot -> pure (nabla_with MaybeBot)
+ IsBot -> addBotCt (nabla_with MaybeBot) y
+ IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
+ _ -> ASSERT( isPmAltConMatchStrict alt )
+ pure (nabla_with IsNotBot) -- strict match ==> not ⊥
equateTys :: [Type] -> [Type] -> [PmCt]
equateTys ts us =
@@ -1671,7 +1676,7 @@ addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
addCoreCt nabla x e = do
dflags <- getDynFlags
let e' = simpleOptExpr dflags e
- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
+ -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
execStateT (core_expr x e') nabla
where
-- | Takes apart a 'CoreExpr' and tries to extract as much information about
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d399d072b03a8bb5055d194983b83fdfdf3adf9b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d399d072b03a8bb5055d194983b83fdfdf3adf9b
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/20200831/0870d2f9/attachment-0001.html>
More information about the ghc-commits
mailing list