1{-# LANGUAGE CPP #-} 2{-# LANGUAGE DeriveDataTypeable #-} 3{-# LANGUAGE MultiWayIf #-} 4 5{-# OPTIONS_HADDOCK not-home #-} 6 7{- 8(c) The University of Glasgow 2006 9(c) The GRASP/AQUA Project, Glasgow University, 1998 10\section[GHC.Core.TyCo.Rep]{Type and Coercion - friends' interface} 11 12Note [The Type-related module hierarchy] 13~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 14 GHC.Core.Class 15 GHC.Core.Coercion.Axiom 16 GHC.Core.TyCon imports GHC.Core.{Class, Coercion.Axiom} 17 GHC.Core.TyCo.Rep imports GHC.Core.{Class, Coercion.Axiom, TyCon} 18 GHC.Core.TyCo.Ppr imports GHC.Core.TyCo.Rep 19 GHC.Core.TyCo.FVs imports GHC.Core.TyCo.Rep 20 GHC.Core.TyCo.Subst imports GHC.Core.TyCo.{Rep, FVs, Ppr} 21 GHC.Core.TyCo.Tidy imports GHC.Core.TyCo.{Rep, FVs} 22 GHC.Builtin.Types.Prim imports GHC.Core.TyCo.Rep ( including mkTyConTy ) 23 GHC.Core.Coercion imports GHC.Core.Type 24-} 25 26-- We expose the relevant stuff from this module via the Type module 27module GHC.Core.TyCo.Rep ( 28 29 -- * Types 30 Type(..), 31 32 TyLit(..), 33 KindOrType, Kind, 34 KnotTied, 35 PredType, ThetaType, -- Synonyms 36 ArgFlag(..), AnonArgFlag(..), 37 38 -- * Coercions 39 Coercion(..), 40 UnivCoProvenance(..), 41 CoercionHole(..), coHoleCoVar, setCoHoleCoVar, 42 CoercionN, CoercionR, CoercionP, KindCoercion, 43 MCoercion(..), MCoercionR, MCoercionN, 44 45 -- * Functions over types 46 mkTyConTy_, mkTyVarTy, mkTyVarTys, 47 mkTyCoVarTy, mkTyCoVarTys, 48 mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys, 49 mkForAllTy, mkForAllTys, mkInvisForAllTys, 50 mkPiTy, mkPiTys, 51 mkFunTyMany, 52 mkScaledFunTy, 53 mkVisFunTyMany, mkVisFunTysMany, 54 mkInvisFunTyMany, mkInvisFunTysMany, 55 nonDetCmpTyLit, cmpTyLit, 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 -- ** Analyzing types 69 TyCoFolder(..), foldTyCo, 70 71 -- * Sizes 72 typeSize, coercionSize, provSize, 73 74 -- * Multiplicities 75 Scaled(..), scaledMult, scaledThing, mapScaledType, Mult 76 ) where 77 78#include "GhclibHsVersions.h" 79 80import GHC.Prelude 81 82import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprCo, pprTyLit ) 83 84 -- Transitively pulls in a LOT of stuff, better to break the loop 85 86-- friends: 87import GHC.Iface.Type 88import GHC.Types.Var 89import GHC.Types.Var.Set 90import GHC.Core.TyCon 91import GHC.Core.Coercion.Axiom 92 93-- others 94import {-# SOURCE #-} GHC.Builtin.Types ( manyDataConTy ) 95import GHC.Types.Basic ( LeftOrRight(..), pickLR ) 96import GHC.Types.Unique ( Uniquable(..) ) 97import GHC.Utils.Outputable 98import GHC.Data.FastString 99import GHC.Utils.Misc 100import GHC.Utils.Panic 101 102-- libraries 103import qualified Data.Data as Data hiding ( TyCon ) 104import Data.IORef ( IORef ) -- for CoercionHole 105 106{- ********************************************************************** 107* * 108 Type 109* * 110********************************************************************** -} 111 112-- | The key representation of types within the compiler 113 114type KindOrType = Type -- See Note [Arguments to type constructors] 115 116-- | The key type representing kinds in the compiler. 117type Kind = Type 118 119-- If you edit this type, you may need to update the GHC formalism 120-- See Note [GHC Formalism] in GHC.Core.Lint 121data Type 122 -- See Note [Non-trivial definitional equality] 123 = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable) 124 125 | AppTy 126 Type 127 Type -- ^ Type application to something other than a 'TyCon'. Parameters: 128 -- 129 -- 1) Function: must /not/ be a 'TyConApp' or 'CastTy', 130 -- must be another 'AppTy', or 'TyVarTy' 131 -- See Note [Respecting definitional equality] \(EQ1) about the 132 -- no 'CastTy' requirement 133 -- 134 -- 2) Argument type 135 136 | TyConApp 137 TyCon 138 [KindOrType] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms. 139 -- Invariant: saturated applications of 'FunTyCon' must 140 -- use 'FunTy' and saturated synonyms must use their own 141 -- constructors. However, /unsaturated/ 'FunTyCon's 142 -- do appear as 'TyConApp's. 143 -- Parameters: 144 -- 145 -- 1) Type constructor being applied to. 146 -- 147 -- 2) Type arguments. Might not have enough type arguments 148 -- here to saturate the constructor. 149 -- Even type synonyms are not necessarily saturated; 150 -- for example unsaturated type synonyms 151 -- can appear as the right hand side of a type synonym. 152 153 | ForAllTy 154 {-# UNPACK #-} !TyCoVarBinder 155 Type -- ^ A Π type. 156 -- INVARIANT: If the binder is a coercion variable, it must 157 -- be mentioned in the Type. See 158 -- Note [Unused coercion variable in ForAllTy] 159 160 | FunTy -- ^ FUN m t1 t2 Very common, so an important special case 161 -- See Note [Function types] 162 { ft_af :: AnonArgFlag -- Is this (->) or (=>)? 163 , ft_mult :: Mult -- Multiplicity 164 , ft_arg :: Type -- Argument type 165 , ft_res :: Type } -- Result type 166 167 | LitTy TyLit -- ^ Type literals are similar to type constructors. 168 169 | CastTy 170 Type 171 KindCoercion -- ^ A kind cast. The coercion is always nominal. 172 -- INVARIANT: The cast is never reflexive 173 -- INVARIANT: The Type is not a CastTy (use TransCo instead) 174 -- INVARIANT: The Type is not a ForAllTy over a type variable 175 -- See Note [Respecting definitional equality] \(EQ2), (EQ3), (EQ4) 176 177 | CoercionTy 178 Coercion -- ^ Injection of a Coercion into a type 179 -- This should only ever be used in the RHS of an AppTy, 180 -- in the list of a TyConApp, when applying a promoted 181 -- GADT data constructor 182 183 deriving Data.Data 184 185instance Outputable Type where 186 ppr = pprType 187 188-- NOTE: Other parts of the code assume that type literals do not contain 189-- types or type variables. 190data TyLit 191 = NumTyLit Integer 192 | StrTyLit FastString 193 | CharTyLit Char 194 deriving (Eq, Data.Data) 195 196-- Non-determinism arises due to uniqCompareFS 197nonDetCmpTyLit :: TyLit -> TyLit -> Ordering 198nonDetCmpTyLit = cmpTyLitWith NonDetFastString 199 200-- Slower than nonDetCmpTyLit but deterministic 201cmpTyLit :: TyLit -> TyLit -> Ordering 202cmpTyLit = cmpTyLitWith LexicalFastString 203 204{-# INLINE cmpTyLitWith #-} 205cmpTyLitWith :: Ord r => (FastString -> r) -> TyLit -> TyLit -> Ordering 206cmpTyLitWith _ (NumTyLit x) (NumTyLit y) = compare x y 207cmpTyLitWith w (StrTyLit x) (StrTyLit y) = compare (w x) (w y) 208cmpTyLitWith _ (CharTyLit x) (CharTyLit y) = compare x y 209cmpTyLitWith _ a b = compare (tag a) (tag b) 210 where 211 tag :: TyLit -> Int 212 tag NumTyLit{} = 0 213 tag StrTyLit{} = 1 214 tag CharTyLit{} = 2 215 216instance Outputable TyLit where 217 ppr = pprTyLit 218 219{- Note [Function types] 220~~~~~~~~~~~~~~~~~~~~~~~~ 221FFunTy is the constructor for a function type. Lots of things to say 222about it! 223 224* FFunTy is the data constructor, meaning "full function type". 225 226* The function type constructor (->) has kind 227 (->) :: forall {r1} {r2}. TYPE r1 -> TYPE r2 -> Type LiftedRep 228 mkTyConApp ensure that we convert a saturated application 229 TyConApp (->) [r1,r2,t1,t2] into FunTy t1 t2 230 dropping the 'r1' and 'r2' arguments; they are easily recovered 231 from 't1' and 't2'. 232 233* For the time being its RuntimeRep quantifiers are left 234 inferred. This is to allow for it to evolve. 235 236* The ft_af field says whether or not this is an invisible argument 237 VisArg: t1 -> t2 Ordinary function type 238 InvisArg: t1 => t2 t1 is guaranteed to be a predicate type, 239 i.e. t1 :: Constraint 240 See Note [Types for coercions, predicates, and evidence] 241 242 This visibility info makes no difference in Core; it matters 243 only when we regard the type as a Haskell source type. 244 245* FunTy is a (unidirectional) pattern synonym that allows 246 positional pattern matching (FunTy arg res), ignoring the 247 ArgFlag. 248-} 249 250{- ----------------------- 251 Commented out until the pattern match 252 checker can handle it; see #16185 253 254 For now we use the CPP macro #define FunTy FFunTy _ 255 (see GhclibHsVersions.h) to allow pattern matching on a 256 (positional) FunTy constructor. 257 258{-# COMPLETE FunTy, TyVarTy, AppTy, TyConApp 259 , ForAllTy, LitTy, CastTy, CoercionTy :: Type #-} 260 261-- | 'FunTy' is a (uni-directional) pattern synonym for the common 262-- case where we want to match on the argument/result type, but 263-- ignoring the AnonArgFlag 264pattern FunTy :: Type -> Type -> Type 265pattern FunTy arg res <- FFunTy { ft_arg = arg, ft_res = res } 266 267 End of commented out block 268---------------------------------- -} 269 270{- Note [Types for coercions, predicates, and evidence] 271~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 272We treat differently: 273 274 (a) Predicate types 275 Test: isPredTy 276 Binders: DictIds 277 Kind: Constraint 278 Examples: (Eq a), and (a ~ b) 279 280 (b) Coercion types are primitive, unboxed equalities 281 Test: isCoVarTy 282 Binders: CoVars (can appear in coercions) 283 Kind: TYPE (TupleRep []) 284 Examples: (t1 ~# t2) or (t1 ~R# t2) 285 286 (c) Evidence types is the type of evidence manipulated by 287 the type constraint solver. 288 Test: isEvVarType 289 Binders: EvVars 290 Kind: Constraint or TYPE (TupleRep []) 291 Examples: all coercion types and predicate types 292 293Coercion types and predicate types are mutually exclusive, 294but evidence types are a superset of both. 295 296When treated as a user type, 297 298 - Predicates (of kind Constraint) are invisible and are 299 implicitly instantiated 300 301 - Coercion types, and non-pred evidence types (i.e. not 302 of kind Constrain), are just regular old types, are 303 visible, and are not implicitly instantiated. 304 305In a FunTy { ft_af = InvisArg }, the argument type is always 306a Predicate type. 307 308Note [Constraints in kinds] 309~~~~~~~~~~~~~~~~~~~~~~~~~~~ 310Do we allow a type constructor to have a kind like 311 S :: Eq a => a -> Type 312 313No, we do not. Doing so would mean would need a TyConApp like 314 S @k @(d :: Eq k) (ty :: k) 315 and we have no way to build, or decompose, evidence like 316 (d :: Eq k) at the type level. 317 318But we admit one exception: equality. We /do/ allow, say, 319 MkT :: (a ~ b) => a -> b -> Type a b 320 321Why? Because we can, without much difficulty. Moreover 322we can promote a GADT data constructor (see TyCon 323Note [Promoted data constructors]), like 324 data GT a b where 325 MkGT : a -> a -> GT a a 326so programmers might reasonably expect to be able to 327promote MkT as well. 328 329How does this work? 330 331* In GHC.Tc.Validity.checkConstraintsOK we reject kinds that 332 have constraints other than (a~b) and (a~~b). 333 334* In Inst.tcInstInvisibleTyBinder we instantiate a call 335 of MkT by emitting 336 [W] co :: alpha ~# beta 337 and producing the elaborated term 338 MkT @alpha @beta (Eq# alpha beta co) 339 We don't generate a boxed "Wanted"; we generate only a 340 regular old /unboxed/ primitive-equality Wanted, and build 341 the box on the spot. 342 343* How can we get such a MkT? By promoting a GADT-style data 344 constructor 345 data T a b where 346 MkT :: (a~b) => a -> b -> T a b 347 See DataCon.mkPromotedDataCon 348 and Note [Promoted data constructors] in GHC.Core.TyCon 349 350* We support both homogeneous (~) and heterogeneous (~~) 351 equality. (See Note [The equality types story] 352 in GHC.Builtin.Types.Prim for a primer on these equality types.) 353 354* How do we prevent a MkT having an illegal constraint like 355 Eq a? We check for this at use-sites; see GHC.Tc.Gen.HsType.tcTyVar, 356 specifically dc_theta_illegal_constraint. 357 358* Notice that nothing special happens if 359 K :: (a ~# b) => blah 360 because (a ~# b) is not a predicate type, and is never 361 implicitly instantiated. (Mind you, it's not clear how you 362 could creates a type constructor with such a kind.) See 363 Note [Types for coercions, predicates, and evidence] 364 365* The existence of promoted MkT with an equality-constraint 366 argument is the (only) reason that the AnonTCB constructor 367 of TyConBndrVis carries an AnonArgFlag (VisArg/InvisArg). 368 For example, when we promote the data constructor 369 MkT :: forall a b. (a~b) => a -> b -> T a b 370 we get a PromotedDataCon with tyConBinders 371 Bndr (a :: Type) (NamedTCB Inferred) 372 Bndr (b :: Type) (NamedTCB Inferred) 373 Bndr (_ :: a ~ b) (AnonTCB InvisArg) 374 Bndr (_ :: a) (AnonTCB VisArg)) 375 Bndr (_ :: b) (AnonTCB VisArg)) 376 377* One might reasonably wonder who *unpacks* these boxes once they are 378 made. After all, there is no type-level `case` construct. The 379 surprising answer is that no one ever does. Instead, if a GADT 380 constructor is used on the left-hand side of a type family equation, 381 that occurrence forces GHC to unify the types in question. For 382 example: 383 384 data G a where 385 MkG :: G Bool 386 387 type family F (x :: G a) :: a where 388 F MkG = False 389 390 When checking the LHS `F MkG`, GHC sees the MkG constructor and then must 391 unify F's implicit parameter `a` with Bool. This succeeds, making the equation 392 393 F Bool (MkG @Bool <Bool>) = False 394 395 Note that we never need unpack the coercion. This is because type 396 family equations are *not* parametric in their kind variables. That 397 is, we could have just said 398 399 type family H (x :: G a) :: a where 400 H _ = False 401 402 The presence of False on the RHS also forces `a` to become Bool, 403 giving us 404 405 H Bool _ = False 406 407 The fact that any of this works stems from the lack of phase 408 separation between types and kinds (unlike the very present phase 409 separation between terms and types). 410 411 Once we have the ability to pattern-match on types below top-level, 412 this will no longer cut it, but it seems fine for now. 413 414 415Note [Arguments to type constructors] 416~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 417Because of kind polymorphism, in addition to type application we now 418have kind instantiation. We reuse the same notations to do so. 419 420For example: 421 422 Just (* -> *) Maybe 423 Right * Nat Zero 424 425are represented by: 426 427 TyConApp (PromotedDataCon Just) [* -> *, Maybe] 428 TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)] 429 430Important note: Nat is used as a *kind* and not as a type. This can be 431confusing, since type-level Nat and kind-level Nat are identical. We 432use the kind of (PromotedDataCon Right) to know if its arguments are 433kinds or types. 434 435This kind instantiation only happens in TyConApp currently. 436 437Note [Non-trivial definitional equality] 438~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 439Is Int |> <*> the same as Int? YES! In order to reduce headaches, 440we decide that any reflexive casts in types are just ignored. 441(Indeed they must be. See Note [Respecting definitional equality].) 442More generally, the `eqType` function, which defines Core's type equality 443relation, ignores casts and coercion arguments, as long as the 444two types have the same kind. This allows us to be a little sloppier 445in keeping track of coercions, which is a good thing. It also means 446that eqType does not depend on eqCoercion, which is also a good thing. 447 448Why is this sensible? That is, why is something different than α-equivalence 449appropriate for the implementation of eqType? 450 451Anything smaller than ~ and homogeneous is an appropriate definition for 452equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any 453expression of type τ can be transmuted to one of type σ at any point by 454casting. The same is true of expressions of type σ. So in some sense, τ and σ 455are interchangeable. 456 457But let's be more precise. If we examine the typing rules of FC (say, those in 458https://cs.brynmawr.edu/~rae/papers/2015/equalities/equalities.pdf) 459there are several places where the same metavariable is used in two different 460premises to a rule. (For example, see Ty_App.) There is an implicit equality 461check here. What definition of equality should we use? By convention, we use 462α-equivalence. Take any rule with one (or more) of these implicit equality 463checks. Then there is an admissible rule that uses ~ instead of the implicit 464check, adding in casts as appropriate. 465 466The only problem here is that ~ is heterogeneous. To make the kinds work out 467in the admissible rule that uses ~, it is necessary to homogenize the 468coercions. That is, if we have η : (τ : κ1) ~ (σ : κ2), then we don't use η; 469we use η |> kind η, which is homogeneous. 470 471The effect of this all is that eqType, the implementation of the implicit 472equality check, can use any homogeneous relation that is smaller than ~, as 473those rules must also be admissible. 474 475A more drawn out argument around all of this is presented in Section 7.2 of 476Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf). 477 478What would go wrong if we insisted on the casts matching? See the beginning of 479Section 8 in the unpublished paper above. Theoretically, nothing at all goes 480wrong. But in practical terms, getting the coercions right proved to be 481nightmarish. And types would explode: during kind-checking, we often produce 482reflexive kind coercions. When we try to cast by these, mkCastTy just discards 483them. But if we used an eqType that distinguished between Int and Int |> <*>, 484then we couldn't discard -- the output of kind-checking would be enormous, 485and we would need enormous casts with lots of CoherenceCo's to straighten 486them out. 487 488Would anything go wrong if eqType respected type families? No, not at all. But 489that makes eqType rather hard to implement. 490 491Thus, the guideline for eqType is that it should be the largest 492easy-to-implement relation that is still smaller than ~ and homogeneous. The 493precise choice of relation is somewhat incidental, as long as the smart 494constructors and destructors in Type respect whatever relation is chosen. 495 496Another helpful principle with eqType is this: 497 498 (EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere. 499 500This principle also tells us that eqType must relate only types with the 501same kinds. 502 503Besides eqType, another equality relation that upholds the (EQ) property above 504is /typechecker equality/, which is implemented as 505GHC.Tc.Utils.TcType.tcEqType. See 506Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType for 507what the difference between eqType and tcEqType is. 508 509Note [Respecting definitional equality] 510~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 511Note [Non-trivial definitional equality] introduces the property (EQ). 512How is this upheld? 513 514Any function that pattern matches on all the constructors will have to 515consider the possibility of CastTy. Presumably, those functions will handle 516CastTy appropriately and we'll be OK. 517 518More dangerous are the splitXXX functions. Let's focus on splitTyConApp. 519We don't want it to fail on (T a b c |> co). Happily, if we have 520 (T a b c |> co) `eqType` (T d e f) 521then co must be reflexive. Why? eqType checks that the kinds are equal, as 522well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f). 523By the kind check, we know that (T a b c |> co) and (T d e f) have the same 524kind. So the only way that co could be non-reflexive is for (T a b c) to have 525a different kind than (T d e f). But because T's kind is closed (all tycon kinds 526are closed), the only way for this to happen is that one of the arguments has 527to differ, leading to a contradiction. Thus, co is reflexive. 528 529Accordingly, by eliminating reflexive casts, splitTyConApp need not worry 530about outermost casts to uphold (EQ). Eliminating reflexive casts is done 531in mkCastTy. 532 533Unforunately, that's not the end of the story. Consider comparing 534 (T a b c) =? (T a b |> (co -> <Type>)) (c |> co) 535These two types have the same kind (Type), but the left type is a TyConApp 536while the right type is not. To handle this case, we say that the right-hand 537type is ill-formed, requiring an AppTy never to have a casted TyConApp 538on its left. It is easy enough to pull around the coercions to maintain 539this invariant, as done in Type.mkAppTy. In the example above, trying to 540form the right-hand type will instead yield (T a b (c |> co |> sym co) |> <Type>). 541Both the casts there are reflexive and will be dropped. Huzzah. 542 543This idea of pulling coercions to the right works for splitAppTy as well. 544 545However, there is one hiccup: it's possible that a coercion doesn't relate two 546Pi-types. For example, if we have @type family Fun a b where Fun a b = a -> b@, 547then we might have (T :: Fun Type Type) and (T |> axFun) Int. That axFun can't 548be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not 549`eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate 550our (EQ) property. 551 552In order to detect reflexive casts reliably, we must make sure not 553to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)). 554 555One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy]. 556The kind of the body is the same as the kind of the ForAllTy. Accordingly, 557 558 ForAllTy tv (ty |> co) and (ForAllTy tv ty) |> co 559 560are `eqType`. But only the first can be split by splitForAllTy. So we forbid 561the second form, instead pushing the coercion inside to get the first form. 562This is done in mkCastTy. 563 564In sum, in order to uphold (EQ), we need the following invariants: 565 566 (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable 567 cast is one that relates either a FunTy to a FunTy or a 568 ForAllTy to a ForAllTy. 569 (EQ2) No reflexive casts in CastTy. 570 (EQ3) No nested CastTys. 571 (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body). 572 See Note [Weird typing rule for ForAllTy] 573 574These invariants are all documented above, in the declaration for Type. 575 576Note [Unused coercion variable in ForAllTy] 577~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 578Suppose we have 579 \(co:t1 ~ t2). e 580 581What type should we give to this expression? 582 (1) forall (co:t1 ~ t2) -> t 583 (2) (t1 ~ t2) -> t 584 585If co is used in t, (1) should be the right choice. 586if co is not used in t, we would like to have (1) and (2) equivalent. 587 588However, we want to keep eqType simple and don't want eqType (1) (2) to return 589True in any case. 590 591We decide to always construct (2) if co is not used in t. 592 593Thus in mkLamType, we check whether the variable is a coercion 594variable (of type (t1 ~# t2), and whether it is un-used in the 595body. If so, it returns a FunTy instead of a ForAllTy. 596 597There are cases we want to skip the check. For example, the check is 598unnecessary when it is known from the context that the input variable 599is a type variable. In those cases, we use mkForAllTy. 600 601Note [Weird typing rule for ForAllTy] 602~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 603Here is the (truncated) typing rule for the dependent ForAllTy: 604 605 inner : TYPE r 606 tyvar is not free in r 607 ---------------------------------------- 608 ForAllTy (Bndr tyvar vis) inner : TYPE r 609 610Note that the kind of `inner` is the kind of the overall ForAllTy. This is 611necessary because every ForAllTy over a type variable is erased at runtime. 612Thus the runtime representation of a ForAllTy (as encoded, via TYPE rep, in 613the kind) must be the same as the representation of the body. We must check 614for skolem-escape, though. The skolem-escape would prevent a definition like 615 616 undefined :: forall (r :: RuntimeRep) (a :: TYPE r). a 617 618because the type's kind (TYPE r) mentions the out-of-scope r. Luckily, the real 619type of undefined is 620 621 undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a 622 623and that HasCallStack constraint neatly sidesteps the potential skolem-escape 624problem. 625 626If the bound variable is a coercion variable: 627 628 inner : TYPE r 629 covar is free in inner 630 ------------------------------------ 631 ForAllTy (Bndr covar vis) inner : Type 632 633Here, the kind of the ForAllTy is just Type, because coercion abstractions 634are *not* erased. The "covar is free in inner" premise is solely to maintain 635the representation invariant documented in 636Note [Unused coercion variable in ForAllTy]. Though there is surface similarity 637between this free-var check and the one in the tyvar rule, these two restrictions 638are truly unrelated. 639 640-} 641 642-- | A type labeled 'KnotTied' might have knot-tied tycons in it. See 643-- Note [Type checking recursive type and class declarations] in 644-- "GHC.Tc.TyCl" 645type KnotTied ty = ty 646 647{- ********************************************************************** 648* * 649 TyCoBinder and ArgFlag 650* * 651********************************************************************** -} 652 653-- | A 'TyCoBinder' represents an argument to a function. TyCoBinders can be 654-- dependent ('Named') or nondependent ('Anon'). They may also be visible or 655-- not. See Note [TyCoBinders] 656data TyCoBinder 657 = Named TyCoVarBinder -- A type-lambda binder 658 | Anon AnonArgFlag (Scaled Type) -- A term-lambda binder. Type here can be CoercionTy. 659 -- Visibility is determined by the AnonArgFlag 660 deriving Data.Data 661 662instance Outputable TyCoBinder where 663 ppr (Anon af ty) = ppr af <+> ppr ty 664 ppr (Named (Bndr v Required)) = ppr v 665 -- See Note [Explicit Case Statement for Specificity] 666 ppr (Named (Bndr v (Invisible spec))) = case spec of 667 SpecifiedSpec -> char '@' <> ppr v 668 InferredSpec -> braces (ppr v) 669 670 671-- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder' 672-- in the 'Named' field. 673type TyBinder = TyCoBinder 674 675-- | Remove the binder's variable from the set, if the binder has 676-- a variable. 677delBinderVar :: VarSet -> TyCoVarBinder -> VarSet 678delBinderVar vars (Bndr tv _) = vars `delVarSet` tv 679 680-- | Does this binder bind an invisible argument? 681isInvisibleBinder :: TyCoBinder -> Bool 682isInvisibleBinder (Named (Bndr _ vis)) = isInvisibleArgFlag vis 683isInvisibleBinder (Anon InvisArg _) = True 684isInvisibleBinder (Anon VisArg _) = False 685 686-- | Does this binder bind a visible argument? 687isVisibleBinder :: TyCoBinder -> Bool 688isVisibleBinder = not . isInvisibleBinder 689 690isNamedBinder :: TyCoBinder -> Bool 691isNamedBinder (Named {}) = True 692isNamedBinder (Anon {}) = False 693 694-- | If its a named binder, is the binder a tyvar? 695-- Returns True for nondependent binder. 696-- This check that we're really returning a *Ty*Binder (as opposed to a 697-- coercion binder). That way, if/when we allow coercion quantification 698-- in more places, we'll know we missed updating some function. 699isTyBinder :: TyCoBinder -> Bool 700isTyBinder (Named bnd) = isTyVarBinder bnd 701isTyBinder _ = True 702 703{- Note [TyCoBinders] 704~~~~~~~~~~~~~~~~~~~ 705A ForAllTy contains a TyCoVarBinder. But a type can be decomposed 706to a telescope consisting of a [TyCoBinder] 707 708A TyCoBinder represents the type of binders -- that is, the type of an 709argument to a Pi-type. GHC Core currently supports two different 710Pi-types: 711 712 * A non-dependent function type, 713 written with ->, e.g. ty1 -> ty2 714 represented as FunTy ty1 ty2. These are 715 lifted to Coercions with the corresponding FunCo. 716 717 * A dependent compile-time-only polytype, 718 written with forall, e.g. forall (a:*). ty 719 represented as ForAllTy (Bndr a v) ty 720 721Both Pi-types classify terms/types that take an argument. In other 722words, if `x` is either a function or a polytype, `x arg` makes sense 723(for an appropriate `arg`). 724 725 726Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] 727~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 728* A ForAllTy (used for both types and kinds) contains a TyCoVarBinder. 729 Each TyCoVarBinder 730 Bndr a tvis 731 is equipped with tvis::ArgFlag, which says whether or not arguments 732 for this binder should be visible (explicit) in source Haskell. 733 734* A TyCon contains a list of TyConBinders. Each TyConBinder 735 Bndr a cvis 736 is equipped with cvis::TyConBndrVis, which says whether or not type 737 and kind arguments for this TyCon should be visible (explicit) in 738 source Haskell. 739 740This table summarises the visibility rules: 741--------------------------------------------------------------------------------------- 742| Occurrences look like this 743| GHC displays type as in Haskell source code 744|-------------------------------------------------------------------------------------- 745| Bndr a tvis :: TyCoVarBinder, in the binder of ForAllTy for a term 746| tvis :: ArgFlag 747| tvis = Inferred: f :: forall {a}. type Arg not allowed: f 748 f :: forall {co}. type Arg not allowed: f 749| tvis = Specified: f :: forall a. type Arg optional: f or f @Int 750| tvis = Required: T :: forall k -> type Arg required: T * 751| This last form is illegal in terms: See Note [No Required TyCoBinder in terms] 752| 753| Bndr k cvis :: TyConBinder, in the TyConBinders of a TyCon 754| cvis :: TyConBndrVis 755| cvis = AnonTCB: T :: kind -> kind Required: T * 756| cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T 757| T :: forall {co}. kind Arg not allowed: T 758| cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T 759| cvis = NamedTCB Required: T :: forall k -> kind Required: T * 760--------------------------------------------------------------------------------------- 761 762[1] In types, in the Specified case, it would make sense to allow 763 optional kind applications, thus (T @*), but we have not 764 yet implemented that 765 766---- In term declarations ---- 767 768* Inferred. Function defn, with no signature: f1 x = x 769 We infer f1 :: forall {a}. a -> a, with 'a' Inferred 770 It's Inferred because it doesn't appear in any 771 user-written signature for f1 772 773* Specified. Function defn, with signature (implicit forall): 774 f2 :: a -> a; f2 x = x 775 So f2 gets the type f2 :: forall a. a -> a, with 'a' Specified 776 even though 'a' is not bound in the source code by an explicit forall 777 778* Specified. Function defn, with signature (explicit forall): 779 f3 :: forall a. a -> a; f3 x = x 780 So f3 gets the type f3 :: forall a. a -> a, with 'a' Specified 781 782* Inferred. Function defn, with signature (explicit forall), marked as inferred: 783 f4 :: forall {a}. a -> a; f4 x = x 784 So f4 gets the type f4 :: forall {a}. a -> a, with 'a' Inferred 785 It's Inferred because the user marked it as such, even though it does appear 786 in the user-written signature for f4 787 788* Inferred/Specified. Function signature with inferred kind polymorphism. 789 f5 :: a b -> Int 790 So 'f5' gets the type f5 :: forall {k} (a:k->*) (b:k). a b -> Int 791 Here 'k' is Inferred (it's not mentioned in the type), 792 but 'a' and 'b' are Specified. 793 794* Specified. Function signature with explicit kind polymorphism 795 f6 :: a (b :: k) -> Int 796 This time 'k' is Specified, because it is mentioned explicitly, 797 so we get f6 :: forall (k:*) (a:k->*) (b:k). a b -> Int 798 799* Similarly pattern synonyms: 800 Inferred - from inferred types (e.g. no pattern type signature) 801 - or from inferred kind polymorphism 802 803---- In type declarations ---- 804 805* Inferred (k) 806 data T1 a b = MkT1 (a b) 807 Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> * 808 The kind variable 'k' is Inferred, since it is not mentioned 809 810 Note that 'a' and 'b' correspond to /Anon/ TyCoBinders in T1's kind, 811 and Anon binders don't have a visibility flag. (Or you could think 812 of Anon having an implicit Required flag.) 813 814* Specified (k) 815 data T2 (a::k->*) b = MkT (a b) 816 Here T's kind is T :: forall (k:*). (k->*) -> k -> * 817 The kind variable 'k' is Specified, since it is mentioned in 818 the signature. 819 820* Required (k) 821 data T k (a::k->*) b = MkT (a b) 822 Here T's kind is T :: forall k:* -> (k->*) -> k -> * 823 The kind is Required, since it bound in a positional way in T's declaration 824 Every use of T must be explicitly applied to a kind 825 826* Inferred (k1), Specified (k) 827 data T a b (c :: k) = MkT (a b) (Proxy c) 828 Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> * 829 So 'k' is Specified, because it appears explicitly, 830 but 'k1' is Inferred, because it does not 831 832Generally, in the list of TyConBinders for a TyCon, 833 834* Inferred arguments always come first 835* Specified, Anon and Required can be mixed 836 837e.g. 838 data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where ... 839 840Here Foo's TyConBinders are 841 [Required 'a', Specified 'b', Anon] 842and its kind prints as 843 Foo :: forall a -> forall b. (a -> b -> Type) -> Type 844 845See also Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl 846 847---- Printing ----- 848 849 We print forall types with enough syntax to tell you their visibility 850 flag. But this is not source Haskell, and these types may not all 851 be parsable. 852 853 Specified: a list of Specified binders is written between `forall` and `.`: 854 const :: forall a b. a -> b -> a 855 856 Inferred: like Specified, but every binder is written in braces: 857 f :: forall {k} (a:k). S k a -> Int 858 859 Required: binders are put between `forall` and `->`: 860 T :: forall k -> * 861 862---- Other points ----- 863 864* In classic Haskell, all named binders (that is, the type variables in 865 a polymorphic function type f :: forall a. a -> a) have been Inferred. 866 867* Inferred variables correspond to "generalized" variables from the 868 Visible Type Applications paper (ESOP'16). 869 870Note [No Required TyCoBinder in terms] 871~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 872We don't allow Required foralls for term variables, including pattern 873synonyms and data constructors. Why? Because then an application 874would need a /compulsory/ type argument (possibly without an "@"?), 875thus (f Int); and we don't have concrete syntax for that. 876 877We could change this decision, but Required, Named TyCoBinders are rare 878anyway. (Most are Anons.) 879 880However the type of a term can (just about) have a required quantifier; 881see Note [Required quantifiers in the type of a term] in GHC.Tc.Gen.Expr. 882-} 883 884 885{- ********************************************************************** 886* * 887 PredType 888* * 889********************************************************************** -} 890 891 892-- | A type of the form @p@ of constraint kind represents a value whose type is 893-- the Haskell predicate @p@, where a predicate is what occurs before 894-- the @=>@ in a Haskell type. 895-- 896-- We use 'PredType' as documentation to mark those types that we guarantee to 897-- have this kind. 898-- 899-- It can be expanded into its representation, but: 900-- 901-- * The type checker must treat it as opaque 902-- 903-- * The rest of the compiler treats it as transparent 904-- 905-- Consider these examples: 906-- 907-- > f :: (Eq a) => a -> Int 908-- > g :: (?x :: Int -> Int) => a -> Int 909-- > h :: (r\l) => {r} => {l::Int | r} 910-- 911-- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\" 912type PredType = Type 913 914-- | A collection of 'PredType's 915type ThetaType = [PredType] 916 917{- 918(We don't support TREX records yet, but the setup is designed 919to expand to allow them.) 920 921A Haskell qualified type, such as that for f,g,h above, is 922represented using 923 * a FunTy for the double arrow 924 * with a type of kind Constraint as the function argument 925 926The predicate really does turn into a real extra argument to the 927function. If the argument has type (p :: Constraint) then the predicate p is 928represented by evidence of type p. 929 930 931%************************************************************************ 932%* * 933 Simple constructors 934%* * 935%************************************************************************ 936 937These functions are here so that they can be used by GHC.Builtin.Types.Prim, 938which in turn is imported by Type 939-} 940 941mkTyVarTy :: TyVar -> Type 942mkTyVarTy v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) ) 943 TyVarTy v 944 945mkTyVarTys :: [TyVar] -> [Type] 946mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy 947 948mkTyCoVarTy :: TyCoVar -> Type 949mkTyCoVarTy v 950 | isTyVar v 951 = TyVarTy v 952 | otherwise 953 = CoercionTy (CoVarCo v) 954 955mkTyCoVarTys :: [TyCoVar] -> [Type] 956mkTyCoVarTys = map mkTyCoVarTy 957 958infixr 3 `mkFunTy`, `mkVisFunTy`, `mkInvisFunTy`, `mkVisFunTyMany`, 959 `mkInvisFunTyMany` -- Associates to the right 960 961mkFunTy :: AnonArgFlag -> Mult -> Type -> Type -> Type 962mkFunTy af mult arg res = FunTy { ft_af = af 963 , ft_mult = mult 964 , ft_arg = arg 965 , ft_res = res } 966 967mkScaledFunTy :: AnonArgFlag -> Scaled Type -> Type -> Type 968mkScaledFunTy af (Scaled mult arg) res = mkFunTy af mult arg res 969 970mkVisFunTy, mkInvisFunTy :: Mult -> Type -> Type -> Type 971mkVisFunTy = mkFunTy VisArg 972mkInvisFunTy = mkFunTy InvisArg 973 974mkFunTyMany :: AnonArgFlag -> Type -> Type -> Type 975mkFunTyMany af = mkFunTy af manyDataConTy 976 977-- | Special, common, case: Arrow type with mult Many 978mkVisFunTyMany :: Type -> Type -> Type 979mkVisFunTyMany = mkVisFunTy manyDataConTy 980 981mkInvisFunTyMany :: Type -> Type -> Type 982mkInvisFunTyMany = mkInvisFunTy manyDataConTy 983 984-- | Make nested arrow types 985mkVisFunTys :: [Scaled Type] -> Type -> Type 986mkVisFunTys tys ty = foldr (mkScaledFunTy VisArg) ty tys 987 988mkVisFunTysMany :: [Type] -> Type -> Type 989mkVisFunTysMany tys ty = foldr mkVisFunTyMany ty tys 990 991mkInvisFunTysMany :: [Type] -> Type -> Type 992mkInvisFunTysMany tys ty = foldr mkInvisFunTyMany ty tys 993 994-- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder 995-- See Note [Unused coercion variable in ForAllTy] 996mkForAllTy :: TyCoVar -> ArgFlag -> Type -> Type 997mkForAllTy tv vis ty = ForAllTy (Bndr tv vis) ty 998 999-- | Wraps foralls over the type using the provided 'TyCoVar's from left to right 1000mkForAllTys :: [TyCoVarBinder] -> Type -> Type 1001mkForAllTys tyvars ty = foldr ForAllTy ty tyvars 1002 1003-- | Wraps foralls over the type using the provided 'InvisTVBinder's from left to right 1004mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type 1005mkInvisForAllTys tyvars ty = foldr ForAllTy ty $ tyVarSpecToBinders tyvars 1006 1007mkPiTy :: TyCoBinder -> Type -> Type 1008mkPiTy (Anon af ty1) ty2 = mkScaledFunTy af ty1 ty2 1009mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty 1010 1011mkPiTys :: [TyCoBinder] -> Type -> Type 1012mkPiTys tbs ty = foldr mkPiTy ty tbs 1013 1014-- | Create a nullary 'TyConApp'. In general you should rather use 1015-- 'GHC.Core.Type.mkTyConTy'. This merely exists to break the import cycle 1016-- between 'GHC.Core.TyCon' and this module. 1017mkTyConTy_ :: TyCon -> Type 1018mkTyConTy_ tycon = TyConApp tycon [] 1019 1020{- 1021%************************************************************************ 1022%* * 1023 Coercions 1024%* * 1025%************************************************************************ 1026-} 1027 1028-- | A 'Coercion' is concrete evidence of the equality/convertibility 1029-- of two types. 1030 1031-- If you edit this type, you may need to update the GHC formalism 1032-- See Note [GHC Formalism] in GHC.Core.Lint 1033data Coercion 1034 -- Each constructor has a "role signature", indicating the way roles are 1035 -- propagated through coercions. 1036 -- - P, N, and R stand for coercions of the given role 1037 -- - e stands for a coercion of a specific unknown role 1038 -- (think "role polymorphism") 1039 -- - "e" stands for an explicit role parameter indicating role e. 1040 -- - _ stands for a parameter that is not a Role or Coercion. 1041 1042 -- These ones mirror the shape of types 1043 = -- Refl :: _ -> N 1044 -- A special case reflexivity for a very common case: Nominal reflexivity 1045 -- If you need Representational, use (GRefl Representational ty MRefl) 1046 -- not (SubCo (Refl ty)) 1047 Refl Type -- See Note [Refl invariant] 1048 1049 -- GRefl :: "e" -> _ -> Maybe N -> e 1050 -- See Note [Generalized reflexive coercion] 1051 | GRefl Role Type MCoercionN -- See Note [Refl invariant] 1052 -- Use (Refl ty), not (GRefl Nominal ty MRefl) 1053 -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _)) 1054 1055 -- These ones simply lift the correspondingly-named 1056 -- Type constructors into Coercions 1057 1058 -- TyConAppCo :: "e" -> _ -> ?? -> e 1059 -- See Note [TyConAppCo roles] 1060 | TyConAppCo Role TyCon [Coercion] -- lift TyConApp 1061 -- The TyCon is never a synonym; 1062 -- we expand synonyms eagerly 1063 -- But it can be a type function 1064 -- TyCon is never a saturated (->); use FunCo instead 1065 1066 | AppCo Coercion CoercionN -- lift AppTy 1067 -- AppCo :: e -> N -> e 1068 1069 -- See Note [Forall coercions] 1070 | ForAllCo TyCoVar KindCoercion Coercion 1071 -- ForAllCo :: _ -> N -> e -> e 1072 1073 | FunCo Role CoercionN Coercion Coercion -- lift FunTy 1074 -- FunCo :: "e" -> N -> e -> e -> e 1075 -- Note: why doesn't FunCo have a AnonArgFlag, like FunTy? 1076 -- Because the AnonArgFlag has no impact on Core; it is only 1077 -- there to guide implicit instantiation of Haskell source 1078 -- types, and that is irrelevant for coercions, which are 1079 -- Core-only. 1080 1081 -- These are special 1082 | CoVarCo CoVar -- :: _ -> (N or R) 1083 -- result role depends on the tycon of the variable's type 1084 1085 -- AxiomInstCo :: e -> _ -> ?? -> e 1086 | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion] 1087 -- See also [CoAxiom index] 1088 -- The coercion arguments always *precisely* saturate 1089 -- arity of (that branch of) the CoAxiom. If there are 1090 -- any left over, we use AppCo. 1091 -- See [Coercion axioms applied to coercions] 1092 -- The roles of the argument coercions are determined 1093 -- by the cab_roles field of the relevant branch of the CoAxiom 1094 1095 | AxiomRuleCo CoAxiomRule [Coercion] 1096 -- AxiomRuleCo is very like AxiomInstCo, but for a CoAxiomRule 1097 -- The number coercions should match exactly the expectations 1098 -- of the CoAxiomRule (i.e., the rule is fully saturated). 1099 1100 | UnivCo UnivCoProvenance Role Type Type 1101 -- :: _ -> "e" -> _ -> _ -> e 1102 1103 | SymCo Coercion -- :: e -> e 1104 | TransCo Coercion Coercion -- :: e -> e -> e 1105 1106 | NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn) 1107 -- :: "e" -> _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles]) 1108 -- Using NthCo on a ForAllCo gives an N coercion always 1109 -- See Note [NthCo and newtypes] 1110 -- 1111 -- Invariant: (NthCo r i co), it is always the case that r = role of (Nth i co) 1112 -- That is: the role of the entire coercion is redundantly cached here. 1113 -- See Note [NthCo Cached Roles] 1114 1115 | LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right) 1116 -- :: _ -> N -> N 1117 | InstCo Coercion CoercionN 1118 -- :: e -> N -> e 1119 -- See Note [InstCo roles] 1120 1121 -- Extract a kind coercion from a (heterogeneous) type coercion 1122 -- NB: all kind coercions are Nominal 1123 | KindCo Coercion 1124 -- :: e -> N 1125 1126 | SubCo CoercionN -- Turns a ~N into a ~R 1127 -- :: N -> R 1128 1129 | HoleCo CoercionHole -- ^ See Note [Coercion holes] 1130 -- Only present during typechecking 1131 deriving Data.Data 1132 1133type CoercionN = Coercion -- always nominal 1134type CoercionR = Coercion -- always representational 1135type CoercionP = Coercion -- always phantom 1136type KindCoercion = CoercionN -- always nominal 1137 1138instance Outputable Coercion where 1139 ppr = pprCo 1140 1141-- | A semantically more meaningful type to represent what may or may not be a 1142-- useful 'Coercion'. 1143data MCoercion 1144 = MRefl 1145 -- A trivial Reflexivity coercion 1146 | MCo Coercion 1147 -- Other coercions 1148 deriving Data.Data 1149type MCoercionR = MCoercion 1150type MCoercionN = MCoercion 1151 1152instance Outputable MCoercion where 1153 ppr MRefl = text "MRefl" 1154 ppr (MCo co) = text "MCo" <+> ppr co 1155 1156{- Note [Refl invariant] 1157~~~~~~~~~~~~~~~~~~~~~~~~ 1158Invariant 1: Refl lifting 1159 Refl (similar for GRefl r ty MRefl) is always lifted as far as possible. 1160 For example 1161 (Refl T) (Refl a) (Refl b) is normalised (by mkAPpCo) to (Refl (T a b)). 1162 1163 You might think that a consequences is: 1164 Every identity coercion has Refl at the root 1165 1166 But that's not quite true because of coercion variables. Consider 1167 g where g :: Int~Int 1168 Left h where h :: Maybe Int ~ Maybe Int 1169 etc. So the consequence is only true of coercions that 1170 have no coercion variables. 1171 1172Invariant 2: TyConAppCo 1173 An application of (Refl T) to some coercions, at least one of which is 1174 NOT the identity, is normalised to TyConAppCo. (They may not be 1175 fully saturated however.) TyConAppCo coercions (like all coercions 1176 other than Refl) are NEVER the identity. 1177 1178Note [Generalized reflexive coercion] 1179~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1180GRefl is a generalized reflexive coercion (see #15192). It wraps a kind 1181coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing 1182rules for GRefl: 1183 1184 ty : k1 1185 ------------------------------------ 1186 GRefl r ty MRefl: ty ~r ty 1187 1188 ty : k1 co :: k1 ~ k2 1189 ------------------------------------ 1190 GRefl r ty (MCo co) : ty ~r ty |> co 1191 1192Consider we have 1193 1194 g1 :: s ~r t 1195 s :: k1 1196 g2 :: k1 ~ k2 1197 1198and we want to construct a coercions co which has type 1199 1200 (s |> g2) ~r t 1201 1202We can define 1203 1204 co = Sym (GRefl r s g2) ; g1 1205 1206It is easy to see that 1207 1208 Refl == GRefl Nominal ty MRefl :: ty ~n ty 1209 1210A nominal reflexive coercion is quite common, so we keep the special form Refl to 1211save allocation. 1212 1213Note [Coercion axioms applied to coercions] 1214~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1215The reason coercion axioms can be applied to coercions and not just 1216types is to allow for better optimization. There are some cases where 1217we need to be able to "push transitivity inside" an axiom in order to 1218expose further opportunities for optimization. 1219 1220For example, suppose we have 1221 1222 C a : t[a] ~ F a 1223 g : b ~ c 1224 1225and we want to optimize 1226 1227 sym (C b) ; t[g] ; C c 1228 1229which has the kind 1230 1231 F b ~ F c 1232 1233(stopping through t[b] and t[c] along the way). 1234 1235We'd like to optimize this to just F g -- but how? The key is 1236that we need to allow axioms to be instantiated by *coercions*, 1237not just by types. Then we can (in certain cases) push 1238transitivity inside the axiom instantiations, and then react 1239opposite-polarity instantiations of the same axiom. In this 1240case, e.g., we match t[g] against the LHS of (C c)'s kind, to 1241obtain the substitution a |-> g (note this operation is sort 1242of the dual of lifting!) and hence end up with 1243 1244 C g : t[b] ~ F c 1245 1246which indeed has the same kind as t[g] ; C c. 1247 1248Now we have 1249 1250 sym (C b) ; C g 1251 1252which can be optimized to F g. 1253 1254Note [CoAxiom index] 1255~~~~~~~~~~~~~~~~~~~~ 1256A CoAxiom has 1 or more branches. Each branch has contains a list 1257of the free type variables in that branch, the LHS type patterns, 1258and the RHS type for that branch. When we apply an axiom to a list 1259of coercions, we must choose which branch of the axiom we wish to 1260use, as the different branches may have different numbers of free 1261type variables. (The number of type patterns is always the same 1262among branches, but that doesn't quite concern us here.) 1263 1264The Int in the AxiomInstCo constructor is the 0-indexed number 1265of the chosen branch. 1266 1267Note [Forall coercions] 1268~~~~~~~~~~~~~~~~~~~~~~~ 1269Constructing coercions between forall-types can be a bit tricky, 1270because the kinds of the bound tyvars can be different. 1271 1272The typing rule is: 1273 1274 1275 kind_co : k1 ~ k2 1276 tv1:k1 |- co : t1 ~ t2 1277 ------------------------------------------------------------------- 1278 ForAllCo tv1 kind_co co : all tv1:k1. t1 ~ 1279 all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co]) 1280 1281First, the TyCoVar stored in a ForAllCo is really an optimisation: this field 1282should be a Name, as its kind is redundant. Thinking of the field as a Name 1283is helpful in understanding what a ForAllCo means. 1284The kind of TyCoVar always matches the left-hand kind of the coercion. 1285 1286The idea is that kind_co gives the two kinds of the tyvar. See how, in the 1287conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right. 1288 1289Of course, a type variable can't have different kinds at the same time. So, 1290we arbitrarily prefer the first kind when using tv1 in the inner coercion 1291co, which shows that t1 equals t2. 1292 1293The last wrinkle is that we need to fix the kinds in the conclusion. In 1294t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of 1295the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with 1296(tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it 1297mentions the same name with different kinds, but it *is* well-kinded, noting 1298that `(tv1:k2) |> sym kind_co` has kind k1. 1299 1300This all really would work storing just a Name in the ForAllCo. But we can't 1301add Names to, e.g., VarSets, and there generally is just an impedance mismatch 1302in a bunch of places. So we use tv1. When we need tv2, we can use 1303setTyVarKind. 1304 1305Note [Predicate coercions] 1306~~~~~~~~~~~~~~~~~~~~~~~~~~ 1307Suppose we have 1308 g :: a~b 1309How can we coerce between types 1310 ([c]~a) => [a] -> c 1311and 1312 ([c]~b) => [b] -> c 1313where the equality predicate *itself* differs? 1314 1315Answer: we simply treat (~) as an ordinary type constructor, so these 1316types really look like 1317 1318 ((~) [c] a) -> [a] -> c 1319 ((~) [c] b) -> [b] -> c 1320 1321So the coercion between the two is obviously 1322 1323 ((~) [c] g) -> [g] -> c 1324 1325Another way to see this to say that we simply collapse predicates to 1326their representation type (see Type.coreView and Type.predTypeRep). 1327 1328This collapse is done by mkPredCo; there is no PredCo constructor 1329in Coercion. This is important because we need Nth to work on 1330predicates too: 1331 Nth 1 ((~) [c] g) = g 1332See Simplify.simplCoercionF, which generates such selections. 1333 1334Note [Roles] 1335~~~~~~~~~~~~ 1336Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated 1337in #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see 1338https://gitlab.haskell.org/ghc/ghc/wikis/roles-implementation 1339 1340Here is one way to phrase the problem: 1341 1342Given: 1343newtype Age = MkAge Int 1344type family F x 1345type instance F Age = Bool 1346type instance F Int = Char 1347 1348This compiles down to: 1349axAge :: Age ~ Int 1350axF1 :: F Age ~ Bool 1351axF2 :: F Int ~ Char 1352 1353Then, we can make: 1354(sym (axF1) ; F axAge ; axF2) :: Bool ~ Char 1355 1356Yikes! 1357 1358The solution is _roles_, as articulated in "Generative Type Abstraction and 1359Type-level Computation" (POPL 2010), available at 1360http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf 1361 1362The specification for roles has evolved somewhat since that paper. For the 1363current full details, see the documentation in docs/core-spec. Here are some 1364highlights. 1365 1366We label every equality with a notion of type equivalence, of which there are 1367three options: Nominal, Representational, and Phantom. A ground type is 1368nominally equivalent only with itself. A newtype (which is considered a ground 1369type in Haskell) is representationally equivalent to its representation. 1370Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P" 1371to denote the equivalences. 1372 1373The axioms above would be: 1374axAge :: Age ~R Int 1375axF1 :: F Age ~N Bool 1376axF2 :: F Age ~N Char 1377 1378Then, because transitivity applies only to coercions proving the same notion 1379of equivalence, the above construction is impossible. 1380 1381However, there is still an escape hatch: we know that any two types that are 1382nominally equivalent are representationally equivalent as well. This is what 1383the form SubCo proves -- it "demotes" a nominal equivalence into a 1384representational equivalence. So, it would seem the following is possible: 1385 1386sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG 1387 1388What saves us here is that the arguments to a type function F, lifted into a 1389coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and 1390we are safe. 1391 1392Roles are attached to parameters to TyCons. When lifting a TyCon into a 1393coercion (through TyConAppCo), we need to ensure that the arguments to the 1394TyCon respect their roles. For example: 1395 1396data T a b = MkT a (F b) 1397 1398If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know 1399that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because 1400the type function F branches on b's *name*, not representation. So, we say 1401that 'a' has role Representational and 'b' has role Nominal. The third role, 1402Phantom, is for parameters not used in the type's definition. Given the 1403following definition 1404 1405data Q a = MkQ Int 1406 1407the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we 1408can construct the coercion Bool ~P Char (using UnivCo). 1409 1410See the paper cited above for more examples and information. 1411 1412Note [TyConAppCo roles] 1413~~~~~~~~~~~~~~~~~~~~~~~ 1414The TyConAppCo constructor has a role parameter, indicating the role at 1415which the coercion proves equality. The choice of this parameter affects 1416the required roles of the arguments of the TyConAppCo. To help explain 1417it, assume the following definition: 1418 1419 type instance F Int = Bool -- Axiom axF : F Int ~N Bool 1420 newtype Age = MkAge Int -- Axiom axAge : Age ~R Int 1421 data Foo a = MkFoo a -- Role on Foo's parameter is Representational 1422 1423TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool 1424 For (TyConAppCo Nominal) all arguments must have role Nominal. Why? 1425 So that Foo Age ~N Foo Int does *not* hold. 1426 1427TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool 1428TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int 1429 For (TyConAppCo Representational), all arguments must have the roles 1430 corresponding to the result of tyConRoles on the TyCon. This is the 1431 whole point of having roles on the TyCon to begin with. So, we can 1432 have Foo Age ~R Foo Int, if Foo's parameter has role R. 1433 1434 If a Representational TyConAppCo is over-saturated (which is otherwise fine), 1435 the spill-over arguments must all be at Nominal. This corresponds to the 1436 behavior for AppCo. 1437 1438TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool 1439 All arguments must have role Phantom. This one isn't strictly 1440 necessary for soundness, but this choice removes ambiguity. 1441 1442The rules here dictate the roles of the parameters to mkTyConAppCo 1443(should be checked by Lint). 1444 1445Note [NthCo and newtypes] 1446~~~~~~~~~~~~~~~~~~~~~~~~~ 1447Suppose we have 1448 1449 newtype N a = MkN Int 1450 type role N representational 1451 1452This yields axiom 1453 1454 NTCo:N :: forall a. N a ~R Int 1455 1456We can then build 1457 1458 co :: forall a b. N a ~R N b 1459 co = NTCo:N a ; sym (NTCo:N b) 1460 1461for any `a` and `b`. Because of the role annotation on N, if we use 1462NthCo, we'll get out a representational coercion. That is: 1463 1464 NthCo r 0 co :: forall a b. a ~R b 1465 1466Yikes! Clearly, this is terrible. The solution is simple: forbid 1467NthCo to be used on newtypes if the internal coercion is representational. 1468 1469This is not just some corner case discovered by a segfault somewhere; 1470it was discovered in the proof of soundness of roles and described 1471in the "Safe Coercions" paper (ICFP '14). 1472 1473Note [NthCo Cached Roles] 1474~~~~~~~~~~~~~~~~~~~~~~~~~ 1475Why do we cache the role of NthCo in the NthCo constructor? 1476Because computing role(Nth i co) involves figuring out that 1477 1478 co :: T tys1 ~ T tys2 1479 1480using coercionKind, and finding (coercionRole co), and then looking 1481at the tyConRoles of T. Avoiding bad asymptotic behaviour here means 1482we have to compute the kind and role of a coercion simultaneously, 1483which makes the code complicated and inefficient. 1484 1485This only happens for NthCo. Caching the role solves the problem, and 1486allows coercionKind and coercionRole to be simple. 1487 1488See #11735 1489 1490Note [InstCo roles] 1491~~~~~~~~~~~~~~~~~~~ 1492Here is (essentially) the typing rule for InstCo: 1493 1494g :: (forall a. t1) ~r (forall a. t2) 1495w :: s1 ~N s2 1496------------------------------- InstCo 1497InstCo g w :: (t1 [a |-> s1]) ~r (t2 [a |-> s2]) 1498 1499Note that the Coercion w *must* be nominal. This is necessary 1500because the variable a might be used in a "nominal position" 1501(that is, a place where role inference would require a nominal 1502role) in t1 or t2. If we allowed w to be representational, we 1503could get bogus equalities. 1504 1505A more nuanced treatment might be able to relax this condition 1506somewhat, by checking if t1 and/or t2 use their bound variables 1507in nominal ways. If not, having w be representational is OK. 1508 1509 1510%************************************************************************ 1511%* * 1512 UnivCoProvenance 1513%* * 1514%************************************************************************ 1515 1516A UnivCo is a coercion whose proof does not directly express its role 1517and kind (indeed for some UnivCos, like PluginProv, there /is/ no proof). 1518 1519The different kinds of UnivCo are described by UnivCoProvenance. Really 1520each is entirely separate, but they all share the need to represent their 1521role and kind, which is done in the UnivCo constructor. 1522 1523-} 1524 1525-- | For simplicity, we have just one UnivCo that represents a coercion from 1526-- some type to some other type, with (in general) no restrictions on the 1527-- type. The UnivCoProvenance specifies more exactly what the coercion really 1528-- is and why a program should (or shouldn't!) trust the coercion. 1529-- It is reasonable to consider each constructor of 'UnivCoProvenance' 1530-- as a totally independent coercion form; their only commonality is 1531-- that they don't tell you what types they coercion between. (That info 1532-- is in the 'UnivCo' constructor of 'Coercion'. 1533data UnivCoProvenance 1534 = PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom 1535 -- roled coercions 1536 1537 | ProofIrrelProv KindCoercion -- ^ From the fact that any two coercions are 1538 -- considered equivalent. See Note [ProofIrrelProv]. 1539 -- Can be used in Nominal or Representational coercions 1540 1541 | PluginProv String -- ^ From a plugin, which asserts that this coercion 1542 -- is sound. The string is for the use of the plugin. 1543 1544 | CorePrepProv -- See Note [Unsafe coercions] in GHC.Core.CoreToStg.Pprep 1545 1546 deriving Data.Data 1547 1548instance Outputable UnivCoProvenance where 1549 ppr (PhantomProv _) = text "(phantom)" 1550 ppr (ProofIrrelProv _) = text "(proof irrel.)" 1551 ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str)) 1552 ppr CorePrepProv = text "(CorePrep)" 1553 1554-- | A coercion to be filled in by the type-checker. See Note [Coercion holes] 1555data CoercionHole 1556 = CoercionHole { ch_co_var :: CoVar 1557 -- See Note [CoercionHoles and coercion free variables] 1558 1559 , ch_ref :: IORef (Maybe Coercion) 1560 } 1561 1562coHoleCoVar :: CoercionHole -> CoVar 1563coHoleCoVar = ch_co_var 1564 1565setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole 1566setCoHoleCoVar h cv = h { ch_co_var = cv } 1567 1568instance Data.Data CoercionHole where 1569 -- don't traverse? 1570 toConstr _ = abstractConstr "CoercionHole" 1571 gunfold _ _ = error "gunfold" 1572 dataTypeOf _ = mkNoRepType "CoercionHole" 1573 1574instance Outputable CoercionHole where 1575 ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv) 1576 1577instance Uniquable CoercionHole where 1578 getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv 1579 1580{- Note [Phantom coercions] 1581~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1582Consider 1583 data T a = T1 | T2 1584Then we have 1585 T s ~R T t 1586for any old s,t. The witness for this is (TyConAppCo T Rep co), 1587where (co :: s ~P t) is a phantom coercion built with PhantomProv. 1588The role of the UnivCo is always Phantom. The Coercion stored is the 1589(nominal) kind coercion between the types 1590 kind(s) ~N kind (t) 1591 1592Note [Coercion holes] 1593~~~~~~~~~~~~~~~~~~~~~~~~ 1594During typechecking, constraint solving for type classes works by 1595 - Generate an evidence Id, d7 :: Num a 1596 - Wrap it in a Wanted constraint, [W] d7 :: Num a 1597 - Use the evidence Id where the evidence is needed 1598 - Solve the constraint later 1599 - When solved, add an enclosing let-binding let d7 = .... in .... 1600 which actually binds d7 to the (Num a) evidence 1601 1602For equality constraints we use a different strategy. See Note [The 1603equality types story] in GHC.Builtin.Types.Prim for background on equality constraints. 1604 - For /boxed/ equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just 1605 like type classes above. (Indeed, boxed equality constraints *are* classes.) 1606 - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2) 1607 we use a different plan 1608 1609For unboxed equalities: 1610 - Generate a CoercionHole, a mutable variable just like a unification 1611 variable 1612 - Wrap the CoercionHole in a Wanted constraint; see GHC.Tc.Utils.TcEvDest 1613 - Use the CoercionHole in a Coercion, via HoleCo 1614 - Solve the constraint later 1615 - When solved, fill in the CoercionHole by side effect, instead of 1616 doing the let-binding thing 1617 1618The main reason for all this is that there may be no good place to let-bind 1619the evidence for unboxed equalities: 1620 1621 - We emit constraints for kind coercions, to be used to cast a 1622 type's kind. These coercions then must be used in types. Because 1623 they might appear in a top-level type, there is no place to bind 1624 these (unlifted) coercions in the usual way. 1625 1626 - A coercion for (forall a. t1) ~ (forall a. t2) will look like 1627 forall a. (coercion for t1~t2) 1628 But the coercion for (t1~t2) may mention 'a', and we don't have 1629 let-bindings within coercions. We could add them, but coercion 1630 holes are easier. 1631 1632 - Moreover, nothing is lost from the lack of let-bindings. For 1633 dictionaries want to achieve sharing to avoid recomoputing the 1634 dictionary. But coercions are entirely erased, so there's little 1635 benefit to sharing. Indeed, even if we had a let-binding, we 1636 always inline types and coercions at every use site and drop the 1637 binding. 1638 1639Other notes about HoleCo: 1640 1641 * INVARIANT: CoercionHole and HoleCo are used only during type checking, 1642 and should never appear in Core. Just like unification variables; a Type 1643 can contain a TcTyVar, but only during type checking. If, one day, we 1644 use type-level information to separate out forms that can appear during 1645 type-checking vs forms that can appear in core proper, holes in Core will 1646 be ruled out. 1647 1648 * See Note [CoercionHoles and coercion free variables] 1649 1650 * Coercion holes can be compared for equality like other coercions: 1651 by looking at the types coerced. 1652 1653 1654Note [CoercionHoles and coercion free variables] 1655~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1656Why does a CoercionHole contain a CoVar, as well as reference to 1657fill in? Because we want to treat that CoVar as a free variable of 1658the coercion. See #14584, and Note [What prevents a 1659constraint from floating] in GHC.Tc.Solver, item (4): 1660 1661 forall k. [W] co1 :: t1 ~# t2 |> co2 1662 [W] co2 :: k ~# * 1663 1664Here co2 is a CoercionHole. But we /must/ know that it is free in 1665co1, because that's all that stops it floating outside the 1666implication. 1667 1668 1669Note [ProofIrrelProv] 1670~~~~~~~~~~~~~~~~~~~~~ 1671A ProofIrrelProv is a coercion between coercions. For example: 1672 1673 data G a where 1674 MkG :: G Bool 1675 1676In core, we get 1677 1678 G :: * -> * 1679 MkG :: forall (a :: *). (a ~ Bool) -> G a 1680 1681Now, consider 'MkG -- that is, MkG used in a type -- and suppose we want 1682a proof that ('MkG a1 co1) ~ ('MkG a2 co2). This will have to be 1683 1684 TyConAppCo Nominal MkG [co3, co4] 1685 where 1686 co3 :: co1 ~ co2 1687 co4 :: a1 ~ a2 1688 1689Note that 1690 co1 :: a1 ~ Bool 1691 co2 :: a2 ~ Bool 1692 1693Here, 1694 co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2) 1695 where 1696 co5 :: (a1 ~ Bool) ~ (a2 ~ Bool) 1697 co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>] 1698-} 1699 1700 1701{- ********************************************************************* 1702* * 1703 foldType and foldCoercion 1704* * 1705********************************************************************* -} 1706 1707{- Note [foldType] 1708~~~~~~~~~~~~~~~~~~ 1709foldType is a bit more powerful than perhaps it looks: 1710 1711* You can fold with an accumulating parameter, via 1712 TyCoFolder env (Endo a) 1713 Recall newtype Endo a = Endo (a->a) 1714 1715* You can fold monadically with a monad M, via 1716 TyCoFolder env (M a) 1717 provided you have 1718 instance .. => Monoid (M a) 1719 1720Note [mapType vs foldType] 1721~~~~~~~~~~~~~~~~~~~~~~~~~~ 1722We define foldType here, but mapType in module Type. Why? 1723 1724* foldType is used in GHC.Core.TyCo.FVs for finding free variables. 1725 It's a very simple function that analyses a type, 1726 but does not construct one. 1727 1728* mapType constructs new types, and so it needs to call 1729 the "smart constructors", mkAppTy, mkCastTy, and so on. 1730 These are sophisticated functions, and can't be defined 1731 here in GHC.Core.TyCo.Rep. 1732 1733Note [Specialising foldType] 1734~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1735We inline foldType at every call site (there are not many), so that it 1736becomes specialised for the particular monoid *and* TyCoFolder at 1737that site. This is just for efficiency, but walking over types is 1738done a *lot* in GHC, so worth optimising. 1739 1740We were worried that 1741 TyCoFolder env (Endo a) 1742might not eta-expand. Recall newtype Endo a = Endo (a->a). 1743 1744In particular, given 1745 fvs :: Type -> TyCoVarSet 1746 fvs ty = appEndo (foldType tcf emptyVarSet ty) emptyVarSet 1747 1748 tcf :: TyCoFolder enf (Endo a) 1749 tcf = TyCoFolder { tcf_tyvar = do_tv, ... } 1750 where 1751 do_tvs is tv = Endo do_it 1752 where 1753 do_it acc | tv `elemVarSet` is = acc 1754 | tv `elemVarSet` acc = acc 1755 | otherwise = acc `extendVarSet` tv 1756 1757 1758we want to end up with 1759 fvs ty = go emptyVarSet ty emptyVarSet 1760 where 1761 go env (TyVarTy tv) acc = acc `extendVarSet` tv 1762 ..etc.. 1763 1764And indeed this happens. 1765 - Selections from 'tcf' are done at compile time 1766 - 'go' is nicely eta-expanded. 1767 1768We were also worried about 1769 deep_fvs :: Type -> TyCoVarSet 1770 deep_fvs ty = appEndo (foldType deep_tcf emptyVarSet ty) emptyVarSet 1771 1772 deep_tcf :: TyCoFolder enf (Endo a) 1773 deep_tcf = TyCoFolder { tcf_tyvar = do_tv, ... } 1774 where 1775 do_tvs is tv = Endo do_it 1776 where 1777 do_it acc | tv `elemVarSet` is = acc 1778 | tv `elemVarSet` acc = acc 1779 | otherwise = deep_fvs (varType tv) 1780 `unionVarSet` acc 1781 `extendVarSet` tv 1782 1783Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf. 1784But, amazingly, we get good code here too. GHC is careful not to makr 1785TyCoFolder data constructor for deep_tcf as a loop breaker, so the 1786record selections still cancel. And eta expansion still happens too. 1787-} 1788 1789data TyCoFolder env a 1790 = TyCoFolder 1791 { tcf_view :: Type -> Maybe Type -- Optional "view" function 1792 -- E.g. expand synonyms 1793 , tcf_tyvar :: env -> TyVar -> a 1794 , tcf_covar :: env -> CoVar -> a 1795 , tcf_hole :: env -> CoercionHole -> a 1796 -- ^ What to do with coercion holes. 1797 -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep". 1798 1799 , tcf_tycobinder :: env -> TyCoVar -> ArgFlag -> env 1800 -- ^ The returned env is used in the extended scope 1801 } 1802 1803{-# INLINE foldTyCo #-} -- See Note [Specialising foldType] 1804foldTyCo :: Monoid a => TyCoFolder env a -> env 1805 -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a) 1806foldTyCo (TyCoFolder { tcf_view = view 1807 , tcf_tyvar = tyvar 1808 , tcf_tycobinder = tycobinder 1809 , tcf_covar = covar 1810 , tcf_hole = cohole }) env 1811 = (go_ty env, go_tys env, go_co env, go_cos env) 1812 where 1813 go_ty env ty | Just ty' <- view ty = go_ty env ty' 1814 go_ty env (TyVarTy tv) = tyvar env tv 1815 go_ty env (AppTy t1 t2) = go_ty env t1 `mappend` go_ty env t2 1816 go_ty _ (LitTy {}) = mempty 1817 go_ty env (CastTy ty co) = go_ty env ty `mappend` go_co env co 1818 go_ty env (CoercionTy co) = go_co env co 1819 go_ty env (FunTy _ w arg res) = go_ty env w `mappend` go_ty env arg `mappend` go_ty env res 1820 go_ty env (TyConApp _ tys) = go_tys env tys 1821 go_ty env (ForAllTy (Bndr tv vis) inner) 1822 = let !env' = tycobinder env tv vis -- Avoid building a thunk here 1823 in go_ty env (varType tv) `mappend` go_ty env' inner 1824 1825 -- Explicit recursion because using foldr builds a local 1826 -- loop (with env free) and I'm not confident it'll be 1827 -- lambda lifted in the end 1828 go_tys _ [] = mempty 1829 go_tys env (t:ts) = go_ty env t `mappend` go_tys env ts 1830 1831 go_cos _ [] = mempty 1832 go_cos env (c:cs) = go_co env c `mappend` go_cos env cs 1833 1834 go_co env (Refl ty) = go_ty env ty 1835 go_co env (GRefl _ ty MRefl) = go_ty env ty 1836 go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co 1837 go_co env (TyConAppCo _ _ args) = go_cos env args 1838 go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2 1839 go_co env (FunCo _ cw c1 c2) = go_co env cw `mappend` 1840 go_co env c1 `mappend` 1841 go_co env c2 1842 go_co env (CoVarCo cv) = covar env cv 1843 go_co env (AxiomInstCo _ _ args) = go_cos env args 1844 go_co env (HoleCo hole) = cohole env hole 1845 go_co env (UnivCo p _ t1 t2) = go_prov env p `mappend` go_ty env t1 1846 `mappend` go_ty env t2 1847 go_co env (SymCo co) = go_co env co 1848 go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2 1849 go_co env (AxiomRuleCo _ cos) = go_cos env cos 1850 go_co env (NthCo _ _ co) = go_co env co 1851 go_co env (LRCo _ co) = go_co env co 1852 go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg 1853 go_co env (KindCo co) = go_co env co 1854 go_co env (SubCo co) = go_co env co 1855 go_co env (ForAllCo tv kind_co co) 1856 = go_co env kind_co `mappend` go_ty env (varType tv) 1857 `mappend` go_co env' co 1858 where 1859 env' = tycobinder env tv Inferred 1860 1861 go_prov env (PhantomProv co) = go_co env co 1862 go_prov env (ProofIrrelProv co) = go_co env co 1863 go_prov _ (PluginProv _) = mempty 1864 go_prov _ CorePrepProv = mempty 1865 1866{- ********************************************************************* 1867* * 1868 typeSize, coercionSize 1869* * 1870********************************************************************* -} 1871 1872-- NB: We put typeSize/coercionSize here because they are mutually 1873-- recursive, and have the CPR property. If we have mutual 1874-- recursion across a hi-boot file, we don't get the CPR property 1875-- and these functions allocate a tremendous amount of rubbish. 1876-- It's not critical (because typeSize is really only used in 1877-- debug mode, but I tripped over an example (T5642) in which 1878-- typeSize was one of the biggest single allocators in all of GHC. 1879-- And it's easy to fix, so I did. 1880 1881-- NB: typeSize does not respect `eqType`, in that two types that 1882-- are `eqType` may return different sizes. This is OK, because this 1883-- function is used only in reporting, not decision-making. 1884 1885typeSize :: Type -> Int 1886typeSize (LitTy {}) = 1 1887typeSize (TyVarTy {}) = 1 1888typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2 1889typeSize (FunTy _ _ t1 t2) = typeSize t1 + typeSize t2 1890typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t 1891typeSize (TyConApp _ ts) = 1 + sum (map typeSize ts) 1892typeSize (CastTy ty co) = typeSize ty + coercionSize co 1893typeSize (CoercionTy co) = coercionSize co 1894 1895coercionSize :: Coercion -> Int 1896coercionSize (Refl ty) = typeSize ty 1897coercionSize (GRefl _ ty MRefl) = typeSize ty 1898coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co 1899coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args) 1900coercionSize (AppCo co arg) = coercionSize co + coercionSize arg 1901coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h 1902coercionSize (FunCo _ w co1 co2) = 1 + coercionSize co1 + coercionSize co2 1903 + coercionSize w 1904coercionSize (CoVarCo _) = 1 1905coercionSize (HoleCo _) = 1 1906coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args) 1907coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2 1908coercionSize (SymCo co) = 1 + coercionSize co 1909coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2 1910coercionSize (NthCo _ _ co) = 1 + coercionSize co 1911coercionSize (LRCo _ co) = 1 + coercionSize co 1912coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg 1913coercionSize (KindCo co) = 1 + coercionSize co 1914coercionSize (SubCo co) = 1 + coercionSize co 1915coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs) 1916 1917provSize :: UnivCoProvenance -> Int 1918provSize (PhantomProv co) = 1 + coercionSize co 1919provSize (ProofIrrelProv co) = 1 + coercionSize co 1920provSize (PluginProv _) = 1 1921provSize CorePrepProv = 1 1922 1923{- 1924************************************************************************ 1925* * 1926 Multiplicities 1927* * 1928************************************************************************ 1929 1930These definitions are here to avoid module loops, and to keep 1931GHC.Core.Multiplicity above this module. 1932 1933-} 1934 1935-- | A shorthand for data with an attached 'Mult' element (the multiplicity). 1936data Scaled a = Scaled !Mult a 1937 deriving (Data.Data) 1938 -- You might think that this would be a natural candidate for 1939 -- Functor, Traversable but Krzysztof says (!3674) "it was too easy 1940 -- to accidentally lift functions (substitutions, zonking etc.) from 1941 -- Type -> Type to Scaled Type -> Scaled Type, ignoring 1942 -- multiplicities and causing bugs". So we don't. 1943 -- 1944 -- Being strict in a is worse for performance, so we are only strict on the 1945 -- Mult part of scaled. 1946 1947 1948instance (Outputable a) => Outputable (Scaled a) where 1949 ppr (Scaled _cnt t) = ppr t 1950 -- Do not print the multiplicity here because it tends to be too verbose 1951 1952scaledMult :: Scaled a -> Mult 1953scaledMult (Scaled m _) = m 1954 1955scaledThing :: Scaled a -> a 1956scaledThing (Scaled _ t) = t 1957 1958-- | Apply a function to both the Mult and the Type in a 'Scaled Type' 1959mapScaledType :: (Type -> Type) -> Scaled Type -> Scaled Type 1960mapScaledType f (Scaled m t) = Scaled (f m) (f t) 1961 1962{- | 1963Mult is a type alias for Type. 1964 1965Mult must contain Type because multiplicity variables are mere type variables 1966(of kind Multiplicity) in Haskell. So the simplest implementation is to make 1967Mult be Type. 1968 1969Multiplicities can be formed with: 1970- One: GHC.Types.One (= oneDataCon) 1971- Many: GHC.Types.Many (= manyDataCon) 1972- Multiplication: GHC.Types.MultMul (= multMulTyCon) 1973 1974So that Mult feels a bit more structured, we provide pattern synonyms and smart 1975constructors for these. 1976-} 1977type Mult = Type 1978