2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
8 Type(..), TyNote(..), UsageAnn(..), -- Representation visible to friends
11 superKind, superBoxity, -- :: SuperKind
13 boxedKind, -- :: Kind :: BX
14 anyBoxKind, -- :: Kind :: BX
15 typeCon, -- :: KindCon :: BX -> KX
16 anyBoxCon, -- :: KindCon :: BX
18 boxedTypeKind, unboxedTypeKind, openTypeKind, -- Kind :: superKind
20 mkArrowKind, mkArrowKinds, hasMoreBoxityInfo,
24 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
26 mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
28 mkFunTy, mkFunTys, splitFunTy_maybe, splitFunTys, splitFunTysN, funResultTy,
31 mkTyConApp, mkTyConTy, splitTyConApp_maybe,
32 splitAlgTyConApp_maybe, splitAlgTyConApp, splitRepTyConApp_maybe,
33 mkDictTy, splitDictTy_maybe, isDictTy,
35 mkSynTy, isSynTy, deNoteType,
37 mkUsgTy, isUsgTy{- dont use -}, isNotUsgTy, splitUsgTy, unUsgTy, tyUsg,
39 mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
40 isForAllTy, applyTy, applyTys, mkPiType,
42 TauType, RhoType, SigmaType, ThetaType,
45 mkSigmaTy, splitSigmaTy,
48 isUnLiftedType, isUnboxedType, isUnboxedTupleType, isAlgType, isDataType,
52 tyVarsOfType, tyVarsOfTypes, namesOfType, typeKind,
55 -- Tidying up for printing
57 tidyOpenType, tidyOpenTypes,
58 tidyTyVar, tidyTyVars,
62 #include "HsVersions.h"
64 import {-# SOURCE #-} DataCon( DataCon, dataConType )
65 import {-# SOURCE #-} PprType( pprType ) -- Only called in debug messages
66 import {-# SOURCE #-} Subst ( mkTyVarSubst, substTy )
69 import Var ( Id, TyVar, IdOrTyVar, UVar,
70 tyVarKind, tyVarName, isId, idType, setTyVarName, setVarOcc
75 import Name ( NamedThing(..), Provenance(..), ExportFlag(..),
76 mkWiredInTyConName, mkGlobalName, mkLocalName, mkKindOccFS, tcName,
77 tidyOccName, TidyOccEnv
80 import Class ( classTyCon, Class )
81 import TyCon ( TyCon, KindCon,
82 mkFunTyCon, mkKindCon, mkSuperKindCon,
83 matchesTyCon, isUnboxedTupleTyCon, isUnLiftedTyCon,
84 isFunTyCon, isDataTyCon, isNewTyCon,
85 isAlgTyCon, isSynTyCon, tyConArity,
86 tyConKind, tyConDataCons, getSynTyConDefn,
87 tyConPrimRep, tyConClass_maybe
91 import BasicTypes ( Unused )
92 import SrcLoc ( mkBuiltinSrcLoc, noSrcLoc )
93 import PrelMods ( pREL_GHC )
94 import Maybes ( maybeToBool )
95 import PrimRep ( PrimRep(..), isFollowableRep )
96 import Unique -- quite a few *Keys
97 import Util ( thenCmp, mapAccumL, seqList, ($!) )
102 %************************************************************************
104 \subsection{Type Classifications}
106 %************************************************************************
110 *unboxed* iff its representation is other than a pointer
111 Unboxed types cannot instantiate a type variable.
112 Unboxed types are always unlifted.
114 *lifted* A type is lifted iff it has bottom as an element.
115 Closures always have lifted types: i.e. any
116 let-bound identifier in Core must have a lifted
117 type. Operationally, a lifted object is one that
119 (NOTE: previously "pointed").
121 *algebraic* A type with one or more constructors, whether declared
122 with "data" or "newtype".
123 An algebraic type is one that can be deconstructed
124 with a case expression.
125 *NOT* the same as lifted types, because we also
126 include unboxed tuples in this classification.
128 *data* A type declared with "data". Also boxed tuples.
130 *primitive* iff it is a built-in type that can't be expressed
133 Currently, all primitive types are unlifted, but that's not necessarily
134 the case. (E.g. Int could be primitive.)
136 Some primitive types are unboxed, such as Int#, whereas some are boxed
137 but unlifted (such as ByteArray#). The only primitive types that we
138 classify as algebraic are the unboxed tuples.
140 examples of type classifications:
142 Type primitive boxed lifted algebraic
143 -----------------------------------------------------------------------------
145 ByteArray# Yes Yes No No
146 (# a, b #) Yes No No Yes
147 ( a, b ) No Yes Yes Yes
150 %************************************************************************
152 \subsection{The data type}
154 %************************************************************************
158 type SuperKind = Type
161 type TyVarSubst = TyVarEnv Type
167 Type -- Function is *not* a TyConApp
170 | TyConApp -- Application of a TyCon
171 TyCon -- *Invariant* saturated appliations of FunTyCon and
172 -- synonyms have their own constructors, below.
173 [Type] -- Might not be saturated.
175 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
179 | NoteTy -- Saturated application of a type synonym
181 Type -- The expanded version
188 = SynNote Type -- The unexpanded version of the type synonym; always a TyConApp
189 | FTVNote TyVarSet -- The free type variables of the noted expression
190 | UsgNote UsageAnn -- The usage annotation at this node
193 = UsOnce -- Used at most once
194 | UsMany -- Used possibly many times (no info; this annotation can be omitted)
195 | UsVar UVar -- Annotation is variable (should only happen inside analysis)
199 %************************************************************************
203 %************************************************************************
211 kv :: KX is a kind variable
217 | AnyBox -- Used *only* for special built-in things
218 -- like error :: forall (a::*?). String -> a
219 -- Here, the 'a' can be instantiated to a boxed or
223 bxv :: BX is a boxity variable
227 | sk -> sk -- In ptic (BX -> KX)
230 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
231 (LocalDef mkBuiltinSrcLoc NotExported)
232 -- mk_kind_name is a bit of a hack
233 -- The LocalDef means that we print the name without
234 -- a qualifier, which is what we want for these kinds.
235 -- It's used for both Kinds and Boxities
241 superKind :: SuperKind -- KX, the type of all kinds
242 superKindName = mk_kind_name kindConKey SLIT("KX")
243 superKind = TyConApp (mkSuperKindCon superKindName) []
245 superBoxity :: SuperKind -- BX, the type of all boxities
246 superBoxityName = mk_kind_name boxityConKey SLIT("BX")
247 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
250 Define Boxed, Unboxed, AnyBox
253 boxedKind, unboxedKind, anyBoxKind :: Kind -- Of superkind superBoxity
255 boxedConName = mk_kind_name boxedConKey SLIT("*")
256 boxedKind = TyConApp (mkKindCon boxedConName superBoxity) []
258 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
259 unboxedKind = TyConApp (mkKindCon unboxedConName superBoxity) []
261 anyBoxConName = mk_kind_name anyBoxConKey SLIT("?")
262 anyBoxCon = mkKindCon anyBoxConName superBoxity -- A kind of wild card
263 anyBoxKind = TyConApp anyBoxCon []
270 typeConName = mk_kind_name typeConKey SLIT("Type")
271 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
274 Define (Type Boxed), (Type Unboxed), (Type AnyBox)
277 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind
278 boxedTypeKind = TyConApp typeCon [boxedKind]
279 unboxedTypeKind = TyConApp typeCon [unboxedKind]
280 openTypeKind = TyConApp typeCon [anyBoxKind]
282 mkArrowKind :: Kind -> Kind -> Kind
283 mkArrowKind k1 k2 = k1 `FunTy` k2
285 mkArrowKinds :: [Kind] -> Kind -> Kind
286 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
290 hasMoreBoxityInfo :: Kind -> Kind -> Bool
291 hasMoreBoxityInfo k1 k2
292 | k2 == openTypeKind = ASSERT( is_type_kind k1) True
293 | otherwise = k1 == k2
295 -- Returns true for things of form (Type x)
296 is_type_kind k = case splitTyConApp_maybe k of
297 Just (tc,[_]) -> tc == typeCon
302 %************************************************************************
304 \subsection{Wired-in type constructors
306 %************************************************************************
308 We define a few wired-in type constructors here to avoid module knots
311 funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon
312 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
317 %************************************************************************
319 \subsection{Constructor-specific functions}
321 %************************************************************************
324 ---------------------------------------------------------------------
328 mkTyVarTy :: TyVar -> Type
331 mkTyVarTys :: [TyVar] -> [Type]
332 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
334 getTyVar :: String -> Type -> TyVar
335 getTyVar msg (TyVarTy tv) = tv
336 getTyVar msg (NoteTy _ t) = getTyVar msg t
337 getTyVar msg other = panic ("getTyVar: " ++ msg)
339 getTyVar_maybe :: Type -> Maybe TyVar
340 getTyVar_maybe (TyVarTy tv) = Just tv
341 getTyVar_maybe (NoteTy _ t) = getTyVar_maybe t
342 getTyVar_maybe other = Nothing
344 isTyVarTy :: Type -> Bool
345 isTyVarTy (TyVarTy tv) = True
346 isTyVarTy (NoteTy _ ty) = isTyVarTy ty
347 isTyVarTy other = False
351 ---------------------------------------------------------------------
354 We need to be pretty careful with AppTy to make sure we obey the
355 invariant that a TyConApp is always visibly so. mkAppTy maintains the
359 mkAppTy orig_ty1 orig_ty2 = ASSERT2( isNotUsgTy orig_ty1 && isNotUsgTy orig_ty2, pprType orig_ty1 <+> text "to" <+> pprType orig_ty2 )
362 mk_app (NoteTy _ ty1) = mk_app ty1
363 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
364 mk_app ty1 = AppTy orig_ty1 orig_ty2
366 mkAppTys :: Type -> [Type] -> Type
367 mkAppTys orig_ty1 [] = orig_ty1
368 -- This check for an empty list of type arguments
369 -- avoids the needless of a type synonym constructor.
370 -- For example: mkAppTys Rational []
371 -- returns to (Ratio Integer), which has needlessly lost
372 -- the Rational part.
373 mkAppTys orig_ty1 orig_tys2 = ASSERT2( isNotUsgTy orig_ty1, pprType orig_ty1 )
376 mk_app (NoteTy _ ty1) = mk_app ty1
377 mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
378 mk_app ty1 = ASSERT2( all isNotUsgTy orig_tys2, pprType orig_ty1 <+> text "to" <+> hsep (map pprType orig_tys2) )
379 foldl AppTy orig_ty1 orig_tys2
381 splitAppTy_maybe :: Type -> Maybe (Type, Type)
382 splitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
383 splitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
384 splitAppTy_maybe (NoteTy _ ty) = splitAppTy_maybe ty
385 splitAppTy_maybe (TyConApp tc []) = Nothing
386 splitAppTy_maybe (TyConApp tc tys) = split tys []
388 split [ty2] acc = Just (TyConApp tc (reverse acc), ty2)
389 split (ty:tys) acc = split tys (ty:acc)
391 splitAppTy_maybe other = Nothing
393 splitAppTy :: Type -> (Type, Type)
394 splitAppTy ty = case splitAppTy_maybe ty of
396 Nothing -> panic "splitAppTy"
398 splitAppTys :: Type -> (Type, [Type])
399 splitAppTys ty = split ty ty []
401 split orig_ty (AppTy ty arg) args = split ty ty (arg:args)
402 split orig_ty (NoteTy _ ty) args = split orig_ty ty args
403 split orig_ty (FunTy ty1 ty2) args = ASSERT( null args )
404 (TyConApp funTyCon [], [ty1,ty2])
405 split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
406 split orig_ty ty args = (orig_ty, args)
410 ---------------------------------------------------------------------
415 mkFunTy :: Type -> Type -> Type
416 mkFunTy arg res = FunTy arg res
418 mkFunTys :: [Type] -> Type -> Type
419 mkFunTys tys ty = foldr FunTy ty tys
421 splitFunTy_maybe :: Type -> Maybe (Type, Type)
422 splitFunTy_maybe (FunTy arg res) = Just (arg, res)
423 splitFunTy_maybe (NoteTy _ ty) = splitFunTy_maybe ty
424 splitFunTy_maybe other = Nothing
426 splitFunTys :: Type -> ([Type], Type)
427 splitFunTys ty = split [] ty ty
429 split args orig_ty (FunTy arg res) = split (arg:args) res res
430 split args orig_ty (NoteTy _ ty) = split args orig_ty ty
431 split args orig_ty ty = (reverse args, orig_ty)
433 splitFunTysN :: String -> Int -> Type -> ([Type], Type)
434 splitFunTysN msg orig_n orig_ty = split orig_n [] orig_ty orig_ty
436 split 0 args syn_ty ty = (reverse args, syn_ty)
437 split n args syn_ty (FunTy arg res) = split (n-1) (arg:args) res res
438 split n args syn_ty (NoteTy _ ty) = split n args syn_ty ty
439 split n args syn_ty ty = pprPanic ("splitFunTysN: " ++ msg) (int orig_n <+> pprType orig_ty)
441 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
442 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
444 split acc [] nty ty = (reverse acc, nty)
445 split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res
446 split acc xs nty (NoteTy _ ty) = split acc xs nty ty
447 split acc (x:xs) nty ty = pprPanic "zipFunTys" (ppr orig_xs <+> pprType orig_ty)
449 funResultTy :: Type -> Type
450 funResultTy (FunTy arg res) = res
451 funResultTy (NoteTy _ ty) = funResultTy ty
452 funResultTy ty = pprPanic "funResultTy" (pprType ty)
456 ---------------------------------------------------------------------
461 mkTyConApp :: TyCon -> [Type] -> Type
463 | isFunTyCon tycon && length tys == 2
465 (ty1:ty2:_) -> FunTy ty1 ty2
468 = ASSERT(not (isSynTyCon tycon))
471 mkTyConTy :: TyCon -> Type
472 mkTyConTy tycon = ASSERT( not (isSynTyCon tycon) )
475 -- splitTyConApp "looks through" synonyms, because they don't
476 -- mean a distinct type, but all other type-constructor applications
477 -- including functions are returned as Just ..
479 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
480 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
481 splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
482 splitTyConApp_maybe (NoteTy _ ty) = splitTyConApp_maybe ty
483 splitTyConApp_maybe other = Nothing
485 -- splitAlgTyConApp_maybe looks for
486 -- *saturated* applications of *algebraic* data types
487 -- "Algebraic" => newtype, data type, or dictionary (not function types)
488 -- We return the constructors too.
490 splitAlgTyConApp_maybe :: Type -> Maybe (TyCon, [Type], [DataCon])
491 splitAlgTyConApp_maybe (TyConApp tc tys)
493 tyConArity tc == length tys = Just (tc, tys, tyConDataCons tc)
494 splitAlgTyConApp_maybe (NoteTy _ ty) = splitAlgTyConApp_maybe ty
495 splitAlgTyConApp_maybe other = Nothing
497 splitAlgTyConApp :: Type -> (TyCon, [Type], [DataCon])
498 -- Here the "algebraic" property is an *assertion*
499 splitAlgTyConApp (TyConApp tc tys) = ASSERT( isAlgTyCon tc && tyConArity tc == length tys )
500 (tc, tys, tyConDataCons tc)
501 splitAlgTyConApp (NoteTy _ ty) = splitAlgTyConApp ty
504 "Dictionary" types are just ordinary data types, but you can
505 tell from the type constructor whether it's a dictionary or not.
508 mkDictTy :: Class -> [Type] -> Type
509 mkDictTy clas tys = TyConApp (classTyCon clas) tys
511 splitDictTy_maybe :: Type -> Maybe (Class, [Type])
512 splitDictTy_maybe (TyConApp tc tys)
513 | maybeToBool maybe_class
514 && tyConArity tc == length tys = Just (clas, tys)
516 maybe_class = tyConClass_maybe tc
517 Just clas = maybe_class
519 splitDictTy_maybe (NoteTy _ ty) = splitDictTy_maybe ty
520 splitDictTy_maybe other = Nothing
522 isDictTy :: Type -> Bool
523 -- This version is slightly more efficient than (maybeToBool . splitDictTy)
524 isDictTy (TyConApp tc tys)
525 | maybeToBool (tyConClass_maybe tc)
526 && tyConArity tc == length tys
528 isDictTy (NoteTy _ ty) = isDictTy ty
529 isDictTy other = False
532 splitRepTyConApp_maybe is like splitTyConApp_maybe except
533 that it looks through
536 in addition to synonyms. It's useful in the back end where we're not
537 interested in newtypes anymore.
540 splitRepTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
541 splitRepTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
542 splitRepTyConApp_maybe (NoteTy _ ty) = splitRepTyConApp_maybe ty
543 splitRepTyConApp_maybe (ForAllTy _ ty) = splitRepTyConApp_maybe ty
544 splitRepTyConApp_maybe (TyConApp tc tys)
546 = case splitFunTy_maybe (applyTys (dataConType (head (tyConDataCons tc))) tys) of
547 Just (rep_ty, _) -> splitRepTyConApp_maybe rep_ty
550 splitRepTyConApp_maybe other = Nothing
553 ---------------------------------------------------------------------
558 mkSynTy syn_tycon tys
559 = ASSERT( isSynTyCon syn_tycon )
560 ASSERT( isNotUsgTy body )
561 NoteTy (SynNote (TyConApp syn_tycon tys))
562 (substTy (mkTyVarSubst tyvars tys) body)
564 (tyvars, body) = getSynTyConDefn syn_tycon
566 isSynTy (NoteTy (SynNote _) _) = True
567 isSynTy other = False
569 deNoteType :: Type -> Type
570 -- Sorry for the cute name
571 deNoteType ty@(TyVarTy tyvar) = ty
572 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
573 deNoteType (NoteTy _ ty) = deNoteType ty
574 deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
575 deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
576 deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
579 Notes on type synonyms
580 ~~~~~~~~~~~~~~~~~~~~~~
581 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
582 to return type synonyms whereever possible. Thus
587 splitFunTys (a -> Foo a) = ([a], Foo a)
590 The reason is that we then get better (shorter) type signatures in
591 interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs.
596 ---------------------------------------------------------------------
600 NB: Invariant: if present, usage note is at the very top of the type.
601 This should be carefully preserved.
603 In some parts of the compiler, comments use the _Once Upon a
604 Polymorphic Type_ (POPL'99) usage of "sigma = usage-annotated type;
605 tau = un-usage-annotated type"; unfortunately this conflicts with the
606 rho/tau/theta/sigma usage in the rest of the compiler.
610 mkUsgTy :: UsageAnn -> Type -> Type
612 mkUsgTy UsMany ty = ASSERT2( isNotUsgTy ty, pprType ty )
615 mkUsgTy usg ty = ASSERT2( isNotUsgTy ty, pprType ty )
616 NoteTy (UsgNote usg) ty
618 -- The isUsgTy function is utterly useless if UsManys are omitted.
619 -- Be warned! KSW 1999-04.
620 isUsgTy :: Type -> Bool
624 isUsgTy (NoteTy (UsgNote _) _) = True
625 isUsgTy other = False
628 -- The isNotUsgTy function may return a false True if UsManys are omitted;
629 -- in other words, A SSERT( isNotUsgTy ty ) may be useful but
630 -- A SSERT( not (isNotUsg ty) ) is asking for trouble. KSW 1999-04.
631 isNotUsgTy :: Type -> Bool
632 isNotUsgTy (NoteTy (UsgNote _) _) = False
633 isNotUsgTy other = True
635 -- splitUsgTy_maybe is not exported, since it is meaningless if
636 -- UsManys are omitted. It is used in several places in this module,
637 -- however. KSW 1999-04.
638 splitUsgTy_maybe :: Type -> Maybe (UsageAnn,Type)
639 splitUsgTy_maybe (NoteTy (UsgNote usg) ty2) = ASSERT( isNotUsgTy ty2 )
641 splitUsgTy_maybe ty = Nothing
643 splitUsgTy :: Type -> (UsageAnn,Type)
644 splitUsgTy ty = case splitUsgTy_maybe ty of
650 pprPanic "splitUsgTy: no usage annot:" $ pprType ty
653 tyUsg :: Type -> UsageAnn
654 tyUsg = fst . splitUsgTy
656 unUsgTy :: Type -> Type
657 -- strip outer usage annotation if present
658 unUsgTy ty = case splitUsgTy_maybe ty of
659 Just (_,ty1) -> ASSERT2( isNotUsgTy ty1, pprType ty )
666 ---------------------------------------------------------------------
670 We need to be clever here with usage annotations; they need to be
671 lifted or lowered through the forall as appropriate.
674 mkForAllTy :: TyVar -> Type -> Type
675 mkForAllTy tyvar ty = case splitUsgTy_maybe ty of
676 Just (usg,ty') -> NoteTy (UsgNote usg)
678 Nothing -> ForAllTy tyvar ty
680 mkForAllTys :: [TyVar] -> Type -> Type
681 mkForAllTys tyvars ty = case splitUsgTy_maybe ty of
682 Just (usg,ty') -> NoteTy (UsgNote usg)
683 (foldr ForAllTy ty' tyvars)
684 Nothing -> foldr ForAllTy ty tyvars
686 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
687 splitForAllTy_maybe ty = case splitUsgTy_maybe ty of
688 Just (usg,ty') -> do (tyvar,ty'') <- splitFAT_m ty'
689 return (tyvar, NoteTy (UsgNote usg) ty'')
690 Nothing -> splitFAT_m ty
692 splitFAT_m (NoteTy _ ty) = splitFAT_m ty
693 splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty)
694 splitFAT_m _ = Nothing
696 isForAllTy :: Type -> Bool
697 isForAllTy (NoteTy _ ty) = isForAllTy ty
698 isForAllTy (ForAllTy tyvar ty) = True
701 splitForAllTys :: Type -> ([TyVar], Type)
702 splitForAllTys ty = case splitUsgTy_maybe ty of
703 Just (usg,ty') -> let (tvs,ty'') = split ty' ty' []
704 in (tvs, NoteTy (UsgNote usg) ty'')
705 Nothing -> split ty ty []
707 split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
708 split orig_ty (NoteTy _ ty) tvs = split orig_ty ty tvs
709 split orig_ty t tvs = (reverse tvs, orig_ty)
712 @mkPiType@ makes a (->) type or a forall type, depending on whether
713 it is given a type variable or a term variable.
716 mkPiType :: IdOrTyVar -> Type -> Type -- The more polymorphic version doesn't work...
717 mkPiType v ty | isId v = mkFunTy (idType v) ty
718 | otherwise = mkForAllTy v ty
721 Applying a for-all to its arguments
724 applyTy :: Type -> Type -> Type
725 applyTy (NoteTy note@(UsgNote _) fun) arg = NoteTy note (applyTy fun arg)
726 applyTy (NoteTy _ fun) arg = applyTy fun arg
727 applyTy (ForAllTy tv ty) arg = ASSERT( isNotUsgTy arg )
728 substTy (mkTyVarSubst [tv] [arg]) ty
729 applyTy other arg = panic "applyTy"
731 applyTys :: Type -> [Type] -> Type
732 applyTys fun_ty arg_tys
733 = substTy (mkTyVarSubst tvs arg_tys) ty
735 (tvs, ty) = split fun_ty arg_tys
737 split fun_ty [] = ([], fun_ty)
738 split (NoteTy _ fun_ty) args = split fun_ty args
739 split (ForAllTy tv fun_ty) (arg:args) = ASSERT2( isNotUsgTy arg, vcat (map pprType arg_tys) $$
740 text "in application of" <+> pprType fun_ty)
741 case split fun_ty args of
742 (tvs, ty) -> (tv:tvs, ty)
743 split other_ty args = panic "applyTys"
745 {- OLD version with bogus usage stuff
747 ************* CHECK WITH KEITH **************
749 go env ty [] = substTy (mkVarEnv env) ty
750 go env (NoteTy note@(UsgNote _) fun)
751 args = NoteTy note (go env fun args)
752 go env (NoteTy _ fun) args = go env fun args
753 go env (ForAllTy tv ty) (arg:args) = go ((tv,arg):env) ty args
754 go env other args = panic "applyTys"
758 Note that we allow applications to be of usage-annotated- types, as an
759 extension: we handle them by lifting the annotation outside. The
760 argument, however, must still be unannotated.
762 %************************************************************************
764 \subsection{Stuff to do with the source-language types}
766 %************************************************************************
771 type ThetaType = [(Class, [Type])]
772 type SigmaType = Type
775 @isTauTy@ tests for nested for-alls.
778 isTauTy :: Type -> Bool
779 isTauTy (TyVarTy v) = True
780 isTauTy (TyConApp _ tys) = all isTauTy tys
781 isTauTy (AppTy a b) = isTauTy a && isTauTy b
782 isTauTy (FunTy a b) = isTauTy a && isTauTy b
783 isTauTy (NoteTy _ ty) = isTauTy ty
784 isTauTy other = False
788 mkRhoTy :: [(Class, [Type])] -> Type -> Type
789 mkRhoTy theta ty = foldr (\(c,t) r -> FunTy (mkDictTy c t) r) ty theta
791 splitRhoTy :: Type -> ([(Class, [Type])], Type)
792 splitRhoTy ty = split ty ty []
794 split orig_ty (FunTy arg res) ts = case splitDictTy_maybe arg of
795 Just pair -> split res res (pair:ts)
796 Nothing -> (reverse ts, orig_ty)
797 split orig_ty (NoteTy _ ty) ts = split orig_ty ty ts
798 split orig_ty ty ts = (reverse ts, orig_ty)
804 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
806 splitSigmaTy :: Type -> ([TyVar], [(Class, [Type])], Type)
810 (tyvars,rho) = splitForAllTys ty
811 (theta,tau) = splitRhoTy rho
815 %************************************************************************
817 \subsection{Kinds and free variables}
819 %************************************************************************
821 ---------------------------------------------------------------------
822 Finding the kind of a type
823 ~~~~~~~~~~~~~~~~~~~~~~~~~~
825 typeKind :: Type -> Kind
827 typeKind (TyVarTy tyvar) = tyVarKind tyvar
828 typeKind (TyConApp tycon tys) = foldr (\_ k -> funResultTy k) (tyConKind tycon) tys
829 typeKind (NoteTy _ ty) = typeKind ty
830 typeKind (AppTy fun arg) = funResultTy (typeKind fun)
832 typeKind (FunTy arg res) = boxedTypeKind -- A function is boxed regardless of its result type
833 -- No functions at the type level, hence we don't need
834 -- to say (typeKind res).
836 typeKind (ForAllTy tv ty) = typeKind ty
840 ---------------------------------------------------------------------
841 Free variables of a type
842 ~~~~~~~~~~~~~~~~~~~~~~~~
844 tyVarsOfType :: Type -> TyVarSet
846 tyVarsOfType (TyVarTy tv) = unitVarSet tv
847 tyVarsOfType (TyConApp tycon tys) = tyVarsOfTypes tys
848 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
849 tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty1
850 tyVarsOfType (NoteTy (UsgNote _) ty) = tyVarsOfType ty
851 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
852 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
853 tyVarsOfType (ForAllTy tyvar ty) = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
855 tyVarsOfTypes :: [Type] -> TyVarSet
856 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
858 -- Add a Note with the free tyvars to the top of the type
859 -- (but under a usage if there is one)
860 addFreeTyVars :: Type -> Type
861 addFreeTyVars (NoteTy note@(UsgNote _) ty) = NoteTy note (addFreeTyVars ty)
862 addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty
863 addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty
865 -- Find the free names of a type, including the type constructors and classes it mentions
866 namesOfType :: Type -> NameSet
867 namesOfType (TyVarTy tv) = unitNameSet (getName tv)
868 namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets`
870 namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
871 namesOfType (NoteTy other_note ty2) = namesOfType ty2
872 namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
873 namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
874 namesOfType (ForAllTy tyvar ty) = namesOfType ty `minusNameSet` unitNameSet (getName tyvar)
876 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
880 %************************************************************************
882 \subsection{TidyType}
884 %************************************************************************
886 tidyTy tidies up a type for printing in an error message, or in
889 It doesn't change the uniques at all, just the print names.
892 tidyTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
893 tidyTyVar env@(tidy_env, subst) tyvar
894 = case lookupVarEnv subst tyvar of
896 Just tyvar' -> -- Already substituted
899 Nothing -> -- Make a new nice name for it
901 case tidyOccName tidy_env (getOccName name) of
902 (tidy', occ') -> -- New occname reqd
903 ((tidy', subst'), tyvar')
905 subst' = extendVarEnv subst tyvar tyvar'
906 tyvar' = setTyVarName tyvar name'
907 name' = mkLocalName (getUnique name) occ' noSrcLoc
908 -- Note: make a *user* tyvar, so it printes nicely
909 -- Could extract src loc, but no need.
911 name = tyVarName tyvar
913 tidyTyVars env tyvars = mapAccumL tidyTyVar env tyvars
915 tidyType :: TidyEnv -> Type -> Type
916 tidyType env@(tidy_env, subst) ty
919 go (TyVarTy tv) = case lookupVarEnv subst tv of
920 Nothing -> TyVarTy tv
921 Just tv' -> TyVarTy tv'
922 go (TyConApp tycon tys) = let args = map go tys
923 in args `seqList` TyConApp tycon args
924 go (NoteTy note ty) = (NoteTy $! (go_note note)) $! (go ty)
925 go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
926 go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
927 go (ForAllTy tv ty) = ForAllTy tv' $! (tidyType env' ty)
929 (env', tv') = tidyTyVar env tv
931 go_note (SynNote ty) = SynNote $! (go ty)
932 go_note note@(FTVNote ftvs) = note -- No need to tidy the free tyvars
933 go_note note@(UsgNote _) = note -- Usage annotation is already tidy
935 tidyTypes env tys = map (tidyType env) tys
939 @tidyOpenType@ grabs the free type varibles, tidies them
940 and then uses @tidyType@ to work over the type itself
943 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
945 = (env', tidyType env' ty)
947 env' = foldl go env (varSetElems (tyVarsOfType ty))
948 go env tyvar = fst (tidyTyVar env tyvar)
950 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
951 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
953 tidyTopType :: Type -> Type
954 tidyTopType ty = tidyType emptyTidyEnv ty
958 %************************************************************************
960 \subsection{Boxedness and liftedness}
962 %************************************************************************
965 isUnboxedType :: Type -> Bool
966 isUnboxedType ty = not (isFollowableRep (typePrimRep ty))
968 isUnLiftedType :: Type -> Bool
969 isUnLiftedType ty = case splitTyConApp_maybe ty of
970 Just (tc, ty_args) -> isUnLiftedTyCon tc
973 isUnboxedTupleType :: Type -> Bool
974 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
975 Just (tc, ty_args) -> isUnboxedTupleTyCon tc
978 -- Should only be applied to *types*; hence the assert
979 isAlgType :: Type -> Bool
980 isAlgType ty = case splitTyConApp_maybe ty of
981 Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
985 -- Should only be applied to *types*; hence the assert
986 isDataType :: Type -> Bool
987 isDataType ty = case splitTyConApp_maybe ty of
988 Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
992 typePrimRep :: Type -> PrimRep
993 typePrimRep ty = case splitTyConApp_maybe ty of
994 Just (tc, ty_args) -> tyConPrimRep tc
998 %************************************************************************
1000 \subsection{Equality on types}
1002 %************************************************************************
1004 For the moment at least, type comparisons don't work if
1005 there are embedded for-alls.
1008 instance Eq Type where
1009 ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
1011 instance Ord Type where
1012 compare ty1 ty2 = cmpTy ty1 ty2
1014 cmpTy :: Type -> Type -> Ordering
1016 = cmp emptyVarEnv ty1 ty2
1018 -- The "env" maps type variables in ty1 to type variables in ty2
1019 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
1020 -- we in effect substitute tv2 for tv1 in t1 before continuing
1021 lookup env tv1 = case lookupVarEnv env tv1 of
1025 -- Get rid of NoteTy
1026 cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2
1027 cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2
1029 -- Deal with equal constructors
1030 cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2
1031 cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
1032 cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
1033 cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2)
1034 cmp env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmp (extendVarEnv env tv1 tv2) t1 t2
1036 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy
1037 cmp env (AppTy _ _) (TyVarTy _) = GT
1039 cmp env (FunTy _ _) (TyVarTy _) = GT
1040 cmp env (FunTy _ _) (AppTy _ _) = GT
1042 cmp env (TyConApp _ _) (TyVarTy _) = GT
1043 cmp env (TyConApp _ _) (AppTy _ _) = GT
1044 cmp env (TyConApp _ _) (FunTy _ _) = GT
1046 cmp env (ForAllTy _ _) other = GT
1051 cmps env (t:ts) [] = GT
1052 cmps env [] (t:ts) = LT
1053 cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s