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 #-}
10 {-# LANGUAGE DeriveDataTypeable #-}
15 PredType(..), -- to friends
17 Kind, ThetaType, -- Synonyms
19 funTyCon, funTyConName,
22 pprType, pprParendType, pprTypeApp,
23 pprTyThing, pprTyThingCategory,
24 pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
27 liftedTypeKind, unliftedTypeKind, openTypeKind,
28 argTypeKind, ubxTupleKind,
29 isLiftedTypeKindCon, isLiftedTypeKind,
30 mkArrowKind, mkArrowKinds, isCoercionKind,
33 -- Kind constructors...
34 liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
35 argTypeKindTyCon, ubxTupleKindTyCon,
38 unliftedTypeKindTyConName, openTypeKindTyConName,
39 ubxTupleKindTyConName, argTypeKindTyConName,
40 liftedTypeKindTyConName,
43 tySuperKind, coSuperKind,
44 isTySuperKind, isCoSuperKind,
45 tySuperKindTyCon, coSuperKindTyCon,
47 pprKind, pprParendKind
50 #include "HsVersions.h"
52 import {-# SOURCE #-} DataCon( DataCon, dataConName )
67 import Data.Data hiding ( TyCon )
70 ----------------------
72 ----------------------
77 Then we want N to be represented as an Int, and that's what we arrange.
78 The front end of the compiler [TcType.lhs] treats N as opaque,
79 the back end treats it as transparent [Type.lhs].
81 There's a bit of a problem with recursive newtypes
83 newtype Q = MkQ (Q->Q)
85 Here the 'implicit expansion' we get from treating P and Q as transparent
86 would give rise to infinite types, which in turn makes eqType diverge.
87 Similarly splitForAllTys and splitFunTys can get into a loop.
91 * Newtypes are always represented using TyConApp.
93 * For non-recursive newtypes, P, treat P just like a type synonym after
94 type-checking is done; i.e. it's opaque during type checking (functions
95 from TcType) but transparent afterwards (functions from Type).
96 "Treat P as a type synonym" means "all functions expand NewTcApps
99 Applications of the data constructor P simply vanish:
103 * For recursive newtypes Q, treat the Q and its representation as
104 distinct right through the compiler. Applications of the data consructor
106 Q = \(x::Q->Q). coerce Q x
107 They are rare, so who cares if they are a tiny bit less efficient.
109 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
110 to cut all loops. The other members of the loop may be marked 'non-recursive'.
113 %************************************************************************
115 \subsection{The data type}
117 %************************************************************************
121 -- | The key representation of types within the compiler
123 = TyVarTy TyVar -- ^ Vanilla type variable
127 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
129 -- 1) Function: must /not/ be a 'TyConApp', must be another 'AppTy', or 'TyVarTy'
135 [Type] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
136 -- Invariant: saturated appliations of 'FunTyCon' must
137 -- use 'FunTy' and saturated synonyms must use their own
138 -- constructors. However, /unsaturated/ 'FunTyCon's do appear as 'TyConApp's.
141 -- 1) Type constructor being applied to.
143 -- 2) Type arguments. Might not have enough type arguments here to saturate the constructor.
144 -- Even type synonyms are not necessarily saturated; for example unsaturated type synonyms
145 -- can appear as the right hand side of a type synonym.
149 Type -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
153 Type -- ^ A polymorphic type
156 PredType -- ^ The type of evidence for a type predictate.
157 -- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
158 -- of a coercion variable; never as the argument or result
159 -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
161 -- See Note [PredTy], and Note [Equality predicates]
162 deriving (Data, Typeable)
164 -- | The key type representing kinds in the compiler.
165 -- Invariant: a kind is always in one of these forms:
168 -- > TyConApp PrimTyCon [...]
169 -- > TyVar kv -- (during inference only)
170 -- > ForAll ... -- (for top-level coercions)
173 -- | "Super kinds", used to help encode 'Kind's as types.
174 -- Invariant: a super kind is always of this form:
176 -- > TyConApp SuperKindTyCon ...
177 type SuperKind = Type
180 -------------------------------------
184 -- | A type of the form @PredTy p@ represents a value whose type is
185 -- the Haskell predicate @p@, where a predicate is what occurs before
186 -- the @=>@ in a Haskell type.
187 -- It can be expanded into its representation, but:
189 -- * The type checker must treat it as opaque
191 -- * The rest of the compiler treats it as transparent
193 -- Consider these examples:
195 -- > f :: (Eq a) => a -> Int
196 -- > g :: (?x :: Int -> Int) => a -> Int
197 -- > h :: (r\l) => {r} => {l::Int | r}
199 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
201 = ClassP Class [Type] -- ^ Class predicate e.g. @Eq a@
202 | IParam (IPName Name) Type -- ^ Implicit parameter e.g. @?x :: Int@
203 | EqPred Type Type -- ^ Equality predicate e.g @ty1 ~ ty2@
204 deriving (Data, Typeable)
206 -- | A collection of 'PredType's
207 type ThetaType = [PredType]
210 (We don't support TREX records yet, but the setup is designed
211 to expand to allow them.)
213 A Haskell qualified type, such as that for f,g,h above, is
215 * a FunTy for the double arrow
216 * with a PredTy as the function argument
218 The predicate really does turn into a real extra argument to the
219 function. If the argument has type (PredTy p) then the predicate p is
220 represented by evidence (a dictionary, for example, of type (predRepTy p).
222 Note [Equality predicates]
223 ~~~~~~~~~~~~~~~~~~~~~~~~~~
224 forall a b. (a ~ S b) => a -> b
225 could be represented by
226 ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
228 ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
230 The latter is what we do. (Unlike for class and implicit parameter
231 constraints, which do use FunTy.)
234 * FunTy is always a *value* function
235 * ForAllTy is discarded at runtime
237 We often need to make a "wildcard" (c::PredTy..). We always use the same
238 name (wildCoVarName), since it's not mentioned.
241 %************************************************************************
245 %************************************************************************
247 Despite the fact that DataCon has to be imported via a hi-boot route,
248 this module seems the right place for TyThing, because it's needed for
249 funTyCon and all the types in TysPrim.
252 -- | A typecheckable-thing, essentially anything that has a name
253 data TyThing = AnId Id
258 instance Outputable TyThing where
261 pprTyThing :: TyThing -> SDoc
262 pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
264 pprTyThingCategory :: TyThing -> SDoc
265 pprTyThingCategory (ATyCon _) = ptext (sLit "Type constructor")
266 pprTyThingCategory (AClass _) = ptext (sLit "Class")
267 pprTyThingCategory (AnId _) = ptext (sLit "Identifier")
268 pprTyThingCategory (ADataCon _) = ptext (sLit "Data constructor")
270 instance NamedThing TyThing where -- Can't put this with the type
271 getName (AnId id) = getName id -- decl, because the DataCon instance
272 getName (ATyCon tc) = getName tc -- isn't visible there
273 getName (AClass cl) = getName cl
274 getName (ADataCon dc) = dataConName dc
278 %************************************************************************
280 Wired-in type constructors
282 %************************************************************************
284 We define a few wired-in type constructors here to avoid module knots
287 --------------------------
288 -- First the TyCons...
290 -- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
291 funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
292 openTypeKindTyCon, unliftedTypeKindTyCon,
293 ubxTupleKindTyCon, argTypeKindTyCon
295 funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
296 openTypeKindTyConName, unliftedTypeKindTyConName,
297 ubxTupleKindTyConName, argTypeKindTyConName
300 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
301 -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
302 -- But if we do that we get kind errors when saying
303 -- instance Control.Arrow (->)
304 -- becuase the expected kind is (*->*->*). The trouble is that the
305 -- expected/actual stuff in the unifier does not go contra-variant, whereas
306 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
307 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
310 tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
311 coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
313 liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName tySuperKind
314 openTypeKindTyCon = mkKindTyCon openTypeKindTyConName tySuperKind
315 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
316 ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName tySuperKind
317 argTypeKindTyCon = mkKindTyCon argTypeKindTyConName tySuperKind
319 --------------------------
320 -- ... and now their names
322 tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
323 coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
324 liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
325 openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
326 unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
327 ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
328 argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
329 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
331 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
332 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
336 -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
337 -- because they are never in scope in the source
340 -- We also need Kinds and SuperKinds, locally and in TyCon
342 kindTyConType :: TyCon -> Type
343 kindTyConType kind = TyConApp kind []
345 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
346 liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
348 liftedTypeKind = kindTyConType liftedTypeKindTyCon
349 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
350 openTypeKind = kindTyConType openTypeKindTyCon
351 argTypeKind = kindTyConType argTypeKindTyCon
352 ubxTupleKind = kindTyConType ubxTupleKindTyCon
354 -- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
355 mkArrowKind :: Kind -> Kind -> Kind
356 mkArrowKind k1 k2 = FunTy k1 k2
358 -- | Iterated application of 'mkArrowKind'
359 mkArrowKinds :: [Kind] -> Kind -> Kind
360 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
362 tySuperKind, coSuperKind :: SuperKind
363 tySuperKind = kindTyConType tySuperKindTyCon
364 coSuperKind = kindTyConType coSuperKindTyCon
366 isTySuperKind :: SuperKind -> Bool
367 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
368 isTySuperKind _ = False
370 isCoSuperKind :: SuperKind -> Bool
371 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
372 isCoSuperKind _ = False
375 -- Lastly we need a few functions on Kinds
377 isLiftedTypeKindCon :: TyCon -> Bool
378 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
380 isLiftedTypeKind :: Kind -> Bool
381 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
382 isLiftedTypeKind _ = False
384 isCoercionKind :: Kind -> Bool
385 -- All coercions are of form (ty1 ~ ty2)
386 -- This function is here rather than in Coercion,
387 -- because it's used in a knot-tied way to enforce invariants in Var
388 isCoercionKind (PredTy (EqPred {})) = True
389 isCoercionKind _ = False
391 coVarPred :: CoVar -> PredType
393 = ASSERT( isCoVar tv )
396 other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
401 %************************************************************************
403 \subsection{The external interface}
405 %************************************************************************
407 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
408 defined to use this. @pprParendType@ is the same, except it puts
409 parens around the type, except for the atomic cases. @pprParendType@
410 works just by setting the initial context precedence very high.
413 data Prec = TopPrec -- No parens
414 | FunPrec -- Function args; no parens for tycon apps
415 | TyConPrec -- Tycon args; no parens for atomic
418 maybeParen :: Prec -> Prec -> SDoc -> SDoc
419 maybeParen ctxt_prec inner_prec pretty
420 | ctxt_prec < inner_prec = pretty
421 | otherwise = parens pretty
424 pprType, pprParendType :: Type -> SDoc
425 pprType ty = ppr_type TopPrec ty
426 pprParendType ty = ppr_type TyConPrec ty
428 pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
429 -- The first arg is the tycon, or sometimes class
430 -- Print infix if the tycon/class looks like an operator
431 pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
434 pprPred :: PredType -> SDoc
435 pprPred (ClassP cls tys) = pprClassPred cls tys
436 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
437 pprPred (EqPred ty1 ty2) = pprEqPred (ty1,ty2)
439 pprEqPred :: (Type,Type) -> SDoc
440 pprEqPred (ty1,ty2) = sep [ ppr_type FunPrec ty1
441 , nest 2 (ptext (sLit "~"))
442 , ppr_type FunPrec ty2]
443 -- Precedence looks like (->) so that we get
446 -- Note parens on the latter!
448 pprClassPred :: Class -> [Type] -> SDoc
449 pprClassPred clas tys = ppr_type_app TopPrec (getName clas) tys
451 pprTheta :: ThetaType -> SDoc
452 -- pprTheta [pred] = pprPred pred -- I'm in two minds about this
453 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
455 pprThetaArrow :: ThetaType -> SDoc
456 pprThetaArrow [] = empty
458 | noParenPred pred = pprPred pred <+> darrow
459 pprThetaArrow preds = parens (sep (punctuate comma (map pprPred preds))) <+> darrow
461 noParenPred :: PredType -> Bool
462 -- A predicate that can appear without parens before a "=>"
465 -- But (?x::Int) => Int -> Int
466 noParenPred (ClassP {}) = True
467 noParenPred (EqPred {}) = True
468 noParenPred (IParam {}) = False
471 instance Outputable Type where
474 instance Outputable PredType where
477 instance Outputable name => OutputableBndr (IPName name) where
478 pprBndr _ n = ppr n -- Simple for now
481 -- OK, here's the main printer
483 pprKind, pprParendKind :: Kind -> SDoc
485 pprParendKind = pprParendType
487 ppr_type :: Prec -> Type -> SDoc
488 ppr_type _ (TyVarTy tv) -- Note [Infix type variables]
489 | isSymOcc (getOccName tv) = parens (ppr tv)
491 ppr_type p (PredTy pred) = maybeParen p TyConPrec $
492 ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
493 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
495 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
496 pprType t1 <+> ppr_type TyConPrec t2
498 ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
499 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
501 ppr_type p (FunTy ty1 ty2)
502 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
503 maybeParen p FunPrec $
504 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
506 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
507 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
509 ppr_forall_type :: Prec -> Type -> SDoc
511 = maybeParen p FunPrec $
512 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
514 (tvs, rho) = split1 [] ty
515 (ctxt, tau) = split2 [] rho
517 -- We need to be extra careful here as equality constraints will occur as
518 -- type variables with an equality kind. So, while collecting quantified
519 -- variables, we separate the coercion variables out and turn them into
520 -- equality predicates.
521 split1 tvs (ForAllTy tv ty)
522 | not (isCoVar tv) = split1 (tv:tvs) ty
523 split1 tvs ty = (reverse tvs, ty)
525 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
526 split2 ps (ForAllTy tv ty)
527 | isCoVar tv = split2 (coVarPred tv : ps) ty
528 split2 ps ty = (reverse ps, ty)
530 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
534 | tc `hasKey` listTyConKey = brackets (pprType ty)
535 | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
536 | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
537 | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
538 | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
539 | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
540 | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
543 | isTupleTyCon tc && tyConArity tc == length tys
544 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
546 = ppr_type_app p (getName tc) tys
548 ppr_type_app :: Prec -> Name -> [Type] -> SDoc
549 -- Used for classes as well as types; that's why it's separate from ppr_tc_app
550 ppr_type_app p tc tys
551 | is_sym_occ -- Print infix if possible
552 , [ty1,ty2] <- tys -- We know nothing of precedence though
553 = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
554 pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
556 = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
557 2 (sep (map pprParendType tys)))
559 is_sym_occ = isSymOcc (getOccName tc)
561 ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
563 = pp_nt_debug <> ppr tc
565 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
566 then ptext (sLit "<recnt>")
567 else ptext (sLit "<nt>"))
571 pprForAll :: [TyVar] -> SDoc
573 pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
575 pprTvBndr :: TyVar -> SDoc
576 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
577 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
582 Note [Infix type variables]
583 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
584 In Haskell 98 you can say
588 and the (~>) is considered a type variable. However, the type
589 pretty-printer in this module will just see (a ~> b) as
591 App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
593 So it'll print the type in prefix form. To avoid confusion we must
594 remember to parenthesise the operator, thus