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