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