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