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