ef035bb3e14174c2101bc68e502f426bf2517e32
[ghc.git] / compiler / types / TypeRep.lhs
1  | %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1998
4 %
5 \section[TypeRep]{Type - friends' interface}
6
7 Note [The Type-related module hierarchy]
8 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9   Class
10   TyCon    imports Class
11   TypeRep
12   TysPrim  imports TypeRep ( including mkTyConTy )
13   Kind     imports TysPrim ( mainly for primitive kinds )
14   Type     imports Kind
15   Coercion imports Type
16
17 \begin{code}
18 {-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
19 {-# OPTIONS_HADDOCK hide #-}
20 -- We expose the relevant stuff from this module via the Type module
21
22 module TypeRep (
23         TyThing(..),
24         Type(..),
25         TyLit(..),
26         KindOrType, Kind, SuperKind,
27         PredType, ThetaType,      -- Synonyms
28
29         -- Functions over types
30         mkTyConTy, mkTyVarTy, mkTyVarTys,
31         isLiftedTypeKind, isSuperKind, isTypeVar, isKindVar,
32
33         -- Pretty-printing
34         pprType, pprParendType, pprTypeApp, pprTvBndr, pprTvBndrs,
35         pprTyThing, pprTyThingCategory, pprSigmaType,
36         pprTheta, pprForAll, pprUserForAll,
37         pprThetaArrowTy, pprClassPred,
38         pprKind, pprParendKind, pprTyLit, suppressKinds,
39         TyPrec(..), maybeParen, pprTcApp,
40         pprPrefixApp, pprArrowChain, ppr_type,
41
42         -- Free variables
43         tyVarsOfType, tyVarsOfTypes, closeOverKinds, varSetElemsKvsFirst,
44
45         -- * Tidying type related things up for printing
46         tidyType,      tidyTypes,
47         tidyOpenType,  tidyOpenTypes,
48         tidyOpenKind,
49         tidyTyVarBndr, tidyTyVarBndrs, tidyFreeTyVars,
50         tidyOpenTyVar, tidyOpenTyVars,
51         tidyTyVarOcc,
52         tidyTopType,
53         tidyKind,
54
55         -- Substitutions
56         TvSubst(..), TvSubstEnv
57     ) where
58
59 #include "HsVersions.h"
60
61 import {-# SOURCE #-} DataCon( dataConTyCon )
62 import ConLike ( ConLike(..) )
63 import {-# SOURCE #-} Type( isPredTy ) -- Transitively pulls in a LOT of stuff, better to break the loop
64
65 -- friends:
66 import Var
67 import VarEnv
68 import VarSet
69 import Name
70 import BasicTypes
71 import TyCon
72 import Class
73 import CoAxiom
74
75 -- others
76 import PrelNames
77 import Outputable
78 import FastString
79 import Util
80 import DynFlags
81
82 -- libraries
83 import Data.List( mapAccumL, partition )
84 import qualified Data.Data        as Data hiding ( TyCon )
85 \end{code}
86
87
88 %************************************************************************
89 %*                                                                      *
90 \subsection{The data type}
91 %*                                                                      *
92 %************************************************************************
93
94
95 \begin{code}
96 -- | The key representation of types within the compiler
97
98 -- If you edit this type, you may need to update the GHC formalism
99 -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
100 data Type
101   = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
102
103   | AppTy         -- See Note [AppTy invariant]
104         Type
105         Type            -- ^ Type application to something other than a 'TyCon'. Parameters:
106                         --
107                         --  1) Function: must /not/ be a 'TyConApp',
108                         --     must be another 'AppTy', or 'TyVarTy'
109                         --
110                         --  2) Argument type
111
112   | TyConApp      -- See Note [AppTy invariant]
113         TyCon
114         [KindOrType]    -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
115                         -- Invariant: saturated appliations of 'FunTyCon' must
116                         -- use 'FunTy' and saturated synonyms must use their own
117                         -- constructors. However, /unsaturated/ 'FunTyCon's
118                         -- do appear as 'TyConApp's.
119                         -- Parameters:
120                         --
121                         -- 1) Type constructor being applied to.
122                         --
123                         -- 2) Type arguments. Might not have enough type arguments
124                         --    here to saturate the constructor.
125                         --    Even type synonyms are not necessarily saturated;
126                         --    for example unsaturated type synonyms
127                         --    can appear as the right hand side of a type synonym.
128
129   | FunTy
130         Type
131         Type            -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
132                         -- See Note [Equality-constrained types]
133
134   | ForAllTy
135         Var         -- Type or kind variable
136         Type            -- ^ A polymorphic type
137
138   | LitTy TyLit     -- ^ Type literals are similar to type constructors.
139
140   deriving (Data.Data, Data.Typeable)
141
142
143 -- NOTE:  Other parts of the code assume that type literals do not contain
144 -- types or type variables.
145 data TyLit
146   = NumTyLit Integer
147   | StrTyLit FastString
148   deriving (Eq, Ord, Data.Data, Data.Typeable)
149
150 type KindOrType = Type -- See Note [Arguments to type constructors]
151
152 -- | The key type representing kinds in the compiler.
153 -- Invariant: a kind is always in one of these forms:
154 --
155 -- > FunTy k1 k2
156 -- > TyConApp PrimTyCon [...]
157 -- > TyVar kv   -- (during inference only)
158 -- > ForAll ... -- (for top-level coercions)
159 type Kind = Type
160
161 -- | "Super kinds", used to help encode 'Kind's as types.
162 -- Invariant: a super kind is always of this form:
163 --
164 -- > TyConApp SuperKindTyCon ...
165 type SuperKind = Type
166 \end{code}
167
168 Note [The kind invariant]
169 ~~~~~~~~~~~~~~~~~~~~~~~~~
170 The kinds
171    #          UnliftedTypeKind
172    OpenKind   super-kind of *, #
173
174 can never appear under an arrow or type constructor in a kind; they
175 can only be at the top level of a kind.  It follows that primitive TyCons,
176 which have a naughty pseudo-kind
177    State# :: * -> #
178 must always be saturated, so that we can never get a type whose kind
179 has a UnliftedTypeKind or ArgTypeKind underneath an arrow.
180
181 Nor can we abstract over a type variable with any of these kinds.
182
183     k :: = kk | # | ArgKind | (#) | OpenKind
184     kk :: = * | kk -> kk | T kk1 ... kkn
185
186 So a type variable can only be abstracted kk.
187
188 Note [Arguments to type constructors]
189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
190 Because of kind polymorphism, in addition to type application we now
191 have kind instantiation. We reuse the same notations to do so.
192
193 For example:
194
195   Just (* -> *) Maybe
196   Right * Nat Zero
197
198 are represented by:
199
200   TyConApp (PromotedDataCon Just) [* -> *, Maybe]
201   TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)]
202
203 Important note: Nat is used as a *kind* and not as a type. This can be
204 confusing, since type-level Nat and kind-level Nat are identical. We
205 use the kind of (PromotedDataCon Right) to know if its arguments are
206 kinds or types.
207
208 This kind instantiation only happens in TyConApp currently.
209
210
211 Note [Equality-constrained types]
212 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
213 The type   forall ab. (a ~ [b]) => blah
214 is encoded like this:
215
216    ForAllTy (a:*) $ ForAllTy (b:*) $
217    FunTy (TyConApp (~) [a, [b]]) $
218    blah
219
220 -------------------------------------
221                 Note [PredTy]
222
223 \begin{code}
224 -- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
225 -- the Haskell predicate @p@, where a predicate is what occurs before
226 -- the @=>@ in a Haskell type.
227 --
228 -- We use 'PredType' as documentation to mark those types that we guarantee to have
229 -- this kind.
230 --
231 -- It can be expanded into its representation, but:
232 --
233 -- * The type checker must treat it as opaque
234 --
235 -- * The rest of the compiler treats it as transparent
236 --
237 -- Consider these examples:
238 --
239 -- > f :: (Eq a) => a -> Int
240 -- > g :: (?x :: Int -> Int) => a -> Int
241 -- > h :: (r\l) => {r} => {l::Int | r}
242 --
243 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
244 type PredType = Type
245
246 -- | A collection of 'PredType's
247 type ThetaType = [PredType]
248 \end{code}
249
250 (We don't support TREX records yet, but the setup is designed
251 to expand to allow them.)
252
253 A Haskell qualified type, such as that for f,g,h above, is
254 represented using
255         * a FunTy for the double arrow
256         * with a type of kind Constraint as the function argument
257
258 The predicate really does turn into a real extra argument to the
259 function.  If the argument has type (p :: Constraint) then the predicate p is
260 represented by evidence of type p.
261
262 %************************************************************************
263 %*                                                                      *
264             Simple constructors
265 %*                                                                      *
266 %************************************************************************
267
268 These functions are here so that they can be used by TysPrim,
269 which in turn is imported by Type
270
271 \begin{code}
272 mkTyVarTy  :: TyVar   -> Type
273 mkTyVarTy  = TyVarTy
274
275 mkTyVarTys :: [TyVar] -> [Type]
276 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
277
278 -- | Create the plain type constructor type which has been applied to no type arguments at all.
279 mkTyConTy :: TyCon -> Type
280 mkTyConTy tycon = TyConApp tycon []
281 \end{code}
282
283 Some basic functions, put here to break loops eg with the pretty printer
284
285 \begin{code}
286 isLiftedTypeKind :: Kind -> Bool
287 isLiftedTypeKind (TyConApp tc []) = tc `hasKey` liftedTypeKindTyConKey
288 isLiftedTypeKind _                = False
289
290 -- | Is this a super-kind (i.e. a type-of-kinds)?
291 isSuperKind :: Type -> Bool
292 isSuperKind (TyConApp skc []) = skc `hasKey` superKindTyConKey
293 isSuperKind _                 = False
294
295 isTypeVar :: Var -> Bool
296 isTypeVar v = isTKVar v && not (isSuperKind (varType v))
297
298 isKindVar :: Var -> Bool
299 isKindVar v = isTKVar v && isSuperKind (varType v)
300 \end{code}
301
302
303 %************************************************************************
304 %*                                                                      *
305                         Free variables of types and coercions
306 %*                                                                      *
307 %************************************************************************
308
309 \begin{code}
310 tyVarsOfType :: Type -> VarSet
311 -- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
312 -- tyVarsOfType returns only the free variables of a type
313 -- For example, tyVarsOfType (a::k) returns {a}, not including the
314 -- kind variable {k}
315 tyVarsOfType (TyVarTy v)         = unitVarSet v
316 tyVarsOfType (TyConApp _ tys)    = tyVarsOfTypes tys
317 tyVarsOfType (LitTy {})          = emptyVarSet
318 tyVarsOfType (FunTy arg res)     = tyVarsOfType arg `unionVarSet` tyVarsOfType res
319 tyVarsOfType (AppTy fun arg)     = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
320 tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
321                                    `unionVarSet` tyVarsOfType (tyVarKind tyvar)
322
323 tyVarsOfTypes :: [Type] -> TyVarSet
324 tyVarsOfTypes = mapUnionVarSet tyVarsOfType
325
326 closeOverKinds :: TyVarSet -> TyVarSet
327 -- Add the kind variables free in the kinds
328 -- of the tyvars in the given set
329 closeOverKinds tvs
330   = foldVarSet (\tv ktvs -> tyVarsOfType (tyVarKind tv) `unionVarSet` ktvs)
331                tvs tvs
332
333 varSetElemsKvsFirst :: VarSet -> [TyVar]
334 -- {k1,a,k2,b} --> [k1,k2,a,b]
335 varSetElemsKvsFirst set
336   = kvs ++ tvs
337   where
338     (kvs, tvs) = partition isKindVar (varSetElems set)
339 \end{code}
340
341 %************************************************************************
342 %*                                                                      *
343                         TyThing
344 %*                                                                      *
345 %************************************************************************
346
347 Despite the fact that DataCon has to be imported via a hi-boot route,
348 this module seems the right place for TyThing, because it's needed for
349 funTyCon and all the types in TysPrim.
350
351 Note [ATyCon for classes]
352 ~~~~~~~~~~~~~~~~~~~~~~~~~
353 Both classes and type constructors are represented in the type environment
354 as ATyCon.  You can tell the difference, and get to the class, with
355    isClassTyCon :: TyCon -> Bool
356    tyConClass_maybe :: TyCon -> Maybe Class
357 The Class and its associated TyCon have the same Name.
358
359 \begin{code}
360 -- | A typecheckable-thing, essentially anything that has a name
361 data TyThing
362   = AnId     Id
363   | AConLike ConLike
364   | ATyCon   TyCon       -- TyCons and classes; see Note [ATyCon for classes]
365   | ACoAxiom (CoAxiom Branched)
366   deriving (Eq, Ord)
367
368 instance Outputable TyThing where
369   ppr = pprTyThing
370
371 pprTyThing :: TyThing -> SDoc
372 pprTyThing thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))
373
374 pprTyThingCategory :: TyThing -> SDoc
375 pprTyThingCategory (ATyCon tc)
376   | isClassTyCon tc = ptext (sLit "Class")
377   | otherwise       = ptext (sLit "Type constructor")
378 pprTyThingCategory (ACoAxiom _) = ptext (sLit "Coercion axiom")
379 pprTyThingCategory (AnId   _)   = ptext (sLit "Identifier")
380 pprTyThingCategory (AConLike (RealDataCon _)) = ptext (sLit "Data constructor")
381 pprTyThingCategory (AConLike (PatSynCon _))  = ptext (sLit "Pattern synonym")
382
383
384 instance NamedThing TyThing where       -- Can't put this with the type
385   getName (AnId id)     = getName id    -- decl, because the DataCon instance
386   getName (ATyCon tc)   = getName tc    -- isn't visible there
387   getName (ACoAxiom cc) = getName cc
388   getName (AConLike cl) = getName cl
389
390 \end{code}
391
392
393 %************************************************************************
394 %*                                                                      *
395                         Substitutions
396       Data type defined here to avoid unnecessary mutual recursion
397 %*                                                                      *
398 %************************************************************************
399
400 \begin{code}
401 -- | Type substitution
402 --
403 -- #tvsubst_invariant#
404 -- The following invariants must hold of a 'TvSubst':
405 --
406 -- 1. The in-scope set is needed /only/ to
407 -- guide the generation of fresh uniques
408 --
409 -- 2. In particular, the /kind/ of the type variables in
410 -- the in-scope set is not relevant
411 --
412 -- 3. The substitution is only applied ONCE! This is because
413 -- in general such application will not reached a fixed point.
414 data TvSubst
415   = TvSubst InScopeSet  -- The in-scope type and kind variables
416             TvSubstEnv  -- Substitutes both type and kind variables
417         -- See Note [Apply Once]
418         -- and Note [Extending the TvSubstEnv]
419
420 -- | A substitution of 'Type's for 'TyVar's
421 --                 and 'Kind's for 'KindVar's
422 type TvSubstEnv = TyVarEnv Type
423         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
424         -- invariant discussed in Note [Apply Once]), and also independently
425         -- in the middle of matching, and unification (see Types.Unify)
426         -- So you have to look at the context to know if it's idempotent or
427         -- apply-once or whatever
428 \end{code}
429
430 Note [Apply Once]
431 ~~~~~~~~~~~~~~~~~
432 We use TvSubsts to instantiate things, and we might instantiate
433         forall a b. ty
434 \with the types
435         [a, b], or [b, a].
436 So the substitution might go [a->b, b->a].  A similar situation arises in Core
437 when we find a beta redex like
438         (/\ a /\ b -> e) b a
439 Then we also end up with a substitution that permutes type variables. Other
440 variations happen to; for example [a -> (a, b)].
441
442         ***************************************************
443         *** So a TvSubst must be applied precisely once ***
444         ***************************************************
445
446 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
447 we use during unifications, it must not be repeatedly applied.
448
449 Note [Extending the TvSubst]
450 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
451 See #tvsubst_invariant# for the invariants that must hold.
452
453 This invariant allows a short-cut when the TvSubstEnv is empty:
454 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
455 then (substTy subst ty) does nothing.
456
457 For example, consider:
458         (/\a. /\b:(a~Int). ...b..) Int
459 We substitute Int for 'a'.  The Unique of 'b' does not change, but
460 nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
461
462 This invariant has several crucial consequences:
463
464 * In substTyVarBndr, we need extend the TvSubstEnv
465         - if the unique has changed
466         - or if the kind has changed
467
468 * In substTyVar, we do not need to consult the in-scope set;
469   the TvSubstEnv is enough
470
471 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
472
473
474
475 %************************************************************************
476 %*                                                                      *
477                    Pretty-printing types
478
479        Defined very early because of debug printing in assertions
480 %*                                                                      *
481 %************************************************************************
482
483 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
484 defined to use this.  @pprParendType@ is the same, except it puts
485 parens around the type, except for the atomic cases.  @pprParendType@
486 works just by setting the initial context precedence very high.
487
488 Note [Precedence in types]
489 ~~~~~~~~~~~~~~~~~~~~~~~~~~
490 We don't keep the fixity of type operators in the operator. So the pretty printer
491 operates the following precedene structre:
492    Type constructor application   binds more tightly than
493    Oerator applications           which bind more tightly than
494    Function arrow
495
496 So we might see  a :+: T b -> c
497 meaning          (a :+: (T b)) -> c
498
499 Maybe operator applications should bind a bit less tightly?
500
501 Anyway, that's the current story, and it is used consistently for Type and HsType
502
503 \begin{code}
504 data TyPrec   -- See Note [Prededence in types]
505
506   = TopPrec         -- No parens
507   | FunPrec         -- Function args; no parens for tycon apps
508   | TyOpPrec        -- Infix operator
509   | TyConPrec       -- Tycon args; no parens for atomic
510   deriving( Eq, Ord )
511
512 maybeParen :: TyPrec -> TyPrec -> SDoc -> SDoc
513 maybeParen ctxt_prec inner_prec pretty
514   | ctxt_prec < inner_prec = pretty
515   | otherwise              = parens pretty
516
517 ------------------
518 pprType, pprParendType :: Type -> SDoc
519 pprType       ty = ppr_type TopPrec ty
520 pprParendType ty = ppr_type TyConPrec ty
521
522 pprTyLit :: TyLit -> SDoc
523 pprTyLit = ppr_tylit TopPrec
524
525 pprKind, pprParendKind :: Kind -> SDoc
526 pprKind       = pprType
527 pprParendKind = pprParendType
528
529 ------------
530 pprClassPred :: Class -> [Type] -> SDoc
531 pprClassPred clas tys = pprTypeApp (classTyCon clas) tys
532
533 ------------
534 pprTheta :: ThetaType -> SDoc
535 -- pprTheta [pred] = pprPred pred        -- I'm in two minds about this
536 pprTheta theta  = parens (sep (punctuate comma (map (ppr_type TopPrec) theta)))
537
538 pprThetaArrowTy :: ThetaType -> SDoc
539 pprThetaArrowTy []     = empty
540 pprThetaArrowTy [pred] = ppr_type TyOpPrec pred <+> darrow
541                          -- TyOpPrec:  Num a     => a -> a  does not need parens
542                          --      bug   (a :~: b) => a -> b  currently does
543                          -- Trac # 9658
544 pprThetaArrowTy preds  = parens (fsep (punctuate comma (map (ppr_type TopPrec) preds)))
545                             <+> darrow
546     -- Notice 'fsep' here rather that 'sep', so that
547     -- type contexts don't get displayed in a giant column
548     -- Rather than
549     --  instance (Eq a,
550     --            Eq b,
551     --            Eq c,
552     --            Eq d,
553     --            Eq e,
554     --            Eq f,
555     --            Eq g,
556     --            Eq h,
557     --            Eq i,
558     --            Eq j,
559     --            Eq k,
560     --            Eq l) =>
561     --           Eq (a, b, c, d, e, f, g, h, i, j, k, l)
562     -- we get
563     --
564     --  instance (Eq a, Eq b, Eq c, Eq d, Eq e, Eq f, Eq g, Eq h, Eq i,
565     --            Eq j, Eq k, Eq l) =>
566     --           Eq (a, b, c, d, e, f, g, h, i, j, k, l)
567
568 ------------------
569 instance Outputable Type where
570     ppr ty = pprType ty
571
572 instance Outputable TyLit where
573    ppr = pprTyLit
574
575 ------------------
576         -- OK, here's the main printer
577
578 ppr_type :: TyPrec -> Type -> SDoc
579 ppr_type _ (TyVarTy tv)       = ppr_tvar tv
580 ppr_type p (TyConApp tc tys)  = pprTyTcApp p tc tys
581 ppr_type p (LitTy l)          = ppr_tylit p l
582 ppr_type p ty@(ForAllTy {})   = ppr_forall_type p ty
583
584 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
585                            ppr_type FunPrec t1 <+> ppr_type TyConPrec t2
586
587 ppr_type p fun_ty@(FunTy ty1 ty2)
588   | isPredTy ty1
589   = ppr_forall_type p fun_ty
590   | otherwise
591   = pprArrowChain p (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
592   where
593     -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
594     ppr_fun_tail (FunTy ty1 ty2)
595       | not (isPredTy ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2
596     ppr_fun_tail other_ty = [ppr_type TopPrec other_ty]
597
598
599 ppr_forall_type :: TyPrec -> Type -> SDoc
600 ppr_forall_type p ty
601   = maybeParen p FunPrec $ ppr_sigma_type True ty
602     -- True <=> we always print the foralls on *nested* quantifiers
603     -- Opt_PrintExplicitForalls only affects top-level quantifiers
604
605 ppr_tvar :: TyVar -> SDoc
606 ppr_tvar tv  -- Note [Infix type variables]
607   = parenSymOcc (getOccName tv) (ppr tv)
608
609 ppr_tylit :: TyPrec -> TyLit -> SDoc
610 ppr_tylit _ tl =
611   case tl of
612     NumTyLit n -> integer n
613     StrTyLit s -> text (show s)
614
615 -------------------
616 ppr_sigma_type :: Bool -> Type -> SDoc
617 -- Bool <=> Show the foralls unconditionally
618 ppr_sigma_type show_foralls_unconditionally ty
619   = sep [ if   show_foralls_unconditionally
620           then pprForAll tvs
621           else pprUserForAll tvs
622         , pprThetaArrowTy ctxt
623         , pprType tau ]
624   where
625     (tvs,  rho) = split1 [] ty
626     (ctxt, tau) = split2 [] rho
627
628     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
629     split1 tvs ty               = (reverse tvs, ty)
630
631     split2 ps (ty1 `FunTy` ty2) | isPredTy ty1 = split2 (ty1:ps) ty2
632     split2 ps ty                               = (reverse ps, ty)
633
634 pprSigmaType :: Type -> SDoc
635 pprSigmaType ty = ppr_sigma_type False ty
636
637 pprUserForAll :: [TyVar] -> SDoc
638 -- Print a user-level forall; see Note [WHen to print foralls]
639 pprUserForAll tvs
640   = sdocWithDynFlags $ \dflags ->
641     ppWhen (any tv_has_kind_var tvs || gopt Opt_PrintExplicitForalls dflags) $
642     pprForAll tvs
643   where
644     tv_has_kind_var tv = not (isEmptyVarSet (tyVarsOfType (tyVarKind tv)))
645
646 pprForAll :: [TyVar] -> SDoc
647 pprForAll []  = empty
648 pprForAll tvs = forAllLit <+> pprTvBndrs tvs <> dot
649
650 pprTvBndrs :: [TyVar] -> SDoc
651 pprTvBndrs tvs = sep (map pprTvBndr tvs)
652
653 pprTvBndr :: TyVar -> SDoc
654 pprTvBndr tv
655   | isLiftedTypeKind kind = ppr_tvar tv
656   | otherwise             = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
657              where
658                kind = tyVarKind tv
659 \end{code}
660
661 Note [When to print foralls]
662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
663 Mostly we want to print top-level foralls when (and only when) the user specifies
664 -fprint-explicit-foralls.  But when kind polymorphism is at work, that suppresses
665 too much information; see Trac #9018.
666
667 So I'm trying out this rule: print explicit foralls if
668   a) User specifies -fprint-explicit-foralls, or
669   b) Any of the quantified type variables has a kind
670      that mentions a kind variable
671
672 This catches common situations, such as a type siguature
673      f :: m a
674 which means
675       f :: forall k. forall (m :: k->*) (a :: k). m a
676 We really want to see both the "forall k" and the kind signatures
677 on m and a.  The latter comes from pprTvBndr.
678
679 Note [Infix type variables]
680 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
681 With TypeOperators you can say
682
683    f :: (a ~> b) -> b
684
685 and the (~>) is considered a type variable.  However, the type
686 pretty-printer in this module will just see (a ~> b) as
687
688    App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
689
690 So it'll print the type in prefix form.  To avoid confusion we must
691 remember to parenthesise the operator, thus
692
693    (~>) a b -> b
694
695 See Trac #2766.
696
697 \begin{code}
698 pprTypeApp :: TyCon -> [Type] -> SDoc
699 pprTypeApp tc tys = pprTyTcApp TopPrec tc tys
700         -- We have to use ppr on the TyCon (not its name)
701         -- so that we get promotion quotes in the right place
702
703 pprTyTcApp :: TyPrec -> TyCon -> [Type] -> SDoc
704 -- Used for types only; so that we can make a
705 -- special case for type-level lists
706 pprTyTcApp p tc tys
707   | tc `hasKey` ipClassNameKey
708   , [LitTy (StrTyLit n),ty] <- tys
709   = maybeParen p FunPrec $
710     char '?' <> ftext n <> ptext (sLit "::") <> ppr_type TopPrec ty
711
712   | tc `hasKey` consDataConKey
713   , [_kind,ty1,ty2] <- tys
714   = sdocWithDynFlags $ \dflags ->
715     if gopt Opt_PrintExplicitKinds dflags then pprTcApp  p ppr_type tc tys
716                                    else pprTyList p ty1 ty2
717
718   | otherwise
719   = pprTcApp p ppr_type tc tys
720
721 pprTcApp :: TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> SDoc
722 -- Used for both types and coercions, hence polymorphism
723 pprTcApp _ pp tc [ty]
724   | tc `hasKey` listTyConKey = pprPromotionQuote tc <> brackets   (pp TopPrec ty)
725   | tc `hasKey` parrTyConKey = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
726
727 pprTcApp p pp tc tys
728   | isTupleTyCon tc && tyConArity tc == length tys
729   = pprPromotionQuote tc <>
730     tupleParens (tupleTyConSort tc) (sep (punctuate comma (map (pp TopPrec) tys)))
731
732   | Just dc <- isPromotedDataCon_maybe tc
733   , let dc_tc = dataConTyCon dc
734   , isTupleTyCon dc_tc
735   , let arity = tyConArity dc_tc    -- E.g. 3 for (,,) k1 k2 k3 t1 t2 t3
736         ty_args = drop arity tys    -- Drop the kind args
737   , ty_args `lengthIs` arity        -- Result is saturated
738   = pprPromotionQuote tc <>
739     (tupleParens (tupleTyConSort dc_tc) $
740      sep (punctuate comma (map (pp TopPrec) ty_args)))
741
742   | otherwise
743   = sdocWithDynFlags (pprTcApp_help p pp tc tys)
744
745 pprTcApp_help :: TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> DynFlags -> SDoc
746 -- This one has accss to the DynFlags
747 pprTcApp_help p pp tc tys dflags
748   | not (isSymOcc (nameOccName (tyConName tc)))
749   = pprPrefixApp p (ppr tc) (map (pp TyConPrec) tys_wo_kinds)
750
751   | [ty1,ty2] <- tys_wo_kinds  -- Infix, two arguments;
752                                -- we know nothing of precedence though
753   = pprInfixApp p pp (ppr tc) ty1 ty2
754
755   |  tc `hasKey` liftedTypeKindTyConKey
756   || tc `hasKey` unliftedTypeKindTyConKey
757   = ASSERT( null tys ) ppr tc   -- Do not wrap *, # in parens
758
759   | otherwise
760   = pprPrefixApp p (parens (ppr tc)) (map (pp TyConPrec) tys_wo_kinds)
761   where
762     tys_wo_kinds = suppressKinds dflags (tyConKind tc) tys
763
764 ------------------
765 suppressKinds :: DynFlags -> Kind -> [a] -> [a]
766 -- Given the kind of a TyCon, and the args to which it is applied,
767 -- suppress the args that are kind args
768 -- C.f. Note [Suppressing kinds] in IfaceType
769 suppressKinds dflags kind xs
770   | gopt Opt_PrintExplicitKinds dflags = xs
771   | otherwise                          = suppress kind xs
772   where
773     suppress (ForAllTy _ kind) (_ : xs) = suppress kind xs
774     suppress (FunTy _ res)     (x:xs)   = x : suppress res xs
775     suppress _                 xs       = xs
776
777 ----------------
778 pprTyList :: TyPrec -> Type -> Type -> SDoc
779 -- Given a type-level list (t1 ': t2), see if we can print
780 -- it in list notation [t1, ...].
781 pprTyList p ty1 ty2
782   = case gather ty2 of
783       (arg_tys, Nothing) -> char '\'' <> brackets (fsep (punctuate comma
784                                             (map (ppr_type TopPrec) (ty1:arg_tys))))
785       (arg_tys, Just tl) -> maybeParen p FunPrec $
786                             hang (ppr_type FunPrec ty1)
787                                2 (fsep [ colon <+> ppr_type FunPrec ty | ty <- arg_tys ++ [tl]])
788   where
789     gather :: Type -> ([Type], Maybe Type)
790      -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
791      --             = (tys, Just tl) means ty is of form t1:t2:...tn:tl
792     gather (TyConApp tc tys)
793       | tc `hasKey` consDataConKey
794       , [_kind, ty1,ty2] <- tys
795       , (args, tl) <- gather ty2
796       = (ty1:args, tl)
797       | tc `hasKey` nilDataConKey
798       = ([], Nothing)
799     gather ty = ([], Just ty)
800
801 ----------------
802 pprInfixApp :: TyPrec -> (TyPrec -> a -> SDoc) -> SDoc -> a -> a -> SDoc
803 pprInfixApp p pp pp_tc ty1 ty2
804   = maybeParen p TyOpPrec $
805     sep [pp TyOpPrec ty1, pprInfixVar True pp_tc <+> pp TyOpPrec ty2]
806
807 pprPrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
808 pprPrefixApp p pp_fun pp_tys
809   | null pp_tys = pp_fun
810   | otherwise   = maybeParen p TyConPrec $
811                   hang pp_fun 2 (sep pp_tys)
812
813 ----------------
814 pprArrowChain :: TyPrec -> [SDoc] -> SDoc
815 -- pprArrowChain p [a,b,c]  generates   a -> b -> c
816 pprArrowChain _ []         = empty
817 pprArrowChain p (arg:args) = maybeParen p FunPrec $
818                              sep [arg, sep (map (arrow <+>) args)]
819 \end{code}
820
821 %************************************************************************
822 %*                                                                      *
823 \subsection{TidyType}
824 %*                                                                      *
825 %************************************************************************
826
827 Tidying is here because it has a special case for FlatSkol
828
829 \begin{code}
830 -- | This tidies up a type for printing in an error message, or in
831 -- an interface file.
832 --
833 -- It doesn't change the uniques at all, just the print names.
834 tidyTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
835 tidyTyVarBndrs env tvs = mapAccumL tidyTyVarBndr env tvs
836
837 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
838 tidyTyVarBndr tidy_env@(occ_env, subst) tyvar
839   = case tidyOccName occ_env occ1 of
840       (tidy', occ') -> ((tidy', subst'), tyvar')
841         where
842           subst' = extendVarEnv subst tyvar tyvar'
843           tyvar' = setTyVarKind (setTyVarName tyvar name') kind'
844           name'  = tidyNameOcc name occ'
845           kind'  = tidyKind tidy_env (tyVarKind tyvar)
846   where
847     name = tyVarName tyvar
848     occ  = getOccName name
849     -- System Names are for unification variables;
850     -- when we tidy them we give them a trailing "0" (or 1 etc)
851     -- so that they don't take precedence for the un-modified name
852     occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0")
853          | otherwise         = occ
854
855
856 ---------------
857 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
858 -- ^ Add the free 'TyVar's to the env in tidy form,
859 -- so that we can tidy the type they are free in
860 tidyFreeTyVars (full_occ_env, var_env) tyvars
861   = fst (tidyOpenTyVars (full_occ_env, var_env) (varSetElems tyvars))
862
863         ---------------
864 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
865 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
866
867 ---------------
868 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
869 -- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
870 -- using the environment if one has not already been allocated. See
871 -- also 'tidyTyVarBndr'
872 tidyOpenTyVar env@(_, subst) tyvar
873   = case lookupVarEnv subst tyvar of
874         Just tyvar' -> (env, tyvar')            -- Already substituted
875         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
876
877 ---------------
878 tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
879 tidyTyVarOcc (_, subst) tv
880   = case lookupVarEnv subst tv of
881         Nothing  -> tv
882         Just tv' -> tv'
883
884 ---------------
885 tidyTypes :: TidyEnv -> [Type] -> [Type]
886 tidyTypes env tys = map (tidyType env) tys
887
888 ---------------
889 tidyType :: TidyEnv -> Type -> Type
890 tidyType _   (LitTy n)            = LitTy n
891 tidyType env (TyVarTy tv)         = TyVarTy (tidyTyVarOcc env tv)
892 tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
893                                     in args `seqList` TyConApp tycon args
894 tidyType env (AppTy fun arg)      = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
895 tidyType env (FunTy fun arg)      = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
896 tidyType env (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
897                                   where
898                                     (envp, tvp) = tidyTyVarBndr env tv
899
900 ---------------
901 -- | Grabs the free type variables, tidies them
902 -- and then uses 'tidyType' to work over the type itself
903 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
904 tidyOpenType env ty
905   = (env', tidyType (trimmed_occ_env, var_env) ty)
906   where
907     (env'@(_, var_env), tvs') = tidyOpenTyVars env (varSetElems (tyVarsOfType ty))
908     trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
909       -- The idea here was that we restrict the new TidyEnv to the
910       -- _free_ vars of the type, so that we don't gratuitously rename
911       -- the _bound_ variables of the type.
912
913 ---------------
914 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
915 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
916
917 ---------------
918 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
919 tidyTopType :: Type -> Type
920 tidyTopType ty = tidyType emptyTidyEnv ty
921
922 ---------------
923 tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
924 tidyOpenKind = tidyOpenType
925
926 tidyKind :: TidyEnv -> Kind -> Kind
927 tidyKind = tidyType
928 \end{code}