2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TypeRep]{Type - friends' interface}
8 Type(..), TyNote(..), -- Representation visible
9 SourceType(..), -- to friends
11 Kind, PredType, ThetaType, -- Synonyms
14 superKind, superBoxity, -- KX and BX respectively
15 liftedBoxity, unliftedBoxity, -- :: BX
17 typeCon, -- :: BX -> KX
18 liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
19 mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
21 usageKindCon, -- :: KX
22 usageTypeKind, -- :: KX
23 usOnceTyCon, usManyTyCon, -- :: $
24 usOnce, usMany, -- :: $
29 #include "HsVersions.h"
33 import VarEnv ( TyVarEnv )
34 import VarSet ( TyVarSet )
36 import BasicTypes ( IPName )
37 import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
38 import Class ( Class )
42 import PrelNames ( superKindName, superBoxityName, liftedConName,
43 unliftedConName, typeConName, openKindConName,
44 usageKindConName, usOnceTyConName, usManyTyConName,
49 %************************************************************************
51 \subsection{Type Classifications}
53 %************************************************************************
57 *unboxed* iff its representation is other than a pointer
58 Unboxed types are also unlifted.
60 *lifted* A type is lifted iff it has bottom as an element.
61 Closures always have lifted types: i.e. any
62 let-bound identifier in Core must have a lifted
63 type. Operationally, a lifted object is one that
66 Only lifted types may be unified with a type variable.
68 *algebraic* A type with one or more constructors, whether declared
69 with "data" or "newtype".
70 An algebraic type is one that can be deconstructed
71 with a case expression.
72 *NOT* the same as lifted types, because we also
73 include unboxed tuples in this classification.
75 *data* A type declared with "data". Also boxed tuples.
77 *primitive* iff it is a built-in type that can't be expressed
80 Currently, all primitive types are unlifted, but that's not necessarily
81 the case. (E.g. Int could be primitive.)
83 Some primitive types are unboxed, such as Int#, whereas some are boxed
84 but unlifted (such as ByteArray#). The only primitive types that we
85 classify as algebraic are the unboxed tuples.
87 examples of type classifications:
89 Type primitive boxed lifted algebraic
90 -----------------------------------------------------------------------------
92 ByteArray# Yes Yes No No
93 (# a, b #) Yes No No Yes
94 ( a, b ) No Yes Yes Yes
99 ----------------------
100 A note about newtypes
101 ----------------------
106 Then we want N to be represented as an Int, and that's what we arrange.
107 The front end of the compiler [TcType.lhs] treats N as opaque,
108 the back end treats it as transparent [Type.lhs].
110 There's a bit of a problem with recursive newtypes
112 newtype Q = MkQ (Q->Q)
114 Here the 'implicit expansion' we get from treating P and Q as transparent
115 would give rise to infinite types, which in turn makes eqType diverge.
116 Similarly splitForAllTys and splitFunTys can get into a loop.
118 Solution: for recursive newtypes use a coerce, and treat the newtype
119 and its representation as distinct right through the compiler. That's
120 what you get if you use recursive newtypes. (They are rare, so who
121 cares if they are a tiny bit less efficient.)
123 So: non-recursive newtypes are represented using a SourceTy (see below)
124 recursive newtypes are represented using a TyConApp
126 The TyCon still says "I'm a newtype", but we do not represent the
127 newtype application as a SourceType; instead as a TyConApp.
130 NOTE: currently [March 02] we regard a newtype as 'recursive' if it's in a
131 mutually recursive group. That's a bit conservative: only if there's a loop
132 consisting only of newtypes do we need consider it as recursive. But it's
133 not so easy to discover that, and the situation isn't that common.
136 %************************************************************************
138 \subsection{The data type}
140 %************************************************************************
144 type SuperKind = Type
147 type TyVarSubst = TyVarEnv Type
153 Type -- Function is *not* a TyConApp
156 | TyConApp -- Application of a TyCon
157 TyCon -- *Invariant* saturated appliations of FunTyCon and
158 -- synonyms have their own constructors, below.
159 [Type] -- Might not be saturated.
161 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
165 | ForAllTy -- A polymorphic type
169 | SourceTy -- A high level source type
170 SourceType -- ...can be expanded to a representation type...
172 | NoteTy -- A type with a note attached
174 Type -- The expanded version
177 = FTVNote TyVarSet -- The free type variables of the noted expression
179 | SynNote Type -- Used for type synonyms
180 -- The Type is always a TyConApp, and is the un-expanded form.
181 -- The type to which the note is attached is the expanded form.
185 -------------------------------------
190 represents a value whose type is the Haskell source type sty.
191 It can be expanded into its representation, but:
193 * The type checker must treat it as opaque
194 * The rest of the compiler treats it as transparent
196 There are two main uses
197 a) Haskell predicates
200 Consider these examples:
201 f :: (Eq a) => a -> Int
202 g :: (?x :: Int -> Int) => a -> Int
203 h :: (r\l) => {r} => {l::Int | r}
205 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
206 Predicates are represented inside GHC by PredType:
210 = ClassP Class [Type] -- Class predicate
211 | IParam (IPName Name) Type -- Implicit parameter
212 | NType TyCon [Type] -- A *saturated*, *non-recursive* newtype application
213 -- [See notes at top about newtypes]
215 type PredType = SourceType -- A subtype for predicates
216 type ThetaType = [PredType]
219 (We don't support TREX records yet, but the setup is designed
220 to expand to allow them.)
222 A Haskell qualified type, such as that for f,g,h above, is
224 * a FunTy for the double arrow
225 * with a PredTy as the function argument
227 The predicate really does turn into a real extra argument to the
228 function. If the argument has type (PredTy p) then the predicate p is
229 represented by evidence (a dictionary, for example, of type (predRepTy p).
232 %************************************************************************
236 %************************************************************************
240 kind :: KX = kind -> kind
242 | Type liftedness -- (Type *) is printed as just *
243 -- (Type #) is printed as just #
245 | UsageKind -- Printed '$'; used for usage annotations
247 | OpenKind -- Can be lifted or unlifted
250 | kv -- A kind variable; *only* happens during kind checking
252 boxity :: BX = * -- Lifted
254 | bv -- A boxity variable; *only* happens during kind checking
256 There's a little subtyping at the kind level:
257 forall b. Type b <: OpenKind
259 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
261 OpenKind, written '?', is used as the kind for certain type variables,
264 1. The universally quantified type variable(s) for special built-in
265 things like error :: forall (a::?). String -> a.
266 Here, the 'a' can be instantiated to a lifted or unlifted type.
268 2. Kind '?' is also used when the typechecker needs to create a fresh
269 type variable, one that may very well later be unified with a type.
270 For example, suppose f::a, and we see an application (f x). Then a
271 must be a function type, so we unify a with (b->c). But what kind
272 are b and c? They can be lifted or unlifted types, or indeed type schemes,
273 so we give them kind '?'.
275 When the type checker generalises over a bunch of type variables, it
276 makes any that still have kind '?' into kind '*'. So kind '?' is never
277 present in an inferred type.
280 ------------------------------------------
281 Define KX, the type of a kind
282 BX, the type of a boxity
285 superKind :: SuperKind -- KX, the type of all kinds
286 superKind = TyConApp (mkSuperKindCon superKindName) []
288 superBoxity :: SuperKind -- BX, the type of all boxities
289 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
292 ------------------------------------------
293 Define boxities: @*@ and @#@
296 liftedBoxity, unliftedBoxity :: Kind -- :: BX
297 liftedBoxity = TyConApp liftedBoxityCon []
298 unliftedBoxity = TyConApp unliftedBoxityCon []
300 liftedBoxityCon = mkKindCon liftedConName superBoxity
301 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
304 ------------------------------------------
305 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
308 typeCon :: KindCon -- :: BX -> KX
309 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
311 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind
313 liftedTypeKind = TyConApp typeCon [liftedBoxity]
314 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
316 openKindCon = mkKindCon openKindConName superKind
317 openTypeKind = TyConApp openKindCon []
319 usageKindCon = mkKindCon usageKindConName superKind
320 usageTypeKind = TyConApp usageKindCon []
323 ------------------------------------------
327 mkArrowKind :: Kind -> Kind -> Kind
328 mkArrowKind k1 k2 = k1 `FunTy` k2
330 mkArrowKinds :: [Kind] -> Kind -> Kind
331 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
334 -----------------------------------------------------------------------------
335 Binary kinds for interface files
338 instance Binary Kind where
339 put_ bh k@(TyConApp tc [])
340 | tc == openKindCon = putByte bh 0
341 | tc == usageKindCon = putByte bh 1
342 put_ bh k@(TyConApp tc [TyConApp bc _])
343 | tc == typeCon && bc == liftedBoxityCon = putByte bh 2
344 | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3
345 put_ bh (FunTy f a) = do putByte bh 4; put_ bh f; put_ bh a
346 put_ bh _ = error "Binary.put(Kind): strange-looking Kind"
351 0 -> return openTypeKind
352 1 -> return usageTypeKind
353 2 -> return liftedTypeKind
354 3 -> return unliftedTypeKind
355 _ -> do f <- get bh; a <- get bh; return (FunTy f a)
358 %************************************************************************
360 \subsection{Wired-in type constructors
362 %************************************************************************
364 We define a few wired-in type constructors here to avoid module knots
367 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [openTypeKind, openTypeKind] liftedTypeKind)
368 -- Functions can take and return either lifted or unlifted types
371 ------------------------------------------
372 Usage tycons @.@ and @!@
374 The usage tycons are of kind usageTypeKind (`$'). The types contain
375 no values, and are used purely for usage annotation.
378 usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
379 usOnce = TyConApp usOnceTyCon []
381 usManyTyCon = mkKindCon usManyTyConName usageTypeKind
382 usMany = TyConApp usManyTyCon []