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 tySuperKind
308 openTypeKindTyCon = mkKindTyCon openTypeKindTyConName tySuperKind
309 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
310 ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName tySuperKind
311 argTypeKindTyCon = mkKindTyCon argTypeKindTyConName tySuperKind
313 --------------------------
314 -- ... and now their names
316 tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
317 coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
318 liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
319 openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
320 unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
321 ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
322 argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
323 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
325 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
326 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
330 -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
331 -- because they are never in scope in the source
334 -- We also need Kinds and SuperKinds, locally and in TyCon
336 kindTyConType :: TyCon -> Type
337 kindTyConType kind = TyConApp kind []
339 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
340 liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
342 liftedTypeKind = kindTyConType liftedTypeKindTyCon
343 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
344 openTypeKind = kindTyConType openTypeKindTyCon
345 argTypeKind = kindTyConType argTypeKindTyCon
346 ubxTupleKind = kindTyConType ubxTupleKindTyCon
348 -- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
349 mkArrowKind :: Kind -> Kind -> Kind
350 mkArrowKind k1 k2 = FunTy k1 k2
352 -- | Iterated application of 'mkArrowKind'
353 mkArrowKinds :: [Kind] -> Kind -> Kind
354 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
356 tySuperKind, coSuperKind :: SuperKind
357 tySuperKind = kindTyConType tySuperKindTyCon
358 coSuperKind = kindTyConType coSuperKindTyCon
360 isTySuperKind :: SuperKind -> Bool
361 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
362 isTySuperKind _ = False
364 isCoSuperKind :: SuperKind -> Bool
365 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
366 isCoSuperKind _ = False
369 -- Lastly we need a few functions on Kinds
371 isLiftedTypeKindCon :: TyCon -> Bool
372 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
374 isLiftedTypeKind :: Kind -> Bool
375 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
376 isLiftedTypeKind _ = False
378 isCoercionKind :: Kind -> Bool
379 -- All coercions are of form (ty1 ~ ty2)
380 -- This function is here rather than in Coercion,
381 -- because it's used in a knot-tied way to enforce invariants in Var
382 isCoercionKind (PredTy (EqPred {})) = True
383 isCoercionKind _ = False
385 coVarPred :: CoVar -> PredType
387 = ASSERT( isCoVar tv )
390 other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
395 %************************************************************************
397 \subsection{The external interface}
399 %************************************************************************
401 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
402 defined to use this. @pprParendType@ is the same, except it puts
403 parens around the type, except for the atomic cases. @pprParendType@
404 works just by setting the initial context precedence very high.
407 data Prec = TopPrec -- No parens
408 | FunPrec -- Function args; no parens for tycon apps
409 | TyConPrec -- Tycon args; no parens for atomic
412 maybeParen :: Prec -> Prec -> SDoc -> SDoc
413 maybeParen ctxt_prec inner_prec pretty
414 | ctxt_prec < inner_prec = pretty
415 | otherwise = parens pretty
418 pprType, pprParendType :: Type -> SDoc
419 pprType ty = ppr_type TopPrec ty
420 pprParendType ty = ppr_type TyConPrec ty
422 pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
423 -- The first arg is the tycon, or sometimes class
424 -- Print infix if the tycon/class looks like an operator
425 pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
428 pprPred :: PredType -> SDoc
429 pprPred (ClassP cls tys) = pprClassPred cls tys
430 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
431 pprPred (EqPred ty1 ty2) = sep [ ppr_type FunPrec ty1
432 , nest 2 (ptext (sLit "~"))
433 , ppr_type FunPrec ty2]
434 -- Precedence looks like (->) so that we get
437 -- Note parens on the latter!
439 pprClassPred :: Class -> [Type] -> SDoc
440 pprClassPred clas tys = ppr_type_app TopPrec (getName clas) tys
442 pprTheta :: ThetaType -> SDoc
443 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
445 pprThetaArrow :: ThetaType -> SDoc
448 | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext (sLit "=>")
451 instance Outputable Type where
454 instance Outputable PredType where
457 instance Outputable name => OutputableBndr (IPName name) where
458 pprBndr _ n = ppr n -- Simple for now
461 -- OK, here's the main printer
463 pprKind, pprParendKind :: Kind -> SDoc
465 pprParendKind = pprParendType
467 ppr_type :: Prec -> Type -> SDoc
468 ppr_type _ (TyVarTy tv) -- Note [Infix type variables]
469 | isSymOcc (getOccName tv) = parens (ppr tv)
471 ppr_type _ (PredTy pred) = ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
472 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
474 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
475 pprType t1 <+> ppr_type TyConPrec t2
477 ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
478 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
480 ppr_type p (FunTy ty1 ty2)
481 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
482 maybeParen p FunPrec $
483 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
485 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
486 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
488 ppr_forall_type :: Prec -> Type -> SDoc
490 = maybeParen p FunPrec $
491 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
493 (tvs, rho) = split1 [] ty
494 (ctxt, tau) = split2 [] rho
496 -- We need to be extra careful here as equality constraints will occur as
497 -- type variables with an equality kind. So, while collecting quantified
498 -- variables, we separate the coercion variables out and turn them into
499 -- equality predicates.
500 split1 tvs (ForAllTy tv ty)
501 | not (isCoVar tv) = split1 (tv:tvs) ty
502 split1 tvs ty = (reverse tvs, ty)
504 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
505 split2 ps (ForAllTy tv ty)
506 | isCoVar tv = split2 (coVarPred tv : ps) ty
507 split2 ps ty = (reverse ps, ty)
509 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
513 | tc `hasKey` listTyConKey = brackets (pprType ty)
514 | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
515 | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
516 | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
517 | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
518 | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
519 | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
522 | isTupleTyCon tc && tyConArity tc == length tys
523 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
525 = ppr_type_app p (getName tc) tys
527 ppr_type_app :: Prec -> Name -> [Type] -> SDoc
528 -- Used for classes as well as types; that's why it's separate from ppr_tc_app
529 ppr_type_app p tc tys
530 | is_sym_occ -- Print infix if possible
531 , [ty1,ty2] <- tys -- We know nothing of precedence though
532 = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
533 pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
535 = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
536 2 (sep (map pprParendType tys)))
538 is_sym_occ = isSymOcc (getOccName tc)
540 ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
542 = pp_nt_debug <> ppr tc
544 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
545 then ptext (sLit "<recnt>")
546 else ptext (sLit "<nt>"))
550 pprForAll :: [TyVar] -> SDoc
552 pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
554 pprTvBndr :: TyVar -> SDoc
555 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
556 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
561 Note [Infix type variables]
562 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
563 In Haskell 98 you can say
567 and the (~>) is considered a type variable. However, the type
568 pretty-printer in this module will just see (a ~> b) as
570 App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
572 So it'll print the type in prefix form. To avoid confusion we must
573 remember to parenthesise the operator, thus