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
24 #include "HsVersions.h"
28 import VarEnv ( TyVarEnv )
29 import VarSet ( TyVarSet )
31 import BasicTypes ( IPName )
32 import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon )
33 import Class ( Class )
37 import PrelNames ( superKindName, superBoxityName, liftedConName,
38 unliftedConName, typeConName, openKindConName,
43 %************************************************************************
45 \subsection{Type Classifications}
47 %************************************************************************
51 *unboxed* iff its representation is other than a pointer
52 Unboxed types are also unlifted.
54 *lifted* A type is lifted iff it has bottom as an element.
55 Closures always have lifted types: i.e. any
56 let-bound identifier in Core must have a lifted
57 type. Operationally, a lifted object is one that
60 Only lifted types may be unified with a type variable.
62 *algebraic* A type with one or more constructors, whether declared
63 with "data" or "newtype".
64 An algebraic type is one that can be deconstructed
65 with a case expression.
66 *NOT* the same as lifted types, because we also
67 include unboxed tuples in this classification.
69 *data* A type declared with "data". Also boxed tuples.
71 *primitive* iff it is a built-in type that can't be expressed
74 Currently, all primitive types are unlifted, but that's not necessarily
75 the case. (E.g. Int could be primitive.)
77 Some primitive types are unboxed, such as Int#, whereas some are boxed
78 but unlifted (such as ByteArray#). The only primitive types that we
79 classify as algebraic are the unboxed tuples.
81 examples of type classifications:
83 Type primitive boxed lifted algebraic
84 -----------------------------------------------------------------------------
86 ByteArray# Yes Yes No No
87 (# a, b #) Yes No No Yes
88 ( a, b ) No Yes Yes Yes
93 ----------------------
95 ----------------------
100 Then we want N to be represented as an Int, and that's what we arrange.
101 The front end of the compiler [TcType.lhs] treats N as opaque,
102 the back end treats it as transparent [Type.lhs].
104 There's a bit of a problem with recursive newtypes
106 newtype Q = MkQ (Q->Q)
108 Here the 'implicit expansion' we get from treating P and Q as transparent
109 would give rise to infinite types, which in turn makes eqType diverge.
110 Similarly splitForAllTys and splitFunTys can get into a loop.
112 Solution: for recursive newtypes use a coerce, and treat the newtype
113 and its representation as distinct right through the compiler. That's
114 what you get if you use recursive newtypes. (They are rare, so who
115 cares if they are a tiny bit less efficient.)
117 So: non-recursive newtypes are represented using a SourceTy (see below)
118 recursive newtypes are represented using a TyConApp
120 The TyCon still says "I'm a newtype", but we do not represent the
121 newtype application as a SourceType; instead as a TyConApp.
124 NOTE: currently [March 02] we regard a newtype as 'recursive' if it's in a
125 mutually recursive group. That's a bit conservative: only if there's a loop
126 consisting only of newtypes do we need consider it as recursive. But it's
127 not so easy to discover that, and the situation isn't that common.
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 | OpenKind -- Can be lifted or unlifted
242 | kv -- A kind variable; *only* happens during kind checking
244 boxity :: BX = * -- Lifted
246 | bv -- A boxity variable; *only* happens during kind checking
248 There's a little subtyping at the kind level:
249 forall b. Type b <: OpenKind
251 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
253 OpenKind, written '?', is used as the kind for certain type variables,
256 1. The universally quantified type variable(s) for special built-in
257 things like error :: forall (a::?). String -> a.
258 Here, the 'a' can be instantiated to a lifted or unlifted type.
260 2. Kind '?' is also used when the typechecker needs to create a fresh
261 type variable, one that may very well later be unified with a type.
262 For example, suppose f::a, and we see an application (f x). Then a
263 must be a function type, so we unify a with (b->c). But what kind
264 are b and c? They can be lifted or unlifted types, or indeed type schemes,
265 so we give them kind '?'.
267 When the type checker generalises over a bunch of type variables, it
268 makes any that still have kind '?' into kind '*'. So kind '?' is never
269 present in an inferred type.
272 ------------------------------------------
273 Define KX, the type of a kind
274 BX, the type of a boxity
277 superKind :: SuperKind -- KX, the type of all kinds
278 superKind = TyConApp (mkSuperKindCon superKindName) []
280 superBoxity :: SuperKind -- BX, the type of all boxities
281 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
284 ------------------------------------------
285 Define boxities: @*@ and @#@
288 liftedBoxity, unliftedBoxity :: Kind -- :: BX
289 liftedBoxity = TyConApp liftedBoxityCon []
290 unliftedBoxity = TyConApp unliftedBoxityCon []
292 liftedBoxityCon = mkKindCon liftedConName superBoxity
293 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
296 ------------------------------------------
297 Define kinds: Type, Type *, Type #, OpenKind
300 typeCon :: KindCon -- :: BX -> KX
301 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
303 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind
305 liftedTypeKind = TyConApp typeCon [liftedBoxity]
306 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
308 openKindCon = mkKindCon openKindConName superKind
309 openTypeKind = TyConApp openKindCon []
312 ------------------------------------------
316 mkArrowKind :: Kind -> Kind -> Kind
317 mkArrowKind k1 k2 = k1 `FunTy` k2
319 mkArrowKinds :: [Kind] -> Kind -> Kind
320 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
323 -----------------------------------------------------------------------------
324 Binary kinds for interface files
327 instance Binary Kind where
328 put_ bh k@(TyConApp tc [])
329 | tc == openKindCon = putByte bh 0
330 put_ bh k@(TyConApp tc [TyConApp bc _])
331 | tc == typeCon && bc == liftedBoxityCon = putByte bh 2
332 | tc == typeCon && bc == unliftedBoxityCon = putByte bh 3
333 put_ bh (FunTy f a) = do putByte bh 4; put_ bh f; put_ bh a
334 put_ bh _ = error "Binary.put(Kind): strange-looking Kind"
339 0 -> return openTypeKind
340 2 -> return liftedTypeKind
341 3 -> return unliftedTypeKind
342 _ -> do f <- get bh; a <- get bh; return (FunTy f a)
345 %************************************************************************
347 \subsection{Wired-in type constructors
349 %************************************************************************
351 We define a few wired-in type constructors here to avoid module knots
354 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
355 -- You might think that (->) should have type (? -> ? -> *), and you'd be right
356 -- But if we do that we get kind errors when saying
357 -- instance Control.Arrow (->)
358 -- becuase the expected kind is (*->*->*). The trouble is that the
359 -- expected/actual stuff in the unifier does not go contra-variant, whereas
360 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
361 -- a prefix way, thus: (->) Int# Int#. And this is unusual.