2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
5 \section[TypeRep]{Type - friends' interface}
10 Type(..), TyNote(..), -- Representation visible
11 PredType(..), -- to friends
13 Kind, ThetaType, -- Synonyms
18 pprType, pprParendType, pprTyThingCategory,
19 pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
22 liftedTypeKind, unliftedTypeKind, openTypeKind,
23 argTypeKind, ubxTupleKind,
24 isLiftedTypeKindCon, isLiftedTypeKind,
25 mkArrowKind, mkArrowKinds, isCoercionKind,
27 -- Kind constructors...
28 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
29 argTypeKindTyCon, ubxTupleKindTyCon,
32 unliftedTypeKindTyConName, openTypeKindTyConName,
33 ubxTupleKindTyConName, argTypeKindTyConName,
34 liftedTypeKindTyConName,
37 tySuperKind, coSuperKind,
38 isTySuperKind, isCoSuperKind,
39 tySuperKindTyCon, coSuperKindTyCon,
41 pprKind, pprParendKind
44 #include "HsVersions.h"
46 import {-# SOURCE #-} DataCon( DataCon, dataConName )
62 %************************************************************************
64 \subsection{Type Classifications}
66 %************************************************************************
70 *unboxed* iff its representation is other than a pointer
71 Unboxed types are also unlifted.
73 *lifted* A type is lifted iff it has bottom as an element.
74 Closures always have lifted types: i.e. any
75 let-bound identifier in Core must have a lifted
76 type. Operationally, a lifted object is one that
79 Only lifted types may be unified with a type variable.
81 *algebraic* A type with one or more constructors, whether declared
82 with "data" or "newtype".
83 An algebraic type is one that can be deconstructed
84 with a case expression.
85 *NOT* the same as lifted types, because we also
86 include unboxed tuples in this classification.
88 *data* A type declared with "data". Also boxed tuples.
90 *primitive* iff it is a built-in type that can't be expressed
93 Currently, all primitive types are unlifted, but that's not necessarily
94 the case. (E.g. Int could be primitive.)
96 Some primitive types are unboxed, such as Int#, whereas some are boxed
97 but unlifted (such as ByteArray#). The only primitive types that we
98 classify as algebraic are the unboxed tuples.
100 examples of type classifications:
102 Type primitive boxed lifted algebraic
103 -----------------------------------------------------------------------------
105 ByteArray# Yes Yes No No
106 (# a, b #) Yes No No Yes
107 ( a, b ) No Yes Yes Yes
112 ----------------------
113 A note about newtypes
114 ----------------------
119 Then we want N to be represented as an Int, and that's what we arrange.
120 The front end of the compiler [TcType.lhs] treats N as opaque,
121 the back end treats it as transparent [Type.lhs].
123 There's a bit of a problem with recursive newtypes
125 newtype Q = MkQ (Q->Q)
127 Here the 'implicit expansion' we get from treating P and Q as transparent
128 would give rise to infinite types, which in turn makes eqType diverge.
129 Similarly splitForAllTys and splitFunTys can get into a loop.
133 * Newtypes are always represented using TyConApp.
135 * For non-recursive newtypes, P, treat P just like a type synonym after
136 type-checking is done; i.e. it's opaque during type checking (functions
137 from TcType) but transparent afterwards (functions from Type).
138 "Treat P as a type synonym" means "all functions expand NewTcApps
141 Applications of the data constructor P simply vanish:
145 * For recursive newtypes Q, treat the Q and its representation as
146 distinct right through the compiler. Applications of the data consructor
148 Q = \(x::Q->Q). coerce Q x
149 They are rare, so who cares if they are a tiny bit less efficient.
151 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
152 to cut all loops. The other members of the loop may be marked 'non-recursive'.
155 %************************************************************************
157 \subsection{The data type}
159 %************************************************************************
167 Type -- Function is *not* a TyConApp
168 Type -- It must be another AppTy, or TyVarTy
169 -- (or NoteTy of these)
171 | TyConApp -- Application of a TyCon, including newtypes *and* synonyms
172 TyCon -- *Invariant* saturated appliations of FunTyCon and
173 -- synonyms have their own constructors, below.
174 -- However, *unsaturated* FunTyCons do appear as TyConApps.
176 [Type] -- Might not be saturated.
177 -- Even type synonyms are not necessarily saturated;
178 -- for example unsaturated type synonyms can appear as the
179 -- RHS of a type synonym.
181 | FunTy -- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
185 | ForAllTy -- A polymorphic type
189 | PredTy -- The type of evidence for a type predictate
190 PredType -- See Note [PredTy], and Note [Equality predicates]
191 -- NB: A PredTy (EqPred _ _) can appear only as the kind
192 -- of a coercion variable; never as the argument or result
193 -- of a FunTy (unlike ClassP, IParam)
195 | NoteTy -- A type with a note attached
197 Type -- The expanded version
199 type Kind = Type -- Invariant: a kind is always
201 -- or TyConApp PrimTyCon [...]
202 -- or TyVar kv (during inference only)
203 -- or ForAll ... (for top-level coercions)
205 type SuperKind = Type -- Invariant: a super kind is always
206 -- TyConApp SuperKindTyCon ...
208 data TyNote = FTVNote TyVarSet -- The free type variables of the noted expression
211 -------------------------------------
216 represents a value whose type is the Haskell predicate p,
217 where a predicate is what occurs before the '=>' in a Haskell type.
218 It can be expanded into its representation, but:
220 * The type checker must treat it as opaque
221 * The rest of the compiler treats it as transparent
223 Consider these examples:
224 f :: (Eq a) => a -> Int
225 g :: (?x :: Int -> Int) => a -> Int
226 h :: (r\l) => {r} => {l::Int | r}
228 Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
229 Predicates are represented inside GHC by PredType:
233 = ClassP Class [Type] -- Class predicate
234 | IParam (IPName Name) Type -- Implicit parameter
235 | EqPred Type Type -- Equality predicate (ty1 :=: ty2)
237 type ThetaType = [PredType]
240 (We don't support TREX records yet, but the setup is designed
241 to expand to allow them.)
243 A Haskell qualified type, such as that for f,g,h above, is
245 * a FunTy for the double arrow
246 * with a PredTy as the function argument
248 The predicate really does turn into a real extra argument to the
249 function. If the argument has type (PredTy p) then the predicate p is
250 represented by evidence (a dictionary, for example, of type (predRepTy p).
252 Note [Equality predicates]
253 ~~~~~~~~~~~~~~~~~~~~~~~~~~
254 forall a b. (a :=: S b) => a -> b
255 could be represented by
256 ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
258 ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
260 The latter is what we do. (Unlike for class and implicit parameter
261 constraints, which do use FunTy.)
264 * FunTy is always a *value* function
265 * ForAllTy is discarded at runtime
267 We often need to make a "wildcard" (c::PredTy..). We always use the same
268 name (wildCoVarName), since it's not mentioned.
271 %************************************************************************
275 %************************************************************************
277 Despite the fact that DataCon has to be imported via a hi-boot route,
278 this module seems the right place for TyThing, because it's needed for
279 funTyCon and all the types in TysPrim.
282 data TyThing = AnId Id
287 instance Outputable TyThing where
288 ppr thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
290 pprTyThingCategory :: TyThing -> SDoc
291 pprTyThingCategory (ATyCon _) = ptext SLIT("Type constructor")
292 pprTyThingCategory (AClass _) = ptext SLIT("Class")
293 pprTyThingCategory (AnId _) = ptext SLIT("Identifier")
294 pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
296 instance NamedThing TyThing where -- Can't put this with the type
297 getName (AnId id) = getName id -- decl, because the DataCon instance
298 getName (ATyCon tc) = getName tc -- isn't visible there
299 getName (AClass cl) = getName cl
300 getName (ADataCon dc) = dataConName dc
304 %************************************************************************
306 Wired-in type constructors
308 %************************************************************************
310 We define a few wired-in type constructors here to avoid module knots
313 --------------------------
314 -- First the TyCons...
316 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
317 -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
318 -- But if we do that we get kind errors when saying
319 -- instance Control.Arrow (->)
320 -- becuase the expected kind is (*->*->*). The trouble is that the
321 -- expected/actual stuff in the unifier does not go contra-variant, whereas
322 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
323 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
326 tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
327 coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
329 liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName
330 openTypeKindTyCon = mkKindTyCon openTypeKindTyConName
331 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
332 ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName
333 argTypeKindTyCon = mkKindTyCon argTypeKindTyConName
335 mkKindTyCon :: Name -> TyCon
336 mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
338 --------------------------
339 -- ... and now their names
341 tySuperKindTyConName = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
342 coSuperKindTyConName = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
343 liftedTypeKindTyConName = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
344 openTypeKindTyConName = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
345 unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
346 ubxTupleKindTyConName = mkPrimTyConName FSLIT("(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
347 argTypeKindTyConName = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
348 funTyConName = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon
350 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
354 -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
355 -- because they are never in scope in the source
358 -- We also need Kinds and SuperKinds, locally and in TyCon
360 kindTyConType :: TyCon -> Type
361 kindTyConType kind = TyConApp kind []
363 liftedTypeKind = kindTyConType liftedTypeKindTyCon
364 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
365 openTypeKind = kindTyConType openTypeKindTyCon
366 argTypeKind = kindTyConType argTypeKindTyCon
367 ubxTupleKind = kindTyConType ubxTupleKindTyCon
369 mkArrowKind :: Kind -> Kind -> Kind
370 mkArrowKind k1 k2 = FunTy k1 k2
372 mkArrowKinds :: [Kind] -> Kind -> Kind
373 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
375 tySuperKind, coSuperKind :: SuperKind
376 tySuperKind = kindTyConType tySuperKindTyCon
377 coSuperKind = kindTyConType coSuperKindTyCon
379 isTySuperKind (NoteTy _ ty) = isTySuperKind ty
380 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
381 isTySuperKind other = False
383 isCoSuperKind :: SuperKind -> Bool
384 isCoSuperKind (NoteTy _ ty) = isCoSuperKind ty
385 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
386 isCoSuperKind other = False
389 -- Lastly we need a few functions on Kinds
391 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
393 isLiftedTypeKind :: Kind -> Bool
394 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
395 isLiftedTypeKind other = False
397 isCoercionKind :: Kind -> Bool
398 -- All coercions are of form (ty1 :=: ty2)
399 -- This function is here rather than in Coercion,
400 -- because it's used in a knot-tied way to enforce invariants in Var
401 isCoercionKind (NoteTy _ k) = isCoercionKind k
402 isCoercionKind (PredTy (EqPred {})) = True
403 isCoercionKind other = False
408 %************************************************************************
410 \subsection{The external interface}
412 %************************************************************************
414 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
415 defined to use this. @pprParendType@ is the same, except it puts
416 parens around the type, except for the atomic cases. @pprParendType@
417 works just by setting the initial context precedence very high.
420 data Prec = TopPrec -- No parens
421 | FunPrec -- Function args; no parens for tycon apps
422 | TyConPrec -- Tycon args; no parens for atomic
425 maybeParen :: Prec -> Prec -> SDoc -> SDoc
426 maybeParen ctxt_prec inner_prec pretty
427 | ctxt_prec < inner_prec = pretty
428 | otherwise = parens pretty
431 pprType, pprParendType :: Type -> SDoc
432 pprType ty = ppr_type TopPrec ty
433 pprParendType ty = ppr_type TyConPrec ty
436 pprPred :: PredType -> SDoc
437 pprPred (ClassP cls tys) = pprClassPred cls tys
438 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
439 pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
441 pprClassPred :: Class -> [Type] -> SDoc
442 pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas)
443 <+> sep (map pprParendType tys)
445 pprTheta :: ThetaType -> SDoc
446 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
448 pprThetaArrow :: ThetaType -> SDoc
451 | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")
454 instance Outputable Type where
457 instance Outputable PredType where
460 instance Outputable name => OutputableBndr (IPName name) where
461 pprBndr _ n = ppr n -- Simple for now
464 -- OK, here's the main printer
467 pprParendKind = pprParendType
469 ppr_type :: Prec -> Type -> SDoc
470 ppr_type p (TyVarTy tv) = ppr tv
471 ppr_type p (PredTy pred) = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
472 ppr_type p (NoteTy other ty2) = ppr_type p ty2
473 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
475 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
476 pprType t1 <+> ppr_type TyConPrec t2
478 ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
479 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
481 ppr_type p (FunTy ty1 ty2)
482 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
483 maybeParen p FunPrec $
484 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
486 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
487 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
489 ppr_forall_type :: Prec -> Type -> SDoc
491 = maybeParen p FunPrec $
492 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
494 (tvs, rho) = split1 [] ty
495 (ctxt, tau) = split2 [] rho
497 split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
498 split1 tvs (NoteTy _ ty) = split1 tvs ty
499 split1 tvs ty = (reverse tvs, ty)
501 split2 ps (NoteTy _ arg -- Rather a disgusting case
502 `FunTy` res) = split2 ps (arg `FunTy` res)
503 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
504 split2 ps (NoteTy _ ty) = split2 ps ty
505 split2 ps ty = (reverse ps, ty)
507 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
511 | tc `hasKey` listTyConKey = brackets (pprType ty)
512 | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
513 | tc `hasKey` liftedTypeKindTyConKey = ptext SLIT("*")
514 | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
515 | tc `hasKey` openTypeKindTyConKey = ptext SLIT("(?)")
516 | tc `hasKey` ubxTupleKindTyConKey = ptext SLIT("(#)")
517 | tc `hasKey` argTypeKindTyConKey = ptext SLIT("??")
520 | isTupleTyCon tc && tyConArity tc == length tys
521 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
523 = maybeParen p TyConPrec $
524 ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)
526 ppr_tc :: TyCon -> SDoc
527 ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
529 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
530 then ptext SLIT("<recnt>")
531 else ptext SLIT("<nt>"))
536 pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot
538 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
539 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)