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