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
33 tcTypeKind, -- :: TcType -> NF_TcM s TcKind
34 --------------------------------
36 newKindVar, newKindVars,
40 --------------------------------
41 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
42 zonkTcType, zonkTcTypes, zonkTcThetaType,
44 zonkTcTypeToType, zonkTcTyVarToTyVar,
49 #include "HsVersions.h"
53 import PprType ( pprType )
54 import Type ( Type(..), Kind, ThetaType, TyNote(..),
56 splitDictTy_maybe, splitForAllTys,
57 isTyVarTy, mkTyVarTy, mkTyVarTys,
58 fullSubstTy, substTopTy,
59 typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
61 import TyCon ( tyConKind )
63 import VarSet ( emptyVarSet )
64 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
68 import TysWiredIn ( voidTy )
70 import Name ( NamedThing(..), setNameUnique, mkSysLocalName )
71 import Unique ( Unique )
72 import Util ( nOfThem )
80 Type definitions are in TcMonad.lhs
83 typeToTcType :: Type -> TcType
86 kindToTcKind :: Kind -> TcKind
87 kindToTcKind kind = kind
92 These tcSplit functions are like their non-Tc analogues, but they
93 follow through bound type variables.
95 No need for tcSplitForAllTy because a type variable can't be instantiated
99 tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType)
103 -- A type variable is never instantiated to a dictionary type,
104 -- so we don't need to do a tcReadVar on the "arg".
105 go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
106 Just pair -> go res res (pair:ts)
107 Nothing -> returnNF_Tc (reverse ts, syn_t)
108 go syn_t (NoteTy _ t) ts = go syn_t t ts
109 go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
111 Just ty | not (isTyVarTy ty) -> go syn_t ty ts
112 other -> returnNF_Tc (reverse ts, syn_t)
113 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
117 %************************************************************************
119 \subsection{New type variables}
121 %************************************************************************
124 newTyVar :: Kind -> NF_TcM s TcTyVar
126 = tcGetUnique `thenNF_Tc` \ uniq ->
127 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
129 newTyVarTy :: Kind -> NF_TcM s TcType
131 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
132 returnNF_Tc (TyVarTy tc_tyvar)
134 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType]
135 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
137 newKindVar :: NF_TcM s TcKind
139 = tcGetUnique `thenNF_Tc` \ uniq ->
140 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
141 returnNF_Tc (TyVarTy kv)
143 newKindVars :: Int -> NF_TcM s [TcKind]
144 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
146 -- Returns a type variable of kind (Type bv) where bv is a new boxity var
147 -- Used when you need a type variable that's definitely a , but you don't know
148 -- what kind of type (boxed or unboxed).
149 newTyVarTy_OpenKind :: NF_TcM s TcType
150 newTyVarTy_OpenKind = newOpenTypeKind `thenNF_Tc` \ kind ->
153 newOpenTypeKind :: NF_TcM s TcKind
154 newOpenTypeKind = newTyVarTy superBoxity `thenNF_Tc` \ bv ->
155 returnNF_Tc (mkTyConApp typeCon [bv])
159 %************************************************************************
161 \subsection{Type instantiation}
163 %************************************************************************
165 Instantiating a bunch of type variables
168 tcInstTyVars :: [TyVar]
169 -> NF_TcM s ([TcTyVar], [TcType], TyVarEnv TcType)
172 = mapNF_Tc inst_tyvar tyvars `thenNF_Tc` \ tc_tyvars ->
174 tys = mkTyVarTys tc_tyvars
176 returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
178 inst_tyvar tyvar -- Could use the name from the tyvar?
179 = tcGetUnique `thenNF_Tc` \ uniq ->
181 kind = tyVarKind tyvar
182 name = setNameUnique (tyVarName tyvar) uniq
183 -- Note that we don't change the print-name
184 -- This won't confuse the type checker but there's a chance
185 -- that two different tyvars will print the same way
186 -- in an error message. -dppr-debug will show up the difference
187 -- Better watch out for this. If worst comes to worst, just
188 -- use mkSysLocalName.
190 tcNewMutTyVar name kind
193 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
194 fresh type variables, returning them and the instantiated body of the for-all.
197 tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
199 = case splitForAllTys ty of
200 ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
201 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
202 returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
203 -- Since the tyvars are freshly made,
204 -- they cannot possibly be captured by
205 -- any existing for-alls. Hence emptyVarSet
210 %************************************************************************
212 \subsection{Putting and getting mutable type variables}
214 %************************************************************************
217 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
218 tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
224 tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
228 Getting is more interesting. The easy thing to do is just to read, thus:
231 tcGetTyVar tyvar = tcReadMutTyVar tyvar
234 But it's more fun to short out indirections on the way: If this
235 version returns a TyVar, then that TyVar is unbound. If it returns
236 any other type, then there might be bound TyVars embedded inside it.
238 We return Nothing iff the original box was unbound.
242 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
243 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
245 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
246 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
247 returnNF_Tc (Just ty')
249 Nothing -> returnNF_Tc Nothing
251 short_out :: TcType -> NF_TcM s TcType
252 short_out ty@(TyVarTy tyvar)
253 | not (isMutTyVar tyvar)
257 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
259 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
260 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
263 other -> returnNF_Tc ty
265 short_out other_ty = returnNF_Tc other_ty
269 %************************************************************************
271 \subsection{Zonking -- the exernal interfaces}
273 %************************************************************************
275 ----------------- Type variables
278 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
279 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
281 zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
282 zonkTcTyVarBndr tyvar
283 = zonkTcTyVar tyvar `thenNF_Tc` \ (TyVarTy tyvar') ->
286 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
287 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
290 ----------------- Types
293 zonkTcType :: TcType -> NF_TcM s TcType
294 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
296 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
297 zonkTcTypes tys = mapNF_Tc zonkTcType tys
299 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
300 zonkTcThetaType theta = mapNF_Tc zonk theta
302 zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
303 returnNF_Tc (c, new_ts)
305 zonkTcKind :: TcKind -> NF_TcM s TcKind
306 zonkTcKind = zonkTcType
309 ------------------- These ...ToType, ...ToKind versions
310 are used at the end of type checking
313 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
314 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
316 -- Zonk a mutable but unbound kind variable to
317 -- (Type Boxed) if it has kind superKind
318 -- Boxed if it has kind superBoxity
319 zonk_unbound_kind_var kv
320 | super_kind == superKind = tcPutTyVar kv boxedTypeKind
321 | otherwise = ASSERT( super_kind == superBoxity )
322 tcPutTyVar kv boxedKind
324 super_kind = tyVarKind kv
327 zonkTcTypeToType :: TcType -> NF_TcM s Type
328 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
330 -- Zonk a mutable but unbound type variable to
331 -- Void if it has kind (Type Boxed)
333 zonk_unbound_tyvar tv
334 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
335 if kind == boxedTypeKind then
336 tcPutTyVar tv voidTy -- Just to creating a new tycon in
337 -- this vastly common case
339 tcPutTyVar tv (TyConApp (mk_void_tycon tv) [])
341 mk_void_tycon tv -- Make a new TyCon with the same kind as the
342 -- type variable tv. Same name too, apart from
343 -- making it start with a capital letter (sigh)
344 -- I can't quite bring myself to write the Name-fiddling
345 -- code yet. ToDo. SLPJ Nov 98
346 = pprPanic "zonkTcTypeToType: free type variable with non-* type:" (ppr tv)
349 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
350 -- of a type variable, at the *end* of type checking.
351 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
352 -- zonks its kind, and then makes an immutable version of tv and binds tv to it.
353 -- Now any bound occurences of the original type variable will get
354 -- zonked to the immutable version.
356 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
357 zonkTcTyVarToTyVar tv
358 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
360 -- Make an immutable version
361 immut_tv = mkTyVar (tyVarName tv) kind
362 immut_tv_ty = mkTyVarTy immut_tv
364 zap tv = tcPutTyVar tv immut_tv_ty
365 -- Bind the mutable version to the immutable one
367 -- If the type variable is mutable, then bind it to immut_tv_ty
368 -- so that all other occurrences of the tyvar will get zapped too
369 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
370 ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
376 %************************************************************************
378 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
380 %* For internal use only! *
382 %************************************************************************
385 -- zonkType is used for Kinds as well
387 -- For unbound, mutable tyvars, zonkType uses the function given to it
388 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
389 -- type variable and zonks the kind too
391 zonkType :: (TcTyVar -> NF_TcM s Type) -- What to do with unbound mutable type variables
392 -- see zonkTcType, and zonkTcTypeToType
395 zonkType unbound_var_fn ty
398 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
399 returnNF_Tc (TyConApp tycon tys')
401 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
402 go ty2 `thenNF_Tc` \ ty2' ->
403 returnNF_Tc (NoteTy (SynNote ty1') ty2')
405 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
407 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
408 go res `thenNF_Tc` \ res' ->
409 returnNF_Tc (FunTy arg' res')
411 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
412 go arg `thenNF_Tc` \ arg' ->
413 returnNF_Tc (mkAppTy fun' arg')
415 -- The two interesting cases!
416 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
418 go (ForAllTy tyvar ty)
419 = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
420 go ty `thenNF_Tc` \ ty' ->
421 returnNF_Tc (ForAllTy tyvar' ty')
424 zonkTyVar :: (TcTyVar -> NF_TcM s Type) -- What to do for an unbound mutable variable
425 -> TcTyVar -> NF_TcM s TcType
426 zonkTyVar unbound_var_fn tyvar
427 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
428 -- zonking a forall type, when the bound type variable
429 -- needn't be mutable
430 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
431 returnNF_Tc (TyVarTy tyvar)
434 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
436 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
437 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
440 %************************************************************************
442 \subsection{tcTypeKind}
444 %************************************************************************
446 Sadly, we need a Tc version of typeKind, that looks though mutable
447 kind variables. See the notes with Type.typeKind for the typeKindF nonsense
449 This is pretty gruesome.
452 tcTypeKind :: TcType -> NF_TcM s TcKind
454 tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar)
455 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
456 tcTypeKind (NoteTy _ ty) = tcTypeKind ty
457 tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind ->
458 tcFunResultTy fun_kind
459 tcTypeKind (FunTy fun arg) = tcTypeKindF arg
460 tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty
462 tcTypeKindF :: TcType -> NF_TcM s TcKind
463 tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty
464 tcTypeKindF (FunTy _ ty) = tcTypeKindF ty
465 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
466 tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind ->
469 fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
470 -- Functions at the type level are always boxed
471 fix_up (NoteTy _ kind) = fix_up kind
472 fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
474 Just kind' -> fix_up kind'
475 Nothing -> returnNF_Tc kind
476 fix_up kind = returnNF_Tc kind
478 tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty
479 tcFunResultTy (FunTy arg res) = returnNF_Tc res
480 tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
482 Just ty' -> tcFunResultTy ty'
483 -- The Nothing case, and the other cases for tcFunResultTy
484 -- should never happen... pattern match failure