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