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