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 TypeRep ( Type(..), Kind, TyNote(..),
56 typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
58 import Type ( ThetaType,
60 splitDictTy_maybe, splitForAllTys, isNotUsgTy,
61 isTyVarTy, mkTyVarTy, mkTyVarTys,
63 import Subst ( Subst, mkTopTyVarSubst, substTy )
64 import TyCon ( tyConKind, mkPrimTyCon )
65 import PrimRep ( PrimRep(VoidRep) )
67 import VarSet ( emptyVarSet )
68 import Var ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
72 import TysWiredIn ( voidTy )
74 import Name ( NamedThing(..), setNameUnique, mkSysLocalName,
75 mkDerivedName, mkDerivedTyConOcc
77 import Unique ( Unique, Uniquable(..) )
78 import Util ( nOfThem )
86 Type definitions are in TcMonad.lhs
89 typeToTcType :: Type -> TcType
92 kindToTcKind :: Kind -> TcKind
93 kindToTcKind kind = kind
98 These tcSplit functions are like their non-Tc analogues, but they
99 follow through bound type variables.
101 No need for tcSplitForAllTy because a type variable can't be instantiated
105 tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType)
109 -- A type variable is never instantiated to a dictionary type,
110 -- so we don't need to do a tcReadVar on the "arg".
111 go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
112 Just pair -> go res res (pair:ts)
113 Nothing -> returnNF_Tc (reverse ts, syn_t)
114 go syn_t (NoteTy _ t) ts = go syn_t t ts
115 go syn_t (TyVarTy tv) ts = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
117 Just ty | not (isTyVarTy ty) -> go syn_t ty ts
118 other -> returnNF_Tc (reverse ts, syn_t)
119 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
123 %************************************************************************
125 \subsection{New type variables}
127 %************************************************************************
130 newTyVar :: Kind -> NF_TcM s TcTyVar
132 = tcGetUnique `thenNF_Tc` \ uniq ->
133 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
135 newTyVarTy :: Kind -> NF_TcM s TcType
137 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
138 returnNF_Tc (TyVarTy tc_tyvar)
140 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType]
141 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
143 newKindVar :: NF_TcM s TcKind
145 = tcGetUnique `thenNF_Tc` \ uniq ->
146 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
147 returnNF_Tc (TyVarTy kv)
149 newKindVars :: Int -> NF_TcM s [TcKind]
150 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
152 -- Returns a type variable of kind (Type bv) where bv is a new boxity var
153 -- Used when you need a type variable that's definitely a , but you don't know
154 -- what kind of type (boxed or unboxed).
155 newTyVarTy_OpenKind :: NF_TcM s TcType
156 newTyVarTy_OpenKind = newOpenTypeKind `thenNF_Tc` \ kind ->
159 newOpenTypeKind :: NF_TcM s TcKind
160 newOpenTypeKind = newTyVarTy superBoxity `thenNF_Tc` \ bv ->
161 returnNF_Tc (mkTyConApp typeCon [bv])
165 %************************************************************************
167 \subsection{Type instantiation}
169 %************************************************************************
171 Instantiating a bunch of type variables
174 tcInstTyVars :: [TyVar]
175 -> NF_TcM s ([TcTyVar], [TcType], Subst)
178 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
180 tys = mkTyVarTys tc_tyvars
182 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
183 -- Since the tyvars are freshly made,
184 -- they cannot possibly be captured by
185 -- any existing for-alls. Hence mkTopTyVarSubst
188 = tcGetUnique `thenNF_Tc` \ uniq ->
190 name = setNameUnique (tyVarName tyvar) uniq
191 -- Note that we don't change the print-name
192 -- This won't confuse the type checker but there's a chance
193 -- that two different tyvars will print the same way
194 -- in an error message. -dppr-debug will show up the difference
195 -- Better watch out for this. If worst comes to worst, just
196 -- use mkSysLocalName.
198 kind = tyVarKind tyvar
201 -- Hack alert! Certain system functions (like error) are quantified
202 -- over type variables with an 'open' kind (a :: ?). When we instantiate
203 -- these tyvars we want to make a type variable whose kind is (Type bv)
204 -- where bv is a boxity variable. This makes sure it's a type, but
205 -- is open about its boxity. We *don't* want to give the thing the
206 -- kind '?' (= Type AnyBox).
208 -- This is all a hack to avoid giving error it's "proper" type:
209 -- error :: forall bv. forall a::Type bv. String -> a
211 (if kind == openTypeKind then
214 returnNF_Tc kind) `thenNF_Tc` \ kind' ->
216 tcNewMutTyVar name kind'
218 tcInstSigVar tyvar -- Very similar to tcInstTyVar
219 = tcGetUnique `thenNF_Tc` \ uniq ->
221 name = setNameUnique (tyVarName tyvar) uniq
222 kind = tyVarKind tyvar
224 ASSERT( not (kind == openTypeKind) ) -- Shouldn't happen
225 tcNewSigTyVar name kind
228 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
229 fresh type variables, returning them and the instantiated body of the for-all.
232 tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
234 = case splitForAllTys ty of
235 ([], _) -> returnNF_Tc ([], ty) -- Nothing to do
236 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
237 returnNF_Tc (tyvars', substTy tenv rho)
242 %************************************************************************
244 \subsection{Putting and getting mutable type variables}
246 %************************************************************************
249 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
250 tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
256 tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
260 Getting is more interesting. The easy thing to do is just to read, thus:
263 tcGetTyVar tyvar = tcReadMutTyVar tyvar
266 But it's more fun to short out indirections on the way: If this
267 version returns a TyVar, then that TyVar is unbound. If it returns
268 any other type, then there might be bound TyVars embedded inside it.
270 We return Nothing iff the original box was unbound.
274 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
275 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
277 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
278 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
279 returnNF_Tc (Just ty')
281 Nothing -> returnNF_Tc Nothing
283 short_out :: TcType -> NF_TcM s TcType
284 short_out ty@(TyVarTy tyvar)
285 | not (isMutTyVar tyvar)
289 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
291 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
292 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
295 other -> returnNF_Tc ty
297 short_out other_ty = returnNF_Tc other_ty
301 %************************************************************************
303 \subsection{Zonking -- the exernal interfaces}
305 %************************************************************************
307 ----------------- Type variables
310 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
311 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
313 zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
314 zonkTcTyVarBndr tyvar
315 = zonkTcTyVar tyvar `thenNF_Tc` \ ty ->
317 TyVarTy tyvar' -> returnNF_Tc tyvar'
318 _ -> pprTrace "zonkTcTyVarBndr" (ppr tyvar <+> ppr ty) $
321 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
322 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
325 ----------------- Types
328 zonkTcType :: TcType -> NF_TcM s TcType
329 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
331 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
332 zonkTcTypes tys = mapNF_Tc zonkTcType tys
334 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
335 zonkTcThetaType theta = mapNF_Tc zonk theta
337 zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
338 returnNF_Tc (c, new_ts)
340 zonkTcKind :: TcKind -> NF_TcM s TcKind
341 zonkTcKind = zonkTcType
344 ------------------- These ...ToType, ...ToKind versions
345 are used at the end of type checking
348 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
349 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
351 -- Zonk a mutable but unbound kind variable to
352 -- (Type Boxed) if it has kind superKind
353 -- Boxed if it has kind superBoxity
354 zonk_unbound_kind_var kv
355 | super_kind == superKind = tcPutTyVar kv boxedTypeKind
356 | otherwise = ASSERT( super_kind == superBoxity )
357 tcPutTyVar kv boxedKind
359 super_kind = tyVarKind kv
362 zonkTcTypeToType :: TcType -> NF_TcM s Type
363 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
365 -- Zonk a mutable but unbound type variable to
366 -- Void if it has kind (Type Boxed)
368 zonk_unbound_tyvar tv
369 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
370 if kind == boxedTypeKind then
371 tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
372 -- this vastly common case
374 tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
376 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
377 -- type variable tv. Same name too, apart from
378 -- making it start with a colon (sigh)
379 = mkPrimTyCon tc_name kind 0 [] VoidRep
381 tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
383 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
384 -- of a type variable, at the *end* of type checking.
385 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
386 -- zonks its kind, and then makes an immutable version of tv and binds tv to it.
387 -- Now any bound occurences of the original type variable will get
388 -- zonked to the immutable version.
390 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
391 zonkTcTyVarToTyVar tv
392 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
394 -- Make an immutable version
395 immut_tv = mkTyVar (tyVarName tv) kind
396 immut_tv_ty = mkTyVarTy immut_tv
398 zap tv = tcPutTyVar tv immut_tv_ty
399 -- Bind the mutable version to the immutable one
401 -- If the type variable is mutable, then bind it to immut_tv_ty
402 -- so that all other occurrences of the tyvar will get zapped too
403 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
404 ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
410 %************************************************************************
412 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
414 %* For internal use only! *
416 %************************************************************************
419 -- zonkType is used for Kinds as well
421 -- For unbound, mutable tyvars, zonkType uses the function given to it
422 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
423 -- type variable and zonks the kind too
425 zonkType :: (TcTyVar -> NF_TcM s Type) -- What to do with unbound mutable type variables
426 -- see zonkTcType, and zonkTcTypeToType
429 zonkType unbound_var_fn ty
432 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
433 returnNF_Tc (TyConApp tycon tys')
435 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
436 go ty2 `thenNF_Tc` \ ty2' ->
437 returnNF_Tc (NoteTy (SynNote ty1') ty2')
439 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
441 go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
442 returnNF_Tc (NoteTy (UsgNote usg) ty2')
444 go (NoteTy (UsgForAll uv) ty2)= go ty2 `thenNF_Tc` \ ty2' ->
445 returnNF_Tc (NoteTy (UsgForAll uv) ty2')
447 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
448 go res `thenNF_Tc` \ res' ->
449 returnNF_Tc (FunTy arg' res')
451 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
452 go arg `thenNF_Tc` \ arg' ->
453 returnNF_Tc (mkAppTy fun' arg')
455 -- The two interesting cases!
456 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
458 go (ForAllTy tyvar ty)
459 = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
460 go ty `thenNF_Tc` \ ty' ->
461 returnNF_Tc (ForAllTy tyvar' ty')
464 zonkTyVar :: (TcTyVar -> NF_TcM s Type) -- What to do for an unbound mutable variable
465 -> TcTyVar -> NF_TcM s TcType
466 zonkTyVar unbound_var_fn tyvar
467 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
468 -- zonking a forall type, when the bound type variable
469 -- needn't be mutable
470 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
471 returnNF_Tc (TyVarTy tyvar)
474 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
476 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
477 Just other_ty -> ASSERT( isNotUsgTy other_ty )
478 zonkType unbound_var_fn other_ty -- Bound
481 %************************************************************************
483 \subsection{tcTypeKind}
485 %************************************************************************
487 Sadly, we need a Tc version of typeKind, that looks though mutable
488 kind variables. See the notes with Type.typeKind for the typeKindF nonsense
490 This is pretty gruesome.
493 tcTypeKind :: TcType -> NF_TcM s TcKind
495 tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar)
496 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
497 tcTypeKind (NoteTy _ ty) = tcTypeKind ty
498 tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind ->
499 tcFunResultTy fun_kind
500 tcTypeKind (FunTy fun arg) = tcTypeKindF arg
501 tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty
503 tcTypeKindF :: TcType -> NF_TcM s TcKind
504 tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty
505 tcTypeKindF (FunTy _ ty) = tcTypeKindF ty
506 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
507 tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind ->
510 fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
511 -- Functions at the type level are always boxed
512 fix_up (NoteTy _ kind) = fix_up kind
513 fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
515 Just kind' -> fix_up kind'
516 Nothing -> returnNF_Tc kind
517 fix_up kind = returnNF_Tc kind
519 tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty
520 tcFunResultTy (FunTy arg res) = returnNF_Tc res
521 tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
523 Just ty' -> tcFunResultTy ty'
524 -- The Nothing case, and the other cases for tcFunResultTy
525 -- should never happen... pattern match failure