+%
+% (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 TcType
+ newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
- TcTyVar(..),
- newTcTyVar,
- newTyVarTy, -- Kind -> NF_TcM s (TcType s)
- newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
+ -----------------------------------------
+ TcType, TcTauType, TcThetaType, TcRhoType,
+ -- Find the type to which a type variable is bound
+ tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType
+ tcGetTyVar, -- :: TcTyVar -> NF_TcM (Maybe TcType) does shorting out
- TcTyVarSet(..),
- -----------------------------------------
- TcType(..), TcMaybe(..),
- TcTauType(..), TcThetaType(..), TcRhoType(..),
+ tcSplitRhoTy,
- -- 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)
+ tcInstTyVar, tcInstTyVars,
+ tcInstSigVars,
+ tcInstType,
+ --------------------------------
+ TcKind,
+ newKindVar, newKindVars, newBoxityVar,
- tcInstTyVars, -- TyVar -> NF_TcM s (TcTyVar s)
- tcInstSigTyVars,
- tcInstType, tcInstTcType, tcInstTheta,
+ --------------------------------
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+ zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
+ zonkTcPredType,
- 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, zonkKindEnv
) where
+#include "HsVersions.h"
-- friends:
-import Type ( Type(..), ThetaType(..), GenType(..), tyVarsOfTypes, getTyVar_maybe )
-import TyVar ( TyVar(..), GenTyVar(..), TyVarSet(..), GenTyVarSet(..),
- 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 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, pprPanic )
-
-import Outputable ( Outputable(..) ) -- Debugging messages
-import PprType ( GenTyVar, GenType )
-import Pretty -- ditto
-import PprStyle ( PprStyle(..) ) -- ditto
+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}
+Utility functions
+~~~~~~~~~~~~~~~~~
+These tcSplit functions are like their non-Tc analogues, but they
+follow through bound type variables.
-Data types
-~~~~~~~~~~
+No need for tcSplitForAllTy because a type variable can't be instantiated
+to a for-all type.
\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)
+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 splitPredTy_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 (UsageTy _ t) ts = go syn_t t ts
+ go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
\end{code}
-\begin{code}
-tcTyVarToTyVar :: TcTyVar s -> TyVar
-tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
-\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 n kind = mapNF_Tc newTyVarTy (take n (repeat kind))
+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)
+newKindVars :: Int -> NF_TcM [TcKind]
+newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
--- For signature type variables, mark them as "DontBind"
-tcInstTyVars, tcInstSigTyVars
- :: [GenTyVar flexi]
- -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
-tcInstTyVars tyvars = inst_tyvars UnBound tyvars
-tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
+newBoxityVar :: NF_TcM TcKind
+newBoxityVar
+ = tcGetUnique `thenNF_Tc` \ uniq ->
+ tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
+ returnNF_Tc (TyVarTy kv)
+\end{code}
-inst_tyvars initial_cts tyvars
- = mapNF_Tc (inst_tyvar initial_cts) tyvars `thenNF_Tc` \ tc_tyvars ->
+%************************************************************************
+%* *
+\subsection{Type instantiation}
+%* *
+%************************************************************************
+
+Instantiating a bunch of type variables
+
+\begin{code}
+tcInstTyVars :: [TyVar]
+ -> NF_TcM ([TcTyVar], [TcType], Subst)
+
+tcInstTyVars tyvars
+ = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
let
- tys = map TyVarTy tc_tyvars
+ tys = mkTyVarTys tc_tyvars
in
- returnNF_Tc (tc_tyvars, tys, tyvars `zip` tys)
+ 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
-inst_tyvar initial_cts (TyVar _ kind name _)
+tcInstTyVar tyvar
= tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutVar initial_cts `thenNF_Tc` \ box ->
- returnNF_Tc (TyVar uniq kind name box)
+ 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)
+
+tcInstSigVars tyvars -- Very similar to tcInstTyVar
+ = tcGetUniques `thenNF_Tc` \ uniqs ->
+ listTc [ ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
+ tcNewSigTyVar name kind
+ | (tyvar, uniq) <- tyvars `zip` uniqs,
+ let name = setNameUnique (tyVarName tyvar) uniq,
+ let kind = tyVarKind tyvar
+ ]
\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.
-
-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.
+@tcInstType@ instantiates the outer-level for-alls of a TcType with
+fresh type variables, splits off the dictionary part, and returns the results.
\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)
-
- 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 (TyVarTy tv@(TyVar uniq kind name _))
- = case assocMaybe env uniq of
- Just tc_ty -> returnNF_Tc tc_ty
- Nothing -> pprPanic "tcInstType:" (ppAboves [ppr PprDebug tenv,
- ppr PprDebug ty_to_inst, ppr PprDebug tv])
-
- do env (ForAllTy tyvar@(TyVar uniq kind name _) ty)
- = inst_tyvar DontBind tyvar `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
-
-
-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)
-
---???tcSpecTy :: Type -> NF_TcM s (
-
-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
+tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+tcInstType ty
+ = case splitForAllTys ty of
+ ([], rho) -> -- There may be overloading but no type variables;
+ -- (?x :: Int) => Int -> Int
+ tcSplitRhoTy rho `thenNF_Tc` \ (theta, tau) ->
+ returnNF_Tc ([], theta, tau)
+
+ (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
+ tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) ->
+ returnNF_Tc (tyvars', theta, tau)
+\end{code}
- do env (ForAllTy (TyVar uniq kind name _) ty) = panic "tcInstTcType"
- -- 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 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
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
-~~~~~~~
-@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
-
-zonkTcType :: TcType s -> NF_TcM s (TcType s)
-zonkTcType ty = zonk (\tyvar -> tyvar) ty
-
-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)
-
-zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
-zonkTcTyVarToTyVar tyvar
- = zonk_tv_to_tv tcTyVarToTyVar tyvar
-
+%************************************************************************
+%* *
+\subsection{Zonking -- the exernal interfaces}
+%* *
+%************************************************************************
-zonk tyvar_fn (TyVarTy tyvar)
- = zonk_tv tyvar_fn tyvar
+----------------- Type variables
-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')
-
-zonk tyvar_fn (TyConTy tc u)
- = returnNF_Tc (TyConTy tc u)
-
-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')
-
-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}
+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}
-zonk tyvar_fn (ForAllUsageTy uv uvs ty)
- = panic "zonk:ForAllUsageTy"
+----------------- Types
-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)
+\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
+
+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 (ClassP c ts) =
+ zonkTcTypes ts `thenNF_Tc` \ new_ts ->
+ returnNF_Tc (ClassP c new_ts)
+zonkTcPredType (IParam n t) =
+ zonkTcType t `thenNF_Tc` \ new_t ->
+ returnNF_Tc (IParam n new_t)
+\end{code}
-zonk tyvar_fn (DictTy c ty u)
- = zonk tyvar_fn ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (DictTy c ty' u)
+------------------- 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}
-zonk_tv tyvar_fn tyvar
- = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- BoundTo ty -> zonk tyvar_fn ty
- other -> returnNF_Tc (TyVarTy (tyvar_fn tyvar))
+%************************************************************************
+%* *
+\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
+%* *
+%* For internal use only! *
+%* *
+%************************************************************************
-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}
+-- 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 (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
+ returnNF_Tc (ClassP 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}
+
projects / ghc-hetmet.git / blobdiff