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
25 tcInstTyVar, tcInstTyVars,
29 --------------------------------
31 newKindVar, newKindVars, newBoxityVar,
33 --------------------------------
34 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
35 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
38 zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
42 #include "HsVersions.h"
46 import TypeRep ( Type(..), Kind, TyNote(..) ) -- friend
47 import Type ( PredType(..),
48 getTyVar, mkAppTy, mkUTy,
49 splitPredTy_maybe, splitForAllTys,
50 isTyVarTy, mkTyVarTy, mkTyVarTys,
51 openTypeKind, liftedTypeKind,
52 superKind, superBoxity, tyVarsOfTypes,
53 defaultKind, liftedBoxity
55 import Subst ( Subst, mkTopTyVarSubst, substTy )
56 import TyCon ( mkPrimTyCon )
57 import PrimRep ( PrimRep(VoidRep) )
58 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
61 import TcMonad -- TcType, amongst others
62 import TysWiredIn ( voidTy )
64 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
65 mkLocalName, mkDerivedTyConOcc
67 import Unique ( Uniquable(..) )
68 import SrcLoc ( noSrcLoc )
69 import Util ( nOfThem )
76 These tcSplit functions are like their non-Tc analogues, but they
77 follow through bound type variables.
79 No need for tcSplitForAllTy because a type variable can't be instantiated
83 tcSplitRhoTy :: TcType -> NF_TcM (TcThetaType, TcType)
87 -- A type variable is never instantiated to a dictionary type,
88 -- so we don't need to do a tcReadVar on the "arg".
89 go syn_t (FunTy arg res) ts = case splitPredTy_maybe arg of
90 Just pair -> go res res (pair:ts)
91 Nothing -> returnNF_Tc (reverse ts, syn_t)
92 go syn_t (NoteTy _ t) ts = go syn_t t ts
93 go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
95 Just ty | not (isTyVarTy ty) -> go syn_t ty ts
96 other -> returnNF_Tc (reverse ts, syn_t)
97 go syn_t (UsageTy _ t) ts = go syn_t t ts
98 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
102 %************************************************************************
104 \subsection{New type variables}
106 %************************************************************************
109 newTyVar :: Kind -> NF_TcM TcTyVar
111 = tcGetUnique `thenNF_Tc` \ uniq ->
112 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
114 newTyVarTy :: Kind -> NF_TcM TcType
116 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
117 returnNF_Tc (TyVarTy tc_tyvar)
119 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
120 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
122 newKindVar :: NF_TcM TcKind
124 = tcGetUnique `thenNF_Tc` \ uniq ->
125 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
126 returnNF_Tc (TyVarTy kv)
128 newKindVars :: Int -> NF_TcM [TcKind]
129 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
131 newBoxityVar :: NF_TcM TcKind
133 = tcGetUnique `thenNF_Tc` \ uniq ->
134 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
135 returnNF_Tc (TyVarTy kv)
139 %************************************************************************
141 \subsection{Type instantiation}
143 %************************************************************************
145 Instantiating a bunch of type variables
148 tcInstTyVars :: [TyVar]
149 -> NF_TcM ([TcTyVar], [TcType], Subst)
152 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
154 tys = mkTyVarTys tc_tyvars
156 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
157 -- Since the tyvars are freshly made,
158 -- they cannot possibly be captured by
159 -- any existing for-alls. Hence mkTopTyVarSubst
162 = tcGetUnique `thenNF_Tc` \ uniq ->
164 name = setNameUnique (tyVarName tyvar) uniq
165 -- Note that we don't change the print-name
166 -- This won't confuse the type checker but there's a chance
167 -- that two different tyvars will print the same way
168 -- in an error message. -dppr-debug will show up the difference
169 -- Better watch out for this. If worst comes to worst, just
170 -- use mkSysLocalName.
172 tcNewMutTyVar name (tyVarKind tyvar)
174 tcInstSigVar tyvar -- Very similar to tcInstTyVar
175 = tcGetUnique `thenNF_Tc` \ uniq ->
177 name = setNameUnique (tyVarName tyvar) uniq
178 kind = tyVarKind tyvar
180 ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
181 tcNewSigTyVar name kind
184 @tcInstType@ instantiates the outer-level for-alls of a TcType with
185 fresh type variables, splits off the dictionary part, and returns the results.
188 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
190 = case splitForAllTys ty of
191 ([], _) -> returnNF_Tc ([], [], ty) -- Nothing to do
192 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
193 tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) ->
194 returnNF_Tc (tyvars', theta, tau)
199 %************************************************************************
201 \subsection{Putting and getting mutable type variables}
203 %************************************************************************
206 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
207 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
214 | not (isMutTyVar tyvar)
215 = pprTrace "tcPutTyVar" (ppr tyvar) $
219 = ASSERT( isMutTyVar tyvar )
220 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
221 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
225 Getting is more interesting. The easy thing to do is just to read, thus:
228 tcGetTyVar tyvar = tcReadMutTyVar tyvar
231 But it's more fun to short out indirections on the way: If this
232 version returns a TyVar, then that TyVar is unbound. If it returns
233 any other type, then there might be bound TyVars embedded inside it.
235 We return Nothing iff the original box was unbound.
239 | not (isMutTyVar tyvar)
240 = pprTrace "tcGetTyVar" (ppr tyvar) $
241 returnNF_Tc (Just (mkTyVarTy tyvar))
244 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
245 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
247 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
248 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
249 returnNF_Tc (Just ty')
251 Nothing -> returnNF_Tc Nothing
253 short_out :: TcType -> NF_TcM TcType
254 short_out ty@(TyVarTy tyvar)
255 | not (isMutTyVar tyvar)
259 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
261 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
262 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
265 other -> returnNF_Tc ty
267 short_out other_ty = returnNF_Tc other_ty
271 %************************************************************************
273 \subsection{Zonking -- the exernal interfaces}
275 %************************************************************************
277 ----------------- Type variables
280 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
281 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
283 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
284 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
285 returnNF_Tc (tyVarsOfTypes tys)
287 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
288 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
290 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
291 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
292 -- Usually this job is done by checkSigTyVars, but in a couple of places
293 -- that is overkill, so we use this simpler chap
294 zonkTcSigTyVars tyvars
295 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
296 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
299 ----------------- Types
302 zonkTcType :: TcType -> NF_TcM TcType
303 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
305 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
306 zonkTcTypes tys = mapNF_Tc zonkTcType tys
308 zonkTcClassConstraints cts = mapNF_Tc zonk cts
309 where zonk (clas, tys)
310 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
311 returnNF_Tc (clas, new_tys)
313 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
314 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
316 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
317 zonkTcPredType (ClassP c ts) =
318 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
319 returnNF_Tc (ClassP c new_ts)
320 zonkTcPredType (IParam n t) =
321 zonkTcType t `thenNF_Tc` \ new_t ->
322 returnNF_Tc (IParam n new_t)
325 ------------------- These ...ToType, ...ToKind versions
326 are used at the end of type checking
329 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
331 = mapNF_Tc zonk_it pairs
333 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
334 returnNF_Tc (name, kind)
336 -- When zonking a kind, we want to
337 -- zonk a *kind* variable to (Type *)
338 -- zonk a *boxity* variable to *
339 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv liftedTypeKind
340 | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
341 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
343 zonkTcTypeToType :: TcType -> NF_TcM Type
344 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
346 -- Zonk a mutable but unbound type variable to
347 -- Void if it has kind Lifted
349 zonk_unbound_tyvar tv
350 | kind == liftedTypeKind || kind == openTypeKind
351 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
352 -- this vastly common case
354 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
358 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
359 -- type variable tv. Same name too, apart from
360 -- making it start with a colon (sigh)
361 -- I dread to think what will happen if this gets out into an
362 -- interface file. Catastrophe likely. Major sigh.
363 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
364 mkPrimTyCon tc_name kind 0 [] VoidRep
366 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
368 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
369 -- of a type variable, at the *end* of type checking. It changes
370 -- the *mutable* type variable into an *immutable* one.
372 -- It does this by making an immutable version of tv and binds tv to it.
373 -- Now any bound occurences of the original type variable will get
374 -- zonked to the immutable version.
376 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
377 zonkTcTyVarToTyVar tv
379 -- Make an immutable version, defaulting
380 -- the kind to lifted if necessary
381 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
382 immut_tv_ty = mkTyVarTy immut_tv
384 zap tv = tcPutTyVar tv immut_tv_ty
385 -- Bind the mutable version to the immutable one
387 -- If the type variable is mutable, then bind it to immut_tv_ty
388 -- so that all other occurrences of the tyvar will get zapped too
389 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
391 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
397 %************************************************************************
399 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
401 %* For internal use only! *
403 %************************************************************************
406 -- zonkType is used for Kinds as well
408 -- For unbound, mutable tyvars, zonkType uses the function given to it
409 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
410 -- type variable and zonks the kind too
412 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
413 -- see zonkTcType, and zonkTcTypeToType
416 zonkType unbound_var_fn ty
419 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
420 returnNF_Tc (TyConApp tycon tys')
422 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
423 go ty2 `thenNF_Tc` \ ty2' ->
424 returnNF_Tc (NoteTy (SynNote ty1') ty2')
426 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
428 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
429 returnNF_Tc (PredTy p')
431 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
432 go res `thenNF_Tc` \ res' ->
433 returnNF_Tc (FunTy arg' res')
435 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
436 go arg `thenNF_Tc` \ arg' ->
437 returnNF_Tc (mkAppTy fun' arg')
439 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
440 go ty `thenNF_Tc` \ ty' ->
441 returnNF_Tc (mkUTy u' ty')
443 -- The two interesting cases!
444 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
446 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
447 go ty `thenNF_Tc` \ ty' ->
448 returnNF_Tc (ForAllTy tyvar' ty')
450 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
451 returnNF_Tc (ClassP c tys')
452 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
453 returnNF_Tc (IParam n ty')
455 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
456 -> TcTyVar -> NF_TcM TcType
457 zonkTyVar unbound_var_fn tyvar
458 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
459 -- zonking a forall type, when the bound type variable
460 -- needn't be mutable
461 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
462 returnNF_Tc (TyVarTy tyvar)
465 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
467 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
468 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound