2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
5 \section[TypeRep]{Type - friends' interface}
9 -- The above warning supression flag is a temporary kludge.
10 -- While working on this module you are encouraged to remove it and fix
11 -- any warnings in the module. See
12 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
17 Type(..), TyNote(..), -- Representation visible
18 PredType(..), -- to friends
20 Kind, ThetaType, -- Synonyms
25 pprType, pprParendType, pprTypeApp,
26 pprTyThing, pprTyThingCategory,
27 pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
30 liftedTypeKind, unliftedTypeKind, openTypeKind,
31 argTypeKind, ubxTupleKind,
32 isLiftedTypeKindCon, isLiftedTypeKind,
33 mkArrowKind, mkArrowKinds, isCoercionKind,
36 -- Kind constructors...
37 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
38 argTypeKindTyCon, ubxTupleKindTyCon,
41 unliftedTypeKindTyConName, openTypeKindTyConName,
42 ubxTupleKindTyConName, argTypeKindTyConName,
43 liftedTypeKindTyConName,
46 tySuperKind, coSuperKind,
47 isTySuperKind, isCoSuperKind,
48 tySuperKindTyCon, coSuperKindTyCon,
50 pprKind, pprParendKind
53 #include "HsVersions.h"
55 import {-# SOURCE #-} DataCon( DataCon, dataConName )
71 %************************************************************************
73 \subsection{Type Classifications}
75 %************************************************************************
79 *unboxed* iff its representation is other than a pointer
80 Unboxed types are also unlifted.
82 *lifted* A type is lifted iff it has bottom as an element.
83 Closures always have lifted types: i.e. any
84 let-bound identifier in Core must have a lifted
85 type. Operationally, a lifted object is one that
88 Only lifted types may be unified with a type variable.
90 *algebraic* A type with one or more constructors, whether declared
91 with "data" or "newtype".
92 An algebraic type is one that can be deconstructed
93 with a case expression.
94 *NOT* the same as lifted types, because we also
95 include unboxed tuples in this classification.
97 *data* A type declared with "data". Also boxed tuples.
99 *primitive* iff it is a built-in type that can't be expressed
102 Currently, all primitive types are unlifted, but that's not necessarily
103 the case. (E.g. Int could be primitive.)
105 Some primitive types are unboxed, such as Int#, whereas some are boxed
106 but unlifted (such as ByteArray#). The only primitive types that we
107 classify as algebraic are the unboxed tuples.
109 examples of type classifications:
111 Type primitive boxed lifted algebraic
112 -----------------------------------------------------------------------------
114 ByteArray# Yes Yes No No
115 (# a, b #) Yes No No Yes
116 ( a, b ) No Yes Yes Yes
121 ----------------------
122 A note about newtypes
123 ----------------------
128 Then we want N to be represented as an Int, and that's what we arrange.
129 The front end of the compiler [TcType.lhs] treats N as opaque,
130 the back end treats it as transparent [Type.lhs].
132 There's a bit of a problem with recursive newtypes
134 newtype Q = MkQ (Q->Q)
136 Here the 'implicit expansion' we get from treating P and Q as transparent
137 would give rise to infinite types, which in turn makes eqType diverge.
138 Similarly splitForAllTys and splitFunTys can get into a loop.
142 * Newtypes are always represented using TyConApp.
144 * For non-recursive newtypes, P, treat P just like a type synonym after
145 type-checking is done; i.e. it's opaque during type checking (functions
146 from TcType) but transparent afterwards (functions from Type).
147 "Treat P as a type synonym" means "all functions expand NewTcApps
150 Applications of the data constructor P simply vanish:
154 * For recursive newtypes Q, treat the Q and its representation as
155 distinct right through the compiler. Applications of the data consructor
157 Q = \(x::Q->Q). coerce Q x
158 They are rare, so who cares if they are a tiny bit less efficient.
160 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
161 to cut all loops. The other members of the loop may be marked 'non-recursive'.
164 %************************************************************************
166 \subsection{The data type}
168 %************************************************************************
176 Type -- Function is *not* a TyConApp
177 Type -- It must be another AppTy, or TyVarTy
178 -- (or NoteTy of these)
180 | TyConApp -- Application of a TyCon, including newtypes *and* synonyms
181 TyCon -- *Invariant* saturated appliations of FunTyCon and
182 -- synonyms have their own constructors, below.
183 -- However, *unsaturated* FunTyCons do appear as TyConApps.
185 [Type] -- Might not be saturated.
186 -- Even type synonyms are not necessarily saturated;
187 -- for example unsaturated type synonyms can appear as the
188 -- RHS of a type synonym.
190 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
194 | ForAllTy -- A polymorphic type
198 | PredTy -- The type of evidence for a type predictate
199 PredType -- See Note [PredTy], and Note [Equality predicates]
200 -- NB: A PredTy (EqPred _ _) can appear only as the kind
201 -- of a coercion variable; never as the argument or result
202 -- of a FunTy (unlike ClassP, IParam)
204 | NoteTy -- A type with a note attached
206 Type -- The expanded version
208 type Kind = Type -- Invariant: a kind is always
210 -- or TyConApp PrimTyCon [...]
211 -- or TyVar kv (during inference only)
212 -- or ForAll ... (for top-level coercions)
214 type SuperKind = Type -- Invariant: a super kind is always
215 -- TyConApp SuperKindTyCon ...
217 data TyNote = FTVNote TyVarSet -- The free type variables of the noted expression
220 -------------------------------------
225 represents a value whose type is the Haskell predicate p,
226 where a predicate is what occurs before the '=>' in a Haskell type.
227 It can be expanded into its representation, but:
229 * The type checker must treat it as opaque
230 * The rest of the compiler treats it as transparent
232 Consider these examples:
233 f :: (Eq a) => a -> Int
234 g :: (?x :: Int -> Int) => a -> Int
235 h :: (r\l) => {r} => {l::Int | r}
237 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
238 Predicates are represented inside GHC by PredType:
242 = ClassP Class [Type] -- Class predicate
243 | IParam (IPName Name) Type -- Implicit parameter
244 | EqPred Type Type -- Equality predicate (ty1 ~ ty2)
246 type ThetaType = [PredType]
249 (We don't support TREX records yet, but the setup is designed
250 to expand to allow them.)
252 A Haskell qualified type, such as that for f,g,h above, is
254 * a FunTy for the double arrow
255 * with a PredTy as the function argument
257 The predicate really does turn into a real extra argument to the
258 function. If the argument has type (PredTy p) then the predicate p is
259 represented by evidence (a dictionary, for example, of type (predRepTy p).
261 Note [Equality predicates]
262 ~~~~~~~~~~~~~~~~~~~~~~~~~~
263 forall a b. (a ~ S b) => a -> b
264 could be represented by
265 ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
267 ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
269 The latter is what we do. (Unlike for class and implicit parameter
270 constraints, which do use FunTy.)
273 * FunTy is always a *value* function
274 * ForAllTy is discarded at runtime
276 We often need to make a "wildcard" (c::PredTy..). We always use the same
277 name (wildCoVarName), since it's not mentioned.
280 %************************************************************************
284 %************************************************************************
286 Despite the fact that DataCon has to be imported via a hi-boot route,
287 this module seems the right place for TyThing, because it's needed for
288 funTyCon and all the types in TysPrim.
291 data TyThing = AnId Id
296 instance Outputable TyThing where
299 pprTyThing :: TyThing -> SDoc
300 pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
302 pprTyThingCategory :: TyThing -> SDoc
303 pprTyThingCategory (ATyCon _) = ptext SLIT("Type constructor")
304 pprTyThingCategory (AClass _) = ptext SLIT("Class")
305 pprTyThingCategory (AnId _) = ptext SLIT("Identifier")
306 pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
308 instance NamedThing TyThing where -- Can't put this with the type
309 getName (AnId id) = getName id -- decl, because the DataCon instance
310 getName (ATyCon tc) = getName tc -- isn't visible there
311 getName (AClass cl) = getName cl
312 getName (ADataCon dc) = dataConName dc
316 %************************************************************************
318 Wired-in type constructors
320 %************************************************************************
322 We define a few wired-in type constructors here to avoid module knots
325 --------------------------
326 -- First the TyCons...
328 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
329 -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
330 -- But if we do that we get kind errors when saying
331 -- instance Control.Arrow (->)
332 -- becuase the expected kind is (*->*->*). The trouble is that the
333 -- expected/actual stuff in the unifier does not go contra-variant, whereas
334 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
335 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
338 tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
339 coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
341 liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName
342 openTypeKindTyCon = mkKindTyCon openTypeKindTyConName
343 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
344 ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName
345 argTypeKindTyCon = mkKindTyCon argTypeKindTyConName
347 mkKindTyCon :: Name -> TyCon
348 mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
350 --------------------------
351 -- ... and now their names
353 tySuperKindTyConName = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
354 coSuperKindTyConName = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
355 liftedTypeKindTyConName = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
356 openTypeKindTyConName = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
357 unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
358 ubxTupleKindTyConName = mkPrimTyConName FSLIT("(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
359 argTypeKindTyConName = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
360 funTyConName = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
362 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
366 -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
367 -- because they are never in scope in the source
370 -- We also need Kinds and SuperKinds, locally and in TyCon
372 kindTyConType :: TyCon -> Type
373 kindTyConType kind = TyConApp kind []
375 liftedTypeKind = kindTyConType liftedTypeKindTyCon
376 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
377 openTypeKind = kindTyConType openTypeKindTyCon
378 argTypeKind = kindTyConType argTypeKindTyCon
379 ubxTupleKind = kindTyConType ubxTupleKindTyCon
381 mkArrowKind :: Kind -> Kind -> Kind
382 mkArrowKind k1 k2 = FunTy k1 k2
384 mkArrowKinds :: [Kind] -> Kind -> Kind
385 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
387 tySuperKind, coSuperKind :: SuperKind
388 tySuperKind = kindTyConType tySuperKindTyCon
389 coSuperKind = kindTyConType coSuperKindTyCon
391 isTySuperKind (NoteTy _ ty) = isTySuperKind ty
392 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
393 isTySuperKind other = False
395 isCoSuperKind :: SuperKind -> Bool
396 isCoSuperKind (NoteTy _ ty) = isCoSuperKind ty
397 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
398 isCoSuperKind other = False
401 -- Lastly we need a few functions on Kinds
403 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
405 isLiftedTypeKind :: Kind -> Bool
406 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
407 isLiftedTypeKind other = False
409 isCoercionKind :: Kind -> Bool
410 -- All coercions are of form (ty1 ~ ty2)
411 -- This function is here rather than in Coercion,
412 -- because it's used in a knot-tied way to enforce invariants in Var
413 isCoercionKind (NoteTy _ k) = isCoercionKind k
414 isCoercionKind (PredTy (EqPred {})) = True
415 isCoercionKind other = False
417 coVarPred :: CoVar -> PredType
419 = ASSERT( isCoVar tv )
421 PredTy eq -> eq -- There shouldn't even be a NoteTy in the way
422 other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
427 %************************************************************************
429 \subsection{The external interface}
431 %************************************************************************
433 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
434 defined to use this. @pprParendType@ is the same, except it puts
435 parens around the type, except for the atomic cases. @pprParendType@
436 works just by setting the initial context precedence very high.
439 data Prec = TopPrec -- No parens
440 | FunPrec -- Function args; no parens for tycon apps
441 | TyConPrec -- Tycon args; no parens for atomic
444 maybeParen :: Prec -> Prec -> SDoc -> SDoc
445 maybeParen ctxt_prec inner_prec pretty
446 | ctxt_prec < inner_prec = pretty
447 | otherwise = parens pretty
450 pprType, pprParendType :: Type -> SDoc
451 pprType ty = ppr_type TopPrec ty
452 pprParendType ty = ppr_type TyConPrec ty
454 pprTypeApp :: NamedThing a => a -> SDoc -> [Type] -> SDoc
455 -- The first arg is the tycon; it's used to arrange printing infix
456 -- if it looks like an operator
457 -- Second arg is the pretty-printed tycon
458 pprTypeApp tc pp_tc tys = ppr_type_app TopPrec (getName tc) pp_tc tys
461 pprPred :: PredType -> SDoc
462 pprPred (ClassP cls tys) = pprClassPred cls tys
463 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
464 pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT("~")), ppr ty2]
465 pprClassPred :: Class -> [Type] -> SDoc
466 pprClassPred clas tys = ppr_type_app TopPrec (getName clas) (ppr clas) tys
468 pprTheta :: ThetaType -> SDoc
469 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
471 pprThetaArrow :: ThetaType -> SDoc
474 | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
477 instance Outputable Type where
480 instance Outputable PredType where
483 instance Outputable name => OutputableBndr (IPName name) where
484 pprBndr _ n = ppr n -- Simple for now
487 -- OK, here's the main printer
490 pprParendKind = pprParendType
492 ppr_type :: Prec -> Type -> SDoc
493 ppr_type p (TyVarTy tv) = ppr tv
494 ppr_type p (PredTy pred) = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
495 ppr_type p (NoteTy other ty2) = ifPprDebug (ptext SLIT("<note>")) <> ppr_type p ty2
496 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
498 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
499 pprType t1 <+> ppr_type TyConPrec t2
501 ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
502 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
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_forall_type :: Prec -> Type -> SDoc
514 = maybeParen p FunPrec $
515 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
517 (tvs, rho) = split1 [] ty
518 (ctxt, tau) = split2 [] rho
520 -- We need to be extra careful here as equality constraints will occur as
521 -- type variables with an equality kind. So, while collecting quantified
522 -- variables, we separate the coercion variables out and turn them into
523 -- equality predicates.
524 split1 tvs (ForAllTy tv ty)
525 | not (isCoVar tv) = split1 (tv:tvs) ty
526 split1 tvs (NoteTy _ ty) = split1 tvs ty
527 split1 tvs ty = (reverse tvs, ty)
529 split2 ps (NoteTy _ 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 (ForAllTy tv ty)
533 | isCoVar tv = split2 (coVarPred tv : ps) ty
534 split2 ps (NoteTy _ ty) = split2 ps ty
535 split2 ps ty = (reverse ps, ty)
537 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
541 | tc `hasKey` listTyConKey = brackets (pprType ty)
542 | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
543 | tc `hasKey` liftedTypeKindTyConKey = ptext SLIT("*")
544 | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
545 | tc `hasKey` openTypeKindTyConKey = ptext SLIT("(?)")
546 | tc `hasKey` ubxTupleKindTyConKey = ptext SLIT("(#)")
547 | tc `hasKey` argTypeKindTyConKey = ptext SLIT("??")
550 | isTupleTyCon tc && tyConArity tc == length tys
551 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
553 = ppr_type_app p (getName tc) (ppr_naked_tc tc) tys
555 ppr_type_app :: Prec -> Name -> SDoc -> [Type] -> SDoc
556 ppr_type_app p tc pp_tc tys
557 | is_sym_occ -- Print infix if possible
558 , [ty1,ty2] <- tys -- We know nothing of precedence though
559 = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
560 pp_tc <+> ppr_type FunPrec ty2])
562 = maybeParen p TyConPrec (hang paren_tc 2 (sep (map pprParendType tys)))
564 is_sym_occ = isSymOcc (getOccName tc)
565 paren_tc | is_sym_occ = parens pp_tc
568 ppr_tc :: TyCon -> SDoc
569 ppr_tc tc = parenSymOcc (getOccName tc) (ppr_naked_tc tc)
571 ppr_naked_tc :: TyCon -> SDoc -- No brackets for SymOcc
573 = pp_nt_debug <> ppr tc
575 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
576 then ptext SLIT("<recnt>")
577 else ptext SLIT("<nt>"))
582 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
584 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
585 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)