X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FFamInstEnv.lhs;h=5b4374afa2e834cad5c9f283e805baf5d82a4462;hp=4cf33fc4d748ab65edfcf84674caa21b63f3538c;hb=0af06ed99ed56341adfdda4a92a0a36678780109;hpb=d2ce0f52d42edf32bb9f13796e6ba6edba8bd516 diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index 4cf33fc..5b4374a 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -29,7 +29,6 @@ import TypeRep import TyCon import Coercion import VarSet -import Var import Name import UniqFM import Outputable @@ -85,18 +84,31 @@ instance Outputable FamInst where pprFamInst :: FamInst -> SDoc pprFamInst famInst = hang (pprFamInstHdr famInst) - 2 (ptext (sLit "--") <+> pprNameLoc (getName 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 = pprTypeApp fam tys - pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance") - | isNewTyCon tycon = ptext (sLit "newtype instance") - | isSynTyCon tycon = ptext (sLit "type instance") - | isAbstractTyCon tycon = ptext (sLit "data 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) @@ -147,13 +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 + -- External package inst-env, Home-package inst-env data FamilyInstEnv = FamIE [FamInst] -- The instances for a particular family, in any order @@ -161,6 +191,9 @@ 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) @@ -225,6 +258,7 @@ 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 @@ -242,6 +276,8 @@ lookupFamInstEnvConflicts -- 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' @@ -271,7 +307,7 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs -- anything else would be difficult to test for at this stage. conflicting old_fam_inst subst | isAlgTyCon fam = True - | otherwise = not (old_rhs `tcEqType` new_rhs) + | otherwise = not (old_rhs `eqType` new_rhs) where old_tycon = famInstTyCon old_fam_inst old_tvs = tyConTyVars old_tycon @@ -306,11 +342,14 @@ lookup_fam_inst_env -- The worker, local to this module -> 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 - = ASSERT( n_tys >= arity ) -- Family type applications must be saturated + = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated home_matches ++ pkg_matches where home_matches = lookup home_ie @@ -404,62 +443,65 @@ topNormaliseType env ty go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms = go rec_nts ty' - go rec_nts (TyConApp tc tys) -- Expand newtypes - | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes] - = if tc `elem` rec_nts -- in Type.lhs + 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 = mkTyConApp co_con tys - in add_co nt_co rec_nts' nt_rhs - where - nt_rhs = newTyConInstRhs tc tys - rec_nts' | isRecursiveTyCon tc = tc:rec_nts - | otherwise = rec_nts - - go rec_nts (TyConApp tc tys) -- Expand open tycons - | isFamilyTyCon tc - , (ACo co, ty) <- normaliseTcApp env tc tys - = -- The ACo says "something happened" - -- Note that normaliseType fully normalises, but it has do to so - -- to be sure that - add_co co rec_nts ty + 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 (mkTransCoercion co co', ty') + Just (co', ty') -> Just (mkTransCo co co', ty') --------------- -normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type) +normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type) normaliseTcApp env tc tys - = let -- First 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 = mkTyConAppCoI tc cois - in -- Now try the top-level redex - case lookupFamInstEnv env tc ntys of - -- A matching family instance exists - [(fam_inst, tys)] -> (fix_coi, nty) - where - rep_tc = famInstTyCon fam_inst - co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc) - co = mkTyConApp co_tycon tys - first_coi = mkTransCoI tycon_coi (ACo co) - (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys) - fix_coi = mkTransCoI first_coi rest_coi - - -- No unique matching family instance exists; + | 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) + = (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 - -> (CoercionI, Type) -- (coercion,new type), where + -> (Coercion, Type) -- (coercion,new type), where -- co :: old-type ~ new_type -- Normalise the input type, by eliminating *all* type-function redexes --- Returns with IdCo if nothing happens +-- Returns with Refl if nothing happens normaliseType env ty | Just ty' <- coreView ty = normaliseType env ty' @@ -468,29 +510,29 @@ normaliseType env (TyConApp tc tys) normaliseType env (AppTy ty1 ty2) = let (coi1,nty1) = normaliseType env ty1 (coi2,nty2) = normaliseType env ty2 - in (mkAppTyCoI coi1 coi2, AppTy nty1 nty2) + in (mkAppCo coi1 coi2, mkAppTy nty1 nty2) normaliseType env (FunTy ty1 ty2) = let (coi1,nty1) = normaliseType env ty1 (coi2,nty2) = normaliseType env ty2 - in (mkFunTyCoI coi1 coi2, FunTy nty1 nty2) + in (mkFunCo coi1 coi2, mkFunTy nty1 nty2) normaliseType env (ForAllTy tyvar ty1) = let (coi,nty1) = normaliseType env ty1 - in (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1) + in (mkForAllCo tyvar coi, ForAllTy tyvar nty1) normaliseType _ ty@(TyVarTy _) - = (IdCo ty,ty) + = (Refl ty,ty) normaliseType env (PredTy predty) = normalisePred env predty --------------- -normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type) +normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type) normalisePred env (ClassP cls tys) - = let (cois,tys') = mapAndUnzip (normaliseType env) tys - in (mkClassPPredCoI cls cois, PredTy $ 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 (coi,ty') = normaliseType env ty - in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty') + = let (co,ty') = normaliseType env ty + in (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty') normalisePred env (EqPred ty1 ty2) - = let (coi1,ty1') = normaliseType env ty1 - (coi2,ty2') = normaliseType env ty2 - in (mkEqPredCoI coi1 coi2, PredTy $ 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}