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