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, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
14 Pred(..), -- to friends
17 PredType, ThetaType, -- Synonyms
19 -- Functions over types
20 mkTyConApp, mkTyConTy, mkTyVarTy, mkTyVarTys,
21 isLiftedTypeKind, isCoercionKind,
24 pprType, pprParendType, pprTypeApp,
25 pprTyThing, pprTyThingCategory,
26 pprPredTy, pprEqPred, pprTheta, pprForAll, pprThetaArrowTy, pprClassPred,
27 pprKind, pprParendKind,
28 Prec(..), maybeParen, pprTcApp, pprTypeNameApp,
29 pprPrefixApp, pprPred, pprArrowChain, pprThetaArrow,
32 tyVarsOfType, tyVarsOfTypes,
33 tyVarsOfPred, tyVarsOfTheta,
34 varsOfPred, varsOfTheta,
38 TvSubst(..), TvSubstEnv
41 #include "HsVersions.h"
43 import {-# SOURCE #-} DataCon( DataCon, dataConName )
61 import qualified Data.Data as Data hiding ( TyCon )
62 import qualified Data.Foldable as Data
63 import qualified Data.Traversable as Data
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 (*never* a coercion variable)
123 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
125 -- 1) Function: must /not/ be a 'TyConApp',
126 -- 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
136 -- do appear as 'TyConApp's.
139 -- 1) Type constructor being applied to.
141 -- 2) Type arguments. Might not have enough type arguments
142 -- here to saturate the constructor.
143 -- Even type synonyms are not necessarily saturated;
144 -- 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]@
150 -- See Note [Equality-constrained types]
153 TyCoVar -- Type variable
154 Type -- ^ A polymorphic type
157 PredType -- ^ The type of evidence for a type predictate.
158 -- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
159 -- of a coercion variable; never as the argument or result of a
160 -- 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
162 -- See Note [PredTy], and Note [Equality predicates]
163 deriving (Data.Data, Data.Typeable)
165 -- | The key type representing kinds in the compiler.
166 -- Invariant: a kind is always in one of these forms:
169 -- > TyConApp PrimTyCon [...]
170 -- > TyVar kv -- (during inference only)
171 -- > ForAll ... -- (for top-level coercions)
174 -- | "Super kinds", used to help encode 'Kind's as types.
175 -- Invariant: a super kind is always of this form:
177 -- > TyConApp SuperKindTyCon ...
178 type SuperKind = Type
181 Note [Equality-constrained types]
182 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
183 The type forall ab. (a ~ [b]) => blah
184 is encoded like this:
186 ForAllTy (a:*) $ ForAllTy (b:*) $
187 FunTy (PredTy (EqPred a [b]) $
190 -------------------------------------
194 -- | A type of the form @PredTy p@ represents a value whose type is
195 -- the Haskell predicate @p@, where a predicate is what occurs before
196 -- the @=>@ in a Haskell type.
197 -- It can be expanded into its representation, but:
199 -- * The type checker must treat it as opaque
201 -- * The rest of the compiler treats it as transparent
203 -- Consider these examples:
205 -- > f :: (Eq a) => a -> Int
206 -- > g :: (?x :: Int -> Int) => a -> Int
207 -- > h :: (r\l) => {r} => {l::Int | r}
209 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
210 type PredType = Pred Type
212 data Pred a -- Typically 'a' is instantiated with Type or Coercion
213 = ClassP Class [a] -- ^ Class predicate e.g. @Eq a@
214 | IParam (IPName Name) a -- ^ Implicit parameter e.g. @?x :: Int@
215 | EqPred a a -- ^ Equality predicate e.g @ty1 ~ ty2@
216 deriving (Data.Data, Data.Typeable, Data.Foldable, Data.Traversable, Functor)
218 -- | A collection of 'PredType's
219 type ThetaType = [PredType]
222 (We don't support TREX records yet, but the setup is designed
223 to expand to allow them.)
225 A Haskell qualified type, such as that for f,g,h above, is
227 * a FunTy for the double arrow
228 * with a PredTy as the function argument
230 The predicate really does turn into a real extra argument to the
231 function. If the argument has type (PredTy p) then the predicate p is
232 represented by evidence (a dictionary, for example, of type (predRepTy p).
234 Note [Equality predicates]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~
236 forall a b. (a ~ S b) => a -> b
237 could be represented by
238 ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
240 ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
242 The latter is what we do. (Unlike for class and implicit parameter
243 constraints, which do use FunTy.)
246 * FunTy is always a *value* function
247 * ForAllTy is discarded at runtime
249 We often need to make a "wildcard" (c::PredTy..). We always use the same
250 name (wildCoVarName), since it's not mentioned.
253 %************************************************************************
257 %************************************************************************
259 These functions are here so that they can be used by TysPrim,
260 which in turn is imported by Type
263 mkTyVarTy :: TyVar -> Type
266 mkTyVarTys :: [TyVar] -> [Type]
267 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
269 -- | A key function: builds a 'TyConApp' or 'FunTy' as apppropriate to its arguments.
270 -- Applies its arguments to the constructor from left to right
271 mkTyConApp :: TyCon -> [Type] -> Type
273 | isFunTyCon tycon, [ty1,ty2] <- tys
279 -- | Create the plain type constructor type which has been applied to no type arguments at all.
280 mkTyConTy :: TyCon -> Type
281 mkTyConTy tycon = mkTyConApp tycon []
283 isLiftedTypeKind :: Kind -> Bool
284 -- This function is here because it's used in the pretty printer
285 isLiftedTypeKind (TyConApp tc []) = tc `hasKey` liftedTypeKindTyConKey
286 isLiftedTypeKind _ = False
288 isCoercionKind :: Kind -> Bool
289 -- All coercions are of form (ty1 ~ ty2)
290 -- This function is here rather than in Coercion, because it
291 -- is used in a knot-tied way to enforce invariants in Var
292 isCoercionKind (PredTy (EqPred {})) = True
293 isCoercionKind _ = False
297 %************************************************************************
299 Free variables of types and coercions
301 %************************************************************************
304 tyVarsOfPred :: PredType -> TyCoVarSet
305 tyVarsOfPred = varsOfPred tyVarsOfType
307 tyVarsOfTheta :: ThetaType -> TyCoVarSet
308 tyVarsOfTheta = varsOfTheta tyVarsOfType
310 tyVarsOfType :: Type -> VarSet
311 -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
312 tyVarsOfType (TyVarTy v) = unitVarSet v
313 tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
314 tyVarsOfType (PredTy sty) = varsOfPred tyVarsOfType sty
315 tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
316 tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
317 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
319 tyVarsOfTypes :: [Type] -> TyVarSet
320 tyVarsOfTypes tys = foldr (unionVarSet . tyVarsOfType) emptyVarSet tys
322 varsOfPred :: (a -> VarSet) -> Pred a -> VarSet
323 varsOfPred f (IParam _ ty) = f ty
324 varsOfPred f (ClassP _ tys) = foldr (unionVarSet . f) emptyVarSet tys
325 varsOfPred f (EqPred ty1 ty2) = f ty1 `unionVarSet` f ty2
327 varsOfTheta :: (a -> VarSet) -> [Pred a] -> VarSet
328 varsOfTheta f = foldr (unionVarSet . varsOfPred f) emptyVarSet
330 predSize :: (a -> Int) -> Pred a -> Int
331 predSize size (IParam _ t) = 1 + size t
332 predSize size (ClassP _ ts) = 1 + sum (map size ts)
333 predSize size (EqPred t1 t2) = size t1 + size t2
336 %************************************************************************
340 %************************************************************************
342 Despite the fact that DataCon has to be imported via a hi-boot route,
343 this module seems the right place for TyThing, because it's needed for
344 funTyCon and all the types in TysPrim.
347 -- | A typecheckable-thing, essentially anything that has a name
348 data TyThing = AnId Id
354 instance Outputable TyThing where
357 pprTyThing :: TyThing -> SDoc
358 pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
360 pprTyThingCategory :: TyThing -> SDoc
361 pprTyThingCategory (ATyCon _) = ptext (sLit "Type constructor")
362 pprTyThingCategory (ACoAxiom _) = ptext (sLit "Coercion axiom")
363 pprTyThingCategory (AClass _) = ptext (sLit "Class")
364 pprTyThingCategory (AnId _) = ptext (sLit "Identifier")
365 pprTyThingCategory (ADataCon _) = ptext (sLit "Data constructor")
367 instance NamedThing TyThing where -- Can't put this with the type
368 getName (AnId id) = getName id -- decl, because the DataCon instance
369 getName (ATyCon tc) = getName tc -- isn't visible there
370 getName (ACoAxiom cc) = getName cc
371 getName (AClass cl) = getName cl
372 getName (ADataCon dc) = dataConName dc
376 %************************************************************************
379 Data type defined here to avoid unnecessary mutual recursion
381 %************************************************************************
384 -- | Type substitution
386 -- #tvsubst_invariant#
387 -- The following invariants must hold of a 'TvSubst':
389 -- 1. The in-scope set is needed /only/ to
390 -- guide the generation of fresh uniques
392 -- 2. In particular, the /kind/ of the type variables in
393 -- the in-scope set is not relevant
395 -- 3. The substition is only applied ONCE! This is because
396 -- in general such application will not reached a fixed point.
398 = TvSubst InScopeSet -- The in-scope type variables
399 TvSubstEnv -- Substitution of types
400 -- See Note [Apply Once]
401 -- and Note [Extending the TvSubstEnv]
403 -- | A substitition of 'Type's for 'TyVar's
404 type TvSubstEnv = TyVarEnv Type
405 -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
406 -- invariant discussed in Note [Apply Once]), and also independently
407 -- in the middle of matching, and unification (see Types.Unify)
408 -- So you have to look at the context to know if it's idempotent or
409 -- apply-once or whatever
414 We use TvSubsts to instantiate things, and we might instantiate
418 So the substition might go [a->b, b->a]. A similar situation arises in Core
419 when we find a beta redex like
421 Then we also end up with a substition that permutes type variables. Other
422 variations happen to; for example [a -> (a, b)].
424 ***************************************************
425 *** So a TvSubst must be applied precisely once ***
426 ***************************************************
428 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
429 we use during unifications, it must not be repeatedly applied.
431 Note [Extending the TvSubst]
432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
433 See #tvsubst_invariant# for the invariants that must hold.
435 This invariant allows a short-cut when the TvSubstEnv is empty:
436 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
437 then (substTy subst ty) does nothing.
439 For example, consider:
440 (/\a. /\b:(a~Int). ...b..) Int
441 We substitute Int for 'a'. The Unique of 'b' does not change, but
442 nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
444 This invariant has several crucial consequences:
446 * In substTyVarBndr, we need extend the TvSubstEnv
447 - if the unique has changed
448 - or if the kind has changed
450 * In substTyVar, we do not need to consult the in-scope set;
451 the TvSubstEnv is enough
453 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
458 %************************************************************************
460 Pretty-printing types
462 Defined very early because of debug printing in assertions
464 %************************************************************************
466 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
467 defined to use this. @pprParendType@ is the same, except it puts
468 parens around the type, except for the atomic cases. @pprParendType@
469 works just by setting the initial context precedence very high.
472 data Prec = TopPrec -- No parens
473 | FunPrec -- Function args; no parens for tycon apps
474 | TyConPrec -- Tycon args; no parens for atomic
477 maybeParen :: Prec -> Prec -> SDoc -> SDoc
478 maybeParen ctxt_prec inner_prec pretty
479 | ctxt_prec < inner_prec = pretty
480 | otherwise = parens pretty
483 pprType, pprParendType :: Type -> SDoc
484 pprType ty = ppr_type TopPrec ty
485 pprParendType ty = ppr_type TyConPrec ty
487 pprKind, pprParendKind :: Kind -> SDoc
489 pprParendKind = pprParendType
492 pprPredTy :: PredType -> SDoc
493 pprPredTy = pprPred ppr_type
495 pprPred :: (Prec -> a -> SDoc) -> Pred a -> SDoc
496 pprPred pp (ClassP cls tys) = ppr_class_pred pp cls tys
497 pprPred pp (IParam ip ty) = ppr ip <> dcolon <> pp TopPrec ty
498 pprPred pp (EqPred ty1 ty2) = ppr_eq_pred pp (Pair ty1 ty2)
501 pprEqPred :: Pair Type -> SDoc
502 pprEqPred = ppr_eq_pred ppr_type
504 ppr_eq_pred :: (Prec -> a -> SDoc) -> Pair a -> SDoc
505 ppr_eq_pred pp (Pair ty1 ty2) = sep [ pp FunPrec ty1
506 , nest 2 (ptext (sLit "~"))
508 -- Precedence looks like (->) so that we get
511 -- Note parens on the latter!
514 pprClassPred :: Class -> [Type] -> SDoc
515 pprClassPred = ppr_class_pred ppr_type
517 ppr_class_pred :: (Prec -> a -> SDoc) -> Class -> [a] -> SDoc
518 ppr_class_pred pp clas tys = pprTypeNameApp TopPrec pp (getName clas) tys
521 pprTheta :: ThetaType -> SDoc
522 -- pprTheta [pred] = pprPred pred -- I'm in two minds about this
523 pprTheta theta = parens (sep (punctuate comma (map pprPredTy theta)))
525 pprThetaArrowTy :: ThetaType -> SDoc
526 pprThetaArrowTy = pprThetaArrow ppr_type
528 pprThetaArrow :: (Prec -> a -> SDoc) -> [Pred a] -> SDoc
529 pprThetaArrow _ [] = empty
530 pprThetaArrow pp [pred]
531 | noParenPred pred = pprPred pp pred <+> darrow
532 pprThetaArrow pp preds = parens (sep (punctuate comma (map (pprPred pp) preds)))
535 noParenPred :: Pred a -> Bool
536 -- A predicate that can appear without parens before a "=>"
539 -- But (?x::Int) => Int -> Int
540 noParenPred (ClassP {}) = True
541 noParenPred (EqPred {}) = True
542 noParenPred (IParam {}) = False
545 instance Outputable Type where
548 instance Outputable (Pred Type) where
549 ppr = pprPredTy -- Not for arbitrary (Pred a), because the
550 -- (Outputable a) doesn't give precedence
552 instance Outputable name => OutputableBndr (IPName name) where
553 pprBndr _ n = ppr n -- Simple for now
556 -- OK, here's the main printer
558 ppr_type :: Prec -> Type -> SDoc
559 ppr_type _ (TyVarTy tv) = ppr_tvar tv
560 ppr_type p (PredTy pred) = maybeParen p TyConPrec $
561 ifPprDebug (ptext (sLit "<pred>")) <> (pprPredTy pred)
562 ppr_type p (TyConApp tc tys) = pprTcApp p ppr_type tc tys
564 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
565 pprType t1 <+> ppr_type TyConPrec t2
567 ppr_type p ty@(ForAllTy {}) = ppr_forall_type p ty
568 ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
570 ppr_type p (FunTy ty1 ty2)
571 = pprArrowChain p (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
573 -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
574 ppr_fun_tail (FunTy ty1 ty2)
575 | not (is_pred ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2
576 ppr_fun_tail other_ty = [ppr_type TopPrec other_ty]
578 is_pred (PredTy {}) = True
581 ppr_forall_type :: Prec -> Type -> SDoc
583 = maybeParen p FunPrec $
584 sep [pprForAll tvs, pprThetaArrowTy ctxt, pprType tau]
586 (tvs, rho) = split1 [] ty
587 (ctxt, tau) = split2 [] rho
589 split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
590 split1 tvs ty = (reverse tvs, ty)
592 split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
593 split2 ps ty = (reverse ps, ty)
595 ppr_tvar :: TyVar -> SDoc
596 ppr_tvar tv -- Note [Infix type variables]
597 | isSymOcc (getOccName tv) = parens (ppr tv)
601 pprForAll :: [TyVar] -> SDoc
603 pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
605 pprTvBndr :: TyVar -> SDoc
607 | isLiftedTypeKind kind = ppr_tvar tv
608 | otherwise = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
613 Note [Infix type variables]
614 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
615 With TypeOperators you can say
619 and the (~>) is considered a type variable. However, the type
620 pretty-printer in this module will just see (a ~> b) as
622 App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
624 So it'll print the type in prefix form. To avoid confusion we must
625 remember to parenthesise the operator, thus
632 pprTcApp :: Prec -> (Prec -> a -> SDoc) -> TyCon -> [a] -> SDoc
633 pprTcApp _ _ tc [] -- No brackets for SymOcc
634 = pp_nt_debug <> ppr tc
636 pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
637 then ptext (sLit "<recnt>")
638 else ptext (sLit "<nt>"))
641 pprTcApp _ pp tc [ty]
642 | tc `hasKey` listTyConKey = brackets (pp TopPrec ty)
643 | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pp TopPrec ty <> ptext (sLit ":]")
644 | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
645 | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
646 | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
647 | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
648 | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
651 | isTupleTyCon tc && tyConArity tc == length tys
652 = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map (pp TopPrec) tys)))
654 = pprTypeNameApp p pp (getName tc) tys
657 pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
658 -- The first arg is the tycon, or sometimes class
659 -- Print infix if the tycon/class looks like an operator
660 pprTypeApp tc tys = pprTypeNameApp TopPrec ppr_type (getName tc) tys
662 pprTypeNameApp :: Prec -> (Prec -> a -> SDoc) -> Name -> [a] -> SDoc
663 -- Used for classes and coercions as well as types; that's why it's separate from pprTcApp
664 pprTypeNameApp p pp tc tys
665 | is_sym_occ -- Print infix if possible
666 , [ty1,ty2] <- tys -- We know nothing of precedence though
667 = maybeParen p FunPrec $
668 sep [pp FunPrec ty1, pprInfixVar True (ppr tc) <+> pp FunPrec ty2]
670 = pprPrefixApp p (pprPrefixVar is_sym_occ (ppr tc)) (map (pp TyConPrec) tys)
672 is_sym_occ = isSymOcc (getOccName tc)
675 pprPrefixApp :: Prec -> SDoc -> [SDoc] -> SDoc
676 pprPrefixApp p pp_fun pp_tys = maybeParen p TyConPrec $
677 hang pp_fun 2 (sep pp_tys)
680 pprArrowChain :: Prec -> [SDoc] -> SDoc
681 -- pprArrowChain p [a,b,c] generates a -> b -> c
682 pprArrowChain _ [] = empty
683 pprArrowChain p (arg:args) = maybeParen p FunPrec $
684 sep [arg, sep (map (arrow <+>) args)]