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