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 %************************************************************************
132 \subsection{The data type}
134 %************************************************************************
138 type SuperKind = Type
141 type TyVarSubst = TyVarEnv Type
147 Type -- Function is *not* a TyConApp
150 | TyConApp -- Application of a TyCon
151 TyCon -- *Invariant* saturated appliations of FunTyCon and
152 -- synonyms have their own constructors, below.
153 [Type] -- Might not be saturated.
155 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
159 | ForAllTy -- A polymorphic type
163 | SourceTy -- A high level source type
164 SourceType -- ...can be expanded to a representation type...
166 | NoteTy -- A type with a note attached
168 Type -- The expanded version
171 = FTVNote TyVarSet -- The free type variables of the noted expression
173 | SynNote Type -- Used for type synonyms
174 -- The Type is always a TyConApp, and is the un-expanded form.
175 -- The type to which the note is attached is the expanded form.
179 -------------------------------------
184 represents a value whose type is the Haskell source type sty.
185 It can be expanded into its representation, but:
187 * The type checker must treat it as opaque
188 * The rest of the compiler treats it as transparent
190 There are two main uses
191 a) Haskell predicates
194 Consider these examples:
195 f :: (Eq a) => a -> Int
196 g :: (?x :: Int -> Int) => a -> Int
197 h :: (r\l) => {r} => {l::Int | r}
199 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
200 Predicates are represented inside GHC by PredType:
204 = ClassP Class [Type] -- Class predicate
205 | IParam (IPName Name) Type -- Implicit parameter
206 | NType TyCon [Type] -- A *saturated*, *non-recursive* newtype application
207 -- [See notes at top about newtypes]
209 type PredType = SourceType -- A subtype for predicates
210 type ThetaType = [PredType]
213 (We don't support TREX records yet, but the setup is designed
214 to expand to allow them.)
216 A Haskell qualified type, such as that for f,g,h above, is
218 * a FunTy for the double arrow
219 * with a PredTy as the function argument
221 The predicate really does turn into a real extra argument to the
222 function. If the argument has type (PredTy p) then the predicate p is
223 represented by evidence (a dictionary, for example, of type (predRepTy p).
226 %************************************************************************
230 %************************************************************************
234 kind :: KX = kind -> kind
236 | Type liftedness -- (Type *) is printed as just *
237 -- (Type #) is printed as just #
239 | UsageKind -- Printed '$'; used for usage annotations
241 | OpenKind -- Can be lifted or unlifted
244 | kv -- A kind variable; *only* happens during kind checking
246 boxity :: BX = * -- Lifted
248 | bv -- A boxity variable; *only* happens during kind checking
250 There's a little subtyping at the kind level:
251 forall b. Type b <: OpenKind
253 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
255 OpenKind, written '?', is used as the kind for certain type variables,
258 1. The universally quantified type variable(s) for special built-in
259 things like error :: forall (a::?). String -> a.
260 Here, the 'a' can be instantiated to a lifted or unlifted type.
262 2. Kind '?' is also used when the typechecker needs to create a fresh
263 type variable, one that may very well later be unified with a type.
264 For example, suppose f::a, and we see an application (f x). Then a
265 must be a function type, so we unify a with (b->c). But what kind
266 are b and c? They can be lifted or unlifted types, or indeed type schemes,
267 so we give them kind '?'.
269 When the type checker generalises over a bunch of type variables, it
270 makes any that still have kind '?' into kind '*'. So kind '?' is never
271 present in an inferred type.
274 ------------------------------------------
275 Define KX, the type of a kind
276 BX, the type of a boxity
279 superKind :: SuperKind -- KX, the type of all kinds
280 superKind = TyConApp (mkSuperKindCon superKindName) []
282 superBoxity :: SuperKind -- BX, the type of all boxities
283 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
286 ------------------------------------------
287 Define boxities: @*@ and @#@
290 liftedBoxity, unliftedBoxity :: Kind -- :: BX
291 liftedBoxity = TyConApp liftedBoxityCon []
292 unliftedBoxity = TyConApp unliftedBoxityCon []
294 liftedBoxityCon = mkKindCon liftedConName superBoxity
295 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
298 ------------------------------------------
299 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
302 typeCon :: KindCon -- :: BX -> KX
303 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
305 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind
307 liftedTypeKind = TyConApp typeCon [liftedBoxity]
308 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
310 openKindCon = mkKindCon openKindConName superKind
311 openTypeKind = TyConApp openKindCon []
313 usageKindCon = mkKindCon usageKindConName superKind
314 usageTypeKind = TyConApp usageKindCon []
317 ------------------------------------------
321 mkArrowKind :: Kind -> Kind -> Kind
322 mkArrowKind k1 k2 = k1 `FunTy` k2
324 mkArrowKinds :: [Kind] -> Kind -> Kind
325 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
328 -----------------------------------------------------------------------------
329 Binary kinds for interface files
332 instance Binary Kind where
333 put_ bh k@(TyConApp tc [])
334 | tc == openKindCon = putByte bh 0
335 | tc == usageKindCon = putByte bh 1
336 put_ bh k@(TyConApp tc [TyConApp bc _])
337 | tc == typeCon && bc == liftedBoxityCon = putByte bh 2
338 | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3
339 put_ bh (FunTy f a) = do putByte bh 4; put_ bh f; put_ bh a
340 put_ bh _ = error "Binary.put(Kind): strange-looking Kind"
345 0 -> return openTypeKind
346 1 -> return usageTypeKind
347 2 -> return liftedTypeKind
348 3 -> return unliftedTypeKind
349 _ -> do f <- get bh; a <- get bh; return (FunTy f a)
352 %************************************************************************
354 \subsection{Wired-in type constructors
356 %************************************************************************
358 We define a few wired-in type constructors here to avoid module knots
361 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
364 ------------------------------------------
365 Usage tycons @.@ and @!@
367 The usage tycons are of kind usageTypeKind (`$'). The types contain
368 no values, and are used purely for usage annotation.
371 usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
372 usOnce = TyConApp usOnceTyCon []
374 usManyTyCon = mkKindCon usManyTyConName usageTypeKind
375 usMany = TyConApp usManyTyCon []