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