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