X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FType.lhs;h=c1e05447ec14b5436c22ca2f73178c7b5b41cd39;hp=fdcec308414322a62dc16a6dd12f52ae2c783d76;hb=deda0c55629600e886f47a5e90bad67953df1ad8;hpb=3287fb1d88a8322a767e45eaea431dacc05862dc diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index fdcec30..c1e0544 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -1,23 +1,50 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1998 % -\section[Type]{Type - public interface} + +Type - public interface \begin{code} +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + module Type ( -- re-exports from TypeRep TyThing(..), Type, PredType(..), ThetaType, funTyCon, - -- Re-exports from Kind - module Kind, + -- Kinds + Kind, SimpleKind, KindVar, + kindFunResult, splitKindFunTys, splitKindFunTysN, + + liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon, + argTypeKindTyCon, ubxTupleKindTyCon, + + liftedTypeKind, unliftedTypeKind, openTypeKind, + argTypeKind, ubxTupleKind, + + tySuperKind, coSuperKind, + + isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, + isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, + isCoSuperKind, isSuperKind, isCoercionKind, isEqPred, + mkArrowKind, mkArrowKinds, + + isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind, + isSubKindCon, -- Re-exports from TyCon PrimRep(..), mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy, - mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe, + mkAppTy, mkAppTys, splitAppTy, splitAppTys, + splitAppTy_maybe, repSplitAppTy_maybe, mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, splitFunTys, splitFunTysN, @@ -25,18 +52,19 @@ module Type ( mkTyConApp, mkTyConTy, tyConAppTyCon, tyConAppArgs, - splitTyConApp_maybe, splitTyConApp, + splitTyConApp_maybe, splitTyConApp, + splitNewTyConApp_maybe, splitNewTyConApp, - repType, typePrimRep, coreView, tcView, + repType, repType', typePrimRep, coreView, tcView, kindView, mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, applyTy, applyTys, isForAllTy, dropForAlls, -- Source types - predTypeRep, mkPredTy, mkPredTys, + predTypeRep, mkPredTy, mkPredTys, pprSourceTyCon, mkFamilyTyConApp, -- Newtypes - splitRecNewType_maybe, + newTyConInstRhs, -- Lifting and boxity isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType, @@ -46,6 +74,9 @@ module Type ( tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta, typeKind, addFreeTyVars, + -- Type families + tyFamInsts, + -- Tidying up for printing tidyType, tidyTypes, tidyOpenType, tidyOpenTypes, @@ -56,7 +87,7 @@ module Type ( -- Comparison coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, - tcEqPred, tcCmpPred, tcEqTypeX, + tcEqPred, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred, -- Seq seqType, seqTypes, @@ -67,14 +98,15 @@ module Type ( mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst, getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv, + isEmptyTvSubst, -- Performing substitution on types substTy, substTys, substTyWith, substTheta, - substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar, + substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar, -- Pretty-printing - pprType, pprParendType, pprTyThingCategory, - pprPred, pprTheta, pprThetaArrow, pprClassPred + pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll, + pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind ) where #include "HsVersions.h" @@ -85,29 +117,23 @@ module Type ( import TypeRep -- friends: -import Kind -import Var ( Var, TyVar, tyVarKind, tyVarName, setTyVarName, mkTyVar ) +import Var import VarEnv import VarSet -import OccName ( tidyOccName ) -import Name ( NamedThing(..), mkInternalName, tidyNameOcc ) -import Class ( Class, classTyCon ) -import TyCon ( TyCon, isRecursiveTyCon, isPrimTyCon, - isUnboxedTupleTyCon, isUnLiftedTyCon, - isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs, - isAlgTyCon, tyConArity, - tcExpandTyCon_maybe, coreExpandTyCon_maybe, - tyConKind, PrimRep(..), tyConPrimRep, - ) +import Name +import Class +import PrelNames +import TyCon -- others -import StaticFlags ( opt_DictsStrict ) -import SrcLoc ( noSrcLoc ) -import Util ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 ) +import StaticFlags +import Util import Outputable -import UniqSet ( sizeUniqSet ) -- Should come via VarSet -import Maybe ( isJust ) +import UniqSet + +import Data.List +import Data.Maybe ( isJust ) \end{code} @@ -122,7 +148,7 @@ In Core, we "look through" non-recursive newtypes and PredTypes. \begin{code} {-# INLINE coreView #-} coreView :: Type -> Maybe Type --- Srips off the *top layer only* of a type to give +-- Strips off the *top layer only* of a type to give -- its underlying representation type. -- Returns Nothing if there is nothing to look through. -- @@ -142,7 +168,9 @@ coreView :: Type -> Maybe Type -- By being non-recursive and inlined, this case analysis gets efficiently -- joined onto the case analysis that the caller is already doing coreView (NoteTy _ ty) = Just ty -coreView (PredTy p) = Just (predTypeRep p) +coreView (PredTy p) + | isEqPred p = Nothing + | otherwise = Just (predTypeRep p) coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys') -- Its important to use mkAppTys, rather than (foldl AppTy), @@ -150,6 +178,8 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc -- partially-applied type constructor; indeed, usually will! coreView ty = Nothing + + ----------------------------------------------- {-# INLINE tcView #-} tcView :: Type -> Maybe Type @@ -158,6 +188,14 @@ tcView (NoteTy _ ty) = Just ty tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys') tcView ty = Nothing + +----------------------------------------------- +{-# INLINE kindView #-} +kindView :: Kind -> Maybe Kind +-- C.f. coreView, tcView +-- For the moment, we don't even handle synonyms in kinds +kindView (NoteTy _ k) = Just k +kindView other = Nothing \end{code} @@ -190,6 +228,7 @@ getTyVar_maybe :: Type -> Maybe TyVar getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty' getTyVar_maybe (TyVarTy tv) = Just tv getTyVar_maybe other = Nothing + \end{code} @@ -231,20 +270,28 @@ mkAppTys orig_ty1 orig_tys2 -- mkTyConApp: see notes with mkAppTy mk_app ty1 = foldl AppTy orig_ty1 orig_tys2 +------------- splitAppTy_maybe :: Type -> Maybe (Type, Type) -splitAppTy_maybe ty | Just ty' <- coreView ty = splitAppTy_maybe ty' -splitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) -splitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) -splitAppTy_maybe (TyConApp tc tys) = case snocView tys of - Nothing -> Nothing - Just (tys',ty') -> Just (TyConApp tc tys', ty') -splitAppTy_maybe other = Nothing +splitAppTy_maybe ty | Just ty' <- coreView ty + = splitAppTy_maybe ty' +splitAppTy_maybe ty = repSplitAppTy_maybe ty +------------- +repSplitAppTy_maybe :: Type -> Maybe (Type,Type) +-- Does the AppTy split, but assumes that any view stuff is already done +repSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) +repSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) +repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of + Just (tys', ty') -> Just (TyConApp tc tys', ty') + Nothing -> Nothing +repSplitAppTy_maybe other = Nothing +------------- splitAppTy :: Type -> (Type, Type) splitAppTy ty = case splitAppTy_maybe ty of Just pr -> pr Nothing -> panic "splitAppTy" +------------- splitAppTys :: Type -> (Type, [Type]) splitAppTys ty = split ty ty [] where @@ -254,6 +301,7 @@ splitAppTys ty = split ty ty [] split orig_ty (FunTy ty1 ty2) args = ASSERT( null args ) (TyConApp funTyCon [], [ty1,ty2]) split orig_ty ty args = (orig_ty, args) + \end{code} @@ -263,10 +311,11 @@ splitAppTys ty = split ty ty [] \begin{code} mkFunTy :: Type -> Type -> Type +mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res mkFunTy arg res = FunTy arg res mkFunTys :: [Type] -> Type -> Type -mkFunTys tys ty = foldr FunTy ty tys +mkFunTys tys ty = foldr mkFunTy ty tys isFunTy :: Type -> Bool isFunTy ty = isJust (splitFunTy_maybe ty) @@ -354,6 +403,29 @@ splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty' splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res]) splitTyConApp_maybe other = Nothing + +-- Sometimes we do NOT want to look throught a newtype. When case matching +-- on a newtype we want a convenient way to access the arguments of a newty +-- constructor so as to properly form a coercion. +splitNewTyConApp :: Type -> (TyCon, [Type]) +splitNewTyConApp ty = case splitNewTyConApp_maybe ty of + Just stuff -> stuff + Nothing -> pprPanic "splitNewTyConApp" (ppr ty) +splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type]) +splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty' +splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) +splitNewTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res]) +splitNewTyConApp_maybe other = Nothing + +newTyConInstRhs :: TyCon -> [Type] -> Type +-- Unwrap one 'layer' of newtype +-- Use the eta'd version if possible +newTyConInstRhs tycon tys + = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs ) + mkAppTys (substTyWith tvs tys1 ty) tys2 + where + (tvs, ty) = newTyConEtadRhs tycon + (tys1, tys2) = splitAtList tvs tys \end{code} @@ -383,7 +455,7 @@ repType looks through (b) synonyms (c) predicates (d) usage annotations - (e) all newtypes, including recursive ones + (e) all newtypes, including recursive ones, but not newtype families It's useful in the back end. \begin{code} @@ -392,20 +464,26 @@ repType :: Type -> Type repType ty | Just ty' <- coreView ty = repType ty' repType (ForAllTy _ ty) = repType ty repType (TyConApp tc tys) - | isNewTyCon tc = -- Recursive newtypes are opaque to coreView - -- but we must expand them here. Sure to - -- be saturated because repType is only applied - -- to types of kind * - ASSERT( isRecursiveTyCon tc && - tys `lengthIs` tyConArity tc ) - repType (new_type_rep tc tys) + | isNewTyCon tc + , (tvs, rep_ty) <- newTyConRep tc + = -- Recursive newtypes are opaque to coreView + -- but we must expand them here. Sure to + -- be saturated because repType is only applied + -- to types of kind * + ASSERT( tys `lengthIs` tyConArity tc ) + repType (substTyWith tvs tys rep_ty) + repType ty = ty --- new_type_rep doesn't ask any questions: --- it just expands newtype, whether recursive or not -new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon ) - case newTyConRep new_tycon of - (tvs, rep_ty) -> substTyWith tvs tys rep_ty +-- repType' aims to be a more thorough version of repType +-- For now it simply looks through the TyConApp args too +repType' ty -- | pprTrace "repType'" (ppr ty $$ ppr (go1 ty)) False = undefined + | otherwise = go1 ty + where + go1 = go . repType + go (TyConApp tc tys) = mkTyConApp tc (map repType' tys) + go ty = ty + -- ToDo: this could be moved to the code generator, using splitTyConApp instead -- of inspecting the type directly. @@ -421,7 +499,6 @@ typePrimRep ty = case repType ty of -- The reason is that f must have kind *->*, not *->*#, because -- (we claim) there is no way to constrain f's kind any other -- way. - \end{code} @@ -535,31 +612,31 @@ predTypeRep (IParam _ ty) = ty predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys -- Result might be a newtype application, but the consumer will -- look through that too if necessary -\end{code} - - -%************************************************************************ -%* * - NewTypes -%* * -%************************************************************************ - -\begin{code} -splitRecNewType_maybe :: Type -> Maybe Type --- Sometimes we want to look through a recursive newtype, and that's what happens here --- It only strips *one layer* off, so the caller will usually call itself recursively --- Only applied to types of kind *, hence the newtype is always saturated -splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty' -splitRecNewType_maybe (TyConApp tc tys) - | isNewTyCon tc - = ASSERT( tys `lengthIs` tyConArity tc ) -- splitRecNewType_maybe only be applied - -- to *types* (of kind *) - ASSERT( isRecursiveTyCon tc ) -- Guaranteed by coreView - case newTyConRhs tc of - (tvs, rep_ty) -> ASSERT( length tvs == length tys ) - Just (substTyWith tvs tys rep_ty) - -splitRecNewType_maybe other = Nothing +predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2)) + +mkFamilyTyConApp :: TyCon -> [Type] -> Type +-- Given a family instance TyCon and its arg types, return the +-- corresponding family type. E.g. +-- data family T a +-- data instance T (Maybe b) = MkT b -- Instance tycon :RTL +-- Then +-- mkFamilyTyConApp :RTL Int = T (Maybe Int) +mkFamilyTyConApp tc tys + | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc + , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys + = mkTyConApp fam_tc (substTys fam_subst fam_tys) + | otherwise + = mkTyConApp tc tys + +-- Pretty prints a tycon, using the family instance in case of a +-- representation tycon. For example +-- e.g. data T [a] = ... +-- In that case we want to print `T [a]', where T is the family TyCon +pprSourceTyCon tycon + | Just (fam_tc, tys) <- tyConFamInst_maybe tycon + = ppr $ fam_tc `TyConApp` tys -- can't be FunTyCon + | otherwise + = ppr tycon \end{code} @@ -574,15 +651,30 @@ splitRecNewType_maybe other = Nothing ~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} typeKind :: Type -> Kind - -typeKind (TyVarTy tyvar) = tyVarKind tyvar -typeKind (TyConApp tycon tys) = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys -typeKind (NoteTy _ ty) = typeKind ty -typeKind (PredTy _) = liftedTypeKind -- Predicates are always - -- represented by lifted types -typeKind (AppTy fun arg) = kindFunResult (typeKind fun) -typeKind (FunTy arg res) = liftedTypeKind -typeKind (ForAllTy tv ty) = typeKind ty +typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) ) + -- We should be looking for the coercion kind, + -- not the type kind + foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys +typeKind (NoteTy _ ty) = typeKind ty +typeKind (PredTy pred) = predKind pred +typeKind (AppTy fun arg) = kindFunResult (typeKind fun) +typeKind (ForAllTy tv ty) = typeKind ty +typeKind (TyVarTy tyvar) = tyVarKind tyvar +typeKind (FunTy arg res) + -- Hack alert. The kind of (Int -> Int#) is liftedTypeKind (*), + -- not unliftedTypKind (#) + -- The only things that can be after a function arrow are + -- (a) types (of kind openTypeKind or its sub-kinds) + -- (b) kinds (of super-kind TY) (e.g. * -> (* -> *)) + | isTySuperKind k = k + | otherwise = ASSERT( isSubOpenTypeKind k) liftedTypeKind + where + k = typeKind res + +predKind :: PredType -> Kind +predKind (EqPred {}) = coSuperKind -- A coercion kind! +predKind (ClassP {}) = liftedTypeKind -- Class and implicitPredicates are +predKind (IParam {}) = liftedTypeKind -- always represented by lifted types \end{code} @@ -604,8 +696,9 @@ tyVarsOfTypes :: [Type] -> TyVarSet tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys tyVarsOfPred :: PredType -> TyVarSet -tyVarsOfPred (IParam _ ty) = tyVarsOfType ty -tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys +tyVarsOfPred (IParam _ ty) = tyVarsOfType ty +tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys +tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 tyVarsOfTheta :: ThetaType -> TyVarSet tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet @@ -619,6 +712,28 @@ addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty %************************************************************************ %* * +\subsection{Type families} +%* * +%************************************************************************ + +Type family instances occuring in a type after expanding synonyms. + +\begin{code} +tyFamInsts :: Type -> [(TyCon, [Type])] +tyFamInsts ty + | Just exp_ty <- tcView ty = tyFamInsts exp_ty +tyFamInsts (TyVarTy _) = [] +tyFamInsts (TyConApp tc tys) + | isOpenSynTyCon tc = [(tc, tys)] + | otherwise = concat (map tyFamInsts tys) +tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 +tyFamInsts (ForAllTy _ ty) = tyFamInsts ty +\end{code} + + +%************************************************************************ +%* * \subsection{TidyType} %* * %************************************************************************ @@ -630,13 +745,17 @@ It doesn't change the uniques at all, just the print names. \begin{code} tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar) -tidyTyVarBndr (tidy_env, subst) tyvar +tidyTyVarBndr env@(tidy_env, subst) tyvar = case tidyOccName tidy_env (getOccName name) of - (tidy', occ') -> ((tidy', subst'), tyvar') - where - subst' = extendVarEnv subst tyvar tyvar' - tyvar' = setTyVarName tyvar name' - name' = tidyNameOcc name occ' + (tidy', occ') -> ((tidy', subst'), tyvar'') + where + subst' = extendVarEnv subst tyvar tyvar'' + tyvar' = setTyVarName tyvar name' + name' = tidyNameOcc name occ' + -- Don't forget to tidy the kind for coercions! + tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind' + | otherwise = tyvar' + kind' = tidyType env (tyVarKind tyvar) where name = tyVarName tyvar @@ -679,6 +798,7 @@ tidyTypes env tys = map (tidyType env) tys tidyPred :: TidyEnv -> PredType -> PredType tidyPred env (IParam n ty) = IParam n (tidyType env ty) tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys) +tidyPred env (EqPred ty1 ty2) = EqPred (tidyType env ty1) (tidyType env ty2) \end{code} @@ -699,42 +819,11 @@ tidyTopType :: Type -> Type tidyTopType ty = tidyType emptyTidyEnv ty \end{code} - -%************************************************************************ -%* * - Tidying Kinds -%* * -%************************************************************************ - -We use a grevious hack for tidying KindVars. A TidyEnv contains -a (VarEnv Var) substitution, to express the renaming; but -KindVars are not Vars. The Right Thing ultimately is to make them -into Vars (and perhaps make Kinds into Types), but I just do a hack -here: I make up a TyVar just to remember the new OccName for the -renamed KindVar - \begin{code} + tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind) -tidyKind env@(tidy_env, subst) (KindVar kvar) - | Just tv <- lookupVarEnv_Directly subst uniq - = (env, KindVar (setKindVarOcc kvar (getOccName tv))) - | otherwise - = ((tidy', subst'), KindVar kvar') - where - uniq = kindVarUniq kvar - (tidy', occ') = tidyOccName tidy_env (kindVarOcc kvar) - kvar' = setKindVarOcc kvar occ' - fake_tv = mkTyVar tv_name (panic "tidyKind:fake tv kind") - tv_name = mkInternalName uniq occ' noSrcLoc - subst' = extendVarEnv subst fake_tv fake_tv - -tidyKind env (FunKind k1 k2) - = (env2, FunKind k1' k2') - where - (env1, k1') = tidyKind env k1 - (env2, k2') = tidyKind env1 k2 +tidyKind env k = tidyOpenType env k -tidyKind env k = (env, k) -- Atomic kinds \end{code} @@ -828,8 +917,9 @@ seqNote :: TyNote -> () seqNote (FTVNote set) = sizeUniqSet set `seq` () seqPred :: PredType -> () -seqPred (ClassP c tys) = c `seq` seqTypes tys -seqPred (IParam n ty) = n `seq` seqType ty +seqPred (ClassP c tys) = c `seq` seqTypes tys +seqPred (IParam n ty) = n `seq` seqType ty +seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2 \end{code} @@ -867,8 +957,8 @@ coreEqType t1 t2 -- attempt to expand one side or the other. -- Now deal with newtypes, synonyms, pred-tys - eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 - | Just t2' <- coreView t2 = eq env t1 t2' + eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 + | Just t2' <- coreView t2 = eq env t1 t2' -- Fall through case; not equal! eq env t1 t2 = False @@ -909,6 +999,27 @@ tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2 \end{code} +Checks whether the second argument is a subterm of the first. (We don't care +about binders, as we are only interested in syntactic subterms.) + +\begin{code} +tcPartOfType :: Type -> Type -> Bool +tcPartOfType t1 t2 = tcEqType t1 t2 +tcPartOfType t1 t2 + | Just t2' <- tcView t2 = tcPartOfType t1 t2' +tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2 +tcPartOfType t1 (AppTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2 +tcPartOfType t1 (FunTy s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2 +tcPartOfType t1 (PredTy p2) = tcPartOfPred t1 p2 +tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts +tcPartOfType t1 (NoteTy _ t2) = tcPartOfType t1 t2 + +tcPartOfPred :: Type -> PredType -> Bool +tcPartOfPred t1 (IParam _ t2) = tcPartOfType t1 t2 +tcPartOfPred t1 (ClassP _ ts) = any (tcPartOfType t1) ts +tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2 +\end{code} + Now here comes the real worker \begin{code} @@ -968,12 +1079,19 @@ cmpTypesX env ty [] = GT ------------- cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2 - -- Compare types as well as names for implicit parameters - -- This comparison is used exclusively (I think) for the - -- finite map built in TcSimplify -cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2 -cmpPredX env (IParam _ _) (ClassP _ _) = LT -cmpPredX env (ClassP _ _) (IParam _ _) = GT + -- Compare names only for implicit parameters + -- This comparison is used exclusively (I believe) + -- for the Avails finite map built in TcSimplify + -- If the types differ we keep them distinct so that we see + -- a distinct pair to run improvement on +cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2) +cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2') + +-- Constructor order: IParam < ClassP < EqPred +cmpPredX env (IParam {}) _ = LT +cmpPredX env (ClassP {}) (IParam {}) = GT +cmpPredX env (ClassP {}) (EqPred {}) = LT +cmpPredX env (EqPred {}) _ = GT \end{code} PredTypes are used as a FM key in TcSimplify, @@ -995,11 +1113,13 @@ instance Ord PredType where { compare = tcCmpPred } data TvSubst = TvSubst InScopeSet -- The in-scope type variables TvSubstEnv -- The substitution itself - -- See Note [Apply Once] + -- See Note [Apply Once] + -- and Note [Extending the TvSubstEnv] {- ---------------------------------------------------------- - Note [Apply Once] +Note [Apply Once] +~~~~~~~~~~~~~~~~~ We use TvSubsts to instantiate things, and we might instantiate forall a b. ty \with the types @@ -1016,6 +1136,38 @@ variations happen to; for example [a -> (a, b)]. A TvSubst is not idempotent, but, unlike the non-idempotent substitution we use during unifications, it must not be repeatedly applied. + +Note [Extending the TvSubst] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The following invariant should hold of a TvSubst + + The in-scope set is needed *only* to + guide the generation of fresh uniques + + In particular, the *kind* of the type variables in + the in-scope set is not relevant + +This invariant allows a short-cut when the TvSubstEnv is empty: +if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds --- +then (substTy subst ty) does nothing. + +For example, consider: + (/\a. /\b:(a~Int). ...b..) Int +We substitute Int for 'a'. The Unique of 'b' does not change, but +nevertheless we add 'b' to the TvSubstEnv, because b's type does change + +This invariant has several crucial consequences: + +* In substTyVarBndr, we need extend the TvSubstEnv + - if the unique has changed + - or if the kind has changed + +* In substTyVar, we do not need to consult the in-scope set; + the TvSubstEnv is enough + +* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty + + -------------------------------------------------------------- -} @@ -1044,6 +1196,7 @@ composeTvSubst in_scope env1 env2 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv isEmptyTvSubst :: TvSubst -> Bool + -- See Note [Extending the TvSubstEnv] isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst @@ -1100,7 +1253,7 @@ zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst zipTopTvSubst tyvars tys #ifdef DEBUG | length tyvars /= length tys - = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst + = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst | otherwise #endif = TvSubst emptyInScopeSet (zipTyEnv tyvars tys) @@ -1167,6 +1320,7 @@ substTheta subst theta substPred :: TvSubst -> PredType -> PredType substPred subst (IParam n ty) = IParam n (subst_ty subst ty) substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys) +substPred subst (EqPred ty1 ty2) = EqPred (subst_ty subst ty1) (subst_ty subst ty2) deShadowTy :: TyVarSet -> Type -> Type -- Remove any nested binders mentioning tvs deShadowTy tvs ty @@ -1174,6 +1328,9 @@ deShadowTy tvs ty where in_scope = mkInScopeSet tvs +subst_ty :: TvSubst -> Type -> Type +-- subst_ty is the main workhorse for type substitution +-- -- Note that the in_scope set is poked only if we hit a forall -- so it may often never be fully computed subst_ty subst ty @@ -1196,37 +1353,221 @@ subst_ty subst ty (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty) substTyVar :: TvSubst -> TyVar -> Type -substTyVar subst tv - = case lookupTyVar subst tv of - Nothing -> TyVarTy tv - Just ty' -> ty' -- See Note [Apply Once] +substTyVar subst@(TvSubst in_scope env) tv + = case lookupTyVar subst tv of { + Nothing -> TyVarTy tv; + Just ty -> ty -- See Note [Apply Once] + } + +substTyVars :: TvSubst -> [TyVar] -> [Type] +substTyVars subst tvs = map (substTyVar subst) tvs lookupTyVar :: TvSubst -> TyVar -> Maybe Type + -- See Note [Extending the TvSubst] lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar) substTyVarBndr subst@(TvSubst in_scope env) old_var - | old_var == new_var -- No need to clone - -- But we *must* zap any current substitution for the variable. - -- For example: - -- (\x.e) with id_subst = [x |-> e'] - -- Here we must simply zap the substitution for x - -- - -- The new_id isn't cloned, but it may have a different type - -- etc, so we must return it, not the old id - = (TvSubst (in_scope `extendInScopeSet` new_var) - (delVarEnv env old_var), - new_var) - - | otherwise -- The new binder is in scope so - -- we'd better rename it away from the in-scope variables - -- Extending the substitution to do this renaming also - -- has the (correct) effect of discarding any existing - -- substitution for that variable - = (TvSubst (in_scope `extendInScopeSet` new_var) - (extendVarEnv env old_var (TyVarTy new_var)), - new_var) + = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var) where - new_var = uniqAway in_scope old_var + is_co_var = isCoVar old_var + + new_env | no_change = delVarEnv env old_var + | otherwise = extendVarEnv env old_var (TyVarTy new_var) + + no_change = new_var == old_var && not is_co_var + -- no_change means that the new_var is identical in + -- all respects to the old_var (same unique, same kind) + -- See Note [Extending the TvSubst] + -- + -- In that case we don't need to extend the substitution + -- to map old to new. But instead we must zap any + -- current substitution for the variable. For example: + -- (\x.e) with id_subst = [x |-> e'] + -- Here we must simply zap the substitution for x + + new_var = uniqAway in_scope subst_old_var -- The uniqAway part makes sure the new variable is not already in scope + + subst_old_var -- subst_old_var is old_var with the substitution applied to its kind + -- It's only worth doing the substitution for coercions, + -- becuase only they can have free type variables + | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var)) + | otherwise = old_var +\end{code} + +---------------------------------------------------- +-- Kind Stuff + +Kinds +~~~~~ +There's a little subtyping at the kind level: + + ? + / \ + / \ + ?? (#) + / \ + * # + +where * [LiftedTypeKind] means boxed type + # [UnliftedTypeKind] means unboxed type + (#) [UbxTupleKind] means unboxed tuple + ?? [ArgTypeKind] is the lub of *,# + ? [OpenTypeKind] means any type at all + +In particular: + + error :: forall a:?. String -> a + (->) :: ?? -> ? -> * + (\(x::t) -> ...) Here t::?? (i.e. not unboxed tuple) + +\begin{code} +type KindVar = TyVar -- invariant: KindVar will always be a + -- TcTyVar with details MetaTv TauTv ... +-- kind var constructors and functions are in TcType + +type SimpleKind = Kind +\end{code} + +Kind inference +~~~~~~~~~~~~~~ +During kind inference, a kind variable unifies only with +a "simple kind", sk + sk ::= * | sk1 -> sk2 +For example + data T a = MkT a (T Int#) +fails. We give T the kind (k -> *), and the kind variable k won't unify +with # (the kind of Int#). + +Type inference +~~~~~~~~~~~~~~ +When creating a fresh internal type variable, we give it a kind to express +constraints on it. E.g. in (\x->e) we make up a fresh type variable for x, +with kind ??. + +During unification we only bind an internal type variable to a type +whose kind is lower in the sub-kind hierarchy than the kind of the tyvar. + +When unifying two internal type variables, we collect their kind constraints by +finding the GLB of the two. Since the partial order is a tree, they only +have a glb if one is a sub-kind of the other. In that case, we bind the +less-informative one to the more informative one. Neat, eh? + + +\begin{code} + +\end{code} + +%************************************************************************ +%* * + Functions over Kinds +%* * +%************************************************************************ + +\begin{code} +kindFunResult :: Kind -> Kind +kindFunResult k = funResultTy k + +splitKindFunTys :: Kind -> ([Kind],Kind) +splitKindFunTys k = splitFunTys k + +splitKindFunTysN :: Int -> Kind -> ([Kind],Kind) +splitKindFunTysN k = splitFunTysN k + +isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool + +isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey + +isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc +isOpenTypeKind other = False + +isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey + +isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc +isUbxTupleKind other = False + +isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey + +isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc +isArgTypeKind other = False + +isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey + +isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc +isUnliftedTypeKind other = False + +isSubOpenTypeKind :: Kind -> Bool +-- True of any sub-kind of OpenTypeKind (i.e. anything except arrow) +isSubOpenTypeKind (FunTy k1 k2) = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) + ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) + False +isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True +isSubOpenTypeKind other = ASSERT( isKind other ) False + -- This is a conservative answer + -- It matters in the call to isSubKind in + -- checkExpectedKind. + +isSubArgTypeKindCon kc + | isUnliftedTypeKindCon kc = True + | isLiftedTypeKindCon kc = True + | isArgTypeKindCon kc = True + | otherwise = False + +isSubArgTypeKind :: Kind -> Bool +-- True of any sub-kind of ArgTypeKind +isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc +isSubArgTypeKind other = False + +isSuperKind :: Type -> Bool +isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc +isSuperKind other = False + +isKind :: Kind -> Bool +isKind k = isSuperKind (typeKind k) + +isSubKind :: Kind -> Kind -> Bool +-- (k1 `isSubKind` k2) checks that k1 <: k2 +isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2 +isSubKind (FunTy a1 r1) (FunTy a2 r2) = (a2 `isSubKind` a1) && (r1 `isSubKind` r2) +isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) + = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2' +isSubKind k1 k2 = False + +eqKind :: Kind -> Kind -> Bool +eqKind = tcEqType + +isSubKindCon :: TyCon -> TyCon -> Bool +-- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2 +isSubKindCon kc1 kc2 + | isLiftedTypeKindCon kc1 && isLiftedTypeKindCon kc2 = True + | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True + | isUbxTupleKindCon kc1 && isUbxTupleKindCon kc2 = True + | isOpenTypeKindCon kc2 = True + -- we already know kc1 is not a fun, its a TyCon + | isArgTypeKindCon kc2 && isSubArgTypeKindCon kc1 = True + | otherwise = False + +defaultKind :: Kind -> Kind +-- Used when generalising: default kind '?' and '??' to '*' +-- +-- When we generalise, we make generic type variables whose kind is +-- simple (* or *->* etc). So generic type variables (other than +-- built-in constants like 'error') always have simple kinds. This is important; +-- consider +-- f x = True +-- We want f to get type +-- f :: forall (a::*). a -> Bool +-- Not +-- f :: forall (a::??). a -> Bool +-- because that would allow a call like (f 3#) as well as (f True), +--and the calling conventions differ. This defaulting is done in TcMType.zonkTcTyVarBndr. +defaultKind k + | isSubOpenTypeKind k = liftedTypeKind + | isSubArgTypeKind k = liftedTypeKind + | otherwise = k + +isEqPred :: PredType -> Bool +isEqPred (EqPred _ _) = True +isEqPred other = False \end{code}