X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FInstEnv.lhs;h=07f68f7b91ce91c6c271b201f7fdce8ddcb20027;hp=70e61661d3a3bc179a853fac14c2535ef4d94fb9;hb=16b9e80dc14db24509f051f294b5b51943285090;hpb=872a4a0fd2a99ea96bee36f5398e87002659e014 diff --git a/compiler/types/InstEnv.lhs b/compiler/types/InstEnv.lhs index 70e6166..07f68f7 100644 --- a/compiler/types/InstEnv.lhs +++ b/compiler/types/InstEnv.lhs @@ -1,4 +1,5 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % \section[InstEnv]{Utilities for typechecking instance declarations} @@ -14,31 +15,26 @@ module InstEnv ( InstEnv, emptyInstEnv, extendInstEnv, extendInstEnvList, lookupInstEnv, instEnvElts, - classInstances, + classInstances, instanceBindFun, instanceCantMatch, roughMatchTcs ) where #include "HsVersions.h" -import Class ( Class ) -import Var ( Id, TyVar, isTcTyVar ) +import Class +import Var import VarSet -import Name ( Name, NamedThing(..), getSrcLoc, nameIsLocalOrFrom, nameModule ) -import OccName ( OccName ) -import NameSet ( unionNameSets, unitNameSet, nameSetToList ) -import Type ( TvSubst ) -import TcType ( Type, PredType, tcEqType, - tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar, - pprThetaArrow, pprClassPred, - tyClsNamesOfType, tcSplitTyConApp_maybe - ) -import TyCon ( tyConName ) -import Unify ( tcMatchTys, tcUnifyTys, BindFlag(..) ) +import Name +import TcType +import TyCon +import Unify import Outputable -import UniqFM ( UniqFM, lookupUFM, emptyUFM, addToUFM_C, eltsUFM ) -import Id ( idType, idName ) -import SrcLoc ( pprDefnLoc ) -import Maybe ( isJust, isNothing ) +import BasicTypes +import UniqFM +import Id +import FastString + +import Data.Maybe ( isJust, isNothing ) \end{code} @@ -49,80 +45,75 @@ import Maybe ( isJust, isNothing ) %************************************************************************ \begin{code} -type DFunId = Id data Instance = Instance { is_cls :: Name -- Class name - -- Used for "rough matching"; see note below + -- Used for "rough matching"; see Note [Rough-match field] + -- INVARIANT: is_tcs = roughMatchTcs is_tys , is_tcs :: [Maybe Name] -- Top of type args - -- Used for "proper matching"; see note + -- Used for "proper matching"; see Note [Proper-match fields] , is_tvs :: TyVarSet -- Template tyvars for full match , is_tys :: [Type] -- Full arg types + -- INVARIANT: is_dfun Id has type + -- forall is_tvs. (...) => is_cls is_tys + + , is_dfun :: DFunId -- See Note [Haddock assumptions] + , is_flag :: OverlapFlag -- See detailed comments with + -- the decl of BasicTypes.OverlapFlag + } +\end{code} - , is_dfun :: DFunId - , is_flag :: OverlapFlag - - , is_orph :: Maybe OccName } - --- The "rough-match" fields --- ~~~~~~~~~~~~~~~~~~~~~~~~~ --- The is_cls, is_args fields allow a "rough match" to be done --- without poking inside the DFunId. Poking the DFunId forces --- us to suck in all the type constructors etc it involves, --- which is a total waste of time if it has no chance of matching --- So the Name, [Maybe Name] fields allow us to say "definitely --- does not match", based only on the Name. --- --- In is_tcs, --- Nothing means that this type arg is a type variable --- --- (Just n) means that this type arg is a --- TyConApp with a type constructor of n. --- This is always a real tycon, never a synonym! --- (Two different synonyms might match, but two --- different real tycons can't.) --- NB: newtypes are not transparent, though! --- --- The "proper-match" fields --- ~~~~~~~~~~~~~~~~~~~~~~~~~ --- The is_tvs, is_tys fields are simply cahced values, pulled --- out (lazily) from the dfun id. They are cached here simply so --- that we don't need to decompose the DFunId each time we want --- to match it. The hope is that the fast-match fields mean --- that we often never poke th proper-match fields --- --- However, note that: --- * is_tvs must be a superset of the free vars of is_tys --- --- * The is_dfun must itself be quantified over exactly is_tvs --- (This is so that we can use the matching substitution to --- instantiate the dfun's context.) --- --- The "orphan" field --- ~~~~~~~~~~~~~~~~~~ --- An instance is an orphan if its head (after the =>) mentions --- nothing defined in this module. --- --- Just n The head mentions n, which is defined in this module --- This is used for versioning; the instance decl is --- considered part of the defn of n when computing versions --- --- Nothing The head mentions nothing defined in this module --- --- If a module contains any orphans, then its interface file is read --- regardless, so that its instances are not missed. --- --- Functional dependencies worsen the situation a bit. Consider --- class C a b | a -> b --- In some other module we might have --- module M where --- data T = ... --- instance C Int T where ... --- This isn't considered an orphan, so we will only read M's interface --- if something from M is used (e.g. T). So there's a risk we'll --- miss the improvement from the instance. Workaround: import M. +Note [Rough-match field] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The is_cls, is_tcs fields allow a "rough match" to be done +without poking inside the DFunId. Poking the DFunId forces +us to suck in all the type constructors etc it involves, +which is a total waste of time if it has no chance of matching +So the Name, [Maybe Name] fields allow us to say "definitely +does not match", based only on the Name. + +In is_tcs, + Nothing means that this type arg is a type variable + + (Just n) means that this type arg is a + TyConApp with a type constructor of n. + This is always a real tycon, never a synonym! + (Two different synonyms might match, but two + different real tycons can't.) + NB: newtypes are not transparent, though! + +Note [Proper-match fields] +~~~~~~~~~~~~~~~~~~~~~~~~~ +The is_tvs, is_tys fields are simply cached values, pulled +out (lazily) from the dfun id. They are cached here simply so +that we don't need to decompose the DFunId each time we want +to match it. The hope is that the fast-match fields mean +that we often never poke th proper-match fields + +However, note that: + * is_tvs must be a superset of the free vars of is_tys + + * The is_dfun must itself be quantified over exactly is_tvs + (This is so that we can use the matching substitution to + instantiate the dfun's context.) + +Note [Haddock assumptions] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +For normal user-written instances, Haddock relies on + + * the SrcSpan of + * the Name of + * the is_dfun of + * an Instance + +being equal to + + * the SrcSpan of + * the instance head type of + * the InstDecl used to construct the Instance. +\begin{code} instanceDFunId :: Instance -> DFunId instanceDFunId = is_dfun @@ -152,51 +143,57 @@ instance Outputable Instance where pprInstance :: Instance -> SDoc -- Prints the Instance as an instance declaration -pprInstance ispec@(Instance { is_flag = flag }) +pprInstance ispec = hang (pprInstanceHdr ispec) - 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc ispec))) + 2 (ptext (sLit "--") <+> pprNameLoc (getName ispec)) -- * pprInstanceHdr is used in VStudio to populate the ClassView tree pprInstanceHdr :: Instance -> SDoc -- Prints the Instance as an instance declaration pprInstanceHdr ispec@(Instance { is_flag = flag }) - = ptext SLIT("instance") <+> ppr flag - <+> sep [pprThetaArrow theta, pprClassPred clas tys] + = getPprStyle $ \ sty -> + let theta_to_print + | debugStyle sty = theta + | otherwise = drop (dfunNSilent dfun) theta + in ptext (sLit "instance") <+> ppr flag + <+> sep [pprThetaArrow theta_to_print, ppr res_ty] where - (_, theta, clas, tys) = instanceHead ispec + dfun = is_dfun ispec + (_, theta, res_ty) = tcSplitSigmaTy (idType dfun) -- Print without the for-all, which the programmer doesn't write pprInstances :: [Instance] -> SDoc pprInstances ispecs = vcat (map pprInstance ispecs) -instanceHead :: Instance -> ([TyVar], [PredType], Class, [Type]) -instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec)) - -mkLocalInstance :: DFunId -> OverlapFlag -> Instance +instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type]) +-- Returns the *source* theta, without the silent arguments +instanceHead ispec + = (tvs, drop n_silent theta, cls, tys) + where + (tvs, theta, tau) = tcSplitSigmaTy (idType dfun) + (cls, tys) = tcSplitDFunHead tau + dfun = is_dfun ispec + n_silent = dfunNSilent dfun + +mkLocalInstance :: DFunId + -> OverlapFlag + -> Instance -- Used for local instances, where we can safely pull on the DFunId mkLocalInstance dfun oflag = Instance { is_flag = oflag, is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys, - is_cls = cls_name, is_tcs = roughMatchTcs tys, - is_orph = orph } + is_cls = className cls, is_tcs = roughMatchTcs tys } where (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun) - mod = nameModule (idName dfun) - cls_name = getName cls - tycl_names = foldr (unionNameSets . tyClsNamesOfType) - (unitNameSet cls_name) tys - orph = case filter (nameIsLocalOrFrom mod) (nameSetToList tycl_names) of - [] -> Nothing - (n:ns) -> Just (getOccName n) - -mkImportedInstance :: Name -> [Maybe Name] -> Maybe OccName + +mkImportedInstance :: Name -> [Maybe Name] -> DFunId -> OverlapFlag -> Instance -- Used for imported instances, where we get the rough-match stuff -- from the interface file -mkImportedInstance cls mb_tcs orph dfun oflag +mkImportedInstance cls mb_tcs dfun oflag = Instance { is_flag = oflag, is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys, - is_cls = cls, is_tcs = mb_tcs, is_orph = orph } + is_cls = cls, is_tcs = mb_tcs } where (tvs, _, _, tys) = tcSplitDFunTy (idType dfun) @@ -212,40 +209,7 @@ instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool -- possibly be instantiated to actual, nor vice versa; -- False is non-committal instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as -instanceCantMatch ts as = False -- Safe - ---------------------------------------------------- -data OverlapFlag - = NoOverlap -- This instance must not overlap another - - | OverlapOk -- Silently ignore this instance if you find a - -- more specific one that matches the constraint - -- you are trying to resolve - -- - -- Example: constraint (Foo [Int]) - -- instances (Foo [Int]) - -- (Foo [a]) OverlapOk - -- Since the second instance has the OverlapOk flag, - -- the first instance will be chosen (otherwise - -- its ambiguous which to choose) - - | Incoherent -- Like OverlapOk, but also ignore this instance - -- if it doesn't match the constraint you are - -- trying to resolve, but could match if the type variables - -- in the constraint were instantiated - -- - -- Example: constraint (Foo [b]) - -- instances (Foo [Int]) Incoherent - -- (Foo [a]) - -- Without the Incoherent flag, we'd complain that - -- instantiating 'b' would change which instance - -- was chosen - deriving( Eq ) - -instance Outputable OverlapFlag where - ppr NoOverlap = empty - ppr OverlapOk = ptext SLIT("[overlap ok]") - ppr Incoherent = ptext SLIT("[incoherent]") +instanceCantMatch _ _ = False -- Safe \end{code} @@ -399,6 +363,9 @@ data ClsInstEnv -- If *not* then the common case of looking up -- (C a b c) can fail immediately +instance Outputable ClsInstEnv where + ppr (ClsIE is b) = ptext (sLit "ClsIE") <+> ppr b <+> pprInstances is + -- INVARIANTS: -- * The is_tvs are distinct in each Instance -- of a ClsInstEnv (so we can safely unify them) @@ -432,12 +399,12 @@ extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs }) add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts) (ins_tyvar || cur_tyvar) ins_tyvar = not (any isJust mb_tcs) -\end{code} +\end{code} %************************************************************************ %* * -\subsection{Looking up an instance} + Looking up an instance %* * %************************************************************************ @@ -446,20 +413,41 @@ the env is kept ordered, the first match must be the only one. The thing we are looking up can have an arbitrary "flexi" part. \begin{code} -lookupInstEnv :: (InstEnv -- External package inst-env - ,InstEnv) -- Home-package inst-env - -> Class -> [Type] -- What we are looking for - -> ([(TvSubst, Instance)], -- Successful matches - [Instance]) -- These don't match but do unify - -- The second component of the tuple happens when we look up - -- Foo [a] - -- in an InstEnv that has entries for - -- Foo [Int] - -- Foo [b] - -- Then which we choose would depend on the way in which 'a' - -- is instantiated. So we report that Foo [b] is a match (mapping b->a) - -- but Foo [Int] is a unifier. This gives the caller a better chance of - -- giving a suitable error messagen +type InstTypes = [Either TyVar Type] + -- Right ty => Instantiate with this type + -- Left tv => Instantiate with any type of this tyvar's kind + +type InstMatch = (Instance, InstTypes) +\end{code} + +Note [InstTypes: instantiating types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A successful match is an Instance, together with the types at which + the dfun_id in the Instance should be instantiated +The instantiating types are (Mabye Type)s because the dfun +might have some tyvars that *only* appear in arguments + dfun :: forall a b. C a b, Ord b => D [a] +When we match this against D [ty], we return the instantiating types + [Right ty, Left b] +where the Nothing indicates that 'b' can be freely instantiated. +(The caller instantiates it to a flexi type variable, which will presumably + presumably later become fixed via functional dependencies.) + +\begin{code} +lookupInstEnv :: (InstEnv, InstEnv) -- External and home package inst-env + -> Class -> [Type] -- What we are looking for + -> ([InstMatch], -- Successful matches + [Instance]) -- These don't match but do unify + +-- The second component of the result pair happens when we look up +-- Foo [a] +-- in an InstEnv that has entries for +-- Foo [Int] +-- Foo [b] +-- Then which we choose would depend on the way in which 'a' +-- is instantiated. So we report that Foo [b] is a match (mapping b->a) +-- but Foo [Int] is a unifier. This gives the caller a better chance of +-- giving a suitable error messagen lookupInstEnv (pkg_ie, home_ie) cls tys = (pruned_matches, all_unifs) @@ -470,10 +458,11 @@ lookupInstEnv (pkg_ie, home_ie) cls tys (pkg_matches, pkg_unifs) = lookup pkg_ie all_matches = home_matches ++ pkg_matches all_unifs = home_unifs ++ pkg_unifs - pruned_matches - | null all_unifs = foldr insert_overlapping [] all_matches - | otherwise = all_matches -- Non-empty unifs is always an error situation, - -- so don't attempt to pune the matches + pruned_matches = foldr insert_overlapping [] all_matches + -- Even if the unifs is non-empty (an error situation) + -- we still prune the matches, so that the error message isn't + -- misleading (complaining of multiple matches when some should be + -- overlapped away) -------------- lookup env = case lookupUFM env cls of @@ -488,6 +477,12 @@ lookupInstEnv (pkg_ie, home_ie) cls tys -> find [] [] insts -------------- + lookup_tv :: TvSubst -> TyVar -> Either TyVar Type + -- See Note [InstTypes: instantiating types] + lookup_tv subst tv = case lookupTyVar subst tv of + Just ty -> Right ty + Nothing -> Left tv + find ms us [] = (ms, us) find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs, is_tys = tpl_tys, is_flag = oflag, @@ -497,48 +492,31 @@ lookupInstEnv (pkg_ie, home_ie) cls tys = find ms us rest | Just subst <- tcMatchTys tpl_tvs tpl_tys tys - = find ((subst,item):ms) us rest + = let + (dfun_tvs, _) = tcSplitForAllTys (idType dfun) + in + ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant + find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest -- Does not match, so next check whether the things unify - -- See Note [overlapping instances] above + -- See Note [Overlapping instances] above | Incoherent <- oflag = find ms us rest | otherwise - = ASSERT2( not (tyVarsOfTypes tys `intersectsVarSet` tpl_tvs), - (ppr cls <+> ppr tys <+> ppr all_tvs) $$ - (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys) + = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs, + (ppr cls <+> ppr tys <+> ppr all_tvs) $$ + (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys) ) -- Unification will break badly if the variables overlap -- They shouldn't because we allocate separate uniques for them - case tcUnifyTys bind_fn tpl_tys tys of + case tcUnifyTys instanceBindFun tpl_tys tys of Just _ -> find ms (item:us) rest - Nothing -> find ms us rest + Nothing -> find ms us rest --------------- -bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem - | otherwise = BindMe - -- The key_tys can contain skolem constants, and we can guarantee that those - -- are never going to be instantiated to anything, so we should not involve - -- them in the unification test. Example: - -- class Foo a where { op :: a -> Int } - -- instance Foo a => Foo [a] -- NB overlap - -- instance Foo [Int] -- NB overlap - -- data T = forall a. Foo a => MkT a - -- f :: T -> Int - -- f (MkT x) = op [x,x] - -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd - -- complain, saying that the choice of instance depended on the instantiation - -- of 'a'; but of course it isn't *going* to be instantiated. - -- - -- We do this only for pattern-bound skolems. For example we reject - -- g :: forall a => [a] -> Int - -- g x = op x - -- on the grounds that the correct instance depends on the instantiation of 'a' - --------------- -insert_overlapping :: (TvSubst, Instance) -> [(TvSubst, Instance)] - -> [(TvSubst, Instance)] +insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch] -- Add a new solution, knocking out strictly less specific ones insert_overlapping new_item [] = [new_item] insert_overlapping new_item (item:items) @@ -554,14 +532,55 @@ insert_overlapping new_item (item:items) new_beats_old = new_item `beats` item old_beats_new = item `beats` new_item - (_, instA) `beats` (_, instB) - = overlap_ok && - isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA)) - -- A beats B if A is more specific than B, and B admits overlap - -- I.e. if B can be instantiated to match A - where - overlap_ok = case is_flag instB of - NoOverlap -> False - other -> True + (instA, _) `beats` (instB, _) + = overlap_ok && + isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA)) + -- A beats B if A is more specific than B, + -- (ie. if B can be instantiated to match A) + -- and overlap is permitted + where + -- Overlap permitted if *either* instance permits overlap + -- This is a change (Trac #3877, Dec 10). It used to + -- require that instB (the less specific one) permitted overlap. + overlap_ok = case (is_flag instA, is_flag instB) of + (NoOverlap, NoOverlap) -> False + _ -> True +\end{code} + + +%************************************************************************ +%* * + Binding decisions +%* * +%************************************************************************ + +\begin{code} +instanceBindFun :: TyVar -> BindFlag +instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar tv = Skolem + | otherwise = BindMe + -- Note [Binding when looking up instances] \end{code} +Note [Binding when looking up instances] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When looking up in the instance environment, or family-instance environment, +we are careful about multiple matches, as described above in +Note [Overlapping instances] + +The key_tys can contain skolem constants, and we can guarantee that those +are never going to be instantiated to anything, so we should not involve +them in the unification test. Example: + class Foo a where { op :: a -> Int } + instance Foo a => Foo [a] -- NB overlap + instance Foo [Int] -- NB overlap + data T = forall a. Foo a => MkT a + f :: T -> Int + f (MkT x) = op [x,x] +The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd +complain, saying that the choice of instance depended on the instantiation +of 'a'; but of course it isn't *going* to be instantiated. + +We do this only for isOverlappableTyVar skolems. For example we reject + g :: forall a => [a] -> Int + g x = op x +on the grounds that the correct instance depends on the instantiation of 'a'