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
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 )
67 ----------------------
69 ----------------------
74 Then we want N to be represented as an Int, and that's what we arrange.
75 The front end of the compiler [TcType.lhs] treats N as opaque,
76 the back end treats it as transparent [Type.lhs].
78 There's a bit of a problem with recursive newtypes
80 newtype Q = MkQ (Q->Q)
82 Here the 'implicit expansion' we get from treating P and Q as transparent
83 would give rise to infinite types, which in turn makes eqType diverge.
84 Similarly splitForAllTys and splitFunTys can get into a loop.
88 * Newtypes are always represented using TyConApp.
90 * For non-recursive newtypes, P, treat P just like a type synonym after
91 type-checking is done; i.e. it's opaque during type checking (functions
92 from TcType) but transparent afterwards (functions from Type).
93 "Treat P as a type synonym" means "all functions expand NewTcApps
96 Applications of the data constructor P simply vanish:
100 * For recursive newtypes Q, treat the Q and its representation as
101 distinct right through the compiler. Applications of the data consructor
103 Q = \(x::Q->Q). coerce Q x
104 They are rare, so who cares if they are a tiny bit less efficient.
106 The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
107 to cut all loops. The other members of the loop may be marked 'non-recursive'.
110 %************************************************************************
112 \subsection{The data type}
114 %************************************************************************
118 -- | The key representation of types within the compiler
120 = TyVarTy TyVar -- ^ Vanilla type variable
124 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
126 -- 1) Function: must /not/ be a 'TyConApp', must be another 'AppTy', or 'TyVarTy'
132 [Type] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
133 -- Invariant: saturated appliations of 'FunTyCon' must
134 -- use 'FunTy' and saturated synonyms must use their own
135 -- constructors. However, /unsaturated/ 'FunTyCon's do appear as 'TyConApp's.
138 -- 1) Type constructor being applied to.
140 -- 2) Type arguments. Might not have enough type arguments here to saturate the constructor.
141 -- Even type synonyms are not necessarily saturated; for example unsaturated type synonyms
142 -- can appear as the right hand side of a type synonym.
146 Type -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
150 Type -- ^ A polymorphic type
153 PredType -- ^ The type of evidence for a type predictate.
154 -- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
155 -- of a coercion variable; never as the argument or result
156 -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
158 -- See Note [PredTy], and Note [Equality predicates]
160 -- | The key type representing kinds in the compiler.
161 -- Invariant: a kind is always in one of these forms:
164 -- > TyConApp PrimTyCon [...]
165 -- > TyVar kv -- (during inference only)
166 -- > ForAll ... -- (for top-level coercions)
169 -- | "Super kinds", used to help encode 'Kind's as types.
170 -- Invariant: a super kind is always of this form:
172 -- > TyConApp SuperKindTyCon ...
173 type SuperKind = Type
176 -------------------------------------
180 -- | A type of the form @PredTy p@ represents a value whose type is
181 -- the Haskell predicate @p@, where a predicate is what occurs before
182 -- the @=>@ in a Haskell type.
183 -- It can be expanded into its representation, but:
185 -- * The type checker must treat it as opaque
187 -- * The rest of the compiler treats it as transparent
189 -- Consider these examples:
191 -- > f :: (Eq a) => a -> Int
192 -- > g :: (?x :: Int -> Int) => a -> Int
193 -- > h :: (r\l) => {r} => {l::Int | r}
195 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
197 = ClassP Class [Type] -- ^ Class predicate e.g. @Eq a@
198 | IParam (IPName Name) Type -- ^ Implicit parameter e.g. @?x :: Int@
199 | EqPred Type Type -- ^ Equality predicate e.g @ty1 ~ ty2@
201 -- | A collection of 'PredType's
202 type ThetaType = [PredType]
205 (We don't support TREX records yet, but the setup is designed
206 to expand to allow them.)
208 A Haskell qualified type, such as that for f,g,h above, is
210 * a FunTy for the double arrow
211 * with a PredTy as the function argument
213 The predicate really does turn into a real extra argument to the
214 function. If the argument has type (PredTy p) then the predicate p is
215 represented by evidence (a dictionary, for example, of type (predRepTy p).
217 Note [Equality predicates]
218 ~~~~~~~~~~~~~~~~~~~~~~~~~~
219 forall a b. (a ~ S b) => a -> b
220 could be represented by
221 ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
223 ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
225 The latter is what we do. (Unlike for class and implicit parameter
226 constraints, which do use FunTy.)
229 * FunTy is always a *value* function
230 * ForAllTy is discarded at runtime
232 We often need to make a "wildcard" (c::PredTy..). We always use the same
233 name (wildCoVarName), since it's not mentioned.
236 %************************************************************************
240 %************************************************************************
242 Despite the fact that DataCon has to be imported via a hi-boot route,
243 this module seems the right place for TyThing, because it's needed for
244 funTyCon and all the types in TysPrim.
247 -- | A typecheckable-thing, essentially anything that has a name
248 data TyThing = AnId Id
253 instance Outputable TyThing where
256 pprTyThing :: TyThing -> SDoc
257 pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
259 pprTyThingCategory :: TyThing -> SDoc
260 pprTyThingCategory (ATyCon _) = ptext (sLit "Type constructor")
261 pprTyThingCategory (AClass _) = ptext (sLit "Class")
262 pprTyThingCategory (AnId _) = ptext (sLit "Identifier")
263 pprTyThingCategory (ADataCon _) = ptext (sLit "Data constructor")
265 instance NamedThing TyThing where -- Can't put this with the type
266 getName (AnId id) = getName id -- decl, because the DataCon instance
267 getName (ATyCon tc) = getName tc -- isn't visible there
268 getName (AClass cl) = getName cl
269 getName (ADataCon dc) = dataConName dc
273 %************************************************************************
275 Wired-in type constructors
277 %************************************************************************
279 We define a few wired-in type constructors here to avoid module knots
282 --------------------------
283 -- First the TyCons...
285 -- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
286 funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
287 openTypeKindTyCon, unliftedTypeKindTyCon,
288 ubxTupleKindTyCon, argTypeKindTyCon
290 funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
291 openTypeKindTyConName, unliftedTypeKindTyConName,
292 ubxTupleKindTyConName, argTypeKindTyConName
295 funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
296 -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
297 -- But if we do that we get kind errors when saying
298 -- instance Control.Arrow (->)
299 -- becuase the expected kind is (*->*->*). The trouble is that the
300 -- expected/actual stuff in the unifier does not go contra-variant, whereas
301 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
302 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
305 tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
306 coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
308 liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName
309 openTypeKindTyCon = mkKindTyCon openTypeKindTyConName
310 unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
311 ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName
312 argTypeKindTyCon = mkKindTyCon argTypeKindTyConName
314 mkKindTyCon :: Name -> TyCon
315 mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
317 --------------------------
318 -- ... and now their names
320 tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
321 coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
322 liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
323 openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
324 unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
325 ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
326 argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
327 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
329 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
330 mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
334 -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
335 -- because they are never in scope in the source
338 -- We also need Kinds and SuperKinds, locally and in TyCon
340 kindTyConType :: TyCon -> Type
341 kindTyConType kind = TyConApp kind []
343 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
344 liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
346 liftedTypeKind = kindTyConType liftedTypeKindTyCon
347 unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
348 openTypeKind = kindTyConType openTypeKindTyCon
349 argTypeKind = kindTyConType argTypeKindTyCon
350 ubxTupleKind = kindTyConType ubxTupleKindTyCon
352 -- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
353 mkArrowKind :: Kind -> Kind -> Kind
354 mkArrowKind k1 k2 = FunTy k1 k2
356 -- | Iterated application of 'mkArrowKind'
357 mkArrowKinds :: [Kind] -> Kind -> Kind
358 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
360 tySuperKind, coSuperKind :: SuperKind
361 tySuperKind = kindTyConType tySuperKindTyCon
362 coSuperKind = kindTyConType coSuperKindTyCon
364 isTySuperKind :: SuperKind -> Bool
365 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
366 isTySuperKind _ = False
368 isCoSuperKind :: SuperKind -> Bool
369 isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
370 isCoSuperKind _ = False
373 -- Lastly we need a few functions on Kinds
375 isLiftedTypeKindCon :: TyCon -> Bool
376 isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
378 isLiftedTypeKind :: Kind -> Bool
379 isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
380 isLiftedTypeKind _ = False
382 isCoercionKind :: Kind -> Bool
383 -- All coercions are of form (ty1 ~ ty2)
384 -- This function is here rather than in Coercion,
385 -- because it's used in a knot-tied way to enforce invariants in Var
386 isCoercionKind (PredTy (EqPred {})) = True
387 isCoercionKind _ = False
389 coVarPred :: CoVar -> PredType
391 = ASSERT( isCoVar tv )
394 other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
399 %************************************************************************
401 \subsection{The external interface}
403 %************************************************************************
405 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
406 defined to use this. @pprParendType@ is the same, except it puts
407 parens around the type, except for the atomic cases. @pprParendType@
408 works just by setting the initial context precedence very high.
411 data Prec = TopPrec -- No parens
412 | FunPrec -- Function args; no parens for tycon apps
413 | TyConPrec -- Tycon args; no parens for atomic
416 maybeParen :: Prec -> Prec -> SDoc -> SDoc
417 maybeParen ctxt_prec inner_prec pretty
418 | ctxt_prec < inner_prec = pretty
419 | otherwise = parens pretty
422 pprType, pprParendType :: Type -> SDoc
423 pprType ty = ppr_type TopPrec ty
424 pprParendType ty = ppr_type TyConPrec ty
426 pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
427 -- The first arg is the tycon, or sometimes class
428 -- Print infix if the tycon/class looks like an operator
429 pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
432 pprPred :: PredType -> SDoc
433 pprPred (ClassP cls tys) = pprClassPred cls tys
434 pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
435 pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext (sLit "~")), ppr ty2]
436 pprClassPred :: Class -> [Type] -> SDoc
437 pprClassPred clas tys = ppr_type_app TopPrec (getName clas) tys
439 pprTheta :: ThetaType -> SDoc
440 pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
442 pprThetaArrow :: ThetaType -> SDoc
445 | otherwise = parens (sep (punctuate comma (map pprPred theta))) <+> ptext (sLit "=>")
448 instance Outputable Type where
451 instance Outputable PredType where
454 instance Outputable name => OutputableBndr (IPName name) where
455 pprBndr _ n = ppr n -- Simple for now
458 -- OK, here's the main printer
460 pprKind, pprParendKind :: Kind -> SDoc
462 pprParendKind = pprParendType
464 ppr_type :: Prec -> Type -> SDoc
465 ppr_type _ (TyVarTy tv) = ppr tv
466 ppr_type _ (PredTy pred) = ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
467 ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
469 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
470 pprType t1 <+> ppr_type TyConPrec t2
472 ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
473 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
475 ppr_type p (FunTy ty1 ty2)
476 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
477 maybeParen p FunPrec $
478 sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
480 ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
481 ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
483 ppr_forall_type :: Prec -> Type -> SDoc
485 = maybeParen p FunPrec $
486 sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
488 (tvs, rho) = split1 [] ty
489 (ctxt, tau) = split2 [] rho
491 -- We need to be extra careful here as equality constraints will occur as
492 -- type variables with an equality kind. So, while collecting quantified
493 -- variables, we separate the coercion variables out and turn them into
494 -- equality predicates.
495 split1 tvs (ForAllTy tv ty)
496 | not (isCoVar tv) = split1 (tv:tvs) ty
497 split1 tvs ty = (reverse tvs, ty)
499 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
500 split2 ps (ForAllTy tv ty)
501 | isCoVar tv = split2 (coVarPred tv : ps) ty
502 split2 ps ty = (reverse ps, ty)
504 ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
508 | tc `hasKey` listTyConKey = brackets (pprType ty)
509 | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
510 | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
511 | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
512 | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
513 | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
514 | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
517 | isTupleTyCon tc && tyConArity tc == length tys
518 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
520 = ppr_type_app p (getName tc) tys
522 ppr_type_app :: Prec -> Name -> [Type] -> SDoc
523 -- Used for classes as well as types; that's why it's separate from ppr_tc_app
524 ppr_type_app p tc tys
525 | is_sym_occ -- Print infix if possible
526 , [ty1,ty2] <- tys -- We know nothing of precedence though
527 = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
528 pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
530 = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
531 2 (sep (map pprParendType tys)))
533 is_sym_occ = isSymOcc (getOccName tc)
535 ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
537 = pp_nt_debug <> ppr tc
539 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
540 then ptext (sLit "<recnt>")
541 else ptext (sLit "<nt>"))
545 pprForAll :: [TyVar] -> SDoc
547 pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
549 pprTvBndr :: TyVar -> SDoc
550 pprTvBndr tv | isLiftedTypeKind kind = ppr tv
551 | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)