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