Update Trac ticket URLs to point to GitLab
[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 not-home #-}
20 {-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-}
21
22 module TyCoRep (
23 TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
24
25 -- * Types
26 Type( TyVarTy, AppTy, TyConApp, ForAllTy
27 , LitTy, CastTy, CoercionTy
28 , FunTy, ft_arg, ft_res, ft_af
29 ), -- Export the type synonym FunTy too
30
31 TyLit(..),
32 KindOrType, Kind,
33 KnotTied,
34 PredType, ThetaType, -- Synonyms
35 ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..),
36
37 -- * Coercions
38 Coercion(..),
39 UnivCoProvenance(..),
40 CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
41 CoercionN, CoercionR, CoercionP, KindCoercion,
42 MCoercion(..), MCoercionR, MCoercionN,
43
44 -- * Functions over types
45 mkTyConTy, mkTyVarTy, mkTyVarTys,
46 mkTyCoVarTy, mkTyCoVarTys,
47 mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkInvisFunTys,
48 mkForAllTy, mkForAllTys,
49 mkPiTy, mkPiTys,
50
51 kindRep_maybe, kindRep,
52 isLiftedTypeKind, isUnliftedTypeKind,
53 isLiftedRuntimeRep, isUnliftedRuntimeRep,
54 isRuntimeRepTy, isRuntimeRepVar,
55 sameVis,
56
57 -- * Functions over binders
58 TyCoBinder(..), TyCoVarBinder, TyBinder,
59 binderVar, binderVars, binderType, binderArgFlag,
60 delBinderVar,
61 isInvisibleArgFlag, isVisibleArgFlag,
62 isInvisibleBinder, isVisibleBinder,
63 isTyBinder, isNamedBinder,
64
65 -- * Functions over coercions
66 pickLR,
67
68 -- * Pretty-printing
69 pprType, pprParendType, pprPrecType, pprPrecTypeX,
70 pprTypeApp, pprTCvBndr, pprTCvBndrs,
71 pprSigmaType,
72 pprTheta, pprParendTheta, pprForAll, pprUserForAll,
73 pprTyVar, pprTyVars,
74 pprThetaArrowTy, pprClassPred,
75 pprKind, pprParendKind, pprTyLit,
76 PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
77 pprDataCons, pprWithExplicitKindsWhen,
78
79 pprCo, pprParendCo,
80
81 debugPprType,
82
83 -- * Free variables
84 tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
85 tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
86 tyCoFVsOfType, tyCoVarsOfTypeList,
87 tyCoFVsOfTypes, tyCoVarsOfTypesList,
88 coVarsOfType, coVarsOfTypes,
89 coVarsOfCo, coVarsOfCos,
90 tyCoVarsOfCo, tyCoVarsOfCos,
91 tyCoVarsOfCoDSet,
92 tyCoFVsOfCo, tyCoFVsOfCos,
93 tyCoVarsOfCoList, tyCoVarsOfProv,
94 almostDevoidCoVarOfCo,
95 injectiveVarsOfType, tyConAppNeedsKindSig,
96
97 noFreeVarsOfType, noFreeVarsOfCo,
98
99 -- * Substitutions
100 TCvSubst(..), TvSubstEnv, CvSubstEnv,
101 emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
102 emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
103 mkTCvSubst, mkTvSubst, mkCvSubst,
104 getTvSubstEnv,
105 getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
106 isInScope, notElemTCvSubst,
107 setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
108 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
109 extendTCvSubst, extendTCvSubstWithClone,
110 extendCvSubst, extendCvSubstWithClone,
111 extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
112 extendTvSubstList, extendTvSubstAndInScope,
113 extendTCvSubstList,
114 unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
115 zipTvSubst, zipCvSubst,
116 zipTCvSubst,
117 mkTvSubstPrs,
118
119 substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
120 substCoWith,
121 substTy, substTyAddInScope,
122 substTyUnchecked, substTysUnchecked, substThetaUnchecked,
123 substTyWithUnchecked,
124 substCoUnchecked, substCoWithUnchecked,
125 substTyWithInScope,
126 substTys, substTheta,
127 lookupTyVar,
128 substCo, substCos, substCoVar, substCoVars, lookupCoVar,
129 cloneTyVarBndr, cloneTyVarBndrs,
130 substVarBndr, substVarBndrs,
131 substTyVarBndr, substTyVarBndrs,
132 substCoVarBndr,
133 substTyVar, substTyVars, substTyCoVars,
134 substForAllCoBndr,
135 substVarBndrUsing, substForAllCoBndrUsing,
136 checkValidSubst, isValidTCvSubst,
137
138 -- * Tidying type related things up for printing
139 tidyType, tidyTypes,
140 tidyOpenType, tidyOpenTypes,
141 tidyOpenKind,
142 tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
143 tidyOpenTyCoVar, tidyOpenTyCoVars,
144 tidyTyCoVarOcc,
145 tidyTopType,
146 tidyKind,
147 tidyCo, tidyCos,
148 tidyTyCoVarBinder, tidyTyCoVarBinders,
149
150 -- * Sizes
151 typeSize, coercionSize, provSize
152 ) where
153
154 #include "HsVersions.h"
155
156 import GhcPrelude
157
158 import {-# SOURCE #-} DataCon( dataConFullSig
159 , dataConUserTyVarBinders
160 , DataCon )
161 import {-# SOURCE #-} Type( isCoercionTy, mkAppTy, mkCastTy
162 , tyCoVarsOfTypeWellScoped
163 , tyCoVarsOfTypesWellScoped
164 , scopedSort
165 , coreView )
166 -- Transitively pulls in a LOT of stuff, better to break the loop
167
168 import {-# SOURCE #-} Coercion
169 import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
170 import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
171 , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
172
173 -- friends:
174 import IfaceType
175 import Var
176 import VarEnv
177 import VarSet
178 import Name hiding ( varName )
179 import TyCon
180 import Class
181 import CoAxiom
182 import FV
183
184 -- others
185 import BasicTypes ( LeftOrRight(..), PprPrec(..), topPrec, sigPrec, opPrec
186 , funPrec, appPrec, maybeParen, pickLR )
187 import PrelNames
188 import Outputable
189 import DynFlags
190 import FastString
191 import Pair
192 import UniqSupply
193 import Util
194 import UniqFM
195 import UniqSet
196
197 -- libraries
198 import qualified Data.Data as Data hiding ( TyCon )
199 import Data.List
200 import Data.IORef ( IORef ) -- for CoercionHole
201
202 {-
203 %************************************************************************
204 %* *
205 TyThing
206 %* *
207 %************************************************************************
208
209 Despite the fact that DataCon has to be imported via a hi-boot route,
210 this module seems the right place for TyThing, because it's needed for
211 funTyCon and all the types in TysPrim.
212
213 It is also SOURCE-imported into Name.hs
214
215
216 Note [ATyCon for classes]
217 ~~~~~~~~~~~~~~~~~~~~~~~~~
218 Both classes and type constructors are represented in the type environment
219 as ATyCon. You can tell the difference, and get to the class, with
220 isClassTyCon :: TyCon -> Bool
221 tyConClass_maybe :: TyCon -> Maybe Class
222 The Class and its associated TyCon have the same Name.
223 -}
224
225 -- | A global typecheckable-thing, essentially anything that has a name.
226 -- Not to be confused with a 'TcTyThing', which is also a typecheckable
227 -- thing but in the *local* context. See 'TcEnv' for how to retrieve
228 -- a 'TyThing' given a 'Name'.
229 data TyThing
230 = AnId Id
231 | AConLike ConLike
232 | ATyCon TyCon -- TyCons and classes; see Note [ATyCon for classes]
233 | ACoAxiom (CoAxiom Branched)
234
235 instance Outputable TyThing where
236 ppr = pprShortTyThing
237
238 instance NamedThing TyThing where -- Can't put this with the type
239 getName (AnId id) = getName id -- decl, because the DataCon instance
240 getName (ATyCon tc) = getName tc -- isn't visible there
241 getName (ACoAxiom cc) = getName cc
242 getName (AConLike cl) = conLikeName cl
243
244 pprShortTyThing :: TyThing -> SDoc
245 -- c.f. PprTyThing.pprTyThing, which prints all the details
246 pprShortTyThing thing
247 = pprTyThingCategory thing <+> quotes (ppr (getName thing))
248
249 pprTyThingCategory :: TyThing -> SDoc
250 pprTyThingCategory = text . capitalise . tyThingCategory
251
252 tyThingCategory :: TyThing -> String
253 tyThingCategory (ATyCon tc)
254 | isClassTyCon tc = "class"
255 | otherwise = "type constructor"
256 tyThingCategory (ACoAxiom _) = "coercion axiom"
257 tyThingCategory (AnId _) = "identifier"
258 tyThingCategory (AConLike (RealDataCon _)) = "data constructor"
259 tyThingCategory (AConLike (PatSynCon _)) = "pattern synonym"
260
261
262 {- **********************************************************************
263 * *
264 Type
265 * *
266 ********************************************************************** -}
267
268 -- | The key representation of types within the compiler
269
270 type KindOrType = Type -- See Note [Arguments to type constructors]
271
272 -- | The key type representing kinds in the compiler.
273 type Kind = Type
274
275 -- If you edit this type, you may need to update the GHC formalism
276 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
277 data Type
278 -- See Note [Non-trivial definitional equality]
279 = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
280
281 | AppTy
282 Type
283 Type -- ^ Type application to something other than a 'TyCon'. Parameters:
284 --
285 -- 1) Function: must /not/ be a 'TyConApp' or 'CastTy',
286 -- must be another 'AppTy', or 'TyVarTy'
287 -- See Note [Respecting definitional equality] (EQ1) about the
288 -- no 'CastTy' requirement
289 --
290 -- 2) Argument type
291
292 | TyConApp
293 TyCon
294 [KindOrType] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
295 -- Invariant: saturated applications of 'FunTyCon' must
296 -- use 'FunTy' and saturated synonyms must use their own
297 -- constructors. However, /unsaturated/ 'FunTyCon's
298 -- do appear as 'TyConApp's.
299 -- Parameters:
300 --
301 -- 1) Type constructor being applied to.
302 --
303 -- 2) Type arguments. Might not have enough type arguments
304 -- here to saturate the constructor.
305 -- Even type synonyms are not necessarily saturated;
306 -- for example unsaturated type synonyms
307 -- can appear as the right hand side of a type synonym.
308
309 | ForAllTy
310 {-# UNPACK #-} !TyCoVarBinder
311 Type -- ^ A Π type.
312
313 | FunTy -- ^ t1 -> t2 Very common, so an important special case
314 -- See Note [Function types]
315 { ft_af :: AnonArgFlag -- Is this (->) or (=>)?
316 , ft_arg :: Type -- Argument type
317 , ft_res :: Type } -- Result type
318
319 | LitTy TyLit -- ^ Type literals are similar to type constructors.
320
321 | CastTy
322 Type
323 KindCoercion -- ^ A kind cast. The coercion is always nominal.
324 -- INVARIANT: The cast is never refl.
325 -- INVARIANT: The Type is not a CastTy (use TransCo instead)
326 -- See Note [Respecting definitional equality] (EQ2) and (EQ3)
327
328 | CoercionTy
329 Coercion -- ^ Injection of a Coercion into a type
330 -- This should only ever be used in the RHS of an AppTy,
331 -- in the list of a TyConApp, when applying a promoted
332 -- GADT data constructor
333
334 deriving Data.Data
335
336 -- NOTE: Other parts of the code assume that type literals do not contain
337 -- types or type variables.
338 data TyLit
339 = NumTyLit Integer
340 | StrTyLit FastString
341 deriving (Eq, Ord, Data.Data)
342
343
344 {- Note [Function types]
345 ~~~~~~~~~~~~~~~~~~~~~~~~
346 FFunTy is the constructor for a function type. Lots of things to say
347 about it!
348
349 * FFunTy is the data constructor, meaning "full function type".
350
351 * The function type constructor (->) has kind
352 (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type LiftedRep
353 mkTyConApp ensure that we convert a saturated application
354 TyConApp (->) [r1,r2,t1,t2] into FunTy t1 t2
355 dropping the 'r1' and 'r2' arguments; they are easily recovered
356 from 't1' and 't2'.
357
358 * The ft_af field says whether or not this is an invisible argument
359 VisArg: t1 -> t2 Ordinary function type
360 InvisArg: t1 => t2 t1 is guaranteed to be a predicate type,
361 i.e. t1 :: Constraint
362 See Note [Types for coercions, predicates, and evidence]
363
364 This visibility info makes no difference in Core; it matters
365 only when we regard the type as a Haskell source type.
366
367 * FunTy is a (unidirectional) pattern synonym that allows
368 positional pattern matching (FunTy arg res), ignoring the
369 ArgFlag.
370 -}
371
372 {- -----------------------
373 Commented out until the pattern match
374 checker can handle it; see #16185
375
376 For now we use the CPP macro #define FunTy FFunTy _
377 (see HsVersions.h) to allow pattern matching on a
378 (positional) FunTy constructor.
379
380 {-# COMPLETE FunTy, TyVarTy, AppTy, TyConApp
381 , ForAllTy, LitTy, CastTy, CoercionTy :: Type #-}
382
383 -- | 'FunTy' is a (uni-directional) pattern synonym for the common
384 -- case where we want to match on the argument/result type, but
385 -- ignoring the AnonArgFlag
386 pattern FunTy :: Type -> Type -> Type
387 pattern FunTy arg res <- FFunTy { ft_arg = arg, ft_res = res }
388
389 End of commented out block
390 ---------------------------------- -}
391
392 {- Note [Types for coercions, predicates, and evidence]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 We treat differently:
395
396 (a) Predicate types
397 Test: isPredTy
398 Binders: DictIds
399 Kind: Constraint
400 Examples: (Eq a), and (a ~ b)
401
402 (b) Coercion types are primitive, unboxed equalities
403 Test: isCoVarTy
404 Binders: CoVars (can appear in coercions)
405 Kind: TYPE (TupleRep [])
406 Examples: (t1 ~# t2) or (t1 ~R# t2)
407
408 (c) Evidence types is the type of evidence manipulated by
409 the type constraint solver.
410 Test: isEvVarType
411 Binders: EvVars
412 Kind: Constraint or TYPE (TupleRep [])
413 Examples: all coercion types and predicate types
414
415 Coercion types and predicate types are mutually exclusive,
416 but evidence types are a superset of both.
417
418 When treated as a user type,
419
420 - Predicates (of kind Constraint) are invisible and are
421 implicitly instantiated
422
423 - Coercion types, and non-pred evidence types (i.e. not
424 of kind Constrain), are just regular old types, are
425 visible, and are not implicitly instantiated.
426
427 In a FunTy { ft_af = InvisArg }, the argument type is always
428 a Predicate type.
429
430 Note [Constraints in kinds]
431 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
432 Do we allow a type constructor to have a kind like
433 S :: Eq a => a -> Type
434
435 No, we do not. Doing so would mean would need a TyConApp like
436 S @k @(d :: Eq k) (ty :: k)
437 and we have no way to build, or decompose, evidence like
438 (d :: Eq k) at the type level.
439
440 But we admit one exception: equality. We /do/ allow, say,
441 MkT :: (a ~ b) => a -> b -> Type a b
442
443 Why? Because we can, without much difficulty. Moreover
444 we can promote a GADT data constructor (see TyCon
445 Note [Promoted data constructors]), like
446 data GT a b where
447 MkGT : a -> a -> GT a a
448 so programmers might reasonably expect to be able to
449 promote MkT as well.
450
451 How does this work?
452
453 * In TcValidity.checkConstraintsOK we reject kinds that
454 have constraints other than (a~b) and (a~~b).
455
456 * In Inst.tcInstInvisibleTyBinder we instantiate a call
457 of MkT by emitting
458 [W] co :: alpha ~# beta
459 and producing the elaborated term
460 MkT @alpha @beta (Eq# alpha beta co)
461 We don't generate a boxed "Wanted"; we generate only a
462 regular old /unboxed/ primitive-equality Wanted, and build
463 the box on the spot.
464
465 * How can we get such a MkT? By promoting a GADT-style data
466 constructor
467 data T a b where
468 MkT :: (a~b) => a -> b -> T a b
469 See DataCon.mkPromotedDataCon
470 and Note [Promoted data constructors] in TyCon
471
472 * We support both homogeneous (~) and heterogeneous (~~)
473 equality. (See Note [The equality types story]
474 in TysPrim for a primer on these equality types.)
475
476 * How do we prevent a MkT having an illegal constraint like
477 Eq a? We check for this at use-sites; see TcHsType.tcTyVar,
478 specifically dc_theta_illegal_constraint.
479
480 * Notice that nothing special happens if
481 K :: (a ~# b) => blah
482 because (a ~# b) is not a predicate type, and is never
483 implicitly instantiated. (Mind you, it's not clear how you
484 could creates a type constructor with such a kind.) See
485 Note [Types for coercions, predicates, and evidence]
486
487 * The existence of promoted MkT with an equality-constraint
488 argument is the (only) reason that the AnonTCB constructor
489 of TyConBndrVis carries an AnonArgFlag (VisArg/InvisArg).
490 For example, when we promote the data constructor
491 MkT :: forall a b. (a~b) => a -> b -> T a b
492 we get a PromotedDataCon with tyConBinders
493 Bndr (a :: Type) (NamedTCB Inferred)
494 Bndr (b :: Type) (NamedTCB Inferred)
495 Bndr (_ :: a ~ b) (AnonTCB InvisArg)
496 Bndr (_ :: a) (AnonTCB VisArg))
497 Bndr (_ :: b) (AnonTCB VisArg))
498
499 * One might reasonably wonder who *unpacks* these boxes once they are
500 made. After all, there is no type-level `case` construct. The
501 surprising answer is that no one ever does. Instead, if a GADT
502 constructor is used on the left-hand side of a type family equation,
503 that occurrence forces GHC to unify the types in question. For
504 example:
505
506 data G a where
507 MkG :: G Bool
508
509 type family F (x :: G a) :: a where
510 F MkG = False
511
512 When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
513 unify F's implicit parameter `a` with Bool. This succeeds, making the equation
514
515 F Bool (MkG @Bool <Bool>) = False
516
517 Note that we never need unpack the coercion. This is because type
518 family equations are *not* parametric in their kind variables. That
519 is, we could have just said
520
521 type family H (x :: G a) :: a where
522 H _ = False
523
524 The presence of False on the RHS also forces `a` to become Bool,
525 giving us
526
527 H Bool _ = False
528
529 The fact that any of this works stems from the lack of phase
530 separation between types and kinds (unlike the very present phase
531 separation between terms and types).
532
533 Once we have the ability to pattern-match on types below top-level,
534 this will no longer cut it, but it seems fine for now.
535
536
537 Note [Arguments to type constructors]
538 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
539 Because of kind polymorphism, in addition to type application we now
540 have kind instantiation. We reuse the same notations to do so.
541
542 For example:
543
544 Just (* -> *) Maybe
545 Right * Nat Zero
546
547 are represented by:
548
549 TyConApp (PromotedDataCon Just) [* -> *, Maybe]
550 TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)]
551
552 Important note: Nat is used as a *kind* and not as a type. This can be
553 confusing, since type-level Nat and kind-level Nat are identical. We
554 use the kind of (PromotedDataCon Right) to know if its arguments are
555 kinds or types.
556
557 This kind instantiation only happens in TyConApp currently.
558
559 Note [Non-trivial definitional equality]
560 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
561 Is Int |> <*> the same as Int? YES! In order to reduce headaches,
562 we decide that any reflexive casts in types are just ignored.
563 (Indeed they must be. See Note [Respecting definitional equality].)
564 More generally, the `eqType` function, which defines Core's type equality
565 relation, ignores casts and coercion arguments, as long as the
566 two types have the same kind. This allows us to be a little sloppier
567 in keeping track of coercions, which is a good thing. It also means
568 that eqType does not depend on eqCoercion, which is also a good thing.
569
570 Why is this sensible? That is, why is something different than α-equivalence
571 appropriate for the implementation of eqType?
572
573 Anything smaller than ~ and homogeneous is an appropriate definition for
574 equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any
575 expression of type τ can be transmuted to one of type σ at any point by
576 casting. The same is true of expressions of type σ. So in some sense, τ and σ
577 are interchangeable.
578
579 But let's be more precise. If we examine the typing rules of FC (say, those in
580 https://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf)
581 there are several places where the same metavariable is used in two different
582 premises to a rule. (For example, see Ty_App.) There is an implicit equality
583 check here. What definition of equality should we use? By convention, we use
584 α-equivalence. Take any rule with one (or more) of these implicit equality
585 checks. Then there is an admissible rule that uses ~ instead of the implicit
586 check, adding in casts as appropriate.
587
588 The only problem here is that ~ is heterogeneous. To make the kinds work out
589 in the admissible rule that uses ~, it is necessary to homogenize the
590 coercions. That is, if we have η : (τ : κ1) ~ (σ : κ2), then we don't use η;
591 we use η |> kind η, which is homogeneous.
592
593 The effect of this all is that eqType, the implementation of the implicit
594 equality check, can use any homogeneous relation that is smaller than ~, as
595 those rules must also be admissible.
596
597 A more drawn out argument around all of this is presented in Section 7.2 of
598 Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf).
599
600 What would go wrong if we insisted on the casts matching? See the beginning of
601 Section 8 in the unpublished paper above. Theoretically, nothing at all goes
602 wrong. But in practical terms, getting the coercions right proved to be
603 nightmarish. And types would explode: during kind-checking, we often produce
604 reflexive kind coercions. When we try to cast by these, mkCastTy just discards
605 them. But if we used an eqType that distinguished between Int and Int |> <*>,
606 then we couldn't discard -- the output of kind-checking would be enormous,
607 and we would need enormous casts with lots of CoherenceCo's to straighten
608 them out.
609
610 Would anything go wrong if eqType respected type families? No, not at all. But
611 that makes eqType rather hard to implement.
612
613 Thus, the guideline for eqType is that it should be the largest
614 easy-to-implement relation that is still smaller than ~ and homogeneous. The
615 precise choice of relation is somewhat incidental, as long as the smart
616 constructors and destructors in Type respect whatever relation is chosen.
617
618 Another helpful principle with eqType is this:
619
620 (EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere.
621
622 This principle also tells us that eqType must relate only types with the
623 same kinds.
624
625 Note [Respecting definitional equality]
626 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
627 Note [Non-trivial definitional equality] introduces the property (EQ).
628 How is this upheld?
629
630 Any function that pattern matches on all the constructors will have to
631 consider the possibility of CastTy. Presumably, those functions will handle
632 CastTy appropriately and we'll be OK.
633
634 More dangerous are the splitXXX functions. Let's focus on splitTyConApp.
635 We don't want it to fail on (T a b c |> co). Happily, if we have
636 (T a b c |> co) `eqType` (T d e f)
637 then co must be reflexive. Why? eqType checks that the kinds are equal, as
638 well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f).
639 By the kind check, we know that (T a b c |> co) and (T d e f) have the same
640 kind. So the only way that co could be non-reflexive is for (T a b c) to have
641 a different kind than (T d e f). But because T's kind is closed (all tycon kinds
642 are closed), the only way for this to happen is that one of the arguments has
643 to differ, leading to a contradiction. Thus, co is reflexive.
644
645 Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
646 about outermost casts to uphold (EQ). Eliminating reflexive casts is done
647 in mkCastTy.
648
649 Unforunately, that's not the end of the story. Consider comparing
650 (T a b c) =? (T a b |> (co -> <Type>)) (c |> co)
651 These two types have the same kind (Type), but the left type is a TyConApp
652 while the right type is not. To handle this case, we say that the right-hand
653 type is ill-formed, requiring an AppTy never to have a casted TyConApp
654 on its left. It is easy enough to pull around the coercions to maintain
655 this invariant, as done in Type.mkAppTy. In the example above, trying to
656 form the right-hand type will instead yield (T a b (c |> co |> sym co) |> <Type>).
657 Both the casts there are reflexive and will be dropped. Huzzah.
658
659 This idea of pulling coercions to the right works for splitAppTy as well.
660
661 However, there is one hiccup: it's possible that a coercion doesn't relate two
662 Pi-types. For example, if we have @type family Fun a b where Fun a b = a -> b@,
663 then we might have (T :: Fun Type Type) and (T |> axFun) Int. That axFun can't
664 be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
665 `eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
666 our (EQ) property.
667
668 Lastly, in order to detect reflexive casts reliably, we must make sure not
669 to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
670
671 In sum, in order to uphold (EQ), we need the following three invariants:
672
673 (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
674 cast is one that relates either a FunTy to a FunTy or a
675 ForAllTy to a ForAllTy.
676 (EQ2) No reflexive casts in CastTy.
677 (EQ3) No nested CastTys.
678 (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
679 See Note [Weird typing rule for ForAllTy] in Type.
680
681 These invariants are all documented above, in the declaration for Type.
682
683 Note [Unused coercion variable in ForAllTy]
684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
685 Suppose we have
686 \(co:t1 ~ t2). e
687
688 What type should we give to this expression?
689 (1) forall (co:t1 ~ t2) -> t
690 (2) (t1 ~ t2) -> t
691
692 If co is used in t, (1) should be the right choice.
693 if co is not used in t, we would like to have (1) and (2) equivalent.
694
695 However, we want to keep eqType simple and don't want eqType (1) (2) to return
696 True in any case.
697
698 We decide to always construct (2) if co is not used in t.
699
700 Thus in mkLamType, we check whether the variable is a coercion
701 variable (of type (t1 ~# t2), and whether it is un-used in the
702 body. If so, it returns a FunTy instead of a ForAllTy.
703
704 There are cases we want to skip the check. For example, the check is
705 unnecessary when it is known from the context that the input variable
706 is a type variable. In those cases, we use mkForAllTy.
707
708 -}
709
710 -- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
711 -- Note [Type checking recursive type and class declarations] in
712 -- TcTyClsDecls
713 type KnotTied ty = ty
714
715 {- **********************************************************************
716 * *
717 TyCoBinder and ArgFlag
718 * *
719 ********************************************************************** -}
720
721 -- | A 'TyCoBinder' represents an argument to a function. TyCoBinders can be
722 -- dependent ('Named') or nondependent ('Anon'). They may also be visible or
723 -- not. See Note [TyCoBinders]
724 data TyCoBinder
725 = Named TyCoVarBinder -- A type-lambda binder
726 | Anon AnonArgFlag Type -- A term-lambda binder. Type here can be CoercionTy.
727 -- Visibility is determined by the AnonArgFlag
728 deriving Data.Data
729
730 -- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder'
731 -- in the 'Named' field.
732 type TyBinder = TyCoBinder
733
734 -- | Remove the binder's variable from the set, if the binder has
735 -- a variable.
736 delBinderVar :: VarSet -> TyCoVarBinder -> VarSet
737 delBinderVar vars (Bndr tv _) = vars `delVarSet` tv
738
739 -- | Does this binder bind an invisible argument?
740 isInvisibleBinder :: TyCoBinder -> Bool
741 isInvisibleBinder (Named (Bndr _ vis)) = isInvisibleArgFlag vis
742 isInvisibleBinder (Anon InvisArg _) = True
743 isInvisibleBinder (Anon VisArg _) = False
744
745 -- | Does this binder bind a visible argument?
746 isVisibleBinder :: TyCoBinder -> Bool
747 isVisibleBinder = not . isInvisibleBinder
748
749 isNamedBinder :: TyCoBinder -> Bool
750 isNamedBinder (Named {}) = True
751 isNamedBinder (Anon {}) = False
752
753 -- | If its a named binder, is the binder a tyvar?
754 -- Returns True for nondependent binder.
755 -- This check that we're really returning a *Ty*Binder (as opposed to a
756 -- coercion binder). That way, if/when we allow coercion quantification
757 -- in more places, we'll know we missed updating some function.
758 isTyBinder :: TyCoBinder -> Bool
759 isTyBinder (Named bnd) = isTyVarBinder bnd
760 isTyBinder _ = True
761
762 {- Note [TyCoBinders]
763 ~~~~~~~~~~~~~~~~~~~
764 A ForAllTy contains a TyCoVarBinder. But a type can be decomposed
765 to a telescope consisting of a [TyCoBinder]
766
767 A TyCoBinder represents the type of binders -- that is, the type of an
768 argument to a Pi-type. GHC Core currently supports two different
769 Pi-types:
770
771 * A non-dependent function type,
772 written with ->, e.g. ty1 -> ty2
773 represented as FunTy ty1 ty2. These are
774 lifted to Coercions with the corresponding FunCo.
775
776 * A dependent compile-time-only polytype,
777 written with forall, e.g. forall (a:*). ty
778 represented as ForAllTy (Bndr a v) ty
779
780 Both Pi-types classify terms/types that take an argument. In other
781 words, if `x` is either a function or a polytype, `x arg` makes sense
782 (for an appropriate `arg`).
783
784
785 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
786 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
787 * A ForAllTy (used for both types and kinds) contains a TyCoVarBinder.
788 Each TyCoVarBinder
789 Bndr a tvis
790 is equipped with tvis::ArgFlag, which says whether or not arguments
791 for this binder should be visible (explicit) in source Haskell.
792
793 * A TyCon contains a list of TyConBinders. Each TyConBinder
794 Bndr a cvis
795 is equipped with cvis::TyConBndrVis, which says whether or not type
796 and kind arguments for this TyCon should be visible (explicit) in
797 source Haskell.
798
799 This table summarises the visibility rules:
800 ---------------------------------------------------------------------------------------
801 | Occurrences look like this
802 | GHC displays type as in Haskell source code
803 |--------------------------------------------------------------------------------------
804 | Bndr a tvis :: TyCoVarBinder, in the binder of ForAllTy for a term
805 | tvis :: ArgFlag
806 | tvis = Inferred: f :: forall {a}. type Arg not allowed: f
807 f :: forall {co}. type Arg not allowed: f
808 | tvis = Specified: f :: forall a. type Arg optional: f or f @Int
809 | tvis = Required: T :: forall k -> type Arg required: T *
810 | This last form is illegal in terms: See Note [No Required TyCoBinder in terms]
811 |
812 | Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon
813 | cvis :: TyConBndrVis
814 | cvis = AnonTCB: T :: kind -> kind Required: T *
815 | cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T
816 | T :: forall {co}. kind Arg not allowed: T
817 | cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T
818 | cvis = NamedTCB Required: T :: forall k -> kind Required: T *
819 ---------------------------------------------------------------------------------------
820
821 [1] In types, in the Specified case, it would make sense to allow
822 optional kind applications, thus (T @*), but we have not
823 yet implemented that
824
825 ---- In term declarations ----
826
827 * Inferred. Function defn, with no signature: f1 x = x
828 We infer f1 :: forall {a}. a -> a, with 'a' Inferred
829 It's Inferred because it doesn't appear in any
830 user-written signature for f1
831
832 * Specified. Function defn, with signature (implicit forall):
833 f2 :: a -> a; f2 x = x
834 So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified
835 even though 'a' is not bound in the source code by an explicit forall
836
837 * Specified. Function defn, with signature (explicit forall):
838 f3 :: forall a. a -> a; f3 x = x
839 So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified
840
841 * Inferred/Specified. Function signature with inferred kind polymorphism.
842 f4 :: a b -> Int
843 So 'f4' gets the type f4 :: forall {k} (a:k->*) (b:k). a b -> Int
844 Here 'k' is Inferred (it's not mentioned in the type),
845 but 'a' and 'b' are Specified.
846
847 * Specified. Function signature with explicit kind polymorphism
848 f5 :: a (b :: k) -> Int
849 This time 'k' is Specified, because it is mentioned explicitly,
850 so we get f5 :: forall (k:*) (a:k->*) (b:k). a b -> Int
851
852 * Similarly pattern synonyms:
853 Inferred - from inferred types (e.g. no pattern type signature)
854 - or from inferred kind polymorphism
855
856 ---- In type declarations ----
857
858 * Inferred (k)
859 data T1 a b = MkT1 (a b)
860 Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> *
861 The kind variable 'k' is Inferred, since it is not mentioned
862
863 Note that 'a' and 'b' correspond to /Anon/ TyCoBinders in T1's kind,
864 and Anon binders don't have a visibility flag. (Or you could think
865 of Anon having an implicit Required flag.)
866
867 * Specified (k)
868 data T2 (a::k->*) b = MkT (a b)
869 Here T's kind is T :: forall (k:*). (k->*) -> k -> *
870 The kind variable 'k' is Specified, since it is mentioned in
871 the signature.
872
873 * Required (k)
874 data T k (a::k->*) b = MkT (a b)
875 Here T's kind is T :: forall k:* -> (k->*) -> k -> *
876 The kind is Required, since it bound in a positional way in T's declaration
877 Every use of T must be explicitly applied to a kind
878
879 * Inferred (k1), Specified (k)
880 data T a b (c :: k) = MkT (a b) (Proxy c)
881 Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
882 So 'k' is Specified, because it appears explicitly,
883 but 'k1' is Inferred, because it does not
884
885 Generally, in the list of TyConBinders for a TyCon,
886
887 * Inferred arguments always come first
888 * Specified, Anon and Required can be mixed
889
890 e.g.
891 data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ...
892
893 Here Foo's TyConBinders are
894 [Required 'a', Specified 'b', Anon]
895 and its kind prints as
896 Foo :: forall a -> forall b. (a -> b -> Type) -> Type
897
898 See also Note [Required, Specified, and Inferred for types] in TcTyClsDecls
899
900 ---- Printing -----
901
902 We print forall types with enough syntax to tell you their visibility
903 flag. But this is not source Haskell, and these types may not all
904 be parsable.
905
906 Specified: a list of Specified binders is written between `forall` and `.`:
907 const :: forall a b. a -> b -> a
908
909 Inferred: with -fprint-explicit-foralls, Inferred binders are written
910 in braces:
911 f :: forall {k} (a:k). S k a -> Int
912 Otherwise, they are printed like Specified binders.
913
914 Required: binders are put between `forall` and `->`:
915 T :: forall k -> *
916
917 ---- Other points -----
918
919 * In classic Haskell, all named binders (that is, the type variables in
920 a polymorphic function type f :: forall a. a -> a) have been Inferred.
921
922 * Inferred variables correspond to "generalized" variables from the
923 Visible Type Applications paper (ESOP'16).
924
925 Note [No Required TyCoBinder in terms]
926 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
927 We don't allow Required foralls for term variables, including pattern
928 synonyms and data constructors. Why? Because then an application
929 would need a /compulsory/ type argument (possibly without an "@"?),
930 thus (f Int); and we don't have concrete syntax for that.
931
932 We could change this decision, but Required, Named TyCoBinders are rare
933 anyway. (Most are Anons.)
934
935 However the type of a term can (just about) have a required quantifier;
936 see Note [Required quantifiers in the type of a term] in TcExpr.
937 -}
938
939
940 {- **********************************************************************
941 * *
942 PredType
943 * *
944 ********************************************************************** -}
945
946
947 -- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
948 -- the Haskell predicate @p@, where a predicate is what occurs before
949 -- the @=>@ in a Haskell type.
950 --
951 -- We use 'PredType' as documentation to mark those types that we guarantee to have
952 -- this kind.
953 --
954 -- It can be expanded into its representation, but:
955 --
956 -- * The type checker must treat it as opaque
957 --
958 -- * The rest of the compiler treats it as transparent
959 --
960 -- Consider these examples:
961 --
962 -- > f :: (Eq a) => a -> Int
963 -- > g :: (?x :: Int -> Int) => a -> Int
964 -- > h :: (r\l) => {r} => {l::Int | r}
965 --
966 -- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
967 type PredType = Type
968
969 -- | A collection of 'PredType's
970 type ThetaType = [PredType]
971
972 {-
973 (We don't support TREX records yet, but the setup is designed
974 to expand to allow them.)
975
976 A Haskell qualified type, such as that for f,g,h above, is
977 represented using
978 * a FunTy for the double arrow
979 * with a type of kind Constraint as the function argument
980
981 The predicate really does turn into a real extra argument to the
982 function. If the argument has type (p :: Constraint) then the predicate p is
983 represented by evidence of type p.
984
985
986 %************************************************************************
987 %* *
988 Simple constructors
989 %* *
990 %************************************************************************
991
992 These functions are here so that they can be used by TysPrim,
993 which in turn is imported by Type
994 -}
995
996 mkTyVarTy :: TyVar -> Type
997 mkTyVarTy v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) )
998 TyVarTy v
999
1000 mkTyVarTys :: [TyVar] -> [Type]
1001 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
1002
1003 mkTyCoVarTy :: TyCoVar -> Type
1004 mkTyCoVarTy v
1005 | isTyVar v
1006 = TyVarTy v
1007 | otherwise
1008 = CoercionTy (CoVarCo v)
1009
1010 mkTyCoVarTys :: [TyCoVar] -> [Type]
1011 mkTyCoVarTys = map mkTyCoVarTy
1012
1013 infixr 3 `mkFunTy`, `mkVisFunTy`, `mkInvisFunTy` -- Associates to the right
1014
1015 mkFunTy :: AnonArgFlag -> Type -> Type -> Type
1016 mkFunTy af arg res = FunTy { ft_af = af, ft_arg = arg, ft_res = res }
1017
1018 mkVisFunTy, mkInvisFunTy :: Type -> Type -> Type
1019 mkVisFunTy = mkFunTy VisArg
1020 mkInvisFunTy = mkFunTy InvisArg
1021
1022 -- | Make nested arrow types
1023 mkVisFunTys, mkInvisFunTys :: [Type] -> Type -> Type
1024 mkVisFunTys tys ty = foldr mkVisFunTy ty tys
1025 mkInvisFunTys tys ty = foldr mkInvisFunTy ty tys
1026
1027 -- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder
1028 -- See Note [Unused coercion variable in ForAllTy]
1029 mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
1030 mkForAllTy tv vis ty = ForAllTy (Bndr tv vis) ty
1031
1032 -- | Wraps foralls over the type using the provided 'TyCoVar's from left to right
1033 mkForAllTys :: [TyCoVarBinder] -> Type -> Type
1034 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
1035
1036 mkPiTy:: TyCoBinder -> Type -> Type
1037 mkPiTy (Anon af ty1) ty2 = FunTy { ft_af = af, ft_arg = ty1, ft_res = ty2 }
1038 mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty
1039
1040 mkPiTys :: [TyCoBinder] -> Type -> Type
1041 mkPiTys tbs ty = foldr mkPiTy ty tbs
1042
1043 -- | Create the plain type constructor type which has been applied to no type arguments at all.
1044 mkTyConTy :: TyCon -> Type
1045 mkTyConTy tycon = TyConApp tycon []
1046
1047 {-
1048 Some basic functions, put here to break loops eg with the pretty printer
1049 -}
1050
1051 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
1052 -- @kindRep * = LiftedRep@; Panics if this is not possible.
1053 -- Treats * and Constraint as the same
1054 kindRep :: HasDebugCallStack => Kind -> Type
1055 kindRep k = case kindRep_maybe k of
1056 Just r -> r
1057 Nothing -> pprPanic "kindRep" (ppr k)
1058
1059 -- | Given a kind (TYPE rr), extract its RuntimeRep classifier rr.
1060 -- For example, @kindRep_maybe * = Just LiftedRep@
1061 -- Returns 'Nothing' if the kind is not of form (TYPE rr)
1062 -- Treats * and Constraint as the same
1063 kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
1064 kindRep_maybe kind
1065 | Just kind' <- coreView kind = kindRep_maybe kind'
1066 | TyConApp tc [arg] <- kind
1067 , tc `hasKey` tYPETyConKey = Just arg
1068 | otherwise = Nothing
1069
1070 -- | This version considers Constraint to be the same as *. Returns True
1071 -- if the argument is equivalent to Type/Constraint and False otherwise.
1072 -- See Note [Kind Constraint and kind Type]
1073 isLiftedTypeKind :: Kind -> Bool
1074 isLiftedTypeKind kind
1075 = case kindRep_maybe kind of
1076 Just rep -> isLiftedRuntimeRep rep
1077 Nothing -> False
1078
1079 -- | Returns True if the kind classifies unlifted types and False otherwise.
1080 -- Note that this returns False for levity-polymorphic kinds, which may
1081 -- be specialized to a kind that classifies unlifted types.
1082 isUnliftedTypeKind :: Kind -> Bool
1083 isUnliftedTypeKind kind
1084 = case kindRep_maybe kind of
1085 Just rep -> isUnliftedRuntimeRep rep
1086 Nothing -> False
1087
1088 isLiftedRuntimeRep :: Type -> Bool
1089 -- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep
1090 -- False of type variables (a :: RuntimeRep)
1091 -- and of other reps e.g. (IntRep :: RuntimeRep)
1092 isLiftedRuntimeRep rep
1093 | Just rep' <- coreView rep = isLiftedRuntimeRep rep'
1094 | TyConApp rr_tc args <- rep
1095 , rr_tc `hasKey` liftedRepDataConKey = ASSERT( null args ) True
1096 | otherwise = False
1097
1098 isUnliftedRuntimeRep :: Type -> Bool
1099 -- True of definitely-unlifted RuntimeReps
1100 -- False of (LiftedRep :: RuntimeRep)
1101 -- and of variables (a :: RuntimeRep)
1102 isUnliftedRuntimeRep rep
1103 | Just rep' <- coreView rep = isUnliftedRuntimeRep rep'
1104 | TyConApp rr_tc _ <- rep -- NB: args might be non-empty
1105 -- e.g. TupleRep [r1, .., rn]
1106 = isPromotedDataCon rr_tc && not (rr_tc `hasKey` liftedRepDataConKey)
1107 -- Avoid searching all the unlifted RuntimeRep type cons
1108 -- In the RuntimeRep data type, only LiftedRep is lifted
1109 -- But be careful of type families (F tys) :: RuntimeRep
1110 | otherwise {- Variables, applications -}
1111 = False
1112
1113 -- | Is this the type 'RuntimeRep'?
1114 isRuntimeRepTy :: Type -> Bool
1115 isRuntimeRepTy ty | Just ty' <- coreView ty = isRuntimeRepTy ty'
1116 isRuntimeRepTy (TyConApp tc args)
1117 | tc `hasKey` runtimeRepTyConKey = ASSERT( null args ) True
1118 isRuntimeRepTy _ = False
1119
1120 -- | Is a tyvar of type 'RuntimeRep'?
1121 isRuntimeRepVar :: TyVar -> Bool
1122 isRuntimeRepVar = isRuntimeRepTy . tyVarKind
1123
1124 {-
1125 %************************************************************************
1126 %* *
1127 Coercions
1128 %* *
1129 %************************************************************************
1130 -}
1131
1132 -- | A 'Coercion' is concrete evidence of the equality/convertibility
1133 -- of two types.
1134
1135 -- If you edit this type, you may need to update the GHC formalism
1136 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
1137 data Coercion
1138 -- Each constructor has a "role signature", indicating the way roles are
1139 -- propagated through coercions.
1140 -- - P, N, and R stand for coercions of the given role
1141 -- - e stands for a coercion of a specific unknown role
1142 -- (think "role polymorphism")
1143 -- - "e" stands for an explicit role parameter indicating role e.
1144 -- - _ stands for a parameter that is not a Role or Coercion.
1145
1146 -- These ones mirror the shape of types
1147 = -- Refl :: _ -> N
1148 Refl Type -- See Note [Refl invariant]
1149 -- Invariant: applications of (Refl T) to a bunch of identity coercions
1150 -- always show up as Refl.
1151 -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
1152
1153 -- Applications of (Refl T) to some coercions, at least one of
1154 -- which is NOT the identity, show up as TyConAppCo.
1155 -- (They may not be fully saturated however.)
1156 -- ConAppCo coercions (like all coercions other than Refl)
1157 -- are NEVER the identity.
1158
1159 -- Use (GRefl Representational ty MRefl), not (SubCo (Refl ty))
1160
1161 -- GRefl :: "e" -> _ -> Maybe N -> e
1162 -- See Note [Generalized reflexive coercion]
1163 | GRefl Role Type MCoercionN -- See Note [Refl invariant]
1164 -- Use (Refl ty), not (GRefl Nominal ty MRefl)
1165 -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _))
1166
1167 -- These ones simply lift the correspondingly-named
1168 -- Type constructors into Coercions
1169
1170 -- TyConAppCo :: "e" -> _ -> ?? -> e
1171 -- See Note [TyConAppCo roles]
1172 | TyConAppCo Role TyCon [Coercion] -- lift TyConApp
1173 -- The TyCon is never a synonym;
1174 -- we expand synonyms eagerly
1175 -- But it can be a type function
1176
1177 | AppCo Coercion CoercionN -- lift AppTy
1178 -- AppCo :: e -> N -> e
1179
1180 -- See Note [Forall coercions]
1181 | ForAllCo TyCoVar KindCoercion Coercion
1182 -- ForAllCo :: _ -> N -> e -> e
1183
1184 | FunCo Role Coercion Coercion -- lift FunTy
1185 -- FunCo :: "e" -> e -> e -> e
1186 -- Note: why doesn't FunCo have a AnonArgFlag, like FunTy?
1187 -- Because the AnonArgFlag has no impact on Core; it is only
1188 -- there to guide implicit instantiation of Haskell source
1189 -- types, and that is irrelevant for coercions, which are
1190 -- Core-only.
1191
1192 -- These are special
1193 | CoVarCo CoVar -- :: _ -> (N or R)
1194 -- result role depends on the tycon of the variable's type
1195
1196 -- AxiomInstCo :: e -> _ -> [N] -> e
1197 | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
1198 -- See also [CoAxiom index]
1199 -- The coercion arguments always *precisely* saturate
1200 -- arity of (that branch of) the CoAxiom. If there are
1201 -- any left over, we use AppCo.
1202 -- See [Coercion axioms applied to coercions]
1203
1204 | AxiomRuleCo CoAxiomRule [Coercion]
1205 -- AxiomRuleCo is very like AxiomInstCo, but for a CoAxiomRule
1206 -- The number coercions should match exactly the expectations
1207 -- of the CoAxiomRule (i.e., the rule is fully saturated).
1208
1209 | UnivCo UnivCoProvenance Role Type Type
1210 -- :: _ -> "e" -> _ -> _ -> e
1211
1212 | SymCo Coercion -- :: e -> e
1213 | TransCo Coercion Coercion -- :: e -> e -> e
1214
1215 | NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
1216 -- :: "e" -> _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles])
1217 -- Using NthCo on a ForAllCo gives an N coercion always
1218 -- See Note [NthCo and newtypes]
1219 --
1220 -- Invariant: (NthCo r i co), it is always the case that r = role of (Nth i co)
1221 -- That is: the role of the entire coercion is redundantly cached here.
1222 -- See Note [NthCo Cached Roles]
1223
1224 | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
1225 -- :: _ -> N -> N
1226 | InstCo Coercion CoercionN
1227 -- :: e -> N -> e
1228 -- See Note [InstCo roles]
1229
1230 -- Extract a kind coercion from a (heterogeneous) type coercion
1231 -- NB: all kind coercions are Nominal
1232 | KindCo Coercion
1233 -- :: e -> N
1234
1235 | SubCo CoercionN -- Turns a ~N into a ~R
1236 -- :: N -> R
1237
1238 | HoleCo CoercionHole -- ^ See Note [Coercion holes]
1239 -- Only present during typechecking
1240 deriving Data.Data
1241
1242 type CoercionN = Coercion -- always nominal
1243 type CoercionR = Coercion -- always representational
1244 type CoercionP = Coercion -- always phantom
1245 type KindCoercion = CoercionN -- always nominal
1246
1247 -- | A semantically more meaningful type to represent what may or may not be a
1248 -- useful 'Coercion'.
1249 data MCoercion
1250 = MRefl
1251 -- A trivial Reflexivity coercion
1252 | MCo Coercion
1253 -- Other coercions
1254 deriving Data.Data
1255 type MCoercionR = MCoercion
1256 type MCoercionN = MCoercion
1257
1258 instance Outputable MCoercion where
1259 ppr MRefl = text "MRefl"
1260 ppr (MCo co) = text "MCo" <+> ppr co
1261
1262 {-
1263 Note [Refl invariant]
1264 ~~~~~~~~~~~~~~~~~~~~~
1265 Invariant 1:
1266
1267 Coercions have the following invariant
1268 Refl (similar for GRefl r ty MRefl) is always lifted as far as possible.
1269
1270 You might think that a consequencs is:
1271 Every identity coercions has Refl at the root
1272
1273 But that's not quite true because of coercion variables. Consider
1274 g where g :: Int~Int
1275 Left h where h :: Maybe Int ~ Maybe Int
1276 etc. So the consequence is only true of coercions that
1277 have no coercion variables.
1278
1279 Note [Generalized reflexive coercion]
1280 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1281
1282 GRefl is a generalized reflexive coercion (see #15192). It wraps a kind
1283 coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing
1284 rules for GRefl:
1285
1286 ty : k1
1287 ------------------------------------
1288 GRefl r ty MRefl: ty ~r ty
1289
1290 ty : k1 co :: k1 ~ k2
1291 ------------------------------------
1292 GRefl r ty (MCo co) : ty ~r ty |> co
1293
1294 Consider we have
1295
1296 g1 :: s ~r t
1297 s :: k1
1298 g2 :: k1 ~ k2
1299
1300 and we want to construct a coercions co which has type
1301
1302 (s |> g2) ~r t
1303
1304 We can define
1305
1306 co = Sym (GRefl r s g2) ; g1
1307
1308 It is easy to see that
1309
1310 Refl == GRefl Nominal ty MRefl :: ty ~n ty
1311
1312 A nominal reflexive coercion is quite common, so we keep the special form Refl to
1313 save allocation.
1314
1315 Note [Coercion axioms applied to coercions]
1316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1317 The reason coercion axioms can be applied to coercions and not just
1318 types is to allow for better optimization. There are some cases where
1319 we need to be able to "push transitivity inside" an axiom in order to
1320 expose further opportunities for optimization.
1321
1322 For example, suppose we have
1323
1324 C a : t[a] ~ F a
1325 g : b ~ c
1326
1327 and we want to optimize
1328
1329 sym (C b) ; t[g] ; C c
1330
1331 which has the kind
1332
1333 F b ~ F c
1334
1335 (stopping through t[b] and t[c] along the way).
1336
1337 We'd like to optimize this to just F g -- but how? The key is
1338 that we need to allow axioms to be instantiated by *coercions*,
1339 not just by types. Then we can (in certain cases) push
1340 transitivity inside the axiom instantiations, and then react
1341 opposite-polarity instantiations of the same axiom. In this
1342 case, e.g., we match t[g] against the LHS of (C c)'s kind, to
1343 obtain the substitution a |-> g (note this operation is sort
1344 of the dual of lifting!) and hence end up with
1345
1346 C g : t[b] ~ F c
1347
1348 which indeed has the same kind as t[g] ; C c.
1349
1350 Now we have
1351
1352 sym (C b) ; C g
1353
1354 which can be optimized to F g.
1355
1356 Note [CoAxiom index]
1357 ~~~~~~~~~~~~~~~~~~~~
1358 A CoAxiom has 1 or more branches. Each branch has contains a list
1359 of the free type variables in that branch, the LHS type patterns,
1360 and the RHS type for that branch. When we apply an axiom to a list
1361 of coercions, we must choose which branch of the axiom we wish to
1362 use, as the different branches may have different numbers of free
1363 type variables. (The number of type patterns is always the same
1364 among branches, but that doesn't quite concern us here.)
1365
1366 The Int in the AxiomInstCo constructor is the 0-indexed number
1367 of the chosen branch.
1368
1369 Note [Forall coercions]
1370 ~~~~~~~~~~~~~~~~~~~~~~~
1371 Constructing coercions between forall-types can be a bit tricky,
1372 because the kinds of the bound tyvars can be different.
1373
1374 The typing rule is:
1375
1376
1377 kind_co : k1 ~ k2
1378 tv1:k1 |- co : t1 ~ t2
1379 -------------------------------------------------------------------
1380 ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
1381 all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
1382
1383 First, the TyCoVar stored in a ForAllCo is really an optimisation: this field
1384 should be a Name, as its kind is redundant. Thinking of the field as a Name
1385 is helpful in understanding what a ForAllCo means.
1386 The kind of TyCoVar always matches the left-hand kind of the coercion.
1387
1388 The idea is that kind_co gives the two kinds of the tyvar. See how, in the
1389 conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
1390
1391 Of course, a type variable can't have different kinds at the same time. So,
1392 we arbitrarily prefer the first kind when using tv1 in the inner coercion
1393 co, which shows that t1 equals t2.
1394
1395 The last wrinkle is that we need to fix the kinds in the conclusion. In
1396 t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
1397 the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
1398 (tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
1399 mentions the same name with different kinds, but it *is* well-kinded, noting
1400 that `(tv1:k2) |> sym kind_co` has kind k1.
1401
1402 This all really would work storing just a Name in the ForAllCo. But we can't
1403 add Names to, e.g., VarSets, and there generally is just an impedance mismatch
1404 in a bunch of places. So we use tv1. When we need tv2, we can use
1405 setTyVarKind.
1406
1407 Note [Predicate coercions]
1408 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1409 Suppose we have
1410 g :: a~b
1411 How can we coerce between types
1412 ([c]~a) => [a] -> c
1413 and
1414 ([c]~b) => [b] -> c
1415 where the equality predicate *itself* differs?
1416
1417 Answer: we simply treat (~) as an ordinary type constructor, so these
1418 types really look like
1419
1420 ((~) [c] a) -> [a] -> c
1421 ((~) [c] b) -> [b] -> c
1422
1423 So the coercion between the two is obviously
1424
1425 ((~) [c] g) -> [g] -> c
1426
1427 Another way to see this to say that we simply collapse predicates to
1428 their representation type (see Type.coreView and Type.predTypeRep).
1429
1430 This collapse is done by mkPredCo; there is no PredCo constructor
1431 in Coercion. This is important because we need Nth to work on
1432 predicates too:
1433 Nth 1 ((~) [c] g) = g
1434 See Simplify.simplCoercionF, which generates such selections.
1435
1436 Note [Roles]
1437 ~~~~~~~~~~~~
1438 Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
1439 in #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
1440 http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
1441
1442 Here is one way to phrase the problem:
1443
1444 Given:
1445 newtype Age = MkAge Int
1446 type family F x
1447 type instance F Age = Bool
1448 type instance F Int = Char
1449
1450 This compiles down to:
1451 axAge :: Age ~ Int
1452 axF1 :: F Age ~ Bool
1453 axF2 :: F Int ~ Char
1454
1455 Then, we can make:
1456 (sym (axF1) ; F axAge ; axF2) :: Bool ~ Char
1457
1458 Yikes!
1459
1460 The solution is _roles_, as articulated in "Generative Type Abstraction and
1461 Type-level Computation" (POPL 2010), available at
1462 http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf
1463
1464 The specification for roles has evolved somewhat since that paper. For the
1465 current full details, see the documentation in docs/core-spec. Here are some
1466 highlights.
1467
1468 We label every equality with a notion of type equivalence, of which there are
1469 three options: Nominal, Representational, and Phantom. A ground type is
1470 nominally equivalent only with itself. A newtype (which is considered a ground
1471 type in Haskell) is representationally equivalent to its representation.
1472 Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
1473 to denote the equivalences.
1474
1475 The axioms above would be:
1476 axAge :: Age ~R Int
1477 axF1 :: F Age ~N Bool
1478 axF2 :: F Age ~N Char
1479
1480 Then, because transitivity applies only to coercions proving the same notion
1481 of equivalence, the above construction is impossible.
1482
1483 However, there is still an escape hatch: we know that any two types that are
1484 nominally equivalent are representationally equivalent as well. This is what
1485 the form SubCo proves -- it "demotes" a nominal equivalence into a
1486 representational equivalence. So, it would seem the following is possible:
1487
1488 sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG
1489
1490 What saves us here is that the arguments to a type function F, lifted into a
1491 coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
1492 we are safe.
1493
1494 Roles are attached to parameters to TyCons. When lifting a TyCon into a
1495 coercion (through TyConAppCo), we need to ensure that the arguments to the
1496 TyCon respect their roles. For example:
1497
1498 data T a b = MkT a (F b)
1499
1500 If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
1501 that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
1502 the type function F branches on b's *name*, not representation. So, we say
1503 that 'a' has role Representational and 'b' has role Nominal. The third role,
1504 Phantom, is for parameters not used in the type's definition. Given the
1505 following definition
1506
1507 data Q a = MkQ Int
1508
1509 the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
1510 can construct the coercion Bool ~P Char (using UnivCo).
1511
1512 See the paper cited above for more examples and information.
1513
1514 Note [TyConAppCo roles]
1515 ~~~~~~~~~~~~~~~~~~~~~~~
1516 The TyConAppCo constructor has a role parameter, indicating the role at
1517 which the coercion proves equality. The choice of this parameter affects
1518 the required roles of the arguments of the TyConAppCo. To help explain
1519 it, assume the following definition:
1520
1521 type instance F Int = Bool -- Axiom axF : F Int ~N Bool
1522 newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
1523 data Foo a = MkFoo a -- Role on Foo's parameter is Representational
1524
1525 TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
1526 For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
1527 So that Foo Age ~N Foo Int does *not* hold.
1528
1529 TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
1530 TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
1531 For (TyConAppCo Representational), all arguments must have the roles
1532 corresponding to the result of tyConRoles on the TyCon. This is the
1533 whole point of having roles on the TyCon to begin with. So, we can
1534 have Foo Age ~R Foo Int, if Foo's parameter has role R.
1535
1536 If a Representational TyConAppCo is over-saturated (which is otherwise fine),
1537 the spill-over arguments must all be at Nominal. This corresponds to the
1538 behavior for AppCo.
1539
1540 TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
1541 All arguments must have role Phantom. This one isn't strictly
1542 necessary for soundness, but this choice removes ambiguity.
1543
1544 The rules here dictate the roles of the parameters to mkTyConAppCo
1545 (should be checked by Lint).
1546
1547 Note [NthCo and newtypes]
1548 ~~~~~~~~~~~~~~~~~~~~~~~~~
1549 Suppose we have
1550
1551 newtype N a = MkN Int
1552 type role N representational
1553
1554 This yields axiom
1555
1556 NTCo:N :: forall a. N a ~R Int
1557
1558 We can then build
1559
1560 co :: forall a b. N a ~R N b
1561 co = NTCo:N a ; sym (NTCo:N b)
1562
1563 for any `a` and `b`. Because of the role annotation on N, if we use
1564 NthCo, we'll get out a representational coercion. That is:
1565
1566 NthCo r 0 co :: forall a b. a ~R b
1567
1568 Yikes! Clearly, this is terrible. The solution is simple: forbid
1569 NthCo to be used on newtypes if the internal coercion is representational.
1570
1571 This is not just some corner case discovered by a segfault somewhere;
1572 it was discovered in the proof of soundness of roles and described
1573 in the "Safe Coercions" paper (ICFP '14).
1574
1575 Note [NthCo Cached Roles]
1576 ~~~~~~~~~~~~~~~~~~~~~~~~~
1577 Why do we cache the role of NthCo in the NthCo constructor?
1578 Because computing role(Nth i co) involves figuring out that
1579
1580 co :: T tys1 ~ T tys2
1581
1582 using coercionKind, and finding (coercionRole co), and then looking
1583 at the tyConRoles of T. Avoiding bad asymptotic behaviour here means
1584 we have to compute the kind and role of a coercion simultaneously,
1585 which makes the code complicated and inefficient.
1586
1587 This only happens for NthCo. Caching the role solves the problem, and
1588 allows coercionKind and coercionRole to be simple.
1589
1590 See #11735
1591
1592 Note [InstCo roles]
1593 ~~~~~~~~~~~~~~~~~~~
1594 Here is (essentially) the typing rule for InstCo:
1595
1596 g :: (forall a. t1) ~r (forall a. t2)
1597 w :: s1 ~N s2
1598 ------------------------------- InstCo
1599 InstCo g w :: (t1 [a |-> s1]) ~r (t2 [a |-> s2])
1600
1601 Note that the Coercion w *must* be nominal. This is necessary
1602 because the variable a might be used in a "nominal position"
1603 (that is, a place where role inference would require a nominal
1604 role) in t1 or t2. If we allowed w to be representational, we
1605 could get bogus equalities.
1606
1607 A more nuanced treatment might be able to relax this condition
1608 somewhat, by checking if t1 and/or t2 use their bound variables
1609 in nominal ways. If not, having w be representational is OK.
1610
1611
1612 %************************************************************************
1613 %* *
1614 UnivCoProvenance
1615 %* *
1616 %************************************************************************
1617
1618 A UnivCo is a coercion whose proof does not directly express its role
1619 and kind (indeed for some UnivCos, like UnsafeCoerceProv, there /is/
1620 no proof).
1621
1622 The different kinds of UnivCo are described by UnivCoProvenance. Really
1623 each is entirely separate, but they all share the need to represent their
1624 role and kind, which is done in the UnivCo constructor.
1625
1626 -}
1627
1628 -- | For simplicity, we have just one UnivCo that represents a coercion from
1629 -- some type to some other type, with (in general) no restrictions on the
1630 -- type. The UnivCoProvenance specifies more exactly what the coercion really
1631 -- is and why a program should (or shouldn't!) trust the coercion.
1632 -- It is reasonable to consider each constructor of 'UnivCoProvenance'
1633 -- as a totally independent coercion form; their only commonality is
1634 -- that they don't tell you what types they coercion between. (That info
1635 -- is in the 'UnivCo' constructor of 'Coercion'.
1636 data UnivCoProvenance
1637 = UnsafeCoerceProv -- ^ From @unsafeCoerce#@. These are unsound.
1638
1639 | PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom
1640 -- roled coercions
1641
1642 | ProofIrrelProv KindCoercion -- ^ From the fact that any two coercions are
1643 -- considered equivalent. See Note [ProofIrrelProv].
1644 -- Can be used in Nominal or Representational coercions
1645
1646 | PluginProv String -- ^ From a plugin, which asserts that this coercion
1647 -- is sound. The string is for the use of the plugin.
1648
1649 deriving Data.Data
1650
1651 instance Outputable UnivCoProvenance where
1652 ppr UnsafeCoerceProv = text "(unsafeCoerce#)"
1653 ppr (PhantomProv _) = text "(phantom)"
1654 ppr (ProofIrrelProv _) = text "(proof irrel.)"
1655 ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
1656
1657 -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
1658 data CoercionHole
1659 = CoercionHole { ch_co_var :: CoVar
1660 -- See Note [CoercionHoles and coercion free variables]
1661
1662 , ch_ref :: IORef (Maybe Coercion)
1663 }
1664
1665 coHoleCoVar :: CoercionHole -> CoVar
1666 coHoleCoVar = ch_co_var
1667
1668 setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
1669 setCoHoleCoVar h cv = h { ch_co_var = cv }
1670
1671 instance Data.Data CoercionHole where
1672 -- don't traverse?
1673 toConstr _ = abstractConstr "CoercionHole"
1674 gunfold _ _ = error "gunfold"
1675 dataTypeOf _ = mkNoRepType "CoercionHole"
1676
1677 instance Outputable CoercionHole where
1678 ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
1679
1680
1681 {- Note [Phantom coercions]
1682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1683 Consider
1684 data T a = T1 | T2
1685 Then we have
1686 T s ~R T t
1687 for any old s,t. The witness for this is (TyConAppCo T Rep co),
1688 where (co :: s ~P t) is a phantom coercion built with PhantomProv.
1689 The role of the UnivCo is always Phantom. The Coercion stored is the
1690 (nominal) kind coercion between the types
1691 kind(s) ~N kind (t)
1692
1693 Note [Coercion holes]
1694 ~~~~~~~~~~~~~~~~~~~~~~~~
1695 During typechecking, constraint solving for type classes works by
1696 - Generate an evidence Id, d7 :: Num a
1697 - Wrap it in a Wanted constraint, [W] d7 :: Num a
1698 - Use the evidence Id where the evidence is needed
1699 - Solve the constraint later
1700 - When solved, add an enclosing let-binding let d7 = .... in ....
1701 which actually binds d7 to the (Num a) evidence
1702
1703 For equality constraints we use a different strategy. See Note [The
1704 equality types story] in TysPrim for background on equality constraints.
1705 - For /boxed/ equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
1706 like type classes above. (Indeed, boxed equality constraints *are* classes.)
1707 - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
1708 we use a different plan
1709
1710 For unboxed equalities:
1711 - Generate a CoercionHole, a mutable variable just like a unification
1712 variable
1713 - Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest
1714 - Use the CoercionHole in a Coercion, via HoleCo
1715 - Solve the constraint later
1716 - When solved, fill in the CoercionHole by side effect, instead of
1717 doing the let-binding thing
1718
1719 The main reason for all this is that there may be no good place to let-bind
1720 the evidence for unboxed equalities:
1721
1722 - We emit constraints for kind coercions, to be used to cast a
1723 type's kind. These coercions then must be used in types. Because
1724 they might appear in a top-level type, there is no place to bind
1725 these (unlifted) coercions in the usual way.
1726
1727 - A coercion for (forall a. t1) ~ (forall a. t2) will look like
1728 forall a. (coercion for t1~t2)
1729 But the coercion for (t1~t2) may mention 'a', and we don't have
1730 let-bindings within coercions. We could add them, but coercion
1731 holes are easier.
1732
1733 - Moreover, nothing is lost from the lack of let-bindings. For
1734 dicionaries want to achieve sharing to avoid recomoputing the
1735 dictionary. But coercions are entirely erased, so there's little
1736 benefit to sharing. Indeed, even if we had a let-binding, we
1737 always inline types and coercions at every use site and drop the
1738 binding.
1739
1740 Other notes about HoleCo:
1741
1742 * INVARIANT: CoercionHole and HoleCo are used only during type checking,
1743 and should never appear in Core. Just like unification variables; a Type
1744 can contain a TcTyVar, but only during type checking. If, one day, we
1745 use type-level information to separate out forms that can appear during
1746 type-checking vs forms that can appear in core proper, holes in Core will
1747 be ruled out.
1748
1749 * See Note [CoercionHoles and coercion free variables]
1750
1751 * Coercion holes can be compared for equality like other coercions:
1752 by looking at the types coerced.
1753
1754
1755 Note [CoercionHoles and coercion free variables]
1756 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1757 Why does a CoercionHole contain a CoVar, as well as reference to
1758 fill in? Because we want to treat that CoVar as a free variable of
1759 the coercion. See #14584, and Note [What prevents a
1760 constraint from floating] in TcSimplify, item (4):
1761
1762 forall k. [W] co1 :: t1 ~# t2 |> co2
1763 [W] co2 :: k ~# *
1764
1765 Here co2 is a CoercionHole. But we /must/ know that it is free in
1766 co1, because that's all that stops it floating outside the
1767 implication.
1768
1769
1770 Note [ProofIrrelProv]
1771 ~~~~~~~~~~~~~~~~~~~~~
1772 A ProofIrrelProv is a coercion between coercions. For example:
1773
1774 data G a where
1775 MkG :: G Bool
1776
1777 In core, we get
1778
1779 G :: * -> *
1780 MkG :: forall (a :: *). (a ~ Bool) -> G a
1781
1782 Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want
1783 a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be
1784
1785 TyConAppCo Nominal MkG [co3, co4]
1786 where
1787 co3 :: co1 ~ co2
1788 co4 :: a1 ~ a2
1789
1790 Note that
1791 co1 :: a1 ~ Bool
1792 co2 :: a2 ~ Bool
1793
1794 Here,
1795 co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2)
1796 where
1797 co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
1798 co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
1799
1800
1801 %************************************************************************
1802 %* *
1803 Free variables of types and coercions
1804 %* *
1805 %************************************************************************
1806 -}
1807
1808 {- Note [Free variables of types]
1809 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1810 The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
1811 a VarSet that is closed over the types of its variables. More precisely,
1812 if S = tyCoVarsOfType( t )
1813 and (a:k) is in S
1814 then tyCoVarsOftype( k ) is a subset of S
1815
1816 Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.
1817
1818 We could /not/ close over the kinds of the variable occurrences, and
1819 instead do so at call sites, but it seems that we always want to do
1820 so, so it's easiest to do it here.
1821
1822 It turns out that getting the free variables of types is performance critical,
1823 so we profiled several versions, exploring different implementation strategies.
1824
1825 1. Baseline version: uses FV naively. Essentially:
1826
1827 tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty
1828
1829 This is not nice, because FV introduces some overhead to implement
1830 determinism, and throught its "interesting var" function, neither of which
1831 we need here, so they are a complete waste.
1832
1833 2. UnionVarSet version: instead of reusing the FV-based code, we simply used
1834 VarSets directly, trying to avoid the overhead of FV. E.g.:
1835
1836 -- FV version:
1837 tyCoFVsOfType (AppTy fun arg) a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c
1838
1839 -- UnionVarSet version:
1840 tyCoVarsOfType (AppTy fun arg) = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg)
1841
1842 This looks deceptively similar, but while FV internally builds a list- and
1843 set-generating function, the VarSet functions manipulate sets directly, and
1844 the latter peforms a lot worse than the naive FV version.
1845
1846 3. Accumulator-style VarSet version: this is what we use now. We do use VarSet
1847 as our data structure, but delegate the actual work to a new
1848 ty_co_vars_of_... family of functions, which use accumulator style and the
1849 "in-scope set" filter found in the internals of FV, but without the
1850 determinism overhead.
1851
1852 See #14880.
1853
1854 Note [Closing over free variable kinds]
1855 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1856 tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over
1857 free variable kinds. In previous GHC versions, this happened naively: whenever
1858 we would encounter an occurrence of a free type variable, we would close over
1859 its kind. This, however is wrong for two reasons (see #14880):
1860
1861 1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k), then
1862 we don't want to have to traverse k more than once.
1863
1864 2. Correctness. Imagine we have forall k. b -> k, where b has
1865 kind k, for some k bound in an outer scope. If we look at b's kind inside
1866 the forall, we'll collect that k is free and then remove k from the set of
1867 free variables. This is plain wrong. We must instead compute that b is free
1868 and then conclude that b's kind is free.
1869
1870 An obvious first approach is to move the closing-over-kinds from the
1871 occurrences of a type variable to after finding the free vars - however, this
1872 turns out to introduce performance regressions, and isn't even entirely
1873 correct.
1874
1875 In fact, it isn't even important *when* we close over kinds; what matters is
1876 that we handle each type var exactly once, and that we do it in the right
1877 context.
1878
1879 So the next approach we tried was to use the "in-scope set" part of FV or the
1880 equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to
1881 say "don't bother with variables we have already closed over". This should work
1882 fine in theory, but the code is complicated and doesn't perform well.
1883
1884 But there is a simpler way, which is implemented here. Consider the two points
1885 above:
1886
1887 1. Efficiency: we now have an accumulator, so the second time we encounter 'a',
1888 we'll ignore it, certainly not looking at its kind - this is why
1889 pre-checking set membership before inserting ends up not only being faster,
1890 but also being correct.
1891
1892 2. Correctness: we have an "in-scope set" (I think we should call it it a
1893 "bound-var set"), specifying variables that are bound by a forall in the type
1894 we are traversing; we simply ignore these variables, certainly not looking at
1895 their kind.
1896
1897 So now consider:
1898
1899 forall k. b -> k
1900
1901 where b :: k->Type is free; but of course, it's a different k! When looking at
1902 b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose
1903 this is our first encounter with b; we want the free vars of its kind. But we
1904 want to behave as if we took the free vars of its kind at the end; that is,
1905 with no bound vars in scope.
1906
1907 So the solution is easy. The old code was this:
1908
1909 ty_co_vars_of_type (TyVarTy v) is acc
1910 | v `elemVarSet` is = acc
1911 | v `elemVarSet` acc = acc
1912 | otherwise = ty_co_vars_of_type (tyVarKind v) is (extendVarSet acc v)
1913
1914 Now all we need to do is take the free vars of tyVarKind v *with an empty
1915 bound-var set*, thus:
1916
1917 ty_co_vars_of_type (TyVarTy v) is acc
1918 | v `elemVarSet` is = acc
1919 | v `elemVarSet` acc = acc
1920 | otherwise = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
1921 ^^^^^^^^^^^
1922
1923 And that's it.
1924
1925 -}
1926
1927 tyCoVarsOfType :: Type -> TyCoVarSet
1928 -- See Note [Free variables of types]
1929 tyCoVarsOfType ty = ty_co_vars_of_type ty emptyVarSet emptyVarSet
1930
1931 tyCoVarsOfTypes :: [Type] -> TyCoVarSet
1932 tyCoVarsOfTypes tys = ty_co_vars_of_types tys emptyVarSet emptyVarSet
1933
1934 ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
1935 ty_co_vars_of_type (TyVarTy v) is acc
1936 | v `elemVarSet` is = acc
1937 | v `elemVarSet` acc = acc
1938 | otherwise = ty_co_vars_of_type (tyVarKind v)
1939 emptyVarSet -- See Note [Closing over free variable kinds]
1940 (extendVarSet acc v)
1941
1942 ty_co_vars_of_type (TyConApp _ tys) is acc = ty_co_vars_of_types tys is acc
1943 ty_co_vars_of_type (LitTy {}) _ acc = acc
1944 ty_co_vars_of_type (AppTy fun arg) is acc = ty_co_vars_of_type fun is (ty_co_vars_of_type arg is acc)
1945 ty_co_vars_of_type (FunTy _ arg res) is acc = ty_co_vars_of_type arg is (ty_co_vars_of_type res is acc)
1946 ty_co_vars_of_type (ForAllTy (Bndr tv _) ty) is acc = ty_co_vars_of_type (varType tv) is $
1947 ty_co_vars_of_type ty (extendVarSet is tv) acc
1948 ty_co_vars_of_type (CastTy ty co) is acc = ty_co_vars_of_type ty is (ty_co_vars_of_co co is acc)
1949 ty_co_vars_of_type (CoercionTy co) is acc = ty_co_vars_of_co co is acc
1950
1951 ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
1952 ty_co_vars_of_types [] _ acc = acc
1953 ty_co_vars_of_types (ty:tys) is acc = ty_co_vars_of_type ty is (ty_co_vars_of_types tys is acc)
1954
1955 tyCoVarsOfCo :: Coercion -> TyCoVarSet
1956 -- See Note [Free variables of types]
1957 tyCoVarsOfCo co = ty_co_vars_of_co co emptyVarSet emptyVarSet
1958
1959 tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
1960 tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet
1961
1962
1963 ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
1964 ty_co_vars_of_co (Refl ty) is acc = ty_co_vars_of_type ty is acc
1965 ty_co_vars_of_co (GRefl _ ty mco) is acc = ty_co_vars_of_type ty is $
1966 ty_co_vars_of_mco mco is acc
1967 ty_co_vars_of_co (TyConAppCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
1968 ty_co_vars_of_co (AppCo co arg) is acc = ty_co_vars_of_co co is $
1969 ty_co_vars_of_co arg is acc
1970 ty_co_vars_of_co (ForAllCo tv kind_co co) is acc = ty_co_vars_of_co kind_co is $
1971 ty_co_vars_of_co co (extendVarSet is tv) acc
1972 ty_co_vars_of_co (FunCo _ co1 co2) is acc = ty_co_vars_of_co co1 is $
1973 ty_co_vars_of_co co2 is acc
1974 ty_co_vars_of_co (CoVarCo v) is acc = ty_co_vars_of_co_var v is acc
1975 ty_co_vars_of_co (HoleCo h) is acc = ty_co_vars_of_co_var (coHoleCoVar h) is acc
1976 -- See Note [CoercionHoles and coercion free variables]
1977 ty_co_vars_of_co (AxiomInstCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
1978 ty_co_vars_of_co (UnivCo p _ t1 t2) is acc = ty_co_vars_of_prov p is $
1979 ty_co_vars_of_type t1 is $
1980 ty_co_vars_of_type t2 is acc
1981 ty_co_vars_of_co (SymCo co) is acc = ty_co_vars_of_co co is acc
1982 ty_co_vars_of_co (TransCo co1 co2) is acc = ty_co_vars_of_co co1 is $
1983 ty_co_vars_of_co co2 is acc
1984 ty_co_vars_of_co (NthCo _ _ co) is acc = ty_co_vars_of_co co is acc
1985 ty_co_vars_of_co (LRCo _ co) is acc = ty_co_vars_of_co co is acc
1986 ty_co_vars_of_co (InstCo co arg) is acc = ty_co_vars_of_co co is $
1987 ty_co_vars_of_co arg is acc
1988 ty_co_vars_of_co (KindCo co) is acc = ty_co_vars_of_co co is acc
1989 ty_co_vars_of_co (SubCo co) is acc = ty_co_vars_of_co co is acc
1990 ty_co_vars_of_co (AxiomRuleCo _ cs) is acc = ty_co_vars_of_cos cs is acc
1991
1992 ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
1993 ty_co_vars_of_mco MRefl _is acc = acc
1994 ty_co_vars_of_mco (MCo co) is acc = ty_co_vars_of_co co is acc
1995
1996 ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
1997 ty_co_vars_of_co_var v is acc
1998 | v `elemVarSet` is = acc
1999 | v `elemVarSet` acc = acc
2000 | otherwise = ty_co_vars_of_type (varType v)
2001 emptyVarSet -- See Note [Closing over free variable kinds]
2002 (extendVarSet acc v)
2003
2004 ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
2005 ty_co_vars_of_cos [] _ acc = acc
2006 ty_co_vars_of_cos (co:cos) is acc = ty_co_vars_of_co co is (ty_co_vars_of_cos cos is acc)
2007
2008 tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
2009 tyCoVarsOfProv prov = ty_co_vars_of_prov prov emptyVarSet emptyVarSet
2010
2011 ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
2012 ty_co_vars_of_prov (PhantomProv co) is acc = ty_co_vars_of_co co is acc
2013 ty_co_vars_of_prov (ProofIrrelProv co) is acc = ty_co_vars_of_co co is acc
2014 ty_co_vars_of_prov UnsafeCoerceProv _ acc = acc
2015 ty_co_vars_of_prov (PluginProv _) _ acc = acc
2016
2017 -- | Generates an in-scope set from the free variables in a list of types
2018 -- and a list of coercions
2019 mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
2020 mkTyCoInScopeSet tys cos
2021 = mkInScopeSet (ty_co_vars_of_types tys emptyVarSet $
2022 ty_co_vars_of_cos cos emptyVarSet emptyVarSet)
2023
2024 -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
2025 -- set. For explanation of why using `VarSet` is not deterministic see
2026 -- Note [Deterministic FV] in FV.
2027 tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
2028 -- See Note [Free variables of types]
2029 tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty
2030
2031 -- | `tyCoFVsOfType` that returns free variables of a type in deterministic
2032 -- order. For explanation of why using `VarSet` is not deterministic see
2033 -- Note [Deterministic FV] in FV.
2034 tyCoVarsOfTypeList :: Type -> [TyCoVar]
2035 -- See Note [Free variables of types]
2036 tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
2037
2038 -- | Returns free variables of types, including kind variables as
2039 -- a non-deterministic set. For type synonyms it does /not/ expand the
2040 -- synonym.
2041 tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet
2042 -- See Note [Free variables of types]
2043 tyCoVarsOfTypesSet tys = tyCoVarsOfTypes $ nonDetEltsUFM tys
2044 -- It's OK to use nonDetEltsUFM here because we immediately forget the
2045 -- ordering by returning a set
2046
2047 -- | Returns free variables of types, including kind variables as
2048 -- a deterministic set. For type synonyms it does /not/ expand the
2049 -- synonym.
2050 tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
2051 -- See Note [Free variables of types]
2052 tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys
2053
2054 -- | Returns free variables of types, including kind variables as
2055 -- a deterministically ordered list. For type synonyms it does /not/ expand the
2056 -- synonym.
2057 tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
2058 -- See Note [Free variables of types]
2059 tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
2060
2061 -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
2062 -- The previous implementation used `unionVarSet` which is O(n+m) and can
2063 -- make the function quadratic.
2064 -- It's exported, so that it can be composed with
2065 -- other functions that compute free variables.
2066 -- See Note [FV naming conventions] in FV.
2067 --
2068 -- Eta-expanded because that makes it run faster (apparently)
2069 -- See Note [FV eta expansion] in FV for explanation.
2070 tyCoFVsOfType :: Type -> FV
2071 -- See Note [Free variables of types]
2072 tyCoFVsOfType (TyVarTy v) f bound_vars (acc_list, acc_set)
2073 | not (f v) = (acc_list, acc_set)
2074 | v `elemVarSet` bound_vars = (acc_list, acc_set)
2075 | v `elemVarSet` acc_set = (acc_list, acc_set)
2076 | otherwise = tyCoFVsOfType (tyVarKind v) f
2077 emptyVarSet -- See Note [Closing over free variable kinds]
2078 (v:acc_list, extendVarSet acc_set v)
2079 tyCoFVsOfType (TyConApp _ tys) f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc
2080 tyCoFVsOfType (LitTy {}) f bound_vars acc = emptyFV f bound_vars acc
2081 tyCoFVsOfType (AppTy fun arg) f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc
2082 tyCoFVsOfType (FunTy _ arg res) f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc
2083 tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty) f bound_vars acc
2084 tyCoFVsOfType (CastTy ty co) f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc
2085 tyCoFVsOfType (CoercionTy co) f bound_vars acc = tyCoFVsOfCo co f bound_vars acc
2086
2087 tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
2088 -- Free vars of (forall b. <thing with fvs>)
2089 tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs
2090
2091 tyCoFVsVarBndrs :: [Var] -> FV -> FV
2092 tyCoFVsVarBndrs vars fvs = foldr tyCoFVsVarBndr fvs vars
2093
2094 tyCoFVsVarBndr :: Var -> FV -> FV
2095 tyCoFVsVarBndr var fvs
2096 = tyCoFVsOfType (varType var) -- Free vars of its type/kind
2097 `unionFV` delFV var fvs -- Delete it from the thing-inside
2098
2099 tyCoFVsOfTypes :: [Type] -> FV
2100 -- See Note [Free variables of types]
2101 tyCoFVsOfTypes (ty:tys) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfTypes tys) fv_cand in_scope acc
2102 tyCoFVsOfTypes [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
2103
2104 -- | Get a deterministic set of the vars free in a coercion
2105 tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
2106 -- See Note [Free variables of types]
2107 tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co
2108
2109 tyCoVarsOfCoList :: Coercion -> [TyCoVar]
2110 -- See Note [Free variables of types]
2111 tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
2112
2113 tyCoFVsOfMCo :: MCoercion -> FV
2114 tyCoFVsOfMCo MRefl = emptyFV
2115 tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co
2116
2117 tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
2118 tyCoVarsOfCosSet cos = tyCoVarsOfCos $ nonDetEltsUFM cos
2119 -- It's OK to use nonDetEltsUFM here because we immediately forget the
2120 -- ordering by returning a set
2121
2122 tyCoFVsOfCo :: Coercion -> FV
2123 -- Extracts type and coercion variables from a coercion
2124 -- See Note [Free variables of types]
2125 tyCoFVsOfCo (Refl ty) fv_cand in_scope acc
2126 = tyCoFVsOfType ty fv_cand in_scope acc
2127 tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
2128 = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc
2129 tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
2130 tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
2131 = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
2132 tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
2133 = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
2134 tyCoFVsOfCo (FunCo _ co1 co2) fv_cand in_scope acc
2135 = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
2136 tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
2137 = tyCoFVsOfCoVar v fv_cand in_scope acc
2138 tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
2139 = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
2140 -- See Note [CoercionHoles and coercion free variables]
2141 tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
2142 tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
2143 = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1
2144 `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
2145 tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2146 tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
2147 tyCoFVsOfCo (NthCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2148 tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2149 tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
2150 tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2151 tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2152 tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
2153
2154 tyCoFVsOfCoVar :: CoVar -> FV
2155 tyCoFVsOfCoVar v fv_cand in_scope acc
2156 = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
2157
2158 tyCoFVsOfProv :: UnivCoProvenance -> FV
2159 tyCoFVsOfProv UnsafeCoerceProv fv_cand in_scope acc = emptyFV fv_cand in_scope acc
2160 tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2161 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
2162 tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
2163
2164 tyCoFVsOfCos :: [Coercion] -> FV
2165 tyCoFVsOfCos [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
2166 tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCos cos) fv_cand in_scope acc
2167
2168
2169 ------------- Extracting the CoVars of a type or coercion -----------
2170
2171 {-
2172
2173 Note [CoVarsOfX and the InterestingVarFun]
2174 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2175
2176 The coVarsOfType, coVarsOfTypes, coVarsOfCo, and coVarsOfCos functions are
2177 implemented in terms of the respective FV equivalents (tyCoFVsOf...), rather
2178 than the VarSet-based flavors (tyCoVarsOf...), despite the performance
2179 considerations outlined in Note [Free variables of types].
2180
2181 This is because FV includes the InterestingVarFun, which is useful here,
2182 because we can cleverly use it to restrict our calculations to CoVars - this
2183 is what getCoVarSet achieves.
2184
2185 See #14880.
2186
2187 -}
2188
2189 getCoVarSet :: FV -> CoVarSet
2190 getCoVarSet fv = snd (fv isCoVar emptyVarSet ([], emptyVarSet))
2191
2192 coVarsOfType :: Type -> CoVarSet
2193 coVarsOfType ty = getCoVarSet (tyCoFVsOfType ty)
2194
2195 coVarsOfTypes :: [Type] -> TyCoVarSet
2196 coVarsOfTypes tys = getCoVarSet (tyCoFVsOfTypes tys)
2197
2198 coVarsOfCo :: Coercion -> CoVarSet
2199 coVarsOfCo co = getCoVarSet (tyCoFVsOfCo co)
2200
2201 coVarsOfCos :: [Coercion] -> CoVarSet
2202 coVarsOfCos cos = getCoVarSet (tyCoFVsOfCos cos)
2203
2204 ----- Whether a covar is /Almost Devoid/ in a type or coercion ----
2205
2206 -- | Given a covar and a coercion, returns True if covar is almost devoid in
2207 -- the coercion. That is, covar can only appear in Refl and GRefl.
2208 -- See last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion
2209 almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
2210 almostDevoidCoVarOfCo cv co =
2211 almost_devoid_co_var_of_co co cv
2212
2213 almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
2214 almost_devoid_co_var_of_co (Refl {}) _ = True -- covar is allowed in Refl and
2215 almost_devoid_co_var_of_co (GRefl {}) _ = True -- GRefl, so we don't look into
2216 -- the coercions
2217 almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv
2218 = almost_devoid_co_var_of_cos cos cv
2219 almost_devoid_co_var_of_co (AppCo co arg) cv
2220 = almost_devoid_co_var_of_co co cv
2221 && almost_devoid_co_var_of_co arg cv
2222 almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv
2223 = almost_devoid_co_var_of_co kind_co cv
2224 && (v == cv || almost_devoid_co_var_of_co co cv)
2225 almost_devoid_co_var_of_co (FunCo _ co1 co2) cv
2226 = almost_devoid_co_var_of_co co1 cv
2227 && almost_devoid_co_var_of_co co2 cv
2228 almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv
2229 almost_devoid_co_var_of_co (HoleCo h) cv = (coHoleCoVar h) /= cv
2230 almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv
2231 = almost_devoid_co_var_of_cos cos cv
2232 almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv
2233 = almost_devoid_co_var_of_prov p cv
2234 && almost_devoid_co_var_of_type t1 cv
2235 && almost_devoid_co_var_of_type t2 cv
2236 almost_devoid_co_var_of_co (SymCo co) cv
2237 = almost_devoid_co_var_of_co co cv
2238 almost_devoid_co_var_of_co (TransCo co1 co2) cv
2239 = almost_devoid_co_var_of_co co1 cv
2240 && almost_devoid_co_var_of_co co2 cv
2241 almost_devoid_co_var_of_co (NthCo _ _ co) cv
2242 = almost_devoid_co_var_of_co co cv
2243 almost_devoid_co_var_of_co (LRCo _ co) cv
2244 = almost_devoid_co_var_of_co co cv
2245 almost_devoid_co_var_of_co (InstCo co arg) cv
2246 = almost_devoid_co_var_of_co co cv
2247 && almost_devoid_co_var_of_co arg cv
2248 almost_devoid_co_var_of_co (KindCo co) cv
2249 = almost_devoid_co_var_of_co co cv
2250 almost_devoid_co_var_of_co (SubCo co) cv
2251 = almost_devoid_co_var_of_co co cv
2252 almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
2253 = almost_devoid_co_var_of_cos cs cv
2254
2255 almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
2256 almost_devoid_co_var_of_cos [] _ = True
2257 almost_devoid_co_var_of_cos (co:cos) cv
2258 = almost_devoid_co_var_of_co co cv
2259 && almost_devoid_co_var_of_cos cos cv
2260
2261 almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
2262 almost_devoid_co_var_of_prov (PhantomProv co) cv
2263 = almost_devoid_co_var_of_co co cv
2264 almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
2265 = almost_devoid_co_var_of_co co cv
2266 almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True
2267 almost_devoid_co_var_of_prov (PluginProv _) _ = True
2268
2269 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
2270 almost_devoid_co_var_of_type (TyVarTy _) _ = True
2271 almost_devoid_co_var_of_type (TyConApp _ tys) cv
2272 = almost_devoid_co_var_of_types tys cv
2273 almost_devoid_co_var_of_type (LitTy {}) _ = True
2274 almost_devoid_co_var_of_type (AppTy fun arg) cv
2275 = almost_devoid_co_var_of_type fun cv
2276 && almost_devoid_co_var_of_type arg cv
2277 almost_devoid_co_var_of_type (FunTy _ arg res) cv
2278 = almost_devoid_co_var_of_type arg cv
2279 && almost_devoid_co_var_of_type res cv
2280 almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv
2281 = almost_devoid_co_var_of_type (varType v) cv
2282 && (v == cv || almost_devoid_co_var_of_type ty cv)
2283 almost_devoid_co_var_of_type (CastTy ty co) cv
2284 = almost_devoid_co_var_of_type ty cv
2285 && almost_devoid_co_var_of_co co cv
2286 almost_devoid_co_var_of_type (CoercionTy co) cv
2287 = almost_devoid_co_var_of_co co cv
2288
2289 almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
2290 almost_devoid_co_var_of_types [] _ = True
2291 almost_devoid_co_var_of_types (ty:tys) cv
2292 = almost_devoid_co_var_of_type ty cv
2293 && almost_devoid_co_var_of_types tys cv
2294
2295 ------------- Injective free vars -----------------
2296
2297 -- | Returns the free variables of a 'Type' that are in injective positions.
2298 -- For example, if @F@ is a non-injective type family, then:
2299 --
2300 -- @
2301 -- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
2302 -- @
2303 --
2304 -- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
2305 -- More formally, if
2306 -- @a@ is in @'injectiveVarsOfType' ty@
2307 -- and @S1(ty) ~ S2(ty)@,
2308 -- then @S1(a) ~ S2(a)@,
2309 -- where @S1@ and @S2@ are arbitrary substitutions.
2310 --
2311 -- See @Note [When does a tycon application need an explicit kind signature?]@.
2312 injectiveVarsOfType :: Type -> FV
2313 injectiveVarsOfType = go
2314 where
2315 go ty | Just ty' <- coreView ty
2316 = go ty'
2317 go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v)
2318 go (AppTy f a) = go f `unionFV` go a
2319 go (FunTy _ ty1 ty2) = go ty1 `unionFV` go ty2
2320 go (TyConApp tc tys) =
2321 case tyConInjectivityInfo tc of
2322 NotInjective -> emptyFV
2323 Injective inj -> mapUnionFV go $
2324 filterByList (inj ++ repeat True) tys
2325 -- Oversaturated arguments to a tycon are
2326 -- always injective, hence the repeat True
2327 go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty
2328 go LitTy{} = emptyFV
2329 go (CastTy ty _) = go ty
2330 go CoercionTy{} = emptyFV
2331
2332 -- | Does a 'TyCon' (that is applied to some number of arguments) need to be
2333 -- ascribed with an explicit kind signature to resolve ambiguity if rendered as
2334 -- a source-syntax type?
2335 -- (See @Note [When does a tycon application need an explicit kind signature?]@
2336 -- for a full explanation of what this function checks for.)
2337
2338 -- Morally, this function ought to belong in TyCon.hs, not TyCoRep.hs, but
2339 -- accomplishing this requires a fair deal of futzing aruond with .hs-boot
2340 -- files.
2341 tyConAppNeedsKindSig
2342 :: Bool -- ^ Should specified binders count towards injective positions in
2343 -- the kind of the TyCon? (If you're using visible kind
2344 -- applications, then you want True here.
2345 -> TyCon
2346 -> Int -- ^ The number of args the 'TyCon' is applied to.
2347 -> Bool -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the
2348 -- number of arguments)
2349 tyConAppNeedsKindSig spec_inj_pos tc n_args
2350 | LT <- listLengthCmp tc_binders n_args
2351 = False
2352 | otherwise
2353 = let (dropped_binders, remaining_binders)
2354 = splitAt n_args tc_binders
2355 result_kind = mkTyConKind remaining_binders tc_res_kind
2356 result_vars = tyCoVarsOfType result_kind
2357 dropped_vars = fvVarSet $
2358 mapUnionFV injective_vars_of_binder dropped_binders
2359
2360 in not (subVarSet result_vars dropped_vars)
2361 where
2362 tc_binders = tyConBinders tc
2363 tc_res_kind = tyConResKind tc
2364
2365 -- Returns the variables that would be fixed by knowing a TyConBinder. See
2366 -- Note [When does a tycon application need an explicit kind signature?]
2367 -- for a more detailed explanation of what this function does.
2368 injective_vars_of_binder :: TyConBinder -> FV
2369 injective_vars_of_binder (Bndr tv vis) =
2370 case vis of
2371 AnonTCB VisArg -> injectiveVarsOfType (varType tv)
2372 NamedTCB argf | source_of_injectivity argf
2373 -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
2374 _ -> emptyFV
2375
2376 source_of_injectivity Required = True
2377 source_of_injectivity Specified = spec_inj_pos
2378 source_of_injectivity Inferred = False
2379
2380 {-
2381 Note [When does a tycon application need an explicit kind signature?]
2382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2383 There are a couple of places in GHC where we convert Core Types into forms that
2384 more closely resemble user-written syntax. These include:
2385
2386 1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app)
2387 2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock)
2388
2389 This conversion presents a challenge: how do we ensure that the resulting type
2390 has enough kind information so as not to be ambiguous? To better motivate this
2391 question, consider the following Core type:
2392
2393 -- Foo :: Type -> Type
2394 type Foo = Proxy Type
2395
2396 There is nothing ambiguous about the RHS of Foo in Core. But if we were to,
2397 say, reify it into a TH Type, then it's tempting to just drop the invisible
2398 Type argument and simply return `Proxy`. But now we've lost crucial kind
2399 information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool`
2400 or `Proxy Int` or something else! We've inadvertently introduced ambiguity.
2401
2402 Unlike in other situations in GHC, we can't just turn on
2403 -fprint-explicit-kinds, as we need to produce something which has the same
2404 structure as a source-syntax type. Moreover, we can't rely on visible kind
2405 application, since the first kind argument to Proxy is inferred, not specified.
2406 Our solution is to annotate certain tycons with their kinds whenever they
2407 appear in applied form in order to resolve the ambiguity. For instance, we
2408 would reify the RHS of Foo like so:
2409
2410 type Foo = (Proxy :: Type -> Type)
2411
2412 We need to devise an algorithm that determines precisely which tycons need
2413 these explicit kind signatures. We certainly don't want to annotate _every_
2414 tycon with a kind signature, or else we might end up with horribly bloated
2415 types like the following:
2416
2417 (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type)
2418
2419 We only want to annotate tycons that absolutely require kind signatures in
2420 order to resolve some sort of ambiguity, and nothing more.
2421
2422 Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type
2423 require a kind signature? It might require it when we need to fill in any of
2424 T's omitted arguments. By "omitted argument", we mean one that is dropped when
2425 reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and
2426 specified arguments (e.g., TH reification in TcSplice), and sometimes the
2427 omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType,
2428 which reifies specified arguments through visible kind application).
2429 Regardless, the key idea is that _some_ arguments are going to be omitted after
2430 reification, and the only mechanism we have at our disposal for filling them in
2431 is through explicit kind signatures.
2432
2433 What do we mean by "fill in"? Let's consider this small example:
2434
2435 T :: forall {k}. Type -> (k -> Type) -> k
2436
2437 Moreover, we have this application of T:
2438
2439 T @{j} Int aty
2440
2441 When we reify this type, we omit the inferred argument @{j}. Is it fixed by the
2442 other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then
2443 we'll generate an equality constraint (kappa -> Type) and, assuming we can
2444 solve it, that will fix `kappa`. (Here, `kappa` is the unification variable
2445 that we instantiate `k` with.)
2446
2447 Therefore, for any application of a tycon T to some arguments, the Question We
2448 Must Answer is:
2449
2450 * Given the first n arguments of T, do the kinds of the non-omitted arguments
2451 fill in the omitted arguments?
2452
2453 (This is still a bit hand-wavey, but we'll refine this question incrementally
2454 as we explain more of the machinery underlying this process.)
2455
2456 Answering this question is precisely the role that the `injectiveVarsOfType`
2457 and `injective_vars_of_binder` functions exist to serve. If an omitted argument
2458 `a` appears in the set returned by `injectiveVarsOfType ty`, then knowing
2459 `ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a
2460 bit.)
2461
2462 More formally, if
2463 `a` is in `injectiveVarsOfType ty`
2464 and S1(ty) ~ S2(ty),
2465 then S1(a) ~ S2(a),
2466 where S1 and S2 are arbitrary substitutions.
2467
2468 For example, is `F` is a non-injective type family, then
2469
2470 injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c}
2471
2472 Now that we know what this function does, here is a second attempt at the
2473 Question We Must Answer:
2474
2475 * Given the first n arguments of T (ty_1 ... ty_n), consider the binders
2476 of T that are instantiated by non-omitted arguments. Do the injective
2477 variables of these binders fill in the remainder of T's kind?
2478
2479 Alright, we're getting closer. Next, we need to clarify what the injective
2480 variables of a tycon binder are. This the role that the
2481 `injective_vars_of_binder` function serves. Here is what this function does for
2482 each form of tycon binder:
2483
2484 * Anonymous binders are injective positions. For example, in the promoted data
2485 constructor '(:):
2486
2487 '(:) :: forall a. a -> [a] -> [a]
2488
2489 The second and third tyvar binders (of kinds `a` and `[a]`) are both
2490 anonymous, so if we had '(:) 'True '[], then the kinds of 'True and
2491 '[] would contribute to the kind of '(:) 'True '[]. Therefore,
2492 injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}.
2493 (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.)
2494 * Named binders:
2495 - Inferred binders are never injective positions. For example, in this data
2496 type:
2497
2498 data Proxy a
2499 Proxy :: forall {k}. k -> Type
2500
2501 If we had Proxy 'True, then the kind of 'True would not contribute to the
2502 kind of Proxy 'True. Therefore,
2503 injective_vars_of_binder(forall {k}. ...) = {}.
2504 - Required binders are injective positions. For example, in this data type:
2505
2506 data Wurble k (a :: k) :: k
2507 Wurble :: forall k -> k -> k
2508
2509 The first tyvar binder (of kind `forall k`) has required visibility, so if
2510 we had Wurble (Maybe a) Nothing, then the kind of Maybe a would
2511 contribute to the kind of Wurble (Maybe a) Nothing. Hence,
2512 injective_vars_of_binder(forall a -> ...) = {a}.
2513 - Specified binders /might/ be injective positions, depending on how you
2514 approach things. Continuing the '(:) example:
2515
2516 '(:) :: forall a. a -> [a] -> [a]
2517
2518 Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind
2519 of '(:) 'True '[], since it's not explicitly instantiated by the user. But
2520 if visible kind application is enabled, then this is possible, since the
2521 user can write '(:) @Bool 'True '[]. (In that case,
2522 injective_vars_of_binder(forall a. ...) = {a}.)
2523
2524 There are some situations where using visible kind application is appropriate
2525 (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH
2526 reification), so the `injective_vars_of_binder` function is parametrized by
2527 a Bool which decides if specified binders should be counted towards
2528 injective positions or not.
2529
2530 Now that we've defined injective_vars_of_binder, we can refine the Question We
2531 Must Answer once more:
2532
2533 * Given the first n arguments of T (ty_1 ... ty_n), consider the binders
2534 of T that are instantiated by non-omitted arguments. For each such binder
2535 b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
2536 superset of the free variables of the remainder of T's kind?
2537
2538 If the answer to this question is "no", then (T ty_1 ... ty_n) needs an
2539 explicit kind signature, since T's kind has kind variables leftover that
2540 aren't fixed by the non-omitted arguments.
2541
2542 One last sticking point: what does "the remainder of T's kind" mean? You might
2543 be tempted to think that it corresponds to all of the arguments in the kind of
2544 T that would normally be instantiated by omitted arguments. But this isn't
2545 quite right, strictly speaking. Consider the following (silly) example:
2546
2547 S :: forall {k}. Type -> Type
2548
2549 And suppose we have this application of S:
2550
2551 S Int Bool
2552
2553 The Int argument would be omitted, and
2554 injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which
2555 might suggest that (S Bool) needs an explicit kind signature. But
2556 (S Bool :: Type) doesn't actually fix `k`! This is because the kind signature
2557 only affects the /result/ of the application, not all of the individual
2558 arguments. So adding a kind signature here won't make a difference. Therefore,
2559 the fourth (and final) iteration of the Question We Must Answer is:
2560
2561 * Given the first n arguments of T (ty_1 ... ty_n), consider the binders
2562 of T that are instantiated by non-omitted arguments. For each such binder
2563 b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
2564 superset of the free variables of the kind of (T ty_1 ... ty_n)?
2565
2566 Phew, that was a lot of work!
2567
2568 How can be sure that this is correct? That is, how can we be sure that in the
2569 event that we leave off a kind annotation, that one could infer the kind of the
2570 tycon application from its arguments? It's essentially a proof by induction: if
2571 we can infer the kinds of every subtree of a type, then the whole tycon
2572 application will have an inferrable kind--unless, of course, the remainder of
2573 the tycon application's kind has uninstantiated kind variables.
2574
2575 What happens if T is oversaturated? That is, if T's kind has fewer than n
2576 arguments, in the case that the concrete application instantiates a result
2577 kind variable with an arrow kind? If we run out of arguments, we do not attach
2578 a kind annotation. This should be a rare case, indeed. Here is an example:
2579
2580 data T1 :: k1 -> k2 -> *
2581 data T2 :: k1 -> k2 -> *
2582
2583 type family G (a :: k) :: k
2584 type instance G T1 = T2
2585
2586 type instance F Char = (G T1 Bool :: (* -> *) -> *) -- F from above
2587
2588 Here G's kind is (forall k. k -> k), and the desugared RHS of that last
2589 instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to
2590 the algorithm above, there are 3 arguments to G so we should peel off 3
2591 arguments in G's kind. But G's kind has only two arguments. This is the
2592 rare special case, and we choose not to annotate the application of G with
2593 a kind signature. After all, we needn't do this, since that instance would
2594 be reified as:
2595
2596 type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
2597
2598 So the kind of G isn't ambiguous anymore due to the explicit kind annotation
2599 on its argument. See #8953 and test th/T8953.
2600 -}
2601
2602 ------------- No free vars -----------------
2603
2604 -- | Returns True if this type has no free variables. Should be the same as
2605 -- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case.
2606 noFreeVarsOfType :: Type -> Bool
2607 noFreeVarsOfType (TyVarTy _) = False
2608 noFreeVarsOfType (AppTy t1 t2) = noFreeVarsOfType t1 && noFreeVarsOfType t2
2609 noFreeVarsOfType (TyConApp _ tys) = all noFreeVarsOfType tys
2610 noFreeVarsOfType ty@(ForAllTy {}) = isEmptyVarSet (tyCoVarsOfType ty)
2611 noFreeVarsOfType (FunTy _ t1 t2) = noFreeVarsOfType t1 && noFreeVarsOfType t2
2612 noFreeVarsOfType (LitTy _) = True
2613 noFreeVarsOfType (CastTy ty co) = noFreeVarsOfType ty && noFreeVarsOfCo co
2614 noFreeVarsOfType (CoercionTy co) = noFreeVarsOfCo co
2615
2616 noFreeVarsOfMCo :: MCoercion -> Bool
2617 noFreeVarsOfMCo MRefl = True
2618 noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co
2619
2620 noFreeVarsOfTypes :: [Type] -> Bool
2621 noFreeVarsOfTypes = all noFreeVarsOfType
2622
2623 -- | Returns True if this coercion has no free variables. Should be the same as
2624 -- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.
2625 noFreeVarsOfCo :: Coercion -> Bool
2626 noFreeVarsOfCo (Refl ty) = noFreeVarsOfType ty
2627 noFreeVarsOfCo (GRefl _ ty co) = noFreeVarsOfType ty && noFreeVarsOfMCo co
2628 noFreeVarsOfCo (TyConAppCo _ _ args) = all noFreeVarsOfCo args
2629 noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
2630 noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co)
2631 noFreeVarsOfCo (FunCo _ c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
2632 noFreeVarsOfCo (CoVarCo _) = False
2633 noFreeVarsOfCo (HoleCo {}) = True -- I'm unsure; probably never happens
2634 noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args
2635 noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p &&
2636 noFreeVarsOfType t1 &&
2637 noFreeVarsOfType t2
2638 noFreeVarsOfCo (SymCo co) = noFreeVarsOfCo co
2639 noFreeVarsOfCo (TransCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
2640 noFreeVarsOfCo (NthCo _ _ co) = noFreeVarsOfCo co
2641 noFreeVarsOfCo (LRCo _ co) = noFreeVarsOfCo co
2642 noFreeVarsOfCo (InstCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
2643 noFreeVarsOfCo (KindCo co) = noFreeVarsOfCo co
2644 noFreeVarsOfCo (SubCo co) = noFreeVarsOfCo co
2645 noFreeVarsOfCo (AxiomRuleCo _ cs) = all noFreeVarsOfCo cs
2646
2647 -- | Returns True if this UnivCoProv has no free variables. Should be the same as
2648 -- isEmptyVarSet . tyCoVarsOfProv, but faster in the non-forall case.
2649 noFreeVarsOfProv :: UnivCoProvenance -> Bool
2650 noFreeVarsOfProv UnsafeCoerceProv = True
2651 noFreeVarsOfProv (PhantomProv co) = noFreeVarsOfCo co
2652 noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co
2653 noFreeVarsOfProv (PluginProv {}) = True
2654
2655 {-
2656 %************************************************************************
2657 %* *
2658 Substitutions
2659 Data type defined here to avoid unnecessary mutual recursion
2660 %* *
2661 %************************************************************************
2662 -}
2663
2664 -- | Type & coercion substitution
2665 --
2666 -- #tcvsubst_invariant#
2667 -- The following invariants must hold of a 'TCvSubst':
2668 --
2669 -- 1. The in-scope set is needed /only/ to
2670 -- guide the generation of fresh uniques
2671 --
2672 -- 2. In particular, the /kind/ of the type variables in
2673 -- the in-scope set is not relevant
2674 --
2675 -- 3. The substitution is only applied ONCE! This is because
2676 -- in general such application will not reach a fixed point.
2677 data TCvSubst
2678 = TCvSubst InScopeSet -- The in-scope type and kind variables
2679 TvSubstEnv -- Substitutes both type and kind variables
2680 CvSubstEnv -- Substitutes coercion variables
2681 -- See Note [Substitutions apply only once]
2682 -- and Note [Extending the TvSubstEnv]
2683 -- and Note [Substituting types and coercions]
2684 -- and Note [The substitution invariant]
2685
2686 -- | A substitution of 'Type's for 'TyVar's
2687 -- and 'Kind's for 'KindVar's
2688 type TvSubstEnv = TyVarEnv Type
2689 -- NB: A TvSubstEnv is used
2690 -- both inside a TCvSubst (with the apply-once invariant
2691 -- discussed in Note [Substitutions apply only once],
2692 -- and also independently in the middle of matching,
2693 -- and unification (see Types.Unify).
2694 -- So you have to look at the context to know if it's idempotent or
2695 -- apply-once or whatever
2696
2697 -- | A substitution of 'Coercion's for 'CoVar's
2698 type CvSubstEnv = CoVarEnv Coercion
2699
2700 {- Note [The substitution invariant]
2701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2702 When calling (substTy subst ty) it should be the case that
2703 the in-scope set in the substitution is a superset of both:
2704
2705 (SIa) The free vars of the range of the substitution
2706 (SIb) The free vars of ty minus the domain of the substitution
2707
2708 The same rules apply to other substitutions (notably CoreSubst.Subst)
2709
2710 * Reason for (SIa). Consider
2711 substTy [a :-> Maybe b] (forall b. b->a)
2712 we must rename the forall b, to get
2713 forall b2. b2 -> Maybe b
2714 Making 'b' part of the in-scope set forces this renaming to
2715 take place.
2716
2717 * Reason for (SIb). Consider
2718 substTy [a :-> Maybe b] (forall b. (a,b,x))
2719 Then if we use the in-scope set {b}, satisfying (SIa), there is
2720 a danger we will rename the forall'd variable to 'x' by mistake,
2721 getting this:
2722 forall x. (Maybe b, x, x)
2723 Breaking (SIb) caused the bug from #11371.
2724
2725 Note: if the free vars of the range of the substitution are freshly created,
2726 then the problems of (SIa) can't happen, and so it would be sound to
2727 ignore (SIa).
2728
2729 Note [Substitutions apply only once]
2730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2731 We use TCvSubsts to instantiate things, and we might instantiate
2732 forall a b. ty
2733 with the types
2734 [a, b], or [b, a].
2735 So the substitution might go [a->b, b->a]. A similar situation arises in Core
2736 when we find a beta redex like
2737 (/\ a /\ b -> e) b a
2738 Then we also end up with a substitution that permutes type variables. Other
2739 variations happen to; for example [a -> (a, b)].
2740
2741 ********************************************************
2742 *** So a substitution must be applied precisely once ***
2743 ********************************************************
2744
2745 A TCvSubst is not idempotent, but, unlike the non-idempotent substitution
2746 we use during unifications, it must not be repeatedly applied.
2747
2748 Note [Extending the TvSubstEnv]
2749 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2750 See #tcvsubst_invariant# for the invariants that must hold.
2751
2752 This invariant allows a short-cut when the subst envs are empty:
2753 if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst)
2754 holds --- then (substTy subst ty) does nothing.
2755
2756 For example, consider:
2757 (/\a. /\b:(a~Int). ...b..) Int
2758 We substitute Int for 'a'. The Unique of 'b' does not change, but
2759 nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
2760
2761 This invariant has several crucial consequences:
2762
2763 * In substVarBndr, we need extend the TvSubstEnv
2764 - if the unique has changed
2765 - or if the kind has changed
2766
2767 * In substTyVar, we do not need to consult the in-scope set;
2768 the TvSubstEnv is enough
2769
2770 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
2771
2772 Note [Substituting types and coercions]
2773 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2774 Types and coercions are mutually recursive, and either may have variables
2775 "belonging" to the other. Thus, every time we wish to substitute in a
2776 type, we may also need to substitute in a coercion, and vice versa.
2777 However, the constructor used to create type variables is distinct from
2778 that of coercion variables, so we carry two VarEnvs in a TCvSubst. Note
2779 that it would be possible to use the CoercionTy constructor to combine
2780 these environments, but that seems like a false economy.
2781
2782 Note that the TvSubstEnv should *never* map a CoVar (built with the Id
2783 constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
2784 the range of the TvSubstEnv should *never* include a type headed with
2785 CoercionTy.
2786 -}
2787
2788 emptyTvSubstEnv :: TvSubstEnv
2789 emptyTvSubstEnv = emptyVarEnv
2790
2791 emptyCvSubstEnv :: CvSubstEnv
2792 emptyCvSubstEnv = emptyVarEnv
2793
2794 composeTCvSubstEnv :: InScopeSet
2795 -> (TvSubstEnv, CvSubstEnv)
2796 -> (TvSubstEnv, CvSubstEnv)
2797 -> (TvSubstEnv, CvSubstEnv)
2798 -- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
2799 -- It assumes that both are idempotent.
2800 -- Typically, @env1@ is the refinement to a base substitution @env2@
2801 composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2)
2802 = ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2
2803 , cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 )
2804 -- First apply env1 to the range of env2
2805 -- Then combine the two, making sure that env1 loses if
2806 -- both bind the same variable; that's why env1 is the
2807 -- *left* argument to plusVarEnv, because the right arg wins
2808 where
2809 subst1 = TCvSubst in_scope tenv1 cenv1
2810
2811 -- | Composes two substitutions, applying the second one provided first,
2812 -- like in function composition.
2813 composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
2814 composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2)
2815 = TCvSubst is3 tenv3 cenv3
2816 where
2817 is3 = is1 `unionInScope` is2
2818 (tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2)
2819
2820 emptyTCvSubst :: TCvSubst
2821 emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv
2822
2823 mkEmptyTCvSubst :: InScopeSet -> TCvSubst
2824 mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv
2825
2826 isEmptyTCvSubst :: TCvSubst -> Bool
2827 -- See Note [Extending the TvSubstEnv]
2828 isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
2829
2830 mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
2831 mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv
2832
2833 mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
2834 -- ^ Make a TCvSubst with specified tyvar subst and empty covar subst
2835 mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv
2836
2837 mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst
2838 -- ^ Make a TCvSubst with specified covar subst and empty tyvar subst
2839 mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv
2840
2841 getTvSubstEnv :: TCvSubst -> TvSubstEnv
2842 getTvSubstEnv (TCvSubst _ env _) = env
2843
2844 getCvSubstEnv :: TCvSubst -> CvSubstEnv
2845 getCvSubstEnv (TCvSubst _ _ env) = env
2846
2847 getTCvInScope :: TCvSubst -> InScopeSet
2848 getTCvInScope (TCvSubst in_scope _ _) = in_scope
2849
2850 -- | Returns the free variables of the types in the range of a substitution as
2851 -- a non-deterministic set.
2852 getTCvSubstRangeFVs :: TCvSubst -> VarSet
2853 getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
2854 = unionVarSet tenvFVs cenvFVs
2855 where
2856 tenvFVs = tyCoVarsOfTypesSet tenv
2857 cenvFVs = tyCoVarsOfCosSet cenv
2858
2859 isInScope :: Var -> TCvSubst -> Bool
2860 isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
2861
2862 notElemTCvSubst :: Var -> TCvSubst -> Bool
2863 notElemTCvSubst v (TCvSubst _ tenv cenv)
2864 | isTyVar v
2865 = not (v `elemVarEnv` tenv)
2866 | otherwise
2867 = not (v `elemVarEnv` cenv)
2868
2869 setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
2870 setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv
2871
2872 setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
2873 setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv
2874
2875 zapTCvSubst :: TCvSubst -> TCvSubst
2876 zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv
2877
2878 extendTCvInScope :: TCvSubst -> Var -> TCvSubst
2879 extendTCvInScope (TCvSubst in_scope tenv cenv) var
2880 = TCvSubst (extendInScopeSet in_scope var) tenv cenv
2881
2882 extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
2883 extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars
2884 = TCvSubst (extendInScopeSetList in_scope vars) tenv cenv
2885
2886 extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
2887 extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
2888 = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
2889
2890 extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
2891 extendTCvSubst subst v ty
2892 | isTyVar v
2893 = extendTvSubst subst v ty
2894 | CoercionTy co <- ty
2895 = extendCvSubst subst v co
2896 | otherwise
2897 = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
2898
2899 extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst
2900 extendTCvSubstWithClone subst tcv
2901 | isTyVar tcv = extendTvSubstWithClone subst tcv
2902 | otherwise = extendCvSubstWithClone subst tcv
2903
2904 extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
2905 extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
2906 = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
2907
2908 extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
2909 extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty
2910 = ASSERT( isTyVar v )
2911 extendTvSubstAndInScope subst v ty
2912 extendTvSubstBinderAndInScope subst (Anon {}) _
2913 = subst
2914
2915 extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
2916 -- Adds a new tv -> tv mapping, /and/ extends the in-scope set
2917 extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv'
2918 = TCvSubst (extendInScopeSetSet in_scope new_in_scope)
2919 (extendVarEnv tenv tv (mkTyVarTy tv'))
2920 cenv
2921 where
2922 new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv'
2923
2924 extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
2925 extendCvSubst (TCvSubst in_scope tenv cenv) v co
2926 = TCvSubst in_scope tenv (extendVarEnv cenv v co)
2927
2928 extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
2929 extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv'
2930 = TCvSubst (extendInScopeSetSet in_scope new_in_scope)
2931 tenv
2932 (extendVarEnv cenv cv (mkCoVarCo cv'))
2933 where
2934 new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv'
2935
2936 extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
2937 -- Also extends the in-scope set
2938 extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
2939 = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
2940 (extendVarEnv tenv tv ty)
2941 cenv
2942
2943 extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
2944 extendTvSubstList subst tvs tys
2945 = foldl2 extendTvSubst subst tvs tys
2946
2947 extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
2948 extendTCvSubstList subst tvs tys
2949 = foldl2 extendTCvSubst subst tvs tys
2950
2951 unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
2952 -- Works when the ranges are disjoint
2953 unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
2954 = ASSERT( not (tenv1 `intersectsVarEnv` tenv2)
2955 && not (cenv1 `intersectsVarEnv` cenv2) )
2956 TCvSubst (in_scope1 `unionInScope` in_scope2)
2957 (tenv1 `plusVarEnv` tenv2)
2958 (cenv1 `plusVarEnv` cenv2)
2959
2960 -- mkTvSubstPrs and zipTvSubst generate the in-scope set from
2961 -- the types given; but it's just a thunk so with a bit of luck
2962 -- it'll never be evaluated
2963
2964 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
2965 -- environment. No CoVars, please!
2966 zipTvSubst :: [TyVar] -> [Type] -> TCvSubst
2967 zipTvSubst tvs tys
2968 | debugIsOn
2969 , not (all isTyVar tvs) || neLength tvs tys
2970 = pprTrace "zipTvSubst" (ppr tvs $$ ppr tys) emptyTCvSubst
2971 | otherwise
2972 = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv
2973 where
2974 tenv = zipTyEnv tvs tys
2975
2976 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
2977 -- environment. No TyVars, please!
2978 zipCvSubst :: [CoVar] -> [Coercion] -> TCvSubst
2979 zipCvSubst cvs cos
2980 | debugIsOn
2981 , not (all isCoVar cvs) || neLength cvs cos
2982 = pprTrace "zipCvSubst" (ppr cvs $$ ppr cos) emptyTCvSubst
2983 | otherwise
2984 = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv
2985 where
2986 cenv = zipCoEnv cvs cos
2987
2988 zipTCvSubst :: [TyCoVar] -> [Type] -> TCvSubst
2989 zipTCvSubst tcvs tys
2990 | debugIsOn
2991 , neLength tcvs tys
2992 = pprTrace "zipTCvSubst" (ppr tcvs $$ ppr tys) emptyTCvSubst
2993 | otherwise
2994 = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys))
2995 where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst
2996 zip_tcvsubst (tv:tvs) (ty:tys) subst
2997 = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty)
2998 zip_tcvsubst _ _ subst = subst -- empty case
2999
3000 -- | Generates the in-scope set for the 'TCvSubst' from the types in the
3001 -- incoming environment. No CoVars, please!
3002 mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst
3003 mkTvSubstPrs prs =
3004 ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs )
3005 mkTvSubst in_scope tenv
3006 where tenv = mkVarEnv prs
3007 in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs
3008 onlyTyVarsAndNoCoercionTy =
3009 and [ isTyVar tv && not (isCoercionTy ty)
3010 | (tv, ty) <- prs ]
3011
3012 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
3013 zipTyEnv tyvars tys
3014 = ASSERT( all (not . isCoercionTy) tys )
3015 mkVarEnv (zipEqual "zipTyEnv" tyvars tys)
3016 -- There used to be a special case for when
3017 -- ty == TyVarTy tv
3018 -- (a not-uncommon case) in which case the substitution was dropped.
3019 -- But the type-tidier changes the print-name of a type variable without
3020 -- changing the unique, and that led to a bug. Why? Pre-tidying, we had
3021 -- a type {Foo t}, where Foo is a one-method class. So Foo is really a newtype.
3022 -- And it happened that t was the type variable of the class. Post-tiding,
3023 -- it got turned into {Foo t2}. The ext-core printer expanded this using
3024 -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
3025 -- and so generated a rep type mentioning t not t2.
3026 --
3027 -- Simplest fix is to nuke the "optimisation"
3028
3029 zipCoEnv :: [CoVar] -> [Coercion] -> CvSubstEnv
3030 zipCoEnv cvs cos = mkVarEnv (zipEqual "zipCoEnv" cvs cos)
3031
3032 instance Outputable TCvSubst where
3033 ppr (TCvSubst ins tenv cenv)
3034 = brackets $ sep[ text "TCvSubst",
3035 nest 2 (text "In scope:" <+> ppr ins),
3036 nest 2 (text "Type env:" <+> ppr tenv),
3037 nest 2 (text "Co env:" <+> ppr cenv) ]
3038
3039 {-
3040 %************************************************************************
3041 %* *
3042 Performing type or kind substitutions
3043 %* *
3044 %************************************************************************
3045
3046 Note [Sym and ForAllCo]
3047 ~~~~~~~~~~~~~~~~~~~~~~~
3048 In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
3049 how do we push sym into a ForAllCo? It's a little ugly.
3050
3051 Here is the typing rule:
3052
3053 h : k1 ~# k2
3054 (tv : k1) |- g : ty1 ~# ty2
3055 ----------------------------
3056 ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~#
3057 (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h]))
3058
3059 Here is what we want:
3060
3061 ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~#
3062 (ForAllTy (tv : k1) ty1)
3063
3064
3065 Because the kinds of the type variables to the right of the colon are the kinds
3066 coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h).
3067
3068 Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want
3069
3070 ForAllCo tv h' g' :
3071 (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~#
3072 (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h']))
3073
3074 We thus see that we want
3075
3076 g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h']
3077
3078 and thus g' = sym (g[tv |-> tv |> h']).
3079
3080 Putting it all together, we get this:
3081
3082 sym (ForAllCo tv h g)
3083 ==>
3084 ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
3085
3086 Note [Substituting in a coercion hole]
3087 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3088 It seems highly suspicious to be substituting in a coercion that still
3089 has coercion holes. Yet, this can happen in a situation like this:
3090
3091 f :: forall k. k :~: Type -> ()
3092 f Refl = let x :: forall (a :: k). [a] -> ...
3093 x = ...
3094
3095 When we check x's type signature, we require that k ~ Type. We indeed
3096 know this due to the Refl pattern match, but the eager unifier can't
3097 make use of givens. So, when we're done looking at x's type, a coercion
3098 hole will remain. Then, when we're checking x's definition, we skolemise
3099 x's type (in order to, e.g., bring the scoped type variable `a` into scope).
3100 This requires performing a substitution for the fresh skolem variables.
3101
3102 This subsitution needs to affect the kind of the coercion hole, too --
3103 otherwise, the kind will have an out-of-scope variable in it. More problematically
3104 in practice (we won't actually notice the out-of-scope variable ever), skolems
3105 in the kind might have too high a level, triggering a failure to uphold the
3106 invariant that no free variables in a type have a higher level than the
3107 ambient level in the type checker. In the event of having free variables in the
3108 hole's kind, I'm pretty sure we'll always have an erroneous program, so we
3109 don't need to worry what will happen when the hole gets filled in. After all,
3110 a hole relating a locally-bound type variable will be unable to be solved. This
3111 is why it's OK not to look through the IORef of a coercion hole during
3112 substitution.
3113
3114 -}
3115
3116 -- | Type substitution, see 'zipTvSubst'
3117 substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
3118 -- Works only if the domain of the substitution is a
3119 -- superset of the type being substituted into
3120 substTyWith tvs tys = {-#SCC "substTyWith" #-}
3121 ASSERT( tvs `equalLength` tys )
3122 substTy (zipTvSubst tvs tys)
3123
3124 -- | Type substitution, see 'zipTvSubst'. Disables sanity checks.
3125 -- The problems that the sanity checks in substTy catch are described in
3126 -- Note [The substitution invariant].
3127 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
3128 -- substTy and remove this function. Please don't use in new code.
3129 substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
3130 substTyWithUnchecked tvs tys
3131 = ASSERT( tvs `equalLength` tys )
3132 substTyUnchecked (zipTvSubst tvs tys)
3133
3134 -- | Substitute tyvars within a type using a known 'InScopeSet'.
3135 -- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
3136 -- invariant]; specifically it should include the free vars of 'tys',
3137 -- and of 'ty' minus the domain of the subst.
3138 substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
3139 substTyWithInScope in_scope tvs tys ty =
3140 ASSERT( tvs `equalLength` tys )
3141 substTy (mkTvSubst in_scope tenv) ty
3142 where tenv = zipTyEnv tvs tys
3143
3144 -- | Coercion substitution, see 'zipTvSubst'
3145 substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
3146 substCoWith tvs tys = ASSERT( tvs `equalLength` tys )
3147 substCo (zipTvSubst tvs tys)
3148
3149 -- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
3150 -- The problems that the sanity checks in substCo catch are described in
3151 -- Note [The substitution invariant].
3152 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
3153 -- substCo and remove this function. Please don't use in new code.
3154 substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
3155 substCoWithUnchecked tvs tys
3156 = ASSERT( tvs `equalLength` tys )
3157 substCoUnchecked (zipTvSubst tvs tys)
3158
3159
3160
3161 -- | Substitute covars within a type
3162 substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
3163 substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
3164
3165 -- | Type substitution, see 'zipTvSubst'
3166 substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
3167 substTysWith tvs tys = ASSERT( tvs `equalLength` tys )
3168 substTys (zipTvSubst tvs tys)
3169
3170 -- | Type substitution, see 'zipTvSubst'
3171 substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
3172 substTysWithCoVars cvs cos = ASSERT( cvs `equalLength` cos )
3173 substTys (zipCvSubst cvs cos)
3174
3175 -- | Substitute within a 'Type' after adding the free variables of the type
3176 -- to the in-scope set. This is useful for the case when the free variables
3177 -- aren't already in the in-scope set or easily available.
3178 -- See also Note [The substitution invariant].
3179 substTyAddInScope :: TCvSubst -> Type -> Type
3180 substTyAddInScope subst ty =
3181 substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
3182
3183 -- | When calling `substTy` it should be the case that the in-scope set in
3184 -- the substitution is a superset of the free vars of the range of the
3185 -- substitution.
3186 -- See also Note [The substitution invariant].
3187 isValidTCvSubst :: TCvSubst -> Bool
3188 isValidTCvSubst (TCvSubst in_scope tenv cenv) =
3189 (tenvFVs `varSetInScope` in_scope) &&
3190 (cenvFVs `varSetInScope` in_scope)
3191 where
3192 tenvFVs = tyCoVarsOfTypesSet tenv
3193 cenvFVs = tyCoVarsOfCosSet cenv
3194
3195 -- | This checks if the substitution satisfies the invariant from
3196 -- Note [The substitution invariant].
3197 checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
3198 checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
3199 = ASSERT2( isValidTCvSubst subst,
3200 text "in_scope" <+> ppr in_scope $$
3201 text "tenv" <+> ppr tenv $$
3202 text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$
3203 text "cenv" <+> ppr cenv $$
3204 text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$
3205 text "tys" <+> ppr tys $$
3206 text "cos" <+> ppr cos )
3207 ASSERT2( tysCosFVsInScope,
3208 text "in_scope" <+> ppr in_scope $$
3209 text "tenv" <+> ppr tenv $$
3210 text "cenv" <+> ppr cenv $$
3211 text "tys" <+> ppr tys $$
3212 text "cos" <+> ppr cos $$
3213 text "needInScope" <+> ppr needInScope )
3214 a
3215 where
3216 substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv
3217 -- It's OK to use nonDetKeysUFM here, because we only use this list to
3218 -- remove some elements from a set
3219 needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
3220 `delListFromUniqSet_Directly` substDomain
3221 tysCosFVsInScope = needInScope `varSetInScope` in_scope
3222
3223
3224 -- | Substitute within a 'Type'
3225 -- The substitution has to satisfy the invariants described in
3226 -- Note [The substitution invariant].
3227 substTy :: HasCallStack => TCvSubst -> Type -> Type
3228 substTy subst ty
3229 | isEmptyTCvSubst subst = ty
3230 | otherwise = checkValidSubst subst [ty] [] $
3231 subst_ty subst ty
3232
3233 -- | Substitute within a 'Type' disabling the sanity checks.
3234 -- The problems that the sanity checks in substTy catch are described in
3235 -- Note [The substitution invariant].
3236 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
3237 -- substTy and remove this function. Please don't use in new code.
3238 substTyUnchecked :: TCvSubst -> Type -> Type
3239 substTyUnchecked subst ty
3240 | isEmptyTCvSubst subst = ty
3241 | otherwise = subst_ty subst ty
3242
3243 -- | Substitute within several 'Type's
3244 -- The substitution has to satisfy the invariants described in
3245 -- Note [The substitution invariant].
3246 substTys :: HasCallStack => TCvSubst -> [Type] -> [Type]
3247 substTys subst tys
3248 | isEmptyTCvSubst subst = tys
3249 | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
3250
3251 -- | Substitute within several 'Type's disabling the sanity checks.
3252 -- The problems that the sanity checks in substTys catch are described in
3253 -- Note [The substitution invariant].
3254 -- The goal of #11371 is to migrate all the calls of substTysUnchecked to
3255 -- substTys and remove this function. Please don't use in new code.
3256 substTysUnchecked :: TCvSubst -> [Type] -> [Type]
3257 substTysUnchecked subst tys
3258 | isEmptyTCvSubst subst = tys
3259 | otherwise = map (subst_ty subst) tys
3260
3261 -- | Substitute within a 'ThetaType'
3262 -- The substitution has to satisfy the invariants described in
3263 -- Note [The substitution invariant].
3264 substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType
3265 substTheta = substTys
3266
3267 -- | Substitute within a 'ThetaType' disabling the sanity checks.
3268 -- The problems that the sanity checks in substTys catch are described in
3269 -- Note [The substitution invariant].
3270 -- The goal of #11371 is to migrate all the calls of substThetaUnchecked to
3271 -- substTheta and remove this function. Please don't use in new code.
3272 substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
3273 substThetaUnchecked = substTysUnchecked
3274
3275
3276 subst_ty :: TCvSubst -> Type -> Type
3277 -- subst_ty is the main workhorse for type substitution
3278 --
3279 -- Note that the in_scope set is poked only if we hit a forall
3280 -- so it may often never be fully computed
3281 subst_ty subst ty
3282 = go ty
3283 where
3284 go (TyVarTy tv) = substTyVar subst tv
3285 go (AppTy fun arg) = mkAppTy (go fun) $! (go arg)
3286 -- The mkAppTy smart constructor is important
3287 -- we might be replacing (a Int), represented with App
3288 -- by [Int], represented with TyConApp
3289 go (TyConApp tc tys) = let args = map go tys
3290 in args `seqList` TyConApp tc args
3291 go ty@(FunTy { ft_arg = arg, ft_res = res })
3292 = let !arg' = go arg
3293 !res' = go res
3294 in ty { ft_arg = arg', ft_res = res' }
3295 go (ForAllTy (Bndr tv vis) ty)
3296 = case substVarBndrUnchecked subst tv of
3297 (subst', tv') ->
3298 (ForAllTy $! ((Bndr $! tv') vis)) $!
3299 (subst_ty subst' ty)
3300 go (LitTy n) = LitTy $! n
3301 go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co)
3302 go (CoercionTy co) = CoercionTy $! (subst_co subst co)
3303
3304 substTyVar :: TCvSubst -> TyVar -> Type
3305 substTyVar (TCvSubst _ tenv _) tv
3306 = ASSERT( isTyVar tv )
3307 case lookupVarEnv tenv tv of
3308 Just ty -> ty
3309 Nothing -> TyVarTy tv
3310
3311 substTyVars :: TCvSubst -> [TyVar] -> [Type]
3312 substTyVars subst = map $ substTyVar subst
3313
3314 substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type]
3315 substTyCoVars subst = map $ substTyCoVar subst
3316
3317 substTyCoVar :: TCvSubst -> TyCoVar -> Type
3318 substTyCoVar subst tv
3319 | isTyVar tv = substTyVar subst tv
3320 | otherwise = CoercionTy $ substCoVar subst tv
3321
3322 lookupTyVar :: TCvSubst -> TyVar -> Maybe Type
3323 -- See Note [Extending the TCvSubst]
3324 lookupTyVar (TCvSubst _ tenv _) tv
3325 = ASSERT( isTyVar tv )
3326 lookupVarEnv tenv tv
3327
3328 -- | Substitute within a 'Coercion'
3329 -- The substitution has to satisfy the invariants described in
3330 -- Note [The substitution invariant].
3331 substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion
3332 substCo subst co
3333 | isEmptyTCvSubst subst = co
3334 | otherwise = checkValidSubst subst [] [co] $ subst_co subst co
3335
3336 -- | Substitute within a 'Coercion' disabling sanity checks.
3337 -- The problems that the sanity checks in substCo catch are described in
3338 -- Note [The substitution invariant].
3339 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
3340 -- substCo and remove this function. Please don't use in new code.
3341 substCoUnchecked :: TCvSubst -> Coercion -> Coercion
3342 substCoUnchecked subst co
3343 | isEmptyTCvSubst subst = co
3344 | otherwise = subst_co subst co
3345
3346 -- | Substitute within several 'Coercion's
3347 -- The substitution has to satisfy the invariants described in
3348 -- Note [The substitution invariant].
3349 substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]
3350 substCos subst cos
3351 | isEmptyTCvSubst subst = cos
3352 | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
3353
3354 subst_co :: TCvSubst -> Coercion -> Coercion
3355 subst_co subst co
3356 = go co
3357 where
3358 go_ty :: Type -> Type
3359 go_ty = subst_ty subst
3360
3361 go_mco :: MCoercion -> MCoercion
3362 go_mco MRefl = MRefl
3363 go_mco (MCo co) = MCo (go co)
3364
3365 go :: Coercion -> Coercion
3366 go (Refl ty) = mkNomReflCo $! (go_ty ty)
3367 go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
3368 go (TyConAppCo r tc args)= let args' = map go args
3369 in args' `seqList` mkTyConAppCo r tc args'
3370 go (AppCo co arg) = (mkAppCo $! go co) $! go arg
3371 go (ForAllCo tv kind_co co)
3372 = case substForAllCoBndrUnchecked subst tv kind_co of
3373 (subst', tv', kind_co') ->
3374 ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co
3375 go (FunCo r co1 co2) = (mkFunCo r $! go co1) $! go co2
3376 go (CoVarCo cv) = substCoVar subst cv
3377 go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
3378 go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $!
3379 (go_ty t1)) $! (go_ty t2)
3380 go (SymCo co) = mkSymCo $! (go co)
3381 go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
3382 go (NthCo r d co) = mkNthCo r d $! (go co)
3383 go (LRCo lr co) = mkLRCo lr $! (go co)
3384 go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
3385 go (KindCo co) = mkKindCo $! (go co)
3386 go (SubCo co) = mkSubCo $! (go co)
3387 go (AxiomRuleCo c cs) = let cs1 = map go cs
3388 in cs1 `seqList` AxiomRuleCo c cs1
3389 go (HoleCo h) = HoleCo $! go_hole h
3390
3391 go_prov UnsafeCoerceProv = UnsafeCoerceProv
3392 go_prov (PhantomProv kco) = PhantomProv (go kco)
3393 go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
3394 go_prov p@(PluginProv _) = p
3395
3396 -- See Note [Substituting in a coercion hole]
3397 go_hole h@(CoercionHole { ch_co_var = cv })
3398 = h { ch_co_var = updateVarType go_ty cv }
3399
3400 substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
3401 -> (TCvSubst, TyCoVar, Coercion)
3402 substForAllCoBndr subst
3403 = substForAllCoBndrUsing False (substCo subst) subst
3404
3405 -- | Like 'substForAllCoBndr', but disables sanity checks.
3406 -- The problems that the sanity checks in substCo catch are described in
3407 -- Note [The substitution invariant].
3408 -- The goal of #11371 is to migrate all the calls of substCoUnchecked to
3409 -- substCo and remove this function. Please don't use in new code.
3410 substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion
3411 -> (TCvSubst, TyCoVar, Coercion)
3412 substForAllCoBndrUnchecked subst
3413 = substForAllCoBndrUsing False (substCoUnchecked subst) subst
3414
3415 -- See Note [Sym and ForAllCo]
3416 substForAllCoBndrUsing :: Bool -- apply sym to binder?
3417 -> (Coercion -> Coercion) -- transformation to kind co
3418 -> TCvSubst -> TyCoVar -> KindCoercion
3419 -> (TCvSubst, TyCoVar, KindCoercion)
3420 substForAllCoBndrUsing sym sco subst old_var
3421 | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var
3422 | otherwise = substForAllCoCoVarBndrUsing sym sco subst old_var
3423
3424 substForAllCoTyVarBndrUsing :: Bool -- apply sym to binder?
3425 -> (Coercion -> Coercion) -- transformation to kind co
3426 -> TCvSubst -> TyVar -> KindCoercion
3427 -> (TCvSubst, TyVar, KindCoercion)
3428 substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co
3429 = ASSERT( isTyVar old_var )
3430 ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv
3431 , new_var, new_kind_co )
3432 where
3433 new_env | no_change && not sym = delVarEnv tenv old_var
3434 | sym = extendVarEnv tenv old_var $
3435 TyVarTy new_var `CastTy` new_kind_co
3436 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
3437
3438 no_kind_change = noFreeVarsOfCo old_kind_co
3439 no_change = no_kind_change && (new_var == old_var)
3440
3441 new_kind_co | no_kind_change = old_kind_co
3442 | otherwise = sco old_kind_co
3443
3444 Pair new_ki1 _ = coercionKind new_kind_co
3445 -- We could do substitution to (tyVarKind old_var). We don't do so because
3446 -- we already substituted new_kind_co, which contains the kind information
3447 -- we want. We don't want to do substitution once more. Also, in most cases,
3448 -- new_kind_co is a Refl, in which case coercionKind is really fast.
3449
3450 new_var = uniqAway in_scope (setTyVarKind old_var new_ki1)
3451
3452 substForAllCoCoVarBndrUsing :: Bool -- apply sym to binder?
3453 -> (Coercion -> Coercion) -- transformation to kind co
3454 -> TCvSubst -> CoVar -> KindCoercion
3455 -> (TCvSubst, CoVar, KindCoercion)
3456 substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv)
3457 old_var old_kind_co
3458 = ASSERT( isCoVar old_var )
3459 ( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv
3460 , new_var, new_kind_co )
3461 where
3462 new_cenv | no_change && not sym = delVarEnv cenv old_var
3463 | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var)
3464
3465 no_kind_change = noFreeVarsOfCo old_kind_co
3466 no_change = no_kind_change && (new_var == old_var)
3467
3468 new_kind_co | no_kind_change = old_kind_co
3469 | otherwise = sco old_kind_co
3470
3471 Pair h1 h2 = coercionKind new_kind_co
3472
3473 new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type
3474 new_var_type | sym = h2
3475 | otherwise = h1
3476
3477 substCoVar :: TCvSubst -> CoVar -> Coercion
3478 substCoVar (TCvSubst _ _ cenv) cv
3479 = case lookupVarEnv cenv cv of
3480 Just co -> co
3481 Nothing -> CoVarCo cv
3482
3483 substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
3484 substCoVars subst cvs = map (substCoVar subst) cvs
3485
3486 lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
3487 lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
3488
3489 substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
3490 substTyVarBndr = substTyVarBndrUsing substTy
3491
3492 substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar])
3493 substTyVarBndrs = mapAccumL substTyVarBndr
3494
3495 substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
3496 substVarBndr = substVarBndrUsing substTy
3497
3498 substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar])
3499 substVarBndrs = mapAccumL substVarBndr
3500
3501 substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
3502 substCoVarBndr = substCoVarBndrUsing substTy
3503
3504 -- | Like 'substVarBndr', but disables sanity checks.
3505 -- The problems that the sanity checks in substTy catch are described in
3506 -- Note [The substitution invariant].
3507 -- The goal of #11371 is to migrate all the calls of substTyUnchecked to
3508 -- substTy and remove this function. Please don't use in new code.
3509 substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
3510 substVarBndrUnchecked = substVarBndrUsing substTyUnchecked
3511
3512 substVarBndrUsing :: (TCvSubst -> Type -> Type)
3513 -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
3514 substVarBndrUsing subst_fn subst v
3515 | isTyVar v = substTyVarBndrUsing subst_fn subst v
3516 | otherwise = substCoVarBndrUsing subst_fn subst v
3517
3518 -- | Substitute a tyvar in a binding position, returning an
3519 -- extended subst and a new tyvar.
3520 -- Use the supplied function to substitute in the kind
3521 substTyVarBndrUsing
3522 :: (TCvSubst -> Type -> Type) -- ^ Use this to substitute in the kind
3523 -> TCvSubst -> TyVar -> (TCvSubst, TyVar)
3524 substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
3525 = ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst )
3526 ASSERT( isTyVar old_var )
3527 (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var)
3528 where
3529 new_env | no_change = delVarEnv tenv old_var
3530 | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
3531
3532 _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv)
3533 -- Assertion check that we are not capturing something in the substitution
3534
3535 old_ki = tyVarKind old_var
3536 no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed
3537 no_change = no_kind_change && (new_var == old_var)
3538 -- no_change means that the new_var is identical in
3539 -- all respects to the old_var (same unique, same kind)
3540 -- See Note [Extending the TCvSubst]
3541 --
3542 -- In that case we don't need to extend the substitution
3543 -- to map old to new. But instead we must zap any
3544 -- current substitution for the variable. For example:
3545 -- (\x.e) with id_subst = [x |-> e']
3546 -- Here we must simply zap the substitution for x
3547
3548 new_var | no_kind_change = uniqAway in_scope old_var
3549 | otherwise = uniqAway in_scope $
3550 setTyVarKind old_var (subst_fn subst old_ki)
3551 -- The uniqAway part makes sure the new variable is not already in scope
3552
3553 -- | Substitute a covar in a binding position, returning an
3554 -- extended subst and a new covar.
3555 -- Use the supplied function to substitute in the kind
3556 substCoVarBndrUsing
3557 :: (TCvSubst -> Type -> Type)
3558 -> TCvSubst -> CoVar -> (TCvSubst, CoVar)
3559 substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
3560 = ASSERT( isCoVar old_var )
3561 (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
3562 where
3563 new_co = mkCoVarCo new_var
3564 no_kind_change = noFreeVarsOfTypes [t1, t2]
3565 no_change = new_var == old_var && no_kind_change
3566
3567 new_cenv | no_change = delVarEnv cenv old_var
3568 | otherwise = extendVarEnv cenv old_var new_co
3569
3570 new_var = uniqAway in_scope subst_old_var
3571 subst_old_var = mkCoVar (varName old_var) new_var_type
3572
3573 (_, _, t1, t2, role) = coVarKindsTypesRole old_var
3574 t1' = subst_fn subst t1
3575 t2' = subst_fn subst t2
3576 new_var_type = mkCoercionType role t1' t2'
3577 -- It's important to do the substitution for coercions,
3578 -- because they can have free type variables
3579
3580 cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
3581 cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq
3582 = ASSERT2( isTyVar tv, ppr tv ) -- I think it's only called on TyVars
3583 (TCvSubst (extendInScopeSet in_scope tv')
3584 (extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv')
3585 where
3586 old_ki = tyVarKind tv
3587 no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed
3588
3589 tv1 | no_kind_change = tv
3590 | otherwise = setTyVarKind tv (substTy subst old_ki)
3591
3592 tv' = setVarUnique tv1 uniq
3593
3594 cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
3595 cloneTyVarBndrs subst [] _usupply = (subst, [])
3596 cloneTyVarBndrs subst (t:ts) usupply = (subst'', tv:tvs)
3597 where
3598 (uniq, usupply') = takeUniqFromSupply usupply
3599 (subst' , tv ) = cloneTyVarBndr subst t uniq
3600 (subst'', tvs) = cloneTyVarBndrs subst' ts usupply'
3601
3602 {-
3603 %************************************************************************
3604 %* *
3605 Pretty-printing types
3606
3607 Defined very early because of debug printing in assertions
3608 %* *
3609 %************************************************************************
3610
3611 @pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
3612 defined to use this. @pprParendType@ is the same, except it puts
3613 parens around the type, except for the atomic cases. @pprParendType@
3614 works just by setting the initial context precedence very high.
3615
3616 Note that any function which pretty-prints a @Type@ first converts the @Type@
3617 to an @IfaceType@. See Note [IfaceType and pretty-printing] in IfaceType.
3618
3619 See Note [Precedence in types] in BasicTypes.
3620 -}
3621
3622 --------------------------------------------------------
3623 -- When pretty-printing types, we convert to IfaceType,
3624 -- and pretty-print that.
3625 -- See Note [Pretty printing via IfaceSyn] in PprTyThing
3626 --------------------------------------------------------
3627
3628 pprType, pprParendType :: Type -> SDoc
3629 pprType = pprPrecType topPrec
3630 pprParendType = pprPrecType appPrec
3631
3632 pprPrecType :: PprPrec -> Type -> SDoc
3633 pprPrecType = pprPrecTypeX emptyTidyEnv
3634
3635 pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc
3636 pprPrecTypeX env prec ty
3637 = getPprStyle $ \sty ->
3638 if debugStyle sty -- Use debugPprType when in
3639 then debug_ppr_ty prec ty -- when in debug-style
3640 else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty)
3641 -- NB: debug-style is used for -dppr-debug
3642 -- dump-style is used for -ddump-tc-trace etc
3643
3644 pprTyLit :: TyLit -> SDoc
3645 pprTyLit = pprIfaceTyLit . toIfaceTyLit
3646
3647 pprKind, pprParendKind :: Kind -> SDoc
3648 pprKind = pprType
3649 pprParendKind = pprParendType
3650
3651 tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
3652 tidyToIfaceTypeStyX env ty sty
3653 | userStyle sty = tidyToIfaceTypeX env ty
3654 | otherwise = toIfaceTypeX (tyCoVarsOfType ty) ty
3655 -- in latter case, don't tidy, as we'll be printing uniques.
3656
3657 tidyToIfaceType :: Type -> IfaceType
3658 tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv
3659
3660 tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
3661 -- It's vital to tidy before converting to an IfaceType
3662 -- or nested binders will become indistinguishable!
3663 --
3664 -- Also for the free type variables, tell toIfaceTypeX to
3665 -- leave them as IfaceFreeTyVar. This is super-important
3666 -- for debug printing.
3667 tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty)
3668 where
3669 env' = tidyFreeTyCoVars env free_tcvs
3670 free_tcvs = tyCoVarsOfTypeWellScoped ty
3671
3672 ------------
3673 pprCo, pprParendCo :: Coercion -> SDoc
3674 pprCo co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty)
3675 pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty)
3676
3677 tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
3678 tidyToIfaceCoSty co sty
3679 | userStyle sty = tidyToIfaceCo co
3680 | otherwise = toIfaceCoercionX (tyCoVarsOfCo co) co
3681 -- in latter case, don't tidy, as we'll be printing uniques.
3682
3683 tidyToIfaceCo :: Coercion -> IfaceCoercion
3684 -- It's vital to tidy before converting to an IfaceType
3685 -- or nested binders will become indistinguishable!
3686 --
3687 -- Also for the free type variables, tell toIfaceCoercionX to
3688 -- leave them as IfaceFreeCoVar. This is super-important
3689 -- for debug printing.
3690 tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co)
3691 where
3692 env = tidyFreeTyCoVars emptyTidyEnv free_tcvs
3693 free_tcvs = scopedSort $ tyCoVarsOfCoList co
3694 ------------
3695 pprClassPred :: Class -> [Type] -> SDoc
3696 pprClassPred clas tys = pprTypeApp (classTyCon clas) tys
3697
3698 ------------
3699 pprTheta :: ThetaType -> SDoc
3700 pprTheta = pprIfaceContext topPrec . map tidyToIfaceType
3701
3702 pprParendTheta :: ThetaType -> SDoc
3703 pprParendTheta = pprIfaceContext appPrec . map tidyToIfaceType
3704
3705 pprThetaArrowTy :: ThetaType -> SDoc
3706 pprThetaArrowTy = pprIfaceContextArr . map tidyToIfaceType
3707
3708 ------------------
3709 instance Outputable Type where
3710 ppr ty = pprType ty
3711
3712 instance Outputable TyLit where
3713 ppr = pprTyLit
3714
3715 ------------------
3716 pprSigmaType :: Type -> SDoc
3717 pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType
3718
3719 pprForAll :: [TyCoVarBinder] -> SDoc
3720 pprForAll tvs = pprIfaceForAll (map toIfaceForAllBndr tvs)
3721
3722 -- | Print a user-level forall; see Note [When to print foralls]
3723 pprUserForAll :: [TyCoVarBinder] -> SDoc
3724 pprUserForAll = pprUserIfaceForAll . map toIfaceForAllBndr
3725
3726 pprTCvBndrs :: [TyCoVarBinder] -> SDoc
3727 pprTCvBndrs tvs = sep (map pprTCvBndr tvs)
3728
3729 pprTCvBndr :: TyCoVarBinder -> SDoc
3730 pprTCvBndr = pprTyVar . binderVar
3731
3732 pprTyVars :: [TyVar] -> SDoc
3733 pprTyVars tvs = sep (map pprTyVar tvs)
3734
3735 pprTyVar :: TyVar -> SDoc
3736 -- Print a type variable binder with its kind (but not if *)
3737 -- Here we do not go via IfaceType, because the duplication with
3738 -- pprIfaceTvBndr is minimal, and the loss of uniques etc in
3739 -- debug printing is disastrous
3740 pprTyVar tv
3741 | isLiftedTypeKind kind = ppr tv
3742 | otherwise = parens (ppr tv <+> dcolon <+> ppr kind)
3743 where
3744 kind = tyVarKind tv
3745
3746 instance Outputable TyCoBinder where
3747 ppr (Anon af ty) = ppr af <+> ppr ty
3748 ppr (Named (Bndr v Required)) = ppr v
3749 ppr (Named (Bndr v Specified)) = char '@' <> ppr v
3750 ppr (Named (Bndr v Inferred)) = braces (ppr v)
3751
3752 -----------------
3753 instance Outputable Coercion where -- defined here to avoid orphans
3754 ppr = pprCo
3755
3756 debugPprType :: Type -> SDoc
3757 -- ^ debugPprType is a simple pretty printer that prints a type
3758 -- without going through IfaceType. It does not format as prettily
3759 -- as the normal route, but it's much more direct, and that can
3760 -- be useful for debugging. E.g. with -dppr-debug it prints the
3761 -- kind on type-variable /occurrences/ which the normal route
3762 -- fundamentally cannot do.
3763 debugPprType ty = debug_ppr_ty topPrec ty
3764
3765 debug_ppr_ty :: PprPrec -> Type -> SDoc
3766 debug_ppr_ty _ (LitTy l)
3767 = ppr l
3768
3769 debug_ppr_ty _ (TyVarTy tv)
3770 = ppr tv -- With -dppr-debug we get (tv :: kind)
3771
3772 debug_ppr_ty prec (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
3773 = maybeParen prec funPrec $
3774 sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res]
3775 where
3776 arrow = case af of
3777 VisArg -> text "->"
3778 InvisArg -> text "=>"
3779
3780 debug_ppr_ty prec (TyConApp tc tys)
3781 | null tys = ppr tc
3782 | otherwise = maybeParen prec appPrec $
3783 hang (ppr tc) 2 (sep (map (debug_ppr_ty appPrec) tys))
3784
3785 debug_ppr_ty _ (AppTy t1 t2)
3786 = hang (debug_ppr_ty appPrec t1) -- Print parens so we see ((a b) c)
3787 2 (debug_ppr_ty appPrec t2) -- so that we can distinguish
3788 -- TyConApp from AppTy
3789
3790 debug_ppr_ty prec (CastTy ty co)
3791 = maybeParen prec topPrec $
3792 hang (debug_ppr_ty topPrec ty)
3793 2 (text "|>" <+> ppr co)
3794
3795 debug_ppr_ty _ (CoercionTy co)
3796 = parens (text "CO" <+> ppr co)
3797
3798 debug_ppr_ty prec ty@(ForAllTy {})
3799 | (tvs, body) <- split ty
3800 = maybeParen prec funPrec $
3801 hang (text "forall" <+> fsep (map ppr tvs) <> dot)
3802 -- The (map ppr tvs) will print kind-annotated
3803 -- tvs, because we are (usually) in debug-style
3804 2 (ppr body)
3805 where
3806 split ty | ForAllTy tv ty' <- ty
3807 , (tvs, body) <- split ty'
3808 = (tv:tvs, body)
3809 | otherwise
3810 = ([], ty)
3811
3812 {-
3813 Note [When to print foralls]
3814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3815 Mostly we want to print top-level foralls when (and only when) the user specifies
3816 -fprint-explicit-foralls. But when kind polymorphism is at work, that suppresses
3817 too much information; see #9018.
3818
3819 So I'm trying out this rule: print explicit foralls if
3820 a) User specifies -fprint-explicit-foralls, or
3821 b) Any of the quantified type variables has a kind
3822 that mentions a kind variable
3823
3824 This catches common situations, such as a type siguature
3825 f :: m a
3826 which means
3827 f :: forall k. forall (m :: k->*) (a :: k). m a
3828 We really want to see both the "forall k" and the kind signatures
3829 on m and a. The latter comes from pprTCvBndr.
3830
3831 Note [Infix type variables]
3832 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
3833 With TypeOperators you can say
3834
3835 f :: (a ~> b) -> b
3836
3837 and the (~>) is considered a type variable. However, the type
3838 pretty-printer in this module will just see (a ~> b) as
3839
3840 App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
3841
3842 So it'll print the type in prefix form. To avoid confusion we must
3843 remember to parenthesise the operator, thus
3844
3845 (~>) a b -> b
3846
3847 See #2766.
3848 -}
3849
3850 pprDataCons :: TyCon -> SDoc
3851 pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons
3852 where
3853 sepWithVBars [] = empty
3854 sepWithVBars docs = sep (punctuate (space <> vbar) docs)
3855
3856 pprDataConWithArgs :: DataCon -> SDoc
3857 pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc]
3858 where
3859 (_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc
3860 user_bndrs = dataConUserTyVarBinders dc
3861 forAllDoc = pprUserForAll user_bndrs
3862 thetaDoc = pprThetaArrowTy theta
3863 argsDoc = hsep (fmap pprParendType arg_tys)
3864
3865
3866 pprTypeApp :: TyCon -> [Type] -> SDoc
3867 pprTypeApp tc tys
3868 = pprIfaceTypeApp topPrec (toIfaceTyCon tc)
3869 (toIfaceTcArgs tc tys)
3870 -- TODO: toIfaceTcArgs seems rather wasteful here
3871
3872 ------------------
3873 -- | Display all kind information (with @-fprint-explicit-kinds@) when the
3874 -- provided 'Bool' argument is 'True'.
3875 -- See @Note [Kind arguments in error messages]@ in "TcErrors".
3876 pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
3877 pprWithExplicitKindsWhen b
3878 = updSDocDynFlags $ \dflags ->
3879 if b then gopt_set dflags Opt_PrintExplicitKinds
3880 else dflags
3881
3882 {-
3883 %************************************************************************
3884 %* *
3885 \subsection{TidyType}
3886 %* *
3887 %************************************************************************
3888 -}
3889
3890 -- | This tidies up a type for printing in an error message, or in
3891 -- an interface file.
3892 --
3893 -- It doesn't change the uniques at all, just the print names.
3894 tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
3895 tidyVarBndrs tidy_env tvs
3896 = mapAccumL tidyVarBndr (avoidNameClashes tvs tidy_env) tvs
3897
3898 tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
3899 tidyVarBndr tidy_env@(occ_env, subst) var
3900 = case tidyOccName occ_env (getHelpfulOccName var) of
3901 (occ_env', occ') -> ((occ_env', subst'), var')
3902 where
3903 subst' = extendVarEnv subst var var'
3904 var' = setVarType (setVarName var name') type'
3905 type' = tidyType tidy_env (varType var)
3906 name' = tidyNameOcc name occ'
3907 name = varName var
3908
3909 avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
3910 -- Seed the occ_env with clashes among the names, see
3911 -- Note [Tidying multiple names at once] in OccName
3912 avoidNameClashes tvs (occ_env, subst)
3913 = (avoidClashesOccEnv occ_env occs, subst)
3914 where
3915 occs = map getHelpfulOccName tvs
3916
3917 getHelpfulOccName :: TyCoVar -> OccName
3918 -- A TcTyVar with a System Name is probably a
3919 -- unification variable; when we tidy them we give them a trailing
3920 -- "0" (or 1 etc) so that they don't take precedence for the
3921 -- un-modified name. Plus, indicating a unification variable in
3922 -- this way is a helpful clue for users
3923 getHelpfulOccName tv
3924 | isSystemName name, isTcTyVar tv
3925 = mkTyVarOcc (occNameString occ ++ "0")
3926 | otherwise
3927 = occ
3928 where
3929 name = varName tv
3930 occ = getOccName name
3931
3932 tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis
3933 -> (TidyEnv, VarBndr TyCoVar vis)
3934 tidyTyCoVarBinder tidy_env (Bndr tv vis)
3935 = (tidy_env', Bndr tv' vis)
3936 where
3937 (tidy_env', tv') = tidyVarBndr tidy_env tv
3938
3939 tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
3940 -> (TidyEnv, [VarBndr TyCoVar vis])
3941 tidyTyCoVarBinders tidy_env tvbs
3942 = mapAccumL tidyTyCoVarBinder
3943 (avoidNameClashes (binderVars tvbs) tidy_env) tvbs
3944
3945 ---------------
3946 tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
3947 -- ^ Add the free 'TyVar's to the env in tidy form,
3948 -- so that we can tidy the type they are free in
3949 tidyFreeTyCoVars (full_occ_env, var_env) tyvars
3950 = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars)
3951
3952 ---------------
3953 tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
3954 tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars
3955
3956 ---------------
3957 tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
3958 -- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
3959 -- using the environment if one has not already been allocated. See
3960 -- also 'tidyVarBndr'
3961 tidyOpenTyCoVar env@(_, subst) tyvar
3962 = case lookupVarEnv subst tyvar of
3963 Just tyvar' -> (env, tyvar') -- Already substituted
3964 Nothing ->
3965 let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar))
3966 in tidyVarBndr env' tyvar -- Treat it as a binder
3967
3968 ---------------
3969 tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
3970 tidyTyCoVarOcc env@(_, subst) tv
3971 = case lookupVarEnv subst tv of
3972 Nothing -> updateVarType (tidyType env) tv
3973 Just tv' -> tv'
3974
3975 ---------------
3976 tidyTypes :: TidyEnv -> [Type] -> [Type]
3977 tidyTypes env tys = map (tidyType env) tys
3978
3979 ---------------
3980 tidyType :: TidyEnv -> Type -> Type
3981 tidyType _ (LitTy n) = LitTy n
3982 tidyType env (TyVarTy tv) = TyVarTy (tidyTyCoVarOcc env tv)
3983 tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
3984 in args `seqList` TyConApp tycon args
3985 tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
3986 tidyType env ty@(FunTy _ arg res) = let { !arg' = tidyType env arg
3987 ; !res' = tidyType env res }
3988 in ty { ft_arg = arg', ft_res = res' }
3989 tidyType env (ty@(ForAllTy{})) = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty
3990 where
3991 (tvs, vis, body_ty) = splitForAllTys' ty
3992 (env', tvs') = tidyVarBndrs env tvs
3993 tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCo env co)
3994 tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co)
3995
3996
3997 -- The following two functions differ from mkForAllTys and splitForAllTys in that
3998 -- they expect/preserve the ArgFlag argument. Thes belong to types/Type.hs, but
3999 -- how should they be named?
4000 mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type
4001 mkForAllTys' tvvs ty = foldr strictMkForAllTy ty tvvs
4002 where
4003 strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((Bndr $! tv) $! vis)) $! ty
4004
4005 splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type)
4006 splitForAllTys' ty = go ty [] []
4007 where
4008 go (ForAllTy (Bndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss)
4009 go ty tvs viss = (reverse tvs, reverse viss, ty)
4010
4011
4012 ---------------
4013 -- | Grabs the free type variables, tidies them
4014 -- and then uses 'tidyType' to work over the type itself
4015 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
4016 tidyOpenTypes env tys
4017 = (env', tidyTypes (trimmed_occ_env, var_env) tys)
4018 where
4019 (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $
4020 tyCoVarsOfTypesWellScoped tys
4021 trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
4022 -- The idea here was that we restrict the new TidyEnv to the
4023 -- _free_ vars of the types, so that we don't gratuitously rename
4024 -- the _bound_ variables of the types.
4025
4026 ---------------
4027 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
4028 tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in
4029 (env', ty')
4030
4031 ---------------
4032 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
4033 tidyTopType :: Type -> Type
4034 tidyTopType ty = tidyType emptyTidyEnv ty
4035
4036 ---------------
4037 tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
4038 tidyOpenKind = tidyOpenType
4039
4040 tidyKind :: TidyEnv -> Kind -> Kind
4041 tidyKind = tidyType
4042
4043 ----------------
4044 tidyCo :: TidyEnv -> Coercion -> Coercion
4045 tidyCo env@(_, subst) co
4046 = go co
4047 where
4048 go_mco MRefl = MRefl
4049 go_mco (MCo co) = MCo (go co)
4050
4051 go (Refl ty) = Refl (tidyType env ty)
4052 go (GRefl r ty mco) = GRefl r (tidyType env ty) $! go_mco mco
4053 go (TyConAppCo r tc cos) = let args = map go cos
4054 in args `seqList` TyConAppCo r tc args
4055 go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
4056 go (ForAllCo tv h co) = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co)
4057 where (envp, tvp) = tidyVarBndr env tv
4058 -- the case above duplicates a bit of work in tidying h and the kind
4059 -- of tv. But the alternative is to use coercionKind, which seems worse.
4060 go (FunCo r co1 co2) = (FunCo r $! go co1) $! go co2
4061 go (CoVarCo cv) = case lookupVarEnv subst cv of
4062 Nothing -> CoVarCo cv
4063 Just cv' -> CoVarCo cv'
4064 go (HoleCo h) = HoleCo h
4065 go (AxiomInstCo con ind cos) = let args = map go cos
4066 in args `seqList` AxiomInstCo con ind args
4067 go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $!
4068 tidyType env t1) $! tidyType env t2
4069 go (SymCo co) = SymCo $! go co
4070 go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
4071 go (NthCo r d co) = NthCo r d $! go co
4072 go (LRCo lr co) = LRCo lr $! go co
4073 go (InstCo co ty) = (InstCo $! go co) $! go ty
4074 go (KindCo co) = KindCo $! go co
4075 go (SubCo co) = SubCo $! go co
4076 go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos
4077 in cos1 `seqList` AxiomRuleCo ax cos1
4078
4079 go_prov UnsafeCoerceProv = UnsafeCoerceProv
4080 go_prov (PhantomProv co) = PhantomProv (go co)
4081 go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
4082 go_prov p@(PluginProv _) = p
4083
4084 tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
4085 tidyCos env = map (tidyCo env)
4086
4087
4088 {- *********************************************************************
4089 * *
4090 typeSize, coercionSize
4091 * *
4092 ********************************************************************* -}
4093
4094 -- NB: We put typeSize/coercionSize here because they are mutually
4095 -- recursive, and have the CPR property. If we have mutual
4096 -- recursion across a hi-boot file, we don't get the CPR property
4097 -- and these functions allocate a tremendous amount of rubbish.
4098 -- It's not critical (because typeSize is really only used in
4099 -- debug mode, but I tripped over an example (T5642) in which
4100 -- typeSize was one of the biggest single allocators in all of GHC.
4101 -- And it's easy to fix, so I did.
4102
4103