2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
5 \section[TypeRep]{Type - friends' interface}
8 -- We expose the relevant stuff from this module via the Type module
9 {-# OPTIONS_HADDOCK hide #-}
14 PredType(..), -- to friends
16 Kind, ThetaType, -- Synonyms
18 funTyCon, funTyConName,
21 pprType, pprParendType, pprTypeApp,
22 pprTyThing, pprTyThingCategory,
23 pprPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
26 liftedTypeKind, unliftedTypeKind, openTypeKind,
27 argTypeKind, ubxTupleKind,
28 isLiftedTypeKindCon, isLiftedTypeKind,
29 mkArrowKind, mkArrowKinds, isCoercionKind,
32 -- Kind constructors...
33 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
34 argTypeKindTyCon, ubxTupleKindTyCon,
37 unliftedTypeKindTyConName, openTypeKindTyConName,
38 ubxTupleKindTyConName, argTypeKindTyConName,
39 liftedTypeKindTyConName,
42 tySuperKind, coSuperKind,
43 isTySuperKind, isCoSuperKind,
44 tySuperKindTyCon, coSuperKindTyCon,
46 pprKind, pprParendKind
49 #include "HsVersions.h"
51 import {-# SOURCE #-} DataCon( DataCon, dataConName )
66 ----------------------
68 ----------------------
73 Then we want N to be represented as an Int, and that's what we arrange.
74 The front end of the compiler [TcType.lhs] treats N as opaque,
75 the back end treats it as transparent [Type.lhs].
77 There's a bit of a problem with recursive newtypes
79 newtype Q = MkQ (Q->Q)
81 Here the 'implicit expansion' we get from treating P and Q as transparent
82 would give rise to infinite types, which in turn makes eqType diverge.
83 Similarly splitForAllTys and splitFunTys can get into a loop.
87 * Newtypes are always represented using TyConApp.
89 * For non-recursive newtypes, P, treat P just like a type synonym after
90 type-checking is done; i.e. it's opaque during type checking (functions
91 from TcType) but transparent afterwards (functions from Type).
92 "Treat P as a type synonym" means "all functions expand NewTcApps
95 Applications of the data constructor P simply vanish:
99 * For recursive newtypes Q, treat the Q and its representation as
100 distinct right through the compiler. Applications of the data consructor
102 Q = \(x::Q->Q). coerce Q x
103 They are rare, so who cares if they are a tiny bit less efficient.
105 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
106 to cut all loops. The other members of the loop may be marked 'non-recursive'.
109 %************************************************************************
111 \subsection{The data type}
113 %************************************************************************
117 -- | The key representation of types within the compiler
119 = TyVarTy TyVar -- ^ Vanilla type variable
123 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
125 -- 1) Function: must /not/ be a 'TyConApp', must be another 'AppTy', or 'TyVarTy'
131 [Type] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
132 -- Invariant: saturated appliations of 'FunTyCon' must
133 -- use 'FunTy' and saturated synonyms must use their own
134 -- constructors. However, /unsaturated/ 'FunTyCon's do appear as 'TyConApp's.
137 -- 1) Type constructor being applied to.
139 -- 2) Type arguments. Might not have enough type arguments here to saturate the constructor.
140 -- Even type synonyms are not necessarily saturated; for example unsaturated type synonyms
141 -- can appear as the right hand side of a type synonym.
145 Type -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
149 Type -- ^ A polymorphic type
152 PredType -- ^ The type of evidence for a type predictate.
153 -- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
154 -- of a coercion variable; never as the argument or result
155 -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
157 -- See Note [PredTy], and Note [Equality predicates]
159 -- | The key type representing kinds in the compiler.
160 -- Invariant: a kind is always in one of these forms:
163 -- > TyConApp PrimTyCon [...]
164 -- > TyVar kv -- (during inference only)
165 -- > ForAll ... -- (for top-level coercions)
168 -- | "Super kinds", used to help encode 'Kind's as types.
169 -- Invariant: a super kind is always of this form:
171 -- > TyConApp SuperKindTyCon ...
172 type SuperKind = Type
175 -------------------------------------
179 -- | A type of the form @PredTy p@ represents a value whose type is
180 -- the Haskell predicate @p@, where a predicate is what occurs before
181 -- the @=>@ in a Haskell type.
182 -- It can be expanded into its representation, but:
184 -- * The type checker must treat it as opaque
186 -- * The rest of the compiler treats it as transparent
188 -- Consider these examples:
190 -- > f :: (Eq a) => a -> Int
191 -- > g :: (?x :: Int -> Int) => a -> Int
192 -- > h :: (r\l) => {r} => {l::Int | r}
194 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
196 = ClassP Class [Type] -- ^ Class predicate e.g. @Eq a@
197 | IParam (IPName Name) Type -- ^ Implicit parameter e.g. @?x :: Int@
198 | EqPred Type Type -- ^ Equality predicate e.g @ty1 ~ ty2@
200 -- | A collection of 'PredType's
201 type ThetaType = [PredType]
204 (We don't support TREX records yet, but the setup is designed
205 to expand to allow them.)
207 A Haskell qualified type, such as that for f,g,h above, is
209 * a FunTy for the double arrow
210 * with a PredTy as the function argument
212 The predicate really does turn into a real extra argument to the
213 function. If the argument has type (PredTy p) then the predicate p is
214 represented by evidence (a dictionary, for example, of type (predRepTy p).
216 Note [Equality predicates]
217 ~~~~~~~~~~~~~~~~~~~~~~~~~~
218 forall a b. (a ~ S b) => a -> b
219 could be represented by
220 ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
222 ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
224 The latter is what we do. (Unlike for class and implicit parameter
225 constraints, which do use FunTy.)
228 * FunTy is always a *value* function
229 * ForAllTy is discarded at runtime
231 We often need to make a "wildcard" (c::PredTy..). We always use the same
232 name (wildCoVarName), since it's not mentioned.
235 %************************************************************************
239 %************************************************************************
241 Despite the fact that DataCon has to be imported via a hi-boot route,
242 this module seems the right place for TyThing, because it's needed for
243 funTyCon and all the types in TysPrim.
246 -- | A typecheckable-thing, essentially anything that has a name
247 data TyThing = AnId Id
252 instance Outputable TyThing where
255 pprTyThing :: TyThing -> SDoc
256 pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
258 pprTyThingCategory :: TyThing -> SDoc
259 pprTyThingCategory (ATyCon _) = ptext (sLit "Type constructor")
260 pprTyThingCategory (AClass _) = ptext (sLit "Class")
261 pprTyThingCategory (AnId _) = ptext (sLit "Identifier")
262 pprTyThingCategory (ADataCon _) = ptext (sLit "Data constructor")
264 instance NamedThing TyThing where -- Can't put this with the type
265 getName (AnId id) = getName id -- decl, because the DataCon instance
266 getName (ATyCon tc) = getName tc -- isn't visible there
267 getName (AClass cl) = getName cl
268 getName (ADataCon dc) = dataConName dc
272 %************************************************************************
274 Wired-in type constructors
276 %************************************************************************
278 We define a few wired-in type constructors here to avoid module knots
281 --------------------------
282 -- First the TyCons...
284 -- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
285 funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
286 openTypeKindTyCon, unliftedTypeKindTyCon,
287 ubxTupleKindTyCon, argTypeKindTyCon
289 funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
290 openTypeKindTyConName, unliftedTypeKindTyConName,
291 ubxTupleKindTyConName, argTypeKindTyConName
294 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
295 -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
296 -- But if we do that we get kind errors when saying
297 -- instance Control.Arrow (->)
298 -- becuase the expected kind is (*->*->*). The trouble is that the
299 -- expected/actual stuff in the unifier does not go contra-variant, whereas
300 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
301 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
304 tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
305 coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
307 liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName
308 openTypeKindTyCon = mkKindTyCon openTypeKindTyConName
309 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
310 ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName
311 argTypeKindTyCon = mkKindTyCon argTypeKindTyConName
313 mkKindTyCon :: Name -> TyCon
314 mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
316 --------------------------
317 -- ... and now their names
319 tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
320 coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
321 liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
322 openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
323 unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
324 ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
325 argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
326 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
328 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
329 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
333 -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
334 -- because they are never in scope in the source
337 -- We also need Kinds and SuperKinds, locally and in TyCon
339 kindTyConType :: TyCon -> Type
340 kindTyConType kind = TyConApp kind []
342 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
343 liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
345 liftedTypeKind = kindTyConType liftedTypeKindTyCon
346 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
347 openTypeKind = kindTyConType openTypeKindTyCon
348 argTypeKind = kindTyConType argTypeKindTyCon
349 ubxTupleKind = kindTyConType ubxTupleKindTyCon
351 -- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
352 mkArrowKind :: Kind -> Kind -> Kind
353 mkArrowKind k1 k2 = FunTy k1 k2
355 -- | Iterated application of 'mkArrowKind'
356 mkArrowKinds :: [Kind] -> Kind -> Kind
357 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
359 tySuperKind, coSuperKind :: SuperKind
360 tySuperKind = kindTyConType tySuperKindTyCon
361 coSuperKind = kindTyConType coSuperKindTyCon
363 isTySuperKind :: SuperKind -> Bool
364 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
365 isTySuperKind _ = False
367 isCoSuperKind :: SuperKind -> Bool
368 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
369 isCoSuperKind _ = False
372 -- Lastly we need a few functions on Kinds
374 isLiftedTypeKindCon :: TyCon -> Bool
375 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
377 isLiftedTypeKind :: Kind -> Bool
378 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
379 isLiftedTypeKind _ = False
381 isCoercionKind :: Kind -> Bool
382 -- All coercions are of form (ty1 ~ ty2)
383 -- This function is here rather than in Coercion,
384 -- because it's used in a knot-tied way to enforce invariants in Var
385 isCoercionKind (PredTy (EqPred {})) = True
386 isCoercionKind _ = False
388 coVarPred :: CoVar -> PredType
390 = ASSERT( isCoVar tv )
393 other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
398 %************************************************************************
400 \subsection{The external interface}
402 %************************************************************************
404 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
405 defined to use this. @pprParendType@ is the same, except it puts
406 parens around the type, except for the atomic cases. @pprParendType@
407 works just by setting the initial context precedence very high.
410 data Prec = TopPrec -- No parens
411 | FunPrec -- Function args; no parens for tycon apps
412 | TyConPrec -- Tycon args; no parens for atomic
415 maybeParen :: Prec -> Prec -> SDoc -> SDoc
416 maybeParen ctxt_prec inner_prec pretty
417 | ctxt_prec < inner_prec = pretty
418 | otherwise = parens pretty
421 pprType, pprParendType :: Type -> SDoc
422 pprType ty = ppr_type TopPrec ty
423 pprParendType ty = ppr_type TyConPrec ty
425 pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
426 -- The first arg is the tycon, or sometimes class
427 -- Print infix if the tycon/class looks like an operator
428 pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
431 pprPred :: PredType -> SDoc
432 pprPred (ClassP cls tys) = pprClassPred cls tys
433 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
434 pprPred (EqPred ty1 ty2) = sep [ ppr_type FunPrec ty1
435 , nest 2 (ptext (sLit "~"))
436 , ppr_type FunPrec ty2]
437 -- Precedence looks like (->) so that we get
440 -- Note parens on the latter!
442 pprClassPred :: Class -> [Type] -> SDoc
443 pprClassPred clas tys = ppr_type_app TopPrec (getName clas) 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
466 pprKind, pprParendKind :: Kind -> SDoc
468 pprParendKind = pprParendType
470 ppr_type :: Prec -> Type -> SDoc
471 ppr_type _ (TyVarTy tv) -- Note [Infix type variables]
472 | isSymOcc (getOccName tv) = parens (ppr tv)
474 ppr_type _ (PredTy pred) = ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
475 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
477 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
478 pprType t1 <+> ppr_type TyConPrec t2
480 ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
481 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
483 ppr_type p (FunTy ty1 ty2)
484 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
485 maybeParen p FunPrec $
486 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
488 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
489 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
491 ppr_forall_type :: Prec -> Type -> SDoc
493 = maybeParen p FunPrec $
494 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
496 (tvs, rho) = split1 [] ty
497 (ctxt, tau) = split2 [] rho
499 -- We need to be extra careful here as equality constraints will occur as
500 -- type variables with an equality kind. So, while collecting quantified
501 -- variables, we separate the coercion variables out and turn them into
502 -- equality predicates.
503 split1 tvs (ForAllTy tv ty)
504 | not (isCoVar tv) = split1 (tv:tvs) ty
505 split1 tvs ty = (reverse tvs, ty)
507 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
508 split2 ps (ForAllTy tv ty)
509 | isCoVar tv = split2 (coVarPred tv : ps) ty
510 split2 ps ty = (reverse ps, ty)
512 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
516 | tc `hasKey` listTyConKey = brackets (pprType ty)
517 | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
518 | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
519 | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
520 | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
521 | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
522 | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
525 | isTupleTyCon tc && tyConArity tc == length tys
526 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
528 = ppr_type_app p (getName tc) tys
530 ppr_type_app :: Prec -> Name -> [Type] -> SDoc
531 -- Used for classes as well as types; that's why it's separate from ppr_tc_app
532 ppr_type_app p tc tys
533 | is_sym_occ -- Print infix if possible
534 , [ty1,ty2] <- tys -- We know nothing of precedence though
535 = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
536 pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
538 = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
539 2 (sep (map pprParendType tys)))
541 is_sym_occ = isSymOcc (getOccName tc)
543 ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
545 = pp_nt_debug <> ppr tc
547 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
548 then ptext (sLit "<recnt>")
549 else ptext (sLit "<nt>"))
553 pprForAll :: [TyVar] -> SDoc
555 pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
557 pprTvBndr :: TyVar -> SDoc
558 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
559 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
564 Note [Infix type variables]
565 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
566 In Haskell 98 you can say
570 and the (~>) is considered a type variable. However, the type
571 pretty-printer in this module will just see (a ~> b) as
573 App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
575 So it'll print the type in prefix form. To avoid confusion we must
576 remember to parenthesise the operator, thus