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 So: non-recursive newtypes are represented using a SourceTy (see below)
122 recursive newtypes are represented using a TyConApp
124 The TyCon still says "I'm a newtype", but we do not represent the
125 newtype application as a SourceType; instead as a TyConApp.
128 %************************************************************************
130 \subsection{The data type}
132 %************************************************************************
136 type SuperKind = Type
140 type TyVarSubst = TyVarEnv Type
146 Type -- Function is *not* a TyConApp
149 | TyConApp -- Application of a TyCon
150 TyCon -- *Invariant* saturated appliations of FunTyCon and
151 -- synonyms have their own constructors, below.
152 [Type] -- Might not be saturated.
154 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
158 | ForAllTy -- A polymorphic type
162 | SourceTy -- A high level source type
163 SourceType -- ...can be expanded to a representation type...
165 | UsageTy -- A usage-annotated type
166 Type -- - Annotation of kind $ (i.e., usage annotation)
167 Type -- - Annotated type
169 | NoteTy -- A type with a note attached
171 Type -- The expanded version
174 = FTVNote TyVarSet -- The free type variables of the noted expression
176 | SynNote Type -- Used for type synonyms
177 -- The Type is always a TyConApp, and is the un-expanded form.
178 -- The type to which the note is attached is the expanded form.
181 INVARIANT: UsageTys are optional, but may *only* appear immediately
182 under a FunTy (either argument), or at top-level of a Type permitted
183 to be annotated (such as the type of an Id). NoteTys are transparent
184 for the purposes of this rule.
186 -------------------------------------
191 represents a value whose type is the Haskell source type sty.
192 It can be expanded into its representation, but:
194 * The type checker must treat it as opaque
195 * The rest of the compiler treats it as transparent
197 There are two main uses
198 a) Haskell predicates
201 Consider these examples:
202 f :: (Eq a) => a -> Int
203 g :: (?x :: Int -> Int) => a -> Int
204 h :: (r\l) => {r} => {l::Int | r}
206 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
207 Predicates are represented inside GHC by PredType:
210 data SourceType = ClassP Class [Type] -- Class predicate
211 | IParam 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, so we give them
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 (mkKindCon liftedConName superBoxity) []
299 unliftedBoxity = TyConApp (mkKindCon unliftedConName superBoxity) []
302 ------------------------------------------
303 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
306 typeCon :: KindCon -- :: BX -> KX
307 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
309 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind
311 liftedTypeKind = TyConApp typeCon [liftedBoxity]
312 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
314 openKindCon = mkKindCon openKindConName superKind
315 openTypeKind = TyConApp openKindCon []
317 usageKindCon = mkKindCon usageKindConName superKind
318 usageTypeKind = TyConApp usageKindCon []
321 ------------------------------------------
325 mkArrowKind :: Kind -> Kind -> Kind
326 mkArrowKind k1 k2 = k1 `FunTy` k2
328 mkArrowKinds :: [Kind] -> Kind -> Kind
329 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
333 %************************************************************************
335 \subsection{Wired-in type constructors
337 %************************************************************************
339 We define a few wired-in type constructors here to avoid module knots
342 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
345 ------------------------------------------
346 Usage tycons @.@ and @!@
348 The usage tycons are of kind usageTypeKind (`$'). The types contain
349 no values, and are used purely for usage annotation.
352 usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
353 usOnce = TyConApp usOnceTyCon []
355 usManyTyCon = mkKindCon usManyTyConName usageTypeKind
356 usMany = TyConApp usManyTyCon []