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