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, TcClassContext,
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,
37 zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
41 #include "HsVersions.h"
45 import TypeRep ( Type(..), Kind, TyNote(..) ) -- friend
46 import Type ( PredType(..),
47 getTyVar, mkAppTy, mkUTy,
48 splitPredTy_maybe, splitForAllTys,
49 isTyVarTy, mkTyVarTy, mkTyVarTys,
50 openTypeKind, liftedTypeKind,
51 superKind, superBoxity, tyVarsOfTypes,
52 defaultKind, liftedBoxity
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 mkLocalName, mkDerivedTyConOcc
66 import Unique ( Uniquable(..) )
67 import SrcLoc ( noSrcLoc )
68 import Util ( nOfThem )
75 These tcSplit functions are like their non-Tc analogues, but they
76 follow through bound type variables.
78 No need for tcSplitForAllTy because a type variable can't be instantiated
82 tcSplitRhoTy :: TcType -> NF_TcM (TcThetaType, TcType)
86 -- A type variable is never instantiated to a dictionary type,
87 -- so we don't need to do a tcReadVar on the "arg".
88 go syn_t (FunTy arg res) ts = case splitPredTy_maybe arg of
89 Just pair -> go res res (pair:ts)
90 Nothing -> returnNF_Tc (reverse ts, syn_t)
91 go syn_t (NoteTy _ t) ts = go syn_t t ts
92 go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
94 Just ty | not (isTyVarTy ty) -> go syn_t ty ts
95 other -> returnNF_Tc (reverse ts, syn_t)
96 go syn_t (UsageTy _ t) ts = go syn_t t ts
97 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
101 %************************************************************************
103 \subsection{New type variables}
105 %************************************************************************
108 newTyVar :: Kind -> NF_TcM TcTyVar
110 = tcGetUnique `thenNF_Tc` \ uniq ->
111 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
113 newTyVarTy :: Kind -> NF_TcM TcType
115 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
116 returnNF_Tc (TyVarTy tc_tyvar)
118 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
119 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
121 newKindVar :: NF_TcM TcKind
123 = tcGetUnique `thenNF_Tc` \ uniq ->
124 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
125 returnNF_Tc (TyVarTy kv)
127 newKindVars :: Int -> NF_TcM [TcKind]
128 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
130 newBoxityVar :: NF_TcM TcKind
132 = tcGetUnique `thenNF_Tc` \ uniq ->
133 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
134 returnNF_Tc (TyVarTy kv)
138 %************************************************************************
140 \subsection{Type instantiation}
142 %************************************************************************
144 Instantiating a bunch of type variables
147 tcInstTyVars :: [TyVar]
148 -> NF_TcM ([TcTyVar], [TcType], Subst)
151 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
153 tys = mkTyVarTys tc_tyvars
155 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
156 -- Since the tyvars are freshly made,
157 -- they cannot possibly be captured by
158 -- any existing for-alls. Hence mkTopTyVarSubst
161 = tcGetUnique `thenNF_Tc` \ uniq ->
163 name = setNameUnique (tyVarName tyvar) uniq
164 -- Note that we don't change the print-name
165 -- This won't confuse the type checker but there's a chance
166 -- that two different tyvars will print the same way
167 -- in an error message. -dppr-debug will show up the difference
168 -- Better watch out for this. If worst comes to worst, just
169 -- use mkSysLocalName.
171 tcNewMutTyVar name (tyVarKind tyvar)
173 tcInstSigVar tyvar -- Very similar to tcInstTyVar
174 = tcGetUnique `thenNF_Tc` \ uniq ->
176 name = setNameUnique (tyVarName tyvar) uniq
177 kind = tyVarKind tyvar
179 ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
180 tcNewSigTyVar name kind
183 @tcInstType@ instantiates the outer-level for-alls of a TcType with
184 fresh type variables, splits off the dictionary part, and returns the results.
187 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
189 = case splitForAllTys ty of
190 ([], _) -> returnNF_Tc ([], [], ty) -- Nothing to do
191 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
192 tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) ->
193 returnNF_Tc (tyvars', theta, tau)
198 %************************************************************************
200 \subsection{Putting and getting mutable type variables}
202 %************************************************************************
205 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
206 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
213 | not (isMutTyVar tyvar)
214 = pprTrace "tcPutTyVar" (ppr tyvar) $
218 = ASSERT( isMutTyVar tyvar )
219 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
220 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
224 Getting is more interesting. The easy thing to do is just to read, thus:
227 tcGetTyVar tyvar = tcReadMutTyVar tyvar
230 But it's more fun to short out indirections on the way: If this
231 version returns a TyVar, then that TyVar is unbound. If it returns
232 any other type, then there might be bound TyVars embedded inside it.
234 We return Nothing iff the original box was unbound.
238 | not (isMutTyVar tyvar)
239 = pprTrace "tcGetTyVar" (ppr tyvar) $
240 returnNF_Tc (Just (mkTyVarTy tyvar))
243 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
244 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
246 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
247 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
248 returnNF_Tc (Just ty')
250 Nothing -> returnNF_Tc Nothing
252 short_out :: TcType -> NF_TcM TcType
253 short_out ty@(TyVarTy tyvar)
254 | not (isMutTyVar tyvar)
258 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
260 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
261 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
264 other -> returnNF_Tc ty
266 short_out other_ty = returnNF_Tc other_ty
270 %************************************************************************
272 \subsection{Zonking -- the exernal interfaces}
274 %************************************************************************
276 ----------------- Type variables
279 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
280 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
282 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
283 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
284 returnNF_Tc (tyVarsOfTypes tys)
286 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
287 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
289 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
290 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
291 -- Usually this job is done by checkSigTyVars, but in a couple of places
292 -- that is overkill, so we use this simpler chap
293 zonkTcSigTyVars tyvars
294 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
295 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
298 ----------------- Types
301 zonkTcType :: TcType -> NF_TcM TcType
302 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
304 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
305 zonkTcTypes tys = mapNF_Tc zonkTcType tys
307 zonkTcClassConstraints cts = mapNF_Tc zonk cts
308 where zonk (clas, tys)
309 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
310 returnNF_Tc (clas, new_tys)
312 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
313 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
315 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
316 zonkTcPredType (Class c ts) =
317 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
318 returnNF_Tc (Class c new_ts)
319 zonkTcPredType (IParam n t) =
320 zonkTcType t `thenNF_Tc` \ new_t ->
321 returnNF_Tc (IParam n new_t)
324 ------------------- These ...ToType, ...ToKind versions
325 are used at the end of type checking
328 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
330 = mapNF_Tc zonk_it pairs
332 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
333 returnNF_Tc (name, kind)
335 -- When zonking a kind, we want to
336 -- zonk a *kind* variable to (Type *)
337 -- zonk a *boxity* variable to *
338 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv liftedTypeKind
339 | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
340 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
342 zonkTcTypeToType :: TcType -> NF_TcM Type
343 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
345 -- Zonk a mutable but unbound type variable to
346 -- Void if it has kind Lifted
348 zonk_unbound_tyvar tv
349 | kind == liftedTypeKind
350 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
351 -- this vastly common case
353 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
357 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
358 -- type variable tv. Same name too, apart from
359 -- making it start with a colon (sigh)
360 -- I dread to think what will happen if this gets out into an
361 -- interface file. Catastrophe likely. Major sigh.
362 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
363 mkPrimTyCon tc_name kind 0 [] VoidRep
365 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
367 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
368 -- of a type variable, at the *end* of type checking. It changes
369 -- the *mutable* type variable into an *immutable* one.
371 -- It does this by making an immutable version of tv and binds tv to it.
372 -- Now any bound occurences of the original type variable will get
373 -- zonked to the immutable version.
375 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
376 zonkTcTyVarToTyVar tv
378 -- Make an immutable version, defaulting
379 -- the kind to lifted if necessary
380 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
381 immut_tv_ty = mkTyVarTy immut_tv
383 zap tv = tcPutTyVar tv immut_tv_ty
384 -- Bind the mutable version to the immutable one
386 -- If the type variable is mutable, then bind it to immut_tv_ty
387 -- so that all other occurrences of the tyvar will get zapped too
388 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
390 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
396 %************************************************************************
398 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
400 %* For internal use only! *
402 %************************************************************************
405 -- zonkType is used for Kinds as well
407 -- For unbound, mutable tyvars, zonkType uses the function given to it
408 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
409 -- type variable and zonks the kind too
411 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
412 -- see zonkTcType, and zonkTcTypeToType
415 zonkType unbound_var_fn ty
418 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
419 returnNF_Tc (TyConApp tycon tys')
421 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
422 go ty2 `thenNF_Tc` \ ty2' ->
423 returnNF_Tc (NoteTy (SynNote ty1') ty2')
425 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
427 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
428 returnNF_Tc (PredTy p')
430 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
431 go res `thenNF_Tc` \ res' ->
432 returnNF_Tc (FunTy arg' res')
434 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
435 go arg `thenNF_Tc` \ arg' ->
436 returnNF_Tc (mkAppTy fun' arg')
438 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
439 go ty `thenNF_Tc` \ ty' ->
440 returnNF_Tc (mkUTy u' ty')
442 -- The two interesting cases!
443 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
445 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
446 go ty `thenNF_Tc` \ ty' ->
447 returnNF_Tc (ForAllTy tyvar' ty')
449 go_pred (Class c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
450 returnNF_Tc (Class c tys')
451 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
452 returnNF_Tc (IParam n ty')
454 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
455 -> TcTyVar -> NF_TcM TcType
456 zonkTyVar unbound_var_fn tyvar
457 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
458 -- zonking a forall type, when the bound type variable
459 -- needn't be mutable
460 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
461 returnNF_Tc (TyVarTy tyvar)
464 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
466 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
467 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound