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, zonkTcClassConstraints, 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, PredType(..),
60 splitPredTy_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 splitPredTy_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 zonkTcClassConstraints cts = mapNF_Tc zonk cts
335 where zonk (clas, tys)
336 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
337 returnNF_Tc (clas, new_tys)
339 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
340 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
342 zonkTcPredType :: TcPredType -> NF_TcM s TcPredType
343 zonkTcPredType (Class c ts) =
344 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
345 returnNF_Tc (Class c new_ts)
346 zonkTcPredType (IParam n t) =
347 zonkTcType t `thenNF_Tc` \ new_t ->
348 returnNF_Tc (IParam n new_t)
350 zonkTcKind :: TcKind -> NF_TcM s TcKind
351 zonkTcKind = zonkTcType
354 ------------------- These ...ToType, ...ToKind versions
355 are used at the end of type checking
358 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
359 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
361 -- Zonk a mutable but unbound kind variable to
362 -- (Type Boxed) if it has kind superKind
363 -- Boxed if it has kind superBoxity
364 zonk_unbound_kind_var kv
365 | super_kind == superKind = tcPutTyVar kv boxedTypeKind
366 | otherwise = ASSERT( super_kind == superBoxity )
367 tcPutTyVar kv boxedKind
369 super_kind = tyVarKind kv
372 zonkTcTypeToType :: TcType -> NF_TcM s Type
373 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
375 -- Zonk a mutable but unbound type variable to
376 -- Void if it has kind (Type Boxed)
378 zonk_unbound_tyvar tv
379 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
380 if kind == boxedTypeKind then
381 tcPutTyVar tv voidTy -- Just to avoid creating a new tycon in
382 -- this vastly common case
384 tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
386 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
387 -- type variable tv. Same name too, apart from
388 -- making it start with a colon (sigh)
389 = mkPrimTyCon tc_name kind 0 [] VoidRep
391 tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
393 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
394 -- of a type variable, at the *end* of type checking.
395 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
396 -- zonks its kind, and then makes an immutable version of tv and binds tv to it.
397 -- Now any bound occurences of the original type variable will get
398 -- zonked to the immutable version.
400 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
401 zonkTcTyVarToTyVar tv
402 = zonkTcKindToKind (tyVarKind tv) `thenNF_Tc` \ kind ->
404 -- Make an immutable version
405 immut_tv = mkTyVar (tyVarName tv) kind
406 immut_tv_ty = mkTyVarTy immut_tv
408 zap tv = tcPutTyVar tv immut_tv_ty
409 -- Bind the mutable version to the immutable one
411 -- If the type variable is mutable, then bind it to immut_tv_ty
412 -- so that all other occurrences of the tyvar will get zapped too
413 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
414 ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
420 %************************************************************************
422 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
424 %* For internal use only! *
426 %************************************************************************
429 -- zonkType is used for Kinds as well
431 -- For unbound, mutable tyvars, zonkType uses the function given to it
432 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
433 -- type variable and zonks the kind too
435 zonkType :: (TcTyVar -> NF_TcM s Type) -- What to do with unbound mutable type variables
436 -- see zonkTcType, and zonkTcTypeToType
439 zonkType unbound_var_fn ty
442 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
443 returnNF_Tc (TyConApp tycon tys')
445 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
446 go ty2 `thenNF_Tc` \ ty2' ->
447 returnNF_Tc (NoteTy (SynNote ty1') ty2')
449 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
451 go (NoteTy (UsgNote usg) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
452 returnNF_Tc (NoteTy (UsgNote usg) ty2')
454 go (NoteTy (UsgForAll uv) ty2)= go ty2 `thenNF_Tc` \ ty2' ->
455 returnNF_Tc (NoteTy (UsgForAll uv) ty2')
457 go (NoteTy (IPNote nm) ty2) = go ty2 `thenNF_Tc` \ ty2' ->
458 returnNF_Tc (NoteTy (IPNote nm) ty2')
460 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
461 go res `thenNF_Tc` \ res' ->
462 returnNF_Tc (FunTy arg' res')
464 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
465 go arg `thenNF_Tc` \ arg' ->
466 returnNF_Tc (mkAppTy fun' arg')
468 -- The two interesting cases!
469 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
471 go (ForAllTy tyvar ty)
472 = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
473 go ty `thenNF_Tc` \ ty' ->
474 returnNF_Tc (ForAllTy tyvar' ty')
477 zonkTyVar :: (TcTyVar -> NF_TcM s Type) -- What to do for an unbound mutable variable
478 -> TcTyVar -> NF_TcM s TcType
479 zonkTyVar unbound_var_fn tyvar
480 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
481 -- zonking a forall type, when the bound type variable
482 -- needn't be mutable
483 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
484 returnNF_Tc (TyVarTy tyvar)
487 = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty ->
489 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
490 Just other_ty -> ASSERT( isNotUsgTy other_ty )
491 zonkType unbound_var_fn other_ty -- Bound
494 %************************************************************************
496 \subsection{tcTypeKind}
498 %************************************************************************
500 Sadly, we need a Tc version of typeKind, that looks though mutable
501 kind variables. See the notes with Type.typeKind for the typeKindF nonsense
503 This is pretty gruesome.
506 tcTypeKind :: TcType -> NF_TcM s TcKind
508 tcTypeKind (TyVarTy tyvar) = returnNF_Tc (tyVarKind tyvar)
509 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
510 tcTypeKind (NoteTy _ ty) = tcTypeKind ty
511 tcTypeKind (AppTy fun arg) = tcTypeKind fun `thenNF_Tc` \ fun_kind ->
512 tcFunResultTy fun_kind
513 tcTypeKind (FunTy fun arg) = tcTypeKindF arg
514 tcTypeKind (ForAllTy _ ty) = tcTypeKindF ty
516 tcTypeKindF :: TcType -> NF_TcM s TcKind
517 tcTypeKindF (NoteTy _ ty) = tcTypeKindF ty
518 tcTypeKindF (FunTy _ ty) = tcTypeKindF ty
519 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
520 tcTypeKindF other = tcTypeKind other `thenNF_Tc` \ kind ->
523 fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
524 -- Functions at the type level are always boxed
525 fix_up (NoteTy _ kind) = fix_up kind
526 fix_up kind@(TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
528 Just kind' -> fix_up kind'
529 Nothing -> returnNF_Tc kind
530 fix_up kind = returnNF_Tc kind
532 tcFunResultTy (NoteTy _ ty) = tcFunResultTy ty
533 tcFunResultTy (FunTy arg res) = returnNF_Tc res
534 tcFunResultTy (TyVarTy tv) = tcGetTyVar tv `thenNF_Tc` \ maybe_ty ->
536 Just ty' -> tcFunResultTy ty'
537 -- The Nothing case, and the other cases for tcFunResultTy
538 -- should never happen... pattern match failure