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 ([], rho) -> tcSplitRhoTy rho `thenNF_Tc` \ (theta, tau) ->
192 returnNF_Tc ([], theta, tau)
193 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
194 tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) ->
195 returnNF_Tc (tyvars', theta, tau)
200 %************************************************************************
202 \subsection{Putting and getting mutable type variables}
204 %************************************************************************
207 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
208 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
215 | not (isMutTyVar tyvar)
216 = pprTrace "tcPutTyVar" (ppr tyvar) $
220 = ASSERT( isMutTyVar tyvar )
221 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
222 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
226 Getting is more interesting. The easy thing to do is just to read, thus:
229 tcGetTyVar tyvar = tcReadMutTyVar tyvar
232 But it's more fun to short out indirections on the way: If this
233 version returns a TyVar, then that TyVar is unbound. If it returns
234 any other type, then there might be bound TyVars embedded inside it.
236 We return Nothing iff the original box was unbound.
240 | not (isMutTyVar tyvar)
241 = pprTrace "tcGetTyVar" (ppr tyvar) $
242 returnNF_Tc (Just (mkTyVarTy tyvar))
245 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
246 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
248 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
249 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
250 returnNF_Tc (Just ty')
252 Nothing -> returnNF_Tc Nothing
254 short_out :: TcType -> NF_TcM TcType
255 short_out ty@(TyVarTy tyvar)
256 | not (isMutTyVar tyvar)
260 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
262 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
263 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
266 other -> returnNF_Tc ty
268 short_out other_ty = returnNF_Tc other_ty
272 %************************************************************************
274 \subsection{Zonking -- the exernal interfaces}
276 %************************************************************************
278 ----------------- Type variables
281 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
282 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
284 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
285 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
286 returnNF_Tc (tyVarsOfTypes tys)
288 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
289 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
291 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
292 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
293 -- Usually this job is done by checkSigTyVars, but in a couple of places
294 -- that is overkill, so we use this simpler chap
295 zonkTcSigTyVars tyvars
296 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
297 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
300 ----------------- Types
303 zonkTcType :: TcType -> NF_TcM TcType
304 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
306 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
307 zonkTcTypes tys = mapNF_Tc zonkTcType tys
309 zonkTcClassConstraints cts = mapNF_Tc zonk cts
310 where zonk (clas, tys)
311 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
312 returnNF_Tc (clas, new_tys)
314 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
315 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
317 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
318 zonkTcPredType (ClassP c ts) =
319 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
320 returnNF_Tc (ClassP c new_ts)
321 zonkTcPredType (IParam n t) =
322 zonkTcType t `thenNF_Tc` \ new_t ->
323 returnNF_Tc (IParam n new_t)
326 ------------------- These ...ToType, ...ToKind versions
327 are used at the end of type checking
330 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
332 = mapNF_Tc zonk_it pairs
334 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
335 returnNF_Tc (name, kind)
337 -- When zonking a kind, we want to
338 -- zonk a *kind* variable to (Type *)
339 -- zonk a *boxity* variable to *
340 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv liftedTypeKind
341 | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
342 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
344 zonkTcTypeToType :: TcType -> NF_TcM Type
345 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
347 -- Zonk a mutable but unbound type variable to
348 -- Void if it has kind Lifted
350 zonk_unbound_tyvar tv
351 | kind == liftedTypeKind || kind == openTypeKind
352 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
353 -- this vastly common case
355 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
359 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
360 -- type variable tv. Same name too, apart from
361 -- making it start with a colon (sigh)
362 -- I dread to think what will happen if this gets out into an
363 -- interface file. Catastrophe likely. Major sigh.
364 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
365 mkPrimTyCon tc_name kind 0 [] VoidRep
367 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
369 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
370 -- of a type variable, at the *end* of type checking. It changes
371 -- the *mutable* type variable into an *immutable* one.
373 -- It does this by making an immutable version of tv and binds tv to it.
374 -- Now any bound occurences of the original type variable will get
375 -- zonked to the immutable version.
377 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
378 zonkTcTyVarToTyVar tv
380 -- Make an immutable version, defaulting
381 -- the kind to lifted if necessary
382 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
383 immut_tv_ty = mkTyVarTy immut_tv
385 zap tv = tcPutTyVar tv immut_tv_ty
386 -- Bind the mutable version to the immutable one
388 -- If the type variable is mutable, then bind it to immut_tv_ty
389 -- so that all other occurrences of the tyvar will get zapped too
390 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
392 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
398 %************************************************************************
400 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
402 %* For internal use only! *
404 %************************************************************************
407 -- zonkType is used for Kinds as well
409 -- For unbound, mutable tyvars, zonkType uses the function given to it
410 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
411 -- type variable and zonks the kind too
413 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
414 -- see zonkTcType, and zonkTcTypeToType
417 zonkType unbound_var_fn ty
420 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
421 returnNF_Tc (TyConApp tycon tys')
423 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
424 go ty2 `thenNF_Tc` \ ty2' ->
425 returnNF_Tc (NoteTy (SynNote ty1') ty2')
427 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
429 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
430 returnNF_Tc (PredTy p')
432 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
433 go res `thenNF_Tc` \ res' ->
434 returnNF_Tc (FunTy arg' res')
436 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
437 go arg `thenNF_Tc` \ arg' ->
438 returnNF_Tc (mkAppTy fun' arg')
440 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
441 go ty `thenNF_Tc` \ ty' ->
442 returnNF_Tc (mkUTy u' ty')
444 -- The two interesting cases!
445 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
447 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
448 go ty `thenNF_Tc` \ ty' ->
449 returnNF_Tc (ForAllTy tyvar' ty')
451 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
452 returnNF_Tc (ClassP c tys')
453 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
454 returnNF_Tc (IParam n ty')
456 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
457 -> TcTyVar -> NF_TcM TcType
458 zonkTyVar unbound_var_fn tyvar
459 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
460 -- zonking a forall type, when the bound type variable
461 -- needn't be mutable
462 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
463 returnNF_Tc (TyVarTy tyvar)
466 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
468 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
469 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound