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(..),
47 getTyVar, mkAppTy, mkUTy,
48 splitPredTy_maybe, splitForAllTys,
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 (UsageTy _ t) ts = go syn_t t ts
96 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
100 %************************************************************************
102 \subsection{New type variables}
104 %************************************************************************
107 newTyVar :: Kind -> NF_TcM TcTyVar
109 = tcGetUnique `thenNF_Tc` \ uniq ->
110 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
112 newTyVarTy :: Kind -> NF_TcM TcType
114 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
115 returnNF_Tc (TyVarTy tc_tyvar)
117 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
118 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
120 newKindVar :: NF_TcM TcKind
122 = tcGetUnique `thenNF_Tc` \ uniq ->
123 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
124 returnNF_Tc (TyVarTy kv)
126 newKindVars :: Int -> NF_TcM [TcKind]
127 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
129 newBoxityVar :: NF_TcM TcKind
131 = tcGetUnique `thenNF_Tc` \ uniq ->
132 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
133 returnNF_Tc (TyVarTy kv)
137 %************************************************************************
139 \subsection{Type instantiation}
141 %************************************************************************
143 Instantiating a bunch of type variables
146 tcInstTyVars :: [TyVar]
147 -> NF_TcM ([TcTyVar], [TcType], Subst)
150 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
152 tys = mkTyVarTys tc_tyvars
154 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
155 -- Since the tyvars are freshly made,
156 -- they cannot possibly be captured by
157 -- any existing for-alls. Hence mkTopTyVarSubst
160 = tcGetUnique `thenNF_Tc` \ uniq ->
162 name = setNameUnique (tyVarName tyvar) uniq
163 -- Note that we don't change the print-name
164 -- This won't confuse the type checker but there's a chance
165 -- that two different tyvars will print the same way
166 -- in an error message. -dppr-debug will show up the difference
167 -- Better watch out for this. If worst comes to worst, just
168 -- use mkSysLocalName.
170 tcNewMutTyVar name (tyVarKind tyvar)
172 tcInstSigVar tyvar -- Very similar to tcInstTyVar
173 = tcGetUnique `thenNF_Tc` \ uniq ->
175 name = setNameUnique (tyVarName tyvar) uniq
176 kind = tyVarKind tyvar
178 ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
179 tcNewSigTyVar name kind
182 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
183 fresh type variables, returning them and the instantiated body of the for-all.
186 tcInstTcType :: TcType -> NF_TcM ([TcTyVar], TcType)
188 = case splitForAllTys ty of
189 ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
190 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
191 returnNF_Tc (tyvars', substTy tenv rho)
196 %************************************************************************
198 \subsection{Putting and getting mutable type variables}
200 %************************************************************************
203 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
204 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
210 tcPutTyVar tyvar ty = UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
211 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
215 Getting is more interesting. The easy thing to do is just to read, thus:
218 tcGetTyVar tyvar = tcReadMutTyVar tyvar
221 But it's more fun to short out indirections on the way: If this
222 version returns a TyVar, then that TyVar is unbound. If it returns
223 any other type, then there might be bound TyVars embedded inside it.
225 We return Nothing iff the original box was unbound.
229 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
230 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
232 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
233 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
234 returnNF_Tc (Just ty')
236 Nothing -> returnNF_Tc Nothing
238 short_out :: TcType -> NF_TcM TcType
239 short_out ty@(TyVarTy tyvar)
240 | not (isMutTyVar tyvar)
244 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
246 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
247 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
250 other -> returnNF_Tc ty
252 short_out other_ty = returnNF_Tc other_ty
256 %************************************************************************
258 \subsection{Zonking -- the exernal interfaces}
260 %************************************************************************
262 ----------------- Type variables
265 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
266 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
268 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
269 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
271 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
272 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
273 -- Usually this job is done by checkSigTyVars, but in a couple of places
274 -- that is overkill, so we use this simpler chap
275 zonkTcSigTyVars tyvars
276 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
277 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
280 ----------------- Types
283 zonkTcType :: TcType -> NF_TcM TcType
284 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
286 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
287 zonkTcTypes tys = mapNF_Tc zonkTcType tys
289 zonkTcClassConstraints cts = mapNF_Tc zonk cts
290 where zonk (clas, tys)
291 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
292 returnNF_Tc (clas, new_tys)
294 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
295 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
297 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
298 zonkTcPredType (Class c ts) =
299 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
300 returnNF_Tc (Class c new_ts)
301 zonkTcPredType (IParam n t) =
302 zonkTcType t `thenNF_Tc` \ new_t ->
303 returnNF_Tc (IParam n new_t)
306 ------------------- These ...ToType, ...ToKind versions
307 are used at the end of type checking
310 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
312 = mapNF_Tc zonk_it pairs
314 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
315 returnNF_Tc (name, kind)
317 -- When zonking a kind, we want to
318 -- zonk a *kind* variable to (Type *)
319 -- zonk a *boxity* variable to *
320 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv boxedTypeKind
321 | tyVarKind kv == superBoxity = tcPutTyVar kv boxedBoxity
322 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
324 zonkTcTypeToType :: TcType -> NF_TcM Type
325 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
327 -- Zonk a mutable but unbound type variable to
328 -- Void if it has kind Boxed
330 zonk_unbound_tyvar tv
331 | kind == boxedTypeKind
332 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
333 -- this vastly common case
335 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
339 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
340 -- type variable tv. Same name too, apart from
341 -- making it start with a colon (sigh)
342 = mkPrimTyCon tc_name kind 0 [] VoidRep
344 tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
346 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
347 -- of a type variable, at the *end* of type checking. It changes
348 -- the *mutable* type variable into an *immutable* one.
350 -- It does this by making an immutable version of tv and binds tv to it.
351 -- Now any bound occurences of the original type variable will get
352 -- zonked to the immutable version.
354 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
355 zonkTcTyVarToTyVar tv
357 -- Make an immutable version, defaulting
358 -- the kind to boxed if necessary
359 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
360 immut_tv_ty = mkTyVarTy immut_tv
362 zap tv = tcPutTyVar tv immut_tv_ty
363 -- Bind the mutable version to the immutable one
365 -- If the type variable is mutable, then bind it to immut_tv_ty
366 -- so that all other occurrences of the tyvar will get zapped too
367 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
369 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
375 %************************************************************************
377 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
379 %* For internal use only! *
381 %************************************************************************
384 -- zonkType is used for Kinds as well
386 -- For unbound, mutable tyvars, zonkType uses the function given to it
387 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
388 -- type variable and zonks the kind too
390 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
391 -- see zonkTcType, and zonkTcTypeToType
394 zonkType unbound_var_fn ty
397 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
398 returnNF_Tc (TyConApp tycon tys')
400 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
401 go ty2 `thenNF_Tc` \ ty2' ->
402 returnNF_Tc (NoteTy (SynNote ty1') ty2')
404 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
406 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
407 returnNF_Tc (PredTy p')
409 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
410 go res `thenNF_Tc` \ res' ->
411 returnNF_Tc (FunTy arg' res')
413 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
414 go arg `thenNF_Tc` \ arg' ->
415 returnNF_Tc (mkAppTy fun' arg')
417 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
418 go ty `thenNF_Tc` \ ty' ->
419 returnNF_Tc (mkUTy u' ty')
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 -> zonkType unbound_var_fn other_ty -- Bound