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