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