X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FFamInstEnv.lhs;h=5b4374afa2e834cad5c9f283e805baf5d82a4462;hp=c44c2003ad85ca3ac1b5267cbb84f8c8766d94d0;hb=0af06ed99ed56341adfdda4a92a0a36678780109;hpb=ab22f4e6456820c1b5169d75f5975a94e61f54ce diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index c44c200..5b4374a 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -6,31 +6,35 @@ FamInstEnv: Type checked family instance declarations \begin{code} module FamInstEnv ( - FamInst(..), famInstTyCon, pprFamInst, pprFamInstHdr, pprFamInsts, + FamInst(..), famInstTyCon, famInstTyVars, + pprFamInst, pprFamInstHdr, pprFamInsts, famInstHead, mkLocalFamInst, mkImportedFamInst, - FamInstEnv, emptyFamInstEnv, extendFamInstEnv, extendFamInstEnvList, + FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, + extendFamInstEnv, extendFamInstEnvList, famInstEnvElts, familyInstances, - lookupFamInstEnv + + lookupFamInstEnv, lookupFamInstEnvConflicts, + + -- Normalisation + topNormaliseType ) where #include "HsVersions.h" import InstEnv import Unify -import TcType import Type +import TypeRep import TyCon +import Coercion import VarSet -import Var import Name -import OccName -import SrcLoc import UniqFM import Outputable - -import Maybe -import Monad +import Maybes +import Util +import FastString \end{code} @@ -43,13 +47,19 @@ import Monad \begin{code} data FamInst = FamInst { fi_fam :: Name -- Family name + -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of + -- Just (tc, tys) -> tc -- Used for "rough matching"; same idea as for class instances , fi_tcs :: [Maybe Name] -- Top of type args + -- INVARIANT: fi_tcs = roughMatchTcs fi_tys -- Used for "proper matching"; ditto , fi_tvs :: TyVarSet -- Template tyvars for full match , fi_tys :: [Type] -- Full arg types + -- INVARIANT: fi_tvs = tyConTyVars fi_tycon + -- fi_tys = case tyConFamInst_maybe fi_tycon of + -- Just (_, tys) -> tys , fi_tycon :: TyCon -- Representation tycon } @@ -58,6 +68,9 @@ data FamInst -- famInstTyCon :: FamInst -> TyCon famInstTyCon = fi_tycon + +famInstTyVars :: FamInst -> TyVarSet +famInstTyVars = fi_tvs \end{code} \begin{code} @@ -71,18 +84,31 @@ instance Outputable FamInst where pprFamInst :: FamInst -> SDoc pprFamInst famInst = hang (pprFamInstHdr famInst) - 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc famInst))) + 2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> pp_ax) + , ptext (sLit "--") <+> pprNameLoc (getName famInst)]) + where + pp_ax = case tyConFamilyCoercion_maybe (fi_tycon famInst) of + Just ax -> ppr ax + Nothing -> ptext (sLit "") pprFamInstHdr :: FamInst -> SDoc -pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon}) - = pprTyConSort <+> pprHead +pprFamInstHdr (FamInst {fi_tycon = rep_tc}) + = pprTyConSort <+> pp_instance <+> pprHead where - pprHead = parenSymOcc (getOccName fam) (ppr fam) <+> - sep (map pprParendType tys) - pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance") - | isNewTyCon tycon = ptext SLIT("newtype instance") - | isSynTyCon tycon = ptext SLIT("type instance") - | otherwise = panic "FamInstEnv.pprFamInstHdr" + Just (fam_tc, tys) = tyConFamInst_maybe rep_tc + + -- For *associated* types, say "type T Int = blah" + -- For *top level* type instances, say "type instance T Int = blah" + pp_instance + | isTyConAssoc fam_tc = empty + | otherwise = ptext (sLit "instance") + + pprHead = pprTypeApp fam_tc tys + pprTyConSort | isDataTyCon rep_tc = ptext (sLit "data") + | isNewTyCon rep_tc = ptext (sLit "newtype") + | isSynTyCon rep_tc = ptext (sLit "type") + | isAbstractTyCon rep_tc = ptext (sLit "data") + | otherwise = panic "FamInstEnv.pprFamInstHdr" pprFamInsts :: [FamInst] -> SDoc pprFamInsts finsts = vcat (map pprFamInst finsts) @@ -133,10 +159,31 @@ mkImportedFamInst fam mb_tcs tycon %* * %************************************************************************ -InstEnv maps a family name to the list of known instances for that family. +Note [FamInstEnv] +~~~~~~~~~~~~~~~~~~~~~ +A FamInstEnv maps a family name to the list of known instances for that family. + +The same FamInstEnv includes both 'data family' and 'type family' instances. +Type families are reduced during type inference, but not data families; +the user explains when to use a data family instance by using contructors +and pattern matching. + +Neverthless it is still useful to have data families in the FamInstEnv: + + - For finding overlaps and conflicts + + - For finding the representation type...see FamInstEnv.topNormaliseType + and its call site in Simplify + + - In standalone deriving instance Eq (T [Int]) we need to find the + representation type for T [Int] \begin{code} type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances + -- See Note [FamInstEnv] + +type FamInstEnvs = (FamInstEnv, FamInstEnv) + -- External package inst-env, Home-package inst-env data FamilyInstEnv = FamIE [FamInst] -- The instances for a particular family, in any order @@ -144,10 +191,16 @@ data FamilyInstEnv -- If *not* then the common case of looking up -- (T a b c) can fail immediately +instance Outputable FamilyInstEnv where + ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs) + -- INVARIANTS: -- * The fs_tvs are distinct in each FamInst -- of a range value of the map (so we can safely unify them) +emptyFamInstEnvs :: (FamInstEnv, FamInstEnv) +emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv) + emptyFamInstEnv :: FamInstEnv emptyFamInstEnv = emptyUFM @@ -172,11 +225,11 @@ extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs}) add (FamIE items tyvar) _ = FamIE (ins_item:items) (ins_tyvar || tyvar) ins_tyvar = not (any isJust mb_tcs) -\end{code} +\end{code} %************************************************************************ %* * -\subsection{Looking up a family instance} + Looking up a family instance %* * %************************************************************************ @@ -185,19 +238,136 @@ Multiple matches are only possible in case of type families (not data families), and then, it doesn't matter which match we choose (as the instances are guaranteed confluent). +We return the matching family instances and the type instance at which it +matches. For example, if we lookup 'T [Int]' and have a family instance + + data instance T [a] = .. + +desugared to + + data :R42T a = .. + coe :Co:R42T a :: T [a] ~ :R42T a + +we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'. + \begin{code} -lookupFamInstEnv :: (FamInstEnv -- External package inst-env - ,FamInstEnv) -- Home-package inst-env - -> TyCon -> [Type] -- What we are looking for - -> [(TvSubst, FamInst)] -- Successful matches -lookupFamInstEnv (pkg_ie, home_ie) fam tys - = home_matches ++ pkg_matches +type FamInstMatch = (FamInst, [Type]) -- Matching type instance + -- See Note [Over-saturated matches] + +lookupFamInstEnv + :: FamInstEnvs + -> TyCon -> [Type] -- What we are looking for + -> [FamInstMatch] -- Successful matches +-- Precondition: the tycon is saturated (or over-saturated) + +lookupFamInstEnv + = lookup_fam_inst_env match True + where + match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys + +lookupFamInstEnvConflicts + :: FamInstEnvs + -> FamInst -- Putative new instance + -> [TyVar] -- Unique tyvars, matching arity of FamInst + -> [FamInstMatch] -- Conflicting matches +-- E.g. when we are about to add +-- f : type instance F [a] = a->a +-- we do (lookupFamInstConflicts f [b]) +-- to find conflicting matches +-- The skolem tyvars are needed because we don't have a +-- unique supply to hand +-- +-- Precondition: the tycon is saturated (or over-saturated) + +lookupFamInstEnvConflicts envs fam_inst skol_tvs + = lookup_fam_inst_env my_unify False envs fam tys' + where + inst_tycon = famInstTyCon fam_inst + (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts" + (tyConFamInst_maybe inst_tycon) + skol_tys = mkTyVarTys skol_tvs + tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys + -- In example above, fam tys' = F [b] + + my_unify old_fam_inst tpl_tvs tpl_tys match_tys + = ASSERT2( tyVarsOfTypes 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 + case tcUnifyTys instanceBindFun tpl_tys match_tys of + Just subst | conflicting old_fam_inst subst -> Just subst + _other -> Nothing + + -- - In the case of data family instances, any overlap is fundamentally a + -- conflict (as these instances imply injective type mappings). + -- - In the case of type family instances, overlap is admitted as long as + -- the right-hand sides of the overlapping rules coincide under the + -- overlap substitution. We require that they are syntactically equal; + -- anything else would be difficult to test for at this stage. + conflicting old_fam_inst subst + | isAlgTyCon fam = True + | otherwise = not (old_rhs `eqType` new_rhs) + where + old_tycon = famInstTyCon old_fam_inst + old_tvs = tyConTyVars old_tycon + old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs) + new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs) +\end{code} + +While @lookupFamInstEnv@ uses a one-way match, the next function +@lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is +needed to check for overlapping instances. + +For class instances, these two variants of lookup are combined into one +function (cf, @InstEnv@). We don't do that for family instances as the +results of matching and unification are used in two different contexts. +Moreover, matching is the wildly more frequently used operation in the case of +indexed synonyms and we don't want to slow that down by needless unification. + +\begin{code} +------------------------------------------------------------ +-- 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 TvSubst + +type OneSidedMatch = Bool -- Are optimisations that are only valid for + -- one sided matches allowed? + +lookup_fam_inst_env -- The worker, local to this module + :: MatchFun + -> OneSidedMatch + -> FamInstEnvs + -> TyCon -> [Type] -- What we are looking for + -> [FamInstMatch] -- Successful matches + +-- Precondition: the tycon is saturated (or over-saturated) + +lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys + | not (isFamilyTyCon fam) + = [] + | otherwise + = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated + home_matches ++ pkg_matches where - rough_tcs = roughMatchTcs tys - all_tvs = all isNothing rough_tcs home_matches = lookup home_ie pkg_matches = lookup pkg_ie + -- See Note [Over-saturated matches] + arity = tyConArity fam + n_tys = length tys + extra_tys = drop arity tys + (match_tys, add_extra_tys) + | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys) + | otherwise = (tys, \res_tys -> res_tys) + -- The second case is the common one, hence functional representation + + -------------- + rough_tcs = roughMatchTcs match_tys + all_tvs = all isNothing rough_tcs && one_sided + -------------- lookup env = case lookupUFM env fam of Nothing -> [] -- No instances for this class @@ -210,6 +380,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys | otherwise -> find insts -------------- + find [] = [] find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_tys = tpl_tys, fi_tycon = tycon }) : rest) -- Fast check for no match, uses the "rough match" fields @@ -217,10 +388,151 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys = find rest -- Proper check - | Just subst <- tcMatchTys tpl_tvs tpl_tys tys - = (subst, item) : find rest + | Just subst <- match_fun item tpl_tvs tpl_tys match_tys + = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest -- No match => try next | otherwise = find rest \end{code} + +Note [Over-saturated matches] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It's ok to look up an over-saturated type constructor. E.g. + type family F a :: * -> * + type instance F (a,b) = Either (a->b) + +The type instance gives rise to a newtype TyCon (at a higher kind +which you can't do in Haskell!): + newtype FPair a b = FP (Either (a->b)) + +Then looking up (F (Int,Bool) Char) will return a FamInstMatch + (FPair, [Int,Bool,Char]) + +The "extra" type argument [Char] just stays on the end. + + + + +%************************************************************************ +%* * + Looking up a family instance +%* * +%************************************************************************ + +\begin{code} +topNormaliseType :: FamInstEnvs + -> Type + -> Maybe (Coercion, Type) + +-- Get rid of *outermost* (or toplevel) +-- * type functions +-- * newtypes +-- using appropriate coercions. +-- By "outer" we mean that toplevelNormaliseType guarantees to return +-- a type that does not have a reducible redex (F ty1 .. tyn) as its +-- outermost form. It *can* return something like (Maybe (F ty)), where +-- (F ty) is a redex. + +-- Its a bit like Type.repType, but handles type families too + +topNormaliseType env ty + = go [] ty + where + go :: [TyCon] -> Type -> Maybe (Coercion, Type) + go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms + = go rec_nts ty' + + go rec_nts (TyConApp tc tys) + | isNewTyCon tc -- Expand newtypes + = if tc `elem` rec_nts -- See Note [Expanding newtypes] in Type.lhs + then Nothing + else let nt_co = mkAxInstCo (newTyConCo tc) tys + in add_co nt_co rec_nts' nt_rhs + + | isFamilyTyCon tc -- Expand open tycons + , (co, ty) <- normaliseTcApp env tc tys + -- Note that normaliseType fully normalises, + -- but it has do to so to be sure that + , not (isReflCo co) + = add_co co rec_nts ty + where + nt_rhs = newTyConInstRhs tc tys + rec_nts' | isRecursiveTyCon tc = tc:rec_nts + | otherwise = rec_nts + + go _ _ = Nothing + + add_co co rec_nts ty + = case go rec_nts ty of + Nothing -> Just (co, ty) + Just (co', ty') -> Just (mkTransCo co co', ty') + + +--------------- +normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type) +normaliseTcApp env tc tys + | isFamilyTyCon tc + , tyConArity tc <= length tys -- Unsaturated data families are possible + , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys + = let -- A matching family instance exists + rep_tc = famInstTyCon fam_inst + co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc) + co = mkAxInstCo co_tycon inst_tys + first_coi = mkTransCo tycon_coi co + (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc inst_tys) + fix_coi = mkTransCo first_coi rest_coi + in + (fix_coi, nty) + + | otherwise -- No unique matching family instance exists; + -- we do not do anything + = (tycon_coi, TyConApp tc ntys) + + where + -- Normalise the arg types so that they'll match + -- when we lookup in in the instance envt + (cois, ntys) = mapAndUnzip (normaliseType env) tys + tycon_coi = mkTyConAppCo tc cois + +--------------- +normaliseType :: FamInstEnvs -- environment with family instances + -> Type -- old type + -> (Coercion, Type) -- (coercion,new type), where + -- co :: old-type ~ new_type +-- Normalise the input type, by eliminating *all* type-function redexes +-- Returns with Refl if nothing happens + +normaliseType env ty + | Just ty' <- coreView ty = normaliseType env ty' +normaliseType env (TyConApp tc tys) + = normaliseTcApp env tc tys +normaliseType env (AppTy ty1 ty2) + = let (coi1,nty1) = normaliseType env ty1 + (coi2,nty2) = normaliseType env ty2 + in (mkAppCo coi1 coi2, mkAppTy nty1 nty2) +normaliseType env (FunTy ty1 ty2) + = let (coi1,nty1) = normaliseType env ty1 + (coi2,nty2) = normaliseType env ty2 + in (mkFunCo coi1 coi2, mkFunTy nty1 nty2) +normaliseType env (ForAllTy tyvar ty1) + = let (coi,nty1) = normaliseType env ty1 + in (mkForAllCo tyvar coi, ForAllTy tyvar nty1) +normaliseType _ ty@(TyVarTy _) + = (Refl ty,ty) +normaliseType env (PredTy predty) + = normalisePred env predty + +--------------- +normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type) +normalisePred env (ClassP cls tys) + = let (cos,tys') = mapAndUnzip (normaliseType env) tys + in (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys') +normalisePred env (IParam ipn ty) + = let (co,ty') = normaliseType env ty + in (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty') +normalisePred env (EqPred ty1 ty2) + = let (co1,ty1') = normaliseType env ty1 + (co2,ty2') = normaliseType env ty2 + in (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2') +\end{code}