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