2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TypeRep]{Type - friends' interface}
8 Type(..), TyNote(..), PredType(..), -- Representation visible to friends
10 Kind, ThetaType, RhoType, TauType, SigmaType, -- Synonyms
13 superKind, superBoxity, -- KX and BX respectively
14 boxedBoxity, unboxedBoxity, -- :: BX
16 typeCon, -- :: BX -> KX
17 boxedTypeKind, unboxedTypeKind, openTypeKind, -- :: KX
18 mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
20 usageKindCon, -- :: KX
21 usageTypeKind, -- :: KX
22 usOnceTyCon, usManyTyCon, -- :: $
23 usOnce, usMany, -- :: $
28 #include "HsVersions.h"
35 import Name ( Name, mkGlobalName, mkKindOccFS, tcName )
36 import OccName ( tcName )
37 import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
38 import Class ( Class )
41 import SrcLoc ( builtinSrcLoc )
42 import PrelNames ( pREL_GHC, superKindName, superBoxityName, boxedConName,
43 unboxedConName, typeConName, openKindConName, funTyConName,
44 usageKindConName, usOnceTyConName, usManyTyConName
48 %************************************************************************
50 \subsection{Type Classifications}
52 %************************************************************************
56 *unboxed* iff its representation is other than a pointer
57 Unboxed types cannot instantiate a type variable.
58 Unboxed types are always 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
65 (NOTE: previously "pointed").
67 *algebraic* A type with one or more constructors, whether declared
68 with "data" or "newtype".
69 An algebraic type is one that can be deconstructed
70 with a case expression.
71 *NOT* the same as lifted types, because we also
72 include unboxed tuples in this classification.
74 *data* A type declared with "data". Also boxed tuples.
76 *primitive* iff it is a built-in type that can't be expressed
79 Currently, all primitive types are unlifted, but that's not necessarily
80 the case. (E.g. Int could be primitive.)
82 Some primitive types are unboxed, such as Int#, whereas some are boxed
83 but unlifted (such as ByteArray#). The only primitive types that we
84 classify as algebraic are the unboxed tuples.
86 examples of type classifications:
88 Type primitive boxed lifted algebraic
89 -----------------------------------------------------------------------------
91 ByteArray# Yes Yes No No
92 (# a, b #) Yes No No Yes
93 ( a, b ) No Yes Yes Yes
96 %************************************************************************
98 \subsection{The data type}
100 %************************************************************************
104 type SuperKind = Type
107 type TyVarSubst = TyVarEnv Type
113 Type -- Function is *not* a TyConApp
116 | TyConApp -- Application of a TyCon
117 TyCon -- *Invariant* saturated appliations of FunTyCon and
118 -- synonyms have their own constructors, below.
119 [Type] -- Might not be saturated.
121 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
125 | ForAllTy -- A polymorphic type
129 | PredTy -- A Haskell predicate
132 | UsageTy -- A usage-annotated type
133 Type -- - Annotation of kind $ (i.e., usage annotation)
134 Type -- - Annotated type
136 | NoteTy -- A type with a note attached
138 Type -- The expanded version
141 = SynNote Type -- The unexpanded version of the type synonym; always a TyConApp
142 | FTVNote TyVarSet -- The free type variables of the noted expression
144 type ThetaType = [PredType]
147 type SigmaType = Type
150 INVARIANT: UsageTys are optional, but may *only* appear immediately
151 under a FunTy (either argument), or at top-level of a Type permitted
152 to be annotated (such as the type of an Id). NoteTys are transparent
153 for the purposes of this rule.
155 -------------------------------------
158 Consider these examples:
159 f :: (Eq a) => a -> Int
160 g :: (?x :: Int -> Int) => a -> Int
161 h :: (r\l) => {r} => {l::Int | r}
163 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
164 Predicates are represented inside GHC by PredType:
167 data PredType = Class Class [Type]
171 (We don't support TREX records yet, but the setup is designed
172 to expand to allow them.)
174 A Haskell qualified type, such as that for f,g,h above, is
176 * a FunTy for the double arrow
177 * with a PredTy as the function argument
179 The predicate really does turn into a real extra argument to the
180 function. If the argument has type (PredTy p) then the predicate p is
181 represented by evidence (a dictionary, for example, of type (predRepTy p).
184 %************************************************************************
188 %************************************************************************
192 kind :: KX = kind -> kind
194 | Type boxity -- (Type *) is printed as just *
195 -- (Type #) is printed as just #
197 | UsageKind -- Printed '$'; used for usage annotations
199 | OpenKind -- Can be boxed or unboxed
202 | kv -- A kind variable; *only* happens during kind checking
204 boxity :: BX = * -- Boxed
206 | bv -- A boxity variable; *only* happens during kind checking
208 There's a little subtyping at the kind level:
209 forall b. Type b <: OpenKind
211 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
213 OpenKind, written '?', is used as the kind for certain type variables,
216 1. The universally quantified type variable(s) for special built-in
217 things like error :: forall (a::?). String -> a.
218 Here, the 'a' can be instantiated to a boxed or unboxed type.
220 2. Kind '?' is also used when the typechecker needs to create a fresh
221 type variable, one that may very well later be unified with a type.
222 For example, suppose f::a, and we see an application (f x). Then a
223 must be a function type, so we unify a with (b->c). But what kind
224 are b and c? They can be boxed or unboxed types, so we give them kind '?'.
226 When the type checker generalises over a bunch of type variables, it
227 makes any that still have kind '?' into kind '*'. So kind '?' is never
228 present in an inferred type.
232 mk_kind_name key str = mkGlobalName key pREL_GHC (mkKindOccFS tcName str) builtinSrcLoc
233 -- mk_kind_name is a bit of a hack
234 -- The LocalDef means that we print the name without
235 -- a qualifier, which is what we want for these kinds.
236 -- It's used for both Kinds and Boxities
239 ------------------------------------------
240 Define KX, the type of a kind
241 BX, the type of a boxity
244 superKind :: SuperKind -- KX, the type of all kinds
245 superKind = TyConApp (mkSuperKindCon superKindName) []
247 superBoxity :: SuperKind -- BX, the type of all boxities
248 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
251 ------------------------------------------
252 Define boxities: @*@ and @#@
255 boxedBoxity, unboxedBoxity :: Kind -- :: BX
256 boxedBoxity = TyConApp (mkKindCon boxedConName superBoxity) []
258 unboxedBoxity = TyConApp (mkKindCon unboxedConName superBoxity) []
261 ------------------------------------------
262 Define kinds: Type, Type *, Type #, OpenKind, and UsageKind
265 typeCon :: KindCon -- :: BX -> KX
266 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
268 boxedTypeKind, unboxedTypeKind, openTypeKind :: Kind -- Of superkind superKind
270 boxedTypeKind = TyConApp typeCon [boxedBoxity]
271 unboxedTypeKind = TyConApp typeCon [unboxedBoxity]
273 openKindCon = mkKindCon openKindConName superKind
274 openTypeKind = TyConApp openKindCon []
276 usageKindCon = mkKindCon usageKindConName superKind
277 usageTypeKind = TyConApp usageKindCon []
280 ------------------------------------------
284 mkArrowKind :: Kind -> Kind -> Kind
285 mkArrowKind k1 k2 = k1 `FunTy` k2
287 mkArrowKinds :: [Kind] -> Kind -> Kind
288 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
292 %************************************************************************
294 \subsection{Wired-in type constructors
296 %************************************************************************
298 We define a few wired-in type constructors here to avoid module knots
301 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [boxedTypeKind, boxedTypeKind] boxedTypeKind)
304 ------------------------------------------
305 Usage tycons @.@ and @!@
307 The usage tycons are of kind usageTypeKind (`$'). The types contain
308 no values, and are used purely for usage annotation. mk_kind_name is
309 used (hackishly) to avoid z-encoding of the names.
312 usOnceTyCon = mkKindCon usOnceTyConName usageTypeKind
313 usOnce = TyConApp usOnceTyCon []
315 usManyTyCon = mkKindCon usManyTyConName usageTypeKind
316 usMany = TyConApp usManyTyCon []