Make equality constraints in kinds invisible
[ghc.git] / compiler / iface / IfaceType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
4
5
6 This module defines interface types and binders
7 -}
8
9 {-# LANGUAGE CPP, FlexibleInstances, BangPatterns #-}
10 {-# LANGUAGE MultiWayIf #-}
11 {-# LANGUAGE TupleSections #-}
12 -- FlexibleInstances for Binary (DefMethSpec IfaceType)
13
14 module IfaceType (
15 IfExtName, IfLclName,
16
17 IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..),
18 IfaceMCoercion(..),
19 IfaceUnivCoProv(..),
20 IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..),
21 IfaceTyLit(..), IfaceAppArgs(..),
22 IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
23 IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
24 IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..),
25 ForallVisFlag(..), ShowForAllFlag(..),
26 mkIfaceForAllTvBndr,
27
28 ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
29 ifTyConBinderVar, ifTyConBinderName,
30
31 -- Equality testing
32 isIfaceLiftedTypeKind,
33
34 -- Conversion from IfaceAppArgs to IfaceTypes/ArgFlags
35 appArgsIfaceTypes, appArgsIfaceTypesArgFlags,
36
37 -- Printing
38 pprIfaceType, pprParendIfaceType, pprPrecIfaceType,
39 pprIfaceContext, pprIfaceContextArr,
40 pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
41 pprIfaceBndrs, pprIfaceAppArgs, pprParendIfaceAppArgs,
42 pprIfaceForAllPart, pprIfaceForAllPartMust, pprIfaceForAll,
43 pprIfaceSigmaType, pprIfaceTyLit,
44 pprIfaceCoercion, pprParendIfaceCoercion,
45 splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
46 pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
47
48 suppressIfaceInvisibles,
49 stripIfaceInvisVars,
50 stripInvisArgs,
51
52 mkIfaceTySubst, substIfaceTyVar, substIfaceAppArgs, inDomIfaceTySubst
53 ) where
54
55 #include "HsVersions.h"
56
57 import GhcPrelude
58
59 import {-# SOURCE #-} TysWiredIn ( coercibleTyCon, heqTyCon
60 , liftedRepDataConTyCon )
61 import {-# SOURCE #-} TyCoRep ( isRuntimeRepTy )
62
63 import DynFlags
64 import TyCon hiding ( pprPromotionQuote )
65 import CoAxiom
66 import Var
67 import PrelNames
68 import Name
69 import BasicTypes
70 import Binary
71 import Outputable
72 import FastString
73 import FastStringEnv
74 import Util
75
76 import Data.Maybe( isJust )
77 import qualified Data.Semigroup as Semi
78
79 {-
80 ************************************************************************
81 * *
82 Local (nested) binders
83 * *
84 ************************************************************************
85 -}
86
87 type IfLclName = FastString -- A local name in iface syntax
88
89 type IfExtName = Name -- An External or WiredIn Name can appear in IfaceSyn
90 -- (However Internal or System Names never should)
91
92 data IfaceBndr -- Local (non-top-level) binders
93 = IfaceIdBndr {-# UNPACK #-} !IfaceIdBndr
94 | IfaceTvBndr {-# UNPACK #-} !IfaceTvBndr
95
96 type IfaceIdBndr = (IfLclName, IfaceType)
97 type IfaceTvBndr = (IfLclName, IfaceKind)
98
99 ifaceTvBndrName :: IfaceTvBndr -> IfLclName
100 ifaceTvBndrName (n,_) = n
101
102 ifaceIdBndrName :: IfaceIdBndr -> IfLclName
103 ifaceIdBndrName (n,_) = n
104
105 ifaceBndrName :: IfaceBndr -> IfLclName
106 ifaceBndrName (IfaceTvBndr bndr) = ifaceTvBndrName bndr
107 ifaceBndrName (IfaceIdBndr bndr) = ifaceIdBndrName bndr
108
109 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
110
111 data IfaceOneShot -- See Note [Preserve OneShotInfo] in CoreTicy
112 = IfaceNoOneShot -- and Note [The oneShot function] in MkId
113 | IfaceOneShot
114
115
116 {-
117 %************************************************************************
118 %* *
119 IfaceType
120 %* *
121 %************************************************************************
122 -}
123
124 -------------------------------
125 type IfaceKind = IfaceType
126
127 -- | A kind of universal type, used for types and kinds.
128 --
129 -- Any time a 'Type' is pretty-printed, it is first converted to an 'IfaceType'
130 -- before being printed. See Note [Pretty printing via IfaceSyn] in PprTyThing
131 data IfaceType
132 = IfaceFreeTyVar TyVar -- See Note [Free tyvars in IfaceType]
133 | IfaceTyVar IfLclName -- Type/coercion variable only, not tycon
134 | IfaceLitTy IfaceTyLit
135 | IfaceAppTy IfaceType IfaceAppArgs
136 -- See Note [Suppressing invisible arguments] for
137 -- an explanation of why the second field isn't
138 -- IfaceType, analogous to AppTy.
139 | IfaceFunTy AnonArgFlag IfaceType IfaceType
140 | IfaceForAllTy IfaceForAllBndr IfaceType
141 | IfaceTyConApp IfaceTyCon IfaceAppArgs -- Not necessarily saturated
142 -- Includes newtypes, synonyms, tuples
143 | IfaceCastTy IfaceType IfaceCoercion
144 | IfaceCoercionTy IfaceCoercion
145
146 | IfaceTupleTy -- Saturated tuples (unsaturated ones use IfaceTyConApp)
147 TupleSort -- What sort of tuple?
148 PromotionFlag -- A bit like IfaceTyCon
149 IfaceAppArgs -- arity = length args
150 -- For promoted data cons, the kind args are omitted
151
152 type IfacePredType = IfaceType
153 type IfaceContext = [IfacePredType]
154
155 data IfaceTyLit
156 = IfaceNumTyLit Integer
157 | IfaceStrTyLit FastString
158 deriving (Eq)
159
160 type IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
161 type IfaceForAllBndr = VarBndr IfaceBndr ArgFlag
162
163 -- | Make an 'IfaceForAllBndr' from an 'IfaceTvBndr'.
164 mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr
165 mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis
166
167 -- | Stores the arguments in a type application as a list.
168 -- See @Note [Suppressing invisible arguments]@.
169 data IfaceAppArgs
170 = IA_Nil
171 | IA_Arg IfaceType -- The type argument
172
173 ArgFlag -- The argument's visibility. We store this here so
174 -- that we can:
175 --
176 -- 1. Avoid pretty-printing invisible (i.e., specified
177 -- or inferred) arguments when
178 -- -fprint-explicit-kinds isn't enabled, or
179 -- 2. When -fprint-explicit-kinds *is*, enabled, print
180 -- specified arguments in @(...) and inferred
181 -- arguments in @{...}.
182
183 IfaceAppArgs -- The rest of the arguments
184
185 instance Semi.Semigroup IfaceAppArgs where
186 IA_Nil <> xs = xs
187 IA_Arg ty argf rest <> xs = IA_Arg ty argf (rest Semi.<> xs)
188
189 instance Monoid IfaceAppArgs where
190 mempty = IA_Nil
191 mappend = (Semi.<>)
192
193 -- Encodes type constructors, kind constructors,
194 -- coercion constructors, the lot.
195 -- We have to tag them in order to pretty print them
196 -- properly.
197 data IfaceTyCon = IfaceTyCon { ifaceTyConName :: IfExtName
198 , ifaceTyConInfo :: IfaceTyConInfo }
199 deriving (Eq)
200
201 -- | The various types of TyCons which have special, built-in syntax.
202 data IfaceTyConSort = IfaceNormalTyCon -- ^ a regular tycon
203
204 | IfaceTupleTyCon !Arity !TupleSort
205 -- ^ e.g. @(a, b, c)@ or @(#a, b, c#)@.
206 -- The arity is the tuple width, not the tycon arity
207 -- (which is twice the width in the case of unboxed
208 -- tuples).
209
210 | IfaceSumTyCon !Arity
211 -- ^ e.g. @(a | b | c)@
212
213 | IfaceEqualityTyCon
214 -- ^ A heterogeneous equality TyCon
215 -- (i.e. eqPrimTyCon, eqReprPrimTyCon, heqTyCon)
216 -- that is actually being applied to two types
217 -- of the same kind. This affects pretty-printing
218 -- only: see Note [Equality predicates in IfaceType]
219 deriving (Eq)
220
221 {- Note [Free tyvars in IfaceType]
222 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
223 Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
224 an IfaceType and pretty printing that. This eliminates a lot of
225 pretty-print duplication, and it matches what we do with pretty-
226 printing TyThings. See Note [Pretty printing via IfaceSyn] in PprTyThing.
227
228 It works fine for closed types, but when printing debug traces (e.g.
229 when using -ddump-tc-trace) we print a lot of /open/ types. These
230 types are full of TcTyVars, and it's absolutely crucial to print them
231 in their full glory, with their unique, TcTyVarDetails etc.
232
233 So we simply embed a TyVar in IfaceType with the IfaceFreeTyVar constructor.
234 Note that:
235
236 * We never expect to serialise an IfaceFreeTyVar into an interface file, nor
237 to deserialise one. IfaceFreeTyVar is used only in the "convert to IfaceType
238 and then pretty-print" pipeline.
239
240 We do the same for covars, naturally.
241
242 Note [Equality predicates in IfaceType]
243 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
244 GHC has several varieties of type equality (see Note [The equality types story]
245 in TysPrim for details). In an effort to avoid confusing users, we suppress
246 the differences during pretty printing unless certain flags are enabled.
247 Here is how each equality predicate* is printed in homogeneous and
248 heterogeneous contexts, depending on which combination of the
249 -fprint-explicit-kinds and -fprint-equality-relations flags is used:
250
251 --------------------------------------------------------------------------------------------
252 | Predicate | Neither flag | -fprint-explicit-kinds |
253 |-------------------------------|----------------------------|-----------------------------|
254 | a ~ b (homogeneous) | a ~ b | (a :: Type) ~ (b :: Type) |
255 | a ~~ b, homogeneously | a ~ b | (a :: Type) ~ (b :: Type) |
256 | a ~~ b, heterogeneously | a ~~ c | (a :: Type) ~~ (c :: k) |
257 | a ~# b, homogeneously | a ~ b | (a :: Type) ~ (b :: Type) |
258 | a ~# b, heterogeneously | a ~~ c | (a :: Type) ~~ (c :: k) |
259 | Coercible a b (homogeneous) | Coercible a b | Coercible @Type a b |
260 | a ~R# b, homogeneously | Coercible a b | Coercible @Type a b |
261 | a ~R# b, heterogeneously | a ~R# b | (a :: Type) ~R# (c :: k) |
262 |-------------------------------|----------------------------|-----------------------------|
263 | Predicate | -fprint-equality-relations | Both flags |
264 |-------------------------------|----------------------------|-----------------------------|
265 | a ~ b (homogeneous) | a ~ b | (a :: Type) ~ (b :: Type) |
266 | a ~~ b, homogeneously | a ~~ b | (a :: Type) ~~ (b :: Type) |
267 | a ~~ b, heterogeneously | a ~~ c | (a :: Type) ~~ (c :: k) |
268 | a ~# b, homogeneously | a ~# b | (a :: Type) ~# (b :: Type) |
269 | a ~# b, heterogeneously | a ~# c | (a :: Type) ~# (c :: k) |
270 | Coercible a b (homogeneous) | Coercible a b | Coercible @Type a b |
271 | a ~R# b, homogeneously | a ~R# b | (a :: Type) ~R# (b :: Type) |
272 | a ~R# b, heterogeneously | a ~R# b | (a :: Type) ~R# (c :: k) |
273 --------------------------------------------------------------------------------------------
274
275 (* There is no heterogeneous, representational, lifted equality counterpart
276 to (~~). There could be, but there seems to be no use for it.)
277
278 This table adheres to the following rules:
279
280 A. With -fprint-equality-relations, print the true equality relation.
281 B. Without -fprint-equality-relations:
282 i. If the equality is representational and homogeneous, use Coercible.
283 ii. Otherwise, if the equality is representational, use ~R#.
284 iii. If the equality is nominal and homogeneous, use ~.
285 iv. Otherwise, if the equality is nominal, use ~~.
286 C. With -fprint-explicit-kinds, print kinds on both sides of an infix operator,
287 as above; or print the kind with Coercible.
288 D. Without -fprint-explicit-kinds, don't print kinds.
289
290 A hetero-kinded equality is used homogeneously when it is applied to two
291 identical kinds. Unfortunately, determining this from an IfaceType isn't
292 possible since we can't see through type synonyms. Consequently, we need to
293 record whether this particular application is homogeneous in IfaceTyConSort
294 for the purposes of pretty-printing.
295
296 See Note [The equality types story] in TysPrim.
297 -}
298
299 data IfaceTyConInfo -- Used to guide pretty-printing
300 -- and to disambiguate D from 'D (they share a name)
301 = IfaceTyConInfo { ifaceTyConIsPromoted :: PromotionFlag
302 , ifaceTyConSort :: IfaceTyConSort }
303 deriving (Eq)
304
305 data IfaceMCoercion
306 = IfaceMRefl
307 | IfaceMCo IfaceCoercion
308
309 data IfaceCoercion
310 = IfaceReflCo IfaceType
311 | IfaceGReflCo Role IfaceType (IfaceMCoercion)
312 | IfaceFunCo Role IfaceCoercion IfaceCoercion
313 | IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
314 | IfaceAppCo IfaceCoercion IfaceCoercion
315 | IfaceForAllCo IfaceBndr IfaceCoercion IfaceCoercion
316 | IfaceCoVarCo IfLclName
317 | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
318 | IfaceAxiomRuleCo IfLclName [IfaceCoercion]
319 -- There are only a fixed number of CoAxiomRules, so it suffices
320 -- to use an IfaceLclName to distinguish them.
321 -- See Note [Adding built-in type families] in TcTypeNats
322 | IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
323 | IfaceSymCo IfaceCoercion
324 | IfaceTransCo IfaceCoercion IfaceCoercion
325 | IfaceNthCo Int IfaceCoercion
326 | IfaceLRCo LeftOrRight IfaceCoercion
327 | IfaceInstCo IfaceCoercion IfaceCoercion
328 | IfaceKindCo IfaceCoercion
329 | IfaceSubCo IfaceCoercion
330 | IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
331 | IfaceHoleCo CoVar -- ^ See Note [Holes in IfaceCoercion]
332
333 data IfaceUnivCoProv
334 = IfaceUnsafeCoerceProv
335 | IfacePhantomProv IfaceCoercion
336 | IfaceProofIrrelProv IfaceCoercion
337 | IfacePluginProv String
338
339 {- Note [Holes in IfaceCoercion]
340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
341 When typechecking fails the typechecker will produce a HoleCo to stand
342 in place of the unproven assertion. While we generally don't want to
343 let these unproven assertions leak into interface files, we still need
344 to be able to pretty-print them as we use IfaceType's pretty-printer
345 to render Types. For this reason IfaceCoercion has a IfaceHoleCo
346 constructor; however, we fails when asked to serialize to a
347 IfaceHoleCo to ensure that they don't end up in an interface file.
348
349
350 %************************************************************************
351 %* *
352 Functions over IFaceTypes
353 * *
354 ************************************************************************
355 -}
356
357 ifaceTyConHasKey :: IfaceTyCon -> Unique -> Bool
358 ifaceTyConHasKey tc key = ifaceTyConName tc `hasKey` key
359
360 isIfaceLiftedTypeKind :: IfaceKind -> Bool
361 isIfaceLiftedTypeKind (IfaceTyConApp tc IA_Nil)
362 = isLiftedTypeKindTyConName (ifaceTyConName tc)
363 isIfaceLiftedTypeKind (IfaceTyConApp tc
364 (IA_Arg (IfaceTyConApp ptr_rep_lifted IA_Nil)
365 Required IA_Nil))
366 = tc `ifaceTyConHasKey` tYPETyConKey
367 && ptr_rep_lifted `ifaceTyConHasKey` liftedRepDataConKey
368 isIfaceLiftedTypeKind _ = False
369
370 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
371 -- Mainly for printing purposes
372 --
373 -- Here we split nested IfaceSigmaTy properly.
374 --
375 -- @
376 -- forall t. T t => forall m a b. M m => (a -> m b) -> t a -> m (t b)
377 -- @
378 --
379 -- If you called @splitIfaceSigmaTy@ on this type:
380 --
381 -- @
382 -- ([t, m, a, b], [T t, M m], (a -> m b) -> t a -> m (t b))
383 -- @
384 splitIfaceSigmaTy ty
385 = case (bndrs, theta) of
386 ([], []) -> (bndrs, theta, tau)
387 _ -> let (bndrs', theta', tau') = splitIfaceSigmaTy tau
388 in (bndrs ++ bndrs', theta ++ theta', tau')
389 where
390 (bndrs, rho) = split_foralls ty
391 (theta, tau) = split_rho rho
392
393 split_foralls (IfaceForAllTy bndr ty)
394 = case split_foralls ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
395 split_foralls rho = ([], rho)
396
397 split_rho (IfaceFunTy InvisArg ty1 ty2)
398 = case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
399 split_rho tau = ([], tau)
400
401 suppressIfaceInvisibles :: DynFlags -> [IfaceTyConBinder] -> [a] -> [a]
402 suppressIfaceInvisibles dflags tys xs
403 | gopt Opt_PrintExplicitKinds dflags = xs
404 | otherwise = suppress tys xs
405 where
406 suppress _ [] = []
407 suppress [] a = a
408 suppress (k:ks) (x:xs)
409 | isInvisibleTyConBinder k = suppress ks xs
410 | otherwise = x : suppress ks xs
411
412 stripIfaceInvisVars :: DynFlags -> [IfaceTyConBinder] -> [IfaceTyConBinder]
413 stripIfaceInvisVars dflags tyvars
414 | gopt Opt_PrintExplicitKinds dflags = tyvars
415 | otherwise = filterOut isInvisibleTyConBinder tyvars
416
417 -- | Extract an 'IfaceBndr' from an 'IfaceForAllBndr'.
418 ifForAllBndrVar :: IfaceForAllBndr -> IfaceBndr
419 ifForAllBndrVar = binderVar
420
421 -- | Extract the variable name from an 'IfaceForAllBndr'.
422 ifForAllBndrName :: IfaceForAllBndr -> IfLclName
423 ifForAllBndrName fab = ifaceBndrName (ifForAllBndrVar fab)
424
425 -- | Extract an 'IfaceBndr' from an 'IfaceTyConBinder'.
426 ifTyConBinderVar :: IfaceTyConBinder -> IfaceBndr
427 ifTyConBinderVar = binderVar
428
429 -- | Extract the variable name from an 'IfaceTyConBinder'.
430 ifTyConBinderName :: IfaceTyConBinder -> IfLclName
431 ifTyConBinderName tcb = ifaceBndrName (ifTyConBinderVar tcb)
432
433 ifTypeIsVarFree :: IfaceType -> Bool
434 -- Returns True if the type definitely has no variables at all
435 -- Just used to control pretty printing
436 ifTypeIsVarFree ty = go ty
437 where
438 go (IfaceTyVar {}) = False
439 go (IfaceFreeTyVar {}) = False
440 go (IfaceAppTy fun args) = go fun && go_args args
441 go (IfaceFunTy _ arg res) = go arg && go res
442 go (IfaceForAllTy {}) = False
443 go (IfaceTyConApp _ args) = go_args args
444 go (IfaceTupleTy _ _ args) = go_args args
445 go (IfaceLitTy _) = True
446 go (IfaceCastTy {}) = False -- Safe
447 go (IfaceCoercionTy {}) = False -- Safe
448
449 go_args IA_Nil = True
450 go_args (IA_Arg arg _ args) = go arg && go_args args
451
452 {- Note [Substitution on IfaceType]
453 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
454 Substitutions on IfaceType are done only during pretty-printing to
455 construct the result type of a GADT, and does not deal with binders
456 (eg IfaceForAll), so it doesn't need fancy capture stuff. -}
457
458 type IfaceTySubst = FastStringEnv IfaceType -- Note [Substitution on IfaceType]
459
460 mkIfaceTySubst :: [(IfLclName,IfaceType)] -> IfaceTySubst
461 -- See Note [Substitution on IfaceType]
462 mkIfaceTySubst eq_spec = mkFsEnv eq_spec
463
464 inDomIfaceTySubst :: IfaceTySubst -> IfaceTvBndr -> Bool
465 -- See Note [Substitution on IfaceType]
466 inDomIfaceTySubst subst (fs, _) = isJust (lookupFsEnv subst fs)
467
468 substIfaceType :: IfaceTySubst -> IfaceType -> IfaceType
469 -- See Note [Substitution on IfaceType]
470 substIfaceType env ty
471 = go ty
472 where
473 go (IfaceFreeTyVar tv) = IfaceFreeTyVar tv
474 go (IfaceTyVar tv) = substIfaceTyVar env tv
475 go (IfaceAppTy t ts) = IfaceAppTy (go t) (substIfaceAppArgs env ts)
476 go (IfaceFunTy af t1 t2) = IfaceFunTy af (go t1) (go t2)
477 go ty@(IfaceLitTy {}) = ty
478 go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceAppArgs env tys)
479 go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceAppArgs env tys)
480 go (IfaceForAllTy {}) = pprPanic "substIfaceType" (ppr ty)
481 go (IfaceCastTy ty co) = IfaceCastTy (go ty) (go_co co)
482 go (IfaceCoercionTy co) = IfaceCoercionTy (go_co co)
483
484 go_mco IfaceMRefl = IfaceMRefl
485 go_mco (IfaceMCo co) = IfaceMCo $ go_co co
486
487 go_co (IfaceReflCo ty) = IfaceReflCo (go ty)
488 go_co (IfaceGReflCo r ty mco) = IfaceGReflCo r (go ty) (go_mco mco)
489 go_co (IfaceFunCo r c1 c2) = IfaceFunCo r (go_co c1) (go_co c2)
490 go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos)
491 go_co (IfaceAppCo c1 c2) = IfaceAppCo (go_co c1) (go_co c2)
492 go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty)
493 go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar cv
494 go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv
495 go_co (IfaceHoleCo cv) = IfaceHoleCo cv
496 go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
497 go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
498 go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
499 go_co (IfaceTransCo co1 co2) = IfaceTransCo (go_co co1) (go_co co2)
500 go_co (IfaceNthCo n co) = IfaceNthCo n (go_co co)
501 go_co (IfaceLRCo lr co) = IfaceLRCo lr (go_co co)
502 go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2)
503 go_co (IfaceKindCo co) = IfaceKindCo (go_co co)
504 go_co (IfaceSubCo co) = IfaceSubCo (go_co co)
505 go_co (IfaceAxiomRuleCo n cos) = IfaceAxiomRuleCo n (go_cos cos)
506
507 go_cos = map go_co
508
509 go_prov IfaceUnsafeCoerceProv = IfaceUnsafeCoerceProv
510 go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co)
511 go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
512 go_prov (IfacePluginProv str) = IfacePluginProv str
513
514 substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
515 substIfaceAppArgs env args
516 = go args
517 where
518 go IA_Nil = IA_Nil
519 go (IA_Arg ty arg tys) = IA_Arg (substIfaceType env ty) arg (go tys)
520
521 substIfaceTyVar :: IfaceTySubst -> IfLclName -> IfaceType
522 substIfaceTyVar env tv
523 | Just ty <- lookupFsEnv env tv = ty
524 | otherwise = IfaceTyVar tv
525
526
527 {-
528 ************************************************************************
529 * *
530 Functions over IfaceAppArgs
531 * *
532 ************************************************************************
533 -}
534
535 stripInvisArgs :: DynFlags -> IfaceAppArgs -> IfaceAppArgs
536 stripInvisArgs dflags tys
537 | gopt Opt_PrintExplicitKinds dflags = tys
538 | otherwise = suppress_invis tys
539 where
540 suppress_invis c
541 = case c of
542 IA_Nil -> IA_Nil
543 IA_Arg t argf ts
544 | isVisibleArgFlag argf
545 -> IA_Arg t argf $ suppress_invis ts
546 -- Keep recursing through the remainder of the arguments, as it's
547 -- possible that there are remaining invisible ones.
548 -- See the "In type declarations" section of Note [VarBndrs,
549 -- TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
550 | otherwise
551 -> suppress_invis ts
552
553 appArgsIfaceTypes :: IfaceAppArgs -> [IfaceType]
554 appArgsIfaceTypes IA_Nil = []
555 appArgsIfaceTypes (IA_Arg t _ ts) = t : appArgsIfaceTypes ts
556
557 appArgsIfaceTypesArgFlags :: IfaceAppArgs -> [(IfaceType, ArgFlag)]
558 appArgsIfaceTypesArgFlags IA_Nil = []
559 appArgsIfaceTypesArgFlags (IA_Arg t a ts)
560 = (t, a) : appArgsIfaceTypesArgFlags ts
561
562 ifaceVisAppArgsLength :: IfaceAppArgs -> Int
563 ifaceVisAppArgsLength = go 0
564 where
565 go !n IA_Nil = n
566 go n (IA_Arg _ argf rest)
567 | isVisibleArgFlag argf = go (n+1) rest
568 | otherwise = go n rest
569
570 {-
571 Note [Suppressing invisible arguments]
572 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
573 We use the IfaceAppArgs data type to specify which of the arguments to a type
574 should be displayed when pretty-printing, under the control of
575 -fprint-explicit-kinds.
576 See also Type.filterOutInvisibleTypes.
577 For example, given
578
579 T :: forall k. (k->*) -> k -> * -- Ordinary kind polymorphism
580 'Just :: forall k. k -> 'Maybe k -- Promoted
581
582 we want
583
584 T * Tree Int prints as T Tree Int
585 'Just * prints as Just *
586
587 For type constructors (IfaceTyConApp), IfaceAppArgs is a quite natural fit,
588 since the corresponding Core constructor:
589
590 data Type
591 = ...
592 | TyConApp TyCon [Type]
593
594 Already puts all of its arguments into a list. So when converting a Type to an
595 IfaceType (see toIfaceAppArgsX in ToIface), we simply use the kind of the TyCon
596 (which is cached) to guide the process of converting the argument Types into an
597 IfaceAppArgs list.
598
599 We also want this behavior for IfaceAppTy, since given:
600
601 data Proxy (a :: k)
602 f :: forall (t :: forall a. a -> Type). Proxy Type (t Bool True)
603
604 We want to print the return type as `Proxy (t True)` without the use of
605 -fprint-explicit-kinds (#15330). Accomplishing this is trickier than in the
606 tycon case, because the corresponding Core constructor for IfaceAppTy:
607
608 data Type
609 = ...
610 | AppTy Type Type
611
612 Only stores one argument at a time. Therefore, when converting an AppTy to an
613 IfaceAppTy (in toIfaceTypeX in ToIface), we:
614
615 1. Flatten the chain of AppTys down as much as possible
616 2. Use typeKind to determine the function Type's kind
617 3. Use this kind to guide the process of converting the argument Types into an
618 IfaceAppArgs list.
619
620 By flattening the arguments like this, we obtain two benefits:
621
622 (a) We can reuse the same machinery to pretty-print IfaceTyConApp arguments as
623 we do IfaceTyApp arguments, which means that we only need to implement the
624 logic to filter out invisible arguments once.
625 (b) Unlike for tycons, finding the kind of a type in general (through typeKind)
626 is not a constant-time operation, so by flattening the arguments first, we
627 decrease the number of times we have to call typeKind.
628
629 Note [Pretty-printing invisible arguments]
630 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
631 Note [Suppressing invisible arguments] is all about how to avoid printing
632 invisible arguments when the -fprint-explicit-kinds flag is disables. Well,
633 what about when it's enabled? Then we can and should print invisible kind
634 arguments, and this Note explains how we do it.
635
636 As two running examples, consider the following code:
637
638 {-# LANGUAGE PolyKinds #-}
639 data T1 a
640 data T2 (a :: k)
641
642 When displaying these types (with -fprint-explicit-kinds on), we could just
643 do the following:
644
645 T1 k a
646 T2 k a
647
648 That certainly gets the job done. But it lacks a crucial piece of information:
649 is the `k` argument inferred or specified? To communicate this, we use visible
650 kind application syntax to distinguish the two cases:
651
652 T1 @{k} a
653 T2 @k a
654
655 Here, @{k} indicates that `k` is an inferred argument, and @k indicates that
656 `k` is a specified argument. (See
657 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep for
658 a lengthier explanation on what "inferred" and "specified" mean.)
659
660 ************************************************************************
661 * *
662 Pretty-printing
663 * *
664 ************************************************************************
665 -}
666
667 if_print_coercions :: SDoc -- ^ if printing coercions
668 -> SDoc -- ^ otherwise
669 -> SDoc
670 if_print_coercions yes no
671 = sdocWithDynFlags $ \dflags ->
672 getPprStyle $ \style ->
673 if gopt Opt_PrintExplicitCoercions dflags
674 || dumpStyle style || debugStyle style
675 then yes
676 else no
677
678 pprIfaceInfixApp :: PprPrec -> SDoc -> SDoc -> SDoc -> SDoc
679 pprIfaceInfixApp ctxt_prec pp_tc pp_ty1 pp_ty2
680 = maybeParen ctxt_prec opPrec $
681 sep [pp_ty1, pp_tc <+> pp_ty2]
682
683 pprIfacePrefixApp :: PprPrec -> SDoc -> [SDoc] -> SDoc
684 pprIfacePrefixApp ctxt_prec pp_fun pp_tys
685 | null pp_tys = pp_fun
686 | otherwise = maybeParen ctxt_prec appPrec $
687 hang pp_fun 2 (sep pp_tys)
688
689 -- ----------------------------- Printing binders ------------------------------------
690
691 instance Outputable IfaceBndr where
692 ppr (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
693 ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr False bndr
694
695 pprIfaceBndrs :: [IfaceBndr] -> SDoc
696 pprIfaceBndrs bs = sep (map ppr bs)
697
698 pprIfaceLamBndr :: IfaceLamBndr -> SDoc
699 pprIfaceLamBndr (b, IfaceNoOneShot) = ppr b
700 pprIfaceLamBndr (b, IfaceOneShot) = ppr b <> text "[OneShot]"
701
702 pprIfaceIdBndr :: IfaceIdBndr -> SDoc
703 pprIfaceIdBndr (name, ty) = parens (ppr name <+> dcolon <+> ppr ty)
704
705 pprIfaceTvBndr :: Bool -> IfaceTvBndr -> SDoc
706 pprIfaceTvBndr use_parens (tv, ki)
707 | isIfaceLiftedTypeKind ki = ppr tv
708 | otherwise = maybe_parens (ppr tv <+> dcolon <+> ppr ki)
709 where
710 maybe_parens | use_parens = parens
711 | otherwise = id
712
713 pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
714 pprIfaceTyConBinders = sep . map go
715 where
716 go :: IfaceTyConBinder -> SDoc
717 go (Bndr (IfaceIdBndr bndr) _) = pprIfaceIdBndr bndr
718 go (Bndr (IfaceTvBndr bndr) vis) =
719 -- See Note [Pretty-printing invisible arguments]
720 case vis of
721 AnonTCB VisArg -> ppr_bndr True
722 AnonTCB InvisArg -> char '@' <> braces (ppr_bndr False)
723 -- The above case is rare. (See Note [AnonTCB InvisArg] in TyCon.)
724 -- Should we print these differently?
725 NamedTCB Required -> ppr_bndr True
726 NamedTCB Specified -> char '@' <> ppr_bndr True
727 NamedTCB Inferred -> char '@' <> braces (ppr_bndr False)
728 where
729 ppr_bndr use_parens = pprIfaceTvBndr use_parens bndr
730
731 instance Binary IfaceBndr where
732 put_ bh (IfaceIdBndr aa) = do
733 putByte bh 0
734 put_ bh aa
735 put_ bh (IfaceTvBndr ab) = do
736 putByte bh 1
737 put_ bh ab
738 get bh = do
739 h <- getByte bh
740 case h of
741 0 -> do aa <- get bh
742 return (IfaceIdBndr aa)
743 _ -> do ab <- get bh
744 return (IfaceTvBndr ab)
745
746 instance Binary IfaceOneShot where
747 put_ bh IfaceNoOneShot = do
748 putByte bh 0
749 put_ bh IfaceOneShot = do
750 putByte bh 1
751 get bh = do
752 h <- getByte bh
753 case h of
754 0 -> do return IfaceNoOneShot
755 _ -> do return IfaceOneShot
756
757 -- ----------------------------- Printing IfaceType ------------------------------------
758
759 ---------------------------------
760 instance Outputable IfaceType where
761 ppr ty = pprIfaceType ty
762
763 pprIfaceType, pprParendIfaceType :: IfaceType -> SDoc
764 pprIfaceType = pprPrecIfaceType topPrec
765 pprParendIfaceType = pprPrecIfaceType appPrec
766
767 pprPrecIfaceType :: PprPrec -> IfaceType -> SDoc
768 -- We still need `eliminateRuntimeRep`, since the `pprPrecIfaceType` maybe
769 -- called from other places, besides `:type` and `:info`.
770 pprPrecIfaceType prec ty = eliminateRuntimeRep (ppr_ty prec) ty
771
772 ppr_sigma :: PprPrec -> IfaceType -> SDoc
773 ppr_sigma ctxt_prec ty
774 = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
775
776 ppr_ty :: PprPrec -> IfaceType -> SDoc
777 ppr_ty ctxt_prec ty@(IfaceForAllTy {}) = ppr_sigma ctxt_prec ty
778 ppr_ty ctxt_prec ty@(IfaceFunTy InvisArg _ _) = ppr_sigma ctxt_prec ty
779
780 ppr_ty _ (IfaceFreeTyVar tyvar) = ppr tyvar -- This is the main reason for IfaceFreeTyVar!
781 ppr_ty _ (IfaceTyVar tyvar) = ppr tyvar -- See Note [TcTyVars in IfaceType]
782 ppr_ty ctxt_prec (IfaceTyConApp tc tys) = pprTyTcApp ctxt_prec tc tys
783 ppr_ty ctxt_prec (IfaceTupleTy i p tys) = pprTuple ctxt_prec i p tys
784 ppr_ty _ (IfaceLitTy n) = pprIfaceTyLit n
785 -- Function types
786 ppr_ty ctxt_prec (IfaceFunTy _ ty1 ty2) -- Should be VisArg
787 = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
788 maybeParen ctxt_prec funPrec $
789 sep [ppr_ty funPrec ty1, sep (ppr_fun_tail ty2)]
790 where
791 ppr_fun_tail (IfaceFunTy VisArg ty1 ty2)
792 = (arrow <+> ppr_ty funPrec ty1) : ppr_fun_tail ty2
793 ppr_fun_tail other_ty
794 = [arrow <+> pprIfaceType other_ty]
795
796 ppr_ty ctxt_prec (IfaceAppTy t ts)
797 = if_print_coercions
798 ppr_app_ty
799 ppr_app_ty_no_casts
800 where
801 ppr_app_ty =
802 sdocWithDynFlags $ \dflags ->
803 pprIfacePrefixApp ctxt_prec
804 (ppr_ty funPrec t)
805 (map (ppr_app_arg appPrec) (tys_wo_kinds dflags))
806
807 tys_wo_kinds dflags = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags ts
808
809 -- Strip any casts from the head of the application
810 ppr_app_ty_no_casts =
811 case t of
812 IfaceCastTy head _ -> ppr_ty ctxt_prec (mk_app_tys head ts)
813 _ -> ppr_app_ty
814
815 mk_app_tys :: IfaceType -> IfaceAppArgs -> IfaceType
816 mk_app_tys (IfaceTyConApp tc tys1) tys2 =
817 IfaceTyConApp tc (tys1 `mappend` tys2)
818 mk_app_tys t1 tys2 = IfaceAppTy t1 tys2
819
820 ppr_ty ctxt_prec (IfaceCastTy ty co)
821 = if_print_coercions
822 (parens (ppr_ty topPrec ty <+> text "|>" <+> ppr co))
823 (ppr_ty ctxt_prec ty)
824
825 ppr_ty ctxt_prec (IfaceCoercionTy co)
826 = if_print_coercions
827 (ppr_co ctxt_prec co)
828 (text "<>")
829
830 {- Note [Defaulting RuntimeRep variables]
831 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
832 RuntimeRep variables are considered by many (most?) users to be little
833 more than syntactic noise. When the notion was introduced there was a
834 signficant and understandable push-back from those with pedagogy in
835 mind, which argued that RuntimeRep variables would throw a wrench into
836 nearly any teach approach since they appear in even the lowly ($)
837 function's type,
838
839 ($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
840
841 which is significantly less readable than its non RuntimeRep-polymorphic type of
842
843 ($) :: (a -> b) -> a -> b
844
845 Moreover, unboxed types don't appear all that often in run-of-the-mill
846 Haskell programs, so it makes little sense to make all users pay this
847 syntactic overhead.
848
849 For this reason it was decided that we would hide RuntimeRep variables
850 for now (see #11549). We do this by defaulting all type variables of
851 kind RuntimeRep to LiftedRep. This is done in a pass right before
852 pretty-printing (defaultRuntimeRepVars, controlled by
853 -fprint-explicit-runtime-reps)
854
855 This applies to /quantified/ variables like 'w' above. What about
856 variables that are /free/ in the type being printed, which certainly
857 happens in error messages. Suppose (#16074) we are reporting a
858 mismatch between two skolems
859 (a :: RuntimeRep) ~ (b :: RuntimeRep)
860 We certainly don't want to say "Can't match LiftedRep ~ LiftedRep"!
861
862 But if we are printing the type
863 (forall (a :: Type r). blah
864 we do want to turn that (free) r into LiftedRep, so it prints as
865 (forall a. blah)
866
867 Conclusion: keep track of whether we we are in the kind of a
868 binder; ohly if so, convert free RuntimeRep variables to LiftedRep.
869 -}
870
871 -- | Default 'RuntimeRep' variables to 'LiftedPtr'. e.g.
872 --
873 -- @
874 -- ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
875 -- (a -> b) -> a -> b
876 -- @
877 --
878 -- turns in to,
879 --
880 -- @ ($) :: forall a (b :: *). (a -> b) -> a -> b @
881 --
882 -- We do this to prevent RuntimeRep variables from incurring a significant
883 -- syntactic overhead in otherwise simple type signatures (e.g. ($)). See
884 -- Note [Defaulting RuntimeRep variables] and #11549 for further discussion.
885 --
886 defaultRuntimeRepVars :: IfaceType -> IfaceType
887 defaultRuntimeRepVars ty = go False emptyFsEnv ty
888 where
889 go :: Bool -- True <=> Inside the kind of a binder
890 -> FastStringEnv () -- Set of enclosing forall-ed RuntimeRep variables
891 -> IfaceType -- (replace them with LiftedRep)
892 -> IfaceType
893 go ink subs (IfaceForAllTy (Bndr (IfaceTvBndr (var, var_kind)) argf) ty)
894 | isRuntimeRep var_kind
895 , isInvisibleArgFlag argf -- Don't default *visible* quantification
896 -- or we get the mess in #13963
897 = let subs' = extendFsEnv subs var ()
898 -- Record that we should replace it with LiftedRep,
899 -- and recurse, discarding the forall
900 in go ink subs' ty
901
902 go ink subs (IfaceForAllTy bndr ty)
903 = IfaceForAllTy (go_ifacebndr subs bndr) (go ink subs ty)
904
905 go _ subs ty@(IfaceTyVar tv)
906 | tv `elemFsEnv` subs
907 = IfaceTyConApp liftedRep IA_Nil
908 | otherwise
909 = ty
910
911 go in_kind _ ty@(IfaceFreeTyVar tv)
912 -- See Note [Defaulting RuntimeRep variables], about free vars
913 | in_kind && TyCoRep.isRuntimeRepTy (tyVarKind tv)
914 = IfaceTyConApp liftedRep IA_Nil
915 | otherwise
916 = ty
917
918 go ink subs (IfaceTyConApp tc tc_args)
919 = IfaceTyConApp tc (go_args ink subs tc_args)
920
921 go ink subs (IfaceTupleTy sort is_prom tc_args)
922 = IfaceTupleTy sort is_prom (go_args ink subs tc_args)
923
924 go ink subs (IfaceFunTy af arg res)
925 = IfaceFunTy af (go ink subs arg) (go ink subs res)
926
927 go ink subs (IfaceAppTy t ts)
928 = IfaceAppTy (go ink subs t) (go_args ink subs ts)
929
930 go ink subs (IfaceCastTy x co)
931 = IfaceCastTy (go ink subs x) co
932
933 go _ _ ty@(IfaceLitTy {}) = ty
934 go _ _ ty@(IfaceCoercionTy {}) = ty
935
936 go_ifacebndr :: FastStringEnv () -> IfaceForAllBndr -> IfaceForAllBndr
937 go_ifacebndr subs (Bndr (IfaceIdBndr (n, t)) argf)
938 = Bndr (IfaceIdBndr (n, go True subs t)) argf
939 go_ifacebndr subs (Bndr (IfaceTvBndr (n, t)) argf)
940 = Bndr (IfaceTvBndr (n, go True subs t)) argf
941
942 go_args :: Bool -> FastStringEnv () -> IfaceAppArgs -> IfaceAppArgs
943 go_args _ _ IA_Nil = IA_Nil
944 go_args ink subs (IA_Arg ty argf args)
945 = IA_Arg (go ink subs ty) argf (go_args ink subs args)
946
947 liftedRep :: IfaceTyCon
948 liftedRep = IfaceTyCon dc_name (IfaceTyConInfo IsPromoted IfaceNormalTyCon)
949 where dc_name = getName liftedRepDataConTyCon
950
951 isRuntimeRep :: IfaceType -> Bool
952 isRuntimeRep (IfaceTyConApp tc _) =
953 tc `ifaceTyConHasKey` runtimeRepTyConKey
954 isRuntimeRep _ = False
955
956 eliminateRuntimeRep :: (IfaceType -> SDoc) -> IfaceType -> SDoc
957 eliminateRuntimeRep f ty
958 = sdocWithDynFlags $ \dflags ->
959 getPprStyle $ \sty ->
960 if userStyle sty && not (gopt Opt_PrintExplicitRuntimeReps dflags)
961 then f (defaultRuntimeRepVars ty)
962 else f ty
963
964 instance Outputable IfaceAppArgs where
965 ppr tca = pprIfaceAppArgs tca
966
967 pprIfaceAppArgs, pprParendIfaceAppArgs :: IfaceAppArgs -> SDoc
968 pprIfaceAppArgs = ppr_app_args topPrec
969 pprParendIfaceAppArgs = ppr_app_args appPrec
970
971 ppr_app_args :: PprPrec -> IfaceAppArgs -> SDoc
972 ppr_app_args ctx_prec = go
973 where
974 go :: IfaceAppArgs -> SDoc
975 go IA_Nil = empty
976 go (IA_Arg t argf ts) = ppr_app_arg ctx_prec (t, argf) <+> go ts
977
978 -- See Note [Pretty-printing invisible arguments]
979 ppr_app_arg :: PprPrec -> (IfaceType, ArgFlag) -> SDoc
980 ppr_app_arg ctx_prec (t, argf) =
981 sdocWithDynFlags $ \dflags ->
982 let print_kinds = gopt Opt_PrintExplicitKinds dflags
983 in case argf of
984 Required -> ppr_ty ctx_prec t
985 Specified | print_kinds
986 -> char '@' <> ppr_ty appPrec t
987 Inferred | print_kinds
988 -> char '@' <> braces (ppr_ty topPrec t)
989 _ -> empty
990
991 -------------------
992 pprIfaceForAllPart :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
993 pprIfaceForAllPart tvs ctxt sdoc
994 = ppr_iface_forall_part ShowForAllWhen tvs ctxt sdoc
995
996 -- | Like 'pprIfaceForAllPart', but always uses an explicit @forall@.
997 pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
998 pprIfaceForAllPartMust tvs ctxt sdoc
999 = ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
1000
1001 pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
1002 pprIfaceForAllCoPart tvs sdoc
1003 = sep [ pprIfaceForAllCo tvs, sdoc ]
1004
1005 ppr_iface_forall_part :: ShowForAllFlag
1006 -> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
1007 ppr_iface_forall_part show_forall tvs ctxt sdoc
1008 = sep [ case show_forall of
1009 ShowForAllMust -> pprIfaceForAll tvs
1010 ShowForAllWhen -> pprUserIfaceForAll tvs
1011 , pprIfaceContextArr ctxt
1012 , sdoc]
1013
1014 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
1015 pprIfaceForAll :: [IfaceForAllBndr] -> SDoc
1016 pprIfaceForAll [] = empty
1017 pprIfaceForAll bndrs@(Bndr _ vis : _)
1018 = sep [ add_separator (forAllLit <+> fsep docs)
1019 , pprIfaceForAll bndrs' ]
1020 where
1021 (bndrs', docs) = ppr_itv_bndrs bndrs vis
1022
1023 add_separator stuff = case vis of
1024 Required -> stuff <+> arrow
1025 _inv -> stuff <> dot
1026
1027
1028 -- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
1029 -- Returns both the list of not-yet-rendered binders and the doc.
1030 -- No anonymous binders here!
1031 ppr_itv_bndrs :: [IfaceForAllBndr]
1032 -> ArgFlag -- ^ visibility of the first binder in the list
1033 -> ([IfaceForAllBndr], [SDoc])
1034 ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
1035 | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in
1036 (bndrs', pprIfaceForAllBndr bndr : doc)
1037 | otherwise = (all_bndrs, [])
1038 ppr_itv_bndrs [] _ = ([], [])
1039
1040 pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
1041 pprIfaceForAllCo [] = empty
1042 pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot
1043
1044 pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
1045 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
1046
1047 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
1048 pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) Inferred)
1049 = sdocWithDynFlags $ \dflags ->
1050 if gopt Opt_PrintExplicitForalls dflags
1051 then braces $ pprIfaceTvBndr False tv
1052 else pprIfaceTvBndr True tv
1053 pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) _) = pprIfaceTvBndr True tv
1054 pprIfaceForAllBndr (Bndr (IfaceIdBndr idv) _) = pprIfaceIdBndr idv
1055
1056 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
1057 pprIfaceForAllCoBndr (tv, kind_co)
1058 = parens (ppr tv <+> dcolon <+> pprIfaceCoercion kind_co)
1059
1060 -- | Show forall flag
1061 --
1062 -- Unconditionally show the forall quantifier with ('ShowForAllMust')
1063 -- or when ('ShowForAllWhen') the names used are free in the binder
1064 -- or when compiling with -fprint-explicit-foralls.
1065 data ShowForAllFlag = ShowForAllMust | ShowForAllWhen
1066
1067 pprIfaceSigmaType :: ShowForAllFlag -> IfaceType -> SDoc
1068 pprIfaceSigmaType show_forall ty
1069 = eliminateRuntimeRep ppr_fn ty
1070 where
1071 ppr_fn iface_ty =
1072 let (tvs, theta, tau) = splitIfaceSigmaTy iface_ty
1073 in ppr_iface_forall_part show_forall tvs theta (ppr tau)
1074
1075 pprUserIfaceForAll :: [IfaceForAllBndr] -> SDoc
1076 pprUserIfaceForAll tvs
1077 = sdocWithDynFlags $ \dflags ->
1078 -- See Note [When to print foralls]
1079 ppWhen (any tv_has_kind_var tvs
1080 || any tv_is_required tvs
1081 || gopt Opt_PrintExplicitForalls dflags) $
1082 pprIfaceForAll tvs
1083 where
1084 tv_has_kind_var (Bndr (IfaceTvBndr (_,kind)) _)
1085 = not (ifTypeIsVarFree kind)
1086 tv_has_kind_var _ = False
1087
1088 tv_is_required = isVisibleArgFlag . binderArgFlag
1089
1090 {-
1091 Note [When to print foralls]
1092 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1093 We opt to explicitly pretty-print `forall`s if any of the following
1094 criteria are met:
1095
1096 1. -fprint-explicit-foralls is on.
1097
1098 2. A bound type variable has a polymorphic kind. E.g.,
1099
1100 forall k (a::k). Proxy a -> Proxy a
1101
1102 Since a's kind mentions a variable k, we print the foralls.
1103
1104 3. A bound type variable is a visible argument (#14238).
1105 Suppose we are printing the kind of:
1106
1107 T :: forall k -> k -> Type
1108
1109 The "forall k ->" notation means that this kind argument is required.
1110 That is, it must be supplied at uses of T. E.g.,
1111
1112 f :: T (Type->Type) Monad -> Int
1113
1114 So we print an explicit "T :: forall k -> k -> Type",
1115 because omitting it and printing "T :: k -> Type" would be
1116 utterly misleading.
1117
1118 See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
1119 in TyCoRep.
1120
1121 N.B. Until now (Aug 2018) we didn't check anything for coercion variables.
1122
1123 Note [Printing foralls in type family instances]
1124 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1125 We use the same criteria as in Note [When to print foralls] to determine
1126 whether a type family instance should be pretty-printed with an explicit
1127 `forall`. Example:
1128
1129 type family Foo (a :: k) :: k where
1130 Foo Maybe = []
1131 Foo (a :: Type) = Int
1132 Foo a = a
1133
1134 Without -fprint-explicit-foralls enabled, this will be pretty-printed as:
1135
1136 type family Foo (a :: k) :: k where
1137 Foo Maybe = []
1138 Foo a = Int
1139 forall k (a :: k). Foo a = a
1140
1141 Note that only the third equation has an explicit forall, since it has a type
1142 variable with a non-Type kind. (If -fprint-explicit-foralls were enabled, then
1143 the second equation would be preceded with `forall a.`.)
1144
1145 There is one tricky point in the implementation: what visibility
1146 do we give the type variables in a type family instance? Type family instances
1147 only store type *variables*, not type variable *binders*, and only the latter
1148 has visibility information. We opt to default the visibility of each of these
1149 type variables to Specified because users can't ever instantiate these
1150 variables manually, so the choice of visibility is only relevant to
1151 pretty-printing. (This is why the `k` in `forall k (a :: k). ...` above is
1152 printed the way it is, even though it wasn't written explicitly in the
1153 original source code.)
1154
1155 We adopt the same strategy for data family instances. Example:
1156
1157 data family DF (a :: k)
1158 data instance DF '[a, b] = DFList
1159
1160 That data family instance is pretty-printed as:
1161
1162 data instance forall j (a :: j) (b :: j). DF '[a, b] = DFList
1163
1164 This is despite that the representation tycon for this data instance (call it
1165 $DF:List) actually has different visibilities for its binders.
1166 However, the visibilities of these binders are utterly irrelevant to the
1167 programmer, who cares only about the specificity of variables in `DF`'s type,
1168 not $DF:List's type. Therefore, we opt to pretty-print all variables in data
1169 family instances as Specified.
1170
1171 Note [Printing promoted type constructors]
1172 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1173 Consider this GHCi session (#14343)
1174 > _ :: Proxy '[ 'True ]
1175 error:
1176 Found hole: _ :: Proxy '['True]
1177
1178 This would be bad, because the '[' looks like a character literal.
1179 Solution: in type-level lists and tuples, add a leading space
1180 if the first type is itself promoted. See pprSpaceIfPromotedTyCon.
1181 -}
1182
1183
1184 -------------------
1185
1186 -- | Prefix a space if the given 'IfaceType' is a promoted 'TyCon'.
1187 -- See Note [Printing promoted type constructors]
1188 pprSpaceIfPromotedTyCon :: IfaceType -> SDoc -> SDoc
1189 pprSpaceIfPromotedTyCon (IfaceTyConApp tyCon _)
1190 = case ifaceTyConIsPromoted (ifaceTyConInfo tyCon) of
1191 IsPromoted -> (space <>)
1192 _ -> id
1193 pprSpaceIfPromotedTyCon _
1194 = id
1195
1196 -- See equivalent function in TyCoRep.hs
1197 pprIfaceTyList :: PprPrec -> IfaceType -> IfaceType -> SDoc
1198 -- Given a type-level list (t1 ': t2), see if we can print
1199 -- it in list notation [t1, ...].
1200 -- Precondition: Opt_PrintExplicitKinds is off
1201 pprIfaceTyList ctxt_prec ty1 ty2
1202 = case gather ty2 of
1203 (arg_tys, Nothing)
1204 -> char '\'' <> brackets (pprSpaceIfPromotedTyCon ty1 (fsep
1205 (punctuate comma (map (ppr_ty topPrec) (ty1:arg_tys)))))
1206 (arg_tys, Just tl)
1207 -> maybeParen ctxt_prec funPrec $ hang (ppr_ty funPrec ty1)
1208 2 (fsep [ colon <+> ppr_ty funPrec ty | ty <- arg_tys ++ [tl]])
1209 where
1210 gather :: IfaceType -> ([IfaceType], Maybe IfaceType)
1211 -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
1212 -- = (tys, Just tl) means ty is of form t1:t2:...tn:tl
1213 gather (IfaceTyConApp tc tys)
1214 | tc `ifaceTyConHasKey` consDataConKey
1215 , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
1216 , isInvisibleArgFlag argf
1217 , (args, tl) <- gather ty2
1218 = (ty1:args, tl)
1219 | tc `ifaceTyConHasKey` nilDataConKey
1220 = ([], Nothing)
1221 gather ty = ([], Just ty)
1222
1223 pprIfaceTypeApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
1224 pprIfaceTypeApp prec tc args = pprTyTcApp prec tc args
1225
1226 pprTyTcApp :: PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
1227 pprTyTcApp ctxt_prec tc tys =
1228 sdocWithDynFlags $ \dflags ->
1229 getPprStyle $ \style ->
1230 pprTyTcApp' ctxt_prec tc tys dflags style
1231
1232 pprTyTcApp' :: PprPrec -> IfaceTyCon -> IfaceAppArgs
1233 -> DynFlags -> PprStyle -> SDoc
1234 pprTyTcApp' ctxt_prec tc tys dflags style
1235 | ifaceTyConName tc `hasKey` ipClassKey
1236 , IA_Arg (IfaceLitTy (IfaceStrTyLit n))
1237 Required (IA_Arg ty Required IA_Nil) <- tys
1238 = maybeParen ctxt_prec funPrec
1239 $ char '?' <> ftext n <> text "::" <> ppr_ty topPrec ty
1240
1241 | IfaceTupleTyCon arity sort <- ifaceTyConSort info
1242 , not (debugStyle style)
1243 , arity == ifaceVisAppArgsLength tys
1244 = pprTuple ctxt_prec sort (ifaceTyConIsPromoted info) tys
1245
1246 | IfaceSumTyCon arity <- ifaceTyConSort info
1247 = pprSum arity (ifaceTyConIsPromoted info) tys
1248
1249 | tc `ifaceTyConHasKey` consDataConKey
1250 , not (gopt Opt_PrintExplicitKinds dflags)
1251 , IA_Arg _ argf (IA_Arg ty1 Required (IA_Arg ty2 Required IA_Nil)) <- tys
1252 , isInvisibleArgFlag argf
1253 = pprIfaceTyList ctxt_prec ty1 ty2
1254
1255 | tc `ifaceTyConHasKey` tYPETyConKey
1256 , IA_Arg (IfaceTyConApp rep IA_Nil) Required IA_Nil <- tys
1257 , rep `ifaceTyConHasKey` liftedRepDataConKey
1258 = kindType
1259
1260 | otherwise
1261 = getPprDebug $ \dbg ->
1262 if | not dbg && tc `ifaceTyConHasKey` errorMessageTypeErrorFamKey
1263 -- Suppress detail unles you _really_ want to see
1264 -> text "(TypeError ...)"
1265
1266 | Just doc <- ppr_equality ctxt_prec tc (appArgsIfaceTypes tys)
1267 -> doc
1268
1269 | otherwise
1270 -> ppr_iface_tc_app ppr_app_arg ctxt_prec tc tys_wo_kinds
1271 where
1272 info = ifaceTyConInfo tc
1273 tys_wo_kinds = appArgsIfaceTypesArgFlags $ stripInvisArgs dflags tys
1274
1275 -- | Pretty-print a type-level equality.
1276 -- Returns (Just doc) if the argument is a /saturated/ application
1277 -- of eqTyCon (~)
1278 -- eqPrimTyCon (~#)
1279 -- eqReprPrimTyCon (~R#)
1280 -- heqTyCon (~~)
1281 --
1282 -- See Note [Equality predicates in IfaceType]
1283 -- and Note [The equality types story] in TysPrim
1284 ppr_equality :: PprPrec -> IfaceTyCon -> [IfaceType] -> Maybe SDoc
1285 ppr_equality ctxt_prec tc args
1286 | hetero_eq_tc
1287 , [k1, k2, t1, t2] <- args
1288 = Just $ print_equality (k1, k2, t1, t2)
1289
1290 | hom_eq_tc
1291 , [k, t1, t2] <- args
1292 = Just $ print_equality (k, k, t1, t2)
1293
1294 | otherwise
1295 = Nothing
1296 where
1297 homogeneous = tc_name `hasKey` eqTyConKey -- (~)
1298 || hetero_tc_used_homogeneously
1299 where
1300 hetero_tc_used_homogeneously
1301 = case ifaceTyConSort $ ifaceTyConInfo tc of
1302 IfaceEqualityTyCon -> True
1303 _other -> False
1304 -- True <=> a heterogeneous equality whose arguments
1305 -- are (in this case) of the same kind
1306
1307 tc_name = ifaceTyConName tc
1308 pp = ppr_ty
1309 hom_eq_tc = tc_name `hasKey` eqTyConKey -- (~)
1310 hetero_eq_tc = tc_name `hasKey` eqPrimTyConKey -- (~#)
1311 || tc_name `hasKey` eqReprPrimTyConKey -- (~R#)
1312 || tc_name `hasKey` heqTyConKey -- (~~)
1313 nominal_eq_tc = tc_name `hasKey` heqTyConKey -- (~~)
1314 || tc_name `hasKey` eqPrimTyConKey -- (~#)
1315 print_equality args =
1316 sdocWithDynFlags $ \dflags ->
1317 getPprStyle $ \style ->
1318 print_equality' args style dflags
1319
1320 print_equality' (ki1, ki2, ty1, ty2) style dflags
1321 | -- If -fprint-equality-relations is on, just print the original TyCon
1322 print_eqs
1323 = ppr_infix_eq (ppr tc)
1324
1325 | -- Homogeneous use of heterogeneous equality (ty1 ~~ ty2)
1326 -- or unlifted equality (ty1 ~# ty2)
1327 nominal_eq_tc, homogeneous
1328 = ppr_infix_eq (text "~")
1329
1330 | -- Heterogeneous use of unlifted equality (ty1 ~# ty2)
1331 not homogeneous
1332 = ppr_infix_eq (ppr heqTyCon)
1333
1334 | -- Homogeneous use of representational unlifted equality (ty1 ~R# ty2)
1335 tc_name `hasKey` eqReprPrimTyConKey, homogeneous
1336 = let ki | print_kinds = [pp appPrec ki1]
1337 | otherwise = []
1338 in pprIfacePrefixApp ctxt_prec (ppr coercibleTyCon)
1339 (ki ++ [pp appPrec ty1, pp appPrec ty2])
1340
1341 -- The other cases work as you'd expect
1342 | otherwise
1343 = ppr_infix_eq (ppr tc)
1344 where
1345 ppr_infix_eq :: SDoc -> SDoc
1346 ppr_infix_eq eq_op = pprIfaceInfixApp ctxt_prec eq_op
1347 (pp_ty_ki ty1 ki1) (pp_ty_ki ty2 ki2)
1348 where
1349 pp_ty_ki ty ki
1350 | print_kinds
1351 = parens (pp topPrec ty <+> dcolon <+> pp opPrec ki)
1352 | otherwise
1353 = pp opPrec ty
1354
1355 print_kinds = gopt Opt_PrintExplicitKinds dflags
1356 print_eqs = gopt Opt_PrintEqualityRelations dflags ||
1357 dumpStyle style || debugStyle style
1358
1359
1360 pprIfaceCoTcApp :: PprPrec -> IfaceTyCon -> [IfaceCoercion] -> SDoc
1361 pprIfaceCoTcApp ctxt_prec tc tys =
1362 ppr_iface_tc_app (\prec (co, _) -> ppr_co prec co) ctxt_prec tc
1363 (map (, Required) tys)
1364 -- We are trying to re-use ppr_iface_tc_app here, which requires its
1365 -- arguments to be accompanied by visibilities. But visibility is
1366 -- irrelevant when printing coercions, so just default everything to
1367 -- Required.
1368
1369 -- | Pretty-prints an application of a type constructor to some arguments
1370 -- (whose visibilities are known). This is polymorphic (over @a@) since we use
1371 -- this function to pretty-print two different things:
1372 --
1373 -- 1. Types (from `pprTyTcApp'`)
1374 --
1375 -- 2. Coercions (from 'pprIfaceCoTcApp')
1376 ppr_iface_tc_app :: (PprPrec -> (a, ArgFlag) -> SDoc)
1377 -> PprPrec -> IfaceTyCon -> [(a, ArgFlag)] -> SDoc
1378 ppr_iface_tc_app pp _ tc [ty]
1379 | tc `ifaceTyConHasKey` listTyConKey = pprPromotionQuote tc <> brackets (pp topPrec ty)
1380
1381 ppr_iface_tc_app pp ctxt_prec tc tys
1382 | tc `ifaceTyConHasKey` liftedTypeKindTyConKey
1383 = kindType
1384
1385 | not (isSymOcc (nameOccName (ifaceTyConName tc)))
1386 = pprIfacePrefixApp ctxt_prec (ppr tc) (map (pp appPrec) tys)
1387
1388 | [ ty1@(_, Required)
1389 , ty2@(_, Required) ] <- tys
1390 -- Infix, two visible arguments (we know nothing of precedence though).
1391 -- Don't apply this special case if one of the arguments is invisible,
1392 -- lest we print something like (@LiftedRep -> @LiftedRep) (#15941).
1393 = pprIfaceInfixApp ctxt_prec (ppr tc)
1394 (pp opPrec ty1) (pp opPrec ty2)
1395
1396 | otherwise
1397 = pprIfacePrefixApp ctxt_prec (parens (ppr tc)) (map (pp appPrec) tys)
1398
1399 pprSum :: Arity -> PromotionFlag -> IfaceAppArgs -> SDoc
1400 pprSum _arity is_promoted args
1401 = -- drop the RuntimeRep vars.
1402 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1403 let tys = appArgsIfaceTypes args
1404 args' = drop (length tys `div` 2) tys
1405 in pprPromotionQuoteI is_promoted
1406 <> sumParens (pprWithBars (ppr_ty topPrec) args')
1407
1408 pprTuple :: PprPrec -> TupleSort -> PromotionFlag -> IfaceAppArgs -> SDoc
1409 pprTuple ctxt_prec ConstraintTuple NotPromoted IA_Nil
1410 = maybeParen ctxt_prec appPrec $
1411 text "() :: Constraint"
1412
1413 -- All promoted constructors have kind arguments
1414 pprTuple _ sort IsPromoted args
1415 = let tys = appArgsIfaceTypes args
1416 args' = drop (length tys `div` 2) tys
1417 spaceIfPromoted = case args' of
1418 arg0:_ -> pprSpaceIfPromotedTyCon arg0
1419 _ -> id
1420 in pprPromotionQuoteI IsPromoted <>
1421 tupleParens sort (spaceIfPromoted (pprWithCommas pprIfaceType args'))
1422
1423 pprTuple _ sort promoted args
1424 = -- drop the RuntimeRep vars.
1425 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
1426 let tys = appArgsIfaceTypes args
1427 args' = case sort of
1428 UnboxedTuple -> drop (length tys `div` 2) tys
1429 _ -> tys
1430 in
1431 pprPromotionQuoteI promoted <>
1432 tupleParens sort (pprWithCommas pprIfaceType args')
1433
1434 pprIfaceTyLit :: IfaceTyLit -> SDoc
1435 pprIfaceTyLit (IfaceNumTyLit n) = integer n
1436 pprIfaceTyLit (IfaceStrTyLit n) = text (show n)
1437
1438 pprIfaceCoercion, pprParendIfaceCoercion :: IfaceCoercion -> SDoc
1439 pprIfaceCoercion = ppr_co topPrec
1440 pprParendIfaceCoercion = ppr_co appPrec
1441
1442 ppr_co :: PprPrec -> IfaceCoercion -> SDoc
1443 ppr_co _ (IfaceReflCo ty) = angleBrackets (ppr ty) <> ppr_role Nominal
1444 ppr_co _ (IfaceGReflCo r ty IfaceMRefl)
1445 = angleBrackets (ppr ty) <> ppr_role r
1446 ppr_co ctxt_prec (IfaceGReflCo r ty (IfaceMCo co))
1447 = ppr_special_co ctxt_prec
1448 (text "GRefl" <+> ppr r <+> pprParendIfaceType ty) [co]
1449 ppr_co ctxt_prec (IfaceFunCo r co1 co2)
1450 = maybeParen ctxt_prec funPrec $
1451 sep (ppr_co funPrec co1 : ppr_fun_tail co2)
1452 where
1453 ppr_fun_tail (IfaceFunCo r co1 co2)
1454 = (arrow <> ppr_role r <+> ppr_co funPrec co1) : ppr_fun_tail co2
1455 ppr_fun_tail other_co
1456 = [arrow <> ppr_role r <+> pprIfaceCoercion other_co]
1457
1458 ppr_co _ (IfaceTyConAppCo r tc cos)
1459 = parens (pprIfaceCoTcApp topPrec tc cos) <> ppr_role r
1460 ppr_co ctxt_prec (IfaceAppCo co1 co2)
1461 = maybeParen ctxt_prec appPrec $
1462 ppr_co funPrec co1 <+> pprParendIfaceCoercion co2
1463 ppr_co ctxt_prec co@(IfaceForAllCo {})
1464 = maybeParen ctxt_prec funPrec $
1465 pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co)
1466 where
1467 (tvs, inner_co) = split_co co
1468
1469 split_co (IfaceForAllCo (IfaceTvBndr (name, _)) kind_co co')
1470 = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
1471 split_co (IfaceForAllCo (IfaceIdBndr (name, _)) kind_co co')
1472 = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
1473 split_co co' = ([], co')
1474
1475 -- Why these three? See Note [TcTyVars in IfaceType]
1476 ppr_co _ (IfaceFreeCoVar covar) = ppr covar
1477 ppr_co _ (IfaceCoVarCo covar) = ppr covar
1478 ppr_co _ (IfaceHoleCo covar) = braces (ppr covar)
1479
1480 ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
1481 = maybeParen ctxt_prec appPrec $
1482 text "UnsafeCo" <+> ppr r <+>
1483 pprParendIfaceType ty1 <+> pprParendIfaceType ty2
1484
1485 ppr_co _ (IfaceUnivCo prov role ty1 ty2)
1486 = text "Univ" <> (parens $
1487 sep [ ppr role <+> pprIfaceUnivCoProv prov
1488 , dcolon <+> ppr ty1 <> comma <+> ppr ty2 ])
1489
1490 ppr_co ctxt_prec (IfaceInstCo co ty)
1491 = maybeParen ctxt_prec appPrec $
1492 text "Inst" <+> pprParendIfaceCoercion co
1493 <+> pprParendIfaceCoercion ty
1494
1495 ppr_co ctxt_prec (IfaceAxiomRuleCo tc cos)
1496 = maybeParen ctxt_prec appPrec $ ppr tc <+> parens (interpp'SP cos)
1497
1498 ppr_co ctxt_prec (IfaceAxiomInstCo n i cos)
1499 = ppr_special_co ctxt_prec (ppr n <> brackets (ppr i)) cos
1500 ppr_co ctxt_prec (IfaceSymCo co)
1501 = ppr_special_co ctxt_prec (text "Sym") [co]
1502 ppr_co ctxt_prec (IfaceTransCo co1 co2)
1503 = maybeParen ctxt_prec opPrec $
1504 ppr_co opPrec co1 <+> semi <+> ppr_co opPrec co2
1505 ppr_co ctxt_prec (IfaceNthCo d co)
1506 = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
1507 ppr_co ctxt_prec (IfaceLRCo lr co)
1508 = ppr_special_co ctxt_prec (ppr lr) [co]
1509 ppr_co ctxt_prec (IfaceSubCo co)
1510 = ppr_special_co ctxt_prec (text "Sub") [co]
1511 ppr_co ctxt_prec (IfaceKindCo co)
1512 = ppr_special_co ctxt_prec (text "Kind") [co]
1513
1514 ppr_special_co :: PprPrec -> SDoc -> [IfaceCoercion] -> SDoc
1515 ppr_special_co ctxt_prec doc cos
1516 = maybeParen ctxt_prec appPrec
1517 (sep [doc, nest 4 (sep (map pprParendIfaceCoercion cos))])
1518
1519 ppr_role :: Role -> SDoc
1520 ppr_role r = underscore <> pp_role
1521 where pp_role = case r of
1522 Nominal -> char 'N'
1523 Representational -> char 'R'
1524 Phantom -> char 'P'
1525
1526 ------------------
1527 pprIfaceUnivCoProv :: IfaceUnivCoProv -> SDoc
1528 pprIfaceUnivCoProv IfaceUnsafeCoerceProv
1529 = text "unsafe"
1530 pprIfaceUnivCoProv (IfacePhantomProv co)
1531 = text "phantom" <+> pprParendIfaceCoercion co
1532 pprIfaceUnivCoProv (IfaceProofIrrelProv co)
1533 = text "irrel" <+> pprParendIfaceCoercion co
1534 pprIfaceUnivCoProv (IfacePluginProv s)
1535 = text "plugin" <+> doubleQuotes (text s)
1536
1537 -------------------
1538 instance Outputable IfaceTyCon where
1539 ppr tc = pprPromotionQuote tc <> ppr (ifaceTyConName tc)
1540
1541 pprPromotionQuote :: IfaceTyCon -> SDoc
1542 pprPromotionQuote tc =
1543 pprPromotionQuoteI $ ifaceTyConIsPromoted $ ifaceTyConInfo tc
1544
1545 pprPromotionQuoteI :: PromotionFlag -> SDoc
1546 pprPromotionQuoteI NotPromoted = empty
1547 pprPromotionQuoteI IsPromoted = char '\''
1548
1549 instance Outputable IfaceCoercion where
1550 ppr = pprIfaceCoercion
1551
1552 instance Binary IfaceTyCon where
1553 put_ bh (IfaceTyCon n i) = put_ bh n >> put_ bh i
1554
1555 get bh = do n <- get bh
1556 i <- get bh
1557 return (IfaceTyCon n i)
1558
1559 instance Binary IfaceTyConSort where
1560 put_ bh IfaceNormalTyCon = putByte bh 0
1561 put_ bh (IfaceTupleTyCon arity sort) = putByte bh 1 >> put_ bh arity >> put_ bh sort
1562 put_ bh (IfaceSumTyCon arity) = putByte bh 2 >> put_ bh arity
1563 put_ bh IfaceEqualityTyCon = putByte bh 3
1564
1565 get bh = do
1566 n <- getByte bh
1567 case n of
1568 0 -> return IfaceNormalTyCon
1569 1 -> IfaceTupleTyCon <$> get bh <*> get bh
1570 2 -> IfaceSumTyCon <$> get bh
1571 _ -> return IfaceEqualityTyCon
1572
1573 instance Binary IfaceTyConInfo where
1574 put_ bh (IfaceTyConInfo i s) = put_ bh i >> put_ bh s
1575
1576 get bh = IfaceTyConInfo <$> get bh <*> get bh
1577
1578 instance Outputable IfaceTyLit where
1579 ppr = pprIfaceTyLit
1580
1581 instance Binary IfaceTyLit where
1582 put_ bh (IfaceNumTyLit n) = putByte bh 1 >> put_ bh n
1583 put_ bh (IfaceStrTyLit n) = putByte bh 2 >> put_ bh n
1584
1585 get bh =
1586 do tag <- getByte bh
1587 case tag of
1588 1 -> do { n <- get bh
1589 ; return (IfaceNumTyLit n) }
1590 2 -> do { n <- get bh
1591 ; return (IfaceStrTyLit n) }
1592 _ -> panic ("get IfaceTyLit " ++ show tag)
1593
1594 instance Binary IfaceAppArgs where
1595 put_ bh tk =
1596 case tk of
1597 IA_Arg t a ts -> putByte bh 0 >> put_ bh t >> put_ bh a >> put_ bh ts
1598 IA_Nil -> putByte bh 1
1599
1600 get bh =
1601 do c <- getByte bh
1602 case c of
1603 0 -> do
1604 t <- get bh
1605 a <- get bh
1606 ts <- get bh
1607 return $! IA_Arg t a ts
1608 1 -> return IA_Nil
1609 _ -> panic ("get IfaceAppArgs " ++ show c)
1610
1611 -------------------
1612
1613 -- Some notes about printing contexts
1614 --
1615 -- In the event that we are printing a singleton context (e.g. @Eq a@) we can
1616 -- omit parentheses. However, we must take care to set the precedence correctly
1617 -- to opPrec, since something like @a :~: b@ must be parenthesized (see
1618 -- #9658).
1619 --
1620 -- When printing a larger context we use 'fsep' instead of 'sep' so that
1621 -- the context doesn't get displayed as a giant column. Rather than,
1622 -- instance (Eq a,
1623 -- Eq b,
1624 -- Eq c,
1625 -- Eq d,
1626 -- Eq e,
1627 -- Eq f,
1628 -- Eq g,
1629 -- Eq h,
1630 -- Eq i,
1631 -- Eq j,
1632 -- Eq k,
1633 -- Eq l) =>
1634 -- Eq (a, b, c, d, e, f, g, h, i, j, k, l)
1635 --
1636 -- we want
1637 --
1638 -- instance (Eq a, Eq b, Eq c, Eq d, Eq e, Eq f, Eq g, Eq h, Eq i,
1639 -- Eq j, Eq k, Eq l) =>
1640 -- Eq (a, b, c, d, e, f, g, h, i, j, k, l)
1641
1642
1643
1644 -- | Prints "(C a, D b) =>", including the arrow.
1645 -- Used when we want to print a context in a type, so we
1646 -- use 'funPrec' to decide whether to parenthesise a singleton
1647 -- predicate; e.g. Num a => a -> a
1648 pprIfaceContextArr :: [IfacePredType] -> SDoc
1649 pprIfaceContextArr [] = empty
1650 pprIfaceContextArr [pred] = ppr_ty funPrec pred <+> darrow
1651 pprIfaceContextArr preds = ppr_parend_preds preds <+> darrow
1652
1653 -- | Prints a context or @()@ if empty
1654 -- You give it the context precedence
1655 pprIfaceContext :: PprPrec -> [IfacePredType] -> SDoc
1656 pprIfaceContext _ [] = text "()"
1657 pprIfaceContext prec [pred] = ppr_ty prec pred
1658 pprIfaceContext _ preds = ppr_parend_preds preds
1659
1660 ppr_parend_preds :: [IfacePredType] -> SDoc
1661 ppr_parend_preds preds = parens (fsep (punctuate comma (map ppr preds)))
1662
1663 instance Binary IfaceType where
1664 put_ _ (IfaceFreeTyVar tv)
1665 = pprPanic "Can't serialise IfaceFreeTyVar" (ppr tv)
1666
1667 put_ bh (IfaceForAllTy aa ab) = do
1668 putByte bh 0
1669 put_ bh aa
1670 put_ bh ab
1671 put_ bh (IfaceTyVar ad) = do
1672 putByte bh 1
1673 put_ bh ad
1674 put_ bh (IfaceAppTy ae af) = do
1675 putByte bh 2
1676 put_ bh ae
1677 put_ bh af
1678 put_ bh (IfaceFunTy af ag ah) = do
1679 putByte bh 3
1680 put_ bh af
1681 put_ bh ag
1682 put_ bh ah
1683 put_ bh (IfaceTyConApp tc tys)
1684 = do { putByte bh 5; put_ bh tc; put_ bh tys }
1685 put_ bh (IfaceCastTy a b)
1686 = do { putByte bh 6; put_ bh a; put_ bh b }
1687 put_ bh (IfaceCoercionTy a)
1688 = do { putByte bh 7; put_ bh a }
1689 put_ bh (IfaceTupleTy s i tys)
1690 = do { putByte bh 8; put_ bh s; put_ bh i; put_ bh tys }
1691 put_ bh (IfaceLitTy n)
1692 = do { putByte bh 9; put_ bh n }
1693
1694 get bh = do
1695 h <- getByte bh
1696 case h of
1697 0 -> do aa <- get bh
1698 ab <- get bh
1699 return (IfaceForAllTy aa ab)
1700 1 -> do ad <- get bh
1701 return (IfaceTyVar ad)
1702 2 -> do ae <- get bh
1703 af <- get bh
1704 return (IfaceAppTy ae af)
1705 3 -> do af <- get bh
1706 ag <- get bh
1707 ah <- get bh
1708 return (IfaceFunTy af ag ah)
1709 5 -> do { tc <- get bh; tys <- get bh
1710 ; return (IfaceTyConApp tc tys) }
1711 6 -> do { a <- get bh; b <- get bh
1712 ; return (IfaceCastTy a b) }
1713 7 -> do { a <- get bh
1714 ; return (IfaceCoercionTy a) }
1715
1716 8 -> do { s <- get bh; i <- get bh; tys <- get bh
1717 ; return (IfaceTupleTy s i tys) }
1718 _ -> do n <- get bh
1719 return (IfaceLitTy n)
1720
1721 instance Binary IfaceMCoercion where
1722 put_ bh IfaceMRefl = do
1723 putByte bh 1
1724 put_ bh (IfaceMCo co) = do
1725 putByte bh 2
1726 put_ bh co
1727
1728 get bh = do
1729 tag <- getByte bh
1730 case tag of
1731 1 -> return IfaceMRefl
1732 2 -> do a <- get bh
1733 return $ IfaceMCo a
1734 _ -> panic ("get IfaceMCoercion " ++ show tag)
1735
1736 instance Binary IfaceCoercion where
1737 put_ bh (IfaceReflCo a) = do
1738 putByte bh 1
1739 put_ bh a
1740 put_ bh (IfaceGReflCo a b c) = do
1741 putByte bh 2
1742 put_ bh a
1743 put_ bh b
1744 put_ bh c
1745 put_ bh (IfaceFunCo a b c) = do
1746 putByte bh 3
1747 put_ bh a
1748 put_ bh b
1749 put_ bh c
1750 put_ bh (IfaceTyConAppCo a b c) = do
1751 putByte bh 4
1752 put_ bh a
1753 put_ bh b
1754 put_ bh c
1755 put_ bh (IfaceAppCo a b) = do
1756 putByte bh 5
1757 put_ bh a
1758 put_ bh b
1759 put_ bh (IfaceForAllCo a b c) = do
1760 putByte bh 6
1761 put_ bh a
1762 put_ bh b
1763 put_ bh c
1764 put_ bh (IfaceCoVarCo a) = do
1765 putByte bh 7
1766 put_ bh a
1767 put_ bh (IfaceAxiomInstCo a b c) = do
1768 putByte bh 8
1769 put_ bh a
1770 put_ bh b
1771 put_ bh c
1772 put_ bh (IfaceUnivCo a b c d) = do
1773 putByte bh 9
1774 put_ bh a
1775 put_ bh b
1776 put_ bh c
1777 put_ bh d
1778 put_ bh (IfaceSymCo a) = do
1779 putByte bh 10
1780 put_ bh a
1781 put_ bh (IfaceTransCo a b) = do
1782 putByte bh 11
1783 put_ bh a
1784 put_ bh b
1785 put_ bh (IfaceNthCo a b) = do
1786 putByte bh 12
1787 put_ bh a
1788 put_ bh b
1789 put_ bh (IfaceLRCo a b) = do
1790 putByte bh 13
1791 put_ bh a
1792 put_ bh b
1793 put_ bh (IfaceInstCo a b) = do
1794 putByte bh 14
1795 put_ bh a
1796 put_ bh b
1797 put_ bh (IfaceKindCo a) = do
1798 putByte bh 15
1799 put_ bh a
1800 put_ bh (IfaceSubCo a) = do
1801 putByte bh 16
1802 put_ bh a
1803 put_ bh (IfaceAxiomRuleCo a b) = do
1804 putByte bh 17
1805 put_ bh a
1806 put_ bh b
1807 put_ _ (IfaceFreeCoVar cv)
1808 = pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
1809 put_ _ (IfaceHoleCo cv)
1810 = pprPanic "Can't serialise IfaceHoleCo" (ppr cv)
1811 -- See Note [Holes in IfaceCoercion]
1812
1813 get bh = do
1814 tag <- getByte bh
1815 case tag of
1816 1 -> do a <- get bh
1817 return $ IfaceReflCo a
1818 2 -> do a <- get bh
1819 b <- get bh
1820 c <- get bh
1821 return $ IfaceGReflCo a b c
1822 3 -> do a <- get bh
1823 b <- get bh
1824 c <- get bh
1825 return $ IfaceFunCo a b c
1826 4 -> do a <- get bh
1827 b <- get bh
1828 c <- get bh
1829 return $ IfaceTyConAppCo a b c
1830 5 -> do a <- get bh
1831 b <- get bh
1832 return $ IfaceAppCo a b
1833 6 -> do a <- get bh
1834 b <- get bh
1835 c <- get bh
1836 return $ IfaceForAllCo a b c
1837 7 -> do a <- get bh
1838 return $ IfaceCoVarCo a
1839 8 -> do a <- get bh
1840 b <- get bh
1841 c <- get bh
1842 return $ IfaceAxiomInstCo a b c
1843 9 -> do a <- get bh
1844 b <- get bh
1845 c <- get bh
1846 d <- get bh
1847 return $ IfaceUnivCo a b c d
1848 10-> do a <- get bh
1849 return $ IfaceSymCo a
1850 11-> do a <- get bh
1851 b <- get bh
1852 return $ IfaceTransCo a b
1853 12-> do a <- get bh
1854 b <- get bh
1855 return $ IfaceNthCo a b
1856 13-> do a <- get bh
1857 b <- get bh
1858 return $ IfaceLRCo a b
1859 14-> do a <- get bh
1860 b <- get bh
1861 return $ IfaceInstCo a b
1862 15-> do a <- get bh
1863 return $ IfaceKindCo a
1864 16-> do a <- get bh
1865 return $ IfaceSubCo a
1866 17-> do a <- get bh
1867 b <- get bh
1868 return $ IfaceAxiomRuleCo a b
1869 _ -> panic ("get IfaceCoercion " ++ show tag)
1870
1871 instance Binary IfaceUnivCoProv where
1872 put_ bh IfaceUnsafeCoerceProv = putByte bh 1
1873 put_ bh (IfacePhantomProv a) = do
1874 putByte bh 2
1875 put_ bh a
1876 put_ bh (IfaceProofIrrelProv a) = do
1877 putByte bh 3
1878 put_ bh a
1879 put_ bh (IfacePluginProv a) = do
1880 putByte bh 4
1881 put_ bh a
1882
1883 get bh = do
1884 tag <- getByte bh
1885 case tag of
1886 1 -> return $ IfaceUnsafeCoerceProv
1887 2 -> do a <- get bh
1888 return $ IfacePhantomProv a
1889 3 -> do a <- get bh
1890 return $ IfaceProofIrrelProv a
1891 4 -> do a <- get bh
1892 return $ IfacePluginProv a
1893 _ -> panic ("get IfaceUnivCoProv " ++ show tag)
1894
1895
1896 instance Binary (DefMethSpec IfaceType) where
1897 put_ bh VanillaDM = putByte bh 0
1898 put_ bh (GenericDM t) = putByte bh 1 >> put_ bh t
1899 get bh = do
1900 h <- getByte bh
1901 case h of
1902 0 -> return VanillaDM
1903 _ -> do { t <- get bh; return (GenericDM t) }