2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TypeRep]{Type - friends' interface}
9 Type(..), TyNote(..), -- Representation visible
10 PredType(..), -- to friends
12 Kind, ThetaType, -- Synonyms
15 superKind, superBoxity, -- KX and BX respectively
16 liftedBoxity, unliftedBoxity, -- :: BX
18 typeCon, -- :: BX -> KX
19 liftedTypeKind, unliftedTypeKind, openTypeKind, -- :: KX
20 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isSuperKind,
21 mkArrowKind, mkArrowKinds, -- :: KX -> KX -> KX
26 pprKind, pprParendKind,
27 pprType, pprParendType,
28 pprPred, pprTheta, pprThetaArrow, pprClassPred
31 #include "HsVersions.h"
33 import {-# SOURCE #-} DataCon( DataCon, dataConName )
36 import Var ( Id, TyVar, tyVarKind )
37 import VarEnv ( TyVarEnv )
38 import VarSet ( TyVarSet )
39 import Name ( Name, NamedThing(..), mkWiredInName, mkInternalName )
40 import OccName ( mkOccFS, mkKindOccFS, tcName )
41 import BasicTypes ( IPName, tupleParens )
42 import TyCon ( TyCon, KindCon, mkFunTyCon, mkKindCon, mkSuperKindCon, isNewTyCon,
43 tyConArity, tupleTyConBoxity, isTupleTyCon, tyConName )
44 import Class ( Class )
47 import PrelNames ( gHC_PRIM, kindConKey, boxityConKey, liftedConKey,
48 unliftedConKey, typeConKey, anyBoxConKey,
49 funTyConKey, listTyConKey, parrTyConKey,
52 import SrcLoc ( noSrcLoc )
56 %************************************************************************
58 \subsection{Type Classifications}
60 %************************************************************************
64 *unboxed* iff its representation is other than a pointer
65 Unboxed types are also unlifted.
67 *lifted* A type is lifted iff it has bottom as an element.
68 Closures always have lifted types: i.e. any
69 let-bound identifier in Core must have a lifted
70 type. Operationally, a lifted object is one that
73 Only lifted types may be unified with a type variable.
75 *algebraic* A type with one or more constructors, whether declared
76 with "data" or "newtype".
77 An algebraic type is one that can be deconstructed
78 with a case expression.
79 *NOT* the same as lifted types, because we also
80 include unboxed tuples in this classification.
82 *data* A type declared with "data". Also boxed tuples.
84 *primitive* iff it is a built-in type that can't be expressed
87 Currently, all primitive types are unlifted, but that's not necessarily
88 the case. (E.g. Int could be primitive.)
90 Some primitive types are unboxed, such as Int#, whereas some are boxed
91 but unlifted (such as ByteArray#). The only primitive types that we
92 classify as algebraic are the unboxed tuples.
94 examples of type classifications:
96 Type primitive boxed lifted algebraic
97 -----------------------------------------------------------------------------
99 ByteArray# Yes Yes No No
100 (# a, b #) Yes No No Yes
101 ( a, b ) No Yes Yes Yes
106 ----------------------
107 A note about newtypes
108 ----------------------
113 Then we want N to be represented as an Int, and that's what we arrange.
114 The front end of the compiler [TcType.lhs] treats N as opaque,
115 the back end treats it as transparent [Type.lhs].
117 There's a bit of a problem with recursive newtypes
119 newtype Q = MkQ (Q->Q)
121 Here the 'implicit expansion' we get from treating P and Q as transparent
122 would give rise to infinite types, which in turn makes eqType diverge.
123 Similarly splitForAllTys and splitFunTys can get into a loop.
127 * Newtypes are always represented using NewTcApp, never as TyConApp.
129 * For non-recursive newtypes, P, treat P just like a type synonym after
130 type-checking is done; i.e. it's opaque during type checking (functions
131 from TcType) but transparent afterwards (functions from Type).
132 "Treat P as a type synonym" means "all functions expand NewTcApps
135 Applications of the data constructor P simply vanish:
139 * For recursive newtypes Q, treat the Q and its representation as
140 distinct right through the compiler. Applications of the data consructor
142 Q = \(x::Q->Q). coerce Q x
143 They are rare, so who cares if they are a tiny bit less efficient.
145 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
146 to cut all loops. The other members of the loop may be marked 'non-recursive'.
149 %************************************************************************
151 \subsection{The data type}
153 %************************************************************************
157 type SuperKind = Type
160 type TyVarSubst = TyVarEnv Type
166 Type -- Function is *not* a TyConApp
169 | TyConApp -- Application of a TyCon
170 TyCon -- *Invariant* saturated appliations of FunTyCon and
171 -- synonyms have their own constructors, below.
172 [Type] -- Might not be saturated.
174 | NewTcApp -- Application of a NewType TyCon. All newtype applications
175 TyCon -- show up like this until they are fed through newTypeRep,
177 -- * an ordinary TyConApp for non-saturated,
178 -- or recursive newtypes
180 -- * the representation type of the newtype for satuarted,
181 -- non-recursive ones
182 -- [But the result of a call to newTypeRep is always consumed
183 -- immediately; it never lives on in another type. So in any
184 -- type, newtypes are always represented with NewTcApp.]
185 [Type] -- Might not be saturated.
187 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
191 | ForAllTy -- A polymorphic type
195 | PredTy -- A high level source type
196 PredType -- ...can be expanded to a representation type...
198 | NoteTy -- A type with a note attached
200 Type -- The expanded version
203 = FTVNote TyVarSet -- The free type variables of the noted expression
205 | SynNote Type -- Used for type synonyms
206 -- The Type is always a TyConApp, and is the un-expanded form.
207 -- The type to which the note is attached is the expanded form.
210 -------------------------------------
215 represents a value whose type is the Haskell predicate p,
216 where a predicate is what occurs before the '=>' in a Haskell type.
217 It can be expanded into its representation, but:
219 * The type checker must treat it as opaque
220 * The rest of the compiler treats it as transparent
222 Consider these examples:
223 f :: (Eq a) => a -> Int
224 g :: (?x :: Int -> Int) => a -> Int
225 h :: (r\l) => {r} => {l::Int | r}
227 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
228 Predicates are represented inside GHC by PredType:
232 = ClassP Class [Type] -- Class predicate
233 | IParam (IPName Name) Type -- Implicit parameter
235 type ThetaType = [PredType]
238 (We don't support TREX records yet, but the setup is designed
239 to expand to allow them.)
241 A Haskell qualified type, such as that for f,g,h above, is
243 * a FunTy for the double arrow
244 * with a PredTy as the function argument
246 The predicate really does turn into a real extra argument to the
247 function. If the argument has type (PredTy p) then the predicate p is
248 represented by evidence (a dictionary, for example, of type (predRepTy p).
251 %************************************************************************
255 %************************************************************************
259 kind :: KX = kind -> kind
261 | Type liftedness -- (Type *) is printed as just *
262 -- (Type #) is printed as just #
264 | OpenKind -- Can be lifted or unlifted
267 | kv -- A kind variable; *only* happens during kind checking
269 boxity :: BX = * -- Lifted
271 | bv -- A boxity variable; *only* happens during kind checking
273 There's a little subtyping at the kind level:
274 forall b. Type b <: OpenKind
276 That is, a type of kind (Type b) is OK in a context requiring an OpenKind
278 OpenKind, written '?', is used as the kind for certain type variables,
281 1. The universally quantified type variable(s) for special built-in
282 things like error :: forall (a::?). String -> a.
283 Here, the 'a' can be instantiated to a lifted or unlifted type.
285 2. Kind '?' is also used when the typechecker needs to create a fresh
286 type variable, one that may very well later be unified with a type.
287 For example, suppose f::a, and we see an application (f x). Then a
288 must be a function type, so we unify a with (b->c). But what kind
289 are b and c? They can be lifted or unlifted types, or indeed type schemes,
290 so we give them kind '?'.
292 When the type checker generalises over a bunch of type variables, it
293 makes any that still have kind '?' into kind '*'. So kind '?' is never
294 present in an inferred type.
297 ------------------------------------------
298 Define KX, the type of a kind
299 BX, the type of a boxity
302 superKindName = kindQual FSLIT("KX") kindConKey
303 superBoxityName = kindQual FSLIT("BX") boxityConKey
304 liftedConName = kindQual FSLIT("*") liftedConKey
305 unliftedConName = kindQual FSLIT("#") unliftedConKey
306 openKindConName = kindQual FSLIT("?") anyBoxConKey
307 typeConName = kindQual FSLIT("Type") typeConKey
309 kindQual str uq = mkInternalName uq (mkKindOccFS tcName str) noSrcLoc
310 -- Kinds are not z-encoded in interface file, hence mkKindOccFS
311 -- And they don't come from any particular module; indeed we always
312 -- want to print them unqualified. Hence the InternalName.
316 superKind :: SuperKind -- KX, the type of all kinds
317 superKind = TyConApp (mkSuperKindCon superKindName) []
319 superBoxity :: SuperKind -- BX, the type of all boxities
320 superBoxity = TyConApp (mkSuperKindCon superBoxityName) []
323 ------------------------------------------
324 Define boxities: @*@ and @#@
327 liftedBoxity, unliftedBoxity :: Kind -- :: BX
328 liftedBoxity = TyConApp liftedBoxityCon []
329 unliftedBoxity = TyConApp unliftedBoxityCon []
331 liftedBoxityCon = mkKindCon liftedConName superBoxity
332 unliftedBoxityCon = mkKindCon unliftedConName superBoxity
335 ------------------------------------------
336 Define kinds: Type, Type *, Type #, OpenKind
339 typeCon :: KindCon -- :: BX -> KX
340 typeCon = mkKindCon typeConName (superBoxity `FunTy` superKind)
342 liftedTypeKind, unliftedTypeKind, openTypeKind :: Kind -- Of superkind superKind
344 liftedTypeKind = TyConApp typeCon [liftedBoxity]
345 unliftedTypeKind = TyConApp typeCon [unliftedBoxity]
347 openKindCon = mkKindCon openKindConName superKind
348 openTypeKind = TyConApp openKindCon []
352 isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind :: Kind -> Bool
353 isLiftedTypeKind (TyConApp tc [TyConApp bc []]) = tyConName tc == typeConName &&
354 tyConName bc == liftedConName
355 isLiftedTypeKind other = False
357 isUnliftedTypeKind (TyConApp tc [TyConApp bc []]) = tyConName tc == typeConName &&
358 tyConName bc == unliftedConName
359 isUnliftedTypeKind other = False
361 isOpenTypeKind (TyConApp tc []) = tyConName tc == openKindConName
362 isOpenTypeKind other = False
364 isSuperKind (TyConApp tc []) = tyConName tc == superKindName
365 isSuperKind other = False
368 ------------------------------------------
372 mkArrowKind :: Kind -> Kind -> Kind
373 mkArrowKind k1 k2 = k1 `FunTy` k2
375 mkArrowKinds :: [Kind] -> Kind -> Kind
376 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
380 %************************************************************************
384 %************************************************************************
386 Despite the fact that DataCon has to be imported via a hi-boot route,
387 this module seems the right place for TyThing, because it's needed for
388 funTyCon and all the types in TysPrim.
391 data TyThing = AnId Id
396 instance Outputable TyThing where
397 ppr (AnId id) = ptext SLIT("AnId") <+> ppr id
398 ppr (ATyCon tc) = ptext SLIT("ATyCon") <+> ppr tc
399 ppr (AClass cl) = ptext SLIT("AClass") <+> ppr cl
400 ppr (ADataCon dc) = ptext SLIT("ADataCon") <+> ppr (dataConName dc)
402 instance NamedThing TyThing where -- Can't put this with the type
403 getName (AnId id) = getName id -- decl, because the DataCon instance
404 getName (ATyCon tc) = getName tc -- isn't visible there
405 getName (AClass cl) = getName cl
406 getName (ADataCon dc) = dataConName dc
410 %************************************************************************
412 \subsection{Wired-in type constructors
414 %************************************************************************
416 We define a few wired-in type constructors here to avoid module knots
419 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
420 -- You might think that (->) should have type (? -> ? -> *), and you'd be right
421 -- But if we do that we get kind errors when saying
422 -- instance Control.Arrow (->)
423 -- becuase the expected kind is (*->*->*). The trouble is that the
424 -- expected/actual stuff in the unifier does not go contra-variant, whereas
425 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
426 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
428 funTyConName = mkWiredInName gHC_PRIM
429 (mkOccFS tcName FSLIT("(->)"))
431 Nothing -- No parent object
432 (ATyCon funTyCon) -- Relevant TyCon
436 %************************************************************************
438 \subsection{The external interface}
440 %************************************************************************
442 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
443 defined to use this. @pprParendType@ is the same, except it puts
444 parens around the type, except for the atomic cases. @pprParendType@
445 works just by setting the initial context precedence very high.
448 data Prec = TopPrec -- No parens
449 | FunPrec -- Function args; no parens for tycon apps
450 | TyConPrec -- Tycon args; no parens for atomic
453 maybeParen :: Prec -> Prec -> SDoc -> SDoc
454 maybeParen ctxt_prec inner_prec pretty
455 | ctxt_prec < inner_prec = pretty
456 | otherwise = parens pretty
459 pprType, pprParendType :: Type -> SDoc
460 pprType ty = ppr_type TopPrec ty
461 pprParendType ty = ppr_type TyConPrec ty
464 pprKind, pprParendKind :: Kind -> SDoc
465 pprKind k = ppr_kind TopPrec k
466 pprParendKind k = ppr_kind TyConPrec k
469 pprPred :: PredType -> SDoc
470 pprPred (ClassP cls tys) = pprClassPred cls tys
471 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
473 pprClassPred :: Class -> [Type] -> SDoc
474 pprClassPred clas tys = ppr clas <+> sep (map pprParendType tys)
476 pprTheta :: ThetaType -> SDoc
477 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
479 pprThetaArrow :: ThetaType -> SDoc
482 | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
485 instance Outputable Type where
488 instance Outputable PredType where
491 instance Outputable name => OutputableBndr (IPName name) where
492 pprBndr _ n = ppr n -- Simple for now
495 -- OK, here's the main printer
497 ppr_type :: Prec -> Type -> SDoc
498 ppr_type p (TyVarTy tv) = ppr tv
499 ppr_type p (PredTy pred) = braces (ppr pred)
500 ppr_type p (NoteTy (SynNote ty1) ty2) = ppr_type p ty1
501 ppr_type p (NoteTy other ty2) = ppr_type p ty2
503 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
504 ppr_type p (NewTcApp tc tys) = ifPprDebug (ptext SLIT("<nt>")) <>
507 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
508 pprType t1 <+> ppr_type TyConPrec t2
510 ppr_type p (FunTy ty1 ty2)
511 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
512 maybeParen p FunPrec $
513 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
515 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
516 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
518 ppr_type p ty@(ForAllTy _ _)
519 = maybeParen p FunPrec $
520 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
522 (tvs, rho) = split1 [] ty
523 (ctxt, tau) = split2 [] rho
525 split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
526 split1 tvs (NoteTy (FTVNote _) ty) = split1 tvs ty
527 split1 tvs ty = (reverse tvs, ty)
529 split2 ps (NoteTy (FTVNote _) arg -- Rather a disgusting case
530 `FunTy` res) = split2 ps (arg `FunTy` res)
531 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
532 split2 ps (NoteTy (FTVNote _) ty) = split2 ps ty
533 split2 ps ty = (reverse ps, ty)
535 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
539 | tc `hasKey` listTyConKey = brackets (pprType ty)
540 | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
542 | isTupleTyCon tc && tyConArity tc == length tys
543 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
545 = maybeParen p TyConPrec $
546 ppr tc <+> sep (map (ppr_type TyConPrec) tys)
549 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
551 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
552 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
558 ppr_kind :: Prec -> Kind -> SDoc
560 | isOpenTypeKind k = ptext SLIT("?")
561 | isLiftedTypeKind k = ptext SLIT("*")
562 | isUnliftedTypeKind k = ptext SLIT("#")
563 ppr_kind p (TyVarTy tv) = ppr tv
564 ppr_kind p (FunTy k1 k2) = maybeParen p FunPrec $
565 sep [ ppr_kind FunPrec k1, arrow <+> pprKind k2]
566 ppr_kind p other = ptext SLIT("STRANGE KIND:") <+> ppr_type p other