X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=48d58fe7584238b60c65c0d964214455665c07d0;hb=d133b73a4d4717892ced072d05e039a54ede0ceb;hp=1008e0cad8bb74316efe01dd30ae0448d76ce2f0;hpb=0596517a9b4b2b32e5d375a986351102ac4540fc;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 1008e0c..48d58fe 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -1,225 +1,264 @@ +% +% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +% +\section[TcType]{Types used in the typechecker} + \begin{code} module TcType ( + + TcTyVar, + TcTyVarSet, + newTyVar, + newTyVarTy, -- Kind -> NF_TcM s TcType + newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType] - TcTyVar(..), - newTcTyVar, - newTyVarTy, -- Kind -> NF_TcM s (TcType s) - newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s] - - - TcTyVarSet(..), + newTyVarTy_OpenKind, -- NF_TcM s TcType + newOpenTypeKind, -- NF_TcM s TcKind ----------------------------------------- - TcType(..), TcMaybe(..), - TcTauType(..), TcThetaType(..), TcRhoType(..), + TcType, TcTauType, TcThetaType, TcRhoType, -- Find the type to which a type variable is bound - tcWriteTyVar, -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s) - tcReadTyVar, -- :: TcTyVar s -> NF_TcM (TcMaybe s) + tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType + tcGetTyVar, -- :: TcTyVar -> NF_TcM (Maybe TcType) does shorting out + + + tcSplitRhoTy, + + tcInstTyVars, + tcInstSigVar, + tcInstTcType, + typeToTcType, - tcInstTyVar, -- TyVar -> NF_TcM s (TcTyVar s) - tcInstType, tcInstTcType, tcInstTheta, + tcTypeKind, -- :: TcType -> NF_TcM s TcKind + -------------------------------- + TcKind, + newKindVar, newKindVars, + kindToTcKind, + zonkTcKind, --- zonkTcType, -- TcType s -> NF_TcM s (TcType s) --- zonkTcTheta, -- TcThetaType s -> NF_TcM s (TcThetaType s) + -------------------------------- + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr, + zonkTcType, zonkTcTypes, zonkTcThetaType, - zonkTcTyVars, -- TcTyVarSet s -> NF_TcM s (TcTyVarSet s) - zonkTcType, -- TcType s -> NF_TcM s (TcType s) - zonkTcTypeToType, -- TcType s -> NF_TcM s Type - zonkTcTyVarToTyVar -- TcTyVar s -> NF_TcM s TyVar + zonkTcTypeToType, zonkTcTyVarToTyVar, + zonkTcKindToKind ) where +#include "HsVersions.h" -- friends: -import Type ( Type(..), ThetaType(..), GenType(..), tyVarsOfTypes, getTyVar_maybe ) -import TyVar ( TyVar(..), GenTyVar(..), TyVarSet(..), GenTyVarSet(..), - tyVarSetToList - ) +import PprType ( pprType ) +import Type ( Type(..), Kind, ThetaType, TyNote(..), + mkAppTy, mkTyConApp, + splitDictTy_maybe, splitForAllTys, isNotUsgTy, + isTyVarTy, mkTyVarTy, mkTyVarTys, + fullSubstTy, substTopTy, + typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity + ) +import TyCon ( tyConKind, mkPrimTyCon ) +import PrimRep ( PrimRep(VoidRep) ) +import VarEnv +import VarSet ( emptyVarSet ) +import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar ) -- others: -import Kind ( Kind ) -import Usage ( Usage(..), GenUsage, UVar(..), duffUsage ) -import Class ( GenClass ) -import TcKind ( TcKind ) import TcMonad - -import Ubiq -import Unique ( Unique ) -import UniqFM ( UniqFM ) -import Name ( getNameShortName ) -import Maybes ( assocMaybe ) -import Util ( panic ) +import TysWiredIn ( voidTy ) + +import Name ( NamedThing(..), setNameUnique, mkSysLocalName, + mkDerivedName, mkDerivedTyConOcc + ) +import Unique ( Unique, Uniquable(..) ) +import Util ( nOfThem ) +import Outputable \end{code} -Data types +Coercions ~~~~~~~~~~ +Type definitions are in TcMonad.lhs \begin{code} -type TcType s = GenType (TcTyVar s) UVar -- Used during typechecker - -- Invariant on ForAllTy in TcTypes: - -- forall a. T - -- a cannot occur inside a MutTyVar in T; that is, - -- T is "flattened" before quantifying over a - -type TcThetaType s = [(Class, TcType s)] -type TcRhoType s = TcType s -- No ForAllTys -type TcTauType s = TcType s -- No DictTys or ForAllTys - -type Box s = MutableVar s (TcMaybe s) +typeToTcType :: Type -> TcType +typeToTcType ty = ty -data TcMaybe s = UnBound - | BoundTo (TcType s) +kindToTcKind :: Kind -> TcKind +kindToTcKind kind = kind +\end{code} --- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s), --- because you get a synonym loop if you do! +Utility functions +~~~~~~~~~~~~~~~~~ +These tcSplit functions are like their non-Tc analogues, but they +follow through bound type variables. -type TcTyVar s = GenTyVar (Box s) -type TcTyVarSet s = GenTyVarSet (Box s) -\end{code} +No need for tcSplitForAllTy because a type variable can't be instantiated +to a for-all type. \begin{code} -tcTyVarToTyVar :: TcTyVar s -> TyVar -tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage +tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType) +tcSplitRhoTy t + = go t t [] + where + -- A type variable is never instantiated to a dictionary type, + -- so we don't need to do a tcReadVar on the "arg". + go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of + Just pair -> go res res (pair:ts) + Nothing -> returnNF_Tc (reverse ts, syn_t) + go syn_t (NoteTy _ t) ts = go syn_t t ts + go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + Just ty | not (isTyVarTy ty) -> go syn_t ty ts + other -> returnNF_Tc (reverse ts, syn_t) + go syn_t t ts = returnNF_Tc (reverse ts, syn_t) \end{code} -Type instantiation -~~~~~~~~~~~~~~~~~~ + +%************************************************************************ +%* * +\subsection{New type variables} +%* * +%************************************************************************ \begin{code} -newTcTyVar :: Maybe ShortName -> Kind -> NF_TcM s (TcTyVar s) -newTcTyVar name kind +newTyVar :: Kind -> NF_TcM s TcTyVar +newTyVar kind = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutVar UnBound `thenNF_Tc` \ box -> - returnNF_Tc (TyVar uniq kind name box) + tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind -newTyVarTy :: Kind -> NF_TcM s (TcType s) +newTyVarTy :: Kind -> NF_TcM s TcType newTyVarTy kind - = newTcTyVar Nothing kind `thenNF_Tc` \ tc_tyvar -> + = newTyVar kind `thenNF_Tc` \ tc_tyvar -> returnNF_Tc (TyVarTy tc_tyvar) -newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s] -newTyVarTys n kind = mapNF_Tc newTyVarTy (take n (repeat kind)) +newTyVarTys :: Int -> Kind -> NF_TcM s [TcType] +newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind) -tcInstTyVar :: TyVar -> NF_TcM s (TcTyVar s) -tcInstTyVar tyvar@(TyVar uniq kind name _) - = newTcTyVar name kind -\end{code} - -@tcInstType@ and @tcInstTcType@ both create a fresh instance of a -type, returning a @TcType@. All inner for-alls are instantiated with -fresh TcTyVars. +newKindVar :: NF_TcM s TcKind +newKindVar + = tcGetUnique `thenNF_Tc` \ uniq -> + tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv -> + returnNF_Tc (TyVarTy kv) -There are two versions, one for instantiating a @Type@, and one for a @TcType@. -The former must instantiate everything; all tyvars must be bound either -by a forall or by an environment passed in. The latter can do some sharing, -and is happy with free tyvars (which is vital when instantiating the type -of local functions). In the future @tcInstType@ may try to be clever about not -instantiating constant sub-parts. +newKindVars :: Int -> NF_TcM s [TcKind] +newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ()) -\begin{code} -tcInstType :: [(TyVar,TcType s)] -> Type -> NF_TcM s (TcType s) -tcInstType tenv ty_to_inst - = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst - where - do env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage) +-- Returns a type variable of kind (Type bv) where bv is a new boxity var +-- Used when you need a type variable that's definitely a , but you don't know +-- what kind of type (boxed or unboxed). +newTyVarTy_OpenKind :: NF_TcM s TcType +newTyVarTy_OpenKind = newOpenTypeKind `thenNF_Tc` \ kind -> + newTyVarTy kind - do env (SynTy tycon tys ty) = mapNF_Tc (do env) tys `thenNF_Tc` \ tys' -> - do env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (SynTy tycon tys' ty') +newOpenTypeKind :: NF_TcM s TcKind +newOpenTypeKind = newTyVarTy superBoxity `thenNF_Tc` \ bv -> + returnNF_Tc (mkTyConApp typeCon [bv]) +\end{code} - do env (FunTy arg res usage) = do env arg `thenNF_Tc` \ arg' -> - do env res `thenNF_Tc` \ res' -> - returnNF_Tc (FunTy arg' res' usage) - do env (AppTy fun arg) = do env fun `thenNF_Tc` \ fun' -> - do env arg `thenNF_Tc` \ arg' -> - returnNF_Tc (AppTy fun' arg') +%************************************************************************ +%* * +\subsection{Type instantiation} +%* * +%************************************************************************ - do env (DictTy clas ty usage)= do env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (DictTy clas ty' usage) +Instantiating a bunch of type variables - do env (TyVarTy (TyVar uniq kind name _)) - = case assocMaybe env uniq of - Just tc_ty -> returnNF_Tc tc_ty - Nothing -> panic "tcInstType" +\begin{code} +tcInstTyVars :: [TyVar] + -> NF_TcM s ([TcTyVar], [TcType], TyVarEnv TcType) + +tcInstTyVars tyvars + = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars -> + let + tys = mkTyVarTys tc_tyvars + in + returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys) + +tcInstTyVar tyvar + = tcGetUnique `thenNF_Tc` \ uniq -> + let + name = setNameUnique (tyVarName tyvar) uniq + -- Note that we don't change the print-name + -- This won't confuse the type checker but there's a chance + -- that two different tyvars will print the same way + -- in an error message. -dppr-debug will show up the difference + -- Better watch out for this. If worst comes to worst, just + -- use mkSysLocalName. + + kind = tyVarKind tyvar + in + + -- Hack alert! Certain system functions (like error) are quantified + -- over type variables with an 'open' kind (a :: ?). When we instantiate + -- these tyvars we want to make a type variable whose kind is (Type bv) + -- where bv is a boxity variable. This makes sure it's a type, but + -- is open about its boxity. We *don't* want to give the thing the + -- kind '?' (= Type AnyBox). + -- + -- This is all a hack to avoid giving error it's "proper" type: + -- error :: forall bv. forall a::Type bv. String -> a + + (if kind == openTypeKind then + newOpenTypeKind + else + returnNF_Tc kind) `thenNF_Tc` \ kind' -> + + tcNewMutTyVar name kind' + +tcInstSigVar tyvar -- Very similar to tcInstTyVar + = tcGetUnique `thenNF_Tc` \ uniq -> + let + name = setNameUnique (tyVarName tyvar) uniq + kind = tyVarKind tyvar + in + ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen + tcNewSigTyVar name kind +\end{code} - do env (ForAllTy (TyVar uniq kind name _) ty) - = newTcTyVar name kind `thenNF_Tc` \ tc_tyvar -> - let - new_env = (uniq, TyVarTy tc_tyvar) : env - in - do new_env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllTy tc_tyvar ty') +@tcInstTcType@ instantiates the outer-level for-alls of a TcType with +fresh type variables, returning them and the instantiated body of the for-all. - -- ForAllUsage impossible +\begin{code} +tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType) +tcInstTcType ty + = case splitForAllTys ty of + ([], _) -> returnNF_Tc ([], ty) -- Nothing to do + (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> + returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho) + -- Since the tyvars are freshly made, + -- they cannot possibly be captured by + -- any existing for-alls. Hence emptyVarSet +\end{code} -tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s) -tcInstTheta tenv theta - = mapNF_Tc go theta - where - go (clas,ty) = tcInstType tenv ty `thenNF_Tc` \ tc_ty -> - returnNF_Tc (clas, tc_ty) -tcInstTcType :: [(TcTyVar s,TcType s)] -> TcType s -> NF_TcM s (TcType s) -tcInstTcType tenv ty_to_inst - = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst - where - do env ty@(TyConTy tycon usage) = returnNF_Tc ty - --- Could do clever stuff here to avoid instantiating constant types - do env (SynTy tycon tys ty) = mapNF_Tc (do env) tys `thenNF_Tc` \ tys' -> - do env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (SynTy tycon tys' ty') - - do env (FunTy arg res usage) = do env arg `thenNF_Tc` \ arg' -> - do env res `thenNF_Tc` \ res' -> - returnNF_Tc (FunTy arg' res' usage) - - do env (AppTy fun arg) = do env fun `thenNF_Tc` \ fun' -> - do env arg `thenNF_Tc` \ arg' -> - returnNF_Tc (AppTy fun' arg') - - do env (DictTy clas ty usage)= do env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (DictTy clas ty' usage) - - do env ty@(TyVarTy (TyVar uniq kind name _)) - = case assocMaybe env uniq of - Just tc_ty -> returnNF_Tc tc_ty - Nothing -> returnNF_Tc ty - - do env (ForAllTy (TyVar uniq kind name _) ty) - = newTcTyVar name kind `thenNF_Tc` \ tc_tyvar -> - let - new_env = (uniq, TyVarTy tc_tyvar) : env - in - do new_env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllTy tc_tyvar ty') - - -- ForAllUsage impossible -\end{code} +%************************************************************************ +%* * +\subsection{Putting and getting mutable type variables} +%* * +%************************************************************************ -Reading and writing TcTyVars -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} -tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s () -tcReadTyVar :: TcTyVar s -> NF_TcM s (TcMaybe s) +tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType +tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType) \end{code} -Writing is easy: +Putting is easy: \begin{code} -tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty) +tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_` + returnNF_Tc ty \end{code} -Reading is more interesting. The easy thing to do is just to read, thus: +Getting is more interesting. The easy thing to do is just to read, thus: + \begin{verbatim} -tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box +tcGetTyVar tyvar = tcReadMutTyVar tyvar \end{verbatim} But it's more fun to short out indirections on the way: If this @@ -229,94 +268,251 @@ any other type, then there might be bound TyVars embedded inside it. We return Nothing iff the original box was unbound. \begin{code} -tcReadTyVar (TyVar uniq kind name box) - = tcReadMutVar box `thenNF_Tc` \ maybe_ty -> +tcGetTyVar tyvar + = ASSERT2( isMutTyVar tyvar, ppr tyvar ) + tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of - UnBound -> returnNF_Tc UnBound - BoundTo ty -> short_out ty `thenNF_Tc` \ ty' -> - tcWriteMutVar box (BoundTo ty') `thenNF_Tc_` - returnNF_Tc (BoundTo ty') - -short_out :: TcType s -> NF_TcM s (TcType s) -short_out ty@(TyVarTy (TyVar uniq kind name box)) - = tcReadMutVar box `thenNF_Tc` \ maybe_ty -> + Just ty -> short_out ty `thenNF_Tc` \ ty' -> + tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_` + returnNF_Tc (Just ty') + + Nothing -> returnNF_Tc Nothing + +short_out :: TcType -> NF_TcM s TcType +short_out ty@(TyVarTy tyvar) + | not (isMutTyVar tyvar) + = returnNF_Tc ty + + | otherwise + = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of - UnBound -> returnNF_Tc ty - BoundTo ty' -> short_out ty' `thenNF_Tc` \ ty' -> - tcWriteMutVar box (BoundTo ty') `thenNF_Tc_` - returnNF_Tc ty' + Just ty' -> short_out ty' `thenNF_Tc` \ ty' -> + tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_` + returnNF_Tc ty' + + other -> returnNF_Tc ty short_out other_ty = returnNF_Tc other_ty \end{code} -Zonking -~~~~~~~ -@zonkTcTypeToType@ converts from @TcType@ to @Type@. It follows through all -the substitutions of course. - -\begin{code} -zonkTcTypeToType :: TcType s -> NF_TcM s Type -zonkTcTypeToType ty = zonk tcTyVarToTyVar ty +%************************************************************************ +%* * +\subsection{Zonking -- the exernal interfaces} +%* * +%************************************************************************ -zonkTcType :: TcType s -> NF_TcM s (TcType s) -zonkTcType ty = zonk (\tyvar -> tyvar) ty +----------------- Type variables -zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s) -zonkTcTyVars tyvars - = mapNF_Tc (zonk_tv (\tyvar -> tyvar)) - (tyVarSetToList tyvars) `thenNF_Tc` \ tys -> - returnNF_Tc (tyVarsOfTypes tys) +\begin{code} +zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType] +zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars + +zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar +zonkTcTyVarBndr tyvar + = zonkTcTyVar tyvar `thenNF_Tc` \ (TyVarTy tyvar') -> + returnNF_Tc tyvar' + +zonkTcTyVar :: TcTyVar -> NF_TcM s TcType +zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar +\end{code} -zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar -zonkTcTyVarToTyVar tyvar - = zonk_tv_to_tv tcTyVarToTyVar tyvar +----------------- Types +\begin{code} +zonkTcType :: TcType -> NF_TcM s TcType +zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty -zonk tyvar_fn (TyVarTy tyvar) - = zonk_tv tyvar_fn tyvar +zonkTcTypes :: [TcType] -> NF_TcM s [TcType] +zonkTcTypes tys = mapNF_Tc zonkTcType tys -zonk tyvar_fn (AppTy ty1 ty2) - = zonk tyvar_fn ty1 `thenNF_Tc` \ ty1' -> - zonk tyvar_fn ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (AppTy ty1' ty2') +zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType +zonkTcThetaType theta = mapNF_Tc zonk theta + where + zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts -> + returnNF_Tc (c, new_ts) -zonk tyvar_fn (TyConTy tc u) - = returnNF_Tc (TyConTy tc u) +zonkTcKind :: TcKind -> NF_TcM s TcKind +zonkTcKind = zonkTcType +\end{code} -zonk tyvar_fn (SynTy tc tys ty) - = mapNF_Tc (zonk tyvar_fn) tys `thenNF_Tc` \ tys' -> - zonk tyvar_fn ty `thenNF_Tc` \ ty' -> - returnNF_Tc (SynTy tc tys' ty') +------------------- These ...ToType, ...ToKind versions + are used at the end of type checking -zonk tyvar_fn (ForAllTy tv ty) - = zonk_tv_to_tv tyvar_fn tv `thenNF_Tc` \ tv' -> - zonk tyvar_fn ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllTy tv' ty') +\begin{code} +zonkTcKindToKind :: TcKind -> NF_TcM s Kind +zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind + where + -- Zonk a mutable but unbound kind variable to + -- (Type Boxed) if it has kind superKind + -- Boxed if it has kind superBoxity + zonk_unbound_kind_var kv + | super_kind == superKind = tcPutTyVar kv boxedTypeKind + | otherwise = ASSERT( super_kind == superBoxity ) + tcPutTyVar kv boxedKind + where + super_kind = tyVarKind kv + + +zonkTcTypeToType :: TcType -> NF_TcM s Type +zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty + where + -- Zonk a mutable but unbound type variable to + -- Void if it has kind (Type Boxed) + -- Voidxxx otherwise + zonk_unbound_tyvar tv + = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind -> + if kind == boxedTypeKind then + tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in + -- this vastly common case + else + tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) []) + + mk_void_tycon tv kind -- Make a new TyCon with the same kind as the + -- type variable tv. Same name too, apart from + -- making it start with a colon (sigh) + = mkPrimTyCon tc_name kind 0 [] VoidRep + where + tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv) + +-- zonkTcTyVarToTyVar is applied to the *binding* occurrence +-- of a type variable, at the *end* of type checking. +-- It zonks the type variable, to get a mutable, but unbound, tyvar, tv; +-- zonks its kind, and then makes an immutable version of tv and binds tv to it. +-- Now any bound occurences of the original type variable will get +-- zonked to the immutable version. + +zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar +zonkTcTyVarToTyVar tv + = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind -> + let + -- Make an immutable version + immut_tv = mkTyVar (tyVarName tv) kind + immut_tv_ty = mkTyVarTy immut_tv + + zap tv = tcPutTyVar tv immut_tv_ty + -- Bind the mutable version to the immutable one + in + -- If the type variable is mutable, then bind it to immut_tv_ty + -- so that all other occurrences of the tyvar will get zapped too + zonkTyVar zap tv `thenNF_Tc` \ ty2 -> + ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 ) + + returnNF_Tc immut_tv +\end{code} -zonk tyvar_fn (ForAllUsageTy uv uvs ty) - = panic "zonk:ForAllUsageTy" -zonk tyvar_fn (FunTy ty1 ty2 u) - = zonk tyvar_fn ty1 `thenNF_Tc` \ ty1' -> - zonk tyvar_fn ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (FunTy ty1' ty2' u) +%************************************************************************ +%* * +\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar} +%* * +%* For internal use only! * +%* * +%************************************************************************ -zonk tyvar_fn (DictTy c ty u) - = zonk tyvar_fn ty `thenNF_Tc` \ ty' -> - returnNF_Tc (DictTy c ty' u) +\begin{code} +-- zonkType is used for Kinds as well + +-- For unbound, mutable tyvars, zonkType uses the function given to it +-- For tyvars bound at a for-all, zonkType zonks them to an immutable +-- type variable and zonks the kind too + +zonkType :: (TcTyVar -> NF_TcM s Type) -- What to do with unbound mutable type variables + -- see zonkTcType, and zonkTcTypeToType + -> TcType + -> NF_TcM s Type +zonkType unbound_var_fn ty + = go ty + where + go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' -> + returnNF_Tc (TyConApp tycon tys') + + go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' -> + go ty2 `thenNF_Tc` \ ty2' -> + returnNF_Tc (NoteTy (SynNote ty1') ty2') + + go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations + + go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' -> + returnNF_Tc (NoteTy (UsgNote usg) ty2') + + go (FunTy arg res) = go arg `thenNF_Tc` \ arg' -> + go res `thenNF_Tc` \ res' -> + returnNF_Tc (FunTy arg' res') + + go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' -> + go arg `thenNF_Tc` \ arg' -> + returnNF_Tc (mkAppTy fun' arg') + + -- The two interesting cases! + go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar + + go (ForAllTy tyvar ty) + = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' -> + go ty `thenNF_Tc` \ ty' -> + returnNF_Tc (ForAllTy tyvar' ty') + + +zonkTyVar :: (TcTyVar -> NF_TcM s Type) -- What to do for an unbound mutable variable + -> TcTyVar -> NF_TcM s TcType +zonkTyVar unbound_var_fn tyvar + | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when + -- zonking a forall type, when the bound type variable + -- needn't be mutable + = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars + returnNF_Tc (TyVarTy tyvar) + + | otherwise + = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + Nothing -> unbound_var_fn tyvar -- Mutable and unbound + Just other_ty -> ASSERT( isNotUsgTy other_ty ) + zonkType unbound_var_fn other_ty -- Bound +\end{code} +%************************************************************************ +%* * +\subsection{tcTypeKind} +%* * +%************************************************************************ -zonk_tv tyvar_fn tyvar - = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - UnBound -> returnNF_Tc (TyVarTy (tyvar_fn tyvar)) - BoundTo ty -> zonk tyvar_fn ty +Sadly, we need a Tc version of typeKind, that looks though mutable +kind variables. See the notes with Type.typeKind for the typeKindF nonsense +This is pretty gruesome. -zonk_tv_to_tv tyvar_fn tyvar - = zonk_tv tyvar_fn tyvar `thenNF_Tc` \ ty -> - case getTyVar_maybe ty of - Nothing -> panic "zonk_tv_to_tv" - Just tyvar -> returnNF_Tc tyvar +\begin{code} +tcTypeKind :: TcType -> NF_TcM s TcKind + +tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar) +tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys +tcTypeKind (NoteTy _ ty) = tcTypeKind ty +tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind -> + tcFunResultTy fun_kind +tcTypeKind (FunTy fun arg) = tcTypeKindF arg +tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty + +tcTypeKindF :: TcType -> NF_TcM s TcKind +tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty +tcTypeKindF (FunTy _ ty) = tcTypeKindF ty +tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty +tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind -> + fix_up kind + where + fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind + -- Functions at the type level are always boxed + fix_up (NoteTy _ kind) = fix_up kind + fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + Just kind' -> fix_up kind' + Nothing -> returnNF_Tc kind + fix_up kind = returnNF_Tc kind + +tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty +tcFunResultTy (FunTy arg res) = returnNF_Tc res +tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + Just ty' -> tcFunResultTy ty' + -- The Nothing case, and the other cases for tcFunResultTy + -- should never happen... pattern match failure \end{code}