diff options
Diffstat (limited to 'compiler/GHC/Core')
| -rw-r--r-- | compiler/GHC/Core/Coercion/Axiom.hs | 1 | ||||
| -rw-r--r-- | compiler/GHC/Core/FamInstEnv.hs | 198 | ||||
| -rw-r--r-- | compiler/GHC/Core/InstEnv.hs | 203 | ||||
| -rw-r--r-- | compiler/GHC/Core/Lint.hs | 4 | ||||
| -rw-r--r-- | compiler/GHC/Core/RoughMap.hs | 451 | ||||
| -rw-r--r-- | compiler/GHC/Core/Unify.hs | 33 |
6 files changed, 687 insertions, 203 deletions
diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs index 5db9f17161..2476cfd7cc 100644 --- a/compiler/GHC/Core/Coercion/Axiom.hs +++ b/compiler/GHC/Core/Coercion/Axiom.hs @@ -455,6 +455,7 @@ See also: type; but it too is eta-reduced. * Note [Implementing eta reduction for data families] in "GHC.Tc.TyCl.Instance". This describes the implementation details of this eta reduction happen. +* Note [RoughMap and rm_empty] for how this complicates the RoughMap implementation slightly. -} instance Eq (CoAxiom br) where diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs index c0981ac9e1..78ed3a104c 100644 --- a/compiler/GHC/Core/FamInstEnv.hs +++ b/compiler/GHC/Core/FamInstEnv.hs @@ -15,7 +15,7 @@ module GHC.Core.FamInstEnv ( mkImportedFamInst, FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, - extendFamInstEnv, extendFamInstEnvList, + unionFamInstEnv, extendFamInstEnv, extendFamInstEnvList, famInstEnvElts, famInstEnvSize, familyInstances, -- * CoAxioms @@ -46,10 +46,10 @@ import GHC.Core.TyCon import GHC.Core.Coercion import GHC.Core.Coercion.Axiom import GHC.Core.Reduction +import GHC.Core.RoughMap import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Types.Name -import GHC.Types.Unique.DFM import GHC.Data.Maybe import GHC.Types.Var import GHC.Types.SrcLoc @@ -61,6 +61,7 @@ import GHC.Utils.Misc import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain +import GHC.Data.Bag {- ************************************************************************ @@ -302,7 +303,17 @@ mkImportedFamInst fam mb_tcs axiom Note [FamInstEnv] ~~~~~~~~~~~~~~~~~ -A FamInstEnv maps a family name to the list of known instances for that family. +A FamInstEnv is a RoughMap of instance heads. Specifically, the keys are formed +by the family name and the instance arguments. That is, an instance: + + type instance Fam (Maybe Int) a + +would insert into the instance environment an instance with a key of the form + + [RM_KnownTc Fam, RM_KnownTc Maybe, RM_WildCard] + +See Note [RoughMap] in GHC.Core.RoughMap. + The same FamInstEnv includes both 'data family' and 'type family' instances. Type families are reduced during type inference, but not data families; @@ -350,30 +361,24 @@ UniqFM and UniqDFM. See Note [Deterministic UniqFM]. -} --- Internally we sometimes index by Name instead of TyCon despite --- of what the type says. This is safe since --- getUnique (tyCon) == getUniqe (tcName tyCon) -type FamInstEnv = UniqDFM TyCon FamilyInstEnv -- Maps a family to its instances - -- See Note [FamInstEnv] - -- See Note [FamInstEnv determinism] - type FamInstEnvs = (FamInstEnv, FamInstEnv) -- External package inst-env, Home-package inst-env -newtype FamilyInstEnv - = FamIE [FamInst] -- The instances for a particular family, in any order +data FamInstEnv + = FamIE !Int -- The number of instances, used to choose the smaller environment + -- when checking type family consistnecy of home modules. + !(RoughMap FamInst) + -- See Note [FamInstEnv] + -- See Note [FamInstEnv determinism] -instance Outputable FamilyInstEnv where - ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs) --- | Index a FamInstEnv by the tyCons name. -toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv -toNameInstEnv = unsafeCastUDFMKey +instance Outputable FamInstEnv where + ppr (FamIE _ fs) = text "FamIE" <+> vcat (map ppr $ elemsRM fs) --- | Create a FamInstEnv from Name indices. -fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv -fromNameInstEnv = unsafeCastUDFMKey +famInstEnvSize :: FamInstEnv -> Int +famInstEnvSize (FamIE sz _) = sz +-- | Create a 'FamInstEnv' from 'Name' indices. -- INVARIANTS: -- * The fs_tvs are distinct in each FamInst -- of a range value of the map (so we can safely unify them) @@ -382,14 +387,12 @@ emptyFamInstEnvs :: (FamInstEnv, FamInstEnv) emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv) emptyFamInstEnv :: FamInstEnv -emptyFamInstEnv = emptyUDFM +emptyFamInstEnv = FamIE 0 emptyRM famInstEnvElts :: FamInstEnv -> [FamInst] -famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts] +famInstEnvElts (FamIE _ rm) = elemsRM rm -- See Note [FamInstEnv determinism] -famInstEnvSize :: FamInstEnv -> Int -famInstEnvSize = nonDetStrictFoldUDFM (\(FamIE elt) sum -> sum + length elt) 0 -- It's OK to use nonDetStrictFoldUDFM here since we're just computing the -- size. @@ -397,19 +400,23 @@ familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst] familyInstances (pkg_fie, home_fie) fam = get home_fie ++ get pkg_fie where - get env = case lookupUDFM env fam of - Just (FamIE insts) -> insts - Nothing -> [] + get :: FamInstEnv -> [FamInst] + get (FamIE _ env) = lookupRM [RML_KnownTc (tyConName fam)] env + + +-- | Makes no particular effort to detect conflicts. +unionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv +unionFamInstEnv (FamIE sa a) (FamIE sb b) = FamIE (sa + sb) (a `unionRM` b) extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv extendFamInstEnvList inst_env fis = foldl' extendFamInstEnv inst_env fis extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv -extendFamInstEnv inst_env +extendFamInstEnv (FamIE s inst_env) ins_item@(FamInst {fi_fam = cls_nm}) - = fromNameInstEnv $ addToUDFM_C add (toNameInstEnv inst_env) cls_nm (FamIE [ins_item]) + = FamIE (s+1) $ insertRM rough_tmpl ins_item inst_env where - add (FamIE items) _ = FamIE (ins_item:items) + rough_tmpl = RM_KnownTc cls_nm : fi_tcs ins_item {- ************************************************************************ @@ -774,9 +781,7 @@ lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst] lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc = get pkg_ie ++ get home_ie where - get ie = case lookupUDFM ie fam_tc of - Nothing -> [] - Just (FamIE fis) -> fis + get (FamIE _ rm) = lookupRM [RML_KnownTc (tyConName fam_tc)] rm lookupFamInstEnv :: FamInstEnvs @@ -785,14 +790,12 @@ lookupFamInstEnv -- Precondition: the tycon is saturated (or over-saturated) lookupFamInstEnv - = lookup_fam_inst_env match - where - match _ _ tpl_tys tys = tcMatchTys tpl_tys tys + = lookup_fam_inst_env WantMatches lookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -- Putative new instance - -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field) + -> [FamInst] -- Conflicting matches (don't look at the fim_tys field) -- E.g. when we are about to add -- f : type instance F [a] = a->a -- we do (lookupFamInstConflicts f [b]) @@ -800,25 +803,10 @@ lookupFamInstEnvConflicts -- -- Precondition: the tycon is saturated (or over-saturated) -lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom }) - = lookup_fam_inst_env my_unify envs fam tys +lookupFamInstEnvConflicts envs fam_inst + = lookup_fam_inst_env (WantConflicts fam_inst) envs fam tys where (fam, tys) = famInstSplitLHS fam_inst - -- In example above, fam tys' = F [b] - - my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _ - = assertPpr (tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs) - ((ppr fam <+> ppr tys) $$ - (ppr tpl_tvs <+> ppr tpl_tys)) $ - -- Unification will break badly if the variables overlap - -- They shouldn't because we allocate separate uniques for them - if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch - then Nothing - else Just noSubst - -- See Note [Family instance overlap conflicts] - - noSubst = panic "lookupFamInstEnvConflicts noSubst" - new_branch = coAxiomSingleBranch new_axiom -------------------------------------------------------------------------------- -- Type family injectivity checking bits -- @@ -927,11 +915,17 @@ lookupFamInstEnvInjectivityConflicts -> FamInstEnvs -- all type instances seens so far -> FamInst -- new type instance that we're checking -> [CoAxBranch] -- conflicting instance declarations -lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie) +lookupFamInstEnvInjectivityConflicts injList fam_inst_envs fam_inst@(FamInst { fi_axiom = new_axiom }) + | not $ isOpenFamilyTyCon fam + = [] + + | otherwise -- See Note [Verifying injectivity annotation]. This function implements -- check (1.B1) for open type families described there. - = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie + = map (coAxiomSingleBranch . fi_axiom) $ + filter isInjConflict $ + familyInstances fam_inst_envs fam where fam = famInstTyCon fam_inst new_branch = coAxiomSingleBranch new_axiom @@ -944,12 +938,6 @@ lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie) = False -- no conflict | otherwise = True - lookup_inj_fam_conflicts ie - | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam - = map (coAxiomSingleBranch . fi_axiom) $ - filter isInjConflict insts - | otherwise = [] - -------------------------------------------------------------------------------- -- Type family overlap checking bits -- @@ -973,46 +961,61 @@ Note [Family instance overlap conflicts] ------------------------------------------------------------ -- Might be a one-way match or a unifier -type MatchFun = FamInst -- The FamInst template - -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst - -> [Type] -- Target to match against - -> Maybe TCvSubst +data FamInstLookupMode a where + -- The FamInst we are trying to find conflicts against + WantConflicts :: FamInst -> FamInstLookupMode FamInst + WantMatches :: FamInstLookupMode FamInstMatch lookup_fam_inst_env' -- The worker, local to this module - :: MatchFun + :: forall a . FamInstLookupMode a -> FamInstEnv -> TyCon -> [Type] -- What we are looking for - -> [FamInstMatch] -lookup_fam_inst_env' match_fun ie fam match_tys + -> [a] +lookup_fam_inst_env' lookup_mode (FamIE _ ie) fam match_tys | isOpenFamilyTyCon fam - , Just (FamIE insts) <- lookupUDFM ie fam - = find insts -- The common case + , let xs = rm_fun (lookupRM' rough_tmpl ie) -- The common case + -- Avoid doing any of the allocation below if there are no instances to look at. + , not $ null xs + = mapMaybe' check_fun xs | otherwise = [] where + rough_tmpl :: [RoughMatchLookupTc] + rough_tmpl = RML_KnownTc (tyConName fam) : map typeToRoughMatchLookupTc match_tys - find [] = [] - find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs - , fi_tys = tpl_tys }) : rest) - -- Fast check for no match, uses the "rough match" fields - | instanceCantMatch rough_tcs mb_tcs - = find rest - - -- Proper check - | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1 - = (FamInstMatch { fim_instance = item - , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 - , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ - substCoVars subst tpl_cvs - }) - : find rest - - -- No match => try next - | otherwise - = find rest - where - (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys + rm_fun :: (Bag FamInst, [FamInst]) -> [FamInst] + (rm_fun, check_fun) = case lookup_mode of + WantConflicts fam_inst -> (snd, unify_fun fam_inst) + WantMatches -> (bagToList . fst, match_fun) - -- Precondition: the tycon is saturated (or over-saturated) + -- Function used for finding unifiers + unify_fun orig_fam_inst item@(FamInst { fi_axiom = old_axiom, fi_tys = tpl_tys, fi_tvs = tpl_tvs }) + + = assertPpr (tyCoVarsOfTypes tys `disjointVarSet` mkVarSet tpl_tvs) + ((ppr fam <+> ppr tys) $$ + (ppr tpl_tvs <+> ppr tpl_tys)) $ + -- Unification will break badly if the variables overlap + -- They shouldn't because we allocate separate uniques for them + if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch + then Nothing + else Just item + -- See Note [Family instance overlap conflicts] + where + new_branch = coAxiomSingleBranch (famInstAxiom orig_fam_inst) + (fam, tys) = famInstSplitLHS orig_fam_inst + + -- Function used for checking matches + match_fun item@(FamInst { fi_tvs = tpl_tvs, fi_cvs = tpl_cvs + , fi_tys = tpl_tys }) = do + subst <- tcMatchTys tpl_tys match_tys1 + return (FamInstMatch { fim_instance = item + , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 + , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $ + substCoVars subst tpl_cvs + }) + where + (match_tys1, match_tys2) = split_tys tpl_tys + + -- Precondition: the tycon is saturated (or over-saturated) -- Deal with over-saturation -- See Note [Over-saturated matches] @@ -1022,18 +1025,17 @@ lookup_fam_inst_env' match_fun ie fam match_tys | otherwise = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys - rough_tcs = roughMatchTcs match_tys1 - in (rough_tcs, match_tys1, match_tys2) + in (match_tys1, match_tys2) (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys pre_rough_split_tys - = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2) + = (pre_match_tys1, pre_match_tys2) lookup_fam_inst_env -- The worker, local to this module - :: MatchFun + :: FamInstLookupMode a -> FamInstEnvs -> TyCon -> [Type] -- What we are looking for - -> [FamInstMatch] -- Successful matches + -> [a] -- Successful matches -- Precondition: the tycon is saturated (or over-saturated) diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs index ab23fcae2c..e223a7cd87 100644 --- a/compiler/GHC/Core/InstEnv.hs +++ b/compiler/GHC/Core/InstEnv.hs @@ -11,17 +11,19 @@ The bits common to GHC.Tc.TyCl.Instance and GHC.Tc.Deriv. module GHC.Core.InstEnv ( DFunId, InstMatch, ClsInstLookupResult, + PotentialUnifiers(..), getPotentialUnifiers, nullUnifiers, OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe, ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances, instanceHead, instanceSig, mkLocalInstance, mkImportedInstance, - instanceDFunId, updateClsInstDFun, instanceRoughTcs, + instanceDFunId, updateClsInstDFuns, updateClsInstDFun, fuzzyClsInstCmp, orphNamesOfClsInst, InstEnvs(..), VisibleOrphanModules, InstEnv, - emptyInstEnv, extendInstEnv, - deleteFromInstEnv, deleteDFunFromInstEnv, + mkInstEnv, emptyInstEnv, unionInstEnv, extendInstEnv, + filterInstEnv, deleteFromInstEnv, deleteDFunFromInstEnv, + anyInstEnv, identicalClsInstHead, - extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts, instEnvClasses, + extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts, instEnvClasses, mapInstEnv, memberInstEnv, instIsVisible, classInstances, instanceBindFun, @@ -34,25 +36,25 @@ import GHC.Prelude import GHC.Tc.Utils.TcType -- InstEnv is really part of the type checker, -- and depends on TcType in many ways import GHC.Core ( IsOrphan(..), isOrphan, chooseOrphanAnchor ) +import GHC.Core.RoughMap import GHC.Unit.Module.Env import GHC.Unit.Types import GHC.Core.Class import GHC.Types.Var +import GHC.Types.Unique.DSet import GHC.Types.Var.Set import GHC.Types.Name import GHC.Types.Name.Set -import GHC.Types.Unique (getUnique) import GHC.Core.Unify import GHC.Types.Basic -import GHC.Types.Unique.DFM import GHC.Types.Id import Data.Data ( Data ) import Data.Maybe ( isJust ) -import GHC.Utils.Misc import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain +import Data.Semigroup {- ************************************************************************ @@ -68,9 +70,12 @@ import GHC.Utils.Panic.Plain data ClsInst = ClsInst { -- Used for "rough matching"; see -- Note [ClsInst laziness and the rough-match fields] - -- INVARIANT: is_tcs = roughMatchTcs is_tys + -- INVARIANT: is_tcs = KnownTc is_cls_nm : roughMatchTcs is_tys is_cls_nm :: Name -- ^ Class name + , is_tcs :: [RoughMatchTc] -- ^ Top of type args + -- The class itself is always + -- the first element of this list -- | @is_dfun_name = idName . is_dfun@. -- @@ -103,13 +108,12 @@ data ClsInst -- instances before displaying them to the user. fuzzyClsInstCmp :: ClsInst -> ClsInst -> Ordering fuzzyClsInstCmp x y = - stableNameCmp (is_cls_nm x) (is_cls_nm y) `mappend` - mconcat (map cmp (zip (is_tcs x) (is_tcs y))) + foldMap cmp (zip (is_tcs x) (is_tcs y)) where - cmp (OtherTc, OtherTc) = EQ - cmp (OtherTc, KnownTc _) = LT - cmp (KnownTc _, OtherTc) = GT - cmp (KnownTc x, KnownTc y) = stableNameCmp x y + cmp (RM_WildCard, RM_WildCard) = EQ + cmp (RM_WildCard, RM_KnownTc _) = LT + cmp (RM_KnownTc _, RM_WildCard) = GT + cmp (RM_KnownTc x, RM_KnownTc y) = stableNameCmp x y isOverlappable, isOverlapping, isIncoherent :: ClsInst -> Bool isOverlappable i = hasOverlappableFlag (overlapMode (is_flag i)) @@ -196,8 +200,9 @@ updateClsInstDFun :: (DFunId -> DFunId) -> ClsInst -> ClsInst updateClsInstDFun tidy_dfun ispec = ispec { is_dfun = tidy_dfun (is_dfun ispec) } -instanceRoughTcs :: ClsInst -> [RoughMatchTc] -instanceRoughTcs = is_tcs +updateClsInstDFuns :: (DFunId -> DFunId) -> InstEnv -> InstEnv +updateClsInstDFuns tidy_dfun (InstEnv rm) + = InstEnv $ fmap (updateClsInstDFun tidy_dfun) rm instance NamedThing ClsInst where getName ispec = getName (is_dfun ispec) @@ -259,7 +264,7 @@ mkLocalInstance dfun oflag tvs cls tys , is_tvs = tvs , is_dfun_name = dfun_name , is_cls = cls, is_cls_nm = cls_name - , is_tys = tys, is_tcs = roughMatchTcs tys + , is_tys = tys, is_tcs = RM_KnownTc cls_name : roughMatchTcs tys , is_orphan = orph } where @@ -290,7 +295,7 @@ mkLocalInstance dfun oflag tvs cls tys choose_one nss = chooseOrphanAnchor (unionNameSets nss) mkImportedInstance :: Name -- ^ the name of the class - -> [RoughMatchTc] -- ^ the types which the class was applied to + -> [RoughMatchTc] -- ^ the rough match signature of the instance -> Name -- ^ the 'Name' of the dictionary binding -> DFunId -- ^ the 'Id' of the dictionary. -> OverlapFlag -- ^ may this instance overlap? @@ -304,7 +309,8 @@ mkImportedInstance cls_nm mb_tcs dfun_name dfun oflag orphan = ClsInst { is_flag = oflag, is_dfun = dfun , is_tvs = tvs, is_tys = tys , is_dfun_name = dfun_name - , is_cls_nm = cls_nm, is_cls = cls, is_tcs = mb_tcs + , is_cls_nm = cls_nm, is_cls = cls + , is_tcs = RM_KnownTc cls_nm : mb_tcs , is_orphan = orphan } where (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun) @@ -386,9 +392,12 @@ UniqDFM. See also Note [Deterministic UniqFM] -- We still use Class as key type as it's both the common case -- and conveys the meaning better. But the implementation of --InstEnv is a bit more lax internally. -type InstEnv = UniqDFM Class ClsInstEnv -- Maps Class to instances for that class +newtype InstEnv = InstEnv (RoughMap ClsInst) -- Maps Class to instances for that class -- See Note [InstEnv determinism] +instance Outputable InstEnv where + ppr (InstEnv rm) = pprInstances $ elemsRM rm + -- | 'InstEnvs' represents the combination of the global type class instance -- environment, the local type class instance environment, and the set of -- transitively reachable orphan modules (according to what modules have been @@ -406,30 +415,32 @@ data InstEnvs = InstEnvs { -- transitively reachable orphan modules (modules that define orphan instances). type VisibleOrphanModules = ModuleSet -newtype ClsInstEnv - = ClsIE [ClsInst] -- The instances for a particular class, in any order - -instance Outputable ClsInstEnv where - ppr (ClsIE is) = pprInstances is -- INVARIANTS: -- * The is_tvs are distinct in each ClsInst -- of a ClsInstEnv (so we can safely unify them) --- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry: +-- Thus, the @ClsInstEnv@ for @Eq@ might contain the following entry: -- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a] -- The "a" in the pattern must be one of the forall'd variables in -- the dfun type. emptyInstEnv :: InstEnv -emptyInstEnv = emptyUDFM +emptyInstEnv = InstEnv emptyRM + +mkInstEnv :: [ClsInst] -> InstEnv +mkInstEnv = extendInstEnvList emptyInstEnv instEnvElts :: InstEnv -> [ClsInst] -instEnvElts ie = [elt | ClsIE elts <- eltsUDFM ie, elt <- elts] +instEnvElts (InstEnv rm) = elemsRM rm -- See Note [InstEnv determinism] -instEnvClasses :: InstEnv -> [Class] -instEnvClasses ie = [is_cls e | ClsIE (e : _) <- eltsUDFM ie] +instEnvEltsForClass :: InstEnv -> Class -> [ClsInst] +instEnvEltsForClass (InstEnv rm) cls = lookupRM [RML_KnownTc (className cls)] rm + +-- N.B. this is not particularly efficient but used only by GHCi. +instEnvClasses :: InstEnv -> UniqDSet Class +instEnvClasses ie = mkUniqDSet $ map is_cls (instEnvElts ie) -- | Test if an instance is visible, by checking that its origin module -- is in 'VisibleOrphanModules'. @@ -449,42 +460,50 @@ classInstances :: InstEnvs -> Class -> [ClsInst] classInstances (InstEnvs { ie_global = pkg_ie, ie_local = home_ie, ie_visible = vis_mods }) cls = get home_ie ++ get pkg_ie where - get env = case lookupUDFM env cls of - Just (ClsIE insts) -> filter (instIsVisible vis_mods) insts - Nothing -> [] + get :: InstEnv -> [ClsInst] + get ie = filter (instIsVisible vis_mods) (instEnvEltsForClass ie cls) -- | Checks for an exact match of ClsInst in the instance environment. -- We use this when we do signature checking in "GHC.Tc.Module" memberInstEnv :: InstEnv -> ClsInst -> Bool -memberInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm } ) = - maybe False (\(ClsIE items) -> any (identicalDFunType ins_item) items) - (lookupUDFM_Directly inst_env (getUnique cls_nm)) +memberInstEnv (InstEnv rm) ins_item@(ClsInst { is_tcs = tcs } ) = + any (identicalDFunType ins_item) (fst $ lookupRM' (map roughMatchTcToLookup tcs) rm) where identicalDFunType cls1 cls2 = eqType (varType (is_dfun cls1)) (varType (is_dfun cls2)) +-- | Makes no particular effort to detect conflicts. +unionInstEnv :: InstEnv -> InstEnv -> InstEnv +unionInstEnv (InstEnv a) (InstEnv b) = InstEnv (a `unionRM` b) + extendInstEnvList :: InstEnv -> [ClsInst] -> InstEnv extendInstEnvList inst_env ispecs = foldl' extendInstEnv inst_env ispecs extendInstEnv :: InstEnv -> ClsInst -> InstEnv -extendInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm }) - = addToUDFM_C_Directly add inst_env (getUnique cls_nm) (ClsIE [ins_item]) - where - add (ClsIE cur_insts) _ = ClsIE (ins_item : cur_insts) +extendInstEnv (InstEnv rm) ins_item@(ClsInst { is_tcs = tcs }) + = InstEnv $ insertRM tcs ins_item rm + +filterInstEnv :: (ClsInst -> Bool) -> InstEnv -> InstEnv +filterInstEnv pred (InstEnv rm) + = InstEnv $ filterRM pred rm + +anyInstEnv :: (ClsInst -> Bool) -> InstEnv -> Bool +anyInstEnv pred (InstEnv rm) + = foldRM (\x rest -> pred x || rest) False rm + +mapInstEnv :: (ClsInst -> ClsInst) -> InstEnv -> InstEnv +mapInstEnv f (InstEnv rm) = InstEnv (f <$> rm) deleteFromInstEnv :: InstEnv -> ClsInst -> InstEnv -deleteFromInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm }) - = adjustUDFM_Directly adjust inst_env (getUnique cls_nm) - where - adjust (ClsIE items) = ClsIE (filterOut (identicalClsInstHead ins_item) items) +deleteFromInstEnv (InstEnv rm) ins_item@(ClsInst { is_tcs = tcs }) + = InstEnv $ filterMatchingRM (not . identicalClsInstHead ins_item) tcs rm deleteDFunFromInstEnv :: InstEnv -> DFunId -> InstEnv -- Delete a specific instance fron an InstEnv -deleteDFunFromInstEnv inst_env dfun - = adjustUDFM adjust inst_env cls +deleteDFunFromInstEnv (InstEnv rm) dfun + = InstEnv $ filterMatchingRM (not . same_dfun) [RM_KnownTc (className cls)] rm where (_, _, cls, _) = tcSplitDFunTy (idType dfun) - adjust (ClsIE items) = ClsIE (filterOut same_dfun items) same_dfun (ClsInst { is_dfun = dfun' }) = dfun == dfun' identicalClsInstHead :: ClsInst -> ClsInst -> Bool @@ -492,10 +511,10 @@ identicalClsInstHead :: ClsInst -> ClsInst -> Bool -- e.g. both are Eq [(a,b)] -- Used for overriding in GHCi -- Obviously should be insensitive to alpha-renaming -identicalClsInstHead (ClsInst { is_cls_nm = cls_nm1, is_tcs = rough1, is_tys = tys1 }) - (ClsInst { is_cls_nm = cls_nm2, is_tcs = rough2, is_tys = tys2 }) - = cls_nm1 == cls_nm2 - && not (instanceCantMatch rough1 rough2) -- Fast check for no match, uses the "rough match" fields +identicalClsInstHead (ClsInst { is_tcs = rough1, is_tys = tys1 }) + (ClsInst { is_tcs = rough2, is_tys = tys2 }) + = not (instanceCantMatch rough1 rough2) -- Fast check for no match, uses the "rough match" fields; + -- also accounts for class name. && isJust (tcMatchTys tys1 tys2) && isJust (tcMatchTys tys2 tys1) @@ -730,7 +749,7 @@ type InstMatch = (ClsInst, [DFunInstType]) type ClsInstLookupResult = ( [InstMatch] -- Successful matches - , [ClsInst] -- These don't match but do unify + , PotentialUnifiers -- These don't match but do unify , [InstMatch] ) -- Unsafe overlapped instances under Safe Haskell -- (see Note [Safe Haskell Overlapping Instances] in -- GHC.Tc.Solver). @@ -811,11 +830,38 @@ lookupUniqueInstEnv instEnv cls tys _other -> Left $ text "instance not found" <+> (ppr $ mkTyConApp (classTyCon cls) tys) +data PotentialUnifiers = NoUnifiers + | OneOrMoreUnifiers [ClsInst] + -- This list is lazy as we only look at all the unifiers when + -- printing an error message. It can be expensive to compute all + -- the unifiers because if you are matching something like C a[sk] then + -- all instances will unify. + +instance Outputable PotentialUnifiers where + ppr NoUnifiers = text "NoUnifiers" + ppr xs = ppr (getPotentialUnifiers xs) + +instance Semigroup PotentialUnifiers where + NoUnifiers <> u = u + u <> NoUnifiers = u + u1 <> u2 = OneOrMoreUnifiers (getPotentialUnifiers u1 ++ getPotentialUnifiers u2) + +instance Monoid PotentialUnifiers where + mempty = NoUnifiers + +getPotentialUnifiers :: PotentialUnifiers -> [ClsInst] +getPotentialUnifiers NoUnifiers = [] +getPotentialUnifiers (OneOrMoreUnifiers cls) = cls + +nullUnifiers :: PotentialUnifiers -> Bool +nullUnifiers NoUnifiers = True +nullUnifiers _ = False + lookupInstEnv' :: InstEnv -- InstEnv to look in -> VisibleOrphanModules -- But filter against this -> Class -> [Type] -- What we are looking for -> ([InstMatch], -- Successful matches - [ClsInst]) -- These don't match but do unify + PotentialUnifiers) -- These don't match but do unify -- (no incoherent ones in here) -- The second component of the result pair happens when we look up -- Foo [a] @@ -827,35 +873,35 @@ lookupInstEnv' :: InstEnv -- InstEnv to look in -- but Foo [Int] is a unifier. This gives the caller a better chance of -- giving a suitable error message -lookupInstEnv' ie vis_mods cls tys - = lookup ie +lookupInstEnv' (InstEnv rm) vis_mods cls tys + = (foldr check_match [] rough_matches, check_unifier rough_unifiers) where - rough_tcs = roughMatchTcs tys - - -------------- - lookup env = case lookupUDFM env cls of - Nothing -> ([],[]) -- No instances for this class - Just (ClsIE insts) -> find [] [] insts + (rough_matches, rough_unifiers) = lookupRM' rough_tcs rm + rough_tcs = RML_KnownTc (className cls) : roughMatchTcsLookup tys -------------- - find ms us [] = (ms, us) - find ms us (item@(ClsInst { is_tcs = mb_tcs, is_tvs = tpl_tvs - , is_tys = tpl_tys }) : rest) + check_match :: ClsInst -> [InstMatch] -> [InstMatch] + check_match item@(ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }) acc | not (instIsVisible vis_mods item) - = find ms us rest -- See Note [Instance lookup and orphan instances] - - -- Fast check for no match, uses the "rough match" fields - | instanceCantMatch rough_tcs mb_tcs - = find ms us rest + = acc -- See Note [Instance lookup and orphan instances] | Just subst <- tcMatchTys tpl_tys tys - = find ((item, map (lookupTyVar subst) tpl_tvs) : ms) us rest + = ((item, map (lookupTyVar subst) tpl_tvs) : acc) + | otherwise + = acc + + check_unifier :: [ClsInst] -> PotentialUnifiers + check_unifier [] = NoUnifiers + check_unifier (item@ClsInst { is_tvs = tpl_tvs, is_tys = tpl_tys }:items) + | not (instIsVisible vis_mods item) + = check_unifier items -- See Note [Instance lookup and orphan instances] + | Just {} <- tcMatchTys tpl_tys tys = check_unifier items -- Does not match, so next check whether the things unify -- See Note [Overlapping instances] -- Ignore ones that are incoherent: Note [Incoherent instances] | isIncoherent item - = find ms us rest + = check_unifier items | otherwise = assertPpr (tys_tv_set `disjointVarSet` tpl_tv_set) @@ -868,10 +914,12 @@ lookupInstEnv' ie vis_mods cls tys -- We consider MaybeApart to be a case where the instance might -- apply in the future. This covers an instance like C Int and -- a target like [W] C (F a), where F is a type family. - SurelyApart -> find ms us rest + SurelyApart -> check_unifier items -- See Note [Infinitary substitution in lookup] - MaybeApart MARInfinite _ -> find ms us rest - _ -> find ms (item:us) rest + MaybeApart MARInfinite _ -> check_unifier items + _ -> + OneOrMoreUnifiers (item: getPotentialUnifiers (check_unifier items)) + where tpl_tv_set = mkVarSet tpl_tvs tys_tv_set = tyCoVarsOfTypes tys @@ -891,13 +939,12 @@ lookupInstEnv check_overlap_safe , ie_visible = vis_mods }) cls tys - = -- pprTrace "lookupInstEnv" (ppr cls <+> ppr tys $$ ppr home_ie) $ - (final_matches, final_unifs, unsafe_overlapped) + = (final_matches, final_unifs, unsafe_overlapped) where (home_matches, home_unifs) = lookupInstEnv' home_ie vis_mods cls tys (pkg_matches, pkg_unifs) = lookupInstEnv' pkg_ie vis_mods cls tys all_matches = home_matches ++ pkg_matches - all_unifs = home_unifs ++ pkg_unifs + all_unifs = home_unifs `mappend` pkg_unifs final_matches = pruneOverlappedMatches all_matches -- Even if the unifs is non-empty (an error situation) -- we still prune the matches, so that the error message isn't @@ -911,7 +958,7 @@ lookupInstEnv check_overlap_safe -- If the selected match is incoherent, discard all unifiers final_unifs = case final_matches of - (m:_) | isIncoherent (fst m) -> [] + (m:_) | isIncoherent (fst m) -> NoUnifiers _ -> all_unifs -- NOTE [Safe Haskell isSafeOverlap] diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index ec9b024fc5..c79ce8be1d 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -52,7 +52,7 @@ import GHC.Core.TyCo.Ppr ( pprTyVar, pprTyVars ) import GHC.Core.TyCon as TyCon import GHC.Core.Coercion.Axiom import GHC.Core.Unify -import GHC.Core.InstEnv ( instanceDFunId ) +import GHC.Core.InstEnv ( instanceDFunId, instEnvElts ) import GHC.Core.Coercion.Opt ( checkAxInstCo ) import GHC.Core.Opt.Arity ( typeArity ) @@ -448,7 +448,7 @@ interactiveInScope ictxt -- C.f. GHC.Tc.Module.setInteractiveContext, Desugar.deSugarExpr (cls_insts, _fam_insts) = ic_instances ictxt te1 = mkTypeEnvWithImplicits (ic_tythings ictxt) - te = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts) + te = extendTypeEnvWithIds te1 (map instanceDFunId $ instEnvElts cls_insts) ids = typeEnvIds te tyvars = tyCoVarsOfTypesList $ map idType ids -- Why the type variables? How can the top level envt have free tyvars? diff --git a/compiler/GHC/Core/RoughMap.hs b/compiler/GHC/Core/RoughMap.hs new file mode 100644 index 0000000000..cc64e96149 --- /dev/null +++ b/compiler/GHC/Core/RoughMap.hs @@ -0,0 +1,451 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE BangPatterns #-} + +-- | 'RoughMap' is an approximate finite map data structure keyed on +-- @['RoughMatchTc']@. This is useful when keying maps on lists of 'Type's +-- (e.g. an instance head). +module GHC.Core.RoughMap + ( -- * RoughMatchTc + RoughMatchTc(..) + , isRoughWildcard + , typeToRoughMatchTc + , RoughMatchLookupTc(..) + , typeToRoughMatchLookupTc + , roughMatchTcToLookup + + -- * RoughMap + , RoughMap + , emptyRM + , lookupRM + , lookupRM' + , insertRM + , filterRM + , filterMatchingRM + , elemsRM + , sizeRM + , foldRM + , unionRM + ) where + +import GHC.Prelude + +import GHC.Data.Bag +import GHC.Core.TyCon +import GHC.Core.TyCo.Rep +import GHC.Core.Type +import GHC.Utils.Outputable +import GHC.Types.Name +import GHC.Types.Name.Env + +import Control.Monad (join) +import Data.Data (Data) +import GHC.Utils.Misc +import Data.Bifunctor +import GHC.Utils.Panic + +{- +Note [RoughMap] +~~~~~~~~~~~~~~~ +We often want to compute whether one type matches another. That is, given +`ty1` and `ty2`, we want to know whether `ty1` is a substitution instance of `ty2`. + +We can bail out early by taking advantage of the following observation: + + If `ty2` is headed by a generative type constructor, say `tc`, + but `ty1` is not headed by that same type constructor, + then `ty1` does not match `ty2`. + +The idea is that we can use a `RoughMap` as a pre-filter, to produce a +short-list of candidates to examine more closely. + +This means we can avoid computing a full substitution if we represent types +as applications of known generative type constructors. So, after type synonym +expansion, we classify application heads into two categories ('RoughMatchTc') + + - `RM_KnownTc tc`: the head is the generative type constructor `tc`, + - `RM_Wildcard`: anything else. + +A (RoughMap val) is semantically a list of (key,[val]) pairs, where + key :: [RoughMatchTc] +So, writing # for `OtherTc`, and Int for `KnownTc "Int"`, we might have + [ ([#, Int, Maybe, #, Int], v1) + , ([Int, #, List], v2 ] + +This map is stored as a trie, so looking up a key is very fast. +See Note [Matching a RoughMap] and Note [Simple Matching Semantics] for details on +lookup. + +We lookup a key of type [RoughMatchLookupTc], and return the list of all values whose +keys "match": + +Given the above map, here are the results of some lookups: + Lookup key Result + ------------------------- + [Int, Int] [v1,v2] -- Matches because the prefix of both entries matches + [Int,Int,List] [v2] + [Bool] [] + +Notice that a single key can map to /multiple/ values. E.g. if we started +with (Maybe Int, val1) and (Maybe Bool, val2), we'd generate a RoughMap +that is semantically the list [( Maybe, [val1,val2] )] + +Note [RoughMap and beta reduction] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There is one tricky case we have to account for when matching a rough map due +to Note [Eta reduction for data families] in `GHC.Core.Coercion.Axiom`: +Consider that the user has written a program containing a data family: + +> data family Fam a b +> data instance Fam Int a = SomeType -- known henceforth as FamIntInst + +The LHS of this instance will be eta reduced, as described in Note [Eta +reduction for data families]. Consequently, we will end up with a `FamInst` +with `fi_tcs = [KnownTc Int]`. Naturally, we need RoughMap to return this +instance when queried for an instance with template, e.g., `[KnownTc Fam, +KnownTc Int, KnownTc Char]`. + +This explains the third clause of the mightMatch specification in Note [Simple Matching Semantics]. +As soon as the the lookup key runs out, the remaining instances might match. + +Note [Matching a RoughMap] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The /lookup key/ into a rough map (RoughMatchLookupTc) is slightly +different to the /insertion key/ (RoughMatchTc). Like the insertion +key each lookup argument is classified to a simpler key which +describes what could match that position. There are three +possibilities: + +* RML_KnownTc Name: The argument is headed by a known type + constructor. Example: 'Bool' is classified as 'RML_KnownTc Bool' + and '[Int]' is classified as `RML_KnownTc []` + +* RML_NoKnownTc: The argument is definitely not headed by any known + type constructor. Example: For instance matching 'a[sk], a[tau]' and 'F a[sk], F a[tau]' + are classified as 'RML_NoKnownTc', for family instance matching no examples. + +* RML_WildCard: The argument could match anything, we don't know + enough about it. For instance matching no examples, for type family matching, + things to do with variables. + +The interesting case for instance matching is the second case, because it does not appear in +an insertion key. The second case arises in two situations: + +1. The head of the application is a type variable. The type variable definitely + doesn't match with any of the KnownTC instances so we can discard them all. For example: + Show a[sk] or Show (a[sk] b[sk]). One place constraints like this arise is when + typechecking derived instances. +2. The head of the application is a known type family. + For example: F a[sk]. The application of F is stuck, and because + F is a type family it won't match any KnownTC instance so it's safe to discard + all these instances. + +Of course, these two cases can still match instances of the form `forall a . Show a =>`, +and those instances are retained as they are classified as RM_WildCard instances. + +Note [Matches vs Unifiers] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The lookupRM' function returns a pair of potential /matches/ and potential /unifiers/. +The potential matches is likely to be much smaller than the bag of potential unifiers due +to the reasoning about rigid type variables described in Note [Matching a RoughMap]. +On the other hand, the instances captured by the RML_NoKnownTC case can still potentially unify +with any instance (depending on the substituion of said rigid variable) so they can't be discounted +from the list of potential unifiers. This is achieved by the RML_NoKnownTC case continuing +the lookup for unifiers by replacing RML_NoKnownTC with RML_LookupOtherTC. + +This distinction between matches and unifiers is also important for type families. +During normal type family lookup, we care about matches and when checking for consistency +we care about the unifiers. This is evident in the code as `lookup_fam_inst_env` is +parameterised over a lookup function which either performs matching checking or unification +checking. + +In addition to this, we only care whether there are zero or non-zero potential +unifiers, even if we have many candidates, the search can stop before consulting +each candidate. We only need the full list of unifiers when displaying error messages. +Therefore the list is computed lazily so much work can be avoided constructing the +list in the first place. + +Note [Simple Matching Semantics] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose `rm` is a RoughMap representing a set of (key,vals) pairs, + where key::[RoughMapTc] and val::a. +Suppose I look up a key lk :: [RoughMapLookupTc] in `rm` +Then I get back (matches, unifiers) where + matches = [ vals | (key,vals) <- rm, key `mightMatch` lk ] + unifiers = [ vals | (key,vals) <- rm, key `mightUnify` lk ] + +Where mightMatch is defined like this: + + mightMatch :: [RoughMapTc] -> [RoughMapLookupTc] -> Bool + mightMatch [] [] = True -- A perfectly sized match might match + mightMatch key [] = True -- A shorter lookup key matches everything + mightMatch [] (_:_) = True -- If the lookup key is longer, then still might match + -- Note [RoughMatch and beta reduction] + mightMatch (k:ks) (lk:lks) = + = case (k,lk) of + -- Standard case, matching on a specific known TyCon. + (RM_KnownTc n1, RML_KnownTc n2) -> n1==n2 && mightMatch ks lks + -- For example, if the key for 'Show Bool' is [RM_KnownTc Show, RM_KnownTc Bool] + ---and we match against (Show a[sk]) [RM_KnownTc Show, RML_NoKnownTc] + -- then Show Bool can never match Show a[sk] so return False. + (RM_KnownTc _, RML_NoKnownTc) -> False + -- Wildcard cases don't inform us anything about the match. + (RM_WildCard, _ ) -> mightMatch ks lks + (_, RML_WildCard) -> mightMatch ks lks + + -- Might unify is very similar to mightMatch apart from RML_NoKnownTc may + -- unify with any instance. + mightUnify :: [RoughMapTc] -> [RoughMapLookupTc] -> Bool + mightUnify [] [] = True -- A perfectly sized match might unify + mightUnify key [] = True -- A shorter lookup key matches everything + mightUnify [] (_:_) = True + mightUnify (k:ks) (lk:lks) = + = case (k,lk) of + (RM_KnownTc n1, RML_KnownTc n2) -> n1==n2 && mightUnify ks lks + (RM_KnownTc _, RML_NoKnownTc) -> mightUnify (k:ks) (RML_WildCard:lks) + (RM_WildCard, _ ) -> mightUnify ks lks + (_, RML_WildCard) -> mightUnify ks lks + + +The guarantee that RoughMap provides is that + +if + insert_ty `tcMatchTy` lookup_ty +then definitely + typeToRoughMatchTc insert_ty `mightMatch` typeToRoughMatchLookupTc lookup_ty +but not vice versa + +this statement encodes the intuition that the RoughMap is used as a quick pre-filter +to remove instances from the matching pool. The contrapositive states that if the +RoughMap reports that the instance doesn't match then `tcMatchTy` will report that the +types don't match as well. + +-} + +-- Key for insertion into a RoughMap +data RoughMatchTc + = RM_KnownTc Name -- INVARIANT: Name refers to a TyCon tc that responds + -- true to `isGenerativeTyCon tc Nominal`. See + -- Note [Rough matching in class and family instances] + | RM_WildCard -- e.g. type variable at the head + deriving( Data ) + +-- Key for lookup into a RoughMap +-- See Note [Matching a RoughMap] +data RoughMatchLookupTc + = RML_KnownTc Name -- ^ The position only matches the specified KnownTc + | RML_NoKnownTc -- ^ The position definitely doesn't match any KnownTc + | RML_WildCard -- ^ The position can match anything + deriving ( Data ) + +instance Outputable RoughMatchLookupTc where + ppr (RML_KnownTc nm) = text "RML_KnownTc" <+> ppr nm + ppr RML_NoKnownTc = text "RML_NoKnownTC" + ppr RML_WildCard = text "_" + +roughMatchTcToLookup :: RoughMatchTc -> RoughMatchLookupTc +roughMatchTcToLookup (RM_KnownTc n) = RML_KnownTc n +roughMatchTcToLookup RM_WildCard = RML_WildCard + +instance Outputable RoughMatchTc where + ppr (RM_KnownTc nm) = text "KnownTc" <+> ppr nm + ppr RM_WildCard = text "OtherTc" + +isRoughWildcard :: RoughMatchTc -> Bool +isRoughWildcard RM_WildCard = True +isRoughWildcard (RM_KnownTc {}) = False + +typeToRoughMatchLookupTc :: Type -> RoughMatchLookupTc +typeToRoughMatchLookupTc ty + | Just (ty', _) <- splitCastTy_maybe ty = typeToRoughMatchLookupTc ty' + | otherwise = + case splitAppTys ty of + -- Case 1: Head of application is a type variable, does not match any KnownTc. + (TyVarTy {}, _) -> RML_NoKnownTc + (TyConApp tc _, _) + -- Case 2: Head of application is a known type constructor, hence KnownTc. + | not (isTypeFamilyTyCon tc) -> RML_KnownTc $! tyConName tc + -- Case 3: Head is a type family so it's stuck and therefore doesn't match + -- any KnownTc + | isTypeFamilyTyCon tc -> RML_NoKnownTc + -- Fallthrough: Otherwise, anything might match this position + _ -> RML_WildCard + +typeToRoughMatchTc :: Type -> RoughMatchTc +typeToRoughMatchTc ty + | Just (ty', _) <- splitCastTy_maybe ty = typeToRoughMatchTc ty' + | Just (tc,_) <- splitTyConApp_maybe ty + , not (isTypeFamilyTyCon tc) = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) + RM_KnownTc $! tyConName tc + -- See Note [Rough matching in class and family instances] + | otherwise = RM_WildCard + +-- | Trie of @[RoughMatchTc]@ +-- +-- *Examples* +-- @ +-- insert [OtherTc] 1 +-- insert [OtherTc] 2 +-- lookup [OtherTc] == [1,2] +-- @ +data RoughMap a = RM { rm_empty :: Bag a + , rm_known :: DNameEnv (RoughMap a) + -- See Note [InstEnv determinism] in GHC.Core.InstEnv + , rm_unknown :: RoughMap a } + | RMEmpty -- an optimised (finite) form of emptyRM + -- invariant: Empty RoughMaps are always represented with RMEmpty + + deriving (Functor) + +instance Outputable a => Outputable (RoughMap a) where + ppr (RM empty known unknown) = + vcat [text "RM" + , nest 2 (vcat [ text "Empty:" <+> ppr empty + , text "Known:" <+> ppr known + , text "Unknown:" <+> ppr unknown])] + ppr RMEmpty = text "{}" + +emptyRM :: RoughMap a +emptyRM = RMEmpty + +-- | Order of result is deterministic. +lookupRM :: [RoughMatchLookupTc] -> RoughMap a -> [a] +lookupRM tcs rm = bagToList (fst $ lookupRM' tcs rm) + + +-- | N.B. Returns a 'Bag' for matches, which allows us to avoid rebuilding all of the lists +-- we find in 'rm_empty', which would otherwise be necessary due to '++' if we +-- returned a list. We use a list for unifiers becuase the tail is computed lazily and +-- we often only care about the first couple of potential unifiers. Constructing a +-- bag forces the tail which performs much too much work. +-- +-- See Note [Matching a RoughMap] +-- See Note [Matches vs Unifiers] +lookupRM' :: [RoughMatchLookupTc] -> RoughMap a -> (Bag a -- Potential matches + , [a]) -- Potential unifiers +lookupRM' _ RMEmpty = (emptyBag, []) +-- See Note [Simple Matching Semantics] about why we return everything when the lookup +-- key runs out. +lookupRM' [] rm = let m = elemsRM rm + in (listToBag m, m) +lookupRM' (RML_KnownTc tc : tcs) rm = + let (common_m, common_u) = lookupRM' tcs (rm_unknown rm) + (m, u) = maybe (emptyBag, []) (lookupRM' tcs) (lookupDNameEnv (rm_known rm) tc) + in (rm_empty rm `unionBags` common_m `unionBags` m + , bagToList (rm_empty rm) ++ common_u ++ u) +-- A RML_NoKnownTC does **not** match any KnownTC but can unify +lookupRM' (RML_NoKnownTc : tcs) rm = + + let (u_m, _u_u) = lookupRM' tcs (rm_unknown rm) + in (rm_empty rm `unionBags` u_m -- Definitely don't match + , snd $ lookupRM' (RML_WildCard : tcs) rm) -- But could unify.. + +lookupRM' (RML_WildCard : tcs) rm = + let (m, u) = bimap unionManyBags concat (mapAndUnzip (lookupRM' tcs) (eltsDNameEnv $ rm_known rm)) + (u_m, u_u) = lookupRM' tcs (rm_unknown rm) + in (rm_empty rm `unionBags` u_m `unionBags` m + , bagToList (rm_empty rm) ++ u_u ++ u) + +unionRM :: RoughMap a -> RoughMap a -> RoughMap a +unionRM RMEmpty a = a +unionRM a RMEmpty = a +unionRM a b = + RM { rm_empty = rm_empty a `unionBags` rm_empty b + , rm_known = plusDNameEnv_C unionRM (rm_known a) (rm_known b) + , rm_unknown = rm_unknown a `unionRM` rm_unknown b + } + + +insertRM :: [RoughMatchTc] -> a -> RoughMap a -> RoughMap a +insertRM k v RMEmpty = + insertRM k v $ RM { rm_empty = emptyBag + , rm_known = emptyDNameEnv + , rm_unknown = emptyRM } +insertRM [] v rm@(RM {}) = + -- See Note [Simple Matching Semantics] + rm { rm_empty = v `consBag` rm_empty rm } +insertRM (RM_KnownTc k : ks) v rm@(RM {}) = + rm { rm_known = alterDNameEnv f (rm_known rm) k } + where + f Nothing = Just $ (insertRM ks v emptyRM) + f (Just m) = Just $ (insertRM ks v m) +insertRM (RM_WildCard : ks) v rm@(RM {}) = + rm { rm_unknown = insertRM ks v (rm_unknown rm) } + +filterRM :: (a -> Bool) -> RoughMap a -> RoughMap a +filterRM _ RMEmpty = RMEmpty +filterRM pred rm = + normalise $ RM { + rm_empty = filterBag pred (rm_empty rm), + rm_known = mapDNameEnv (filterRM pred) (rm_known rm), + rm_unknown = filterRM pred (rm_unknown rm) + } + +-- | Place a 'RoughMap' in normal form, turning all empty 'RM's into +-- 'RMEmpty's. Necessary after removing items. +normalise :: RoughMap a -> RoughMap a +normalise RMEmpty = RMEmpty +normalise (RM empty known RMEmpty) + | isEmptyBag empty + , isEmptyDNameEnv known = RMEmpty +normalise rm = rm + +-- | Filter all elements that might match a particular key with the given +-- predicate. +filterMatchingRM :: (a -> Bool) -> [RoughMatchTc] -> RoughMap a -> RoughMap a +filterMatchingRM _ _ RMEmpty = RMEmpty +filterMatchingRM pred [] rm = filterRM pred rm +filterMatchingRM pred (RM_KnownTc tc : tcs) rm = + normalise $ RM { + rm_empty = filterBag pred (rm_empty rm), + rm_known = alterDNameEnv (join . fmap (dropEmpty . filterMatchingRM pred tcs)) (rm_known rm) tc, + rm_unknown = filterMatchingRM pred tcs (rm_unknown rm) + } +filterMatchingRM pred (RM_WildCard : tcs) rm = + normalise $ RM { + rm_empty = filterBag pred (rm_empty rm), + rm_known = mapDNameEnv (filterMatchingRM pred tcs) (rm_known rm), + rm_unknown = filterMatchingRM pred tcs (rm_unknown rm) + } + +dropEmpty :: RoughMap a -> Maybe (RoughMap a) +dropEmpty RMEmpty = Nothing +dropEmpty rm = Just rm + +elemsRM :: RoughMap a -> [a] +elemsRM = foldRM (:) [] + +foldRM :: (a -> b -> b) -> b -> RoughMap a -> b +foldRM f = go + where + -- N.B. local worker ensures that the loop can be specialised to the fold + -- function. + go z RMEmpty = z + go z (RM{ rm_unknown = unk, rm_known = known, rm_empty = empty}) = + foldr + f + (foldDNameEnv + (flip go) + (go z unk) + known + ) + empty + +nonDetStrictFoldRM :: (b -> a -> b) -> b -> RoughMap a -> b +nonDetStrictFoldRM f = go + where + -- N.B. local worker ensures that the loop can be specialised to the fold + -- function. + go !z RMEmpty = z + go z rm@(RM{}) = + foldl' + f + (nonDetStrictFoldDNameEnv + (flip go) + (go z (rm_unknown rm)) + (rm_known rm) + ) + (rm_empty rm) + +sizeRM :: RoughMap a -> Int +sizeRM = nonDetStrictFoldRM (\acc _ -> acc + 1) 0 diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs index a4dbdcb75d..a18899ec09 100644 --- a/compiler/GHC/Core/Unify.hs +++ b/compiler/GHC/Core/Unify.hs @@ -11,8 +11,8 @@ module GHC.Core.Unify ( tcMatchTyX_BM, ruleMatchTyKiX, -- * Rough matching - RoughMatchTc(..), roughMatchTcs, instanceCantMatch, - typesCantMatch, isRoughOtherTc, + RoughMatchTc(..), roughMatchTcs, roughMatchTcsLookup, instanceCantMatch, + typesCantMatch, isRoughWildcard, -- Side-effect free unification tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis, @@ -39,6 +39,7 @@ import GHC.Core.TyCon import GHC.Core.TyCo.Rep import GHC.Core.TyCo.FVs ( tyCoVarsOfCoList, tyCoFVsOfTypes ) import GHC.Core.TyCo.Subst ( mkTvSubst ) +import GHC.Core.RoughMap import GHC.Core.Map.Type import GHC.Utils.FV( FV, fvVarSet, fvVarList ) import GHC.Utils.Misc @@ -49,11 +50,9 @@ import GHC.Types.Unique.FM import GHC.Types.Unique.Set import {-# SOURCE #-} GHC.Tc.Utils.TcType ( tcEqType ) import GHC.Exts( oneShot ) -import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Data.FastString -import Data.Data ( Data ) import Data.List ( mapAccumL ) import Control.Monad import qualified Data.Semigroup as S @@ -291,27 +290,11 @@ But it is never albeit perhaps only after 'a' is instantiated. -} -data RoughMatchTc - = KnownTc Name -- INVARIANT: Name refers to a TyCon tc that responds - -- true to `isGenerativeTyCon tc Nominal`. See - -- Note [Rough matching in class and family instances] - | OtherTc -- e.g. type variable at the head - deriving( Data ) - -isRoughOtherTc :: RoughMatchTc -> Bool -isRoughOtherTc OtherTc = True -isRoughOtherTc (KnownTc {}) = False - roughMatchTcs :: [Type] -> [RoughMatchTc] -roughMatchTcs tys = map rough tys - where - rough ty - | Just (ty', _) <- splitCastTy_maybe ty = rough ty' - | Just (tc,_) <- splitTyConApp_maybe ty - , not (isTypeFamilyTyCon tc) = assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) $ - KnownTc (tyConName tc) - -- See Note [Rough matching in class and family instances] - | otherwise = OtherTc +roughMatchTcs tys = map typeToRoughMatchTc tys + +roughMatchTcsLookup :: [Type] -> [RoughMatchLookupTc] +roughMatchTcsLookup tys = map typeToRoughMatchLookupTc tys instanceCantMatch :: [RoughMatchTc] -> [RoughMatchTc] -> Bool -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot @@ -321,7 +304,7 @@ instanceCantMatch (mt : ts) (ma : as) = itemCantMatch mt ma || instanceCantMatch instanceCantMatch _ _ = False -- Safe itemCantMatch :: RoughMatchTc -> RoughMatchTc -> Bool -itemCantMatch (KnownTc t) (KnownTc a) = t /= a +itemCantMatch (RM_KnownTc t) (RM_KnownTc a) = t /= a itemCantMatch _ _ = False |