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