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