-\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(TcIdBndr), TcIdOcc(..),
-
- -----------------------------------------
- SYN_IE(TcTyVar),
- SYN_IE(TcTyVarSet),
- newTcTyVar,
- newTyVarTy, -- Kind -> NF_TcM s (TcType s)
- newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
+
+ TcTyVar,
+ TcTyVarSet,
+ newTyVar,
+ newTyVarTy, -- Kind -> NF_TcM s TcType
+ newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType]
+
+ newTyVarTy_OpenKind, -- NF_TcM s TcType
+ newOpenTypeKind, -- NF_TcM s TcKind
-----------------------------------------
- SYN_IE(TcType), TcMaybe(..),
- SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(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
- tcSplitForAllTy, tcSplitRhoTy,
+ tcSplitRhoTy,
tcInstTyVars,
- tcInstSigTyVars,
- tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
- tcInstTheta, tcInstId,
+ tcInstSigVar,
+ tcInstTcType,
- zonkTcTyVars,
- zonkTcType,
- zonkTcTypeToType,
- zonkTcTyVar,
- zonkTcTyVarToTyVar
+ typeToTcType,
+
+ tcTypeKind, -- :: TcType -> NF_TcM s TcKind
+ --------------------------------
+ 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, isTyVarTy,
- mkForAllTys, instantiateTy
- )
-import TyVar ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet),
- SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv,
- nullTyVarEnv, mkTyVarEnv,
- tyVarSetToList
- )
-import PprType ( GenType, GenTyVar ) -- Instances only
+import PprType ( pprType )
+import Type ( Type(..), Kind, ThetaType, TyNote(..),
+ mkAppTy, mkTyConApp,
+ splitDictTy_maybe, splitForAllTys, isNotUsgTy,
+ isTyVarTy, mkTyVarTy, mkTyVarTys,
+ typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
+ )
+import Subst ( Subst, mkTopTyVarSubst, substTy )
+import TyCon ( tyConKind, mkPrimTyCon )
+import PrimRep ( PrimRep(VoidRep) )
+import VarEnv
+import VarSet ( emptyVarSet )
+import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
-- others:
-import Class ( GenClass, SYN_IE(Class) )
-import TyCon ( isFunTyCon )
-import Id ( idType, GenId, SYN_IE(Id) )
-import Kind ( Kind )
-import TcKind ( TcKind )
import TcMonad
-import Usage ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
-
-import TysPrim ( voidTy )
-
-IMP_Ubiq()
-import Name ( NamedThing(..) )
-import Unique ( Unique )
-import UniqFM ( UniqFM )
-import Maybes ( assocMaybe )
-import Outputable ( Outputable(..) )
-import Util ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
+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 TcIdBndr s = GenId (TcType s) -- Binders are all TcTypes
-data TcIdOcc s = TcId (TcIdBndr s) -- Bindees may be either
- | RealId Id
-
-instance Eq (TcIdOcc s) where
- (TcId id1) == (TcId id2) = id1 == id2
- (RealId id1) == (RealId id2) = id1 == id2
- _ == _ = False
-
-instance Outputable (TcIdOcc s) where
- ppr sty (TcId id) = ppr sty id
- ppr sty (RealId id) = ppr sty id
-
-instance NamedThing (TcIdOcc s) where
- getName (TcId id) = getName id
- getName (RealId id) = getName id
-\end{code}
-
-
-\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)
-\end{code}
+typeToTcType :: Type -> TcType
+typeToTcType ty = ty
-\begin{code}
-tcTyVarToTyVar :: TcTyVar s -> TyVar
-tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
+kindToTcKind :: Kind -> TcKind
+kindToTcKind kind = kind
\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 ([(Class,TcType s)], TcType s)
+tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType)
tcSplitRhoTy t
= go t t []
where
- go syn_t (FunTy (DictTy c t _) r _) ts = go r r ((c,t):ts)
- go syn_t (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
- | isFunTyCon tycon
- = go r r ((c,t):ts)
- go syn_t (SynTy _ _ 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)
+ -- 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 :: Kind -> NF_TcM s (TcTyVar s)
-newTcTyVar kind
+newTyVar :: Kind -> NF_TcM s 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 s 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 s [TcType]
newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
+newKindVar :: NF_TcM s TcKind
+newKindVar
+ = tcGetUnique `thenNF_Tc` \ uniq ->
+ tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
+ returnNF_Tc (TyVarTy kv)
+
+newKindVars :: Int -> NF_TcM s [TcKind]
+newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
+
+-- 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
+
+newOpenTypeKind :: NF_TcM s TcKind
+newOpenTypeKind = newTyVarTy superBoxity `thenNF_Tc` \ bv ->
+ returnNF_Tc (mkTyConApp typeCon [bv])
+\end{code}
+
--- For signature type variables, mark them as "DontBind"
-tcInstTyVars, tcInstSigTyVars
- :: [GenTyVar flexi]
- -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
+%************************************************************************
+%* *
+\subsection{Type instantiation}
+%* *
+%************************************************************************
-tcInstTyVars tyvars = inst_tyvars UnBound tyvars
-tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
+Instantiating a bunch of type variables
-inst_tyvars initial_cts tyvars
- = mapNF_Tc (inst_tyvar initial_cts) tyvars `thenNF_Tc` \ tc_tyvars ->
+\begin{code}
+tcInstTyVars :: [TyVar]
+ -> NF_TcM s ([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, zipEqual "inst_tyvars" tyvars 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 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)"
-\end{code}
+ 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' ->
-@tcInstType@ and @tcInstSigType@ both create a fresh instance of a
-type, returning a @TcType@. All inner for-alls are instantiated with
-fresh TcTyVars.
+ tcNewMutTyVar name kind'
-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.
+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}
-On the other hand, @tcInstTcType@ instantiates a TcType. It uses
-instantiateTy which could take advantage of sharing some day.
+@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
+fresh type variables, returning them and the instantiated body of the for-all.
\begin{code}
-tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
+tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
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 :: [(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" --(vcat [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"-- (vcat [ppr PprDebug ty_to_inst,
- -- ppr PprDebug tyvar])
+ = case splitForAllTys ty of
+ ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
+ (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
+ returnNF_Tc (tyvars', substTy tenv rho)
+\end{code}
-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 PprDebug tv, ppr PprDebug tv_ty]) $
- returnNF_Tc (tcTyVarToTyVar tv)
+%************************************************************************
+%* *
+\subsection{Putting and getting mutable type variables}
+%* *
+%************************************************************************
+\begin{code}
+tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
+tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
+\end{code}
-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
+Putting is easy:
- lookup env tyvar = case lookupTyVarEnv env tyvar of
- Just ty -> returnNF_Tc ty
- Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
+\begin{code}
+tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
+ returnNF_Tc ty
+\end{code}
+Getting is more interesting. The easy thing to do is just to read, thus:
-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)
+\begin{verbatim}
+tcGetTyVar tyvar = tcReadMutTyVar tyvar
+\end{verbatim}
- 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')
+But it's more fun to short out indirections on the way: If this
+version returns a TyVar, then that TyVar is unbound. If it returns
+any other type, then there might be bound TyVars embedded inside it.
- doo env (FunTy arg res usage) = doo env arg `thenNF_Tc` \ arg' ->
- doo env res `thenNF_Tc` \ res' ->
- returnNF_Tc (FunTy arg' res' usage)
+We return Nothing iff the original box was unbound.
- doo env (AppTy fun arg) = doo env fun `thenNF_Tc` \ fun' ->
- doo env arg `thenNF_Tc` \ arg' ->
- returnNF_Tc (AppTy fun' arg')
+\begin{code}
+tcGetTyVar tyvar
+ = ASSERT2( isMutTyVar tyvar, ppr tyvar )
+ tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ case maybe_ty of
+ Just ty -> short_out ty `thenNF_Tc` \ ty' ->
+ tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
+ returnNF_Tc (Just ty')
- doo env (DictTy clas ty usage)= doo env ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (DictTy clas ty' usage)
+ Nothing -> returnNF_Tc Nothing
- doo env (ForAllUsageTy u us ty) = doo env ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (ForAllUsageTy u us ty')
+short_out :: TcType -> NF_TcM s TcType
+short_out ty@(TyVarTy tyvar)
+ | not (isMutTyVar tyvar)
+ = returnNF_Tc 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')
+ | otherwise
+ = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ case maybe_ty of
+ Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
+ tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
+ returnNF_Tc ty'
+ other -> returnNF_Tc ty
-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) --
-
-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')
+short_out other_ty = returnNF_Tc other_ty
\end{code}
-Reading and writing TcTyVars
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+%************************************************************************
+%* *
+\subsection{Zonking -- the exernal interfaces}
+%* *
+%************************************************************************
+
+----------------- Type variables
+
\begin{code}
-tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
-tcReadTyVar :: TcTyVar s -> NF_TcM s (TcMaybe s)
+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}
-Writing is easy:
+----------------- Types
\begin{code}
-tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
+zonkTcType :: TcType -> NF_TcM s TcType
+zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
+
+zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
+zonkTcTypes tys = mapNF_Tc zonkTcType tys
+
+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)
+
+zonkTcKind :: TcKind -> NF_TcM s TcKind
+zonkTcKind = zonkTcType
\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
-\end{verbatim}
+------------------- These ...ToType, ...ToKind versions
+ are used at the end of type checking
-But it's more fun to short out indirections on the way: If this
-version returns a TyVar, then that TyVar is unbound. If it returns
-any other type, then there might be bound TyVars embedded inside it.
+\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}
-We return Nothing iff the original box was unbound.
+
+%************************************************************************
+%* *
+\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
+%* *
+%* For internal use only! *
+%* *
+%************************************************************************
\begin{code}
-tcReadTyVar (TyVar uniq kind name box)
- = tcReadMutVar box `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')
+-- 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')
- other -> returnNF_Tc other
+ go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
+ go ty2 `thenNF_Tc` \ ty2' ->
+ returnNF_Tc (NoteTy (SynNote ty1') ty2')
-short_out :: TcType s -> NF_TcM s (TcType s)
-short_out ty@(TyVarTy (TyVar uniq kind name box))
- = tcReadMutVar box `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'
+ go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
- other -> returnNF_Tc ty
+ go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
+ returnNF_Tc (NoteTy (UsgNote usg) ty2')
-short_out other_ty = returnNF_Tc other_ty
+ 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}
+%* *
+%************************************************************************
+
+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.
-Zonking
-~~~~~~~
\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)
-
-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 (AppTy ty1' ty2')
-
-zonkTcType (TyConTy tc u)
- = returnNF_Tc (TyConTy tc u)
-
-zonkTcType (SynTy tc tys ty)
- = mapNF_Tc zonkTcType tys `thenNF_Tc` \ tys' ->
- zonkTcType ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (SynTy tc tys' ty')
-
-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:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
-
- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
-
-zonkTcType (ForAllUsageTy uv uvs ty)
- = panic "zonk:ForAllUsageTy"
-
-zonkTcType (FunTy ty1 ty2 u)
- = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
- zonkTcType ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (FunTy ty1' ty2' u)
-
-zonkTcType (DictTy c ty u)
- = zonkTcType ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (DictTy c ty' u)
+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}
projects / ghc-hetmet.git / blobdiff