[Git][ghc/ghc][wip/T14422] PmCheck: Look up COMPLETE pragmas by constituent ConLikes
Sebastian Graf
gitlab at gitlab.haskell.org
Tue Sep 1 17:57:59 UTC 2020
Sebastian Graf pushed to branch wip/T14422 at Glasgow Haskell Compiler / GHC
Commits:
ff8ff6b0 by Sebastian Graf at 2020-09-01T19:57:47+02:00
PmCheck: Look up COMPLETE pragmas by constituent ConLikes
By having a way to look up COMPLETE pragmas from one of their ConLikes,
we can drastically simplify the logic that tries to initialise available
COMPLETE sets of a variable during the pattern-match checking process,
as well as fixing a few bugs.
- - - - -
13 changed files:
- compiler/GHC/Driver/Types.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- compiler/GHC/Iface/Load.hs
- compiler/GHC/Iface/Make.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Utils/Env.hs
- compiler/GHC/Types/Name/Occurrence.hs
- compiler/GHC/Types/Unique/DFM.hs
- docs/users_guide/exts/pragmas.rst
Changes:
=====================================
compiler/GHC/Driver/Types.hs
=====================================
@@ -146,7 +146,7 @@ module GHC.Driver.Types (
handleFlagWarnings, printOrThrowWarnings,
-- * COMPLETE signature
- CompleteMatch(..), CompleteMatchMap,
+ ConLikeSet, CompleteMatch(..), CompleteMatchMap,
mkCompleteMatchMap, extendCompleteMatchMap,
-- * Exstensible Iface fields
@@ -2746,9 +2746,10 @@ data ExternalPackageState
-- from all the external-package modules
eps_ann_env :: !PackageAnnEnv, -- ^ The total 'AnnEnv' accumulated
-- from all the external-package modules
- eps_complete_matches :: !PackageCompleteMatchMap,
+ eps_complete_matches :: PackageCompleteMatchMap,
-- ^ The total 'CompleteMatchMap' accumulated
-- from all the external-package modules
+ -- may only be forced /after/ type-checking
eps_mod_fam_inst_env :: !(ModuleEnv FamInstEnv), -- ^ The family instances accumulated from external
-- packages, keyed off the module that declared them
@@ -3203,36 +3204,47 @@ byteCodeOfObject other = pprPanic "byteCodeOfObject" (ppr other)
-------------------------------------------
+type ConLikeSet = UniqDSet ConLike
+
-- | A list of conlikes which represents a complete pattern match.
-- These arise from @COMPLETE@ signatures.
-
+--
-- See Note [Implementation of COMPLETE signatures]
-data CompleteMatch = CompleteMatch {
- completeMatchConLikes :: [Name]
- -- ^ The ConLikes that form a covering family
- -- (e.g. Nothing, Just)
- , completeMatchTyCon :: Name
- -- ^ The TyCon that they cover (e.g. Maybe)
- }
+data CompleteMatch
+ = CompleteMatch
+ { completeMatchName :: !Name
+ -- ^ A Name for this @COMPLETE@ sig. We only need the 'Unique', but the name
+ -- is needed for serialising to interface files. Thus always a proxy name
+ -- like @$CL_a1bz at .
+ , completeMatchConLikes :: ConLikeSet
+ -- ^ The ConLikes that form a covering family (e.g. Nothing, Just)
+ -- Needs to be lazy, because it's lazily loaded from interface files and only
+ -- type-checked after we already accessed 'completeMatchName'.
+ }
instance Outputable CompleteMatch where
- ppr (CompleteMatch cl ty) = text "CompleteMatch:" <+> ppr cl
- <+> dcolon <+> ppr ty
-
--- | A map keyed by the 'completeMatchTyCon' which has type Name.
+ ppr (CompleteMatch n cls) = text "CompleteMatch(" <> ppr n <> text "):"
+ <+> ppr cls
+-- | A map associating 'ConLike's to 'CompleteMatch'es in which they
+-- occur.
+--
-- See Note [Implementation of COMPLETE signatures]
-type CompleteMatchMap = UniqFM Name [CompleteMatch]
+type CompleteMatchMap = UniqDFM ConLike [CompleteMatch]
mkCompleteMatchMap :: [CompleteMatch] -> CompleteMatchMap
-mkCompleteMatchMap = extendCompleteMatchMap emptyUFM
+mkCompleteMatchMap = extendCompleteMatchMap emptyUDFM
extendCompleteMatchMap :: CompleteMatchMap -> [CompleteMatch]
-> CompleteMatchMap
-extendCompleteMatchMap = foldl' insertMatch
+extendCompleteMatchMap = foldl' go_over_cls
where
- insertMatch :: CompleteMatchMap -> CompleteMatch -> CompleteMatchMap
- insertMatch ufm c@(CompleteMatch _ t) = addToUFM_C (++) ufm t [c]
+ go_over_cls :: CompleteMatchMap -> CompleteMatch -> CompleteMatchMap
+ go_over_cls udfm c@(CompleteMatch _ cls) =
+ foldl' (go_over_cl c) udfm (uniqDSetToList cls)
+ go_over_cl :: CompleteMatch -> CompleteMatchMap -> ConLike -> CompleteMatchMap
+ go_over_cl c udfm cl =
+ addToUDFM_C (\old _new -> c:old) udfm cl [c]
{-
Note [Implementation of COMPLETE signatures]
=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -88,7 +88,7 @@ import GHC.Driver.Ppr
import GHC.Utils.Error
import GHC.Utils.Panic
import GHC.Data.FastString
-import GHC.Types.Unique.FM ( lookupWithDefaultUFM_Directly )
+import GHC.Types.Unique.DFM ( lookupWithDefaultUDFM )
import GHC.Types.Literal ( mkLitString )
import GHC.Types.CostCentre.State
@@ -534,14 +534,12 @@ dsGetMetaEnv :: DsM (NameEnv DsMetaVal)
dsGetMetaEnv = do { env <- getLclEnv; return (dsl_meta env) }
-- | The @COMPLETE@ pragmas provided by the user for a given `TyCon`.
-dsGetCompleteMatches :: TyCon -> DsM [CompleteMatch]
-dsGetCompleteMatches tc = do
+dsGetCompleteMatches :: ConLike -> DsM [CompleteMatch]
+dsGetCompleteMatches cl = do
eps <- getEps
env <- getGblEnv
- -- We index into a UniqFM from Name -> elt, for tyCon it holds that
- -- getUnique (tyConName tc) == getUnique tc. So we lookup using the
- -- unique directly instead.
- let lookup_completes ufm = lookupWithDefaultUFM_Directly ufm [] (getUnique tc)
+ let lookup_completes :: CompleteMatchMap -> [CompleteMatch]
+ lookup_completes udfm = lookupWithDefaultUDFM udfm [] cl
eps_matches_list = lookup_completes $ eps_complete_matches eps
env_matches_list = lookup_completes $ ds_complete_matches env
return $ eps_matches_list ++ env_matches_list
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -66,7 +66,7 @@ import GHC.Core.TyCo.Rep
import GHC.Core.Type
import GHC.Tc.Solver (tcNormalise, tcCheckSatisfiability)
import GHC.Core.Unify (tcMatchTy)
-import GHC.Tc.Types (completeMatchConLikes)
+import GHC.Tc.Types (CompleteMatch(..))
import GHC.Core.Coercion
import GHC.Utils.Monad hiding (foldlM)
import GHC.HsToCore.Monad hiding (foldlM)
@@ -80,7 +80,6 @@ import Data.Bifunctor (second)
import Data.Either (partitionEithers)
import Data.Foldable (foldlM, minimumBy, toList)
import Data.List (find)
-import qualified Data.List.NonEmpty as NonEmpty
import Data.Ord (comparing)
import qualified Data.Semigroup as Semigroup
import Data.Tuple (swap)
@@ -105,11 +104,57 @@ mkPmId ty = getUniqueM >>= \unique ->
-----------------------------------------------
-- * Caching possible matches of a COMPLETE set
-markMatched :: ConLike -> PossibleMatches -> PossibleMatches
-markMatched _ NoPM = NoPM
-markMatched con (PM ms) = PM (del_one_con con <$> ms)
- where
- del_one_con = flip delOneFromUniqDSet
+-- | A pseudo-'CompleteMatch' for the vanilla complete set of the data defn of
+-- the given 'DataCon'.
+-- Ex.: @vanillaCompleteMatchDC 'Just' ==> ("Maybe", {'Just','Nothing'})@
+vanillaCompleteMatchDC :: DataCon -> CompleteMatch
+vanillaCompleteMatchDC dc =
+ expectJust "vanillaCompleteMatchDC" $ vanillaCompleteMatchTC (dataConTyCon dc)
+
+-- | A pseudo-'CompleteMatch' for the vanilla complete set of the given data
+-- 'TyCon'.
+-- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
+vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
+vanillaCompleteMatchTC tc =
+ let -- | TYPE acts like an empty data type on the term-level (#14086), but
+ -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
+ -- special case.
+ mb_dcs | tc == tYPETyCon = Just []
+ | otherwise = tyConDataCons_maybe tc
+ -- | Using the Name of the TyCon instead of a Name of an actual
+ -- CompleteMatches here is OK, since they're in the same Occ NameSpace
+ -- and thus can't clash.
+ nm = getName tc
+ in CompleteMatch nm . mkUniqDSet . map RealDataCon <$> mb_dcs
+
+-- | Adds the 'CompleteMatches' that the 'ConLike' is part of to the
+-- 'ResidualCompleteMatches', if not already present. We can identify two
+-- 'CompleteMatches' by their 'Name', which conveniently is the index of
+-- the Map in 'ResidualCompleteMatches'.
+addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
+addConLikeMatches cl (RCM cmpls) = do
+ tracePm "get cmpl" empty
+ cs <- dsGetCompleteMatches cl
+ -- Add the vanilla COMPLETE set from the data defn
+ let cs' = case cl of
+ RealDataCon dc -> vanillaCompleteMatchDC dc : cs
+ _ -> cs
+ pure $ RCM $ addListToUDFM_C (\old _new -> old) cmpls
+ [ (n, c) | CompleteMatch n c <- cs' ]
+
+-- | Adds the /vanilla/ 'CompleteMatches' of the data 'TyCon' to the
+-- 'ResidualCompleteMatches', if not already present.
+-- Like 'addConLikeMatches', but based on the data 'TyCon' and adds
+-- only the vanilla COMPLETE set.
+addTyConMatches :: TyCon -> ResidualCompleteMatches -> ResidualCompleteMatches
+addTyConMatches tc rcm@(RCM cmpls) = case vanillaCompleteMatchTC tc of
+ Nothing -> rcm
+ Just (CompleteMatch n c) -> RCM $ addToUDFM_C (\old _new -> old) cmpls n c
+
+markMatched :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
+markMatched cl rcm = do
+ RCM cmpl <- addConLikeMatches cl rcm
+ pure $ RCM (flip delOneFromUniqDSet cl <$> cmpl)
---------------------------------------------------
-- * Instantiating constructors, types and evidence
@@ -492,7 +537,7 @@ tyOracle (TySt inert) cts
-- | A 'SatisfiabilityCheck' based on new type-level constraints.
-- Returns a new 'Nabla' if the new constraints are compatible with existing
-- ones. Doesn't bother calling out to the type oracle if the bag of new type
--- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle
+-- constraints was empty. Will only recheck 'ResidualCompleteMatches' in the term oracle
-- for emptiness if the first argument is 'True'.
tyIsSatisfiable :: Bool -> Bag PredType -> SatisfiabilityCheck
tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \nabla ->
@@ -624,13 +669,16 @@ tmIsSatisfiable new_tm_cs = SC $ \nabla -> runMaybeT $ foldlM addTmCt nabla new_
-----------------------
-- * Looking up VarInfo
+emptyRCM :: ResidualCompleteMatches
+emptyRCM = RCM emptyUDFM
+
emptyVarInfo :: Id -> VarInfo
-- We could initialise @bot@ to @Just False@ in case of an unlifted type here,
-- but it's cleaner to let the user of the constraint solver take care of this.
-- After all, there are also strict fields, the unliftedness of which isn't
-- evident in the type. So treating unlifted types here would never be
-- sufficient anyway.
-emptyVarInfo x = VI (idType x) [] emptyPmAltConSet MaybeBot NoPM
+emptyVarInfo x = VI (idType x) [] emptyPmAltConSet MaybeBot emptyRCM
lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x'
@@ -656,85 +704,6 @@ lookupVarInfoNT ts x = case lookupVarInfo ts x of
| isNewDataCon dc = Just y
go _ = Nothing
-initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
-initPossibleMatches ty_st vi at VI{ vi_ty = ty, vi_cache = NoPM } = do
- -- New evidence might lead to refined info on ty, in turn leading to discovery
- -- of a COMPLETE set.
- res <- pmTopNormaliseType ty_st ty
- let ty' = normalisedSourceType res
- case splitTyConApp_maybe ty' of
- Nothing -> pure vi{ vi_ty = ty' }
- Just (tc, [_])
- | tc == tYPETyCon
- -- TYPE acts like an empty data type on the term-level (#14086), but
- -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
- -- special case.
- -> pure vi{ vi_ty = ty', vi_cache = PM (pure emptyUniqDSet) }
- Just (tc, tc_args) -> do
- -- See Note [COMPLETE sets on data families]
- (tc_rep, tc_fam) <- case tyConFamInst_maybe tc of
- Just (tc_fam, _) -> pure (tc, tc_fam)
- Nothing -> do
- env <- dsGetFamInstEnvs
- let (tc_rep, _tc_rep_args, _co) = tcLookupDataFamInst env tc tc_args
- pure (tc_rep, tc)
- -- Note that the common case here is tc_rep == tc_fam
- let mb_rdcs = map RealDataCon <$> tyConDataCons_maybe tc_rep
- let rdcs = maybeToList mb_rdcs
- -- NB: tc_fam, because COMPLETE sets are associated with the parent data
- -- family TyCon
- pragmas <- dsGetCompleteMatches tc_fam
- let fams = mapM dsLookupConLike . completeMatchConLikes
- pscs <- mapM fams pragmas
- -- pprTrace "initPossibleMatches" (ppr ty $$ ppr ty' $$ ppr tc_rep <+> ppr tc_fam <+> ppr tc_args $$ ppr (rdcs ++ pscs)) (return ())
- case NonEmpty.nonEmpty (rdcs ++ pscs) of
- Nothing -> pure vi{ vi_ty = ty' } -- Didn't find any COMPLETE sets
- Just cs -> pure vi{ vi_ty = ty', vi_cache = PM (mkUniqDSet <$> cs) }
-initPossibleMatches _ vi = pure vi
-
-{- Note [COMPLETE sets on data families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-User-defined COMPLETE sets involving data families are attached to the family
-TyCon, whereas the built-in COMPLETE set is attached to a data family instance's
-representation TyCon. This matters for COMPLETE sets involving both DataCons
-and PatSyns (from #17207):
-
- data family T a
- data family instance T () = A | B
- pattern C = B
- {-# COMPLETE A, C #-}
- f :: T () -> ()
- f A = ()
- f C = ()
-
-The match on A is actually wrapped in a CoPat, matching impedance between T ()
-and its representation TyCon, which we translate as
- at x | let y = x |> co, A <- y@ in PmCheck.
-
-Which TyCon should we use for looking up the COMPLETE set? The representation
-TyCon from the match on A would only reveal the built-in COMPLETE set, while the
-data family TyCon would only give the user-defined one. But when initialising
-the PossibleMatches for a given Type, we want to do so only once, because
-merging different COMPLETE sets after the fact is very complicated and possibly
-inefficient.
-
-So in fact, we just *drop* the coercion arising from the CoPat when handling
-handling the constraint @y ~ x |> co@ in addCoreCt, just equating @y ~ x at .
-We then handle the fallout in initPossibleMatches, which has to get a hand at
-both the representation TyCon tc_rep and the parent data family TyCon tc_fam.
-It considers three cases after having established that the Type is a TyConApp:
-
-1. The TyCon is a vanilla data type constructor
-2. The TyCon is tc_rep
-3. The TyCon is tc_fam
-
-1. is simple and subsumed by the handling of the other two.
-We check for case 2. by 'tyConFamInst_maybe' and get the tc_fam out.
-Otherwise (3.), we try to lookup the data family instance at that particular
-type to get out the tc_rep. In case 1., this will just return the original
-TyCon, so tc_rep = tc_fam afterwards.
--}
-
------------------------------------------------
-- * Exported utility functions querying 'Nabla'
@@ -897,11 +866,7 @@ addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
addNotConCt _ _ (PmAltConLike (RealDataCon dc))
| isNewDataCon dc = mzero -- (3) in Note [Coverage checking Newtype matches]
addNotConCt nabla at MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do
- -- 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)
+ let vi@(VI _ pos neg _ rcm) = 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))
@@ -917,9 +882,11 @@ addNotConCt nabla at MkNabla{ nabla_tm_st = ts@(TmSt env reps) } x nalt = do
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
- -> ensureInhabited nabla vi1{ vi_cache = markMatched cl pm }
- _ -> pure vi1
+ PmAltConLike cl -> do
+ rcm' <- lift (markMatched cl rcm)
+ ensureInhabited nabla vi1{ vi_cache = rcm' }
+ _ ->
+ pure vi1
pure nabla{ nabla_tm_st = TmSt (setEntrySDIE env x vi2) reps }
hasRequiredTheta :: PmAltCon -> Bool
@@ -1007,17 +974,16 @@ ensureInhabited :: Nabla -> VarInfo -> MaybeT DsM VarInfo
ensureInhabited nabla vi = case vi_bot vi of
MaybeBot -> pure vi -- The |-Bot rule from the paper
IsBot -> pure vi
- IsNotBot -> lift (initPossibleMatches (nabla_ty_st nabla) vi) >>= inst_complete_sets
+ IsNotBot -> inst_complete_sets vi
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 -> 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
+ inst_complete_sets vi at VI{ vi_cache = RCM ms } = do
ms <- traverse (\cs -> inst_complete_set vi cs (uniqDSetToList cs)) ms
- pure vi{ vi_cache = PM ms }
+ pure vi{ vi_cache = RCM ms }
inst_complete_set :: VarInfo -> ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
-- (inst_complete_set cs cls) iterates over cls, deleting from cs
@@ -1586,8 +1552,12 @@ provideEvidence = go
Just (y, newty_nabla) -> do
-- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥.
let vi = lookupVarInfo (nabla_tm_st newty_nabla) y
- vi <- initPossibleMatches (nabla_ty_st newty_nabla) vi
- mb_cls <- pickMinimalCompleteSet newty_nabla (vi_cache vi)
+ res <- pmTopNormaliseType (nabla_ty_st newty_nabla) (vi_ty vi)
+ let y_ty' = normalisedSourceType res
+ let rcm = case splitTyConApp_maybe y_ty' of
+ Nothing -> vi_cache vi
+ Just (tc, _) -> addTyConMatches tc (vi_cache vi)
+ mb_cls <- pickMinimalCompleteSet newty_nabla rcm
case uniqDSetToList <$> mb_cls of
Just cls@(_:_) -> instantiate_cons y core_ty xs n newty_nabla cls
Just [] | vi_bot vi == IsNotBot -> pure []
@@ -1631,12 +1601,13 @@ provideEvidence = go
other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls
pure (con_nablas ++ other_cons_nablas)
-pickMinimalCompleteSet :: Nabla -> PossibleMatches -> DsM (Maybe ConLikeSet)
-pickMinimalCompleteSet _ NoPM = pure Nothing
+pickMinimalCompleteSet :: Nabla -> ResidualCompleteMatches -> DsM (Maybe ConLikeSet)
+pickMinimalCompleteSet _ (RCM clss)
+ | null clss = pure Nothing
-- TODO: First prune sets with type info in nabla. But this is good enough for
-- now and less costly. See #17386.
-pickMinimalCompleteSet _ (PM clss) = do
- tracePm "pickMinimalCompleteSet" (ppr $ NonEmpty.toList clss)
+pickMinimalCompleteSet _ rcm@(RCM clss) = do
+ tracePm "pickMinimalCompleteSet" (ppr rcm)
pure (Just (minimumBy (comparing sizeUniqDSet) clss))
-- | Finds a representant of the semantic equality class of the given @e at .
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs
=====================================
@@ -24,8 +24,8 @@ module GHC.HsToCore.PmCheck.Types (
literalToPmLit, negatePmLit, overloadPmLit,
pmLitAsStringLit, coreExprAsPmLit,
- -- * Caching partially matched COMPLETE sets
- ConLikeSet, PossibleMatches(..),
+ -- * Caching residual COMPLETE sets
+ ConLikeSet, ResidualCompleteMatches(..),
-- * PmAltConSet
PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
@@ -69,10 +69,10 @@ import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Driver.Types (ConLikeSet)
import Numeric (fromRat)
import Data.Foldable (find)
-import qualified Data.List.NonEmpty as NonEmpty
import Data.Ratio
import qualified Data.Semigroup as Semi
@@ -415,21 +415,15 @@ instance Outputable PmAltCon where
instance Outputable PmEquality where
ppr = text . show
-type ConLikeSet = UniqDSet ConLike
+-- | A data type that caches for the 'VarInfo' of @x@ the results of querying
+-- 'completeMatchConLikes' for all the @K@ for which we know @x /~ K@ and then
+-- striking out all occurrences of those @K at s from these sets.
+-- For motivation, see Section 5.3 in Lower Your Guards.
+newtype ResidualCompleteMatches = RCM (UniqDFM Name ConLikeSet) -- 'Name of the 'CompleteMatch'
--- | A data type caching the results of 'completeMatchConLikes' with support for
--- deletion of constructors that were already matched on.
-data PossibleMatches
- = PM (NonEmpty.NonEmpty ConLikeSet)
- -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE set
- -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
- -- set at all, for which we have 'NoPM'.
- | NoPM
- -- ^ No COMPLETE set for this type (yet). Think of overloaded literals.
-
-instance Outputable PossibleMatches where
- ppr (PM cs) = ppr (NonEmpty.toList cs)
- ppr NoPM = text "<NoPM>"
+instance Outputable ResidualCompleteMatches where
+ -- formats as "[{Nothing,Just},{P,Q}]"
+ ppr (RCM cs) = ppr (map snd (udfmToList cs))
-- | Either @Indirect x@, meaning the value is represented by that of @x@, or
-- an @Entry@ containing containing the actual value it represents.
@@ -516,7 +510,7 @@ data TmState
-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
-- and negative ('vi_neg') facts, like "x is not (:)".
--- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set
+-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
-- ('vi_cache').
--
-- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.PmCheck.Oracle".
@@ -559,7 +553,7 @@ data VarInfo
-- * 'IsBot': @x ~ ⊥@
-- * 'IsNotBot': @x ≁ ⊥@
- , vi_cache :: !PossibleMatches
+ , vi_cache :: !ResidualCompleteMatches
-- ^ A cache of the associated COMPLETE sets. At any time a superset of
-- possible constructors of each COMPLETE set. So, if it's not in here, we
-- can't possibly match on it. Complementary to 'vi_neg'. We still need it
=====================================
compiler/GHC/Iface/Load.hs
=====================================
@@ -70,6 +70,7 @@ import GHC.Data.Maybe
import GHC.Utils.Error
import GHC.Driver.Finder
import GHC.Types.Unique.FM
+import GHC.Types.Unique.DFM
import GHC.Types.SrcLoc
import GHC.Utils.Outputable as Outputable
import GHC.Iface.Binary
@@ -1037,9 +1038,8 @@ initExternalPackageState home_unit
eps_fam_inst_env = emptyFamInstEnv,
eps_rule_base = mkRuleBase builtinRules',
-- Initialise the EPS rule pool with the built-in rules
- eps_mod_fam_inst_env
- = emptyModuleEnv,
- eps_complete_matches = emptyUFM,
+ eps_mod_fam_inst_env = emptyModuleEnv,
+ eps_complete_matches = emptyUDFM,
eps_ann_env = emptyAnnEnv,
eps_stats = EpsStats { n_ifaces_in = 0, n_decls_in = 0, n_decls_out = 0
, n_insts_in = 0, n_insts_out = 0
=====================================
compiler/GHC/Iface/Make.hs
=====================================
@@ -57,6 +57,7 @@ import GHC.Types.Avail
import GHC.Types.Name.Reader
import GHC.Types.Name.Env
import GHC.Types.Name.Set
+import GHC.Types.Unique.DSet
import GHC.Unit
import GHC.Utils.Error
import GHC.Utils.Outputable
@@ -323,7 +324,8 @@ mkIface_ hsc_env
-}
mkIfaceCompleteSig :: CompleteMatch -> IfaceCompleteMatch
-mkIfaceCompleteSig (CompleteMatch cls tc) = IfaceCompleteMatch cls tc
+mkIfaceCompleteSig (CompleteMatch n cls) =
+ IfaceCompleteMatch n (map conLikeName (uniqDSetToList cls))
{-
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -324,7 +324,7 @@ data IfaceAnnotation
type IfaceAnnTarget = AnnTarget OccName
-data IfaceCompleteMatch = IfaceCompleteMatch [IfExtName] IfExtName
+data IfaceCompleteMatch = IfaceCompleteMatch IfExtName [IfExtName]
instance Outputable IfaceCompleteMatch where
ppr (IfaceCompleteMatch cls ty) = text "COMPLETE" <> colon <+> ppr cls
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -67,6 +67,7 @@ import GHC.Types.Name.Set
import GHC.Core.Opt.OccurAnal ( occurAnalyseExpr )
import GHC.Unit.Module
import GHC.Types.Unique.FM
+import GHC.Types.Unique.DSet ( mkUniqDSet )
import GHC.Types.Unique.Supply
import GHC.Utils.Outputable
import GHC.Data.Maybe
@@ -1151,7 +1152,10 @@ tcIfaceCompleteSigs :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
tcIfaceCompleteSigs = mapM tcIfaceCompleteSig
tcIfaceCompleteSig :: IfaceCompleteMatch -> IfL CompleteMatch
-tcIfaceCompleteSig (IfaceCompleteMatch ms t) = return (CompleteMatch ms t)
+tcIfaceCompleteSig (IfaceCompleteMatch u ms) =
+ CompleteMatch u . mkUniqDSet <$> mapM (forkM doc . tcIfaceConLike) ms
+ where
+ doc = text "COMPLETE sig" <+> ppr ms
{-
************************************************************************
@@ -1760,7 +1764,13 @@ tcIfaceDataCon :: Name -> IfL DataCon
tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
; case thing of
AConLike (RealDataCon dc) -> return dc
- _ -> pprPanic "tcIfaceExtDC" (ppr name$$ ppr thing) }
+ _ -> pprPanic "tcIfaceDataCon" (ppr name$$ ppr thing) }
+
+tcIfaceConLike :: Name -> IfL ConLike
+tcIfaceConLike name = do { thing <- tcIfaceGlobal name
+ ; case thing of
+ AConLike cl -> return cl
+ _ -> pprPanic "tcIfaceConLike" (ppr name$$ ppr thing) }
tcIfaceExtId :: Name -> IfL Id
tcIfaceExtId name = do { thing <- tcIfaceGlobal name
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -44,9 +44,8 @@ import GHC.Tc.Utils.TcMType
import GHC.Core.Multiplicity
import GHC.Core.FamInstEnv( normaliseType )
import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
-import GHC.Core.TyCon
import GHC.Tc.Utils.TcType
-import GHC.Core.Type (mkStrLitTy, tidyOpenType, splitTyConApp_maybe, mkCastTy)
+import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
import GHC.Builtin.Types.Prim
import GHC.Builtin.Types( mkBoxedTupleTy )
import GHC.Types.Id
@@ -69,9 +68,9 @@ import GHC.Utils.Panic
import GHC.Builtin.Names( ipClassName )
import GHC.Tc.Validity (checkValidType)
import GHC.Types.Unique.FM
+import GHC.Types.Unique.DSet
import GHC.Types.Unique.Set
import qualified GHC.LanguageExtensions as LangExt
-import GHC.Core.ConLike
import Control.Monad
import Data.Foldable (find)
@@ -197,112 +196,23 @@ tcTopBinds binds sigs
-- The top level bindings are flattened into a giant
-- implicitly-mutually-recursive LHsBinds
-
--- Note [Typechecking Complete Matches]
--- Much like when a user bundled a pattern synonym, the result types of
--- all the constructors in the match pragma must be consistent.
---
--- If we allowed pragmas with inconsistent types then it would be
--- impossible to ever match every constructor in the list and so
--- the pragma would be useless.
-
-
-
-
-
--- This is only used in `tcCompleteSig`. We fold over all the conlikes,
--- this accumulator keeps track of the first `ConLike` with a concrete
--- return type. After fixing the return type, all other constructors with
--- a fixed return type must agree with this.
---
--- The fields of `Fixed` cache the first conlike and its return type so
--- that we can compare all the other conlikes to it. The conlike is
--- stored for error messages.
---
--- `Nothing` in the case that the type is fixed by a type signature
-data CompleteSigType = AcceptAny | Fixed (Maybe ConLike) TyCon
-
tcCompleteSigs :: [LSig GhcRn] -> TcM [CompleteMatch]
tcCompleteSigs sigs =
let
- doOne :: Sig GhcRn -> TcM (Maybe CompleteMatch)
- doOne c@(CompleteMatchSig _ _ lns mtc)
- = fmap Just $ do
- addErrCtxt (text "In" <+> ppr c) $
- case mtc of
- Nothing -> infer_complete_match
- Just tc -> check_complete_match tc
- where
-
- checkCLTypes acc = foldM checkCLType (acc, []) (unLoc lns)
-
- infer_complete_match = do
- (res, cls) <- checkCLTypes AcceptAny
- case res of
- AcceptAny -> failWithTc ambiguousError
- Fixed _ tc -> return $ mkMatch cls tc
-
- check_complete_match tc_name = do
- ty_con <- tcLookupLocatedTyCon tc_name
- (_, cls) <- checkCLTypes (Fixed Nothing ty_con)
- return $ mkMatch cls ty_con
-
- mkMatch :: [ConLike] -> TyCon -> CompleteMatch
- mkMatch cls ty_con = CompleteMatch {
- -- foldM is a left-fold and will have accumulated the ConLikes in
- -- the reverse order. foldrM would accumulate in the correct order,
- -- but would type-check the last ConLike first, which might also be
- -- confusing from the user's perspective. Hence reverse here.
- completeMatchConLikes = reverse (map conLikeName cls),
- completeMatchTyCon = tyConName ty_con
- }
+ doOne :: (Int, LSig GhcRn) -> TcM (Maybe CompleteMatch)
+ -- We don't need to "type-check" COMPLETE signatures anymore; if their
+ -- combinations are invalid it will be found so at match sites. Hence we
+ -- keep '_mtc' only for backwards compatibility.
+ doOne (n, L loc c@(CompleteMatchSig _ext _src_txt (L _ ns) _mtc))
+ = fmap Just $ setSrcSpan loc $ addErrCtxt (text "In" <+> ppr c) $
+ CompleteMatch <$> newCompleteMatchName n loc
+ <*> (mkUniqDSet <$> mapM (addLocM tcLookupConLike) ns)
doOne _ = return Nothing
- ambiguousError :: SDoc
- ambiguousError =
- text "A type signature must be provided for a set of polymorphic"
- <+> text "pattern synonyms."
-
-
- -- See note [Typechecking Complete Matches]
- checkCLType :: (CompleteSigType, [ConLike]) -> Located Name
- -> TcM (CompleteSigType, [ConLike])
- checkCLType (cst, cs) n = do
- cl <- addLocM tcLookupConLike n
- let (_,_,_,_,_,_, res_ty) = conLikeFullSig cl
- res_ty_con = fst <$> splitTyConApp_maybe res_ty
- case (cst, res_ty_con) of
- (AcceptAny, Nothing) -> return (AcceptAny, cl:cs)
- (AcceptAny, Just tc) -> return (Fixed (Just cl) tc, cl:cs)
- (Fixed mfcl tc, Nothing) -> return (Fixed mfcl tc, cl:cs)
- (Fixed mfcl tc, Just tc') ->
- if tc == tc'
- then return (Fixed mfcl tc, cl:cs)
- else case mfcl of
- Nothing ->
- addErrCtxt (text "In" <+> ppr cl) $
- failWithTc typeSigErrMsg
- Just cl -> failWithTc (errMsg cl)
- where
- typeSigErrMsg :: SDoc
- typeSigErrMsg =
- text "Couldn't match expected type"
- <+> quotes (ppr tc)
- <+> text "with"
- <+> quotes (ppr tc')
-
- errMsg :: ConLike -> SDoc
- errMsg fcl =
- text "Cannot form a group of complete patterns from patterns"
- <+> quotes (ppr fcl) <+> text "and" <+> quotes (ppr cl)
- <+> text "as they match different type constructors"
- <+> parens (quotes (ppr tc)
- <+> text "resp."
- <+> quotes (ppr tc'))
-- For some reason I haven't investigated further, the signatures come in
-- backwards wrt. declaration order. So we reverse them here, because it makes
-- a difference for incomplete match suggestions.
- in mapMaybeM (addLocM doOne) (reverse sigs) -- process in declaration order
+ in mapMaybeM doOne $ zip [1..] $ reverse sigs
tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
-- A hs-boot file has only one BindGroup, and it only has type
=====================================
compiler/GHC/Tc/Utils/Env.hs
=====================================
@@ -64,8 +64,8 @@ module GHC.Tc.Utils.Env(
topIdLvl, isBrackStage,
-- New Ids
- newDFunName, newFamInstTyConName,
- newFamInstAxiomName,
+ newDFunName, newCompleteMatchName,
+ newFamInstTyConName, newFamInstAxiomName,
mkStableIdFromString, mkStableIdFromName,
mkWrapperName
) where
@@ -1012,6 +1012,12 @@ newDFunName clas tys loc
; dfun_occ <- chooseUniqueOccTc (mkDFunOcc info_string is_boot)
; newGlobalBinder mod dfun_occ loc }
+newCompleteMatchName :: Int -> SrcSpan -> TcM Name
+newCompleteMatchName n loc
+ = do { mod <- getModule
+ ; let occ = mkCompleteMatchOcc (show n)
+ ; newGlobalBinder mod occ loc }
+
newFamInstTyConName :: Located Name -> [Type] -> TcM Name
newFamInstTyConName (L loc name) tys = mk_fam_inst_name id loc name [tys]
=====================================
compiler/GHC/Types/Name/Occurrence.hs
=====================================
@@ -70,6 +70,7 @@ module GHC.Types.Name.Occurrence (
mkInstTyCoOcc, mkEqPredCoOcc,
mkRecFldSelOcc,
mkTyConRepOcc,
+ mkCompleteMatchOcc,
-- ** Deconstruction
occNameFS, occNameString, occNameSpace,
@@ -652,6 +653,9 @@ mkGen1R = mk_simple_deriv tcName "Rep1_"
mkRecFldSelOcc :: String -> OccName
mkRecFldSelOcc s = mk_deriv varName "$sel" [fsLit s]
+mkCompleteMatchOcc :: String -> OccName
+mkCompleteMatchOcc s = mk_deriv tcName "$CM" [fsLit s]
+
mk_simple_deriv :: NameSpace -> FastString -> OccName -> OccName
mk_simple_deriv sp px occ = mk_deriv sp px [occNameFS occ]
=====================================
compiler/GHC/Types/Unique/DFM.hs
=====================================
@@ -32,6 +32,7 @@ module GHC.Types.Unique.DFM (
addToUDFM_C_Directly,
addToUDFM_Directly,
addListToUDFM,
+ addListToUDFM_C,
delFromUDFM,
delListFromUDFM,
adjustUDFM,
@@ -41,6 +42,7 @@ module GHC.Types.Unique.DFM (
plusUDFM,
plusUDFM_C,
lookupUDFM, lookupUDFM_Directly,
+ lookupWithDefaultUDFM, lookupWithDefaultUDFM_Directly,
elemUDFM,
foldUDFM,
eltsUDFM,
@@ -68,6 +70,7 @@ import GHC.Prelude
import GHC.Types.Unique ( Uniquable(..), Unique, getKey )
import GHC.Utils.Outputable
+import GHC.Data.Maybe ( orElse )
import qualified Data.IntMap as M
import Data.Data
@@ -206,6 +209,10 @@ addListToUDFM = foldl' (\m (k, v) -> addToUDFM m k v)
addListToUDFM_Directly :: UniqDFM key elt -> [(Unique,elt)] -> UniqDFM key elt
addListToUDFM_Directly = foldl' (\m (k, v) -> addToUDFM_Directly m k v)
+addListToUDFM_C
+ :: Uniquable key => (elt -> elt -> elt) -> UniqDFM key elt -> [(key,elt)] -> UniqDFM key elt
+addListToUDFM_C f = foldl' (\m (k, v) -> addToUDFM_C f m k v)
+
addListToUDFM_Directly_C
:: (elt -> elt -> elt) -> UniqDFM key elt -> [(Unique,elt)] -> UniqDFM key elt
addListToUDFM_Directly_C f = foldl' (\m (k, v) -> addToUDFM_C_Directly f m k v)
@@ -274,6 +281,12 @@ lookupUDFM (UDFM m _i) k = taggedFst `fmap` M.lookup (getKey $ getUnique k) m
lookupUDFM_Directly :: UniqDFM key elt -> Unique -> Maybe elt
lookupUDFM_Directly (UDFM m _i) k = taggedFst `fmap` M.lookup (getKey k) m
+lookupWithDefaultUDFM :: Uniquable key => UniqDFM key elt -> elt -> key -> elt
+lookupWithDefaultUDFM m v k = lookupUDFM m k `orElse` v
+
+lookupWithDefaultUDFM_Directly :: UniqDFM key elt -> elt -> Unique -> elt
+lookupWithDefaultUDFM_Directly m v k = lookupUDFM_Directly m k `orElse` v
+
elemUDFM :: Uniquable key => key -> UniqDFM key elt -> Bool
elemUDFM k (UDFM m _i) = M.member (getKey $ getUnique k) m
=====================================
docs/users_guide/exts/pragmas.rst
=====================================
@@ -887,29 +887,6 @@ modules. ``COMPLETE`` pragmas should be thought of as asserting a
universal truth about a set of patterns and as a result, should not be
used to silence context specific incomplete match warnings.
-When specifying a ``COMPLETE`` pragma, the result types of all patterns must
-be consistent with each other. This is a sanity check as it would be impossible
-to match on all the patterns if the types were inconsistent.
-
-The result type must also be unambiguous. Usually this can be inferred but
-when all the pattern synonyms in a group are polymorphic in the constructor
-the user must provide a type signature. ::
-
- class LL f where
- go :: f a -> ()
-
- instance LL [] where
- go _ = ()
-
- pattern T :: LL f => f a
- pattern T <- (go -> ())
-
- {-# COMPLETE T :: [] #-}
-
- -- No warning
- foo :: [a] -> Int
- foo T = 5
-
.. _overlap-pragma:
``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ff8ff6b0e2db6740d0c2ac4cdd5b439569f8b47b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ff8ff6b0e2db6740d0c2ac4cdd5b439569f8b47b
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/20200901/d4a94aa0/attachment-0001.html>
More information about the ghc-commits
mailing list