2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
12 newTyVarTy, -- Kind -> NF_TcM TcType
13 newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
15 -----------------------------------------
16 TcType, TcTauType, TcThetaType, TcRhoType,
18 -- Find the type to which a type variable is bound
19 tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType
20 tcGetTyVar, -- :: TcTyVar -> NF_TcM (Maybe TcType) does shorting out
29 --------------------------------
31 newKindVar, newKindVars, newBoxityVar,
33 --------------------------------
34 zonkTcTyVar, zonkTcTyVars, zonkTcSigTyVars,
35 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
37 zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
41 #include "HsVersions.h"
45 import TypeRep ( Type(..), Kind, TyNote(..) ) -- friend
46 import Type ( PredType(..),
48 splitPredTy_maybe, splitForAllTys, isNotUsgTy,
49 isTyVarTy, mkTyVarTy, mkTyVarTys,
50 openTypeKind, boxedTypeKind,
51 superKind, superBoxity,
52 defaultKind, boxedBoxity
54 import Subst ( Subst, mkTopTyVarSubst, substTy )
55 import TyCon ( mkPrimTyCon )
56 import PrimRep ( PrimRep(VoidRep) )
57 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
60 import TcMonad -- TcType, amongst others
61 import TysWiredIn ( voidTy )
63 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
64 mkDerivedName, mkDerivedTyConOcc
66 import Unique ( Uniquable(..) )
67 import Util ( nOfThem )
74 These tcSplit functions are like their non-Tc analogues, but they
75 follow through bound type variables.
77 No need for tcSplitForAllTy because a type variable can't be instantiated
81 tcSplitRhoTy :: TcType -> NF_TcM (TcThetaType, TcType)
85 -- A type variable is never instantiated to a dictionary type,
86 -- so we don't need to do a tcReadVar on the "arg".
87 go syn_t (FunTy arg res) ts = case splitPredTy_maybe arg of
88 Just pair -> go res res (pair:ts)
89 Nothing -> returnNF_Tc (reverse ts, syn_t)
90 go syn_t (NoteTy _ t) ts = go syn_t t ts
91 go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
93 Just ty | not (isTyVarTy ty) -> go syn_t ty ts
94 other -> returnNF_Tc (reverse ts, syn_t)
95 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
99 %************************************************************************
101 \subsection{New type variables}
103 %************************************************************************
106 newTyVar :: Kind -> NF_TcM TcTyVar
108 = tcGetUnique `thenNF_Tc` \ uniq ->
109 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
111 newTyVarTy :: Kind -> NF_TcM TcType
113 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
114 returnNF_Tc (TyVarTy tc_tyvar)
116 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
117 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
119 newKindVar :: NF_TcM TcKind
121 = tcGetUnique `thenNF_Tc` \ uniq ->
122 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
123 returnNF_Tc (TyVarTy kv)
125 newKindVars :: Int -> NF_TcM [TcKind]
126 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
128 newBoxityVar :: NF_TcM TcKind
130 = tcGetUnique `thenNF_Tc` \ uniq ->
131 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
132 returnNF_Tc (TyVarTy kv)
136 %************************************************************************
138 \subsection{Type instantiation}
140 %************************************************************************
142 Instantiating a bunch of type variables
145 tcInstTyVars :: [TyVar]
146 -> NF_TcM ([TcTyVar], [TcType], Subst)
149 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
151 tys = mkTyVarTys tc_tyvars
153 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
154 -- Since the tyvars are freshly made,
155 -- they cannot possibly be captured by
156 -- any existing for-alls. Hence mkTopTyVarSubst
159 = tcGetUnique `thenNF_Tc` \ uniq ->
161 name = setNameUnique (tyVarName tyvar) uniq
162 -- Note that we don't change the print-name
163 -- This won't confuse the type checker but there's a chance
164 -- that two different tyvars will print the same way
165 -- in an error message. -dppr-debug will show up the difference
166 -- Better watch out for this. If worst comes to worst, just
167 -- use mkSysLocalName.
169 tcNewMutTyVar name (tyVarKind tyvar)
171 tcInstSigVar tyvar -- Very similar to tcInstTyVar
172 = tcGetUnique `thenNF_Tc` \ uniq ->
174 name = setNameUnique (tyVarName tyvar) uniq
175 kind = tyVarKind tyvar
177 ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
178 tcNewSigTyVar name kind
181 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
182 fresh type variables, returning them and the instantiated body of the for-all.
185 tcInstTcType :: TcType -> NF_TcM ([TcTyVar], TcType)
187 = case splitForAllTys ty of
188 ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
189 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
190 returnNF_Tc (tyvars', substTy tenv rho)
195 %************************************************************************
197 \subsection{Putting and getting mutable type variables}
199 %************************************************************************
202 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
203 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
209 tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
213 Getting is more interesting. The easy thing to do is just to read, thus:
216 tcGetTyVar tyvar = tcReadMutTyVar tyvar
219 But it's more fun to short out indirections on the way: If this
220 version returns a TyVar, then that TyVar is unbound. If it returns
221 any other type, then there might be bound TyVars embedded inside it.
223 We return Nothing iff the original box was unbound.
227 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
228 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
230 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
231 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
232 returnNF_Tc (Just ty')
234 Nothing -> returnNF_Tc Nothing
236 short_out :: TcType -> NF_TcM TcType
237 short_out ty@(TyVarTy tyvar)
238 | not (isMutTyVar tyvar)
242 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
244 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
245 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
248 other -> returnNF_Tc ty
250 short_out other_ty = returnNF_Tc other_ty
254 %************************************************************************
256 \subsection{Zonking -- the exernal interfaces}
258 %************************************************************************
260 ----------------- Type variables
263 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
264 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
266 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
267 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
269 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
270 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
271 -- Usually this job is done by checkSigTyVars, but in a couple of places
272 -- that is overkill, so we use this simpler chap
273 zonkTcSigTyVars tyvars
274 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
275 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
278 ----------------- Types
281 zonkTcType :: TcType -> NF_TcM TcType
282 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
284 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
285 zonkTcTypes tys = mapNF_Tc zonkTcType tys
287 zonkTcClassConstraints cts = mapNF_Tc zonk cts
288 where zonk (clas, tys)
289 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
290 returnNF_Tc (clas, new_tys)
292 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
293 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
295 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
296 zonkTcPredType (Class c ts) =
297 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
298 returnNF_Tc (Class c new_ts)
299 zonkTcPredType (IParam n t) =
300 zonkTcType t `thenNF_Tc` \ new_t ->
301 returnNF_Tc (IParam n new_t)
304 ------------------- These ...ToType, ...ToKind versions
305 are used at the end of type checking
308 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
310 = mapNF_Tc zonk_it pairs
312 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
313 returnNF_Tc (name, kind)
315 -- When zonking a kind, we want to
316 -- zonk a *kind* variable to (Type *)
317 -- zonk a *boxity* variable to *
318 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv boxedTypeKind
319 | tyVarKind kv == superBoxity = tcPutTyVar kv boxedBoxity
320 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
322 zonkTcTypeToType :: TcType -> NF_TcM Type
323 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
325 -- Zonk a mutable but unbound type variable to
326 -- Void if it has kind Boxed
328 zonk_unbound_tyvar tv
329 | kind == boxedTypeKind
330 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
331 -- this vastly common case
333 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
337 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
338 -- type variable tv. Same name too, apart from
339 -- making it start with a colon (sigh)
340 = mkPrimTyCon tc_name kind 0 [] VoidRep
342 tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
344 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
345 -- of a type variable, at the *end* of type checking. It changes
346 -- the *mutable* type variable into an *immutable* one.
348 -- It does this by making an immutable version of tv and binds tv to it.
349 -- Now any bound occurences of the original type variable will get
350 -- zonked to the immutable version.
352 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
353 zonkTcTyVarToTyVar tv
355 -- Make an immutable version, defaulting
356 -- the kind to boxed if necessary
357 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
358 immut_tv_ty = mkTyVarTy immut_tv
360 zap tv = tcPutTyVar tv immut_tv_ty
361 -- Bind the mutable version to the immutable one
363 -- If the type variable is mutable, then bind it to immut_tv_ty
364 -- so that all other occurrences of the tyvar will get zapped too
365 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
367 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
373 %************************************************************************
375 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
377 %* For internal use only! *
379 %************************************************************************
382 -- zonkType is used for Kinds as well
384 -- For unbound, mutable tyvars, zonkType uses the function given to it
385 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
386 -- type variable and zonks the kind too
388 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
389 -- see zonkTcType, and zonkTcTypeToType
392 zonkType unbound_var_fn ty
395 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
396 returnNF_Tc (TyConApp tycon tys')
398 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
399 go ty2 `thenNF_Tc` \ ty2' ->
400 returnNF_Tc (NoteTy (SynNote ty1') ty2')
402 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
404 go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
405 returnNF_Tc (NoteTy (UsgNote usg) ty2')
407 go (NoteTy (UsgForAll uv) ty2)= go ty2 `thenNF_Tc` \ ty2' ->
408 returnNF_Tc (NoteTy (UsgForAll uv) ty2')
410 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
411 returnNF_Tc (PredTy p')
413 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
414 go res `thenNF_Tc` \ res' ->
415 returnNF_Tc (FunTy arg' res')
417 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
418 go arg `thenNF_Tc` \ arg' ->
419 returnNF_Tc (mkAppTy fun' arg')
421 -- The two interesting cases!
422 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
424 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
425 go ty `thenNF_Tc` \ ty' ->
426 returnNF_Tc (ForAllTy tyvar' ty')
428 go_pred (Class c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
429 returnNF_Tc (Class c tys')
430 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
431 returnNF_Tc (IParam n ty')
433 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
434 -> TcTyVar -> NF_TcM TcType
435 zonkTyVar unbound_var_fn tyvar
436 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
437 -- zonking a forall type, when the bound type variable
438 -- needn't be mutable
439 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
440 returnNF_Tc (TyVarTy tyvar)
443 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
445 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
446 Just other_ty -> ASSERT( isNotUsgTy other_ty )
447 zonkType unbound_var_fn other_ty -- Bound