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,
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 isUnliftedTypeKind (TyConApp tc [TyConApp bc []]) = tyConName tc == typeConName &&
356 tyConName bc == unliftedConName
357 isOpenTypeKind (TyConApp tc []) = tyConName tc == openKindConName
359 isSuperKind (TyConApp tc []) = tyConName tc == superKindName
362 ------------------------------------------
366 mkArrowKind :: Kind -> Kind -> Kind
367 mkArrowKind k1 k2 = k1 `FunTy` k2
369 mkArrowKinds :: [Kind] -> Kind -> Kind
370 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
374 %************************************************************************
378 %************************************************************************
380 Despite the fact that DataCon has to be imported via a hi-boot route,
381 this module seems the right place for TyThing, because it's needed for
382 funTyCon and all the types in TysPrim.
385 data TyThing = AnId Id
390 instance Outputable TyThing where
391 ppr (AnId id) = ptext SLIT("AnId") <+> ppr id
392 ppr (ATyCon tc) = ptext SLIT("ATyCon") <+> ppr tc
393 ppr (AClass cl) = ptext SLIT("AClass") <+> ppr cl
394 ppr (ADataCon dc) = ptext SLIT("ADataCon") <+> ppr (dataConName dc)
396 instance NamedThing TyThing where -- Can't put this with the type
397 getName (AnId id) = getName id -- decl, because the DataCon instance
398 getName (ATyCon tc) = getName tc -- isn't visible there
399 getName (AClass cl) = getName cl
400 getName (ADataCon dc) = dataConName dc
404 %************************************************************************
406 \subsection{Wired-in type constructors
408 %************************************************************************
410 We define a few wired-in type constructors here to avoid module knots
413 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
414 -- You might think that (->) should have type (? -> ? -> *), and you'd be right
415 -- But if we do that we get kind errors when saying
416 -- instance Control.Arrow (->)
417 -- becuase the expected kind is (*->*->*). The trouble is that the
418 -- expected/actual stuff in the unifier does not go contra-variant, whereas
419 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
420 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
422 funTyConName = mkWiredInName gHC_PRIM
423 (mkOccFS tcName FSLIT("(->)"))
425 Nothing -- No parent object
426 (ATyCon funTyCon) -- Relevant TyCon
430 %************************************************************************
432 \subsection{The external interface}
434 %************************************************************************
436 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
437 defined to use this. @pprParendType@ is the same, except it puts
438 parens around the type, except for the atomic cases. @pprParendType@
439 works just by setting the initial context precedence very high.
442 data Prec = TopPrec -- No parens
443 | FunPrec -- Function args; no parens for tycon apps
444 | TyConPrec -- Tycon args; no parens for atomic
447 maybeParen :: Prec -> Prec -> SDoc -> SDoc
448 maybeParen ctxt_prec inner_prec pretty
449 | ctxt_prec < inner_prec = pretty
450 | otherwise = parens pretty
453 pprType, pprParendType :: Type -> SDoc
454 pprType ty = ppr_type TopPrec ty
455 pprParendType ty = ppr_type TyConPrec ty
458 pprKind, pprParendKind :: Kind -> SDoc
459 pprKind k = ppr_kind TopPrec k
460 pprParendKind k = ppr_kind TyConPrec k
463 pprPred :: PredType -> SDoc
464 pprPred (ClassP cls tys) = pprClassPred cls tys
465 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
467 pprClassPred :: Class -> [Type] -> SDoc
468 pprClassPred clas tys = ppr clas <+> sep (map pprParendType tys)
470 pprTheta :: ThetaType -> SDoc
471 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
473 pprThetaArrow :: ThetaType -> SDoc
476 | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
479 instance Outputable Type where
482 instance Outputable PredType where
485 instance Outputable name => OutputableBndr (IPName name) where
486 pprBndr _ n = ppr n -- Simple for now
489 -- OK, here's the main printer
491 ppr_type :: Prec -> Type -> SDoc
492 ppr_type p (TyVarTy tv) = ppr tv
493 ppr_type p (PredTy pred) = braces (ppr pred)
494 ppr_type p (NoteTy (SynNote ty1) ty2) = ppr_type p ty1
495 ppr_type p (NoteTy other ty2) = ppr_type p ty2
497 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
498 ppr_type p (NewTcApp tc tys) = ifPprDebug (ptext SLIT("<nt>")) <>
501 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
502 pprType t1 <+> ppr_type TyConPrec t2
504 ppr_type p (FunTy ty1 ty2)
505 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
506 maybeParen p FunPrec $
507 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
509 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
510 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
512 ppr_type p ty@(ForAllTy _ _)
513 = maybeParen p FunPrec $
514 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
516 (tvs, rho) = split1 [] ty
517 (ctxt, tau) = split2 [] rho
519 split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
520 split1 tvs ty = (reverse tvs, ty)
522 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
523 split2 ps ty = (reverse ps, ty)
525 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
529 | tc `hasKey` listTyConKey = brackets (pprType ty)
530 | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
532 | isTupleTyCon tc && tyConArity tc == length tys
533 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
535 = maybeParen p TyConPrec $
536 ppr tc <+> sep (map (ppr_type TyConPrec) tys)
539 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
541 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
542 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
548 ppr_kind :: Prec -> Kind -> SDoc
550 | isOpenTypeKind k = ptext SLIT("?")
551 | isLiftedTypeKind k = ptext SLIT("*")
552 | isUnliftedTypeKind k = ptext SLIT("#")
553 ppr_kind p (TyVarTy tv) = ppr tv
554 ppr_kind p (FunTy k1 k2) = maybeParen p FunPrec $
555 sep [ ppr_kind FunPrec k1, arrow <+> pprKind k2]
556 ppr_kind p other = ptext SLIT("STRANGE KIND:") <+> ppr_type p other