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