Commit b03fd3bc authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot

PmCheck: Use ConLikeSet to model negative info

In #17911, Simon recognised many warnings stemming from over-long list
unions while coverage checking Cabal's `LicenseId` module.

This patch introduces a new `PmAltConSet` type which uses a `UniqDSet`
instead of an association list for `ConLike`s. For `PmLit`s, it will
still use an assocation list, though, because a similar map data
structure would entail a lot of busy work.

Fixes #17911.
parent 5cbf9934
Pipeline #16934 failed with stages
in 299 minutes and 12 seconds
...@@ -51,7 +51,6 @@ import GHC.Core.Make (mkListExpr, mkCharExpr) ...@@ -51,7 +51,6 @@ import GHC.Core.Make (mkListExpr, mkCharExpr)
import UniqSupply import UniqSupply
import FastString import FastString
import SrcLoc import SrcLoc
import ListSetOps (unionLists)
import Maybes import Maybes
import GHC.Core.ConLike import GHC.Core.ConLike
import GHC.Core.DataCon import GHC.Core.DataCon
...@@ -613,9 +612,6 @@ Maintaining these invariants in 'addVarCt' (the core of the term oracle) and ...@@ -613,9 +612,6 @@ Maintaining these invariants in 'addVarCt' (the core of the term oracle) and
- (Refine) If we had @x /~ K zs@, unify each y with each z in turn. - (Refine) If we had @x /~ K zs@, unify each y with each z in turn.
* Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addNotConCt') * Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addNotConCt')
- (Refut) If we have @x ~ K ys@, refute. - (Refut) If we have @x ~ K ys@, refute.
- (Redundant) If we have @x ~ K2@ and @eqPmAltCon K K2 == Disjoint@
(ex. Just and Nothing), the info is redundant and can be
discarded.
- (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get - (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get
@x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in @x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in
COMPLETE set, so should refute. COMPLETE set, so should refute.
...@@ -655,7 +651,7 @@ tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM addTmCt delta new_ ...@@ -655,7 +651,7 @@ tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM addTmCt delta new_
-- * Looking up VarInfo -- * Looking up VarInfo
emptyVarInfo :: Id -> VarInfo emptyVarInfo :: Id -> VarInfo
emptyVarInfo x = VI (idType x) [] [] NoPM emptyVarInfo x = VI (idType x) [] emptyPmAltConSet NoPM
lookupVarInfo :: TmState -> Id -> VarInfo lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x' -- (lookupVarInfo tms x) tells what we know about 'x'
...@@ -754,7 +750,7 @@ TyCon, so tc_rep = tc_fam afterwards. ...@@ -754,7 +750,7 @@ TyCon, so tc_rep = tc_fam afterwards.
canDiverge :: Delta -> Id -> Bool canDiverge :: Delta -> Id -> Bool
canDiverge delta@MkDelta{ delta_tm_st = ts } x canDiverge delta@MkDelta{ delta_tm_st = ts } x
| VI _ pos neg _ <- lookupVarInfo ts x | VI _ pos neg _ <- lookupVarInfo ts x
= null neg && all pos_can_diverge pos = isEmptyPmAltConSet neg && all pos_can_diverge pos
where where
pos_can_diverge (PmAltConLike (RealDataCon dc), _, [y]) pos_can_diverge (PmAltConLike (RealDataCon dc), _, [y])
-- See Note [Divergence of Newtype matches] -- See Note [Divergence of Newtype matches]
...@@ -793,8 +789,8 @@ lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon] ...@@ -793,8 +789,8 @@ lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
lookupRefuts MkDelta{ delta_tm_st = ts@(TmSt (SDIE env) _) } k = lookupRefuts MkDelta{ delta_tm_st = ts@(TmSt (SDIE env) _) } k =
case lookupUDFM env k of case lookupUDFM env k of
Nothing -> [] Nothing -> []
Just (Indirect y) -> vi_neg (lookupVarInfo ts y) Just (Indirect y) -> pmAltConSetElems (vi_neg (lookupVarInfo ts y))
Just (Entry vi) -> vi_neg vi Just (Entry vi) -> pmAltConSetElems (vi_neg vi)
isDataConSolution :: (PmAltCon, [TyVar], [Id]) -> Bool isDataConSolution :: (PmAltCon, [TyVar], [Id]) -> Bool
isDataConSolution (PmAltConLike (RealDataCon _), _, _) = True isDataConSolution (PmAltConLike (RealDataCon _), _, _) = True
...@@ -937,7 +933,7 @@ addNotConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do ...@@ -937,7 +933,7 @@ addNotConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do
| any (implies nalt) pos = neg | any (implies nalt) pos = neg
-- See Note [Completeness checking with required Thetas] -- See Note [Completeness checking with required Thetas]
| hasRequiredTheta nalt = neg | hasRequiredTheta nalt = neg
| otherwise = unionLists neg [nalt] | otherwise = extendPmAltConSet neg nalt
let vi_ext = vi{ vi_neg = neg' } let vi_ext = vi{ vi_neg = neg' }
-- 3. Make sure there's at least one other possible constructor -- 3. Make sure there's at least one other possible constructor
vi' <- case nalt of vi' <- case nalt of
...@@ -1129,7 +1125,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y ...@@ -1129,7 +1125,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y
delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x) delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x)
-- Do the same for negative info -- Do the same for negative info
let add_refut delta nalt = addNotConCt delta y nalt let add_refut delta nalt = addNotConCt delta y nalt
delta_neg <- foldlM add_refut delta_pos (vi_neg vi_x) delta_neg <- foldlM add_refut delta_pos (pmAltConSetElems (vi_neg vi_x))
-- vi_cache will be updated in addNotConCt, so we are good to -- vi_cache will be updated in addNotConCt, so we are good to
-- go! -- go!
pure delta_neg pure delta_neg
...@@ -1144,7 +1140,7 @@ addConCt :: Delta -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Delta ...@@ -1144,7 +1140,7 @@ addConCt :: Delta -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Delta
addConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do addConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do
VI ty pos neg cache <- lift (initLookupVarInfo delta x) VI ty pos neg cache <- lift (initLookupVarInfo delta x)
-- First try to refute with a negative fact -- First try to refute with a negative fact
guard (all ((/= Equal) . eqPmAltCon alt) neg) guard (not (elemPmAltConSet alt neg))
-- Then see if any of the other solutions (remember: each of them is an -- Then see if any of the other solutions (remember: each of them is an
-- additional refinement of the possible values x could take) indicate a -- additional refinement of the possible values x could take) indicate a
-- contradiction -- contradiction
...@@ -1160,11 +1156,8 @@ addConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do ...@@ -1160,11 +1156,8 @@ addConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do
let tm_cts = zipWithEqual "addConCt" PmVarCt args other_args let tm_cts = zipWithEqual "addConCt" PmVarCt args other_args
MaybeT $ addPmCts delta (listToBag ty_cts `unionBags` listToBag tm_cts) MaybeT $ addPmCts delta (listToBag ty_cts `unionBags` listToBag tm_cts)
Nothing -> do Nothing -> do
-- Filter out redundant negative facts (those that compare Just False to
-- the new solution)
let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg
let pos' = (alt, tvs, args):pos let pos' = (alt, tvs, args):pos
pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache)) reps} pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg cache)) reps}
equateTys :: [Type] -> [Type] -> [PmCt] equateTys :: [Type] -> [Type] -> [PmCt]
equateTys ts us = equateTys ts us =
...@@ -1553,7 +1546,7 @@ provideEvidence = go ...@@ -1553,7 +1546,7 @@ provideEvidence = go
[] []
-- When there are literals involved, just print negative info -- When there are literals involved, just print negative info
-- instead of listing missed constructors -- instead of listing missed constructors
| notNull [ l | PmAltLit l <- neg ] | notNull [ l | PmAltLit l <- pmAltConSetElems neg ]
-> go xs n delta -> go xs n delta
[] -> try_instantiate x xs n delta [] -> try_instantiate x xs n delta
......
...@@ -24,6 +24,10 @@ module GHC.HsToCore.PmCheck.Types ( ...@@ -24,6 +24,10 @@ module GHC.HsToCore.PmCheck.Types (
-- * Caching partially matched COMPLETE sets -- * Caching partially matched COMPLETE sets
ConLikeSet, PossibleMatches(..), ConLikeSet, PossibleMatches(..),
-- * PmAltConSet
PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
extendPmAltConSet, pmAltConSetElems,
-- * A 'DIdEnv' where entries may be shared -- * A 'DIdEnv' where entries may be shared
Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE, Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
setIndirectSDIE, setEntrySDIE, traverseSDIE, setIndirectSDIE, setEntrySDIE, traverseSDIE,
...@@ -49,6 +53,7 @@ import Name ...@@ -49,6 +53,7 @@ import Name
import GHC.Core.DataCon import GHC.Core.DataCon
import GHC.Core.ConLike import GHC.Core.ConLike
import Outputable import Outputable
import ListSetOps (unionLists)
import Maybes import Maybes
import GHC.Core.Type import GHC.Core.Type
import GHC.Core.TyCon import GHC.Core.TyCon
...@@ -152,6 +157,33 @@ eqConLike _ _ = PossiblyOverlap ...@@ -152,6 +157,33 @@ eqConLike _ _ = PossiblyOverlap
data PmAltCon = PmAltConLike ConLike data PmAltCon = PmAltConLike ConLike
| PmAltLit PmLit | PmAltLit PmLit
data PmAltConSet = PACS !ConLikeSet ![PmLit]
emptyPmAltConSet :: PmAltConSet
emptyPmAltConSet = PACS emptyUniqDSet []
isEmptyPmAltConSet :: PmAltConSet -> Bool
isEmptyPmAltConSet (PACS cls lits) = isEmptyUniqDSet cls && null lits
-- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
-- the given 'PmAltCon' according to 'eqPmAltCon'.
elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
elemPmAltConSet (PmAltConLike cl) (PACS cls _ ) = elementOfUniqDSet cl cls
elemPmAltConSet (PmAltLit lit) (PACS _ lits) = elem lit lits
extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
extendPmAltConSet (PACS cls lits) (PmAltConLike cl)
= PACS (addOneToUniqDSet cls cl) lits
extendPmAltConSet (PACS cls lits) (PmAltLit lit)
= PACS cls (unionLists lits [lit])
pmAltConSetElems :: PmAltConSet -> [PmAltCon]
pmAltConSetElems (PACS cls lits)
= map PmAltConLike (uniqDSetToList cls) ++ map PmAltLit lits
instance Outputable PmAltConSet where
ppr = ppr . pmAltConSetElems
-- | We can't in general decide whether two 'PmAltCon's match the same set of -- | We can't in general decide whether two 'PmAltCon's match the same set of
-- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a -- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a
-- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'. -- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
...@@ -475,7 +507,7 @@ data VarInfo ...@@ -475,7 +507,7 @@ data VarInfo
-- However, no more than one RealDataCon in the list, otherwise contradiction -- However, no more than one RealDataCon in the list, otherwise contradiction
-- because of generativity. -- because of generativity.
, vi_neg :: ![PmAltCon] , vi_neg :: !PmAltConSet
-- ^ Negative info: A list of 'PmAltCon's that it cannot match. -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
-- Example, assuming -- Example, assuming
-- --
...@@ -489,6 +521,9 @@ data VarInfo ...@@ -489,6 +521,9 @@ data VarInfo
-- between 'vi_pos' and 'vi_neg'. -- between 'vi_pos' and 'vi_neg'.
-- See Note [Why record both positive and negative info?] -- See Note [Why record both positive and negative info?]
-- It's worth having an actual set rather than a simple association list,
-- because files like Cabal's `LicenseId` define relatively huge enums
-- that lead to quadratic or worse behavior.
, vi_cache :: !PossibleMatches , vi_cache :: !PossibleMatches
-- ^ A cache of the associated COMPLETE sets. At any time a superset of -- ^ A cache of the associated COMPLETE sets. At any time a superset of
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment