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