X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FFamInstEnv.lhs;h=d1a344521d722fa3d2f22b1afdb99468093e1ac5;hb=87b3c589498941332029a8a9da35e94a6139f0eb;hp=9b49f5c34393fb9ac329bd4620894c90678cd6be;hpb=8a5d47de2b82d9cca86546a7bd89d915488934ef;p=ghc-hetmet.git diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index 9b49f5c..d1a3445 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -6,13 +6,18 @@ 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, + extendFamInstEnv, extendFamInstEnvList, famInstEnvElts, familyInstances, - lookupFamInstEnv, lookupFamInstEnvUnify + lookupFamInstEnv, lookupFamInstEnvUnify, + + -- Normalisation + toplevelNormaliseFamInst ) where #include "HsVersions.h" @@ -22,7 +27,9 @@ import Unify import TcGadt import TcType import Type +import TypeRep import TyCon +import Coercion import VarSet import Var import Name @@ -30,9 +37,10 @@ import OccName import SrcLoc import UniqFM import Outputable +import Maybes +import Util import Maybe -import Monad \end{code} @@ -45,13 +53,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 } @@ -60,6 +74,8 @@ data FamInst -- famInstTyCon :: FamInst -> TyCon famInstTyCon = fi_tycon + +famInstTyVars = fi_tvs \end{code} \begin{code} @@ -73,14 +89,13 @@ instance Outputable FamInst where pprFamInst :: FamInst -> SDoc pprFamInst famInst = hang (pprFamInstHdr famInst) - 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc famInst))) + 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcSpan famInst))) pprFamInstHdr :: FamInst -> SDoc pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon}) = pprTyConSort <+> pprHead where - pprHead = parenSymOcc (getOccName fam) (ppr fam) <+> - sep (map pprParendType tys) + pprHead = pprTypeApp (parenSymOcc (getOccName fam) (ppr fam)) tys pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance") | isNewTyCon tycon = ptext SLIT("newtype instance") | isSynTyCon tycon = ptext SLIT("type instance") @@ -140,6 +155,9 @@ InstEnv maps a family name to the list of known instances for that family. \begin{code} type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances +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 Bool -- True <=> there is an instance of form T a b c @@ -174,7 +192,7 @@ 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} %************************************************************************ %* * @@ -187,11 +205,24 @@ 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 +type FamInstMatch = (FamInst, [Type]) -- Matching type instance + +lookupFamInstEnv :: FamInstEnvs -> TyCon -> [Type] -- What we are looking for - -> [(TvSubst, FamInst)] -- Successful matches + -> [FamInstMatch] -- Successful matches lookupFamInstEnv (pkg_ie, home_ie) fam tys = home_matches ++ pkg_matches where @@ -221,7 +252,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys -- Proper check | Just subst <- tcMatchTys tpl_tvs tpl_tys tys - = (subst, item) : find rest + = (item, substTyVars subst (tyConTyVars tycon)) : find rest -- No match => try next | otherwise @@ -240,7 +271,7 @@ indexed synonyms and we don't want to slow that down by needless unification. \begin{code} lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type] - -> [(TvSubst, FamInst)] + -> [(FamInstMatch)] lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys = home_matches ++ pkg_matches where @@ -276,7 +307,9 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam 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 - Just subst -> (subst, item) : find rest + Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon) + in + (item, rep_tys) : find rest Nothing -> find rest -- See explanation at @InstEnv.bind_fn@. @@ -284,3 +317,99 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem | otherwise = BindMe \end{code} + +-------------------------------------- +-- Normalisation + +\begin{code} + -- get rid of TOPLEVEL type functions by rewriting them + -- i.e. treating their equations as a TRS +toplevelNormaliseFamInst :: FamInstEnvs -> + Type -> + (CoercionI,Type) +toplevelNormaliseFamInst env ty + | Just ty' <- tcView ty = normaliseFamInst env ty' +toplevelNormaliseFamInst env ty@(TyConApp tyCon tys) + | isOpenTyCon tyCon + = normaliseFamInst env ty +toplevelNormaliseFamInst env ty + = (IdCo,ty) + + + -- get rid of ALL type functions by rewriting them + -- i.e. treating their equations as a TRS +normaliseFamInst :: FamInstEnvs -> -- environment with family instances + Type -> -- old type + (CoercionI,Type) -- (coercion,new type) +normaliseFamInst env ty + | Just ty' <- tcView ty = normaliseFamInst env ty' +normaliseFamInst env ty@(TyConApp tyCon tys) = + let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys + tycon_coi = mkTyConAppCoI tyCon ntys cois + maybe_ty_co = lookupFamInst env tyCon ntys + in case maybe_ty_co of + -- a matching family instance exists + Just (ty',co) -> + let first_coi = mkTransCoI tycon_coi (ACo co) + (rest_coi,nty) = normaliseFamInst env ty' + fix_coi = mkTransCoI first_coi rest_coi + in (fix_coi,nty) + -- no matching family instance exists + -- we do not do anything + Nothing -> + (tycon_coi,TyConApp tyCon ntys) +normaliseFamInst env ty@(AppTy ty1 ty2) = + let (coi1,nty1) = normaliseFamInst env ty1 + (coi2,nty2) = normaliseFamInst env ty2 + in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2) +normaliseFamInst env ty@(FunTy ty1 ty2) = + let (coi1,nty1) = normaliseFamInst env ty1 + (coi2,nty2) = normaliseFamInst env ty2 + in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2) +normaliseFamInst env ty@(ForAllTy tyvar ty1) = + let (coi,nty1) = normaliseFamInst env ty1 + in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1) +normaliseFamInst env ty@(NoteTy note ty1) = + let (coi,nty1) = normaliseFamInst env ty1 + in (mkNoteTyCoI note coi,NoteTy note nty1) +normaliseFamInst env ty@(TyVarTy _) = + (IdCo,ty) +normaliseFamInst env (PredTy predty) = + normaliseFamInstPred env predty + +normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type) +normaliseFamInstPred env (ClassP cls tys) = + let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys + in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys') +normaliseFamInstPred env (IParam ipn ty) = + let (coi,ty') = normaliseFamInst env ty + in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty') +normaliseFamInstPred env (EqPred ty1 ty2) = + let (coi1,ty1') = normaliseFamInst env ty1 + (coi2,ty2') = normaliseFamInst env ty2 + in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2') + +lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion) + +-- (lookupFamInst F tys) looks for a top-level instance +-- co : forall a. F tys' = G a +-- (The rhs is always of form G a; see Note [The FamInst structure] +-- in FamInst.) +-- where we can instantiate 'a' with t to make tys'[t/a] = tys +-- Hence (co t) : F tys ~ G t +-- Then we return (Just (G t, co t)) + +lookupFamInst env tycon tys + | not (isOpenTyCon tycon) -- Dead code; fix. + = Nothing + | otherwise + = case lookupFamInstEnv env tycon tys of + [(subst, fam_inst)] -> + Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars) + where -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc) + -- is in the domain of the substitution + rep_tc = famInstTyCon fam_inst + coercion_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc) + substituted_vars = substTyVars subst (tyConTyVars rep_tc) + other -> Nothing +\end{code}