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