2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TypeRep]{Type - friends' interface}
8 Type(..), TyNote(..), UsageAnn(..), -- Representation visible to friends
11 superKind, superBoxity, -- KX and BX respectively
12 boxedBoxity, unboxedBoxity, -- :: BX
14 typeCon, -- :: BX -> KX
15 boxedTypeKind, unboxedTypeKind, openTypeKind, -- :: KX
16 mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
21 #include "HsVersions.h"
24 import Var ( TyVar, UVar )
28 import Name ( Name, Provenance(..), ExportFlag(..),
29 mkWiredInTyConName, mkGlobalName, mkKindOccFS, tcName,
31 import TyCon ( TyCon, KindCon,
32 mkFunTyCon, mkKindCon, mkSuperKindCon,
36 import SrcLoc ( mkBuiltinSrcLoc )
37 import PrelNames ( pREL_GHC )
38 import Unique -- quite a few *Keys
39 import Util ( thenCmp )
42 %************************************************************************
44 \subsection{Type Classifications}
46 %************************************************************************
50 *unboxed* iff its representation is other than a pointer
51 Unboxed types cannot instantiate a type variable.
52 Unboxed types are always unlifted.
54 *lifted* A type is lifted iff it has bottom as an element.
55 Closures always have lifted types: i.e. any
56 let-bound identifier in Core must have a lifted
57 type. Operationally, a lifted object is one that
59 (NOTE: previously "pointed").
61 *algebraic* A type with one or more constructors, whether declared
62 with "data" or "newtype".
63 An algebraic type is one that can be deconstructed
64 with a case expression.
65 *NOT* the same as lifted types, because we also
66 include unboxed tuples in this classification.
68 *data* A type declared with "data". Also boxed tuples.
70 *primitive* iff it is a built-in type that can't be expressed
73 Currently, all primitive types are unlifted, but that's not necessarily
74 the case. (E.g. Int could be primitive.)
76 Some primitive types are unboxed, such as Int#, whereas some are boxed
77 but unlifted (such as ByteArray#). The only primitive types that we
78 classify as algebraic are the unboxed tuples.
80 examples of type classifications:
82 Type primitive boxed lifted algebraic
83 -----------------------------------------------------------------------------
85 ByteArray# Yes Yes No No
86 (# a, b #) Yes No No Yes
87 ( a, b ) No Yes Yes Yes
90 %************************************************************************
92 \subsection{The data type}
94 %************************************************************************
101 type TyVarSubst = TyVarEnv Type
107 Type -- Function is *not* a TyConApp
110 | TyConApp -- Application of a TyCon
111 TyCon -- *Invariant* saturated appliations of FunTyCon and
112 -- synonyms have their own constructors, below.
113 [Type] -- Might not be saturated.
115 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
119 | NoteTy -- Saturated application of a type synonym
121 Type -- The expanded version
128 = SynNote Type -- The unexpanded version of the type synonym; always a TyConApp
129 | FTVNote TyVarSet -- The free type variables of the noted expression
130 | UsgNote UsageAnn -- The usage annotation at this node
131 | UsgForAll UVar -- Annotation variable binder
132 | IPNote Name -- It's an implicit parameter
135 = UsOnce -- Used at most once
136 | UsMany -- Used possibly many times (no info; this annotation can be omitted)
137 | UsVar UVar -- Annotation is variable (unbound OK only inside analysis)
141 %************************************************************************
145 %************************************************************************
149 kind :: KX = kind -> kind
150 | Type boxity -- (Type *) is printed as just *
151 -- (Type #) is printed as just #
153 | OpenKind -- Can be boxed or unboxed
156 | kv -- A kind variable; *only* happens during kind checking
158 boxity :: BX = * -- Boxed
160 | bv -- A boxity variable; *only* happens during kind checking
162 There's a little subtyping at the kind level:
163 forall b. Type b <: OpenKind
165 That is, a type of kind (Type b) OK in a context requiring an AnyBox.
167 OpenKind, written '?', is used as the kind for certain type variables,
170 1. The universally quantified type variable(s) for special built-in
171 things like error :: forall (a::?). String -> a.
172 Here, the 'a' can be instantiated to a boxed or unboxed type.
174 2. Kind '?' is also used when the typechecker needs to create a fresh
175 type variable, one that may very well later be unified with a type.
176 For example, suppose f::a, and we see an application (f x). Then a
177 must be a function type, so we unify a with (b->c). But what kind
178 are b and c? They can be boxed or unboxed types, so we give them kind '?'.
180 When the type checker generalises over a bunch of type variables, it
181 makes any that still have kind '?' into kind '*'. So kind '?' is never
182 present in an inferred type.
186 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str)
187 (LocalDef mkBuiltinSrcLoc NotExported)
188 -- mk_kind_name is a bit of a hack
189 -- The LocalDef means that we print the name without
190 -- a qualifier, which is what we want for these kinds.
191 -- It's used for both Kinds and Boxities
194 ------------------------------------------
195 Define KX, the type of a kind
196 BX, the type of a boxity
199 superKind :: SuperKind -- KX, the type of all kinds
200 superKindName = mk_kind_name kindConKey SLIT("KX")
201 superKind = TyConApp (mkSuperKindCon superKindName) []
203 superBoxity :: SuperKind -- BX, the type of all boxities
204 superBoxityName = mk_kind_name boxityConKey SLIT("BX")
205 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
208 ------------------------------------------
209 Define boxities: @*@ and @#@
212 boxedBoxity, unboxedBoxity :: Kind -- :: BX
214 boxedConName = mk_kind_name boxedConKey SLIT("*")
215 boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
217 unboxedConName = mk_kind_name unboxedConKey SLIT("#")
218 unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) []
221 ------------------------------------------
222 Define kinds: Type, Type *, Type #, and OpenKind
225 typeCon :: KindCon -- :: BX -> KX
226 typeConName = mk_kind_name typeConKey SLIT("Type")
227 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
229 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind -- Of superkind superKind
231 boxedTypeKind = TyConApp typeCon [boxedBoxity]
232 unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
234 openKindConName = mk_kind_name anyBoxConKey SLIT("?")
235 openKindCon = mkKindCon openKindConName superKind
236 openTypeKind = TyConApp openKindCon []
239 ------------------------------------------
243 mkArrowKind :: Kind -> Kind -> Kind
244 mkArrowKind k1 k2 = k1 `FunTy` k2
246 mkArrowKinds :: [Kind] -> Kind -> Kind
247 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
251 %************************************************************************
253 \subsection{Wired-in type constructors
255 %************************************************************************
257 We define a few wired-in type constructors here to avoid module knots
260 funTyConName = mkWiredInTyConName funTyConKey pREL_GHC SLIT("(->)") funTyCon
261 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
265 %************************************************************************
267 \subsection{Equality on types}
269 %************************************************************************
271 For the moment at least, type comparisons don't work if
272 there are embedded for-alls.
275 instance Eq Type where
276 ty1 == ty2 = case ty1 `cmpTy` ty2 of { EQ -> True; other -> False }
278 instance Ord Type where
279 compare ty1 ty2 = cmpTy ty1 ty2
281 cmpTy :: Type -> Type -> Ordering
283 = cmp emptyVarEnv ty1 ty2
285 -- The "env" maps type variables in ty1 to type variables in ty2
286 -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
287 -- we in effect substitute tv2 for tv1 in t1 before continuing
288 lookup env tv1 = case lookupVarEnv env tv1 of
293 cmp env (NoteTy _ ty1) ty2 = cmp env ty1 ty2
294 cmp env ty1 (NoteTy _ ty2) = cmp env ty1 ty2
296 -- Deal with equal constructors
297 cmp env (TyVarTy tv1) (TyVarTy tv2) = lookup env tv1 `compare` tv2
298 cmp env (AppTy f1 a1) (AppTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
299 cmp env (FunTy f1 a1) (FunTy f2 a2) = cmp env f1 f2 `thenCmp` cmp env a1 a2
300 cmp env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmps env tys1 tys2)
301 cmp env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmp (extendVarEnv env tv1 tv2) t1 t2
303 -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy
304 cmp env (AppTy _ _) (TyVarTy _) = GT
306 cmp env (FunTy _ _) (TyVarTy _) = GT
307 cmp env (FunTy _ _) (AppTy _ _) = GT
309 cmp env (TyConApp _ _) (TyVarTy _) = GT
310 cmp env (TyConApp _ _) (AppTy _ _) = GT
311 cmp env (TyConApp _ _) (FunTy _ _) = GT
313 cmp env (ForAllTy _ _) other = GT
318 cmps env (t:ts) [] = GT
319 cmps env [] (t:ts) = LT
320 cmps env (t1:t1s) (t2:t2s) = cmp env t1 t2 `thenCmp` cmps env t1s t2s