X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=73c183bcfe87ae0b0adc408d927eec5a74ea4981;hb=510d96b44148caf7261dcc3530648c5905016efc;hp=2944d90d2da8ab645b456f3d0f66d23a5c58eb05;hpb=9dd6e1c216993624a2cd74b62ca0f0569c02c26b;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 2944d90..73c183b 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -1,34 +1,40 @@ +% +% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +% +\section[TcType]{Types used in the typechecker} + \begin{code} module TcType ( - TcTyVar, TcBox, + TcTyVar, TcTyVarSet, - newTcTyVar, - newTyVarTy, -- Kind -> NF_TcM s (TcType s) - newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s] + newTyVar, + newTyVarTy, -- Kind -> NF_TcM TcType + newTyVarTys, -- Int -> Kind -> NF_TcM [TcType] ----------------------------------------- - TcType, TcMaybe(..), - TcTauType, TcThetaType, TcRhoType, + TcType, TcTauType, TcThetaType, TcRhoType, TcClassContext, -- 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 - tcSplitForAllTy, tcSplitRhoTy, + tcSplitRhoTy, - tcInstTyVars, - tcInstSigTyVars, + tcInstTyVar, tcInstTyVars, + tcInstSigVar, tcInstType, - tcInstSigType, tcInstTcType, tcInstSigTcType, - tcInstTheta, - zonkTcTyVars, zonkSigTyVar, - zonkTcType, zonkTcTypes, zonkTcThetaType, - zonkTcTypeToType, - zonkTcTyVar, - zonkTcTyVarToTyVar + -------------------------------- + TcKind, + newKindVar, newKindVars, newBoxityVar, + + -------------------------------- + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars, + zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, + + zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv ) where @@ -36,290 +42,189 @@ module TcType ( -- friends: -import Type ( Type, ThetaType, GenType(..), mkAppTy, - tyVarsOfTypes, getTyVar_maybe, splitDictTy_maybe, - splitForAllTys, splitRhoTy, isTyVarTy, - mkForAllTys, instantiateTy - ) -import TyVar ( TyVar, GenTyVar(..), TyVarSet, GenTyVarSet, - TyVarEnv, lookupTyVarEnv, addToTyVarEnv, - emptyTyVarEnv, mkTyVarEnv, zipTyVarEnv, - tyVarSetToList - ) +import TypeRep ( Type(..), Kind, TyNote(..) ) -- friend +import Type ( PredType(..), + getTyVar, mkAppTy, mkUTy, + splitPredTy_maybe, splitForAllTys, + isTyVarTy, mkTyVarTy, mkTyVarTys, + openTypeKind, liftedTypeKind, + superKind, superBoxity, tyVarsOfTypes, + defaultKind, liftedBoxity + ) +import Subst ( Subst, mkTopTyVarSubst, substTy ) +import TyCon ( mkPrimTyCon ) +import PrimRep ( PrimRep(VoidRep) ) +import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar ) -- others: -import Class ( Class ) -import TyCon ( isFunTyCon ) -import Kind ( Kind ) -import TcKind ( TcKind ) -import TcMonad - -import TysPrim ( voidTy ) - -import Name ( NamedThing(..) ) -import Unique ( Unique ) -import UniqFM ( UniqFM ) -import Maybes ( assocMaybe ) -import BasicTypes ( unused ) -import Util ( zipEqual, nOfThem ) +import TcMonad -- TcType, amongst others +import TysWiredIn ( voidTy ) + +import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName, + mkLocalName, mkDerivedTyConOcc + ) +import Unique ( Uniquable(..) ) +import SrcLoc ( noSrcLoc ) +import Util ( nOfThem ) import Outputable \end{code} - -Data types -~~~~~~~~~~ - - -\begin{code} -type TcType s = GenType (TcBox s) -- 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 TcBox s = TcRef s (TcMaybe s) - -data TcMaybe s = UnBound - | BoundTo (TcType s) - --- 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 (TcBox s) -type TcTyVarSet s = GenTyVarSet (TcBox s) -\end{code} - -\begin{code} -tcTyVarToTyVar :: TcTyVar s -> TyVar -tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name unused -\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} -tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s) -tcSplitForAllTy t - = go t t [] - where - go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs) - go syn_t (SynTy _ t) tvs = go syn_t t tvs - go syn_t (TyVarTy tv) tvs = tcReadTyVar tv `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs - other -> returnNF_Tc (reverse tvs, syn_t) - go syn_t t tvs = returnNF_Tc (reverse tvs, syn_t) - -tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s) +tcSplitRhoTy :: TcType -> NF_TcM (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 + go syn_t (FunTy arg res) ts = case splitPredTy_maybe arg of Just pair -> go res res (pair:ts) Nothing -> returnNF_Tc (reverse ts, syn_t) - go syn_t (SynTy _ t) ts = go syn_t t ts - go syn_t (TyVarTy tv) ts = tcReadTyVar tv `thenNF_Tc` \ maybe_ty -> + 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 - BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts - other -> returnNF_Tc (reverse ts, syn_t) + Just ty | not (isTyVarTy ty) -> go syn_t ty ts + other -> returnNF_Tc (reverse ts, syn_t) + go syn_t (UsageTy _ t) ts = go syn_t t ts go syn_t t ts = returnNF_Tc (reverse ts, syn_t) \end{code} -Type instantiation -~~~~~~~~~~~~~~~~~~ +%************************************************************************ +%* * +\subsection{New type variables} +%* * +%************************************************************************ \begin{code} -newTcTyVar :: Kind -> NF_TcM s (TcTyVar s) -newTcTyVar kind +newTyVar :: Kind -> NF_TcM TcTyVar +newTyVar kind = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutVar UnBound `thenNF_Tc` \ box -> - returnNF_Tc (TyVar uniq kind Nothing box) + tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind -newTyVarTy :: Kind -> NF_TcM s (TcType s) +newTyVarTy :: Kind -> NF_TcM TcType newTyVarTy kind - = newTcTyVar 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 :: Int -> Kind -> NF_TcM [TcType] newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind) +newKindVar :: NF_TcM TcKind +newKindVar + = tcGetUnique `thenNF_Tc` \ uniq -> + tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv -> + returnNF_Tc (TyVarTy kv) --- For signature type variables, use the user name for the type variable -tcInstTyVars, tcInstSigTyVars - :: [GenTyVar flexi] - -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s)) +newKindVars :: Int -> NF_TcM [TcKind] +newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ()) -tcInstTyVars tyvars = inst_tyvars inst_tyvar tyvars -tcInstSigTyVars tyvars = inst_tyvars inst_sig_tyvar tyvars - -inst_tyvars inst tyvars - = mapNF_Tc inst tyvars `thenNF_Tc` \ tc_tyvars -> - let - tys = map TyVarTy tc_tyvars - in - returnNF_Tc (tc_tyvars, tys, zipTyVarEnv tyvars tys) - -inst_tyvar (TyVar _ kind name _) - = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutVar UnBound `thenNF_Tc` \ box -> - returnNF_Tc (TyVar uniq kind Nothing box) - -- The "Nothing" means that it'll always print with its - -- unique (or something similar). If we leave the original (Just Name) - -- in there then error messages will say "can't match (T a) against (T a)" - -inst_sig_tyvar (TyVar _ kind name _) - = tcGetUnique `thenNF_Tc` \ uniq -> - - tcNewMutVar UnBound `thenNF_Tc` \ box -> - -- Was DontBind, but we've nuked that "optimisation" - - returnNF_Tc (TyVar uniq kind name box) - -- We propagate the name of the sigature type variable +newBoxityVar :: NF_TcM TcKind +newBoxityVar + = tcGetUnique `thenNF_Tc` \ uniq -> + tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv -> + returnNF_Tc (TyVarTy kv) \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. -The difference is that tcInstType instantiates all forall'd type -variables (and their bindees) with anonymous type variables, whereas -tcInstSigType instantiates them with named type variables. -@tcInstSigType@ also doesn't take an environment. +%************************************************************************ +%* * +\subsection{Type instantiation} +%* * +%************************************************************************ -On the other hand, @tcInstTcType@ instantiates a TcType. It uses -instantiateTy which could take advantage of sharing some day. +Instantiating a bunch of type variables \begin{code} -tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s) -tcInstTcType ty - = tcSplitForAllTy ty `thenNF_Tc` \ (tyvars, rho) -> - case tyvars of - [] -> returnNF_Tc ([], ty) -- Nothing to do - other -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> - returnNF_Tc (tyvars', instantiateTy tenv rho) - -tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s) -tcInstSigTcType ty - = tcSplitForAllTy ty `thenNF_Tc` \ (tyvars, rho) -> - case tyvars of - [] -> returnNF_Tc ([], ty) -- Nothing to do - other -> tcInstSigTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> - returnNF_Tc (tyvars', instantiateTy tenv rho) - -tcInstType :: TyVarEnv (TcType s) - -> GenType flexi - -> NF_TcM s (TcType s) -tcInstType tenv ty_to_inst - = tcConvert bind_fn occ_fn tenv ty_to_inst - where - bind_fn = inst_tyvar - occ_fn env tyvar = case lookupTyVarEnv env tyvar of - Just ty -> returnNF_Tc ty - Nothing -> panic "tcInstType:1" --(vcat [ppr ty_to_inst, - -- ppr tyvar]) - -tcInstSigType :: GenType flexi -> NF_TcM s (TcType s) -tcInstSigType ty_to_inst - = tcConvert bind_fn occ_fn emptyTyVarEnv ty_to_inst - where - bind_fn = inst_sig_tyvar -- Note: inst_sig_tyvar, not inst_tyvar - -- I don't think that can lead to strange error messages - occ_fn env tyvar = case lookupTyVarEnv env tyvar of - Just ty -> returnNF_Tc ty - Nothing -> panic "tcInstType:2"-- (vcat [ppr ty_to_inst, - -- ppr 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:" (hsep [ppr tv, ppr 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 +tcInstTyVars :: [TyVar] + -> NF_TcM ([TcTyVar], [TcType], Subst) +tcInstTyVars tyvars + = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars -> + let + tys = mkTyVarTys tc_tyvars + in + returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys) + -- Since the tyvars are freshly made, + -- they cannot possibly be captured by + -- any existing for-alls. Hence mkTopTyVarSubst -tcConvert bind_fn occ_fn env ty_to_convert - = doo env ty_to_convert - where - doo env (TyConApp tycon tys) = mapNF_Tc (doo env) tys `thenNF_Tc` \ tys' -> - returnNF_Tc (TyConApp tycon 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. + in + tcNewMutTyVar name (tyVarKind tyvar) - doo env (SynTy ty1 ty2) = doo env ty1 `thenNF_Tc` \ ty1' -> - doo env ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (SynTy ty1' ty2') +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} - doo env (FunTy arg res) = doo env arg `thenNF_Tc` \ arg' -> - doo env res `thenNF_Tc` \ res' -> - returnNF_Tc (FunTy arg' res') - - doo env (AppTy fun arg) = doo env fun `thenNF_Tc` \ fun' -> - doo env arg `thenNF_Tc` \ arg' -> - returnNF_Tc (mkAppTy fun' arg') +@tcInstType@ instantiates the outer-level for-alls of a TcType with +fresh type variables, splits off the dictionary part, and returns the results. - -- The two interesting cases! - doo env (TyVarTy tv) = occ_fn env tv +\begin{code} +tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType) +tcInstType ty + = case splitForAllTys ty of + ([], _) -> returnNF_Tc ([], [], ty) -- Nothing to do + (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> + tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) -> + returnNF_Tc (tyvars', theta, tau) +\end{code} - doo env (ForAllTy tyvar ty) - = bind_fn tyvar `thenNF_Tc` \ tyvar' -> - let - new_env = addToTyVarEnv env tyvar (TyVarTy tyvar') - in - doo new_env ty `thenNF_Tc` \ ty' -> - returnNF_Tc (ForAllTy tyvar' ty') -tcInstTheta :: TyVarEnv (TcType s) -> ThetaType -> NF_TcM s (TcThetaType s) -tcInstTheta tenv theta - = mapNF_Tc go theta - where - go (clas,tys) = mapNF_Tc (tcInstType tenv) tys `thenNF_Tc` \ tc_tys -> - returnNF_Tc (clas, tc_tys) -\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 TcType +tcGetTyVar :: TcTyVar -> NF_TcM (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 + | not (isMutTyVar tyvar) + = pprTrace "tcPutTyVar" (ppr tyvar) $ + returnNF_Tc ty + + | otherwise + = ASSERT( isMutTyVar tyvar ) + UASSERT2( not (isUTy ty), ppr tyvar <+> ppr 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 @@ -329,93 +234,236 @@ 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 + | not (isMutTyVar tyvar) + = pprTrace "tcGetTyVar" (ppr tyvar) $ + returnNF_Tc (Just (mkTyVarTy tyvar)) + + | otherwise + = ASSERT2( isMutTyVar tyvar, ppr tyvar ) + tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of - BoundTo ty -> short_out ty `thenNF_Tc` \ ty' -> - tcWriteMutVar box (BoundTo ty') `thenNF_Tc_` - returnNF_Tc (BoundTo ty') + Just ty -> short_out ty `thenNF_Tc` \ ty' -> + tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_` + returnNF_Tc (Just ty') - other -> returnNF_Tc other + Nothing -> returnNF_Tc Nothing -short_out :: TcType s -> NF_TcM s (TcType s) -short_out ty@(TyVarTy (TyVar uniq kind name box)) - = tcReadMutVar box `thenNF_Tc` \ maybe_ty -> +short_out :: TcType -> NF_TcM TcType +short_out ty@(TyVarTy tyvar) + | not (isMutTyVar tyvar) + = returnNF_Tc ty + + | otherwise + = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of - 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 + other -> returnNF_Tc ty short_out other_ty = returnNF_Tc other_ty \end{code} -Zonking -~~~~~~~ +%************************************************************************ +%* * +\subsection{Zonking -- the exernal interfaces} +%* * +%************************************************************************ + +----------------- Type variables + \begin{code} -zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s) -zonkTcTyVars tyvars - = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars) `thenNF_Tc` \ tys -> - returnNF_Tc (tyVarsOfTypes tys) - -zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s) -zonkTcTyVar tyvar - = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty -- tcReadTyVar never returns a bound tyvar - BoundTo other -> zonkTcType other - other -> returnNF_Tc (TyVarTy tyvar) - --- Signature type variables only get bound to each other, --- never to a type -zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s) -zonkSigTyVar tyvar - = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar' -- tcReadTyVar never returns a bound tyvar - BoundTo other -> panic "zonkSigTyVar" -- Should only be bound to another tyvar - other -> returnNF_Tc tyvar +zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType] +zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars + +zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet +zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys -> + returnNF_Tc (tyVarsOfTypes tys) + +zonkTcTyVar :: TcTyVar -> NF_TcM TcType +zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar + +zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar] +-- This guy is to zonk the tyvars we're about to feed into tcSimplify +-- Usually this job is done by checkSigTyVars, but in a couple of places +-- that is overkill, so we use this simpler chap +zonkTcSigTyVars tyvars + = zonkTcTyVars tyvars `thenNF_Tc` \ tys -> + returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys) +\end{code} + +----------------- Types -zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s] +\begin{code} +zonkTcType :: TcType -> NF_TcM TcType +zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty + +zonkTcTypes :: [TcType] -> NF_TcM [TcType] 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) - -zonkTcType :: TcType s -> NF_TcM s (TcType s) - -zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar - -zonkTcType (AppTy ty1 ty2) - = zonkTcType ty1 `thenNF_Tc` \ ty1' -> - zonkTcType ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (mkAppTy ty1' ty2') - -zonkTcType (TyConApp tc tys) - = mapNF_Tc zonkTcType tys `thenNF_Tc` \ tys' -> - returnNF_Tc (TyConApp tc tys') - -zonkTcType (SynTy ty1 ty2) - = zonkTcType ty1 `thenNF_Tc` \ ty1' -> - zonkTcType ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (SynTy ty1' 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') - _ -> panic "zonkTcType" - -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $ - -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty') - -zonkTcType (FunTy ty1 ty2) - = zonkTcType ty1 `thenNF_Tc` \ ty1' -> - zonkTcType ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (FunTy ty1' ty2') +zonkTcClassConstraints cts = mapNF_Tc zonk cts + where zonk (clas, tys) + = zonkTcTypes tys `thenNF_Tc` \ new_tys -> + returnNF_Tc (clas, new_tys) + +zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType +zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta + +zonkTcPredType :: TcPredType -> NF_TcM TcPredType +zonkTcPredType (Class c ts) = + zonkTcTypes ts `thenNF_Tc` \ new_ts -> + returnNF_Tc (Class c new_ts) +zonkTcPredType (IParam n t) = + zonkTcType t `thenNF_Tc` \ new_t -> + returnNF_Tc (IParam n new_t) +\end{code} + +------------------- These ...ToType, ...ToKind versions + are used at the end of type checking + +\begin{code} +zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)] +zonkKindEnv pairs + = mapNF_Tc zonk_it pairs + where + zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind -> + returnNF_Tc (name, kind) + + -- When zonking a kind, we want to + -- zonk a *kind* variable to (Type *) + -- zonk a *boxity* variable to * + zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv liftedTypeKind + | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity + | otherwise = pprPanic "zonkKindEnv" (ppr kv) + +zonkTcTypeToType :: TcType -> NF_TcM Type +zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty + where + -- Zonk a mutable but unbound type variable to + -- Void if it has kind Lifted + -- :Void otherwise + zonk_unbound_tyvar tv + | kind == liftedTypeKind || kind == openTypeKind + = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in + -- this vastly common case + | otherwise + = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) []) + where + kind = tyVarKind tv + + 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) + -- I dread to think what will happen if this gets out into an + -- interface file. Catastrophe likely. Major sigh. + = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $ + mkPrimTyCon tc_name kind 0 [] VoidRep + where + tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc + +-- zonkTcTyVarToTyVar is applied to the *binding* occurrence +-- of a type variable, at the *end* of type checking. It changes +-- the *mutable* type variable into an *immutable* one. +-- +-- It does this by making 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 TyVar +zonkTcTyVarToTyVar tv + = let + -- Make an immutable version, defaulting + -- the kind to lifted if necessary + immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv)) + 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 -> + + WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 ) + + returnNF_Tc immut_tv \end{code} + + +%************************************************************************ +%* * +\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar} +%* * +%* For internal use only! * +%* * +%************************************************************************ + +\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 Type) -- What to do with unbound mutable type variables + -- see zonkTcType, and zonkTcTypeToType + -> TcType + -> NF_TcM 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 (PredTy p) = go_pred p `thenNF_Tc` \ p' -> + returnNF_Tc (PredTy p') + + 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') + + go (UsageTy u ty) = go u `thenNF_Tc` \ u' -> + go ty `thenNF_Tc` \ ty' -> + returnNF_Tc (mkUTy u' ty') + + -- 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') + + go_pred (Class c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' -> + returnNF_Tc (Class c tys') + go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' -> + returnNF_Tc (IParam n ty') + +zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable + -> TcTyVar -> NF_TcM 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 -> zonkType unbound_var_fn other_ty -- Bound +\end{code} +