newTyVarTy, -- Kind -> NF_TcM s TcType
newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType]
- newTyVarTy_OpenKind, -- NF_TcM s TcType
- newOpenTypeKind, -- NF_TcM s TcKind
-
-----------------------------------------
TcType, TcTauType, TcThetaType, TcRhoType,
tcSplitRhoTy,
tcInstTyVars,
+ tcInstSigVar,
tcInstTcType,
- typeToTcType,
-
- tcTypeKind, -- :: TcType -> NF_TcM s TcKind
--------------------------------
TcKind,
- newKindVar, newKindVars,
- kindToTcKind,
- zonkTcKind,
+ newKindVar, newKindVars, newBoxityVar,
--------------------------------
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
- zonkTcType, zonkTcTypes, zonkTcThetaType,
+ zonkTcTyVar, zonkTcTyVars, zonkTcSigTyVars,
+ zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcTypeToType, zonkTcTyVarToTyVar,
- zonkTcKindToKind
+ zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
) where
-- friends:
-import PprType ( pprType )
-import Type ( Type(..), Kind, ThetaType, TyNote(..),
- mkAppTy, mkTyConApp,
- splitDictTy_maybe, splitForAllTys,
+import TypeRep ( Type(..), Kind, TyNote(..) ) -- friend
+import Type ( ThetaType, PredType(..),
+ getTyVar, mkAppTy, mkTyConApp, mkPredTy,
+ splitPredTy_maybe, splitForAllTys, isNotUsgTy,
isTyVarTy, mkTyVarTy, mkTyVarTys,
- fullSubstTy, substTopTy,
- typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
+ openTypeKind, boxedTypeKind,
+ superKind, superBoxity,
+ defaultKind, boxedBoxity
)
-import TyCon ( tyConKind )
-import VarEnv
-import VarSet ( emptyVarSet )
+import Subst ( Subst, mkTopTyVarSubst, substTy )
+import TyCon ( tyConKind, mkPrimTyCon )
+import PrimRep ( PrimRep(VoidRep) )
import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
-- others:
-import TcMonad
+import TcMonad -- TcType, amongst others
import TysWiredIn ( voidTy )
-import Name ( NamedThing(..), setNameUnique, mkSysLocalName )
-import Unique ( Unique )
+import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
+ mkDerivedName, mkDerivedTyConOcc
+ )
+import Unique ( Unique, Uniquable(..) )
import Util ( nOfThem )
import Outputable
\end{code}
-
-Coercions
-~~~~~~~~~~
-Type definitions are in TcMonad.lhs
-
-\begin{code}
-typeToTcType :: Type -> TcType
-typeToTcType ty = ty
-
-kindToTcKind :: Kind -> TcKind
-kindToTcKind kind = kind
-\end{code}
-
Utility functions
~~~~~~~~~~~~~~~~~
These tcSplit functions are like their non-Tc analogues, but they
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 (NoteTy _ t) ts = go syn_t t ts
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])
+newBoxityVar :: NF_TcM s TcKind
+newBoxityVar
+ = tcGetUnique `thenNF_Tc` \ uniq ->
+ tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
+ returnNF_Tc (TyVarTy kv)
\end{code}
\begin{code}
tcInstTyVars :: [TyVar]
- -> NF_TcM s ([TcTyVar], [TcType], TyVarEnv TcType)
+ -> NF_TcM s ([TcTyVar], [TcType], Subst)
tcInstTyVars tyvars
- = mapNF_Tc inst_tyvar tyvars `thenNF_Tc` \ tc_tyvars ->
+ = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
let
tys = mkTyVarTys tc_tyvars
in
- returnNF_Tc (tc_tyvars, tys, zipVarEnv 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 tyvar -- Could use the name from the tyvar?
+tcInstTyVar tyvar
= tcGetUnique `thenNF_Tc` \ uniq ->
let
- kind = tyVarKind tyvar
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
-- Better watch out for this. If worst comes to worst, just
-- use mkSysLocalName.
in
- tcNewMutTyVar name kind
+ tcNewMutTyVar name (tyVarKind tyvar)
+
+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}
@tcInstTcType@ instantiates the outer-level for-alls of a TcType with
= case splitForAllTys ty of
([], _) -> returnNF_Tc ([], ty) -- Nothing to do
(tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
- returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
- -- Since the tyvars are freshly made,
- -- they cannot possibly be captured by
- -- any existing for-alls. Hence emptyVarSet
+ returnNF_Tc (tyvars', substTy tenv rho)
\end{code}
zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
-zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
-zonkTcTyVarBndr tyvar
- = zonkTcTyVar tyvar `thenNF_Tc` \ (TyVarTy tyvar') ->
- returnNF_Tc tyvar'
-
zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+
+zonkTcSigTyVars :: [TcTyVar] -> NF_TcM s [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] -> 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)
+zonkTcClassConstraints cts = mapNF_Tc zonk cts
+ where zonk (clas, tys)
+ = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
+ returnNF_Tc (clas, new_tys)
-zonkTcKind :: TcKind -> NF_TcM s TcKind
-zonkTcKind = zonkTcType
+zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
+zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
+
+zonkTcPredType :: TcPredType -> NF_TcM s 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}
-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
+zonkKindEnv :: [(Name, TcKind)] -> NF_TcM s [(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 boxedTypeKind
+ | tyVarKind kv == superBoxity = tcPutTyVar kv boxedBoxity
+ | otherwise = pprPanic "zonkKindEnv" (ppr 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
+ -- Void if it has kind Boxed
+ -- :Void 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) [])
-
- mk_void_tycon tv -- Make a new TyCon with the same kind as the
- -- type variable tv. Same name too, apart from
- -- making it start with a capital letter (sigh)
- -- I can't quite bring myself to write the Name-fiddling
- -- code yet. ToDo. SLPJ Nov 98
- = pprPanic "zonkTcTypeToType: free type variable with non-* type:" (ppr tv)
+ | kind == boxedTypeKind
+ = 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)
+ = 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.
+-- 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 s TyVar
zonkTcTyVarToTyVar tv
- = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
- let
- -- Make an immutable version
- immut_tv = mkTyVar (tyVarName tv) kind
+ = let
+ -- Make an immutable version, defaulting
+ -- the kind to boxed if necessary
+ immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
immut_tv_ty = mkTyVarTy immut_tv
zap tv = tcPutTyVar tv immut_tv_ty
-- 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 )
+
+ WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
returnNF_Tc immut_tv
\end{code}
go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
+ go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
+ returnNF_Tc (NoteTy (UsgNote usg) ty2')
+
+ go (NoteTy (UsgForAll uv) ty2)= go ty2 `thenNF_Tc` \ ty2' ->
+ returnNF_Tc (NoteTy (UsgForAll uv) ty2')
+
+ 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')
returnNF_Tc (mkAppTy fun' arg')
-- The two interesting cases!
- go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
+ 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 (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 s Type) -- What to do for an unbound mutable variable
-> TcTyVar -> NF_TcM s TcType
= 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
+ 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.
-
-\begin{code}
-tcTypeKind :: TcType -> NF_TcM s TcKind
-
-tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar)
-tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
-tcTypeKind (NoteTy _ ty) = tcTypeKind ty
-tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind ->
- tcFunResultTy fun_kind
-tcTypeKind (FunTy fun arg) = tcTypeKindF arg
-tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty
-
-tcTypeKindF :: TcType -> NF_TcM s TcKind
-tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty
-tcTypeKindF (FunTy _ ty) = tcTypeKindF ty
-tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
-tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind ->
- fix_up kind
- where
- fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
- -- Functions at the type level are always boxed
- fix_up (NoteTy _ kind) = fix_up kind
- fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just kind' -> fix_up kind'
- Nothing -> returnNF_Tc kind
- fix_up kind = returnNF_Tc kind
-
-tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty
-tcFunResultTy (FunTy arg res) = returnNF_Tc res
-tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> tcFunResultTy ty'
- -- The Nothing case, and the other cases for tcFunResultTy
- -- should never happen... pattern match failure
-\end{code}