+
+------------------- 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 (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}
+