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