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 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 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
184 fresh type variables, returning them and the instantiated body of the for-all.
187 tcInstTcType :: TcType -> NF_TcM ([TcTyVar], TcType)
189 = case splitForAllTys ty of
190 ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
191 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
192 returnNF_Tc (tyvars', substTy tenv rho)
197 %************************************************************************
199 \subsection{Putting and getting mutable type variables}
201 %************************************************************************
204 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
205 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
211 tcPutTyVar tyvar ty = UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
212 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
216 Getting is more interesting. The easy thing to do is just to read, thus:
219 tcGetTyVar tyvar = tcReadMutTyVar tyvar
222 But it's more fun to short out indirections on the way: If this
223 version returns a TyVar, then that TyVar is unbound. If it returns
224 any other type, then there might be bound TyVars embedded inside it.
226 We return Nothing iff the original box was unbound.
230 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
231 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
233 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
234 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
235 returnNF_Tc (Just ty')
237 Nothing -> returnNF_Tc Nothing
239 short_out :: TcType -> NF_TcM TcType
240 short_out ty@(TyVarTy tyvar)
241 | not (isMutTyVar tyvar)
245 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
247 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
248 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
251 other -> returnNF_Tc ty
253 short_out other_ty = returnNF_Tc other_ty
257 %************************************************************************
259 \subsection{Zonking -- the exernal interfaces}
261 %************************************************************************
263 ----------------- Type variables
266 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
267 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
269 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
270 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
272 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
273 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
274 -- Usually this job is done by checkSigTyVars, but in a couple of places
275 -- that is overkill, so we use this simpler chap
276 zonkTcSigTyVars tyvars
277 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
278 returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
281 ----------------- Types
284 zonkTcType :: TcType -> NF_TcM TcType
285 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
287 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
288 zonkTcTypes tys = mapNF_Tc zonkTcType tys
290 zonkTcClassConstraints cts = mapNF_Tc zonk cts
291 where zonk (clas, tys)
292 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
293 returnNF_Tc (clas, new_tys)
295 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
296 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
298 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
299 zonkTcPredType (Class c ts) =
300 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
301 returnNF_Tc (Class c new_ts)
302 zonkTcPredType (IParam n t) =
303 zonkTcType t `thenNF_Tc` \ new_t ->
304 returnNF_Tc (IParam n new_t)
307 ------------------- These ...ToType, ...ToKind versions
308 are used at the end of type checking
311 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
313 = mapNF_Tc zonk_it pairs
315 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
316 returnNF_Tc (name, kind)
318 -- When zonking a kind, we want to
319 -- zonk a *kind* variable to (Type *)
320 -- zonk a *boxity* variable to *
321 zonk_unbound_kind_var kv | tyVarKind kv == superKind = tcPutTyVar kv boxedTypeKind
322 | tyVarKind kv == superBoxity = tcPutTyVar kv boxedBoxity
323 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
325 zonkTcTypeToType :: TcType -> NF_TcM Type
326 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
328 -- Zonk a mutable but unbound type variable to
329 -- Void if it has kind Boxed
331 zonk_unbound_tyvar tv
332 | kind == boxedTypeKind
333 = tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
334 -- this vastly common case
336 = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
340 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
341 -- type variable tv. Same name too, apart from
342 -- making it start with a colon (sigh)
343 -- I dread to think what will happen if this gets out into an
344 -- interface file. Catastrophe likely. Major sigh.
345 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
346 mkPrimTyCon tc_name kind 0 [] VoidRep
348 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
350 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
351 -- of a type variable, at the *end* of type checking. It changes
352 -- the *mutable* type variable into an *immutable* one.
354 -- It does this by making an immutable version of tv and binds tv to it.
355 -- Now any bound occurences of the original type variable will get
356 -- zonked to the immutable version.
358 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
359 zonkTcTyVarToTyVar tv
361 -- Make an immutable version, defaulting
362 -- the kind to boxed if necessary
363 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
364 immut_tv_ty = mkTyVarTy immut_tv
366 zap tv = tcPutTyVar tv immut_tv_ty
367 -- Bind the mutable version to the immutable one
369 -- If the type variable is mutable, then bind it to immut_tv_ty
370 -- so that all other occurrences of the tyvar will get zapped too
371 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
373 WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
379 %************************************************************************
381 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
383 %* For internal use only! *
385 %************************************************************************
388 -- zonkType is used for Kinds as well
390 -- For unbound, mutable tyvars, zonkType uses the function given to it
391 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
392 -- type variable and zonks the kind too
394 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
395 -- see zonkTcType, and zonkTcTypeToType
398 zonkType unbound_var_fn ty
401 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
402 returnNF_Tc (TyConApp tycon tys')
404 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
405 go ty2 `thenNF_Tc` \ ty2' ->
406 returnNF_Tc (NoteTy (SynNote ty1') ty2')
408 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
410 go (PredTy p) = go_pred p `thenNF_Tc` \ p' ->
411 returnNF_Tc (PredTy p')
413 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
414 go res `thenNF_Tc` \ res' ->
415 returnNF_Tc (FunTy arg' res')
417 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
418 go arg `thenNF_Tc` \ arg' ->
419 returnNF_Tc (mkAppTy fun' arg')
421 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
422 go ty `thenNF_Tc` \ ty' ->
423 returnNF_Tc (mkUTy u' ty')
425 -- The two interesting cases!
426 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
428 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
429 go ty `thenNF_Tc` \ ty' ->
430 returnNF_Tc (ForAllTy tyvar' ty')
432 go_pred (Class c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
433 returnNF_Tc (Class c tys')
434 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
435 returnNF_Tc (IParam n ty')
437 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
438 -> TcTyVar -> NF_TcM TcType
439 zonkTyVar unbound_var_fn tyvar
440 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
441 -- zonking a forall type, when the bound type variable
442 -- needn't be mutable
443 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
444 returnNF_Tc (TyVarTy tyvar)
447 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
449 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
450 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound