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