Re-add FunTy (big patch)
[ghc.git] / compiler / types / TyCoRep.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1998
4 \section[TyCoRep]{Type and Coercion - friends' interface}
5
6 Note [The Type-related module hierarchy]
7 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8 Class
9 CoAxiom
10 TyCon imports Class, CoAxiom
11 TyCoRep imports Class, CoAxiom, TyCon
12 TysPrim imports TyCoRep ( including mkTyConTy )
13 Kind imports TysPrim ( mainly for primitive kinds )
14 Type imports Kind
15 Coercion imports Type
16 -}
17
18 -- We expose the relevant stuff from this module via the Type module
19 {-# OPTIONS_HADDOCK hide #-}
20 {-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
21 DeriveTraversable, MultiWayIf #-}
22 {-# LANGUAGE ImplicitParams #-}
23
24 module TyCoRep (
25 TyThing(..),
26 Type(..),
27 TyLit(..),
28 KindOrType, Kind,
29 PredType, ThetaType, -- Synonyms
30 VisibilityFlag(..),
31
32 -- * Coercions
33 Coercion(..), LeftOrRight(..),
34 UnivCoProvenance(..), CoercionHole(..),
35 CoercionN, CoercionR, CoercionP, KindCoercion,
36
37 -- * Functions over types
38 mkTyConTy, mkTyVarTy, mkTyVarTys,
39 mkFunTy, mkFunTys, mkForAllTy, mkForAllTys,
40 mkPiTy, mkPiTys,
41 isLiftedTypeKind, isUnliftedTypeKind,
42 isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
43 isRuntimeRepKindedTy, dropRuntimeRepArgs,
44 sameVis,
45
46 -- * Functions over binders
47 TyBinder(..), TyVarBinder(..),
48 binderVar, binderType, binderVisibility,
49 delBinderVar,
50 isInvisible, isVisible,
51 isInvisibleBinder, isVisibleBinder,
52
53 -- * Functions over coercions
54 pickLR,
55
56 -- * Pretty-printing
57 pprType, pprParendType, pprTypeApp, pprTvBndr, pprTvBndrs,
58 pprShortTyThing, pprTyThingCategory, pprSigmaType,
59 pprTheta, pprForAll, pprForAllImplicit, pprUserForAll,
60 pprThetaArrowTy, pprClassPred,
61 pprKind, pprParendKind, pprTyLit,
62 TyPrec(..), maybeParen, pprTcAppCo, pprTcAppTy,
63 pprPrefixApp, pprArrowChain, ppr_type,
64 pprDataCons, ppSuggestExplicitKinds,
65
66 -- * Free variables
67 tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
68 tyCoFVsBndr, tyCoFVsOfType, tyCoVarsOfTypeList,
69 tyCoFVsOfTypes, tyCoVarsOfTypesList,
70 closeOverKindsDSet, closeOverKindsFV, closeOverKindsList,
71 coVarsOfType, coVarsOfTypes,
72 coVarsOfCo, coVarsOfCos,
73 tyCoVarsOfCo, tyCoVarsOfCos,
74 tyCoVarsOfCoDSet,
75 tyCoFVsOfCo, tyCoFVsOfCos,
76 tyCoVarsOfCoList, tyCoVarsOfProv,
77 closeOverKinds,
78
79 -- * Substitutions
80 TCvSubst(..), TvSubstEnv, CvSubstEnv,
81 emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
82 emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
83 mkTCvSubst, mkTvSubst,
84 getTvSubstEnv,
85 getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
86 isInScope, notElemTCvSubst,
87 setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
88 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
89 extendTCvSubst,
90 extendCvSubst, extendCvSubstWithClone,
91 extendTvSubst, extendTvSubstWithClone,
92 extendTvSubstList, extendTvSubstAndInScope,
93 unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
94 zipTvSubst, zipCvSubst,
95 mkTvSubstPrs,
96
97 substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
98 substCoWith,
99 substTy, substTyAddInScope,
100 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
101 substTyWithUnchecked,
102 substCoUnchecked, substCoWithUnchecked,
103 substTyWithInScope,
104 substTys, substTheta,
105 lookupTyVar, substTyVarBndr,
106 substCo, substCos, substCoVar, substCoVars, lookupCoVar,
107 substCoVarBndr, cloneTyVarBndr, cloneTyVarBndrs,
108 substTyVar, substTyVars,
109 substForAllCoBndr,
110 substTyVarBndrCallback, substForAllCoBndrCallback,
111 substCoVarBndrCallback,
112
113 -- * Tidying type related things up for printing
114 tidyType, tidyTypes,
115 tidyOpenType, tidyOpenTypes,
116 tidyOpenKind,
117 tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
118 tidyOpenTyCoVar, tidyOpenTyCoVars,
119 tidyTyVarOcc,
120 tidyTopType,
121 tidyKind,
122 tidyCo, tidyCos,
123 tidyTyVarBinder, tidyTyVarBinders
124 ) where
125
126 #include "HsVersions.h"
127
128 import {-# SOURCE #-} DataCon( dataConTyCon, dataConFullSig
129 , dataConUnivTyVarBinders, dataConExTyVarBinders
130 , DataCon, filterEqSpec )
131 import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy
132 , tyCoVarsOfTypesWellScoped
133 , partitionInvisibles, coreView, typeKind
134 , eqType )
135 -- Transitively pulls in a LOT of stuff, better to break the loop
136
137 import {-# SOURCE #-} Coercion
138 import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
139 import {-# SOURCE #-} TysWiredIn ( ptrRepLiftedTy )
140
141 -- friends:
142 import Var
143 import VarEnv
144 import VarSet
145 import Name hiding ( varName )
146 import BasicTypes
147 import TyCon
148 import Class
149 import CoAxiom
150 import FV
151
152 -- others
153 import PrelNames
154 import Binary
155 import Outputable
156 import DynFlags
157 import StaticFlags ( opt_PprStyle_Debug )
158 import FastString
159 import Pair
160 import UniqSupply
161 import Util
162 import UniqFM
163
164 -- libraries
165 import qualified Data.Data as Data hiding ( TyCon )
166 import Data.List
167 import Data.IORef ( IORef ) -- for CoercionHole
168 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
169 import GHC.Stack (CallStack)
170 #endif
171
172 {- **********************************************************************
173 * *
174 Type
175 * *
176 ********************************************************************** -}
177
178 -- | The key representation of types within the compiler
179
180 type KindOrType = Type -- See Note [Arguments to type constructors]
181
182 -- | The key type representing kinds in the compiler.
183 type Kind = Type
184
185 -- If you edit this type, you may need to update the GHC formalism
186 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
187 data Type
188 -- See Note [Non-trivial definitional equality]
189 = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
190
191 | AppTy -- See Note [AppTy rep]
192 Type
193 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
194 --
195 -- 1) Function: must /not/ be a 'TyConApp',
196 -- must be another 'AppTy', or 'TyVarTy'
197 --
198 -- 2) Argument type
199
200 | TyConApp -- See Note [AppTy rep]
201 TyCon
202 [KindOrType] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
203 -- Invariant: saturated applications of 'FunTyCon' must
204 -- use 'FunTy' and saturated synonyms must use their own
205 -- constructors. However, /unsaturated/ 'FunTyCon's
206 -- do appear as 'TyConApp's.
207 -- Parameters:
208 --
209 -- 1) Type constructor being applied to.
210 --
211 -- 2) Type arguments. Might not have enough type arguments
212 -- here to saturate the constructor.
213 -- Even type synonyms are not necessarily saturated;
214 -- for example unsaturated type synonyms
215 -- can appear as the right hand side of a type synonym.
216
217 | ForAllTy
218 {-# UNPACK #-} !TyVarBinder
219 Type -- ^ A Π type.
220 -- This includes arrow types, constructed with
221 -- @ForAllTy (Anon ...)@. See also Note [TyBinder].
222
223 | FunTy Type Type -- ^ t1 -> t2 Very common, so an important special case
224
225 | LitTy TyLit -- ^ Type literals are similar to type constructors.
226
227 | CastTy
228 Type
229 KindCoercion -- ^ A kind cast. The coercion is always nominal.
230 -- INVARIANT: The cast is never refl.
231 -- INVARIANT: The cast is "pushed down" as far as it
232 -- can go. See Note [Pushing down casts]
233
234 | CoercionTy
235 Coercion -- ^ Injection of a Coercion into a type
236 -- This should only ever be used in the RHS of an AppTy,
237 -- in the list of a TyConApp, when applying a promoted
238 -- GADT data constructor
239
240 deriving Data.Data
241
242
243 -- NOTE: Other parts of the code assume that type literals do not contain
244 -- types or type variables.
245 data TyLit
246 = NumTyLit Integer
247 | StrTyLit FastString
248 deriving (Eq, Ord, Data.Data)
249
250 {- Note [The kind invariant]
251 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
252 The kinds
253 # UnliftedTypeKind
254 OpenKind super-kind of *, #
255
256 can never appear under an arrow or type constructor in a kind; they
257 can only be at the top level of a kind. It follows that primitive TyCons,
258 which have a naughty pseudo-kind
259 State# :: * -> #
260 must always be saturated, so that we can never get a type whose kind
261 has a UnliftedTypeKind or ArgTypeKind underneath an arrow.
262
263 Nor can we abstract over a type variable with any of these kinds.
264
265 k :: = kk | # | ArgKind | (#) | OpenKind
266 kk :: = * | kk -> kk | T kk1 ... kkn
267
268 So a type variable can only be abstracted kk.
269
270 Note [AppTy rep]
271 ~~~~~~~~~~~~~~~~
272 Types of the form 'f a' must be of kind *, not #, so we are guaranteed
273 that they are represented by pointers. The reason is that f must have
274 kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
275 in TyCoRep.
276
277 Note [Arguments to type constructors]
278 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
279 Because of kind polymorphism, in addition to type application we now
280 have kind instantiation. We reuse the same notations to do so.
281
282 For example:
283
284 Just (* -> *) Maybe
285 Right * Nat Zero
286
287 are represented by:
288
289 TyConApp (PromotedDataCon Just) [* -> *, Maybe]
290 TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)]
291
292 Important note: Nat is used as a *kind* and not as a type. This can be
293 confusing, since type-level Nat and kind-level Nat are identical. We
294 use the kind of (PromotedDataCon Right) to know if its arguments are
295 kinds or types.
296
297 This kind instantiation only happens in TyConApp currently.
298
299 Note [Pushing down casts]
300 ~~~~~~~~~~~~~~~~~~~~~~~~~
301 Suppose we have (a :: k1 -> *), (b :: k1), and (co :: * ~ q).
302 The type (a b |> co) is `eqType` to ((a |> co') b), where
303 co' = (->) <k1> co. Thus, to make this visible to functions
304 that inspect types, we always push down coercions, preferring
305 the second form. Note that this also applies to TyConApps!
306
307 Note [Non-trivial definitional equality]
308 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
309 Is Int |> <*> the same as Int? YES! In order to reduce headaches,
310 we decide that any reflexive casts in types are just ignored. More
311 generally, the `eqType` function, which defines Core's type equality
312 relation, ignores casts and coercion arguments, as long as the
313 two types have the same kind. This allows us to be a little sloppier
314 in keeping track of coercions, which is a good thing. It also means
315 that eqType does not depend on eqCoercion, which is also a good thing.
316
317 Why is this sensible? That is, why is something different than α-equivalence
318 appropriate for the implementation of eqType?
319
320 Anything smaller than ~ and homogeneous is an appropriate definition for
321 equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any
322 expression of type τ can be transmuted to one of type σ at any point by
323 casting. The same is true of types of type τ. So in some sense, τ and σ are
324 interchangeable.
325
326 But let's be more precise. If we examine the typing rules of FC (say, those in
327 http://www.cis.upenn.edu/~eir/papers/2015/equalities/equalities-extended.pdf)
328 there are several places where the same metavariable is used in two different
329 premises to a rule. (For example, see Ty_App.) There is an implicit equality
330 check here. What definition of equality should we use? By convention, we use
331 α-equivalence. Take any rule with one (or more) of these implicit equality
332 checks. Then there is an admissible rule that uses ~ instead of the implicit
333 check, adding in casts as appropriate.
334
335 The only problem here is that ~ is heterogeneous. To make the kinds work out
336 in the admissible rule that uses ~, it is necessary to homogenize the
337 coercions. That is, if we have η : (τ : κ1) ~ (σ : κ2), then we don't use η;
338 we use η |> kind η, which is homogeneous.
339
340 The effect of this all is that eqType, the implementation of the implicit
341 equality check, can use any homogeneous relation that is smaller than ~, as
342 those rules must also be admissible.
343
344 What would go wrong if we insisted on the casts matching? See the beginning of
345 Section 8 in the unpublished paper above. Theoretically, nothing at all goes
346 wrong. But in practical terms, getting the coercions right proved to be
347 nightmarish. And types would explode: during kind-checking, we often produce
348 reflexive kind coercions. When we try to cast by these, mkCastTy just discards
349 them. But if we used an eqType that distinguished between Int and Int |> <*>,
350 then we couldn't discard -- the output of kind-checking would be enormous,
351 and we would need enormous casts with lots of CoherenceCo's to straighten
352 them out.
353
354 Would anything go wrong if eqType respected type families? No, not at all. But
355 that makes eqType rather hard to implement.
356
357 Thus, the guideline for eqType is that it should be the largest
358 easy-to-implement relation that is still smaller than ~ and homogeneous. The
359 precise choice of relation is somewhat incidental, as long as the smart
360 constructors and destructors in Type respect whatever relation is chosen.
361
362 Another helpful principle with eqType is this:
363
364 ** If (t1 eqType t2) then I can replace t1 by t2 anywhere. **
365
366 This principle also tells us that eqType must relate only types with the
367 same kinds.
368 -}
369
370 {- **********************************************************************
371 * *
372 TyBinder and VisibilityFlag
373 * *
374 ********************************************************************** -}
375
376 -- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
377 -- ('Named') or nondependent ('Anon'). They may also be visible or not.
378 -- See Note [TyBinders]
379 data TyBinder
380 = Named TyVarBinder
381 | Anon Type -- Visibility is determined by the type (Constraint vs. *)
382 deriving Data.Data
383
384 data TyVarBinder
385 = TvBndr TyVar -- Always a TyVar (not CoVar or Id)
386 VisibilityFlag
387 deriving Data.Data
388
389 -- | Is something required to appear in source Haskell ('Visible'),
390 -- permitted by request ('Specified') (visible type application), or
391 -- prohibited entirely from appearing in source Haskell ('Invisible')?
392 -- See Note [TyBinders and VisibilityFlags]
393 data VisibilityFlag = Visible | Specified | Invisible
394 deriving (Eq, Data.Data)
395
396 binderVar :: TyVarBinder -> TyVar
397 binderVar (TvBndr v _) = v
398
399 binderType :: TyVarBinder -> Type
400 binderType (TvBndr v _) = varType v
401
402 binderVisibility :: TyVarBinder -> VisibilityFlag
403 binderVisibility (TvBndr _ vis) = vis
404
405 -- | Remove the binder's variable from the set, if the binder has
406 -- a variable.
407 delBinderVar :: VarSet -> TyVarBinder -> VarSet
408 delBinderVar vars (TvBndr tv _) = vars `delVarSet` tv
409
410 -- | Does this binder bind an invisible argument?
411 isInvisibleBinder :: TyBinder -> Bool
412 isInvisibleBinder (Named (TvBndr _ vis)) = isInvisible vis
413 isInvisibleBinder (Anon ty) = isPredTy ty
414
415 -- | Does this binder bind a visible argument?
416 isVisibleBinder :: TyBinder -> Bool
417 isVisibleBinder = not . isInvisibleBinder
418
419 -- | Do these denote the same level of visibility? Except that
420 -- 'Specified' and 'Invisible' are considered the same. Used
421 -- for printing.
422 sameVis :: VisibilityFlag -> VisibilityFlag -> Bool
423 sameVis Visible Visible = True
424 sameVis Visible _ = False
425 sameVis _ Visible = False
426 sameVis _ _ = True
427
428 isVisible :: VisibilityFlag -> Bool
429 isVisible Visible = True
430 isVisible _ = False
431
432 isInvisible :: VisibilityFlag -> Bool
433 isInvisible v = not (isVisible v)
434
435
436 {- Note [TyBinders]
437 ~~~~~~~~~~~~~~~~~~~
438 A ForAllTy contains a TyVarBinder. But a type can be decomposed
439 to a telescope consisting of a [TyBinder]
440
441 A TyBinder represents the type of binders -- that is, the type of an
442 argument to a Pi-type. GHC Core currently supports two different
443 Pi-types:
444
445 * A non-dependent function,
446 written with ->, e.g. ty1 -> ty2
447 represented as FunTy ty1 ty2
448
449 * A dependent compile-time-only polytype,
450 written with forall, e.g. forall (a:*). ty
451 represented as ForAllTy (TvBndr a v) ty
452
453 Both Pi-types classify terms/types that take an argument. In other
454 words, if `x` is either a function or a polytype, `x arg` makes sense
455 (for an appropriate `arg`). It is thus often convenient to group
456 Pi-types together. This is ForAllTy.
457
458 The two constructors for TyBinder sort out the two different possibilities.
459 `Named` builds a polytype, while `Anon` builds an ordinary function.
460 (ForAllTy (Anon arg) res used to be called FunTy arg res.)
461
462 Note [TyBinders and VisibilityFlags]
463 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
464 A ForAllTy contains a TyVarBinder. Each TyVarBinder is equipped
465 with a VisibilityFlag, which says whether or not arguments for this
466 binder should be visible (explicit) in source Haskell.
467
468 -----------------------------------------------------------------------
469 Occurrences look like this
470 TyBinder GHC displays type as in Haskell souce code
471 -----------------------------------------------------------------------
472 In the type of a term
473 Anon: f :: type -> type Arg required: f x
474 Named Invisible: f :: forall {a}. type Arg not allowed: f
475 Named Specified: f :: forall a. type Arg optional: f or f @Int
476 Named Visible: Illegal: See Note [No Visible TyBinder in terms]
477
478 In the kind of a type
479 Anon: T :: kind -> kind Required: T *
480 Named Invisible: T :: forall {k}. kind Arg not allowed: T
481 Named Specified: T :: forall k. kind Arg not allowed[1]: T
482 Named Visible: T :: forall k -> kind Required: T *
483 ------------------------------------------------------------------------
484
485 [1] In types, in the Specified case, it would make sense to allow
486 optional kind applications, thus (T @*), but we have not
487 yet implemented that
488
489 ---- Examples of where the different visiblities come from -----
490
491 In term declarations:
492
493 * Invisible. Function defn, with no signature: f1 x = x
494 We infer f1 :: forall {a}. a -> a, with 'a' Invisible
495 It's Invisible because it doesn't appear in any
496 user-written signature for f1
497
498 * Specified. Function defn, with signature (implicit forall):
499 f2 :: a -> a; f2 x = x
500 So f2 gets the type f2 :: forall a. a->a, with 'a' Specified
501 even though 'a' is not bound in the source code by an explicit forall
502
503 * Specified. Function defn, with signature (explicit forall):
504 f3 :: forall a. a -> a; f3 x = x
505 So f3 gets the type f3 :: forall a. a->a, with 'a' Specified
506
507 * Invisible/Specified. Function signature with inferred kind polymorphism.
508 f4 :: a b -> Int
509 So 'f4' get the type f4 :: forall {k} (a:k->*) (b:k). a b -> Int
510 Here 'k' is Invisible (it's not mentioned in the type),
511 but 'a' and 'b' are Specified.
512
513 * Specified. Function signature with explicit kind polymorphism
514 f5 :: a (b :: k) -> Int
515 This time 'k' is Specified, because it is mentioned explicitly,
516 so we get f5 :: forall (k:*) (a:k->*) (b:k). a b -> Int
517
518 * Similarly pattern synonyms:
519 Invisible - from inferred types (e.g. no pattern type signature)
520 - or from inferred kind polymorphism
521
522 In type declarations:
523
524 * Invisible (k)
525 data T1 a b = MkT1 (a b)
526 Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> *
527 The kind variable 'k' is Invisible, since it is not mentioned
528
529 Note that 'a' and 'b' correspond to /Anon/ TyBinders in T1's kind,
530 and Anon binders don't have a visibility flag. (Or you could think
531 of Anon having an implicit Visible flag.)
532
533 * Specified (k)
534 data T2 (a::k->*) b = MkT (a b)
535 Here T's kind is T :: forall (k:*). (k->*) -> k -> *
536 The kind variable 'k' is Specified, since it is mentioned in
537 the signature.
538
539 * Visible (k)
540 data T k (a::k->*) b = MkT (a b)
541 Here T's kind is T :: forall k:* -> (k->*) -> k -> *
542 The kind Visible, since it bound in a positional way in T's declaration
543 Every use of T must be explicitly applied to a kind
544
545 * Invisible (k1), Specified (k)
546 data T a b (c :: k) = MkT (a b) (Proxy c)
547 Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
548 So 'k' is Specified, because it appears explicitly,
549 but 'k1' is Invisible, because it does not
550
551 ---- Printing -----
552
553 We print forall types with enough syntax to tell you their visiblity
554 flag. But this is not source Haskell, and these types may not all
555 be parsable.
556
557 Specified: a list of Specified binders is written between `forall` and `.`:
558 const :: forall a b. a -> b -> a
559
560 Invisible: with -fprint-explicit-foralls, Invisible binders are written
561 in braces:
562 f :: forall {k} (a:k). S k a -> Int
563 Otherwise, they are printed like Specified binders.
564
565 Visible: binders are put between `forall` and `->`:
566 T :: forall k -> *
567
568 ---- Other points -----
569
570 * In classic Haskell, all named binders (that is, the type variables in
571 a polymorphic function type f :: forall a. a -> a) have been Invisible.
572
573 * Invisible variables correspond to "generalized" variables from the
574 Visible Type Applications paper (ESOP'16).
575
576 Note [No Visible TyBinder in terms]
577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
578 We don't allow Visible foralls for term variables, including pattern
579 synonyms and data constructors. Why? Because then an application
580 would need a /compulsory/ type argument (possibly without an "@"?),
581 thus (f Int); and we don't have concrete syntax for that.
582
583 We could change this decision, but Visible, Named TyBinders are rare
584 anyway. (Most are Anons.)
585 -}
586
587 instance Binary VisibilityFlag where
588 put_ bh Visible = putByte bh 0
589 put_ bh Specified = putByte bh 1
590 put_ bh Invisible = putByte bh 2
591
592 get bh = do
593 h <- getByte bh
594 case h of
595 0 -> return Visible
596 1 -> return Specified
597 _ -> return Invisible
598
599
600 {- **********************************************************************
601 * *
602 PredType
603 * *
604 ********************************************************************** -}
605
606
607 -- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
608 -- the Haskell predicate @p@, where a predicate is what occurs before
609 -- the @=>@ in a Haskell type.
610 --
611 -- We use 'PredType' as documentation to mark those types that we guarantee to have
612 -- this kind.
613 --
614 -- It can be expanded into its representation, but:
615 --
616 -- * The type checker must treat it as opaque
617 --
618 -- * The rest of the compiler treats it as transparent
619 --
620 -- Consider these examples:
621 --
622 -- > f :: (Eq a) => a -> Int
623 -- > g :: (?x :: Int -> Int) => a -> Int
624 -- > h :: (r\l) => {r} => {l::Int | r}
625 --
626 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
627 type PredType = Type
628
629 -- | A collection of 'PredType's
630 type ThetaType = [PredType]
631
632 {-
633 (We don't support TREX records yet, but the setup is designed
634 to expand to allow them.)
635
636 A Haskell qualified type, such as that for f,g,h above, is
637 represented using
638 * a FunTy for the double arrow
639 * with a type of kind Constraint as the function argument
640
641 The predicate really does turn into a real extra argument to the
642 function. If the argument has type (p :: Constraint) then the predicate p is
643 represented by evidence of type p.
644
645
646 %************************************************************************
647 %* *
648 Simple constructors
649 %* *
650 %************************************************************************
651
652 These functions are here so that they can be used by TysPrim,
653 which in turn is imported by Type
654 -}
655
656 -- named with "Only" to prevent naive use of mkTyVarTy
657 mkTyVarTy :: TyVar -> Type
658 mkTyVarTy v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) )
659 TyVarTy v
660
661 mkTyVarTys :: [TyVar] -> [Type]
662 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
663
664 infixr 3 `mkFunTy` -- Associates to the right
665 -- | Make an arrow type
666 mkFunTy :: Type -> Type -> Type
667 mkFunTy arg res = FunTy arg res
668
669 -- | Make nested arrow types
670 mkFunTys :: [Type] -> Type -> Type
671 mkFunTys tys ty = foldr mkFunTy ty tys
672
673 mkForAllTy :: TyVarBinder -> Type -> Type
674 mkForAllTy = ForAllTy
675
676 -- | Wraps foralls over the type using the provided 'TyVar's from left to right
677 mkForAllTys :: [TyVarBinder] -> Type -> Type
678 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
679
680 mkPiTy :: TyBinder -> Type -> Type
681 mkPiTy (Anon ty1) ty2 = FunTy ty1 ty2
682 mkPiTy (Named tvb) ty = ForAllTy tvb ty
683
684 mkPiTys :: [TyBinder] -> Type -> Type
685 mkPiTys tbs ty = foldr mkPiTy ty tbs
686
687 -- | Does this type classify a core (unlifted) Coercion?
688 -- At either role nominal or reprsentational
689 -- (t1 ~# t2) or (t1 ~R# t2)
690 isCoercionType :: Type -> Bool
691 isCoercionType (TyConApp tc tys)
692 | (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
693 , length tys == 4
694 = True
695 isCoercionType _ = False
696
697
698 -- | Create the plain type constructor type which has been applied to no type arguments at all.
699 mkTyConTy :: TyCon -> Type
700 mkTyConTy tycon = TyConApp tycon []
701
702 {-
703 Some basic functions, put here to break loops eg with the pretty printer
704 -}
705
706 -- | This version considers Constraint to be distinct from *.
707 isLiftedTypeKind :: Kind -> Bool
708 isLiftedTypeKind ki | Just ki' <- coreView ki = isLiftedTypeKind ki'
709 isLiftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
710 = tc `hasKey` tYPETyConKey
711 && ptr_rep `hasKey` ptrRepLiftedDataConKey
712 isLiftedTypeKind _ = False
713
714 isUnliftedTypeKind :: Kind -> Bool
715 isUnliftedTypeKind ki | Just ki' <- coreView ki = isUnliftedTypeKind ki'
716 isUnliftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
717 | tc `hasKey` tYPETyConKey
718 , ptr_rep `hasKey` ptrRepLiftedDataConKey
719 = False
720 isUnliftedTypeKind (TyConApp tc [arg])
721 = tc `hasKey` tYPETyConKey && isEmptyVarSet (tyCoVarsOfType arg)
722 -- all other possibilities are unlifted
723 isUnliftedTypeKind _ = False
724
725 -- | Is this the type 'RuntimeRep'?
726 isRuntimeRepTy :: Type -> Bool
727 isRuntimeRepTy ty | Just ty' <- coreView ty = isRuntimeRepTy ty'
728 isRuntimeRepTy (TyConApp tc []) = tc `hasKey` runtimeRepTyConKey
729 isRuntimeRepTy _ = False
730
731 -- | Is this a type of kind RuntimeRep? (e.g. PtrRep)
732 isRuntimeRepKindedTy :: Type -> Bool
733 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
734
735 -- | Is a tyvar of type 'RuntimeRep'?
736 isRuntimeRepVar :: TyVar -> Bool
737 isRuntimeRepVar = isRuntimeRepTy . tyVarKind
738
739 -- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
740 -- dropping 'PtrRep arguments of unboxed tuple TyCon applications:
741 --
742 -- dropRuntimeRepArgs [ 'PtrRepLifted, 'PtrRepUnlifted
743 -- , String, Int# ] == [String, Int#]
744 --
745 dropRuntimeRepArgs :: [Type] -> [Type]
746 dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
747
748 {-
749 %************************************************************************
750 %* *
751 Coercions
752 %* *
753 %************************************************************************
754 -}
755
756 -- | A 'Coercion' is concrete evidence of the equality/convertibility
757 -- of two types.
758
759 -- If you edit this type, you may need to update the GHC formalism
760 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
761 data Coercion
762 -- Each constructor has a "role signature", indicating the way roles are
763 -- propagated through coercions.
764 -- - P, N, and R stand for coercions of the given role
765 -- - e stands for a coercion of a specific unknown role
766 -- (think "role polymorphism")
767 -- - "e" stands for an explicit role parameter indicating role e.
768 -- - _ stands for a parameter that is not a Role or Coercion.
769
770 -- These ones mirror the shape of types
771 = -- Refl :: "e" -> _ -> e
772 Refl Role Type -- See Note [Refl invariant]
773 -- Invariant: applications of (Refl T) to a bunch of identity coercions
774 -- always show up as Refl.
775 -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
776
777 -- Applications of (Refl T) to some coercions, at least one of
778 -- which is NOT the identity, show up as TyConAppCo.
779 -- (They may not be fully saturated however.)
780 -- ConAppCo coercions (like all coercions other than Refl)
781 -- are NEVER the identity.
782
783 -- Use (Refl Representational _), not (SubCo (Refl Nominal _))
784
785 -- These ones simply lift the correspondingly-named
786 -- Type constructors into Coercions
787
788 -- TyConAppCo :: "e" -> _ -> ?? -> e
789 -- See Note [TyConAppCo roles]
790 | TyConAppCo Role TyCon [Coercion] -- lift TyConApp
791 -- The TyCon is never a synonym;
792 -- we expand synonyms eagerly
793 -- But it can be a type function
794
795 | AppCo Coercion CoercionN -- lift AppTy
796 -- AppCo :: e -> N -> e
797
798 -- See Note [Forall coercions]
799 | ForAllCo TyVar KindCoercion Coercion
800 -- ForAllCo :: _ -> N -> e -> e
801
802 -- These are special
803 | CoVarCo CoVar -- :: _ -> (N or R)
804 -- result role depends on the tycon of the variable's type
805
806 -- AxiomInstCo :: e -> _ -> [N] -> e
807 | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
808 -- See also [CoAxiom index]
809 -- The coercion arguments always *precisely* saturate
810 -- arity of (that branch of) the CoAxiom. If there are
811 -- any left over, we use AppCo.
812 -- See [Coercion axioms applied to coercions]
813
814 | UnivCo UnivCoProvenance Role Type Type
815 -- :: _ -> "e" -> _ -> _ -> e
816
817 | SymCo Coercion -- :: e -> e
818 | TransCo Coercion Coercion -- :: e -> e -> e
819
820 -- The number coercions should match exactly the expectations
821 -- of the CoAxiomRule (i.e., the rule is fully saturated).
822 | AxiomRuleCo CoAxiomRule [Coercion]
823
824 | NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
825 -- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
826 -- Using NthCo on a ForAllCo gives an N coercion always
827 -- See Note [NthCo and newtypes]
828
829 | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
830 -- :: _ -> N -> N
831 | InstCo Coercion CoercionN
832 -- :: e -> N -> e
833 -- See Note [InstCo roles]
834
835 -- Coherence applies a coercion to the left-hand type of another coercion
836 -- See Note [Coherence]
837 | CoherenceCo Coercion KindCoercion
838 -- :: e -> N -> e
839
840 -- Extract a kind coercion from a (heterogeneous) type coercion
841 -- NB: all kind coercions are Nominal
842 | KindCo Coercion
843 -- :: e -> N
844
845 | SubCo CoercionN -- Turns a ~N into a ~R
846 -- :: N -> R
847
848 deriving Data.Data
849
850 type CoercionN = Coercion -- always nominal
851 type CoercionR = Coercion -- always representational
852 type CoercionP = Coercion -- always phantom
853 type KindCoercion = CoercionN -- always nominal
854
855 -- If you edit this type, you may need to update the GHC formalism
856 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
857 data LeftOrRight = CLeft | CRight
858 deriving( Eq, Data.Data )
859
860 instance Binary LeftOrRight where
861 put_ bh CLeft = putByte bh 0
862 put_ bh CRight = putByte bh 1
863
864 get bh = do { h <- getByte bh
865 ; case h of
866 0 -> return CLeft
867 _ -> return CRight }
868
869 pickLR :: LeftOrRight -> (a,a) -> a
870 pickLR CLeft (l,_) = l
871 pickLR CRight (_,r) = r
872
873
874 {-
875 Note [Refl invariant]
876 ~~~~~~~~~~~~~~~~~~~~~
877 Invariant 1:
878
879 Coercions have the following invariant
880 Refl is always lifted as far as possible.
881
882 You might think that a consequencs is:
883 Every identity coercions has Refl at the root
884
885 But that's not quite true because of coercion variables. Consider
886 g where g :: Int~Int
887 Left h where h :: Maybe Int ~ Maybe Int
888 etc. So the consequence is only true of coercions that
889 have no coercion variables.
890
891 Note [Coercion axioms applied to coercions]
892 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
893 The reason coercion axioms can be applied to coercions and not just
894 types is to allow for better optimization. There are some cases where
895 we need to be able to "push transitivity inside" an axiom in order to
896 expose further opportunities for optimization.
897
898 For example, suppose we have
899
900 C a : t[a] ~ F a
901 g : b ~ c
902
903 and we want to optimize
904
905 sym (C b) ; t[g] ; C c
906
907 which has the kind
908
909 F b ~ F c
910
911 (stopping through t[b] and t[c] along the way).
912
913 We'd like to optimize this to just F g -- but how? The key is
914 that we need to allow axioms to be instantiated by *coercions*,
915 not just by types. Then we can (in certain cases) push
916 transitivity inside the axiom instantiations, and then react
917 opposite-polarity instantiations of the same axiom. In this
918 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
919 obtain the substitution a |-> g (note this operation is sort
920 of the dual of lifting!) and hence end up with
921
922 C g : t[b] ~ F c
923
924 which indeed has the same kind as t[g] ; C c.
925
926 Now we have
927
928 sym (C b) ; C g
929
930 which can be optimized to F g.
931
932 Note [CoAxiom index]
933 ~~~~~~~~~~~~~~~~~~~~
934 A CoAxiom has 1 or more branches. Each branch has contains a list
935 of the free type variables in that branch, the LHS type patterns,
936 and the RHS type for that branch. When we apply an axiom to a list
937 of coercions, we must choose which branch of the axiom we wish to
938 use, as the different branches may have different numbers of free
939 type variables. (The number of type patterns is always the same
940 among branches, but that doesn't quite concern us here.)
941
942 The Int in the AxiomInstCo constructor is the 0-indexed number
943 of the chosen branch.
944
945 Note [Forall coercions]
946 ~~~~~~~~~~~~~~~~~~~~~~~
947 Constructing coercions between forall-types can be a bit tricky,
948 because the kinds of the bound tyvars can be different.
949
950 The typing rule is:
951
952
953 kind_co : k1 ~ k2
954 tv1:k1 |- co : t1 ~ t2
955 -------------------------------------------------------------------
956 ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
957 all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
958
959 First, the TyVar stored in a ForAllCo is really an optimisation: this field
960 should be a Name, as its kind is redundant. Thinking of the field as a Name
961 is helpful in understanding what a ForAllCo means.
962
963 The idea is that kind_co gives the two kinds of the tyvar. See how, in the
964 conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
965
966 Of course, a type variable can't have different kinds at the same time. So,
967 we arbitrarily prefer the first kind when using tv1 in the inner coercion
968 co, which shows that t1 equals t2.
969
970 The last wrinkle is that we need to fix the kinds in the conclusion. In
971 t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
972 the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
973 (tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
974 mentions the same name with different kinds, but it *is* well-kinded, noting
975 that `(tv1:k2) |> sym kind_co` has kind k1.
976
977 This all really would work storing just a Name in the ForAllCo. But we can't
978 add Names to, e.g., VarSets, and there generally is just an impedence mismatch
979 in a bunch of places. So we use tv1. When we need tv2, we can use
980 setTyVarKind.
981
982 Note [Coherence]
983 ~~~~~~~~~~~~~~~~
984 The Coherence typing rule is thus:
985
986 g1 : s ~ t s : k1 g2 : k1 ~ k2
987 ------------------------------------
988 CoherenceCo g1 g2 : (s |> g2) ~ t
989
990 While this looks (and is) unsymmetric, a combination of other coercion
991 combinators can make the symmetric version.
992
993 For role information, see Note [Roles and kind coercions].
994
995 Note [Predicate coercions]
996 ~~~~~~~~~~~~~~~~~~~~~~~~~~
997 Suppose we have
998 g :: a~b
999 How can we coerce between types
1000 ([c]~a) => [a] -> c
1001 and
1002 ([c]~b) => [b] -> c
1003 where the equality predicate *itself* differs?
1004
1005 Answer: we simply treat (~) as an ordinary type constructor, so these
1006 types really look like
1007
1008 ((~) [c] a) -> [a] -> c
1009 ((~) [c] b) -> [b] -> c
1010
1011 So the coercion between the two is obviously
1012
1013 ((~) [c] g) -> [g] -> c
1014
1015 Another way to see this to say that we simply collapse predicates to
1016 their representation type (see Type.coreView and Type.predTypeRep).
1017
1018 This collapse is done by mkPredCo; there is no PredCo constructor
1019 in Coercion. This is important because we need Nth to work on
1020 predicates too:
1021 Nth 1 ((~) [c] g) = g
1022 See Simplify.simplCoercionF, which generates such selections.
1023
1024 Note [Roles]
1025 ~~~~~~~~~~~~
1026 Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
1027 in Trac #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
1028 http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
1029
1030 Here is one way to phrase the problem:
1031
1032 Given:
1033 newtype Age = MkAge Int
1034 type family F x
1035 type instance F Age = Bool
1036 type instance F Int = Char
1037
1038 This compiles down to:
1039 axAge :: Age ~ Int
1040 axF1 :: F Age ~ Bool
1041 axF2 :: F Int ~ Char
1042
1043 Then, we can make:
1044 (sym (axF1) ; F axAge ; axF2) :: Bool ~ Char
1045
1046 Yikes!
1047
1048 The solution is _roles_, as articulated in "Generative Type Abstraction and
1049 Type-level Computation" (POPL 2010), available at
1050 http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf
1051
1052 The specification for roles has evolved somewhat since that paper. For the
1053 current full details, see the documentation in docs/core-spec. Here are some
1054 highlights.
1055
1056 We label every equality with a notion of type equivalence, of which there are
1057 three options: Nominal, Representational, and Phantom. A ground type is
1058 nominally equivalent only with itself. A newtype (which is considered a ground
1059 type in Haskell) is representationally equivalent to its representation.
1060 Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
1061 to denote the equivalences.
1062
1063 The axioms above would be:
1064 axAge :: Age ~R Int
1065 axF1 :: F Age ~N Bool
1066 axF2 :: F Age ~N Char
1067
1068 Then, because transitivity applies only to coercions proving the same notion
1069 of equivalence, the above construction is impossible.
1070
1071 However, there is still an escape hatch: we know that any two types that are
1072 nominally equivalent are representationally equivalent as well. This is what
1073 the form SubCo proves -- it "demotes" a nominal equivalence into a
1074 representational equivalence. So, it would seem the following is possible:
1075
1076 sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG
1077
1078 What saves us here is that the arguments to a type function F, lifted into a
1079 coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
1080 we are safe.
1081
1082 Roles are attached to parameters to TyCons. When lifting a TyCon into a
1083 coercion (through TyConAppCo), we need to ensure that the arguments to the
1084 TyCon respect their roles. For example:
1085
1086 data T a b = MkT a (F b)
1087
1088 If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
1089 that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
1090 the type function F branches on b's *name*, not representation. So, we say
1091 that 'a' has role Representational and 'b' has role Nominal. The third role,
1092 Phantom, is for parameters not used in the type's definition. Given the
1093 following definition
1094
1095 data Q a = MkQ Int
1096
1097 the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
1098 can construct the coercion Bool ~P Char (using UnivCo).
1099
1100 See the paper cited above for more examples and information.
1101
1102 Note [TyConAppCo roles]
1103 ~~~~~~~~~~~~~~~~~~~~~~~
1104 The TyConAppCo constructor has a role parameter, indicating the role at
1105 which the coercion proves equality. The choice of this parameter affects
1106 the required roles of the arguments of the TyConAppCo. To help explain
1107 it, assume the following definition:
1108
1109 type instance F Int = Bool -- Axiom axF : F Int ~N Bool
1110 newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
1111 data Foo a = MkFoo a -- Role on Foo's parameter is Representational
1112
1113 TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
1114 For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
1115 So that Foo Age ~N Foo Int does *not* hold.
1116
1117 TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
1118 TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
1119 For (TyConAppCo Representational), all arguments must have the roles
1120 corresponding to the result of tyConRoles on the TyCon. This is the
1121 whole point of having roles on the TyCon to begin with. So, we can
1122 have Foo Age ~R Foo Int, if Foo's parameter has role R.
1123
1124 If a Representational TyConAppCo is over-saturated (which is otherwise fine),
1125 the spill-over arguments must all be at Nominal. This corresponds to the
1126 behavior for AppCo.
1127
1128 TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
1129 All arguments must have role Phantom. This one isn't strictly
1130 necessary for soundness, but this choice removes ambiguity.
1131
1132 The rules here dictate the roles of the parameters to mkTyConAppCo
1133 (should be checked by Lint).
1134
1135 Note [NthCo and newtypes]
1136 ~~~~~~~~~~~~~~~~~~~~~~~~~
1137 Suppose we have
1138
1139 newtype N a = MkN Int
1140 type role N representational
1141
1142 This yields axiom
1143
1144 NTCo:N :: forall a. N a ~R Int
1145
1146 We can then build
1147
1148 co :: forall a b. N a ~R N b
1149 co = NTCo:N a ; sym (NTCo:N b)
1150
1151 for any `a` and `b`. Because of the role annotation on N, if we use
1152 NthCo, we'll get out a representational coercion. That is:
1153
1154 NthCo 0 co :: forall a b. a ~R b
1155
1156 Yikes! Clearly, this is terrible. The solution is simple: forbid
1157 NthCo to be used on newtypes if the internal coercion is representational.
1158
1159 This is not just some corner case discovered by a segfault somewhere;
1160 it was discovered in the proof of soundness of roles and described
1161 in the "Safe Coercions" paper (ICFP '14).
1162
1163 Note [InstCo roles]
1164 ~~~~~~~~~~~~~~~~~~~
1165 Here is (essentially) the typing rule for InstCo:
1166
1167 g :: (forall a. t1) ~r (forall a. t2)
1168 w :: s1 ~N s2
1169 ------------------------------- InstCo
1170 InstCo g w :: (t1 [a |-> s1]) ~r (t2 [a |-> s2])
1171
1172 Note that the Coercion w *must* be nominal. This is necessary
1173 because the variable a might be used in a "nominal position"
1174 (that is, a place where role inference would require a nominal
1175 role) in t1 or t2. If we allowed w to be representational, we
1176 could get bogus equalities.
1177
1178 A more nuanced treatment might be able to relax this condition
1179 somewhat, by checking if t1 and/or t2 use their bound variables
1180 in nominal ways. If not, having w be representational is OK.
1181
1182
1183 %************************************************************************
1184 %* *
1185 UnivCoProvenance
1186 %* *
1187 %************************************************************************
1188
1189 A UnivCo is a coercion whose proof does not directly express its role
1190 and kind (indeed for some UnivCos, like UnsafeCoerceProv, there /is/
1191 no proof).
1192
1193 The different kinds of UnivCo are described by UnivCoProvenance. Really
1194 each is entirely separate, but they all share the need to represent their
1195 role and kind, which is done in the UnivCo constructor.
1196
1197 -}
1198
1199 -- | For simplicity, we have just one UnivCo that represents a coercion from
1200 -- some type to some other type, with (in general) no restrictions on the
1201 -- type. The UnivCoProvenance specifies more exactly what the coercion really
1202 -- is and why a program should (or shouldn't!) trust the coercion.
1203 -- It is reasonable to consider each constructor of 'UnivCoProvenance'
1204 -- as a totally independent coercion form; their only commonality is
1205 -- that they don't tell you what types they coercion between. (That info
1206 -- is in the 'UnivCo' constructor of 'Coercion'.
1207 data UnivCoProvenance
1208 = UnsafeCoerceProv -- ^ From @unsafeCoerce#@. These are unsound.
1209
1210 | PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
1211 -- roled coercions
1212
1213 | ProofIrrelProv KindCoercion -- ^ From the fact that any two coercions are
1214 -- considered equivalent. See Note [ProofIrrelProv].
1215 -- Can be used in Nominal or Representational coercions
1216
1217 | PluginProv String -- ^ From a plugin, which asserts that this coercion
1218 -- is sound. The string is for the use of the plugin.
1219
1220 | HoleProv CoercionHole -- ^ See Note [Coercion holes]
1221 deriving Data.Data
1222
1223 instance Outputable UnivCoProvenance where
1224 ppr UnsafeCoerceProv = text "(unsafeCoerce#)"
1225 ppr (PhantomProv _) = text "(phantom)"
1226 ppr (ProofIrrelProv _) = text "(proof irrel.)"
1227 ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
1228 ppr (HoleProv hole) = parens (text "hole" <> ppr hole)
1229
1230 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
1231 data CoercionHole
1232 = CoercionHole { chUnique :: Unique -- ^ used only for debugging
1233 , chCoercion :: IORef (Maybe Coercion)
1234 }
1235
1236 instance Data.Data CoercionHole where
1237 -- don't traverse?
1238 toConstr _ = abstractConstr "CoercionHole"
1239 gunfold _ _ = error "gunfold"
1240 dataTypeOf _ = mkNoRepType "CoercionHole"
1241
1242 instance Outputable CoercionHole where
1243 ppr (CoercionHole u _) = braces (ppr u)
1244
1245
1246 {- Note [Phantom coercions]
1247 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1248 Consider
1249 data T a = T1 | T2
1250 Then we have
1251 T s ~R T t
1252 for any old s,t. The witness for this is (TyConAppCo T Rep co),
1253 where (co :: s ~P t) is a phantom coercion built with PhantomProv.
1254 The role of the UnivCo is always Phantom. The Coercion stored is the
1255 (nominal) kind coercion between the types
1256 kind(s) ~N kind (t)
1257
1258 Note [Coercion holes]
1259 ~~~~~~~~~~~~~~~~~~~~~~~~
1260 During typechecking, constraint solving for type classes works by
1261 - Generate an evidence Id, d7 :: Num a
1262 - Wrap it in a Wanted constraint, [W] d7 :: Num a
1263 - Use the evidence Id where the evidence is needed
1264 - Solve the constraint later
1265 - When solved, add an enclosing let-binding let d7 = .... in ....
1266 which actually binds d7 to the (Num a) evidence
1267
1268 For equality constraints we use a different strategy. See Note [The
1269 equality types story] in TysPrim for background on equality constraints.
1270 - For boxed equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
1271 like type classes above. (Indeed, boxed equality constraints *are* classes.)
1272 - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
1273 we use a different plan
1274
1275 For unboxed equalities:
1276 - Generate a CoercionHole, a mutable variable just like a unification
1277 variable
1278 - Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest
1279 - Use the CoercionHole in a Coercion, via HoleProv
1280 - Solve the constraint later
1281 - When solved, fill in the CoercionHole by side effect, instead of
1282 doing the let-binding thing
1283
1284 The main reason for all this is that there may be no good place to let-bind
1285 the evidence for unboxed equalities:
1286 - We emit constraints for kind coercions, to be used
1287 to cast a type's kind. These coercions then must be used in types. Because
1288 they might appear in a top-level type, there is no place to bind these
1289 (unlifted) coercions in the usual way.
1290
1291 - A coercion for (forall a. t1) ~ forall a. t2) will look like
1292 forall a. (coercion for t1~t2)
1293 But the coercion for (t1~t2) may mention 'a', and we don't have let-bindings
1294 within coercions. We could add them, but coercion holes are easier.
1295
1296 Other notes about HoleCo:
1297
1298 * INVARIANT: CoercionHole and HoleProv are used only during type checking,
1299 and should never appear in Core. Just like unification variables; a Type
1300 can contain a TcTyVar, but only during type checking. If, one day, we
1301 use type-level information to separate out forms that can appear during
1302 type-checking vs forms that can appear in core proper, holes in Core will
1303 be ruled out.
1304
1305 * The Unique carried with a coercion hole is used solely for debugging.
1306
1307 * Coercion holes can be compared for equality only like other coercions:
1308 only by looking at the types coerced.
1309
1310 * We don't use holes for other evidence because other evidence wants to
1311 be /shared/. But coercions are entirely erased, so there's little
1312 benefit to sharing.
1313
1314 Note [ProofIrrelProv]
1315 ~~~~~~~~~~~~~~~~~~~~~
1316 A ProofIrrelProv is a coercion between coercions. For example:
1317
1318 data G a where
1319 MkG :: G Bool
1320
1321 In core, we get
1322
1323 G :: * -> *
1324 MkG :: forall (a :: *). (a ~ Bool) -> G a
1325
1326 Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
1327 a proof that ('MkG co1 a1) ~ ('MkG co2 a2). This will have to be
1328
1329 TyConAppCo Nominal MkG [co3, co4]
1330 where
1331 co3 :: co1 ~ co2
1332 co4 :: a1 ~ a2
1333
1334 Note that
1335 co1 :: a1 ~ Bool
1336 co2 :: a2 ~ Bool
1337
1338 Here,
1339 co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2)
1340 where
1341 co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
1342 co5 = TyConAppCo Nominal (~) [<*>, <*>, co4, <Bool>]
1343
1344
1345 %************************************************************************
1346 %* *
1347 Free variables of types and coercions
1348 %* *
1349 %************************************************************************
1350 -}
1351
1352 {- Note [Free variables of types]
1353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1354 The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
1355 a VarSet that is closed over the types of its variables. More precisely,
1356 if S = tyCoVarsOfType( t )
1357 and (a:k) is in S
1358 then tyCoVarsOftype( k ) is a subset of S
1359
1360 Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.
1361
1362 We could /not/ close over the kinds of the variable occurrences, and
1363 instead do so at call sites, but it seems that we always want to do
1364 so, so it's easiest to do it here.
1365 -}
1366
1367
1368 -- | Returns free variables of a type, including kind variables as
1369 -- a non-deterministic set. For type synonyms it does /not/ expand the
1370 -- synonym.
1371 tyCoVarsOfType :: Type -> TyCoVarSet
1372 -- See Note [Free variables of types]
1373 tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty
1374
1375 -- | `tyVarsOfType` that returns free variables of a type in a deterministic
1376 -- set. For explanation of why using `VarSet` is not deterministic see
1377 -- Note [Deterministic FV] in FV.
1378 tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
1379 -- See Note [Free variables of types]
1380 tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty
1381
1382 -- | `tyVarsOfType` that returns free variables of a type in deterministic
1383 -- order. For explanation of why using `VarSet` is not deterministic see
1384 -- Note [Deterministic FV] in FV.
1385 tyCoVarsOfTypeList :: Type -> [TyCoVar]
1386 -- See Note [Free variables of types]
1387 tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
1388
1389 -- | The worker for `tyVarsOfType` and `tyVarsOfTypeList`.
1390 -- The previous implementation used `unionVarSet` which is O(n+m) and can
1391 -- make the function quadratic.
1392 -- It's exported, so that it can be composed with
1393 -- other functions that compute free variables.
1394 -- See Note [FV naming conventions] in FV.
1395 --
1396 -- Eta-expanded because that makes it run faster (apparently)
1397 -- See Note [FV eta expansion] in FV for explanation.
1398 tyCoFVsOfType :: Type -> FV
1399 -- See Note [Free variables of types]
1400 tyCoFVsOfType (TyVarTy v) a b c = (unitFV v `unionFV` tyCoFVsOfType (tyVarKind v)) a b c
1401 tyCoFVsOfType (TyConApp _ tys) a b c = tyCoFVsOfTypes tys a b c
1402 tyCoFVsOfType (LitTy {}) a b c = emptyFV a b c
1403 tyCoFVsOfType (AppTy fun arg) a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c
1404 tyCoFVsOfType (FunTy arg res) a b c = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) a b c
1405 tyCoFVsOfType (ForAllTy bndr ty) a b c = tyCoFVsBndr bndr (tyCoFVsOfType ty) a b c
1406 tyCoFVsOfType (CastTy ty co) a b c = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) a b c
1407 tyCoFVsOfType (CoercionTy co) a b c = tyCoFVsOfCo co a b c
1408
1409 tyCoFVsBndr :: TyVarBinder -> FV -> FV
1410 -- Free vars of (forall b. <thing with fvs>)
1411 tyCoFVsBndr (TvBndr tv _) fvs = (delFV tv fvs)
1412 `unionFV` tyCoFVsOfType (tyVarKind tv)
1413
1414 -- | Returns free variables of types, including kind variables as
1415 -- a non-deterministic set. For type synonyms it does /not/ expand the
1416 -- synonym.
1417 tyCoVarsOfTypes :: [Type] -> TyCoVarSet
1418 -- See Note [Free variables of types]
1419 tyCoVarsOfTypes tys = fvVarSet $ tyCoFVsOfTypes tys
1420
1421 -- | Returns free variables of types, including kind variables as
1422 -- a deterministic set. For type synonyms it does /not/ expand the
1423 -- synonym.
1424 tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
1425 -- See Note [Free variables of types]
1426 tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys
1427
1428 -- | Returns free variables of types, including kind variables as
1429 -- a deterministically ordered list. For type synonyms it does /not/ expand the
1430 -- synonym.
1431 tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
1432 -- See Note [Free variables of types]
1433 tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
1434
1435 tyCoFVsOfTypes :: [Type] -> FV
1436 -- See Note [Free variables of types]
1437 tyCoFVsOfTypes (ty:tys) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfTypes tys) fv_cand in_scope acc
1438 tyCoFVsOfTypes [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
1439
1440 tyCoVarsOfCo :: Coercion -> TyCoVarSet
1441 -- See Note [Free variables of types]
1442 tyCoVarsOfCo co = fvVarSet $ tyCoFVsOfCo co
1443
1444 -- | Get a deterministic set of the vars free in a coercion
1445 tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
1446 -- See Note [Free variables of types]
1447 tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co
1448
1449 tyCoVarsOfCoList :: Coercion -> [TyCoVar]
1450 -- See Note [Free variables of types]
1451 tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
1452
1453 tyCoFVsOfCo :: Coercion -> FV
1454 -- Extracts type and coercion variables from a coercion
1455 -- See Note [Free variables of types]
1456 tyCoFVsOfCo (Refl _ ty) fv_cand in_scope acc = tyCoFVsOfType ty fv_cand in_scope acc
1457 tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
1458 tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
1459 = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
1460 tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
1461 = (delFV tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
1462 tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
1463 = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
1464 tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
1465 tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
1466 = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1
1467 `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
1468 tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1469 tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
1470 tyCoFVsOfCo (NthCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1471 tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1472 tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
1473 tyCoFVsOfCo (CoherenceCo c1 c2) fv_cand in_scope acc = (tyCoFVsOfCo c1 `unionFV` tyCoFVsOfCo c2) fv_cand in_scope acc
1474 tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1475 tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1476 tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
1477
1478 tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
1479 tyCoVarsOfProv prov = fvVarSet $ tyCoFVsOfProv prov
1480
1481 tyCoFVsOfProv :: UnivCoProvenance -> FV
1482 tyCoFVsOfProv UnsafeCoerceProv fv_cand in_scope acc = emptyFV fv_cand in_scope acc
1483 tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1484 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
1485 tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
1486 tyCoFVsOfProv (HoleProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
1487
1488 tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
1489 tyCoVarsOfCos cos = fvVarSet $ tyCoFVsOfCos cos
1490
1491 tyCoFVsOfCos :: [Coercion] -> FV
1492 tyCoFVsOfCos [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
1493 tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCos cos) fv_cand in_scope acc
1494
1495 coVarsOfType :: Type -> CoVarSet
1496 coVarsOfType (TyVarTy v) = coVarsOfType (tyVarKind v)
1497 coVarsOfType (TyConApp _ tys) = coVarsOfTypes tys
1498 coVarsOfType (LitTy {}) = emptyVarSet
1499 coVarsOfType (AppTy fun arg) = coVarsOfType fun `unionVarSet` coVarsOfType arg
1500 coVarsOfType (FunTy arg res) = coVarsOfType arg `unionVarSet` coVarsOfType res
1501 coVarsOfType (ForAllTy (TvBndr tv _) ty)
1502 = (coVarsOfType ty `delVarSet` tv)
1503 `unionVarSet` coVarsOfType (tyVarKind tv)
1504 coVarsOfType (CastTy ty co) = coVarsOfType ty `unionVarSet` coVarsOfCo co
1505 coVarsOfType (CoercionTy co) = coVarsOfCo co
1506
1507 coVarsOfTypes :: [Type] -> TyCoVarSet
1508 coVarsOfTypes tys = mapUnionVarSet coVarsOfType tys
1509
1510 coVarsOfCo :: Coercion -> CoVarSet
1511 -- Extract *coercion* variables only. Tiresome to repeat the code, but easy.
1512 coVarsOfCo (Refl _ ty) = coVarsOfType ty
1513 coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args
1514 coVarsOfCo (AppCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg
1515 coVarsOfCo (ForAllCo tv kind_co co)
1516 = coVarsOfCo co `delVarSet` tv `unionVarSet` coVarsOfCo kind_co
1517 coVarsOfCo (CoVarCo v) = unitVarSet v `unionVarSet` coVarsOfType (varType v)
1518 coVarsOfCo (AxiomInstCo _ _ args) = coVarsOfCos args
1519 coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2]
1520 coVarsOfCo (SymCo co) = coVarsOfCo co
1521 coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
1522 coVarsOfCo (NthCo _ co) = coVarsOfCo co
1523 coVarsOfCo (LRCo _ co) = coVarsOfCo co
1524 coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg
1525 coVarsOfCo (CoherenceCo c1 c2) = coVarsOfCos [c1, c2]
1526 coVarsOfCo (KindCo co) = coVarsOfCo co
1527 coVarsOfCo (SubCo co) = coVarsOfCo co
1528 coVarsOfCo (AxiomRuleCo _ cs) = coVarsOfCos cs
1529
1530 coVarsOfProv :: UnivCoProvenance -> CoVarSet
1531 coVarsOfProv UnsafeCoerceProv = emptyVarSet
1532 coVarsOfProv (PhantomProv co) = coVarsOfCo co
1533 coVarsOfProv (ProofIrrelProv co) = coVarsOfCo co
1534 coVarsOfProv (PluginProv _) = emptyVarSet
1535 coVarsOfProv (HoleProv _) = emptyVarSet
1536
1537 coVarsOfCos :: [Coercion] -> CoVarSet
1538 coVarsOfCos cos = mapUnionVarSet coVarsOfCo cos
1539
1540 -- | Add the kind variables free in the kinds of the tyvars in the given set.
1541 -- Returns a non-deterministic set.
1542 closeOverKinds :: TyVarSet -> TyVarSet
1543 closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUFM
1544 -- It's OK to use nonDetEltsUFM here because we immediately forget
1545 -- about the ordering by returning a set.
1546
1547 -- | Given a list of tyvars returns a deterministic FV computation that
1548 -- returns the given tyvars with the kind variables free in the kinds of the
1549 -- given tyvars.
1550 closeOverKindsFV :: [TyVar] -> FV
1551 closeOverKindsFV tvs =
1552 mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
1553
1554 -- | Add the kind variables free in the kinds of the tyvars in the given set.
1555 -- Returns a deterministically ordered list.
1556 closeOverKindsList :: [TyVar] -> [TyVar]
1557 closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
1558
1559 -- | Add the kind variables free in the kinds of the tyvars in the given set.
1560 -- Returns a deterministic set.
1561 closeOverKindsDSet :: DTyVarSet -> DTyVarSet
1562 closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
1563
1564 {-
1565 %************************************************************************
1566 %* *
1567 TyThing
1568 %* *
1569 %************************************************************************
1570
1571 Despite the fact that DataCon has to be imported via a hi-boot route,
1572 this module seems the right place for TyThing, because it's needed for
1573 funTyCon and all the types in TysPrim.
1574
1575 Note [ATyCon for classes]
1576 ~~~~~~~~~~~~~~~~~~~~~~~~~
1577 Both classes and type constructors are represented in the type environment
1578 as ATyCon. You can tell the difference, and get to the class, with
1579 isClassTyCon :: TyCon -> Bool
1580 tyConClass_maybe :: TyCon -> Maybe Class
1581 The Class and its associated TyCon have the same Name.
1582 -}
1583
1584 -- | A global typecheckable-thing, essentially anything that has a name.
1585 -- Not to be confused with a 'TcTyThing', which is also a typecheckable
1586 -- thing but in the *local* context. See 'TcEnv' for how to retrieve
1587 -- a 'TyThing' given a 'Name'.
1588 data TyThing
1589 = AnId Id
1590 | AConLike ConLike
1591 | ATyCon TyCon -- TyCons and classes; see Note [ATyCon for classes]
1592 | ACoAxiom (CoAxiom Branched)
1593
1594 instance Outputable TyThing where
1595 ppr = pprShortTyThing
1596
1597 pprShortTyThing :: TyThing -> SDoc
1598 -- c.f. PprTyThing.pprTyThing, which prints all the details
1599 pprShortTyThing thing
1600 = pprTyThingCategory thing <+> quotes (ppr (getName thing))
1601
1602 pprTyThingCategory :: TyThing -> SDoc
1603 pprTyThingCategory (ATyCon tc)
1604 | isClassTyCon tc = text "Class"
1605 | otherwise = text "Type constructor"
1606 pprTyThingCategory (ACoAxiom _) = text "Coercion axiom"
1607 pprTyThingCategory (AnId _) = text "Identifier"
1608 pprTyThingCategory (AConLike (RealDataCon _)) = text "Data constructor"
1609 pprTyThingCategory (AConLike (PatSynCon _)) = text "Pattern synonym"
1610
1611
1612 instance NamedThing TyThing where -- Can't put this with the type
1613 getName (AnId id) = getName id -- decl, because the DataCon instance
1614 getName (ATyCon tc) = getName tc -- isn't visible there
1615 getName (ACoAxiom cc) = getName cc
1616 getName (AConLike cl) = conLikeName cl
1617
1618 {-
1619 %************************************************************************
1620 %* *
1621 Substitutions
1622 Data type defined here to avoid unnecessary mutual recursion
1623 %* *
1624 %************************************************************************
1625 -}
1626
1627 -- | Type & coercion substitution
1628 --
1629 -- #tcvsubst_invariant#
1630 -- The following invariants must hold of a 'TCvSubst':
1631 --
1632 -- 1. The in-scope set is needed /only/ to
1633 -- guide the generation of fresh uniques
1634 --
1635 -- 2. In particular, the /kind/ of the type variables in
1636 -- the in-scope set is not relevant
1637 --
1638 -- 3. The substitution is only applied ONCE! This is because
1639 -- in general such application will not reach a fixed point.
1640 data TCvSubst
1641 = TCvSubst InScopeSet -- The in-scope type and kind variables
1642 TvSubstEnv -- Substitutes both type and kind variables
1643 CvSubstEnv -- Substitutes coercion variables
1644 -- See Note [Apply Once]
1645 -- and Note [Extending the TvSubstEnv]
1646 -- and Note [Substituting types and coercions]
1647 -- and Note [The substitution invariant]
1648
1649 -- | A substitution of 'Type's for 'TyVar's
1650 -- and 'Kind's for 'KindVar's
1651 type TvSubstEnv = TyVarEnv Type
1652 -- A TvSubstEnv is used both inside a TCvSubst (with the apply-once
1653 -- invariant discussed in Note [Apply Once]), and also independently
1654 -- in the middle of matching, and unification (see Types.Unify)
1655 -- So you have to look at the context to know if it's idempotent or
1656 -- apply-once or whatever
1657
1658 -- | A substitution of 'Coercion's for 'CoVar's
1659 type CvSubstEnv = CoVarEnv Coercion
1660
1661 {-
1662 Note [Apply Once]
1663 ~~~~~~~~~~~~~~~~~
1664 We use TCvSubsts to instantiate things, and we might instantiate
1665 forall a b. ty
1666 \with the types
1667 [a, b], or [b, a].
1668 So the substitution might go [a->b, b->a]. A similar situation arises in Core
1669 when we find a beta redex like
1670 (/\ a /\ b -> e) b a
1671 Then we also end up with a substitution that permutes type variables. Other
1672 variations happen to; for example [a -> (a, b)].
1673
1674 ****************************************************
1675 *** So a TCvSubst must be applied precisely once ***
1676 ****************************************************
1677
1678 A TCvSubst is not idempotent, but, unlike the non-idempotent substitution
1679 we use during unifications, it must not be repeatedly applied.
1680
1681 Note [Extending the TvSubstEnv]
1682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1683 See #tcvsubst_invariant# for the invariants that must hold.
1684
1685 This invariant allows a short-cut when the subst envs are empty:
1686 if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst)
1687 holds --- then (substTy subst ty) does nothing.
1688
1689 For example, consider:
1690 (/\a. /\b:(a~Int). ...b..) Int
1691 We substitute Int for 'a'. The Unique of 'b' does not change, but
1692 nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
1693
1694 This invariant has several crucial consequences:
1695
1696 * In substTyVarBndr, we need extend the TvSubstEnv
1697 - if the unique has changed
1698 - or if the kind has changed
1699
1700 * In substTyVar, we do not need to consult the in-scope set;
1701 the TvSubstEnv is enough
1702
1703 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
1704
1705 Note [Substituting types and coercions]
1706 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1707 Types and coercions are mutually recursive, and either may have variables
1708 "belonging" to the other. Thus, every time we wish to substitute in a
1709 type, we may also need to substitute in a coercion, and vice versa.
1710 However, the constructor used to create type variables is distinct from
1711 that of coercion variables, so we carry two VarEnvs in a TCvSubst. Note
1712 that it would be possible to use the CoercionTy constructor to combine
1713 these environments, but that seems like a false economy.
1714
1715 Note that the TvSubstEnv should *never* map a CoVar (built with the Id
1716 constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
1717 the range of the TvSubstEnv should *never* include a type headed with
1718 CoercionTy.
1719
1720 Note [The substitution invariant]
1721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1722 When calling (substTy subst ty) it should be the case that
1723 the in-scope set in the substitution is a superset of both:
1724
1725 * The free vars of the range of the substitution
1726 * The free vars of ty minus the domain of the substitution
1727
1728 If we want to substitute [a -> ty1, b -> ty2] I used to
1729 think it was enough to generate an in-scope set that includes
1730 fv(ty1,ty2). But that's not enough; we really should also take the
1731 free vars of the type we are substituting into! Example:
1732 (forall b. (a,b,x)) [a -> List b]
1733 Then if we use the in-scope set {b}, there is a danger we will rename
1734 the forall'd variable to 'x' by mistake, getting this:
1735 (forall x. (List b, x, x))
1736
1737 Breaking this invariant caused the bug from #11371.
1738 -}
1739
1740 emptyTvSubstEnv :: TvSubstEnv
1741 emptyTvSubstEnv = emptyVarEnv
1742
1743 emptyCvSubstEnv :: CvSubstEnv
1744 emptyCvSubstEnv = emptyVarEnv
1745
1746 composeTCvSubstEnv :: InScopeSet
1747 -> (TvSubstEnv, CvSubstEnv)
1748 -> (TvSubstEnv, CvSubstEnv)
1749 -> (TvSubstEnv, CvSubstEnv)
1750 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
1751 -- It assumes that both are idempotent.
1752 -- Typically, @env1@ is the refinement to a base substitution @env2@
1753 composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2)
1754 = ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2
1755 , cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 )
1756 -- First apply env1 to the range of env2
1757 -- Then combine the two, making sure that env1 loses if
1758 -- both bind the same variable; that's why env1 is the
1759 -- *left* argument to plusVarEnv, because the right arg wins
1760 where
1761 subst1 = TCvSubst in_scope tenv1 cenv1
1762
1763 -- | Composes two substitutions, applying the second one provided first,
1764 -- like in function composition.
1765 composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
1766 composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2)
1767 = TCvSubst is3 tenv3 cenv3
1768 where
1769 is3 = is1 `unionInScope` is2
1770 (tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2)
1771
1772 emptyTCvSubst :: TCvSubst
1773 emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv
1774
1775 mkEmptyTCvSubst :: InScopeSet -> TCvSubst
1776 mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv
1777
1778 isEmptyTCvSubst :: TCvSubst -> Bool
1779 -- See Note [Extending the TvSubstEnv]
1780 isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
1781
1782 mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
1783 mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv
1784
1785 mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
1786 -- ^ Make a TCvSubst with specified tyvar subst and empty covar subst
1787 mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv
1788
1789 getTvSubstEnv :: TCvSubst -> TvSubstEnv
1790 getTvSubstEnv (TCvSubst _ env _) = env
1791
1792 getCvSubstEnv :: TCvSubst -> CvSubstEnv
1793 getCvSubstEnv (TCvSubst _ _ env) = env
1794
1795 getTCvInScope :: TCvSubst -> InScopeSet
1796 getTCvInScope (TCvSubst in_scope _ _) = in_scope
1797
1798 -- | Returns the free variables of the types in the range of a substitution as
1799 -- a non-deterministic set.
1800 getTCvSubstRangeFVs :: TCvSubst -> VarSet
1801 getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
1802 = unionVarSet tenvFVs cenvFVs
1803 where
1804 tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv
1805 cenvFVs = tyCoVarsOfCos $ varEnvElts cenv
1806
1807 isInScope :: Var -> TCvSubst -> Bool
1808 isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
1809
1810 notElemTCvSubst :: Var -> TCvSubst -> Bool
1811 notElemTCvSubst v (TCvSubst _ tenv cenv)
1812 | isTyVar v
1813 = not (v `elemVarEnv` tenv)
1814 | otherwise
1815 = not (v `elemVarEnv` cenv)
1816
1817 setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
1818 setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv
1819
1820 setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
1821 setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv
1822
1823 zapTCvSubst :: TCvSubst -> TCvSubst
1824 zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv
1825
1826 extendTCvInScope :: TCvSubst -> Var -> TCvSubst
1827 extendTCvInScope (TCvSubst in_scope tenv cenv) var
1828 = TCvSubst (extendInScopeSet in_scope var) tenv cenv
1829
1830 extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
1831 extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars
1832 = TCvSubst (extendInScopeSetList in_scope vars) tenv cenv
1833
1834 extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
1835 extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
1836 = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
1837
1838 extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
1839 extendTCvSubst subst v ty
1840 | isTyVar v
1841 = extendTvSubst subst v ty
1842 | CoercionTy co <- ty
1843 = extendCvSubst subst v co
1844 | otherwise
1845 = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
1846
1847 extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
1848 extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
1849 = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
1850
1851 extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
1852 -- Adds a new tv -> tv mapping, /and/ extends the in-scope set
1853 extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv'
1854 = TCvSubst (extendInScopeSetSet in_scope new_in_scope)
1855 (extendVarEnv tenv tv (mkTyVarTy tv'))
1856 cenv
1857 where
1858 new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv'
1859
1860 extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
1861 extendCvSubst (TCvSubst in_scope tenv cenv) v co
1862 = TCvSubst in_scope tenv (extendVarEnv cenv v co)
1863
1864 extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
1865 extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv'
1866 = TCvSubst (extendInScopeSetSet in_scope new_in_scope)
1867 tenv
1868 (extendVarEnv cenv cv (mkCoVarCo cv'))
1869 where
1870 new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv'
1871
1872 extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
1873 -- Also extends the in-scope set
1874 extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
1875 = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
1876 (extendVarEnv tenv tv ty)
1877 cenv
1878
1879 extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
1880 extendTvSubstList subst tvs tys
1881 = foldl2 extendTvSubst subst tvs tys
1882
1883 unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
1884 -- Works when the ranges are disjoint
1885 unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
1886 = ASSERT( not (tenv1 `intersectsVarEnv` tenv2)
1887 && not (cenv1 `intersectsVarEnv` cenv2) )
1888 TCvSubst (in_scope1 `unionInScope` in_scope2)
1889 (tenv1 `plusVarEnv` tenv2)
1890 (cenv1 `plusVarEnv` cenv2)
1891
1892 -- mkTvSubstPrs and zipTvSubst generate the in-scope set from
1893 -- the types given; but it's just a thunk so with a bit of luck
1894 -- it'll never be evaluated
1895
1896 -- | Generates an in-scope set from the free variables in a list of types
1897 -- and a list of coercions
1898 mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
1899 mkTyCoInScopeSet tys cos
1900 = mkInScopeSet (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
1901
1902 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
1903 -- environment. No CoVars, please!
1904 zipTvSubst :: [TyVar] -> [Type] -> TCvSubst
1905 zipTvSubst tvs tys
1906 | debugIsOn
1907 , not (all isTyVar tvs) || length tvs /= length tys
1908 = pprTrace "zipTvSubst" (ppr tvs $$ ppr tys) emptyTCvSubst
1909 | otherwise
1910 = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv
1911 where
1912 tenv = zipTyEnv tvs tys
1913
1914 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
1915 -- environment. No TyVars, please!
1916 zipCvSubst :: [CoVar] -> [Coercion] -> TCvSubst
1917 zipCvSubst cvs cos
1918 | debugIsOn
1919 , not (all isCoVar cvs) || length cvs /= length cos
1920 = pprTrace "zipCvSubst" (ppr cvs $$ ppr cos) emptyTCvSubst
1921 | otherwise
1922 = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv
1923 where
1924 cenv = zipCoEnv cvs cos
1925
1926 -- | Generates the in-scope set for the 'TCvSubst' from the types in the
1927 -- incoming environment. No CoVars, please!
1928 mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst
1929 mkTvSubstPrs prs =
1930 ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs )
1931 mkTvSubst in_scope tenv
1932 where tenv = mkVarEnv prs
1933 in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs
1934 onlyTyVarsAndNoCoercionTy =
1935 and [ isTyVar tv && not (isCoercionTy ty)
1936 | (tv, ty) <- prs ]
1937
1938 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1939 zipTyEnv tyvars tys
1940 = ASSERT( all (not . isCoercionTy) tys )
1941 mkVarEnv (zipEqual "zipTyEnv" tyvars tys)
1942 -- There used to be a special case for when
1943 -- ty == TyVarTy tv
1944 -- (a not-uncommon case) in which case the substitution was dropped.
1945 -- But the type-tidier changes the print-name of a type variable without
1946 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
1947 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
1948 -- And it happened that t was the type variable of the class. Post-tiding,
1949 -- it got turned into {Foo t2}. The ext-core printer expanded this using
1950 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1951 -- and so generated a rep type mentioning t not t2.
1952 --
1953 -- Simplest fix is to nuke the "optimisation"
1954
1955 zipCoEnv :: [CoVar] -> [Coercion] -> CvSubstEnv
1956 zipCoEnv cvs cos = mkVarEnv (zipEqual "zipCoEnv" cvs cos)
1957
1958 instance Outputable TCvSubst where
1959 ppr (TCvSubst ins tenv cenv)
1960 = brackets $ sep[ text "TCvSubst",
1961 nest 2 (text "In scope:" <+> ppr ins),
1962 nest 2 (text "Type env:" <+> ppr tenv),
1963 nest 2 (text "Co env:" <+> ppr cenv) ]
1964
1965 {-
1966 %************************************************************************
1967 %* *
1968 Performing type or kind substitutions
1969 %* *
1970 %************************************************************************
1971
1972 Note [Sym and ForAllCo]
1973 ~~~~~~~~~~~~~~~~~~~~~~~
1974 In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
1975 how do we push sym into a ForAllCo? It's a little ugly.
1976
1977 Here is the typing rule:
1978
1979 h : k1 ~# k2
1980 (tv : k1) |- g : ty1 ~# ty2
1981 ----------------------------
1982 ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~#
1983 (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h]))
1984
1985 Here is what we want:
1986
1987 ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~#
1988 (ForAllTy (tv : k1) ty1)
1989
1990
1991 Because the kinds of the type variables to the right of the colon are the kinds
1992 coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h).
1993
1994 Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want
1995
1996 ForAllCo tv h' g' :
1997 (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~#
1998 (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h']))
1999
2000 We thus see that we want
2001
2002 g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h']
2003
2004 and thus g' = sym (g[tv |-> tv |> h']).
2005
2006 Putting it all together, we get this:
2007
2008 sym (ForAllCo tv h g)
2009 ==>
2010 ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
2011
2012 -}
2013
2014 -- | Type substitution, see 'zipTvSubst'
2015 substTyWith ::
2016 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2017 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2018 (?callStack :: CallStack) =>
2019 #endif
2020 [TyVar] -> [Type] -> Type -> Type
2021 -- Works only if the domain of the substitution is a
2022 -- superset of the type being substituted into
2023 substTyWith tvs tys = ASSERT( length tvs == length tys )
2024 substTy (zipTvSubst tvs tys)
2025
2026 -- | Type substitution, see 'zipTvSubst'. Disables sanity checks.
2027 -- The problems that the sanity checks in substTy catch are described in
2028 -- Note [The substitution invariant].
2029 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
2030 -- substTy and remove this function. Please don't use in new code.
2031 substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
2032 substTyWithUnchecked tvs tys
2033 = ASSERT( length tvs == length tys )
2034 substTyUnchecked (zipTvSubst tvs tys)
2035
2036 -- | Substitute tyvars within a type using a known 'InScopeSet'.
2037 -- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
2038 -- invariant]; specifically it should include the free vars of 'tys',
2039 -- and of 'ty' minus the domain of the subst.
2040 substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
2041 substTyWithInScope in_scope tvs tys ty =
2042 ASSERT( length tvs == length tys )
2043 substTy (mkTvSubst in_scope tenv) ty
2044 where tenv = zipTyEnv tvs tys
2045
2046 -- | Coercion substitution, see 'zipTvSubst'
2047 substCoWith ::
2048 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2049 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2050 (?callStack :: CallStack) =>
2051 #endif
2052 [TyVar] -> [Type] -> Coercion -> Coercion
2053 substCoWith tvs tys = ASSERT( length tvs == length tys )
2054 substCo (zipTvSubst tvs tys)
2055
2056 -- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
2057 -- The problems that the sanity checks in substCo catch are described in
2058 -- Note [The substitution invariant].
2059 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
2060 -- substCo and remove this function. Please don't use in new code.
2061 substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
2062 substCoWithUnchecked tvs tys
2063 = ASSERT( length tvs == length tys )
2064 substCoUnchecked (zipTvSubst tvs tys)
2065
2066
2067
2068 -- | Substitute covars within a type
2069 substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
2070 substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
2071
2072 -- | Type substitution, see 'zipTvSubst'
2073 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
2074 substTysWith tvs tys = ASSERT( length tvs == length tys )
2075 substTys (zipTvSubst tvs tys)
2076
2077 -- | Type substitution, see 'zipTvSubst'
2078 substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
2079 substTysWithCoVars cvs cos = ASSERT( length cvs == length cos )
2080 substTys (zipCvSubst cvs cos)
2081
2082 -- | Substitute within a 'Type' after adding the free variables of the type
2083 -- to the in-scope set. This is useful for the case when the free variables
2084 -- aren't already in the in-scope set or easily available.
2085 -- See also Note [The substitution invariant].
2086 substTyAddInScope :: TCvSubst -> Type -> Type
2087 substTyAddInScope subst ty =
2088 substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
2089
2090 -- | When calling `substTy` it should be the case that the in-scope set in
2091 -- the substitution is a superset of the free vars of the range of the
2092 -- substitution.
2093 -- See also Note [The substitution invariant].
2094 isValidTCvSubst :: TCvSubst -> Bool
2095 isValidTCvSubst (TCvSubst in_scope tenv cenv) =
2096 (tenvFVs `varSetInScope` in_scope) &&
2097 (cenvFVs `varSetInScope` in_scope)
2098 where
2099 tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv
2100 cenvFVs = tyCoVarsOfCos $ varEnvElts cenv
2101
2102 -- | This checks if the substitution satisfies the invariant from
2103 -- Note [The substitution invariant].
2104 checkValidSubst ::
2105 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2106 (?callStack :: CallStack) =>
2107 #endif
2108 TCvSubst -> [Type] -> [Coercion] -> a -> a
2109 checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
2110 = ASSERT2( isValidTCvSubst subst,
2111 text "in_scope" <+> ppr in_scope $$
2112 text "tenv" <+> ppr tenv $$
2113 text "tenvFVs"
2114 <+> ppr (tyCoVarsOfTypes $ varEnvElts tenv) $$
2115 text "cenv" <+> ppr cenv $$
2116 text "cenvFVs"
2117 <+> ppr (tyCoVarsOfCos $ varEnvElts cenv) $$
2118 text "tys" <+> ppr tys $$
2119 text "cos" <+> ppr cos )
2120 ASSERT2( tysCosFVsInScope,
2121 text "in_scope" <+> ppr in_scope $$
2122 text "tenv" <+> ppr tenv $$
2123 text "cenv" <+> ppr cenv $$
2124 text "tys" <+> ppr tys $$
2125 text "cos" <+> ppr cos $$
2126 text "needInScope" <+> ppr needInScope )
2127 a
2128 where
2129 substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv
2130 -- It's OK to use nonDetKeysUFM here, because we only use this list to
2131 -- remove some elements from a set
2132 needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
2133 `delListFromUFM_Directly` substDomain
2134 tysCosFVsInScope = needInScope `varSetInScope` in_scope
2135
2136
2137 -- | Substitute within a 'Type'
2138 -- The substitution has to satisfy the invariants described in
2139 -- Note [The substitution invariant].
2140 substTy ::
2141 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2142 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2143 (?callStack :: CallStack) =>
2144 #endif
2145 TCvSubst -> Type -> Type
2146 substTy subst ty
2147 | isEmptyTCvSubst subst = ty
2148 | otherwise = checkValidSubst subst [ty] [] $ subst_ty subst ty
2149
2150 -- | Substitute within a 'Type' disabling the sanity checks.
2151 -- The problems that the sanity checks in substTy catch are described in
2152 -- Note [The substitution invariant].
2153 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
2154 -- substTy and remove this function. Please don't use in new code.
2155 substTyUnchecked :: TCvSubst -> Type -> Type
2156 substTyUnchecked subst ty
2157 | isEmptyTCvSubst subst = ty
2158 | otherwise = subst_ty subst ty
2159
2160 -- | Substitute within several 'Type's
2161 -- The substitution has to satisfy the invariants described in
2162 -- Note [The substitution invariant].
2163 substTys ::
2164 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2165 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2166 (?callStack :: CallStack) =>
2167 #endif
2168 TCvSubst -> [Type] -> [Type]
2169 substTys subst tys
2170 | isEmptyTCvSubst subst = tys
2171 | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
2172
2173 -- | Substitute within several 'Type's disabling the sanity checks.
2174 -- The problems that the sanity checks in substTys catch are described in
2175 -- Note [The substitution invariant].
2176 -- The goal of #11371 is to migrate all the calls of substTysUnchecked to
2177 -- substTys and remove this function. Please don't use in new code.
2178 substTysUnchecked :: TCvSubst -> [Type] -> [Type]
2179 substTysUnchecked subst tys
2180 | isEmptyTCvSubst subst = tys
2181 | otherwise = map (subst_ty subst) tys
2182
2183 -- | Substitute within a 'ThetaType'
2184 -- The substitution has to satisfy the invariants described in
2185 -- Note [The substitution invariant].
2186 substTheta ::
2187 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2188 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2189 (?callStack :: CallStack) =>
2190 #endif
2191 TCvSubst -> ThetaType -> ThetaType
2192 substTheta = substTys
2193
2194 -- | Substitute within a 'ThetaType' disabling the sanity checks.
2195 -- The problems that the sanity checks in substTys catch are described in
2196 -- Note [The substitution invariant].
2197 -- The goal of #11371 is to migrate all the calls of substThetaUnchecked to
2198 -- substTheta and remove this function. Please don't use in new code.
2199 substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
2200 substThetaUnchecked = substTysUnchecked
2201
2202
2203 subst_ty :: TCvSubst -> Type -> Type
2204 -- subst_ty is the main workhorse for type substitution
2205 --
2206 -- Note that the in_scope set is poked only if we hit a forall
2207 -- so it may often never be fully computed
2208 subst_ty subst ty
2209 = go ty
2210 where
2211 go (TyVarTy tv) = substTyVar subst tv
2212 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
2213 -- The mkAppTy smart constructor is important
2214 -- we might be replacing (a Int), represented with App
2215 -- by [Int], represented with TyConApp
2216 go (TyConApp tc tys) = let args = map go tys
2217 in args `seqList` TyConApp tc args
2218 go (FunTy arg res) = (FunTy $! go arg) $! go res
2219 go (ForAllTy (TvBndr tv vis) ty)
2220 = case substTyVarBndrUnchecked subst tv of
2221 (subst', tv') ->
2222 (ForAllTy $! ((TvBndr $! tv') vis)) $!
2223 (subst_ty subst' ty)
2224 go (LitTy n) = LitTy $! n
2225 go (CastTy ty co) = (CastTy $! (go ty)) $! (subst_co subst co)
2226 go (CoercionTy co) = CoercionTy $! (subst_co subst co)
2227
2228 substTyVar :: TCvSubst -> TyVar -> Type
2229 substTyVar (TCvSubst _ tenv _) tv
2230 = ASSERT( isTyVar tv )
2231 case lookupVarEnv tenv tv of
2232 Just ty -> ty
2233 Nothing -> TyVarTy tv
2234
2235 substTyVars :: TCvSubst -> [TyVar] -> [Type]
2236 substTyVars subst = map $ substTyVar subst
2237
2238 lookupTyVar :: TCvSubst -> TyVar -> Maybe Type
2239 -- See Note [Extending the TCvSubst]
2240 lookupTyVar (TCvSubst _ tenv _) tv
2241 = ASSERT( isTyVar tv )
2242 lookupVarEnv tenv tv
2243
2244 -- | Substitute within a 'Coercion'
2245 -- The substitution has to satisfy the invariants described in
2246 -- Note [The substitution invariant].
2247 substCo ::
2248 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2249 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2250 (?callStack :: CallStack) =>
2251 #endif
2252 TCvSubst -> Coercion -> Coercion
2253 substCo subst co
2254 | isEmptyTCvSubst subst = co
2255 | otherwise = checkValidSubst subst [] [co] $ subst_co subst co
2256
2257 -- | Substitute within a 'Coercion' disabling sanity checks.
2258 -- The problems that the sanity checks in substCo catch are described in
2259 -- Note [The substitution invariant].
2260 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
2261 -- substCo and remove this function. Please don't use in new code.
2262 substCoUnchecked :: TCvSubst -> Coercion -> Coercion
2263 substCoUnchecked subst co
2264 | isEmptyTCvSubst subst = co
2265 | otherwise = subst_co subst co
2266
2267 -- | Substitute within several 'Coercion's
2268 -- The substitution has to satisfy the invariants described in
2269 -- Note [The substitution invariant].
2270 substCos ::
2271 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2272 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2273 (?callStack :: CallStack) =>
2274 #endif
2275 TCvSubst -> [Coercion] -> [Coercion]
2276 substCos subst cos
2277 | isEmptyTCvSubst subst = cos
2278 | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
2279
2280 subst_co :: TCvSubst -> Coercion -> Coercion
2281 subst_co subst co
2282 = go co
2283 where
2284 go_ty :: Type -> Type
2285 go_ty = subst_ty subst
2286
2287 go :: Coercion -> Coercion
2288 go (Refl r ty) = mkReflCo r $! go_ty ty
2289 go (TyConAppCo r tc args)= let args' = map go args
2290 in args' `seqList` mkTyConAppCo r tc args'
2291 go (AppCo co arg) = (mkAppCo $! go co) $! go arg
2292 go (ForAllCo tv kind_co co)
2293 = case substForAllCoBndrUnchecked subst tv kind_co of { (subst', tv', kind_co') ->
2294 ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co }
2295 go (CoVarCo cv) = substCoVar subst cv
2296 go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
2297 go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $!
2298 (go_ty t1)) $! (go_ty t2)
2299 go (SymCo co) = mkSymCo $! (go co)
2300 go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
2301 go (NthCo d co) = mkNthCo d $! (go co)
2302 go (LRCo lr co) = mkLRCo lr $! (go co)
2303 go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
2304 go (CoherenceCo co1 co2) = (mkCoherenceCo $! (go co1)) $! (go co2)
2305 go (KindCo co) = mkKindCo $! (go co)
2306 go (SubCo co) = mkSubCo $! (go co)
2307 go (AxiomRuleCo c cs) = let cs1 = map go cs
2308 in cs1 `seqList` AxiomRuleCo c cs1
2309
2310 go_prov UnsafeCoerceProv = UnsafeCoerceProv
2311 go_prov (PhantomProv kco) = PhantomProv (go kco)
2312 go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
2313 go_prov p@(PluginProv _) = p
2314 go_prov p@(HoleProv _) = p
2315 -- NB: this last case is a little suspicious, but we need it. Originally,
2316 -- there was a panic here, but it triggered from deeplySkolemise. Because
2317 -- we only skolemise tyvars that are manually bound, this operation makes
2318 -- sense, even over a coercion with holes.
2319
2320 substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion)
2321 substForAllCoBndr subst
2322 = substForAllCoBndrCallback False (substCo subst) subst
2323
2324 -- | Like 'substForAllCoBndr', but disables sanity checks.
2325 -- The problems that the sanity checks in substCo catch are described in
2326 -- Note [The substitution invariant].
2327 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
2328 -- substCo and remove this function. Please don't use in new code.
2329 substForAllCoBndrUnchecked :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion)
2330 substForAllCoBndrUnchecked subst
2331 = substForAllCoBndrCallback False (substCoUnchecked subst) subst
2332
2333 -- See Note [Sym and ForAllCo]
2334 substForAllCoBndrCallback :: Bool -- apply sym to binder?
2335 -> (Coercion -> Coercion) -- transformation to kind co
2336 -> TCvSubst -> TyVar -> Coercion
2337 -> (TCvSubst, TyVar, Coercion)
2338 substForAllCoBndrCallback sym sco (TCvSubst in_scope tenv cenv)
2339 old_var old_kind_co
2340 = ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv
2341 , new_var, new_kind_co )
2342 where
2343 new_env | no_change && not sym = delVarEnv tenv old_var
2344 | sym = extendVarEnv tenv old_var $
2345 TyVarTy new_var `CastTy` new_kind_co
2346 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
2347
2348 no_kind_change = isEmptyVarSet (tyCoVarsOfCo old_kind_co)
2349 no_change = no_kind_change && (new_var == old_var)
2350
2351 new_kind_co | no_kind_change = old_kind_co
2352 | otherwise = sco old_kind_co
2353
2354 Pair new_ki1 _ = coercionKind new_kind_co
2355
2356 new_var = uniqAway in_scope (setTyVarKind old_var new_ki1)
2357
2358 substCoVar :: TCvSubst -> CoVar -> Coercion
2359 substCoVar (TCvSubst _ _ cenv) cv
2360 = case lookupVarEnv cenv cv of
2361 Just co -> co
2362 Nothing -> CoVarCo cv
2363
2364 substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
2365 substCoVars subst cvs = map (substCoVar subst) cvs
2366
2367 lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
2368 lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
2369
2370 substTyVarBndr ::
2371 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
2372 #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
2373 (?callStack :: CallStack) =>
2374 #endif
2375 TCvSubst -> TyVar -> (TCvSubst, TyVar)
2376 substTyVarBndr = substTyVarBndrCallback substTy
2377
2378 -- | Like 'substTyVarBndr' but disables sanity checks.
2379 -- The problems that the sanity checks in substTy catch are described in
2380 -- Note [The substitution invariant].
2381 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
2382 -- substTy and remove this function. Please don't use in new code.
2383 substTyVarBndrUnchecked :: TCvSubst -> TyVar -> (TCvSubst, TyVar)
2384 substTyVarBndrUnchecked = substTyVarBndrCallback substTyUnchecked
2385
2386 -- | Substitute a tyvar in a binding position, returning an
2387 -- extended subst and a new tyvar.
2388 substTyVarBndrCallback :: (TCvSubst -> Type -> Type) -- ^ the subst function
2389 -> TCvSubst -> TyVar -> (TCvSubst, TyVar)
2390 substTyVarBndrCallback subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
2391 = ASSERT2( _no_capture, pprTvBndr old_var $$ pprTvBndr new_var $$ ppr subst )
2392 ASSERT( isTyVar old_var )
2393 (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var)
2394 where
2395 new_env | no_change = delVarEnv tenv old_var
2396 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
2397
2398 _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypes (varEnvElts tenv))
2399 -- Assertion check that we are not capturing something in the substitution
2400
2401 old_ki = tyVarKind old_var
2402 no_kind_change = isEmptyVarSet (tyCoVarsOfType old_ki) -- verify that kind is closed
2403 no_change = no_kind_change && (new_var == old_var)
2404 -- no_change means that the new_var is identical in
2405 -- all respects to the old_var (same unique, same kind)
2406 -- See Note [Extending the TCvSubst]
2407 --
2408 -- In that case we don't need to extend the substitution
2409 -- to map old to new. But instead we must zap any
2410 -- current substitution for the variable. For example:
2411 -- (\x.e) with id_subst = [x |-> e']
2412 -- Here we must simply zap the substitution for x
2413
2414 new_var | no_kind_change = uniqAway in_scope old_var
2415 | otherwise = uniqAway in_scope $
2416 setTyVarKind old_var (subst_fn subst old_ki)
2417 -- The uniqAway part makes sure the new variable is not already in scope
2418
2419 substCoVarBndr :: TCvSubst -> CoVar -> (TCvSubst, CoVar)
2420 substCoVarBndr = substCoVarBndrCallback False substTy
2421
2422 substCoVarBndrCallback :: Bool -- apply "sym" to the covar?
2423 -> (TCvSubst -> Type -> Type)
2424 -> TCvSubst -> CoVar -> (TCvSubst, CoVar)
2425 substCoVarBndrCallback sym subst_fun subst@(TCvSubst in_scope tenv cenv) old_var
2426 = ASSERT( isCoVar old_var )
2427 (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
2428 where
2429 -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
2430 -- In that case, mkCoVarCo will return a ReflCoercion, and
2431 -- we want to substitute that (not new_var) for old_var
2432 new_co = (if sym then mkSymCo else id) $ mkCoVarCo new_var
2433 no_kind_change = isEmptyVarSet (tyCoVarsOfTypes [t1, t2])
2434 no_change = new_var == old_var && not (isReflCo new_co) && no_kind_change
2435
2436 new_cenv | no_change = delVarEnv cenv old_var
2437 | otherwise = extendVarEnv cenv old_var new_co
2438
2439 new_var = uniqAway in_scope subst_old_var
2440 subst_old_var = mkCoVar (varName old_var) new_var_type
2441
2442 (_, _, t1, t2, role) = coVarKindsTypesRole old_var
2443 t1' = subst_fun subst t1
2444 t2' = subst_fun subst t2
2445 new_var_type = uncurry (mkCoercionType role) (if sym then (t2', t1') else (t1', t2'))
2446 -- It's important to do the substitution for coercions,
2447 -- because they can have free type variables
2448
2449 cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
2450 cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq
2451 = ASSERT2( isTyVar tv, ppr tv ) -- I think it's only called on TyVars
2452 (TCvSubst (extendInScopeSet in_scope tv')
2453 (extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv')
2454 where
2455 old_ki = tyVarKind tv
2456 no_kind_change = isEmptyVarSet (tyCoVarsOfType old_ki) -- verify that kind is closed
2457
2458 tv1 | no_kind_change = tv
2459 | otherwise = setTyVarKind tv (substTy subst old_ki)
2460
2461 tv' = setVarUnique tv1 uniq
2462
2463 cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
2464 cloneTyVarBndrs subst [] _usupply = (subst, [])
2465 cloneTyVarBndrs subst (t:ts) usupply = (subst'', tv:tvs)
2466 where
2467 (uniq, usupply') = takeUniqFromSupply usupply
2468 (subst' , tv ) = cloneTyVarBndr subst t uniq
2469 (subst'', tvs) = cloneTyVarBndrs subst' ts usupply'
2470
2471 {-
2472 %************************************************************************
2473 %* *
2474 Pretty-printing types
2475
2476 Defined very early because of debug printing in assertions
2477 %* *
2478 %************************************************************************
2479
2480 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
2481 defined to use this. @pprParendType@ is the same, except it puts
2482 parens around the type, except for the atomic cases. @pprParendType@
2483 works just by setting the initial context precedence very high.
2484
2485 Note [Precedence in types]
2486 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2487 We don't keep the fixity of type operators in the operator. So the pretty printer
2488 operates the following precedene structre:
2489 Type constructor application binds more tightly than
2490 Operator applications which bind more tightly than
2491 Function arrow
2492
2493 So we might see a :+: T b -> c
2494 meaning (a :+: (T b)) -> c
2495
2496 Maybe operator applications should bind a bit less tightly?
2497
2498 Anyway, that's the current story, and it is used consistently for Type and HsType
2499 -}
2500
2501 data TyPrec -- See Note [Prededence in types]
2502 = TopPrec -- No parens
2503 | FunPrec -- Function args; no parens for tycon apps
2504 | TyOpPrec -- Infix operator
2505 | TyConPrec -- Tycon args; no parens for atomic
2506 deriving( Eq, Ord )
2507
2508 maybeParen :: TyPrec -> TyPrec -> SDoc -> SDoc
2509 maybeParen ctxt_prec inner_prec pretty
2510 | ctxt_prec < inner_prec = pretty
2511 | otherwise = parens pretty
2512
2513 ------------------
2514
2515 {-
2516 Note [Defaulting RuntimeRep variables]
2517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2518
2519 RuntimeRep variables are considered by many (most?) users to be little more than
2520 syntactic noise. When the notion was introduced there was a signficant and
2521 understandable push-back from those with pedagogy in mind, which argued that
2522 RuntimeRep variables would throw a wrench into nearly any teach approach since
2523 they appear in even the lowly ($) function's type,
2524
2525 ($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
2526
2527 which is significantly less readable than its non RuntimeRep-polymorphic type of
2528
2529 ($) :: (a -> b) -> a -> b
2530
2531 Moreover, unboxed types don't appear all that often in run-of-the-mill Haskell
2532 programs, so it makes little sense to make all users pay this syntactic
2533 overhead.
2534
2535 For this reason it was decided that we would hide RuntimeRep variables for now
2536 (see #11549). We do this by defaulting all type variables of kind RuntimeRep to
2537 PtrLiftedRep. This is done in a pass right before pretty-printing
2538 (defaultRuntimeRepVars, controlled by -fprint-explicit-runtime-reps)
2539 -}
2540
2541 -- | Default 'RuntimeRep' variables to 'LiftedPtr'. e.g.
2542 --
2543 -- @
2544 -- ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
2545 -- (a -> b) -> a -> b
2546 -- @
2547 --
2548 -- turns in to,
2549 --
2550 -- @ ($) :: forall a (b :: *). (a -> b) -> a -> b @
2551 --
2552 -- We do this to prevent RuntimeRep variables from incurring a significant
2553 -- syntactic overhead in otherwise simple type signatures (e.g. ($)). See
2554 -- Note [Defaulting RuntimeRep variables] and #11549 for further discussion.
2555 --
2556 defaultRuntimeRepVars :: Type -> Type
2557 defaultRuntimeRepVars = defaultRuntimeRepVars' emptyVarSet
2558
2559 defaultRuntimeRepVars' :: TyVarSet -- ^ the binders which we should default
2560 -> Type -> Type
2561 -- TODO: Eventually we should just eliminate the Type pretty-printer
2562 -- entirely and simply use IfaceType; this task is tracked as #11660.
2563 defaultRuntimeRepVars' subs (ForAllTy (TvBndr var vis) ty)
2564 | isRuntimeRepVar var =
2565 let subs' = extendVarSet subs var
2566 in defaultRuntimeRepVars' subs' ty
2567 | otherwise =
2568 let var' = var { varType = defaultRuntimeRepVars' subs (varType var) }
2569 in ForAllTy (TvBndr var' vis) (defaultRuntimeRepVars' subs ty)
2570
2571 defaultRuntimeRepVars' subs (FunTy kind ty) =
2572 FunTy (defaultRuntimeRepVars' subs kind)
2573 (defaultRuntimeRepVars' subs ty)
2574
2575 defaultRuntimeRepVars' subs (TyVarTy var)
2576 | var `elemVarSet` subs = ptrRepLiftedTy
2577
2578 defaultRuntimeRepVars' subs (TyConApp tc args) =
2579 TyConApp tc $ map (defaultRuntimeRepVars' subs) args
2580
2581 defaultRuntimeRepVars' subs (AppTy x y) =
2582 defaultRuntimeRepVars' subs x `AppTy` defaultRuntimeRepVars' subs y
2583
2584 defaultRuntimeRepVars' subs (CastTy ty co) =
2585 CastTy (defaultRuntimeRepVars' subs ty) co
2586
2587 defaultRuntimeRepVars' _ other = other
2588
2589 eliminateRuntimeRep :: (Type -> SDoc) -> Type -> SDoc
2590 eliminateRuntimeRep f ty = sdocWithDynFlags $ \dflags ->
2591 if gopt Opt_PrintExplicitRuntimeReps dflags
2592 then f ty
2593 else f (defaultRuntimeRepVars ty)
2594
2595 pprType, pprParendType :: Type -> SDoc
2596 pprType ty = eliminateRuntimeRep (ppr_type TopPrec) ty
2597 pprParendType ty = eliminateRuntimeRep (ppr_type TyConPrec) ty
2598
2599 pprTyLit :: TyLit -> SDoc
2600 pprTyLit = ppr_tylit TopPrec
2601
2602 pprKind, pprParendKind :: Kind -> SDoc
2603 pprKind = pprType
2604 pprParendKind = pprParendType
2605
2606 ------------
2607 pprClassPred :: Class -> [Type] -> SDoc
2608 pprClassPred clas tys = pprTypeApp (classTyCon clas) tys
2609
2610 ------------
2611 pprTheta :: ThetaType -> SDoc
2612 pprTheta [pred] = ppr_type TopPrec pred -- I'm in two minds about this
2613 pprTheta theta = parens (sep (punctuate comma (map (ppr_type TopPrec) theta)))
2614
2615 pprThetaArrowTy :: ThetaType -> SDoc
2616 pprThetaArrowTy [] = empty
2617 pprThetaArrowTy [pred] = ppr_type TyOpPrec pred <+> darrow
2618 -- TyOpPrec: Num a => a -> a does not need parens
2619 -- bug (a :~: b) => a -> b currently does
2620 -- Trac # 9658
2621 pprThetaArrowTy preds = parens (fsep (punctuate comma (map (ppr_type TopPrec) preds)))
2622 <+> darrow
2623 -- Notice 'fsep' here rather that 'sep', so that
2624 -- type contexts don't get displayed in a giant column
2625 -- Rather than
2626 -- instance (Eq a,
2627 -- Eq b,
2628 -- Eq c,
2629 -- Eq d,
2630 -- Eq e,
2631 -- Eq f,
2632 -- Eq g,
2633 -- Eq h,
2634 -- Eq i,
2635 -- Eq j,
2636 -- Eq k,
2637 -- Eq l) =>
2638 -- Eq (a, b, c, d, e, f, g, h, i, j, k, l)
2639 -- we get
2640 --
2641 -- instance (Eq a, Eq b, Eq c, Eq d, Eq e, Eq f, Eq g, Eq h, Eq i,
2642 -- Eq j, Eq k, Eq l) =>
2643 -- Eq (a, b, c, d, e, f, g, h, i, j, k, l)
2644
2645 ------------------
2646 instance Outputable Type where
2647 ppr ty = pprType ty
2648
2649 instance Outputable TyLit where
2650 ppr = pprTyLit
2651
2652 ------------------
2653 -- OK, here's the main printer
2654
2655 ppr_type :: TyPrec -> Type -> SDoc
2656 ppr_type _ (TyVarTy tv) = ppr_tvar tv
2657
2658 ppr_type p (TyConApp tc tys) = pprTyTcApp p tc tys
2659 ppr_type p (LitTy l) = ppr_tylit p l
2660 ppr_type p ty@(ForAllTy {}) = ppr_forall_type p ty
2661 ppr_type p ty@(FunTy {}) = ppr_forall_type p ty
2662
2663 ppr_type p (AppTy t1 t2)
2664 = if_print_coercions
2665 ppr_app_ty
2666 (case split_app_tys t1 [t2] of
2667 (CastTy head _, args) -> ppr_type p (mk_app_tys head args)
2668 _ -> ppr_app_ty)
2669 where
2670 ppr_app_ty = maybeParen p TyConPrec $
2671 ppr_type FunPrec t1 <+> ppr_type TyConPrec t2
2672
2673 split_app_tys (AppTy ty1 ty2) args = split_app_tys ty1 (ty2:args)
2674 split_app_tys head args = (head, args)
2675
2676 mk_app_tys (TyConApp tc tys1) tys2 = TyConApp tc (tys1 ++ tys2)
2677 mk_app_tys ty1 tys2 = foldl AppTy ty1 tys2
2678
2679 ppr_type p (CastTy ty co)
2680 = if_print_coercions
2681 (parens (ppr_type TopPrec ty <+> text "|>" <+> ppr co))
2682 (ppr_type p ty)
2683
2684 ppr_type _ (CoercionTy co)
2685 = if_print_coercions
2686 (parens (ppr co))
2687 (text "<>")
2688
2689 ppr_forall_type :: TyPrec -> Type -> SDoc
2690 -- Used for types starting with ForAllTy or FunTy
2691 ppr_forall_type p ty
2692 = maybeParen p FunPrec $
2693 sdocWithDynFlags $ \dflags ->
2694 ppr_sigma_type dflags True ty
2695 -- True <=> we always print the foralls on *nested* quantifiers
2696 -- Opt_PrintExplicitForalls only affects top-level quantifiers
2697
2698 ppr_tvar :: TyVar -> SDoc
2699 ppr_tvar tv -- Note [Infix type variables]
2700 = parenSymOcc (getOccName tv) (ppr tv)
2701
2702 ppr_tylit :: TyPrec -> TyLit -> SDoc
2703 ppr_tylit _ tl =
2704 case tl of
2705 NumTyLit n -> integer n
2706 StrTyLit s -> text (show s)
2707
2708 if_print_coercions :: SDoc -- if printing coercions
2709 -> SDoc -- otherwise
2710 -> SDoc
2711 if_print_coercions yes no
2712 = sdocWithDynFlags $ \dflags ->
2713 getPprStyle $ \style ->
2714 if gopt Opt_PrintExplicitCoercions dflags
2715 || dumpStyle style || debugStyle style
2716 then yes
2717 else no
2718
2719 -------------------
2720 ppr_sigma_type :: DynFlags
2721 -> Bool -- ^ True <=> Show the foralls unconditionally
2722 -> Type -> SDoc
2723 -- Used for types starting with ForAllTy or FunTy
2724 -- Suppose we have (forall a. Show a => forall b. a -> b). When we're not
2725 -- printing foralls, we want to drop both the (forall a) and the (forall b).
2726 -- This logic does so.
2727 ppr_sigma_type dflags False orig_ty
2728 | not (gopt Opt_PrintExplicitForalls dflags)
2729 , all (isEmptyVarSet . tyCoVarsOfType . tyVarKind) tv_bndrs
2730 -- See Note [When to print foralls]
2731 = sep [ pprThetaArrowTy theta
2732 , pprArrowChain TopPrec (ppr_fun_tail tau) ]
2733 where
2734 (tv_bndrs, theta, tau) = split [] [] orig_ty
2735
2736 split :: [TyVar] -> [PredType] -> Type
2737 -> ([TyVar], [PredType], Type)
2738 split bndr_acc theta_acc (ForAllTy (TvBndr tv vis) ty)
2739 | isInvisible vis = split (tv : bndr_acc) theta_acc ty
2740 split bndr_acc theta_acc (FunTy ty1 ty2)
2741 | isPredTy ty1 = split bndr_acc (ty1 : theta_acc) ty2
2742 split bndr_acc theta_acc ty = (reverse bndr_acc, reverse theta_acc, ty)
2743
2744 ppr_sigma_type _ _ ty
2745 = sep [ pprForAll bndrs
2746 , pprThetaArrowTy ctxt
2747 , pprArrowChain TopPrec (ppr_fun_tail tau) ]
2748 where
2749 (bndrs, rho) = split1 [] ty
2750 (ctxt, tau) = split2 [] rho
2751
2752 split1 bndrs (ForAllTy bndr ty) = split1 (bndr:bndrs) ty
2753 split1 bndrs ty = (reverse bndrs, ty)
2754
2755 split2 ps (FunTy ty1 ty2) | isPredTy ty1 = split2 (ty1:ps) ty2
2756 split2 ps ty = (reverse ps, ty)
2757
2758 -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
2759 ppr_fun_tail :: Type -> [SDoc]
2760 ppr_fun_tail (FunTy ty1 ty2)
2761 | not (isPredTy ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2
2762 ppr_fun_tail other_ty = [ppr_type TopPrec other_ty]
2763
2764 pprSigmaType :: Type -> SDoc
2765 pprSigmaType ty = sdocWithDynFlags $ \dflags ->
2766 eliminateRuntimeRep (ppr_sigma_type dflags False) ty
2767
2768 pprUserForAll :: [TyVarBinder] -> SDoc
2769 -- Print a user-level forall; see Note [When to print foralls]
2770 pprUserForAll bndrs
2771 = sdocWithDynFlags $ \dflags ->
2772 ppWhen (any bndr_has_kind_var bndrs || gopt Opt_PrintExplicitForalls dflags) $
2773 pprForAll bndrs
2774 where
2775 bndr_has_kind_var bndr
2776 = not (isEmptyVarSet (tyCoVarsOfType (binderType bndr)))
2777
2778 pprForAllImplicit :: [TyVar] -> SDoc
2779 pprForAllImplicit tvs = pprForAll [ TvBndr tv Specified | tv <- tvs ]
2780
2781 -- | Render the "forall ... ." or "forall ... ->" bit of a type.
2782 -- Do not pass in anonymous binders!
2783 pprForAll :: [TyVarBinder] -> SDoc
2784 pprForAll [] = empty
2785 pprForAll bndrs@(TvBndr _ vis : _)
2786 = add_separator (forAllLit <+> doc) <+> pprForAll bndrs'
2787 where
2788 (bndrs', doc) = ppr_tv_bndrs bndrs vis
2789
2790 add_separator stuff = case vis of
2791 Visible -> stuff <+> arrow
2792 _inv -> stuff <> dot
2793
2794 pprTvBndrs :: [TyVar] -> SDoc
2795 pprTvBndrs tvs = sep (map pprTvBndr tvs)
2796
2797 -- | Render the ... in @(forall ... .)@ or @(forall ... ->)@.
2798 -- Returns both the list of not-yet-rendered binders and the doc.
2799 -- No anonymous binders here!
2800 ppr_tv_bndrs :: [TyVarBinder]
2801 -> VisibilityFlag -- ^ visibility of the first binder in the list
2802 -> ([TyVarBinder], SDoc)
2803 ppr_tv_bndrs all_bndrs@(TvBndr tv vis : bndrs) vis1
2804 | vis `sameVis` vis1 = let (bndrs', doc) = ppr_tv_bndrs bndrs vis1
2805 pp_tv = sdocWithDynFlags $ \dflags ->
2806 if Invisible == vis &&
2807 gopt Opt_PrintExplicitForalls dflags
2808 then braces (pprTvBndrNoParens tv)
2809 else pprTvBndr tv
2810 in
2811 (bndrs', pp_tv <+> doc)
2812 | otherwise = (all_bndrs, empty)
2813 ppr_tv_bndrs [] _ = ([], empty)
2814
2815 pprTvBndr :: TyVar -> SDoc
2816 pprTvBndr tv
2817 | isLiftedTypeKind kind = ppr_tvar tv
2818 | otherwise = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
2819 where
2820 kind = tyVarKind tv
2821
2822 pprTvBndrNoParens :: TyVar -> SDoc
2823 pprTvBndrNoParens tv
2824 | isLiftedTypeKind kind = ppr_tvar tv
2825 | otherwise = ppr_tvar tv <+> dcolon <+> pprKind kind
2826 where
2827 kind = tyVarKind tv
2828
2829 instance Outputable TyVarBinder where
2830 ppr (TvBndr v Visible) = ppr v
2831 ppr (TvBndr v Specified) = char '@' <> ppr v
2832 ppr (TvBndr v Invisible) = braces (ppr v)
2833
2834 instance Outputable TyBinder where
2835 ppr (Named tvb) = ppr tvb
2836 ppr (Anon ty) = text "[anon]" <+> ppr ty
2837
2838 instance Outputable VisibilityFlag where
2839 ppr Visible = text "[vis]"
2840 ppr Specified = text "[spec]"
2841 ppr Invisible = text "[invis]"
2842
2843 -----------------
2844 instance Outputable Coercion where -- defined here to avoid orphans
2845 ppr = pprCo
2846 instance Outputable LeftOrRight where
2847 ppr CLeft = text "Left"
2848 ppr CRight = text "Right"
2849
2850 {-
2851 Note [When to print foralls]
2852 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2853 Mostly we want to print top-level foralls when (and only when) the user specifies
2854 -fprint-explicit-foralls. But when kind polymorphism is at work, that suppresses
2855 too much information; see Trac #9018.
2856
2857 So I'm trying out this rule: print explicit foralls if
2858 a) User specifies -fprint-explicit-foralls, or
2859 b) Any of the quantified type variables has a kind
2860 that mentions a kind variable
2861
2862 This catches common situations, such as a type siguature
2863 f :: m a
2864 which means
2865 f :: forall k. forall (m :: k->*) (a :: k). m a
2866 We really want to see both the "forall k" and the kind signatures
2867 on m and a. The latter comes from pprTvBndr.
2868
2869 Note [Infix type variables]
2870 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2871 With TypeOperators you can say
2872
2873 f :: (a ~> b) -> b
2874
2875 and the (~>) is considered a type variable. However, the type
2876 pretty-printer in this module will just see (a ~> b) as
2877
2878 App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
2879
2880 So it'll print the type in prefix form. To avoid confusion we must
2881 remember to parenthesise the operator, thus
2882
2883 (~>) a b -> b
2884
2885 See Trac #2766.
2886 -}
2887
2888 pprDataCons :: TyCon -> SDoc
2889 pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons
2890 where
2891 sepWithVBars [] = empty
2892 sepWithVBars docs = sep (punctuate (space <> vbar) docs)
2893
2894 pprDataConWithArgs :: DataCon -> SDoc
2895 pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc]
2896 where
2897 (_univ_tvs, _ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc
2898 univ_bndrs = dataConUnivTyVarBinders dc
2899 ex_bndrs = dataConExTyVarBinders dc
2900 forAllDoc = pprUserForAll $ (filterEqSpec eq_spec univ_bndrs ++ ex_bndrs)
2901 thetaDoc = pprThetaArrowTy theta
2902 argsDoc = hsep (fmap pprParendType arg_tys)
2903
2904
2905 pprTypeApp :: TyCon -> [Type] -> SDoc
2906 pprTypeApp tc tys = pprTyTcApp TopPrec tc tys
2907 -- We have to use ppr on the TyCon (not its name)
2908 -- so that we get promotion quotes in the right place
2909
2910 pprTyTcApp :: TyPrec -> TyCon -> [Type] -> SDoc
2911 -- Used for types only; so that we can make a
2912 -- special case for type-level lists
2913 pprTyTcApp p tc tys
2914 | tc `hasKey` ipClassKey
2915 , [LitTy (StrTyLit n),ty] <- tys
2916 = maybeParen p FunPrec $
2917 char '?' <> ftext n <> text "::" <> ppr_type TopPrec ty
2918
2919 | tc `hasKey` consDataConKey
2920 , [_kind,ty1,ty2] <- tys
2921 = sdocWithDynFlags $ \dflags ->
2922 if gopt Opt_PrintExplicitKinds dflags then ppr_deflt
2923 else pprTyList p ty1 ty2
2924
2925 | not opt_PprStyle_Debug
2926 , tc `hasKey` errorMessageTypeErrorFamKey
2927 = text "(TypeError ...)" -- Suppress detail unles you _really_ want to see
2928
2929 | tc `hasKey` tYPETyConKey
2930 , [TyConApp ptr_rep []] <- tys
2931 , ptr_rep `hasKey` ptrRepLiftedDataConKey
2932 = unicodeSyntax (char '') (char '*')
2933
2934 | tc `hasKey` tYPETyConKey
2935 , [TyConApp ptr_rep []] <- tys
2936 , ptr_rep `hasKey` ptrRepUnliftedDataConKey
2937 = char '#'
2938
2939 | otherwise
2940 = ppr_deflt
2941 where
2942 ppr_deflt = pprTcAppTy p ppr_type tc tys
2943
2944 pprTcAppTy :: TyPrec -> (TyPrec -> Type -> SDoc) -> TyCon -> [Type] -> SDoc
2945 pprTcAppTy p pp tc tys
2946 = getPprStyle $ \style -> pprTcApp style id p pp tc tys
2947
2948 pprTcAppCo :: TyPrec -> (TyPrec -> Coercion -> SDoc)
2949 -> TyCon -> [Coercion] -> SDoc
2950 pprTcAppCo p pp tc cos
2951 = getPprStyle $ \style ->
2952 pprTcApp style (pFst . coercionKind) p pp tc cos
2953
2954 pprTcApp :: PprStyle
2955 -> (a -> Type) -> TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> SDoc
2956 -- Used for both types and coercions, hence polymorphism
2957 pprTcApp _ _ _ pp tc [ty]
2958 | tc `hasKey` listTyConKey = pprPromotionQuote tc <> brackets (pp TopPrec ty)
2959 | tc `hasKey` parrTyConKey = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
2960
2961 pprTcApp style to_type p pp tc tys
2962 | not (debugStyle style)
2963 , Just sort <- tyConTuple_maybe tc
2964 , let arity = tyConArity tc
2965 , arity == length tys
2966 , let num_to_drop = case sort of UnboxedTuple -> arity `div` 2
2967 _ -> 0
2968 = pprTupleApp p pp tc sort (drop num_to_drop tys)
2969
2970 | not (debugStyle style)
2971 , Just dc <- isPromotedDataCon_maybe tc
2972 , let dc_tc = dataConTyCon dc
2973 , Just tup_sort <- tyConTuple_maybe dc_tc
2974 , let arity = tyConArity dc_tc -- E.g. 3 for (,,) k1 k2 k3 t1 t2 t3
2975 ty_args = drop arity tys -- Drop the kind args
2976 , ty_args `lengthIs` arity -- Result is saturated
2977 = pprPromotionQuote tc <>
2978 (tupleParens tup_sort $ pprWithCommas (pp TopPrec) ty_args)
2979
2980 | otherwise
2981 = sdocWithDynFlags $ \dflags ->
2982 pprTcApp_help to_type p pp tc tys dflags style
2983 where
2984
2985 pprTupleApp :: TyPrec -> (TyPrec -> a -> SDoc)
2986 -> TyCon -> TupleSort -> [a] -> SDoc
2987 -- Print a saturated tuple
2988 pprTupleApp p pp tc sort tys
2989 | null tys
2990 , ConstraintTuple <- sort
2991 = if opt_PprStyle_Debug then text "(%%)"
2992 else maybeParen p FunPrec $
2993 text "() :: Constraint"
2994 | otherwise
2995 = pprPromotionQuote tc <>
2996 tupleParens sort (pprWithCommas (pp TopPrec) tys)
2997
2998 pprTcApp_help :: (a -> Type) -> TyPrec -> (TyPrec -> a -> SDoc)
2999 -> TyCon -> [a] -> DynFlags -> PprStyle -> SDoc
3000 -- This one has accss to the DynFlags
3001 pprTcApp_help to_type p pp tc tys dflags style
3002 | not (isSymOcc (nameOccName tc_name)) -- Print prefix
3003 = pprPrefixApp p pp_tc (map (pp TyConPrec) tys_wo_kinds)
3004
3005 | Just args <- mb_saturated_equality
3006 = print_equality args
3007
3008 -- So we have an operator symbol of some kind
3009
3010 | [ty1,ty2] <- tys_wo_kinds -- Infix, two arguments;
3011 -- we know nothing of precedence though
3012 = pprInfixApp p pp pp_tc ty1 ty2
3013
3014 | tc_name `hasKey` starKindTyConKey
3015 || tc_name `hasKey` unicodeStarKindTyConKey
3016 || tc_name `hasKey` unliftedTypeKindTyConKey
3017 = pp_tc -- Do not wrap *, # in parens
3018
3019 | otherwise -- Unsaturated operator
3020 = pprPrefixApp p (parens (pp_tc)) (map (pp TyConPrec) tys_wo_kinds)
3021 where
3022 tc_name = tyConName tc
3023 pp_tc = ppr tc
3024 tys_wo_kinds = suppressInvisibles to_type dflags tc tys
3025
3026 mb_saturated_equality
3027 | hetero_eq_tc
3028 , [k1, k2, t1, t2] <- tys
3029 = Just (k1, k2, t1, t2)
3030 | homo_eq_tc
3031 , [k, t1, t2] <- tys -- we must have (~)
3032 = Just (k, k, t1, t2)
3033 | otherwise
3034 = Nothing
3035
3036 homo_eq_tc = tc `hasKey` eqTyConKey -- ~
3037 hetero_eq_tc = tc `hasKey` eqPrimTyConKey -- ~#
3038 || tc `hasKey` eqReprPrimTyConKey -- ~R#
3039 || tc `hasKey` heqTyConKey -- ~~
3040
3041 -- This is all a bit ad-hoc, trying to print out the best representation
3042 -- of equalities. If you see a better design, go for it.
3043
3044 print_equality (ki1, ki2, ty1, ty2)
3045 | print_eqs
3046 = ppr_infix_eq pp_tc
3047
3048 | hetero_eq_tc
3049 , print_kinds || not (to_type ki1 `eqType` to_type ki2)
3050 = ppr_infix_eq $ if tc `hasKey` eqPrimTyConKey
3051 then text "~~"
3052 else pp_tc
3053
3054 | otherwise
3055 = if tc `hasKey` eqReprPrimTyConKey
3056 then text "Coercible" <+> (sep [ pp TyConPrec ty1
3057 , pp TyConPrec ty2 ])
3058 else sep [pp TyOpPrec ty1, text "~", pp TyOpPrec ty2]
3059
3060 where
3061 ppr_infix_eq eq_op
3062 = sep [ parens (pp TyOpPrec ty1 <+> dcolon <+> pp TyOpPrec ki1)
3063 , eq_op
3064 , parens (pp TyOpPrec ty2 <+> dcolon <+> pp TyOpPrec ki2)]
3065
3066 print_kinds = gopt Opt_PrintExplicitKinds dflags
3067 print_eqs = gopt Opt_PrintEqualityRelations dflags ||
3068 dumpStyle style ||
3069 debugStyle style
3070
3071 ------------------
3072 -- | Given a 'TyCon',and the args to which it is applied,
3073 -- suppress the args that are implicit
3074 suppressInvisibles :: (a -> Type) -> DynFlags -> TyCon -> [a] -> [a]
3075 suppressInvisibles to_type dflags tc xs
3076 | gopt Opt_PrintExplicitKinds dflags = xs
3077 | otherwise = snd $ partitionInvisibles tc to_type xs
3078
3079 ----------------
3080 pprTyList :: TyPrec -> Type -> Type -> SDoc
3081 -- Given a type-level list (t1 ': t2), see if we can print
3082 -- it in list notation [t1, ...].
3083 pprTyList p ty1 ty2
3084 = case gather ty2 of
3085 (arg_tys, Nothing) -> char '\'' <> brackets (fsep (punctuate comma
3086 (map (ppr_type TopPrec) (ty1:arg_tys))))
3087 (arg_tys, Just tl) -> maybeParen p FunPrec $
3088 hang (ppr_type FunPrec ty1)
3089 2 (fsep [ colon <+> ppr_type FunPrec ty | ty <- arg_tys ++ [tl]])
3090 where
3091 gather :: Type -> ([Type], Maybe Type)
3092 -- (gather ty) = (tys, Nothing) means ty is a list [t1, .., tn]
3093 -- = (tys, Just tl) means ty is of form t1:t2:...tn:tl
3094 gather (TyConApp tc tys)
3095 | tc `hasKey` consDataConKey
3096 , [_kind, ty1,ty2] <- tys
3097 , (args, tl) <- gather ty2
3098 = (ty1:args, tl)
3099 | tc `hasKey` nilDataConKey
3100 = ([], Nothing)
3101 gather ty = ([], Just ty)
3102
3103 ----------------
3104 pprInfixApp :: TyPrec -> (TyPrec -> a -> SDoc) -> SDoc -> a -> a -> SDoc
3105 pprInfixApp p pp pp_tc ty1 ty2
3106 = maybeParen p TyOpPrec $
3107 sep [pp TyOpPrec ty1, pprInfixVar True pp_tc <+> pp TyOpPrec ty2]
3108
3109 pprPrefixApp :: TyPrec -> SDoc -> [SDoc] -> SDoc
3110 pprPrefixApp p pp_fun pp_tys
3111 | null pp_tys = pp_fun
3112 | otherwise = maybeParen p TyConPrec $
3113 hang pp_fun 2 (sep pp_tys)
3114 ----------------
3115 pprArrowChain :: TyPrec -> [SDoc] -> SDoc
3116 -- pprArrowChain p [a,b,c] generates a -> b -> c
3117 pprArrowChain _ [] = empty
3118 pprArrowChain p (arg:args) = maybeParen p FunPrec $
3119 sep [arg, sep (map (arrow <+>) args)]
3120
3121 ppSuggestExplicitKinds :: SDoc
3122 -- Print a helpful suggstion about -fprint-explicit-kinds,
3123 -- if it is not already on
3124 ppSuggestExplicitKinds
3125 = sdocWithDynFlags $ \ dflags ->
3126 ppUnless (gopt Opt_PrintExplicitKinds dflags) $
3127 text "Use -fprint-explicit-kinds to see the kind arguments"
3128
3129 {-
3130 %************************************************************************
3131 %* *
3132 \subsection{TidyType}
3133 %* *
3134 %************************************************************************
3135 -}
3136
3137 -- | This tidies up a type for printing in an error message, or in
3138 -- an interface file.
3139 --
3140 -- It doesn't change the uniques at all, just the print names.
3141 tidyTyCoVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
3142 tidyTyCoVarBndrs env tvs = mapAccumL tidyTyCoVarBndr env tvs
3143
3144 tidyTyCoVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
3145 tidyTyCoVarBndr tidy_env@(occ_env, subst) tyvar
3146 = case tidyOccName occ_env occ1 of
3147 (tidy', occ') -> ((tidy', subst'), tyvar')
3148 where
3149 subst' = extendVarEnv subst tyvar tyvar'
3150 tyvar' = setTyVarKind (setTyVarName tyvar name') kind'
3151 name' = tidyNameOcc name occ'
3152 kind' = tidyKind tidy_env (tyVarKind tyvar)
3153 where
3154 name = tyVarName tyvar
3155 occ = getOccName name
3156 -- System Names are for unification variables;
3157 -- when we tidy them we give them a trailing "0" (or 1 etc)
3158 -- so that they don't take precedence for the un-modified name
3159 -- Plus, indicating a unification variable in this way is a
3160 -- helpful clue for users
3161 occ1 | isSystemName name
3162 = if isTyVar tyvar
3163 then mkTyVarOcc (occNameString occ ++ "0")
3164 else mkVarOcc (occNameString occ ++ "0")
3165 | otherwise = occ
3166
3167 tidyTyVarBinder :: TidyEnv -> TyVarBinder -> (TidyEnv, TyVarBinder)
3168 tidyTyVarBinder tidy_env (TvBndr tv vis)
3169 = (tidy_env', TvBndr tv' vis)
3170 where
3171 (tidy_env', tv') = tidyTyCoVarBndr tidy_env tv
3172
3173 tidyTyVarBinders :: TidyEnv -> [TyVarBinder] -> (TidyEnv, [TyVarBinder])
3174 tidyTyVarBinders = mapAccumL tidyTyVarBinder
3175
3176 ---------------
3177 tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
3178 -- ^ Add the free 'TyVar's to the env in tidy form,
3179 -- so that we can tidy the type they are free in
3180 tidyFreeTyCoVars (full_occ_env, var_env) tyvars
3181 = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars)
3182
3183 ---------------
3184 tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
3185 tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars
3186
3187 ---------------
3188 tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
3189 -- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
3190 -- using the environment if one has not already been allocated. See
3191 -- also 'tidyTyCoVarBndr'
3192 tidyOpenTyCoVar env@(_, subst) tyvar
3193 = case lookupVarEnv subst tyvar of
3194 Just tyvar' -> (env, tyvar') -- Already substituted
3195 Nothing ->
3196 let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar))
3197 in tidyTyCoVarBndr env' tyvar -- Treat it as a binder
3198
3199 ---------------
3200 tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
3201 tidyTyVarOcc env@(_, subst) tv
3202 = case lookupVarEnv subst tv of
3203 Nothing -> updateTyVarKind (tidyType env) tv
3204 Just tv' -> tv'
3205
3206 ---------------
3207 tidyTypes :: TidyEnv -> [Type] -> [Type]
3208 tidyTypes env tys = map (tidyType env) tys
3209
3210 ---------------
3211 tidyType :: TidyEnv -> Type -> Type
3212 tidyType _ (LitTy n) = LitTy n
3213 tidyType env (TyVarTy tv) = TyVarTy (tidyTyVarOcc env tv)
3214 tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
3215 in args `seqList` TyConApp tycon args
3216 tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
3217 tidyType env (FunTy fun arg) = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
3218 tidyType env (ForAllTy (TvBndr tv vis) ty)
3219 = (ForAllTy $! ((TvBndr $! tvp) $! vis)) $! (tidyType envp ty)
3220 where
3221 (envp, tvp) = tidyTyCoVarBndr env tv
3222 tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCo env co)
3223 tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co)
3224
3225 ---------------
3226 -- | Grabs the free type variables, tidies them
3227 -- and then uses 'tidyType' to work over the type itself
3228 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
3229 tidyOpenTypes env tys
3230 = (env', tidyTypes (trimmed_occ_env, var_env) tys)
3231 where
3232 (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $
3233 tyCoVarsOfTypesWellScoped tys
3234 trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
3235 -- The idea here was that we restrict the new TidyEnv to the
3236 -- _free_ vars of the types, so that we don't gratuitously rename
3237 -- the _bound_ variables of the types.
3238
3239 ---------------
3240 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
3241 tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in
3242 (env', ty')
3243
3244 ---------------
3245 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
3246 tidyTopType :: Type -> Type
3247 tidyTopType ty = tidyType emptyTidyEnv ty
3248
3249 ---------------
3250 tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
3251 tidyOpenKind = tidyOpenType
3252
3253 tidyKind :: TidyEnv -> Kind -> Kind
3254 tidyKind = tidyType
3255
3256 ----------------
3257 tidyCo :: TidyEnv -> Coercion -> Coercion
3258 tidyCo env@(_, subst) co
3259 = go co
3260 where
3261 go (Refl r ty) = Refl r (tidyType env ty)
3262 go (TyConAppCo r tc cos) = let args = map go cos
3263 in args `seqList` TyConAppCo r tc args
3264 go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
3265 go (ForAllCo tv h co) = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co)
3266 where (envp, tvp) = tidyTyCoVarBndr env tv
3267 -- the case above duplicates a bit of work in tidying h and the kind
3268 -- of tv. But the alternative is to use coercionKind, which seems worse.
3269 go (CoVarCo cv) = case lookupVarEnv subst cv of
3270 Nothing -> CoVarCo cv
3271 Just cv' -> CoVarCo cv'
3272 go (AxiomInstCo con ind cos) = let args = map go cos
3273 in args `seqList` AxiomInstCo con ind args
3274 go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $!
3275 tidyType env t1) $! tidyType env t2
3276 go (SymCo co) = SymCo $! go co
3277 go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
3278 go (NthCo d co) = NthCo d $! go co
3279 go (LRCo lr co) = LRCo lr $! go co
3280 go (InstCo co ty) = (InstCo $! go co) $! go ty
3281 go (CoherenceCo co1 co2) = (CoherenceCo $! go co1) $! go co2
3282 go (KindCo co) = KindCo $! go co
3283 go (SubCo co) = SubCo $! go co
3284 go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos
3285 in cos1 `seqList` AxiomRuleCo ax cos1
3286
3287 go_prov UnsafeCoerceProv = UnsafeCoerceProv
3288 go_prov (PhantomProv co) = PhantomProv (go co)
3289 go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
3290 go_prov p@(PluginProv _) = p
3291 go_prov p@(HoleProv _) = p
3292
3293 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
3294 tidyCos env = map (tidyCo env)