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 tcInstSigVars tyvars -- Very similar to tcInstTyVar
175 = tcGetUniques `thenNF_Tc` \ uniqs ->
176 listTc [ ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
177 tcNewSigTyVar name kind
178 | (tyvar, uniq) <- tyvars `zip` uniqs,
179 let name = setNameUnique (tyVarName tyvar) uniq,
180 let kind = tyVarKind tyvar
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) -> -- There may be overloading but no type variables;
192 -- (?x :: Int) => Int -> Int
193 tcSplitRhoTy rho `thenNF_Tc` \ (theta, tau) ->
194 returnNF_Tc ([], theta, tau)
196 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
197 tcSplitRhoTy (substTy tenv rho) `thenNF_Tc` \ (theta, tau) ->
198 returnNF_Tc (tyvars', theta, tau)
203 %************************************************************************
205 \subsection{Putting and getting mutable type variables}
207 %************************************************************************
210 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
211 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
218 | not (isMutTyVar tyvar)
219 = pprTrace "tcPutTyVar" (ppr tyvar) $
223 = ASSERT( isMutTyVar tyvar )
224 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
225 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
229 Getting is more interesting. The easy thing to do is just to read, thus:
232 tcGetTyVar tyvar = tcReadMutTyVar tyvar
235 But it's more fun to short out indirections on the way: If this
236 version returns a TyVar, then that TyVar is unbound. If it returns
237 any other type, then there might be bound TyVars embedded inside it.
239 We return Nothing iff the original box was unbound.
243 | not (isMutTyVar tyvar)
244 = pprTrace "tcGetTyVar" (ppr tyvar) $
245 returnNF_Tc (Just (mkTyVarTy tyvar))
248 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
249 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
251 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
252 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
253 returnNF_Tc (Just ty')
255 Nothing -> returnNF_Tc Nothing
257 short_out :: TcType -> NF_TcM TcType
258 short_out ty@(TyVarTy tyvar)
259 | not (isMutTyVar tyvar)
263 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
265 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
266 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
269 other -> returnNF_Tc ty
271 short_out other_ty = returnNF_Tc other_ty
275 %************************************************************************
277 \subsection{Zonking -- the exernal interfaces}
279 %************************************************************************
281 ----------------- Type variables
284 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
285 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
287 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
288 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
289 returnNF_Tc (tyVarsOfTypes tys)
291 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
292 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
294 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
295 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
296 -- Usually this job is done by checkSigTyVars, but in a couple of places
297 -- that is overkill, so we use this simpler chap
298 zonkTcSigTyVars tyvars
299 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
300 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
303 ----------------- Types
306 zonkTcType :: TcType -> NF_TcM TcType
307 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
309 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
310 zonkTcTypes tys = mapNF_Tc zonkTcType tys
312 zonkTcClassConstraints cts = mapNF_Tc zonk cts
313 where zonk (clas, tys)
314 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
315 returnNF_Tc (clas, new_tys)
317 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
318 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
320 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
321 zonkTcPredType (ClassP c ts) =
322 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
323 returnNF_Tc (ClassP c new_ts)
324 zonkTcPredType (IParam n t) =
325 zonkTcType t `thenNF_Tc` \ new_t ->
326 returnNF_Tc (IParam n new_t)
329 ------------------- These ...ToType, ...ToKind versions
330 are used at the end of type checking
333 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
335 = mapNF_Tc zonk_it pairs
337 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
338 returnNF_Tc (name, kind)
340 -- When zonking a kind, we want to
341 -- zonk a *kind* variable to (Type *)
342 -- zonk a *boxity* variable to *
343 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv liftedTypeKind
344 | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
345 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
347 zonkTcTypeToType :: TcType -> NF_TcM Type
348 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
350 -- Zonk a mutable but unbound type variable to
351 -- Void if it has kind Lifted
353 zonk_unbound_tyvar tv
354 | kind == liftedTypeKind || kind == openTypeKind
355 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
356 -- this vastly common case
358 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
362 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
363 -- type variable tv. Same name too, apart from
364 -- making it start with a colon (sigh)
365 -- I dread to think what will happen if this gets out into an
366 -- interface file. Catastrophe likely. Major sigh.
367 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
368 mkPrimTyCon tc_name kind 0 [] VoidRep
370 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
372 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
373 -- of a type variable, at the *end* of type checking. It changes
374 -- the *mutable* type variable into an *immutable* one.
376 -- It does this by making an immutable version of tv and binds tv to it.
377 -- Now any bound occurences of the original type variable will get
378 -- zonked to the immutable version.
380 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
381 zonkTcTyVarToTyVar tv
383 -- Make an immutable version, defaulting
384 -- the kind to lifted if necessary
385 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
386 immut_tv_ty = mkTyVarTy immut_tv
388 zap tv = tcPutTyVar tv immut_tv_ty
389 -- Bind the mutable version to the immutable one
391 -- If the type variable is mutable, then bind it to immut_tv_ty
392 -- so that all other occurrences of the tyvar will get zapped too
393 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
395 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
401 %************************************************************************
403 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
405 %* For internal use only! *
407 %************************************************************************
410 -- zonkType is used for Kinds as well
412 -- For unbound, mutable tyvars, zonkType uses the function given to it
413 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
414 -- type variable and zonks the kind too
416 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
417 -- see zonkTcType, and zonkTcTypeToType
420 zonkType unbound_var_fn ty
423 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
424 returnNF_Tc (TyConApp tycon tys')
426 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
427 go ty2 `thenNF_Tc` \ ty2' ->
428 returnNF_Tc (NoteTy (SynNote ty1') ty2')
430 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
432 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
433 returnNF_Tc (PredTy p')
435 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
436 go res `thenNF_Tc` \ res' ->
437 returnNF_Tc (FunTy arg' res')
439 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
440 go arg `thenNF_Tc` \ arg' ->
441 returnNF_Tc (mkAppTy fun' arg')
443 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
444 go ty `thenNF_Tc` \ ty' ->
445 returnNF_Tc (mkUTy u' ty')
447 -- The two interesting cases!
448 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
450 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
451 go ty `thenNF_Tc` \ ty' ->
452 returnNF_Tc (ForAllTy tyvar' ty')
454 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
455 returnNF_Tc (ClassP c tys')
456 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
457 returnNF_Tc (IParam n ty')
459 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
460 -> TcTyVar -> NF_TcM TcType
461 zonkTyVar unbound_var_fn tyvar
462 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
463 -- zonking a forall type, when the bound type variable
464 -- needn't be mutable
465 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
466 returnNF_Tc (TyVarTy tyvar)
469 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
471 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
472 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound