2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TypeRep]{Type - friends' interface}
8 Type(..), TyNote(..), SourceType(..), -- Representation visible to friends
10 Kind, TauType, PredType, ThetaType, -- Synonyms
13 superKind, superBoxity, -- KX and BX respectively
14 liftedBoxity, unliftedBoxity, -- :: BX
16 typeCon, -- :: BX -> KX
17 liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
18 mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
20 usageKindCon, -- :: KX
21 usageTypeKind, -- :: KX
22 usOnceTyCon, usManyTyCon, -- :: $
23 usOnce, usMany, -- :: $
28 #include "HsVersions.h"
36 import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
37 import Class ( Class )
40 import PrelNames ( superKindName, superBoxityName, liftedConName,
41 unliftedConName, typeConName, openKindConName,
42 usageKindConName, usOnceTyConName, usManyTyConName,
47 %************************************************************************
49 \subsection{Type Classifications}
51 %************************************************************************
55 *unboxed* iff its representation is other than a pointer
56 Unboxed types are also unlifted.
58 *lifted* A type is lifted iff it has bottom as an element.
59 Closures always have lifted types: i.e. any
60 let-bound identifier in Core must have a lifted
61 type. Operationally, a lifted object is one that
64 Only lifted types may be unified with a type variable.
66 *algebraic* A type with one or more constructors, whether declared
67 with "data" or "newtype".
68 An algebraic type is one that can be deconstructed
69 with a case expression.
70 *NOT* the same as lifted types, because we also
71 include unboxed tuples in this classification.
73 *data* A type declared with "data". Also boxed tuples.
75 *primitive* iff it is a built-in type that can't be expressed
78 Currently, all primitive types are unlifted, but that's not necessarily
79 the case. (E.g. Int could be primitive.)
81 Some primitive types are unboxed, such as Int#, whereas some are boxed
82 but unlifted (such as ByteArray#). The only primitive types that we
83 classify as algebraic are the unboxed tuples.
85 examples of type classifications:
87 Type primitive boxed lifted algebraic
88 -----------------------------------------------------------------------------
90 ByteArray# Yes Yes No No
91 (# a, b #) Yes No No Yes
92 ( a, b ) No Yes Yes Yes
97 ----------------------
99 ----------------------
104 Then we want N to be represented as an Int, and that's what we arrange.
105 The front end of the compiler [TcType.lhs] treats N as opaque,
106 the back end treats it as transparent [Type.lhs].
108 There's a bit of a problem with recursive newtypes
110 newtype Q = MkQ (Q->Q)
112 Here the 'implicit expansion' we get from treating P and Q as transparent
113 would give rise to infinite types, which in turn makes eqType diverge.
114 Similarly splitForAllTys and splitFunTys can get into a loop.
116 Solution: for recursive newtypes use a coerce, and treat the newtype
117 and its representation as distinct right through the compiler. That's
118 what you get if you use recursive newtypes. (They are rare, so who
119 cares if they are a tiny bit less efficient.)
121 The TyCon still says "I'm a newtype", but we do not represent the
122 newtype application as a SourceType; instead as a TyConApp.
125 %************************************************************************
127 \subsection{The data type}
129 %************************************************************************
133 type SuperKind = Type
137 type TyVarSubst = TyVarEnv Type
143 Type -- Function is *not* a TyConApp
146 | TyConApp -- Application of a TyCon
147 TyCon -- *Invariant* saturated appliations of FunTyCon and
148 -- synonyms have their own constructors, below.
149 [Type] -- Might not be saturated.
151 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
155 | ForAllTy -- A polymorphic type
159 | SourceTy -- A high level source type
160 SourceType -- ...can be expanded to a representation type...
162 | UsageTy -- A usage-annotated type
163 Type -- - Annotation of kind $ (i.e., usage annotation)
164 Type -- - Annotated 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.
178 INVARIANT: UsageTys are optional, but may *only* appear immediately
179 under a FunTy (either argument), or at top-level of a Type permitted
180 to be annotated (such as the type of an Id). NoteTys are transparent
181 for the purposes of this rule.
183 -------------------------------------
188 represents a value whose type is the Haskell source type sty.
189 It can be expanded into its representation, but:
191 * The type checker must treat it as opaque
192 * The rest of the compiler treats it as transparent
194 There are two main uses
195 a) Haskell predicates
198 Consider these examples:
199 f :: (Eq a) => a -> Int
200 g :: (?x :: Int -> Int) => a -> Int
201 h :: (r\l) => {r} => {l::Int | r}
203 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
204 Predicates are represented inside GHC by PredType:
207 data SourceType = ClassP Class [Type] -- Class predicate
208 | IParam Name Type -- Implicit parameter
209 | NType TyCon [Type] -- A *saturated*, *non-recursive* newtype application
210 -- [See notes at top about newtypes]
212 type PredType = SourceType -- A subtype for predicates
213 type ThetaType = [PredType]
216 (We don't support TREX records yet, but the setup is designed
217 to expand to allow them.)
219 A Haskell qualified type, such as that for f,g,h above, is
221 * a FunTy for the double arrow
222 * with a PredTy as the function argument
224 The predicate really does turn into a real extra argument to the
225 function. If the argument has type (PredTy p) then the predicate p is
226 represented by evidence (a dictionary, for example, of type (predRepTy p).
229 %************************************************************************
233 %************************************************************************
237 kind :: KX = kind -> kind
239 | Type liftedness -- (Type *) is printed as just *
240 -- (Type #) is printed as just #
242 | UsageKind -- Printed '$'; used for usage annotations
244 | OpenKind -- Can be lifted or unlifted
247 | kv -- A kind variable; *only* happens during kind checking
249 boxity :: BX = * -- Lifted
251 | bv -- A boxity variable; *only* happens during kind checking
253 There's a little subtyping at the kind level:
254 forall b. Type b <: OpenKind
256 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
258 OpenKind, written '?', is used as the kind for certain type variables,
261 1. The universally quantified type variable(s) for special built-in
262 things like error :: forall (a::?). String -> a.
263 Here, the 'a' can be instantiated to a lifted or unlifted type.
265 2. Kind '?' is also used when the typechecker needs to create a fresh
266 type variable, one that may very well later be unified with a type.
267 For example, suppose f::a, and we see an application (f x). Then a
268 must be a function type, so we unify a with (b->c). But what kind
269 are b and c? They can be lifted or unlifted types, so we give them
272 When the type checker generalises over a bunch of type variables, it
273 makes any that still have kind '?' into kind '*'. So kind '?' is never
274 present in an inferred type.
277 ------------------------------------------
278 Define KX, the type of a kind
279 BX, the type of a boxity
282 superKind :: SuperKind -- KX, the type of all kinds
283 superKind = TyConApp (mkSuperKindCon superKindName) []
285 superBoxity :: SuperKind -- BX, the type of all boxities
286 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
289 ------------------------------------------
290 Define boxities: @*@ and @#@
293 liftedBoxity, unliftedBoxity :: Kind -- :: BX
294 liftedBoxity = TyConApp (mkKindCon liftedConName superBoxity) []
296 unliftedBoxity = TyConApp (mkKindCon unliftedConName superBoxity) []
299 ------------------------------------------
300 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
303 typeCon :: KindCon -- :: BX -> KX
304 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
306 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind
308 liftedTypeKind = TyConApp typeCon [liftedBoxity]
309 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
311 openKindCon = mkKindCon openKindConName superKind
312 openTypeKind = TyConApp openKindCon []
314 usageKindCon = mkKindCon usageKindConName superKind
315 usageTypeKind = TyConApp usageKindCon []
318 ------------------------------------------
322 mkArrowKind :: Kind -> Kind -> Kind
323 mkArrowKind k1 k2 = k1 `FunTy` k2
325 mkArrowKinds :: [Kind] -> Kind -> Kind
326 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
330 %************************************************************************
332 \subsection{Wired-in type constructors
334 %************************************************************************
336 We define a few wired-in type constructors here to avoid module knots
339 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
342 ------------------------------------------
343 Usage tycons @.@ and @!@
345 The usage tycons are of kind usageTypeKind (`$'). The types contain
346 no values, and are used purely for usage annotation.
349 usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
350 usOnce = TyConApp usOnceTyCon []
352 usManyTyCon = mkKindCon usManyTyConName usageTypeKind
353 usMany = TyConApp usManyTyCon []