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