2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
12 newTyVarTy, -- Kind -> NF_TcM s TcType
13 newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType]
15 newTyVarTy_OpenKind, -- NF_TcM s TcType
16 newOpenTypeKind, -- NF_TcM s TcKind
18 -----------------------------------------
19 TcType, TcTauType, TcThetaType, TcRhoType,
21 -- Find the type to which a type variable is bound
22 tcPutTyVar, -- :: TcTyVar -> TcType -> NF_TcM TcType
23 tcGetTyVar, -- :: TcTyVar -> NF_TcM (Maybe TcType) does shorting out
34 tcTypeKind, -- :: TcType -> NF_TcM s TcKind
35 --------------------------------
37 newKindVar, newKindVars,
41 --------------------------------
42 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
43 zonkTcType, zonkTcTypes, zonkTcThetaType,
45 zonkTcTypeToType, zonkTcTyVarToTyVar,
50 #include "HsVersions.h"
54 import PprType ( pprType )
55 import Type ( Type(..), Kind, ThetaType, TyNote(..),
57 splitDictTy_maybe, splitForAllTys,
58 isTyVarTy, mkTyVarTy, mkTyVarTys,
59 fullSubstTy, substTopTy,
60 typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
62 import TyCon ( tyConKind, mkPrimTyCon )
63 import PrimRep ( PrimRep(VoidRep) )
65 import VarSet ( emptyVarSet )
66 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
70 import TysWiredIn ( voidTy )
72 import Name ( NamedThing(..), setNameUnique, mkSysLocalName,
73 mkDerivedName, mkDerivedTyConOcc
75 import Unique ( Unique, Uniquable(..) )
76 import Util ( nOfThem )
84 Type definitions are in TcMonad.lhs
87 typeToTcType :: Type -> TcType
90 kindToTcKind :: Kind -> TcKind
91 kindToTcKind kind = kind
96 These tcSplit functions are like their non-Tc analogues, but they
97 follow through bound type variables.
99 No need for tcSplitForAllTy because a type variable can't be instantiated
103 tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType)
107 -- A type variable is never instantiated to a dictionary type,
108 -- so we don't need to do a tcReadVar on the "arg".
109 go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
110 Just pair -> go res res (pair:ts)
111 Nothing -> returnNF_Tc (reverse ts, syn_t)
112 go syn_t (NoteTy _ t) ts = go syn_t t ts
113 go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
115 Just ty | not (isTyVarTy ty) -> go syn_t ty ts
116 other -> returnNF_Tc (reverse ts, syn_t)
117 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
121 %************************************************************************
123 \subsection{New type variables}
125 %************************************************************************
128 newTyVar :: Kind -> NF_TcM s TcTyVar
130 = tcGetUnique `thenNF_Tc` \ uniq ->
131 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
133 newTyVarTy :: Kind -> NF_TcM s TcType
135 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
136 returnNF_Tc (TyVarTy tc_tyvar)
138 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType]
139 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
141 newKindVar :: NF_TcM s TcKind
143 = tcGetUnique `thenNF_Tc` \ uniq ->
144 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
145 returnNF_Tc (TyVarTy kv)
147 newKindVars :: Int -> NF_TcM s [TcKind]
148 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
150 -- Returns a type variable of kind (Type bv) where bv is a new boxity var
151 -- Used when you need a type variable that's definitely a , but you don't know
152 -- what kind of type (boxed or unboxed).
153 newTyVarTy_OpenKind :: NF_TcM s TcType
154 newTyVarTy_OpenKind = newOpenTypeKind `thenNF_Tc` \ kind ->
157 newOpenTypeKind :: NF_TcM s TcKind
158 newOpenTypeKind = newTyVarTy superBoxity `thenNF_Tc` \ bv ->
159 returnNF_Tc (mkTyConApp typeCon [bv])
163 %************************************************************************
165 \subsection{Type instantiation}
167 %************************************************************************
169 Instantiating a bunch of type variables
172 tcInstTyVars :: [TyVar]
173 -> NF_TcM s ([TcTyVar], [TcType], TyVarEnv TcType)
176 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
178 tys = mkTyVarTys tc_tyvars
180 returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
183 = tcGetUnique `thenNF_Tc` \ uniq ->
185 name = setNameUnique (tyVarName tyvar) uniq
186 -- Note that we don't change the print-name
187 -- This won't confuse the type checker but there's a chance
188 -- that two different tyvars will print the same way
189 -- in an error message. -dppr-debug will show up the difference
190 -- Better watch out for this. If worst comes to worst, just
191 -- use mkSysLocalName.
193 kind = tyVarKind tyvar
196 -- Hack alert! Certain system functions (like error) are quantified
197 -- over type variables with an 'open' kind (a :: ?). When we instantiate
198 -- these tyvars we want to make a type variable whose kind is (Type bv)
199 -- where bv is a boxity variable. This makes sure it's a type, but
200 -- is open about its boxity. We *don't* want to give the thing the
201 -- kind '?' (= Type AnyBox).
203 -- This is all a hack to avoid giving error it's "proper" type:
204 -- error :: forall bv. forall a::Type bv. String -> a
206 (if kind == openTypeKind then
209 returnNF_Tc kind) `thenNF_Tc` \ kind' ->
211 tcNewMutTyVar name kind'
213 tcInstSigVar tyvar -- Very similar to tcInstTyVar
214 = tcGetUnique `thenNF_Tc` \ uniq ->
216 name = setNameUnique (tyVarName tyvar) uniq
217 kind = tyVarKind tyvar
219 ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
220 tcNewSigTyVar name kind
223 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
224 fresh type variables, returning them and the instantiated body of the for-all.
227 tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
229 = case splitForAllTys ty of
230 ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
231 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
232 returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
233 -- Since the tyvars are freshly made,
234 -- they cannot possibly be captured by
235 -- any existing for-alls. Hence emptyVarSet
240 %************************************************************************
242 \subsection{Putting and getting mutable type variables}
244 %************************************************************************
247 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
248 tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
254 tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
258 Getting is more interesting. The easy thing to do is just to read, thus:
261 tcGetTyVar tyvar = tcReadMutTyVar tyvar
264 But it's more fun to short out indirections on the way: If this
265 version returns a TyVar, then that TyVar is unbound. If it returns
266 any other type, then there might be bound TyVars embedded inside it.
268 We return Nothing iff the original box was unbound.
272 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
273 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
275 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
276 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
277 returnNF_Tc (Just ty')
279 Nothing -> returnNF_Tc Nothing
281 short_out :: TcType -> NF_TcM s TcType
282 short_out ty@(TyVarTy tyvar)
283 | not (isMutTyVar tyvar)
287 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
289 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
290 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
293 other -> returnNF_Tc ty
295 short_out other_ty = returnNF_Tc other_ty
299 %************************************************************************
301 \subsection{Zonking -- the exernal interfaces}
303 %************************************************************************
305 ----------------- Type variables
308 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
309 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
311 zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
312 zonkTcTyVarBndr tyvar
313 = zonkTcTyVar tyvar `thenNF_Tc` \ (TyVarTy tyvar') ->
316 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
317 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
320 ----------------- Types
323 zonkTcType :: TcType -> NF_TcM s TcType
324 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
326 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
327 zonkTcTypes tys = mapNF_Tc zonkTcType tys
329 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
330 zonkTcThetaType theta = mapNF_Tc zonk theta
332 zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
333 returnNF_Tc (c, new_ts)
335 zonkTcKind :: TcKind -> NF_TcM s TcKind
336 zonkTcKind = zonkTcType
339 ------------------- These ...ToType, ...ToKind versions
340 are used at the end of type checking
343 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
344 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
346 -- Zonk a mutable but unbound kind variable to
347 -- (Type Boxed) if it has kind superKind
348 -- Boxed if it has kind superBoxity
349 zonk_unbound_kind_var kv
350 | super_kind == superKind = tcPutTyVar kv boxedTypeKind
351 | otherwise = ASSERT( super_kind == superBoxity )
352 tcPutTyVar kv boxedKind
354 super_kind = tyVarKind kv
357 zonkTcTypeToType :: TcType -> NF_TcM s Type
358 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
360 -- Zonk a mutable but unbound type variable to
361 -- Void if it has kind (Type Boxed)
363 zonk_unbound_tyvar tv
364 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
365 if kind == boxedTypeKind then
366 tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
367 -- this vastly common case
369 tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
371 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
372 -- type variable tv. Same name too, apart from
373 -- making it start with a colon (sigh)
374 = mkPrimTyCon tc_name kind 0 VoidRep
376 tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
378 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
379 -- of a type variable, at the *end* of type checking.
380 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
381 -- zonks its kind, and then makes an immutable version of tv and binds tv to it.
382 -- Now any bound occurences of the original type variable will get
383 -- zonked to the immutable version.
385 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
386 zonkTcTyVarToTyVar tv
387 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
389 -- Make an immutable version
390 immut_tv = mkTyVar (tyVarName tv) kind
391 immut_tv_ty = mkTyVarTy immut_tv
393 zap tv = tcPutTyVar tv immut_tv_ty
394 -- Bind the mutable version to the immutable one
396 -- If the type variable is mutable, then bind it to immut_tv_ty
397 -- so that all other occurrences of the tyvar will get zapped too
398 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
399 ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
405 %************************************************************************
407 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
409 %* For internal use only! *
411 %************************************************************************
414 -- zonkType is used for Kinds as well
416 -- For unbound, mutable tyvars, zonkType uses the function given to it
417 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
418 -- type variable and zonks the kind too
420 zonkType :: (TcTyVar -> NF_TcM s Type) -- What to do with unbound mutable type variables
421 -- see zonkTcType, and zonkTcTypeToType
424 zonkType unbound_var_fn ty
427 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
428 returnNF_Tc (TyConApp tycon tys')
430 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
431 go ty2 `thenNF_Tc` \ ty2' ->
432 returnNF_Tc (NoteTy (SynNote ty1') ty2')
434 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
436 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
437 go res `thenNF_Tc` \ res' ->
438 returnNF_Tc (FunTy arg' res')
440 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
441 go arg `thenNF_Tc` \ arg' ->
442 returnNF_Tc (mkAppTy fun' arg')
444 -- The two interesting cases!
445 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
447 go (ForAllTy tyvar ty)
448 = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
449 go ty `thenNF_Tc` \ ty' ->
450 returnNF_Tc (ForAllTy tyvar' ty')
453 zonkTyVar :: (TcTyVar -> NF_TcM s Type) -- What to do for an unbound mutable variable
454 -> TcTyVar -> NF_TcM s TcType
455 zonkTyVar unbound_var_fn tyvar
456 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
457 -- zonking a forall type, when the bound type variable
458 -- needn't be mutable
459 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
460 returnNF_Tc (TyVarTy tyvar)
463 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
465 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
466 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
469 %************************************************************************
471 \subsection{tcTypeKind}
473 %************************************************************************
475 Sadly, we need a Tc version of typeKind, that looks though mutable
476 kind variables. See the notes with Type.typeKind for the typeKindF nonsense
478 This is pretty gruesome.
481 tcTypeKind :: TcType -> NF_TcM s TcKind
483 tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar)
484 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
485 tcTypeKind (NoteTy _ ty) = tcTypeKind ty
486 tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind ->
487 tcFunResultTy fun_kind
488 tcTypeKind (FunTy fun arg) = tcTypeKindF arg
489 tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty
491 tcTypeKindF :: TcType -> NF_TcM s TcKind
492 tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty
493 tcTypeKindF (FunTy _ ty) = tcTypeKindF ty
494 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
495 tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind ->
498 fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
499 -- Functions at the type level are always boxed
500 fix_up (NoteTy _ kind) = fix_up kind
501 fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
503 Just kind' -> fix_up kind'
504 Nothing -> returnNF_Tc kind
505 fix_up kind = returnNF_Tc kind
507 tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty
508 tcFunResultTy (FunTy arg res) = returnNF_Tc res
509 tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
511 Just ty' -> tcFunResultTy ty'
512 -- The Nothing case, and the other cases for tcFunResultTy
513 -- should never happen... pattern match failure