[Git][ghc/ghc][wip/T18341] 2 commits: Fix a few bugs
Sebastian Graf
gitlab at gitlab.haskell.org
Thu Jul 2 13:58:45 UTC 2020
Sebastian Graf pushed to branch wip/T18341 at Glasgow Haskell Compiler / GHC
Commits:
f1cf8d5e by Sebastian Graf at 2020-07-02T15:54:13+02:00
Fix a few bugs
- - - - -
d1888d46 by Sebastian Graf at 2020-07-02T15:54:22+02:00
Accept tests
- - - - -
4 changed files:
- compiler/GHC/HsToCore/PmCheck.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs
- testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
Changes:
=====================================
compiler/GHC/HsToCore/PmCheck.hs
=====================================
@@ -992,19 +992,21 @@ checkGrdTree' (Rhs sdoc) deltas = do
-- let x = e: Refine with x ~ e
checkGrdTree' (Guard (PmLet x e) tree) deltas = do
deltas' <- addPmCtDeltas deltas (PmCoreCt x e)
+ tracePm "check:Let" (ppr x <+> char '=' <+> ppr e)
checkGrdTree' tree deltas'
-- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
checkGrdTree' (Guard (PmBang x) tree) deltas = do
has_diverged <- addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
- tracePm "checkGrdTree':PmBang" (ppr deltas $$ ppr has_diverged $$ ppr x)
deltas' <- addPmCtDeltas deltas (PmNotBotCt x)
+ tracePm "check:Bang" (ppr x <+> ppr has_diverged $$ ppr deltas')
res <- checkGrdTree' tree deltas'
pure res{ cr_clauses = applyWhen has_diverged mayDiverge (cr_clauses res) }
-- Con: Fall through on x /~ K, refine with x ~ K ys and type info
checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
- tracePm "checkGrdTree'" (ppr deltas $$ ppr (pmConCts x con tvs dicts args))
- deltas' <- addPmCtsDeltas deltas (pmConCts x con tvs dicts args)
+ let cts = pmConCts x con tvs dicts args
+ tracePm "check:Con" (ppr cts)
+ deltas' <- addPmCtsDeltas deltas cts
CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
limit <- maxPmCheckModels <$> getDynFlags
let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
@@ -1014,6 +1016,7 @@ checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
, cr_approx = prec Semi.<> prec' }
-- Sequence: Thread residual uncovered sets from equation to equation
checkGrdTree' (Sequence l r) unc_0 = do
+ tracePm "check:Sequence:l" (ppr l)
CheckResult l' unc_1 prec_l <- checkGrdTree' l unc_0
CheckResult r' unc_2 prec_r <- checkGrdTree' r unc_1
pure CheckResult
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -518,7 +518,7 @@ tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta ->
Just ty_st' -> do
let delta' = delta{ delta_ty_st = ty_st' }
if recheck_complete_sets
- then ensureAllPossibleMatchesInhabited delta'
+ then ensureAllInhabited delta'
else pure (Just delta')
@@ -705,13 +705,6 @@ initPossibleMatches ty_st vi at VI{ vi_ty = ty, vi_cache = NoPM } = do
Just cs -> pure vi{ vi_ty = ty', vi_cache = PM (mkUniqDSet <$> cs) }
initPossibleMatches _ vi = pure vi
--- | @initLookupVarInfo ts x@ looks up the 'VarInfo' for @x@ in @ts@ and tries
--- to initialise the 'vi_cache' component if it was 'NoPM' through
--- 'initPossibleMatches'.
-initLookupVarInfo :: Delta -> Id -> DsM VarInfo
-initLookupVarInfo MkDelta{ delta_tm_st = ts, delta_ty_st = ty_st } x
- = initPossibleMatches ty_st (lookupVarInfo ts x)
-
{- Note [COMPLETE sets on data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
User-defined COMPLETE sets involving data families are attached to the family
@@ -919,8 +912,8 @@ addBotCt delta at MkDelta{ delta_tm_st = TmSt env reps } x = do
-- that leads to a contradiction.
-- See Note [TmState invariants].
addNotConCt :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta
-addNotConCt delta at MkDelta{ delta_tm_st = TmSt env reps } x nalt = do
- vi@(VI _ pos neg _ pm) <- lift (initLookupVarInfo delta x)
+addNotConCt delta at MkDelta{ delta_tm_st = ts@(TmSt env reps) } x nalt = do
+ let vi@(VI _ pos neg _ pm) = 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))
@@ -932,13 +925,13 @@ addNotConCt delta at MkDelta{ delta_tm_st = TmSt env reps } x nalt = do
-- See Note [Completeness checking with required Thetas]
| hasRequiredTheta nalt = neg
| otherwise = extendPmAltConSet neg nalt
- let vi_ext = vi{ vi_neg = neg' }
+ let vi1 = vi{ vi_neg = neg' }
-- 3. Make sure there's at least one other possible constructor
- vi' <- case nalt of
+ vi2 <- case nalt of
PmAltConLike cl
- -> MaybeT (ensureInhabited delta vi_ext{ vi_cache = markMatched cl pm })
- _ -> pure vi_ext
- pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') reps }
+ -> MaybeT (ensureInhabited delta vi1{ vi_cache = markMatched cl pm })
+ _ -> pure vi1
+ pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi2) reps }
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike cl) = notNull req_theta
@@ -1010,8 +1003,8 @@ addNotBotCt delta at MkDelta{ delta_tm_st = TmSt env reps } x = do
Just True -> mzero -- There was x ~ ⊥. Contradiction!
Just False -> pure delta -- There already is x /~ ⊥. Nothing left to do
Nothing -> do -- We add x /~ ⊥ and test if x is still inhabited
- vi' <- MaybeT $ ensureInhabited delta vi{ vi_bot = Just False }
- pure delta{ delta_tm_st = TmSt (setEntrySDIE env y vi') reps}
+ vi <- MaybeT $ ensureInhabited delta vi{ vi_bot = Just False }
+ pure delta{ delta_tm_st = TmSt (setEntrySDIE env y vi) reps}
ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
-- Returns (Just vi) if at least one member of each ConLike in the COMPLETE
@@ -1024,7 +1017,9 @@ ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
-- avoids doing unnecessary work.
ensureInhabited _ vi at VI{ vi_bot = Nothing } = pure (Just vi)
ensureInhabited _ vi at VI{ vi_bot = Just True } = pure (Just vi)
-ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This would be much less tedious with lenses
+ensureInhabited delta vi = do
+ vi <- initPossibleMatches (delta_ty_st delta) vi
+ fmap (set_cache vi) <$> test (vi_cache vi)
where
set_cache vi cache = vi { vi_cache = cache }
@@ -1059,7 +1054,7 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
-- No need to run the term oracle compared to pmIsSatisfiable
fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
-- Important to pass False to tyIsSatisfiable here, so that we won't
- -- recursively call ensureAllPossibleMatchesInhabited, leading to an
+ -- recursively call ensureAllInhabited, leading to an
-- endless recursion.
[ tyIsSatisfiable False ty_cs
, tysAreNonVoid initRecTc strict_arg_tys
@@ -1069,8 +1064,8 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
-- 'vi_cache', considering the current type information in 'Delta'.
-- This check is necessary after having matched on a GADT con to weed out
-- impossible matches.
-ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
-ensureAllPossibleMatchesInhabited delta at MkDelta{ delta_tm_st = TmSt env reps }
+ensureAllInhabited :: Delta -> DsM (Maybe Delta)
+ensureAllInhabited delta at MkDelta{ delta_tm_st = TmSt env reps }
= runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env)
where
set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env reps }
@@ -1136,8 +1131,8 @@ equate delta at MkDelta{ delta_tm_st = TmSt env reps } x y
--
-- See Note [TmState invariants].
addConCt :: Delta -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Delta
-addConCt delta at MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do
- VI ty pos neg bot cache <- lift (initLookupVarInfo delta x)
+addConCt delta at MkDelta{ delta_tm_st = ts@(TmSt env reps) } x alt tvs args = do
+ let VI ty pos neg bot cache = lookupVarInfo ts x
-- First try to refute with a negative fact
guard (not (elemPmAltConSet alt neg))
-- Then see if any of the other solutions (remember: each of them is an
@@ -1562,7 +1557,7 @@ provideEvidence = go
go [] _ delta = pure [delta]
go (x:xs) n delta = do
tracePm "provideEvidence" (ppr x $$ ppr xs $$ ppr delta $$ ppr n)
- VI _ pos neg _ _ <- initLookupVarInfo delta x
+ let VI _ pos neg _ _ = lookupVarInfo (delta_tm_st delta) x
case pos of
_:_ -> do
-- All solutions must be valid at once. Try to find candidates for their
@@ -1600,8 +1595,9 @@ provideEvidence = go
Nothing -> pure []
Just (y, newty_delta) -> do
-- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥.
- pm <- vi_cache <$> initLookupVarInfo newty_delta y
- mb_cls <- pickMinimalCompleteSet newty_delta pm
+ let vi = lookupVarInfo (delta_tm_st newty_delta) y
+ vi <- initPossibleMatches (delta_ty_st newty_delta) vi
+ mb_cls <- pickMinimalCompleteSet newty_delta (vi_cache vi)
case uniqDSetToList <$> mb_cls of
Just cls@(_:_) -> instantiate_cons y core_ty xs n newty_delta cls
Just [] | not (canDiverge newty_delta y) -> pure []
=====================================
testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs
=====================================
@@ -3,8 +3,10 @@
-- As a result, these functions elicit the symptoms describe in the warnings
-- message, e.g.
-- - False positives on exhaustivity
--- - Turns redundant into inaccessible clauses
-- - Fails to report redundant matches
+--
+-- We used to turn redundant into inaccessible clauses, but SG was unable to
+-- produce a testcase. See the comment below.
module TooManyDeltas where
data T = A | B
@@ -13,12 +15,19 @@ data T = A | B
f :: T -> T -> ()
f A A = ()
+-- SG: As of July 2020, g doesn't reproduce anymore.
+-- Because we treat constructor matches lazily and push data con match
+-- strictness into a preceding bang guard, The single place that calls the
+-- throttling function will not regress in laziness. Note that by throttling we
+-- can only "forget" the x /~ K constraint from unc_this, not the preceding
+-- x /~ ⊥ constraint.
+
-- | Reports that the third clause is inaccessible, when really it is
-- redundant.
g :: T -> T -> ()
g _ A = ()
g A A = () -- inaccessible, correctly flagged
-g A A = () -- redundant, not inaccessible!
+g A A = () -- redundant, used to be inaccessible (see above).
g _ _ = () -- (this one is not about exhaustivity)
-- | Fails to report that the second clause is redundant.
=====================================
testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
=====================================
@@ -1,12 +1,12 @@
-TooManyDeltas.hs:14:1: warning:
+TooManyDeltas.hs:16:1: warning:
Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
• Redundant clauses might not be reported at all
• Redundant clauses might be reported as inaccessible
• Patterns reported as unmatched might actually be matched
Increase the limit or resolve the warnings to suppress this message.
-TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
+TooManyDeltas.hs:16:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’:
Patterns not matched:
@@ -15,17 +15,17 @@ TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
B A
B B
-TooManyDeltas.hs:19:1: warning:
+TooManyDeltas.hs:28:1: warning:
Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
• Redundant clauses might not be reported at all
• Redundant clauses might be reported as inaccessible
• Patterns reported as unmatched might actually be matched
Increase the limit or resolve the warnings to suppress this message.
-TooManyDeltas.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+TooManyDeltas.hs:29:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘g’: g A A = ...
-TooManyDeltas.hs:21:1: warning: [-Woverlapping-patterns (in -Wdefault)]
- Pattern match has inaccessible right hand side
+TooManyDeltas.hs:30:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match is redundant
In an equation for ‘g’: g A A = ...
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/874ab47e9924257eff4887a710a7c62dc51de854...d1888d46e4cbb27f7d0a3ba89bf4f69bfc5776f0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/874ab47e9924257eff4887a710a7c62dc51de854...d1888d46e4cbb27f7d0a3ba89bf4f69bfc5776f0
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/20200702/c0e70e46/attachment-0001.html>
More information about the ghc-commits
mailing list