X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=54cb45175c23b950d9f40bf47ef69d022948584c;hb=438596897ebbe25a07e1c82085cfbc5bdb00f09e;hp=eff458dc8b119b5510bd2a26a9b433bc1ac11fc2;hpb=f7ecf7234c224489be8a5e63fced903b655d92ee;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index eff458d..54cb451 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -1,114 +1,117 @@ -\begin{code} -#include "HsVersions.h" +% +% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +% +\section[TcType]{Types used in the typechecker} +\begin{code} module TcType ( - - SYN_IE(TcTyVar), + + TcTyVar, TcBox, + TcTyVarSet, newTcTyVar, newTyVarTy, -- Kind -> NF_TcM s (TcType s) newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s] - - SYN_IE(TcTyVarSet), - ----------------------------------------- - SYN_IE(TcType), TcMaybe(..), - SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(TcRhoType), + TcType, TcMaybe(..), + 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) + tcSplitRhoTy, + tcInstTyVars, - tcInstSigTyVars, - tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType, - tcInstTheta, tcInstId, + tcInstTcType, - zonkTcTyVars, - zonkTcType, - zonkTcTypeToType, - zonkTcTyVar, - zonkTcTyVarToTyVar + typeToTcType, + + -------------------------------- + TcKind, + newKindVar, newKindVars, + kindToTcKind, + zonkTcKind, + + -------------------------------- + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr, + zonkTcType, zonkTcTypes, zonkTcThetaType, + + zonkTcTypeToType, zonkTcTyVarToTyVar, + zonkTcKindToKind ) where +#include "HsVersions.h" -- friends: -import Type ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..), - tyVarsOfTypes, getTyVar_maybe, - splitForAllTy, splitRhoTy, - mkForAllTys, instantiateTy - ) -import TyVar ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet), - SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv, - nullTyVarEnv, mkTyVarEnv, - tyVarSetToList - ) +import PprType () +import Type ( Type, Kind, ThetaType, GenType(..), TyNote(..), + mkAppTy, + splitDictTy_maybe, splitForAllTys, + isTyVarTy, mkTyVarTys, + fullSubstTy, substFlexiTy, + boxedTypeKind, superKind + ) +import VarEnv +import VarSet ( emptyVarSet ) +import Var ( TyVar, GenTyVar, tyVarKind, tyVarFlexi, tyVarName, + mkFlexiTyVar, removeTyVarFlexi, isFlexiTyVar, isTyVar + ) -- others: -import Class ( GenClass ) -import Id ( idType ) -import Kind ( Kind ) -import TcKind ( TcKind ) -import TcMonad hiding ( rnMtoTcM ) -import Usage ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage ) +import TcMonad +import Name ( changeUnique ) -import TysPrim ( voidTy ) +import TysWiredIn ( voidTy ) -IMP_Ubiq() +import Name ( NamedThing(..), changeUnique, mkSysLocalName ) import Unique ( Unique ) -import UniqFM ( UniqFM ) -import Maybes ( assocMaybe ) -import Util ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} ) - ---import Outputable ( Outputable(..) ) -- Debugging messages ---import PprType ( GenTyVar, GenType ) ---import Pretty -- ditto ---import PprStyle ( PprStyle(..) ) -- ditto +import Util ( nOfThem ) +import Outputable \end{code} Data types ~~~~~~~~~~ +See 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) - -data TcMaybe s = UnBound - | BoundTo (TcType s) - | DontBind -- This variant is used for tyvars - -- arising from type signatures, or - -- existentially quantified tyvars; - -- The idea is that we must not unify - -- such tyvars with anything except - -- themselves. - --- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s), --- because you get a synonym loop if you do! - -type TcTyVar s = GenTyVar (Box s) -type TcTyVarSet s = GenTyVarSet (Box s) +tcTyVarToTyVar :: TcTyVar s -> TyVar +tcTyVarToTyVar = removeTyVarFlexi \end{code} +Utility functions +~~~~~~~~~~~~~~~~~ +These tcSplit functions are like their non-Tc analogues, but they +follow through bound type variables. + +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 s -> NF_TcM s (TcThetaType s, TcType s) +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 = tcReadTyVar tv `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + BoundTo 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 + +New type variables ~~~~~~~~~~~~~~~~~~ \begin{code} @@ -116,7 +119,10 @@ newTcTyVar :: Kind -> NF_TcM s (TcTyVar s) newTcTyVar kind = tcGetUnique `thenNF_Tc` \ uniq -> tcNewMutVar UnBound `thenNF_Tc` \ box -> - returnNF_Tc (TyVar uniq kind Nothing box) + let + name = mkSysLocalName uniq + in + returnNF_Tc (mkFlexiTyVar name kind box) newTyVarTy :: Kind -> NF_TcM s (TcType s) newTyVarTy kind @@ -126,169 +132,75 @@ newTyVarTy kind newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s] newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind) +newKindVar :: NF_TcM s (TcKind s) +newKindVar = newTyVarTy superKind --- For signature type variables, mark them as "DontBind" -tcInstTyVars, tcInstSigTyVars - :: [GenTyVar flexi] - -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)]) +newKindVars :: Int -> NF_TcM s [TcKind s] +newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ()) +\end{code} -tcInstTyVars tyvars = inst_tyvars UnBound tyvars -tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars +Type instantiation +~~~~~~~~~~~~~~~~~~ + +Instantiating a bunch of type variables + +\begin{code} +tcInstTyVars :: [GenTyVar flexi] + -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s)) -inst_tyvars initial_cts tyvars - = mapNF_Tc (inst_tyvar initial_cts) tyvars `thenNF_Tc` \ tc_tyvars -> +tcInstTyVars tyvars + = mapNF_Tc inst_tyvar tyvars `thenNF_Tc` \ tc_tyvars -> let - tys = map TyVarTy tc_tyvars + tys = mkTyVarTys tc_tyvars in - returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys) + returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys) -inst_tyvar initial_cts (TyVar _ kind name _) +inst_tyvar tyvar -- Could use the name from the tyvar? = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutVar initial_cts `thenNF_Tc` \ box -> - returnNF_Tc (TyVar uniq kind name box) + tcNewMutVar UnBound `thenNF_Tc` \ box -> + let + name = changeUnique (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. + in + returnNF_Tc (mkFlexiTyVar name (tyVarKind tyvar) box) \end{code} -@tcInstType@ and @tcInstSigType@ both create a fresh instance of a -type, returning a @TcType@. All inner for-alls are instantiated with -fresh TcTyVars. +@tcInstTcType@ instantiates the outer-level for-alls of a TcType with +fresh type variables, returning them and the instantiated body of the for-all. -The difference is that tcInstType instantiates all forall'd type -variables (and their bindees) with UnBound type variables, whereas -tcInstSigType instantiates them with DontBind types variables. -@tcInstSigType@ also doesn't take an environment. - -On the other hand, @tcInstTcType@ instantiates a TcType. It uses -instantiateTy which could take advantage of sharing some day. \begin{code} tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s) tcInstTcType ty - = case tyvars of + = let + (tyvars, rho) = splitForAllTys ty + in + case tyvars of [] -> returnNF_Tc ([], ty) -- Nothing to do other -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> - returnNF_Tc (tyvars', instantiateTy tenv rho) - where - (tyvars, rho) = splitForAllTy ty - -tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s) -tcInstSigTcType ty - = case tyvars of - [] -> returnNF_Tc ([], ty) -- Nothing to do - other -> tcInstSigTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> - returnNF_Tc (tyvars', instantiateTy tenv rho) - where - (tyvars, rho) = splitForAllTy ty - -tcInstType :: [(GenTyVar flexi,TcType s)] - -> GenType (GenTyVar flexi) UVar - -> NF_TcM s (TcType s) -tcInstType tenv ty_to_inst - = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst - where - bind_fn = inst_tyvar UnBound - occ_fn env tyvar = case lookupTyVarEnv env tyvar of - Just ty -> returnNF_Tc ty - Nothing -> panic "tcInstType:1" --(ppAboves [ppr PprDebug ty_to_inst, - -- ppr PprDebug tyvar]) - -tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s) -tcInstSigType ty_to_inst - = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst - where - bind_fn = inst_tyvar DontBind - occ_fn env tyvar = case lookupTyVarEnv env tyvar of - Just ty -> returnNF_Tc ty - Nothing -> panic "tcInstType:2"-- (ppAboves [ppr PprDebug ty_to_inst, - -- ppr PprDebug tyvar]) - -zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar -zonkTcTyVarToTyVar tv - = zonkTcTyVar tv `thenNF_Tc` \ tv_ty -> - case tv_ty of -- Should be a tyvar! - - TyVarTy tv' -> returnNF_Tc (tcTyVarToTyVar tv') - - _ -> --pprTrace "zonkTcTyVarToTyVar:" (ppCat [ppr PprDebug tv, ppr PprDebug tv_ty]) $ - returnNF_Tc (tcTyVarToTyVar tv) - - -zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type -zonkTcTypeToType env ty - = tcConvert zonkTcTyVarToTyVar occ_fn env ty - where - occ_fn env tyvar - = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - BoundTo (TyVarTy tyvar') -> lookup env tyvar' - BoundTo other_ty -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty - other -> lookup env tyvar - - lookup env tyvar = case lookupTyVarEnv env tyvar of - Just ty -> returnNF_Tc ty - Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void - - -tcConvert bind_fn occ_fn env ty_to_convert - = doo env ty_to_convert - where - doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage) - - doo env (SynTy tycon tys ty) = mapNF_Tc (doo env) tys `thenNF_Tc` \ tys' -> - doo env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (SynTy tycon tys' ty') - - doo env (FunTy arg res usage) = doo env arg `thenNF_Tc` \ arg' -> - doo env res `thenNF_Tc` \ res' -> - returnNF_Tc (FunTy arg' res' usage) - - doo env (AppTy fun arg) = doo env fun `thenNF_Tc` \ fun' -> - doo env arg `thenNF_Tc` \ arg' -> - returnNF_Tc (AppTy fun' arg') - - doo env (DictTy clas ty usage)= doo env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (DictTy clas ty' usage) - - doo env (ForAllUsageTy u us ty) = doo env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllUsageTy u us ty') - - -- The two interesting cases! - doo env (TyVarTy tv) = occ_fn env tv - - doo env (ForAllTy tyvar ty) - = bind_fn tyvar `thenNF_Tc` \ tyvar' -> - let - new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar') - in - doo new_env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllTy tyvar' ty') + 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} +Sometimes we have to convert a Type to a TcType. I wonder whether we could +do this less than we do? -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) - --- A useful function that takes an occurrence of a global thing --- and instantiates its type with fresh type variables -tcInstId :: Id - -> NF_TcM s ([TcTyVar s], -- It's instantiated type - TcThetaType s, -- - TcType s) -- +\begin{code} +typeToTcType :: Type -> TcType s +typeToTcType t = substFlexiTy emptyVarEnv t -tcInstId id - = let - (tyvars, rho) = splitForAllTy (idType id) - in - tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', arg_tys, tenv) -> - tcInstType tenv rho `thenNF_Tc` \ rho' -> - let - (theta', tau') = splitRhoTy rho' - in - returnNF_Tc (tyvars', theta', tau') +kindToTcKind :: Kind -> TcKind s +kindToTcKind = typeToTcType \end{code} + Reading and writing TcTyVars ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} @@ -299,12 +211,12 @@ tcReadTyVar :: TcTyVar s -> NF_TcM s (TcMaybe s) Writing is easy: \begin{code} -tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty) +tcWriteTyVar tyvar ty = tcWriteMutVar (tyVarFlexi tyvar) (BoundTo ty) \end{code} Reading is more interesting. The easy thing to do is just to read, thus: \begin{verbatim} -tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box +tcReadTyVar tyvar = tcReadMutVar (tyVarFlexi tyvar) \end{verbatim} But it's more fun to short out indirections on the way: If this @@ -314,7 +226,7 @@ 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) +tcReadTyVar tyvar = tcReadMutVar box `thenNF_Tc` \ maybe_ty -> case maybe_ty of BoundTo ty -> short_out ty `thenNF_Tc` \ ty' -> @@ -322,9 +234,11 @@ tcReadTyVar (TyVar uniq kind name box) returnNF_Tc (BoundTo ty') other -> returnNF_Tc other + where + box = tyVarFlexi tyvar short_out :: TcType s -> NF_TcM s (TcType s) -short_out ty@(TyVarTy (TyVar uniq kind name box)) +short_out ty@(TyVarTy tyvar) = tcReadMutVar box `thenNF_Tc` \ maybe_ty -> case maybe_ty of BoundTo ty' -> short_out ty' `thenNF_Tc` \ ty' -> @@ -332,27 +246,51 @@ short_out ty@(TyVarTy (TyVar uniq kind name box)) returnNF_Tc ty' other -> returnNF_Tc ty + where + box = tyVarFlexi tyvar short_out other_ty = returnNF_Tc other_ty \end{code} -Zonking -~~~~~~~ +Zonking Tc types to Tc types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} -zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s) -zonkTcTyVars tyvars - = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars) `thenNF_Tc` \ tys -> - returnNF_Tc (tyVarsOfTypes tys) +zonkTcTyVars :: [TcTyVar s] -> NF_TcM s [TcType s] +zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s) zonkTcTyVar tyvar + | not (isFlexiTyVar tyvar) -- Not a flexi tyvar. This can happen when + -- zonking a forall type, when the bound type variable + -- needn't be a flexi. + = ASSERT( isTyVar tyvar ) + returnNF_Tc (TyVarTy tyvar) + + | otherwise -- Is a flexi tyvar = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of - BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty + BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty -- tcReadTyVar never returns a bound tyvar BoundTo other -> zonkTcType other other -> returnNF_Tc (TyVarTy tyvar) +zonkTcTyVarBndr :: TcTyVar s -> NF_TcM s (TcTyVar s) +zonkTcTyVarBndr tyvar + = zonkTcTyVar tyvar `thenNF_Tc` \ (TyVarTy tyvar') -> + returnNF_Tc tyvar' + +zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s] +zonkTcTypes tys = mapNF_Tc zonkTcType tys + +zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s) +zonkTcThetaType theta = mapNF_Tc zonk theta + where + zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts -> + returnNF_Tc (c, new_ts) + +zonkTcKind :: TcKind s -> NF_TcM s (TcKind s) +zonkTcKind = zonkTcType + zonkTcType :: TcType s -> NF_TcM s (TcType s) zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar @@ -360,35 +298,93 @@ zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar zonkTcType (AppTy ty1 ty2) = zonkTcType ty1 `thenNF_Tc` \ ty1' -> zonkTcType ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (AppTy ty1' ty2') - -zonkTcType (TyConTy tc u) - = returnNF_Tc (TyConTy tc u) + returnNF_Tc (mkAppTy ty1' ty2') -zonkTcType (SynTy tc tys ty) +zonkTcType (TyConApp tc tys) = mapNF_Tc zonkTcType tys `thenNF_Tc` \ tys' -> - zonkTcType ty `thenNF_Tc` \ ty' -> - returnNF_Tc (SynTy tc tys' ty') + returnNF_Tc (TyConApp tc tys') + +zonkTcType (NoteTy (SynNote ty1) ty2) + = zonkTcType ty1 `thenNF_Tc` \ ty1' -> + zonkTcType ty2 `thenNF_Tc` \ ty2' -> + returnNF_Tc (NoteTy (SynNote ty1') ty2') + +zonkTcType (NoteTy (FTVNote _) ty2) = zonkTcType ty2 zonkTcType (ForAllTy tv ty) = zonkTcTyVar tv `thenNF_Tc` \ tv_ty -> zonkTcType ty `thenNF_Tc` \ ty' -> case tv_ty of -- Should be a tyvar! - TyVarTy tv' -> - returnNF_Tc (ForAllTy tv' ty') - _ -> --pprTrace "zonkTcType:ForAllTy:" (ppCat [ppr PprDebug tv, ppr PprDebug tv_ty]) $ - - returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty') + TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty') + _ -> panic "zonkTcType" + -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $ + -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty') -zonkTcType (ForAllUsageTy uv uvs ty) - = panic "zonk:ForAllUsageTy" - -zonkTcType (FunTy ty1 ty2 u) +zonkTcType (FunTy ty1 ty2) = zonkTcType ty1 `thenNF_Tc` \ ty1' -> zonkTcType ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (FunTy ty1' ty2' u) + returnNF_Tc (FunTy ty1' ty2') +\end{code} + +Zonking Tc types to Type/Kind +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +\begin{code} +zonkTcKindToKind :: TcKind s -> NF_TcM s Kind +zonkTcKindToKind kind = zonkTcToType boxedTypeKind emptyVarEnv kind + +zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type +zonkTcTypeToType env ty = zonkTcToType voidTy env ty + +zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar +zonkTcTyVarToTyVar tv + = zonkTcTyVarBndr tv `thenNF_Tc` \ tv' -> + returnNF_Tc (tcTyVarToTyVar tv') -zonkTcType (DictTy c ty u) - = zonkTcType ty `thenNF_Tc` \ ty' -> - returnNF_Tc (DictTy c ty' u) +-- zonkTcToType is used for Kinds as well +zonkTcToType :: Type -> TyVarEnv Type -> TcType s -> NF_TcM s Type +zonkTcToType unbound_var_ty env 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 (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! + -- c.f. zonkTcTyVar + go (TyVarTy tyvar) + | not (isFlexiTyVar tyvar) = lookup env tyvar + + | otherwise = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + BoundTo (TyVarTy tyvar') -> lookup env tyvar' + BoundTo other_ty -> go other_ty + other -> lookup env tyvar + + go (ForAllTy tyvar ty) + = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' -> + let + new_env = extendVarEnv env tyvar (TyVarTy tyvar') + in + zonkTcToType unbound_var_ty new_env ty `thenNF_Tc` \ ty' -> + returnNF_Tc (ForAllTy tyvar' ty') + + + lookup env tyvar = returnNF_Tc (case lookupVarEnv env tyvar of + Just ty -> ty + Nothing -> unbound_var_ty) \end{code} + +