Implement Partial Type Signatures
[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, pprSigmaTypeExtraCts,
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 pprThetaArrowTyExtra :: ThetaType -> SDoc
569 pprThetaArrowTyExtra []    = text "_" <+> darrow
570 pprThetaArrowTyExtra preds = parens (fsep (punctuate comma xs)) <+> darrow
571   where xs = (map (ppr_type TopPrec) preds) ++ [text "_"]
572 ------------------
573 instance Outputable Type where
574     ppr ty = pprType ty
575
576 instance Outputable TyLit where
577    ppr = pprTyLit
578
579 ------------------
580         -- OK, here's the main printer
581
582 ppr_type :: TyPrec -> Type -> SDoc
583 ppr_type _ (TyVarTy tv)       = ppr_tvar tv
584 ppr_type p (TyConApp tc tys)  = pprTyTcApp p tc tys
585 ppr_type p (LitTy l)          = ppr_tylit p l
586 ppr_type p ty@(ForAllTy {})   = ppr_forall_type p ty
587
588 ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
589                            ppr_type FunPrec t1 <+> ppr_type TyConPrec t2
590
591 ppr_type p fun_ty@(FunTy ty1 ty2)
592   | isPredTy ty1
593   = ppr_forall_type p fun_ty
594   | otherwise
595   = pprArrowChain p (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
596   where
597     -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
598     ppr_fun_tail (FunTy ty1 ty2)
599       | not (isPredTy ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2
600     ppr_fun_tail other_ty = [ppr_type TopPrec other_ty]
601
602
603 ppr_forall_type :: TyPrec -> Type -> SDoc
604 ppr_forall_type p ty
605   = maybeParen p FunPrec $ ppr_sigma_type True False ty
606     -- True <=> we always print the foralls on *nested* quantifiers
607     -- Opt_PrintExplicitForalls only affects top-level quantifiers
608     -- False <=> we don't print an extra-constraints wildcard
609
610 ppr_tvar :: TyVar -> SDoc
611 ppr_tvar tv  -- Note [Infix type variables]
612   = parenSymOcc (getOccName tv) (ppr tv)
613
614 ppr_tylit :: TyPrec -> TyLit -> SDoc
615 ppr_tylit _ tl =
616   case tl of
617     NumTyLit n -> integer n
618     StrTyLit s -> text (show s)
619
620 -------------------
621 ppr_sigma_type :: Bool -> Bool -> Type -> SDoc
622 -- First Bool <=> Show the foralls unconditionally
623 -- Second Bool <=> Show an extra-constraints wildcard
624 ppr_sigma_type show_foralls_unconditionally extra_cts ty
625   = sep [ if   show_foralls_unconditionally
626           then pprForAll tvs
627           else pprUserForAll tvs
628         , if extra_cts
629           then pprThetaArrowTyExtra ctxt
630           else pprThetaArrowTy ctxt
631         , pprType tau ]
632   where
633     (tvs,  rho) = split1 [] ty
634     (ctxt, tau) = split2 [] rho
635
636     split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
637     split1 tvs ty               = (reverse tvs, ty)
638
639     split2 ps (ty1 `FunTy` ty2) | isPredTy ty1 = split2 (ty1:ps) ty2
640     split2 ps ty                               = (reverse ps, ty)
641
642 pprSigmaType :: Type -> SDoc
643 pprSigmaType ty = ppr_sigma_type False False ty
644
645 pprSigmaTypeExtraCts :: Bool -> Type -> SDoc
646 pprSigmaTypeExtraCts = ppr_sigma_type False
647
648 pprUserForAll :: [TyVar] -> SDoc
649 -- Print a user-level forall; see Note [WHen to print foralls]
650 pprUserForAll tvs
651   = sdocWithDynFlags $ \dflags ->
652     ppWhen (any tv_has_kind_var tvs || gopt Opt_PrintExplicitForalls dflags) $
653     pprForAll tvs
654   where
655     tv_has_kind_var tv = not (isEmptyVarSet (tyVarsOfType (tyVarKind tv)))
656
657 pprForAll :: [TyVar] -> SDoc
658 pprForAll []  = empty
659 pprForAll tvs = forAllLit <+> pprTvBndrs tvs <> dot
660
661 pprTvBndrs :: [TyVar] -> SDoc
662 pprTvBndrs tvs = sep (map pprTvBndr tvs)
663
664 pprTvBndr :: TyVar -> SDoc
665 pprTvBndr tv
666   | isLiftedTypeKind kind = ppr_tvar tv
667   | otherwise             = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
668              where
669                kind = tyVarKind tv
670 \end{code}
671
672 Note [When to print foralls]
673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
674 Mostly we want to print top-level foralls when (and only when) the user specifies
675 -fprint-explicit-foralls.  But when kind polymorphism is at work, that suppresses
676 too much information; see Trac #9018.
677
678 So I'm trying out this rule: print explicit foralls if
679   a) User specifies -fprint-explicit-foralls, or
680   b) Any of the quantified type variables has a kind
681      that mentions a kind variable
682
683 This catches common situations, such as a type siguature
684      f :: m a
685 which means
686       f :: forall k. forall (m :: k->*) (a :: k). m a
687 We really want to see both the "forall k" and the kind signatures
688 on m and a.  The latter comes from pprTvBndr.
689
690 Note [Infix type variables]
691 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
692 With TypeOperators you can say
693
694    f :: (a ~> b) -> b
695
696 and the (~>) is considered a type variable.  However, the type
697 pretty-printer in this module will just see (a ~> b) as
698
699    App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
700
701 So it'll print the type in prefix form.  To avoid confusion we must
702 remember to parenthesise the operator, thus
703
704    (~>) a b -> b
705
706 See Trac #2766.
707
708 \begin{code}
709 pprTypeApp :: TyCon -> [Type] -> SDoc
710 pprTypeApp tc tys = pprTyTcApp TopPrec tc tys
711         -- We have to use ppr on the TyCon (not its name)
712         -- so that we get promotion quotes in the right place
713
714 pprTyTcApp :: TyPrec -> TyCon -> [Type] -> SDoc
715 -- Used for types only; so that we can make a
716 -- special case for type-level lists
717 pprTyTcApp p tc tys
718   | tc `hasKey` ipClassNameKey
719   , [LitTy (StrTyLit n),ty] <- tys
720   = maybeParen p FunPrec $
721     char '?' <> ftext n <> ptext (sLit "::") <> ppr_type TopPrec ty
722
723   | tc `hasKey` consDataConKey
724   , [_kind,ty1,ty2] <- tys
725   = sdocWithDynFlags $ \dflags ->
726     if gopt Opt_PrintExplicitKinds dflags then pprTcApp  p ppr_type tc tys
727                                    else pprTyList p ty1 ty2
728
729   | otherwise
730   = pprTcApp p ppr_type tc tys
731
732 pprTcApp :: TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> SDoc
733 -- Used for both types and coercions, hence polymorphism
734 pprTcApp _ pp tc [ty]
735   | tc `hasKey` listTyConKey = pprPromotionQuote tc <> brackets   (pp TopPrec ty)
736   | tc `hasKey` parrTyConKey = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
737
738 pprTcApp p pp tc tys
739   | isTupleTyCon tc && tyConArity tc == length tys
740   = pprPromotionQuote tc <>
741     tupleParens (tupleTyConSort tc) (sep (punctuate comma (map (pp TopPrec) tys)))
742
743   | Just dc <- isPromotedDataCon_maybe tc
744   , let dc_tc = dataConTyCon dc
745   , isTupleTyCon dc_tc
746   , let arity = tyConArity dc_tc    -- E.g. 3 for (,,) k1 k2 k3 t1 t2 t3
747         ty_args = drop arity tys    -- Drop the kind args
748   , ty_args `lengthIs` arity        -- Result is saturated
749   = pprPromotionQuote tc <>
750     (tupleParens (tupleTyConSort dc_tc) $
751      sep (punctuate comma (map (pp TopPrec) ty_args)))
752
753   | otherwise
754   = sdocWithDynFlags (pprTcApp_help p pp tc tys)
755
756 pprTcApp_help :: TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> DynFlags -> SDoc
757 -- This one has accss to the DynFlags
758 pprTcApp_help p pp tc tys dflags
759   | not (isSymOcc (nameOccName (tyConName tc)))
760   = pprPrefixApp p (ppr tc) (map (pp TyConPrec) tys_wo_kinds)
761
762   | [ty1,ty2] <- tys_wo_kinds  -- Infix, two arguments;
763                                -- we know nothing of precedence though
764   = pprInfixApp p pp (ppr tc) ty1 ty2
765
766   |  tc `hasKey` liftedTypeKindTyConKey
767   || tc `hasKey` unliftedTypeKindTyConKey
768   = ASSERT( null tys ) ppr tc   -- Do not wrap *, # in parens
769
770   | otherwise
771   = pprPrefixApp p (parens (ppr tc)) (map (pp TyConPrec) tys_wo_kinds)
772   where
773     tys_wo_kinds = suppressKinds dflags (tyConKind tc) tys
774
775 ------------------
776 suppressKinds :: DynFlags -> Kind -> [a] -> [a]
777 -- Given the kind of a TyCon, and the args to which it is applied,
778 -- suppress the args that are kind args
779 -- C.f. Note [Suppressing kinds] in IfaceType
780 suppressKinds dflags kind xs
781   | gopt Opt_PrintExplicitKinds dflags = xs
782   | otherwise                          = suppress kind xs
783   where
784     suppress (ForAllTy _ kind) (_ : xs) = suppress kind xs
785     suppress (FunTy _ res)     (x:xs)   = x : suppress res xs
786     suppress _                 xs       = xs
787
788 ----------------
789 pprTyList :: TyPrec -> Type -> Type -> SDoc
790 -- Given a type-level list (t1 ': t2), see if we can print
791 -- it in list notation [t1, ...].
792 pprTyList p ty1 ty2
793   = case gather ty2 of
794       (arg_tys, Nothing) -> char '\'' <> brackets (fsep (punctuate comma
795                                             (map (ppr_type TopPrec) (ty1:arg_tys))))
796       (arg_tys, Just tl) -> maybeParen p FunPrec $
797                             hang (ppr_type FunPrec ty1)
798                                2 (fsep [ colon <+> ppr_type FunPrec ty | ty <- arg_tys ++ [tl]])
799   where
800     gather :: Type -> ([Type], Maybe Type)
801      -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
802      --             = (tys, Just tl) means ty is of form t1:t2:...tn:tl
803     gather (TyConApp tc tys)
804       | tc `hasKey` consDataConKey
805       , [_kind, ty1,ty2] <- tys
806       , (args, tl) <- gather ty2
807       = (ty1:args, tl)
808       | tc `hasKey` nilDataConKey
809       = ([], Nothing)
810     gather ty = ([], Just ty)
811
812 ----------------
813 pprInfixApp :: TyPrec -> (TyPrec -> a -> SDoc) -> SDoc -> a -> a -> SDoc
814 pprInfixApp p pp pp_tc ty1 ty2
815   = maybeParen p TyOpPrec $
816     sep [pp TyOpPrec ty1, pprInfixVar True pp_tc <+> pp TyOpPrec ty2]
817
818 pprPrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
819 pprPrefixApp p pp_fun pp_tys
820   | null pp_tys = pp_fun
821   | otherwise   = maybeParen p TyConPrec $
822                   hang pp_fun 2 (sep pp_tys)
823
824 ----------------
825 pprArrowChain :: TyPrec -> [SDoc] -> SDoc
826 -- pprArrowChain p [a,b,c]  generates   a -> b -> c
827 pprArrowChain _ []         = empty
828 pprArrowChain p (arg:args) = maybeParen p FunPrec $
829                              sep [arg, sep (map (arrow <+>) args)]
830 \end{code}
831
832 %************************************************************************
833 %*                                                                      *
834 \subsection{TidyType}
835 %*                                                                      *
836 %************************************************************************
837
838 Tidying is here because it has a special case for FlatSkol
839
840 \begin{code}
841 -- | This tidies up a type for printing in an error message, or in
842 -- an interface file.
843 --
844 -- It doesn't change the uniques at all, just the print names.
845 tidyTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
846 tidyTyVarBndrs env tvs = mapAccumL tidyTyVarBndr env tvs
847
848 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
849 tidyTyVarBndr tidy_env@(occ_env, subst) tyvar
850   = case tidyOccName occ_env occ1 of
851       (tidy', occ') -> ((tidy', subst'), tyvar')
852         where
853           subst' = extendVarEnv subst tyvar tyvar'
854           tyvar' = setTyVarKind (setTyVarName tyvar name') kind'
855           name'  = tidyNameOcc name occ'
856           kind'  = tidyKind tidy_env (tyVarKind tyvar)
857   where
858     name = tyVarName tyvar
859     occ  = getOccName name
860     -- System Names are for unification variables;
861     -- when we tidy them we give them a trailing "0" (or 1 etc)
862     -- so that they don't take precedence for the un-modified name
863     occ1 | isSystemName name = mkTyVarOcc (occNameString occ ++ "0")
864          | otherwise         = occ
865
866
867 ---------------
868 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
869 -- ^ Add the free 'TyVar's to the env in tidy form,
870 -- so that we can tidy the type they are free in
871 tidyFreeTyVars (full_occ_env, var_env) tyvars
872   = fst (tidyOpenTyVars (full_occ_env, var_env) (varSetElems tyvars))
873
874         ---------------
875 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
876 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
877
878 ---------------
879 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
880 -- ^ Treat a new 'TyVar' as a binder, and give it a fresh tidy name
881 -- using the environment if one has not already been allocated. See
882 -- also 'tidyTyVarBndr'
883 tidyOpenTyVar env@(_, subst) tyvar
884   = case lookupVarEnv subst tyvar of
885         Just tyvar' -> (env, tyvar')            -- Already substituted
886         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
887
888 ---------------
889 tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
890 tidyTyVarOcc (_, subst) tv
891   = case lookupVarEnv subst tv of
892         Nothing  -> tv
893         Just tv' -> tv'
894
895 ---------------
896 tidyTypes :: TidyEnv -> [Type] -> [Type]
897 tidyTypes env tys = map (tidyType env) tys
898
899 ---------------
900 tidyType :: TidyEnv -> Type -> Type
901 tidyType _   (LitTy n)            = LitTy n
902 tidyType env (TyVarTy tv)         = TyVarTy (tidyTyVarOcc env tv)
903 tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
904                                     in args `seqList` TyConApp tycon args
905 tidyType env (AppTy fun arg)      = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
906 tidyType env (FunTy fun arg)      = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
907 tidyType env (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
908                                   where
909                                     (envp, tvp) = tidyTyVarBndr env tv
910
911 ---------------
912 -- | Grabs the free type variables, tidies them
913 -- and then uses 'tidyType' to work over the type itself
914 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
915 tidyOpenType env ty
916   = (env', tidyType (trimmed_occ_env, var_env) ty)
917   where
918     (env'@(_, var_env), tvs') = tidyOpenTyVars env (varSetElems (tyVarsOfType ty))
919     trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
920       -- The idea here was that we restrict the new TidyEnv to the
921       -- _free_ vars of the type, so that we don't gratuitously rename
922       -- the _bound_ variables of the type.
923
924 ---------------
925 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
926 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
927
928 ---------------
929 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
930 tidyTopType :: Type -> Type
931 tidyTopType ty = tidyType emptyTidyEnv ty
932
933 ---------------
934 tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
935 tidyOpenKind = tidyOpenType
936
937 tidyKind :: TidyEnv -> Kind -> Kind
938 tidyKind = tidyType
939 \end{code}