1-- (c) The University of Glasgow 2006 2-- (c) The GRASP/AQUA Project, Glasgow University, 1998 3-- 4-- Type - public interface 5 6{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, ViewPatterns, MultiWayIf #-} 7{-# OPTIONS_GHC -fno-warn-orphans #-} 8{-# OPTIONS_GHC -Wno-incomplete-record-updates #-} 9 10-- | Main functions for manipulating types and type-related things 11module GHC.Core.Type ( 12 -- Note some of this is just re-exports from TyCon.. 13 14 -- * Main data types representing Types 15 -- $type_classification 16 17 -- $representation_types 18 Type, ArgFlag(..), AnonArgFlag(..), 19 Specificity(..), 20 KindOrType, PredType, ThetaType, 21 Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder, 22 Mult, Scaled, 23 KnotTied, 24 25 -- ** Constructing and deconstructing types 26 mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe, 27 getCastedTyVar_maybe, tyVarKind, varType, 28 29 mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys, 30 splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe, 31 32 mkFunTy, mkVisFunTy, mkInvisFunTy, 33 mkVisFunTys, 34 mkVisFunTyMany, mkInvisFunTyMany, 35 mkVisFunTysMany, mkInvisFunTysMany, 36 splitFunTy, splitFunTy_maybe, 37 splitFunTys, funResultTy, funArgTy, 38 39 mkTyConApp, mkTyConTy, tYPE, 40 tyConAppTyCon_maybe, tyConAppTyConPicky_maybe, 41 tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs, 42 splitTyConApp_maybe, splitTyConApp, tyConAppArgN, 43 tcSplitTyConApp_maybe, 44 splitListTyConApp_maybe, 45 repSplitTyConApp_maybe, 46 47 mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys, 48 mkSpecForAllTy, mkSpecForAllTys, 49 mkVisForAllTys, mkTyCoInvForAllTy, 50 mkInfForAllTy, mkInfForAllTys, 51 splitForAllTyCoVars, 52 splitForAllReqTVBinders, splitForAllInvisTVBinders, 53 splitForAllTyCoVarBinders, 54 splitForAllTyCoVar_maybe, splitForAllTyCoVar, 55 splitForAllTyVar_maybe, splitForAllCoVar_maybe, 56 splitPiTy_maybe, splitPiTy, splitPiTys, 57 mkTyConBindersPreferAnon, 58 mkPiTy, mkPiTys, 59 piResultTy, piResultTys, 60 applyTysX, dropForAlls, 61 mkFamilyTyConApp, 62 buildSynTyCon, 63 64 mkNumLitTy, isNumLitTy, 65 mkStrLitTy, isStrLitTy, 66 mkCharLitTy, isCharLitTy, 67 isLitTy, 68 69 isPredTy, 70 71 getRuntimeRep_maybe, kindRep_maybe, kindRep, 72 73 mkCastTy, mkCoercionTy, splitCastTy_maybe, 74 75 userTypeError_maybe, pprUserTypeErrorTy, 76 77 coAxNthLHS, 78 stripCoercionTy, 79 80 splitInvisPiTys, splitInvisPiTysN, 81 invisibleTyBndrCount, 82 filterOutInvisibleTypes, filterOutInferredTypes, 83 partitionInvisibleTypes, partitionInvisibles, 84 tyConArgFlags, appTyArgFlags, 85 86 -- ** Analyzing types 87 TyCoMapper(..), mapTyCo, mapTyCoX, 88 TyCoFolder(..), foldTyCo, 89 90 -- (Newtypes) 91 newTyConInstRhs, 92 93 -- ** Binders 94 sameVis, 95 mkTyCoVarBinder, mkTyCoVarBinders, 96 mkTyVarBinder, mkTyVarBinders, 97 tyVarSpecToBinders, 98 mkAnonBinder, 99 isAnonTyCoBinder, 100 binderVar, binderVars, binderType, binderArgFlag, 101 tyCoBinderType, tyCoBinderVar_maybe, 102 tyBinderType, 103 binderRelevantType_maybe, 104 isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, 105 isInvisibleBinder, isNamedBinder, 106 tyConBindersTyCoBinders, 107 108 -- ** Common type constructors 109 funTyCon, unrestrictedFunTyCon, 110 111 -- ** Predicates on types 112 isTyVarTy, isFunTy, isCoercionTy, 113 isCoercionTy_maybe, isForAllTy, 114 isForAllTy_ty, isForAllTy_co, 115 isPiTy, isTauTy, isFamFreeTy, 116 isCoVarType, isAtomicTy, 117 118 isValidJoinPointType, 119 tyConAppNeedsKindSig, 120 121 -- *** Levity and boxity 122 isLiftedType_maybe, 123 isLiftedTypeKind, isUnliftedTypeKind, isBoxedTypeKind, pickyIsLiftedTypeKind, 124 isLiftedRuntimeRep, isUnliftedRuntimeRep, isBoxedRuntimeRep, 125 isLiftedLevity, isUnliftedLevity, 126 isUnliftedType, isBoxedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType, 127 isAlgType, isDataFamilyAppType, 128 isPrimitiveType, isStrictType, 129 isLevityTy, isLevityVar, 130 isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy, 131 dropRuntimeRepArgs, 132 getRuntimeRep, 133 134 -- * Multiplicity 135 136 isMultiplicityTy, isMultiplicityVar, 137 unrestricted, linear, tymult, 138 mkScaled, irrelevantMult, scaledSet, 139 pattern One, pattern Many, 140 isOneDataConTy, isManyDataConTy, 141 isLinearType, 142 143 -- * Main data types representing Kinds 144 Kind, 145 146 -- ** Finding the kind of a type 147 typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly, 148 tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind, 149 tcIsBoxedTypeKind, tcIsRuntimeTypeKind, 150 151 -- ** Common Kind 152 liftedTypeKind, unliftedTypeKind, 153 154 -- * Type free variables 155 tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs, 156 tyCoVarsOfType, tyCoVarsOfTypes, 157 tyCoVarsOfTypeDSet, 158 coVarsOfType, 159 coVarsOfTypes, 160 161 anyFreeVarsOfType, anyFreeVarsOfTypes, 162 noFreeVarsOfType, 163 splitVisVarsOfType, splitVisVarsOfTypes, 164 expandTypeSynonyms, 165 typeSize, occCheckExpand, 166 167 -- ** Closing over kinds 168 closeOverKindsDSet, closeOverKindsList, 169 closeOverKinds, 170 171 -- * Well-scoped lists of variables 172 scopedSort, tyCoVarsOfTypeWellScoped, 173 tyCoVarsOfTypesWellScoped, 174 175 -- * Type comparison 176 eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX, 177 nonDetCmpTypesX, nonDetCmpTc, 178 eqVarBndrs, 179 180 -- * Forcing evaluation of types 181 seqType, seqTypes, 182 183 -- * Other views onto Types 184 coreView, tcView, 185 186 tyConsOfType, 187 188 -- * Main type substitution data types 189 TvSubstEnv, -- Representation widely visible 190 TCvSubst(..), -- Representation visible to a few friends 191 192 -- ** Manipulating type substitutions 193 emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst, 194 195 mkTCvSubst, zipTvSubst, mkTvSubstPrs, 196 zipTCvSubst, 197 notElemTCvSubst, 198 getTvSubstEnv, setTvSubstEnv, 199 zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs, 200 extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet, 201 extendTCvSubst, extendCvSubst, 202 extendTvSubst, extendTvSubstBinderAndInScope, 203 extendTvSubstList, extendTvSubstAndInScope, 204 extendTCvSubstList, 205 extendTvSubstWithClone, 206 extendTCvSubstWithClone, 207 isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv, 208 isEmptyTCvSubst, unionTCvSubst, 209 210 -- ** Performing substitution on types and kinds 211 substTy, substTys, substScaledTy, substScaledTys, substTyWith, substTysWith, substTheta, 212 substTyAddInScope, 213 substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked, 214 substThetaUnchecked, substTyWithUnchecked, 215 substCoUnchecked, substCoWithUnchecked, 216 substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars, 217 substVarBndr, substVarBndrs, 218 substTyCoBndr, 219 cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar, 220 221 -- * Tidying type related things up for printing 222 tidyType, tidyTypes, 223 tidyOpenType, tidyOpenTypes, 224 tidyOpenKind, 225 tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, 226 tidyOpenTyCoVar, tidyOpenTyCoVars, 227 tidyTyCoVarOcc, 228 tidyTopType, 229 tidyKind, 230 tidyTyCoVarBinder, tidyTyCoVarBinders, 231 232 -- * Kinds 233 isConstraintKindCon, 234 classifiesTypeWithValues, 235 isKindLevPoly 236 ) where 237 238#include "GhclibHsVersions.h" 239 240import GHC.Prelude 241 242import GHC.Types.Basic 243 244-- We import the representation and primitive functions from GHC.Core.TyCo.Rep. 245-- Many things are reexported, but not the representation! 246 247import GHC.Core.TyCo.Rep 248import GHC.Core.TyCo.Subst 249import GHC.Core.TyCo.Tidy 250import GHC.Core.TyCo.FVs 251 252-- friends: 253import GHC.Types.Var 254import GHC.Types.Var.Env 255import GHC.Types.Var.Set 256import GHC.Types.Unique.Set 257 258import GHC.Core.TyCon 259import GHC.Builtin.Types.Prim 260import {-# SOURCE #-} GHC.Builtin.Types 261 ( charTy, naturalTy, listTyCon 262 , typeSymbolKind, liftedTypeKind, unliftedTypeKind 263 , liftedRepTyCon, unliftedRepTyCon 264 , constraintKind 265 , unrestrictedFunTyCon 266 , manyDataConTy, oneDataConTy ) 267import GHC.Types.Name( Name ) 268import GHC.Builtin.Names 269import GHC.Core.Coercion.Axiom 270import {-# SOURCE #-} GHC.Core.Coercion 271 ( mkNomReflCo, mkGReflCo, mkReflCo 272 , mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo 273 , mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo 274 , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo 275 , mkKindCo, mkSubCo 276 , decomposePiCos, coercionKind, coercionLKind 277 , coercionRKind, coercionType 278 , isReflexiveCo, seqCo ) 279 280-- others 281import GHC.Utils.Misc 282import GHC.Utils.FV 283import GHC.Utils.Outputable 284import GHC.Utils.Panic 285import GHC.Data.FastString 286import GHC.Data.Pair 287import GHC.Data.List.SetOps 288import GHC.Types.Unique ( nonDetCmpUnique ) 289 290import GHC.Data.Maybe ( orElse, expectJust ) 291import Data.Maybe ( isJust ) 292import Control.Monad ( guard ) 293 294-- $type_classification 295-- #type_classification# 296-- 297-- Types are any, but at least one, of: 298-- 299-- [Boxed] Iff its representation is a pointer to an object on the 300-- GC'd heap. Operationally, heap objects can be entered as 301-- a means of evaluation. 302-- 303-- [Lifted] Iff it has bottom as an element: An instance of a 304-- lifted type might diverge when evaluated. 305-- GHC Haskell's unboxed types are unlifted. 306-- An unboxed, but lifted type is not very useful. 307-- (Example: A byte-represented type, where evaluating 0xff 308-- computes the 12345678th collatz number modulo 0xff.) 309-- Only lifted types may be unified with a type variable. 310-- 311-- [Algebraic] Iff it is a type with one or more constructors, whether 312-- declared with @data@ or @newtype@. 313-- An algebraic type is one that can be deconstructed 314-- with a case expression. There are algebraic types that 315-- are not lifted types, like unlifted data types or 316-- unboxed tuples. 317-- 318-- [Data] Iff it is a type declared with @data@, or a boxed tuple. 319-- There are also /unlifted/ data types. 320-- 321-- [Primitive] Iff it is a built-in type that can't be expressed in Haskell. 322-- 323-- Currently, all primitive types are unlifted, but that's not necessarily 324-- the case: for example, @Int@ could be primitive. 325-- 326-- Some primitive types are unboxed, such as @Int#@, whereas some are boxed 327-- but unlifted (such as @ByteArray#@). The only primitive types that we 328-- classify as algebraic are the unboxed tuples. 329-- 330-- Some examples of type classifications that may make this a bit clearer are: 331-- 332-- @ 333-- Type primitive boxed lifted algebraic 334-- ----------------------------------------------------------------------------- 335-- Int# Yes No No No 336-- ByteArray# Yes Yes No No 337-- (\# a, b \#) Yes No No Yes 338-- (\# a | b \#) Yes No No Yes 339-- ( a, b ) No Yes Yes Yes 340-- [a] No Yes Yes Yes 341-- @ 342 343-- $representation_types 344-- A /source type/ is a type that is a separate type as far as the type checker is 345-- concerned, but which has a more low-level representation as far as Core-to-Core 346-- passes and the rest of the back end is concerned. 347-- 348-- You don't normally have to worry about this, as the utility functions in 349-- this module will automatically convert a source into a representation type 350-- if they are spotted, to the best of its abilities. If you don't want this 351-- to happen, use the equivalent functions from the "TcType" module. 352 353{- 354************************************************************************ 355* * 356 Type representation 357* * 358************************************************************************ 359 360Note [coreView vs tcView] 361~~~~~~~~~~~~~~~~~~~~~~~~~ 362So far as the typechecker is concerned, 'Constraint' and 'TYPE 363LiftedRep' are distinct kinds. 364 365But in Core these two are treated as identical. 366 367We implement this by making 'coreView' convert 'Constraint' to 'TYPE 368LiftedRep' on the fly. The function tcView (used in the type checker) 369does not do this. Accordingly, tcView is used in type-checker-oriented 370functions (including the pure unifier, used in instance resolution), 371while coreView is used during e.g. optimisation passes. 372 373See also #11715, which tracks removing this inconsistency. 374 375The inconsistency actually leads to a potential soundness bug, in that 376Constraint and Type are considered *apart* by the type family engine. 377To wit, we can write 378 379 type family F a 380 type instance F Type = Bool 381 type instance F Constraint = Int 382 383and (because Type ~# Constraint in Core), thus build a coercion between 384Int and Bool. I (Richard E) conjecture that this never happens in practice, 385but it's very uncomfortable. This, essentially, is the root problem 386underneath #11715, which is quite resistant to an easy fix. The best 387idea is to have roles in kind coercions, but that has yet to be implemented. 388See also "A Role for Dependent Types in Haskell", ICFP 2019, which describes 389how roles in kinds might work out. 390 391-} 392 393-- | Gives the typechecker view of a type. This unwraps synonyms but 394-- leaves 'Constraint' alone. c.f. 'coreView', which turns 'Constraint' into 395-- 'Type'. Returns 'Nothing' if no unwrapping happens. 396-- See also Note [coreView vs tcView] 397tcView :: Type -> Maybe Type 398tcView (TyConApp tc tys) 399 | res@(Just _) <- expandSynTyConApp_maybe tc tys 400 = res 401tcView _ = Nothing 402-- See Note [Inlining coreView]. 403{-# INLINE tcView #-} 404 405coreView :: Type -> Maybe Type 406-- ^ This function strips off the /top layer only/ of a type synonym 407-- application (if any) its underlying representation type. 408-- Returns 'Nothing' if there is nothing to look through. 409-- This function considers 'Constraint' to be a synonym of @Type@. 410-- 411-- By being non-recursive and inlined, this case analysis gets efficiently 412-- joined onto the case analysis that the caller is already doing 413coreView ty@(TyConApp tc tys) 414 | res@(Just _) <- expandSynTyConApp_maybe tc tys 415 = res 416 417 -- At the Core level, Constraint = Type 418 -- See Note [coreView vs tcView] 419 | isConstraintKindCon tc 420 = ASSERT2( null tys, ppr ty ) 421 Just liftedTypeKind 422 423coreView _ = Nothing 424-- See Note [Inlining coreView]. 425{-# INLINE coreView #-} 426 427----------------------------------------------- 428 429-- | @expandSynTyConApp_maybe tc tys@ expands the RHS of type synonym @tc@ 430-- instantiated at arguments @tys@, or returns 'Nothing' if @tc@ is not a 431-- synonym. 432expandSynTyConApp_maybe :: TyCon -> [Type] -> Maybe Type 433expandSynTyConApp_maybe tc tys 434 | Just (tvs, rhs) <- synTyConDefn_maybe tc 435 , tys `lengthAtLeast` arity 436 = Just (expand_syn arity tvs rhs tys) 437 | otherwise 438 = Nothing 439 where 440 arity = tyConArity tc 441-- Without this INLINE the call to expandSynTyConApp_maybe in coreView 442-- will result in an avoidable allocation. 443{-# INLINE expandSynTyConApp_maybe #-} 444 445-- | A helper for 'expandSynTyConApp_maybe' to avoid inlining this cold path 446-- into call-sites. 447expand_syn :: Int -- ^ the arity of the synonym 448 -> [TyVar] -- ^ the variables bound by the synonym 449 -> Type -- ^ the RHS of the synonym 450 -> [Type] -- ^ the type arguments the synonym is instantiated at. 451 -> Type 452expand_syn arity tvs rhs tys 453 | tys `lengthExceeds` arity = mkAppTys rhs' (drop arity tys) 454 | otherwise = rhs' 455 where 456 rhs' = substTy (mkTvSubstPrs (tvs `zip` tys)) rhs 457 -- The free vars of 'rhs' should all be bound by 'tenv', so it's 458 -- ok to use 'substTy' here (which is what expandSynTyConApp_maybe does). 459 -- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst. 460 -- Its important to use mkAppTys, rather than (foldl AppTy), 461 -- because the function part might well return a 462 -- partially-applied type constructor; indeed, usually will! 463-- We never want to inline this cold-path. 464{-# INLINE expand_syn #-} 465 466coreFullView :: Type -> Type 467-- ^ Iterates 'coreView' until there is no more to synonym to expand. 468-- See Note [Inlining coreView]. 469coreFullView ty@(TyConApp tc _) 470 | isTypeSynonymTyCon tc || isConstraintKindCon tc = go ty 471 where 472 go ty 473 | Just ty' <- coreView ty = go ty' 474 | otherwise = ty 475 476coreFullView ty = ty 477{-# INLINE coreFullView #-} 478 479{- Note [Inlining coreView] 480~~~~~~~~~~~~~~~~~~~~~~~~~~~ 481It is very common to have a function 482 483 f :: Type -> ... 484 f ty | Just ty' <- coreView ty = f ty' 485 f (TyVarTy ...) = ... 486 f ... = ... 487 488If f is not otherwise recursive, the initial call to coreView 489causes f to become recursive, which kills the possibility of 490inlining. Instead, for non-recursive functions, we prefer to 491use coreFullView, which guarantees to unwrap top-level type 492synonyms. It can be inlined and is efficient and non-allocating 493in its fast path. For this to really be fast, all calls made 494on its fast path must also be inlined, linked back to this Note. 495-} 496 497----------------------------------------------- 498expandTypeSynonyms :: Type -> Type 499-- ^ Expand out all type synonyms. Actually, it'd suffice to expand out 500-- just the ones that discard type variables (e.g. type Funny a = Int) 501-- But we don't know which those are currently, so we just expand all. 502-- 503-- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type, 504-- not in the kinds of any TyCon or TyVar mentioned in the type. 505-- 506-- Keep this synchronized with 'synonymTyConsOfType' 507expandTypeSynonyms ty 508 = go (mkEmptyTCvSubst in_scope) ty 509 where 510 in_scope = mkInScopeSet (tyCoVarsOfType ty) 511 512 go subst (TyConApp tc tys) 513 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys 514 = let subst' = mkTvSubst in_scope (mkVarEnv tenv) 515 -- Make a fresh substitution; rhs has nothing to 516 -- do with anything that has happened so far 517 -- NB: if you make changes here, be sure to build an 518 -- /idempotent/ substitution, even in the nested case 519 -- type T a b = a -> b 520 -- type S x y = T y x 521 -- (#11665) 522 in mkAppTys (go subst' rhs) tys' 523 | otherwise 524 = TyConApp tc expanded_tys 525 where 526 expanded_tys = (map (go subst) tys) 527 528 go _ (LitTy l) = LitTy l 529 go subst (TyVarTy tv) = substTyVar subst tv 530 go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2) 531 go subst ty@(FunTy _ mult arg res) 532 = ty { ft_mult = go subst mult, ft_arg = go subst arg, ft_res = go subst res } 533 go subst (ForAllTy (Bndr tv vis) t) 534 = let (subst', tv') = substVarBndrUsing go subst tv in 535 ForAllTy (Bndr tv' vis) (go subst' t) 536 go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co) 537 go subst (CoercionTy co) = mkCoercionTy (go_co subst co) 538 539 go_mco _ MRefl = MRefl 540 go_mco subst (MCo co) = MCo (go_co subst co) 541 542 go_co subst (Refl ty) 543 = mkNomReflCo (go subst ty) 544 go_co subst (GRefl r ty mco) 545 = mkGReflCo r (go subst ty) (go_mco subst mco) 546 -- NB: coercions are always expanded upon creation 547 go_co subst (TyConAppCo r tc args) 548 = mkTyConAppCo r tc (map (go_co subst) args) 549 go_co subst (AppCo co arg) 550 = mkAppCo (go_co subst co) (go_co subst arg) 551 go_co subst (ForAllCo tv kind_co co) 552 = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in 553 mkForAllCo tv' kind_co' (go_co subst' co) 554 go_co subst (FunCo r w co1 co2) 555 = mkFunCo r (go_co subst w) (go_co subst co1) (go_co subst co2) 556 go_co subst (CoVarCo cv) 557 = substCoVar subst cv 558 go_co subst (AxiomInstCo ax ind args) 559 = mkAxiomInstCo ax ind (map (go_co subst) args) 560 go_co subst (UnivCo p r t1 t2) 561 = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2) 562 go_co subst (SymCo co) 563 = mkSymCo (go_co subst co) 564 go_co subst (TransCo co1 co2) 565 = mkTransCo (go_co subst co1) (go_co subst co2) 566 go_co subst (NthCo r n co) 567 = mkNthCo r n (go_co subst co) 568 go_co subst (LRCo lr co) 569 = mkLRCo lr (go_co subst co) 570 go_co subst (InstCo co arg) 571 = mkInstCo (go_co subst co) (go_co subst arg) 572 go_co subst (KindCo co) 573 = mkKindCo (go_co subst co) 574 go_co subst (SubCo co) 575 = mkSubCo (go_co subst co) 576 go_co subst (AxiomRuleCo ax cs) 577 = AxiomRuleCo ax (map (go_co subst) cs) 578 go_co _ (HoleCo h) 579 = pprPanic "expandTypeSynonyms hit a hole" (ppr h) 580 581 go_prov subst (PhantomProv co) = PhantomProv (go_co subst co) 582 go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co) 583 go_prov _ p@(PluginProv _) = p 584 go_prov _ p@CorePrepProv = p 585 586 -- the "False" and "const" are to accommodate the type of 587 -- substForAllCoBndrUsing, which is general enough to 588 -- handle coercion optimization (which sometimes swaps the 589 -- order of a coercion) 590 go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst 591 592-- | An INLINE helper for function such as 'kindRep_maybe' below. 593-- 594-- @isTyConKeyApp_maybe key ty@ returns @Just tys@ iff 595-- the type @ty = T tys@, where T's unique = key 596isTyConKeyApp_maybe :: Unique -> Type -> Maybe [Type] 597isTyConKeyApp_maybe key ty 598 | TyConApp tc args <- coreFullView ty 599 , tc `hasKey` key 600 = Just args 601 | otherwise 602 = Nothing 603{-# INLINE isTyConKeyApp_maybe #-} 604 605-- | Extract the RuntimeRep classifier of a type from its kind. For example, 606-- @kindRep * = LiftedRep@; Panics if this is not possible. 607-- Treats * and Constraint as the same 608kindRep :: HasDebugCallStack => Kind -> Type 609kindRep k = case kindRep_maybe k of 610 Just r -> r 611 Nothing -> pprPanic "kindRep" (ppr k) 612 613-- | Given a kind (TYPE rr), extract its RuntimeRep classifier rr. 614-- For example, @kindRep_maybe * = Just LiftedRep@ 615-- Returns 'Nothing' if the kind is not of form (TYPE rr) 616-- Treats * and Constraint as the same 617kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type 618kindRep_maybe kind 619 | Just [arg] <- isTyConKeyApp_maybe tYPETyConKey kind = Just arg 620 | otherwise = Nothing 621 622-- | Returns True if the kind classifies types which are allocated on 623-- the GC'd heap and False otherwise. Note that this returns False for 624-- levity-polymorphic kinds, which may be specialized to a kind that 625-- classifies AddrRep or even unboxed kinds. 626isBoxedTypeKind :: Kind -> Bool 627isBoxedTypeKind kind 628 = case kindRep_maybe kind of 629 Just rep -> isBoxedRuntimeRep rep 630 Nothing -> False 631 632-- | This version considers Constraint to be the same as *. Returns True 633-- if the argument is equivalent to Type/Constraint and False otherwise. 634-- See Note [Kind Constraint and kind Type] 635isLiftedTypeKind :: Kind -> Bool 636isLiftedTypeKind kind 637 = case kindRep_maybe kind of 638 Just rep -> isLiftedRuntimeRep rep 639 Nothing -> False 640 641pickyIsLiftedTypeKind :: Kind -> Bool 642-- Checks whether the kind is literally 643-- TYPE LiftedRep 644-- or TYPE ('BoxedRep 'Lifted) 645-- or Type 646-- without expanding type synonyms or anything 647-- Used only when deciding whether to suppress the ":: *" in 648-- (a :: *) when printing kinded type variables 649-- See Note [Suppressing * kinds] in GHC.Core.TyCo.Ppr 650pickyIsLiftedTypeKind kind 651 | TyConApp tc [arg] <- kind 652 , tc `hasKey` tYPETyConKey 653 , TyConApp rr_tc rr_args <- arg = case rr_args of 654 [] -> rr_tc `hasKey` liftedRepTyConKey 655 [rr_arg] 656 | rr_tc `hasKey` boxedRepDataConKey 657 , TyConApp lev [] <- rr_arg 658 , lev `hasKey` liftedDataConKey -> True 659 _ -> False 660 | TyConApp tc [] <- kind 661 , tc `hasKey` liftedTypeKindTyConKey = True 662 | otherwise = False 663 664-- | Returns True if the kind classifies unlifted types (like 'Int#') and False 665-- otherwise. Note that this returns False for levity-polymorphic kinds, which 666-- may be specialized to a kind that classifies unlifted types. 667isUnliftedTypeKind :: Kind -> Bool 668isUnliftedTypeKind kind 669 = case kindRep_maybe kind of 670 Just rep -> isUnliftedRuntimeRep rep 671 Nothing -> False 672 673-- | See 'isBoxedRuntimeRep_maybe'. 674isBoxedRuntimeRep :: Type -> Bool 675isBoxedRuntimeRep rep = isJust (isBoxedRuntimeRep_maybe rep) 676 677-- | `isBoxedRuntimeRep_maybe (rep :: RuntimeRep)` returns `Just lev` if `rep` 678-- expands to `Boxed lev` and returns `Nothing` otherwise. 679-- 680-- Types with this runtime rep are represented by pointers on the GC'd heap. 681isBoxedRuntimeRep_maybe :: Type -> Maybe Type 682isBoxedRuntimeRep_maybe rep 683 | Just [lev] <- isTyConKeyApp_maybe boxedRepDataConKey rep 684 = Just lev 685 | otherwise 686 = Nothing 687 688isLiftedRuntimeRep :: Type -> Bool 689-- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep 690-- False of type variables (a :: RuntimeRep) 691-- and of other reps e.g. (IntRep :: RuntimeRep) 692isLiftedRuntimeRep rep 693 | Just [lev] <- isTyConKeyApp_maybe boxedRepDataConKey rep 694 = isLiftedLevity lev 695 | otherwise 696 = False 697 698isUnliftedRuntimeRep :: Type -> Bool 699-- PRECONDITION: The type has kind RuntimeRep 700-- True of definitely-unlifted RuntimeReps 701-- False of (LiftedRep :: RuntimeRep) 702-- and of variables (a :: RuntimeRep) 703isUnliftedRuntimeRep rep 704 | TyConApp rr_tc args <- coreFullView rep -- NB: args might be non-empty 705 -- e.g. TupleRep [r1, .., rn] 706 , isPromotedDataCon rr_tc = 707 -- NB: args might be non-empty e.g. TupleRep [r1, .., rn] 708 if (rr_tc `hasKey` boxedRepDataConKey) 709 then case args of 710 [lev] -> isUnliftedLevity lev 711 _ -> False 712 else True 713 -- Avoid searching all the unlifted RuntimeRep type cons 714 -- In the RuntimeRep data type, only LiftedRep is lifted 715 -- But be careful of type families (F tys) :: RuntimeRep, 716 -- hence the isPromotedDataCon rr_tc 717isUnliftedRuntimeRep _ = False 718 719-- | An INLINE helper for function such as 'isLiftedRuntimeRep' below. 720isNullaryTyConKeyApp :: Unique -> Type -> Bool 721isNullaryTyConKeyApp key ty 722 | Just args <- isTyConKeyApp_maybe key ty 723 = ASSERT( null args ) True 724 | otherwise 725 = False 726{-# INLINE isNullaryTyConKeyApp #-} 727 728isLiftedLevity :: Type -> Bool 729isLiftedLevity = isNullaryTyConKeyApp liftedDataConKey 730 731isUnliftedLevity :: Type -> Bool 732isUnliftedLevity = isNullaryTyConKeyApp unliftedDataConKey 733 734-- | Is this the type 'Levity'? 735isLevityTy :: Type -> Bool 736isLevityTy = isNullaryTyConKeyApp levityTyConKey 737 738-- | Is this the type 'RuntimeRep'? 739isRuntimeRepTy :: Type -> Bool 740isRuntimeRepTy = isNullaryTyConKeyApp runtimeRepTyConKey 741 742-- | Is a tyvar of type 'RuntimeRep'? 743isRuntimeRepVar :: TyVar -> Bool 744isRuntimeRepVar = isRuntimeRepTy . tyVarKind 745 746-- | Is a tyvar of type 'Levity'? 747isLevityVar :: TyVar -> Bool 748isLevityVar = isLevityTy . tyVarKind 749 750-- | Is this the type 'Multiplicity'? 751isMultiplicityTy :: Type -> Bool 752isMultiplicityTy = isNullaryTyConKeyApp multiplicityTyConKey 753 754-- | Is a tyvar of type 'Multiplicity'? 755isMultiplicityVar :: TyVar -> Bool 756isMultiplicityVar = isMultiplicityTy . tyVarKind 757 758{- ********************************************************************* 759* * 760 mapType 761* * 762************************************************************************ 763 764These functions do a map-like operation over types, performing some operation 765on all variables and binding sites. Primarily used for zonking. 766 767Note [Efficiency for ForAllCo case of mapTyCoX] 768~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 769As noted in Note [Forall coercions] in GHC.Core.TyCo.Rep, a ForAllCo is a bit redundant. 770It stores a TyCoVar and a Coercion, where the kind of the TyCoVar always matches 771the left-hand kind of the coercion. This is convenient lots of the time, but 772not when mapping a function over a coercion. 773 774The problem is that tcm_tybinder will affect the TyCoVar's kind and 775mapCoercion will affect the Coercion, and we hope that the results will be 776the same. Even if they are the same (which should generally happen with 777correct algorithms), then there is an efficiency issue. In particular, 778this problem seems to make what should be a linear algorithm into a potentially 779exponential one. But it's only going to be bad in the case where there's 780lots of foralls in the kinds of other foralls. Like this: 781 782 forall a : (forall b : (forall c : ...). ...). ... 783 784This construction seems unlikely. So we'll do the inefficient, easy way 785for now. 786 787Note [Specialising mappers] 788~~~~~~~~~~~~~~~~~~~~~~~~~~~ 789These INLINE pragmas are indispensable. mapTyCo and mapTyCoX are used 790to implement zonking, and it's vital that they get specialised to the TcM 791monad and the particular mapper in use. 792 793Even specialising to the monad alone made a 20% allocation difference 794in perf/compiler/T5030. 795 796See Note [Specialising foldType] in "GHC.Core.TyCo.Rep" for more details of this 797idiom. 798-} 799 800-- | This describes how a "map" operation over a type/coercion should behave 801data TyCoMapper env m 802 = TyCoMapper 803 { tcm_tyvar :: env -> TyVar -> m Type 804 , tcm_covar :: env -> CoVar -> m Coercion 805 , tcm_hole :: env -> CoercionHole -> m Coercion 806 -- ^ What to do with coercion holes. 807 -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep". 808 809 , tcm_tycobinder :: env -> TyCoVar -> ArgFlag -> m (env, TyCoVar) 810 -- ^ The returned env is used in the extended scope 811 812 , tcm_tycon :: TyCon -> m TyCon 813 -- ^ This is used only for TcTyCons 814 -- a) To zonk TcTyCons 815 -- b) To turn TcTyCons into TyCons. 816 -- See Note [Type checking recursive type and class declarations] 817 -- in "GHC.Tc.TyCl" 818 } 819 820{-# INLINE mapTyCo #-} -- See Note [Specialising mappers] 821mapTyCo :: Monad m => TyCoMapper () m 822 -> ( Type -> m Type 823 , [Type] -> m [Type] 824 , Coercion -> m Coercion 825 , [Coercion] -> m[Coercion]) 826mapTyCo mapper 827 = case mapTyCoX mapper of 828 (go_ty, go_tys, go_co, go_cos) 829 -> (go_ty (), go_tys (), go_co (), go_cos ()) 830 831{-# INLINE mapTyCoX #-} -- See Note [Specialising mappers] 832mapTyCoX :: Monad m => TyCoMapper env m 833 -> ( env -> Type -> m Type 834 , env -> [Type] -> m [Type] 835 , env -> Coercion -> m Coercion 836 , env -> [Coercion] -> m[Coercion]) 837mapTyCoX (TyCoMapper { tcm_tyvar = tyvar 838 , tcm_tycobinder = tycobinder 839 , tcm_tycon = tycon 840 , tcm_covar = covar 841 , tcm_hole = cohole }) 842 = (go_ty, go_tys, go_co, go_cos) 843 where 844 go_tys _ [] = return [] 845 go_tys env (ty:tys) = (:) <$> go_ty env ty <*> go_tys env tys 846 847 go_ty env (TyVarTy tv) = tyvar env tv 848 go_ty env (AppTy t1 t2) = mkAppTy <$> go_ty env t1 <*> go_ty env t2 849 go_ty _ ty@(LitTy {}) = return ty 850 go_ty env (CastTy ty co) = mkCastTy <$> go_ty env ty <*> go_co env co 851 go_ty env (CoercionTy co) = CoercionTy <$> go_co env co 852 853 go_ty env ty@(FunTy _ w arg res) 854 = do { w' <- go_ty env w; arg' <- go_ty env arg; res' <- go_ty env res 855 ; return (ty { ft_mult = w', ft_arg = arg', ft_res = res' }) } 856 857 go_ty env ty@(TyConApp tc tys) 858 | isTcTyCon tc 859 = do { tc' <- tycon tc 860 ; mkTyConApp tc' <$> go_tys env tys } 861 862 -- Not a TcTyCon 863 | null tys -- Avoid allocation in this very 864 = return ty -- common case (E.g. Int, LiftedRep etc) 865 866 | otherwise 867 = mkTyConApp tc <$> go_tys env tys 868 869 go_ty env (ForAllTy (Bndr tv vis) inner) 870 = do { (env', tv') <- tycobinder env tv vis 871 ; inner' <- go_ty env' inner 872 ; return $ ForAllTy (Bndr tv' vis) inner' } 873 874 go_cos _ [] = return [] 875 go_cos env (co:cos) = (:) <$> go_co env co <*> go_cos env cos 876 877 go_mco _ MRefl = return MRefl 878 go_mco env (MCo co) = MCo <$> (go_co env co) 879 880 go_co env (Refl ty) = Refl <$> go_ty env ty 881 go_co env (GRefl r ty mco) = mkGReflCo r <$> go_ty env ty <*> go_mco env mco 882 go_co env (AppCo c1 c2) = mkAppCo <$> go_co env c1 <*> go_co env c2 883 go_co env (FunCo r cw c1 c2) = mkFunCo r <$> go_co env cw <*> go_co env c1 <*> go_co env c2 884 go_co env (CoVarCo cv) = covar env cv 885 go_co env (HoleCo hole) = cohole env hole 886 go_co env (UnivCo p r t1 t2) = mkUnivCo <$> go_prov env p <*> pure r 887 <*> go_ty env t1 <*> go_ty env t2 888 go_co env (SymCo co) = mkSymCo <$> go_co env co 889 go_co env (TransCo c1 c2) = mkTransCo <$> go_co env c1 <*> go_co env c2 890 go_co env (AxiomRuleCo r cos) = AxiomRuleCo r <$> go_cos env cos 891 go_co env (NthCo r i co) = mkNthCo r i <$> go_co env co 892 go_co env (LRCo lr co) = mkLRCo lr <$> go_co env co 893 go_co env (InstCo co arg) = mkInstCo <$> go_co env co <*> go_co env arg 894 go_co env (KindCo co) = mkKindCo <$> go_co env co 895 go_co env (SubCo co) = mkSubCo <$> go_co env co 896 go_co env (AxiomInstCo ax i cos) = mkAxiomInstCo ax i <$> go_cos env cos 897 go_co env co@(TyConAppCo r tc cos) 898 | isTcTyCon tc 899 = do { tc' <- tycon tc 900 ; mkTyConAppCo r tc' <$> go_cos env cos } 901 902 -- Not a TcTyCon 903 | null cos -- Avoid allocation in this very 904 = return co -- common case (E.g. Int, LiftedRep etc) 905 906 | otherwise 907 = mkTyConAppCo r tc <$> go_cos env cos 908 go_co env (ForAllCo tv kind_co co) 909 = do { kind_co' <- go_co env kind_co 910 ; (env', tv') <- tycobinder env tv Inferred 911 ; co' <- go_co env' co 912 ; return $ mkForAllCo tv' kind_co' co' } 913 -- See Note [Efficiency for ForAllCo case of mapTyCoX] 914 915 go_prov env (PhantomProv co) = PhantomProv <$> go_co env co 916 go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co 917 go_prov _ p@(PluginProv _) = return p 918 go_prov _ p@CorePrepProv = return p 919 920 921{- 922************************************************************************ 923* * 924\subsection{Constructor-specific functions} 925* * 926************************************************************************ 927 928 929--------------------------------------------------------------------- 930 TyVarTy 931 ~~~~~~~ 932-} 933 934-- | Attempts to obtain the type variable underlying a 'Type', and panics with the 935-- given message if this is not a type variable type. See also 'getTyVar_maybe' 936getTyVar :: String -> Type -> TyVar 937getTyVar msg ty = case getTyVar_maybe ty of 938 Just tv -> tv 939 Nothing -> panic ("getTyVar: " ++ msg) 940 941isTyVarTy :: Type -> Bool 942isTyVarTy ty = isJust (getTyVar_maybe ty) 943 944-- | Attempts to obtain the type variable underlying a 'Type' 945getTyVar_maybe :: Type -> Maybe TyVar 946getTyVar_maybe = repGetTyVar_maybe . coreFullView 947 948-- | If the type is a tyvar, possibly under a cast, returns it, along 949-- with the coercion. Thus, the co is :: kind tv ~N kind ty 950getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN) 951getCastedTyVar_maybe ty = case coreFullView ty of 952 CastTy (TyVarTy tv) co -> Just (tv, co) 953 TyVarTy tv -> Just (tv, mkReflCo Nominal (tyVarKind tv)) 954 _ -> Nothing 955 956-- | Attempts to obtain the type variable underlying a 'Type', without 957-- any expansion 958repGetTyVar_maybe :: Type -> Maybe TyVar 959repGetTyVar_maybe (TyVarTy tv) = Just tv 960repGetTyVar_maybe _ = Nothing 961 962{- 963--------------------------------------------------------------------- 964 AppTy 965 ~~~~~ 966We need to be pretty careful with AppTy to make sure we obey the 967invariant that a TyConApp is always visibly so. mkAppTy maintains the 968invariant: use it. 969 970Note [Decomposing fat arrow c=>t] 971~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 972Can we unify (a b) with (Eq a => ty)? If we do so, we end up with 973a partial application like ((=>) Eq a) which doesn't make sense in 974source Haskell. In contrast, we *can* unify (a b) with (t1 -> t2). 975Here's an example (#9858) of how you might do it: 976 i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep 977 i p = typeRep p 978 979 j = i (Proxy :: Proxy (Eq Int => Int)) 980The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes, 981but suppose we want that. But then in the call to 'i', we end 982up decomposing (Eq Int => Int), and we definitely don't want that. 983 984This really only applies to the type checker; in Core, '=>' and '->' 985are the same, as are 'Constraint' and '*'. But for now I've put 986the test in repSplitAppTy_maybe, which applies throughout, because 987the other calls to splitAppTy are in GHC.Core.Unify, which is also used by 988the type checker (e.g. when matching type-function equations). 989 990-} 991 992-- | Applies a type to another, as in e.g. @k a@ 993mkAppTy :: Type -> Type -> Type 994 -- See Note [Respecting definitional equality], invariant (EQ1). 995mkAppTy (CastTy fun_ty co) arg_ty 996 | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty] 997 = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co 998 999mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2]) 1000mkAppTy ty1 ty2 = AppTy ty1 ty2 1001 -- Note that the TyConApp could be an 1002 -- under-saturated type synonym. GHC allows that; e.g. 1003 -- type Foo k = k a -> k a 1004 -- type Id x = x 1005 -- foo :: Foo Id -> Foo Id 1006 -- 1007 -- Here Id is partially applied in the type sig for Foo, 1008 -- but once the type synonyms are expanded all is well 1009 -- 1010 -- Moreover in GHC.Tc.Types.tcInferTyApps we build up a type 1011 -- (T t1 t2 t3) one argument at a type, thus forming 1012 -- (T t1), (T t1 t2), etc 1013 1014mkAppTys :: Type -> [Type] -> Type 1015mkAppTys ty1 [] = ty1 1016mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy 1017 -- Why do this? See (EQ1) of 1018 -- Note [Respecting definitional equality] 1019 -- in GHC.Core.TyCo.Rep 1020 = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers 1021 where 1022 (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys 1023 (args_to_cast, leftovers) = splitAtList arg_cos arg_tys 1024 casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos 1025mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2) 1026mkAppTys ty1 tys2 = foldl' AppTy ty1 tys2 1027 1028------------- 1029splitAppTy_maybe :: Type -> Maybe (Type, Type) 1030-- ^ Attempt to take a type application apart, whether it is a 1031-- function, type constructor, or plain type application. Note 1032-- that type family applications are NEVER unsaturated by this! 1033splitAppTy_maybe = repSplitAppTy_maybe . coreFullView 1034 1035------------- 1036repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type) 1037-- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that 1038-- any Core view stuff is already done 1039repSplitAppTy_maybe (FunTy _ w ty1 ty2) 1040 = Just (TyConApp funTyCon [w, rep1, rep2, ty1], ty2) 1041 where 1042 rep1 = getRuntimeRep ty1 1043 rep2 = getRuntimeRep ty2 1044 1045repSplitAppTy_maybe (AppTy ty1 ty2) 1046 = Just (ty1, ty2) 1047 1048repSplitAppTy_maybe (TyConApp tc tys) 1049 | not (mustBeSaturated tc) || tys `lengthExceeds` tyConArity tc 1050 , Just (tys', ty') <- snocView tys 1051 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps! 1052 1053repSplitAppTy_maybe _other = Nothing 1054 1055-- This one doesn't break apart (c => t). 1056-- See Note [Decomposing fat arrow c=>t] 1057-- Defined here to avoid module loops between Unify and TcType. 1058tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type) 1059-- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that 1060-- any coreView stuff is already done. Refuses to look through (c => t) 1061tcRepSplitAppTy_maybe (FunTy { ft_af = af, ft_mult = w, ft_arg = ty1, ft_res = ty2 }) 1062 | InvisArg <- af 1063 = Nothing -- See Note [Decomposing fat arrow c=>t] 1064 | otherwise 1065 = Just (TyConApp funTyCon [w, rep1, rep2, ty1], ty2) 1066 where 1067 rep1 = getRuntimeRep ty1 1068 rep2 = getRuntimeRep ty2 1069 1070tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) 1071tcRepSplitAppTy_maybe (TyConApp tc tys) 1072 | not (mustBeSaturated tc) || tys `lengthExceeds` tyConArity tc 1073 , Just (tys', ty') <- snocView tys 1074 = Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps! 1075tcRepSplitAppTy_maybe _other = Nothing 1076 1077------------- 1078splitAppTy :: Type -> (Type, Type) 1079-- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe', 1080-- and panics if this is not possible 1081splitAppTy ty = case splitAppTy_maybe ty of 1082 Just pr -> pr 1083 Nothing -> panic "splitAppTy" 1084 1085------------- 1086splitAppTys :: Type -> (Type, [Type]) 1087-- ^ Recursively splits a type as far as is possible, leaving a residual 1088-- type being applied to and the type arguments applied to it. Never fails, 1089-- even if that means returning an empty list of type applications. 1090splitAppTys ty = split ty ty [] 1091 where 1092 split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args 1093 split _ (AppTy ty arg) args = split ty ty (arg:args) 1094 split _ (TyConApp tc tc_args) args 1095 = let -- keep type families saturated 1096 n | mustBeSaturated tc = tyConArity tc 1097 | otherwise = 0 1098 (tc_args1, tc_args2) = splitAt n tc_args 1099 in 1100 (TyConApp tc tc_args1, tc_args2 ++ args) 1101 split _ (FunTy _ w ty1 ty2) args 1102 = ASSERT( null args ) 1103 (TyConApp funTyCon [], [w, rep1, rep2, ty1, ty2]) 1104 where 1105 rep1 = getRuntimeRep ty1 1106 rep2 = getRuntimeRep ty2 1107 1108 split orig_ty _ args = (orig_ty, args) 1109 1110-- | Like 'splitAppTys', but doesn't look through type synonyms 1111repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type]) 1112repSplitAppTys ty = split ty [] 1113 where 1114 split (AppTy ty arg) args = split ty (arg:args) 1115 split (TyConApp tc tc_args) args 1116 = let n | mustBeSaturated tc = tyConArity tc 1117 | otherwise = 0 1118 (tc_args1, tc_args2) = splitAt n tc_args 1119 in 1120 (TyConApp tc tc_args1, tc_args2 ++ args) 1121 split (FunTy _ w ty1 ty2) args 1122 = ASSERT( null args ) 1123 (TyConApp funTyCon [], [w, rep1, rep2, ty1, ty2]) 1124 where 1125 rep1 = getRuntimeRep ty1 1126 rep2 = getRuntimeRep ty2 1127 1128 split ty args = (ty, args) 1129 1130{- 1131 LitTy 1132 ~~~~~ 1133-} 1134 1135mkNumLitTy :: Integer -> Type 1136mkNumLitTy n = LitTy (NumTyLit n) 1137 1138-- | Is this a numeric literal. We also look through type synonyms. 1139isNumLitTy :: Type -> Maybe Integer 1140isNumLitTy ty 1141 | LitTy (NumTyLit n) <- coreFullView ty = Just n 1142 | otherwise = Nothing 1143 1144mkStrLitTy :: FastString -> Type 1145mkStrLitTy s = LitTy (StrTyLit s) 1146 1147-- | Is this a symbol literal. We also look through type synonyms. 1148isStrLitTy :: Type -> Maybe FastString 1149isStrLitTy ty 1150 | LitTy (StrTyLit s) <- coreFullView ty = Just s 1151 | otherwise = Nothing 1152 1153mkCharLitTy :: Char -> Type 1154mkCharLitTy c = LitTy (CharTyLit c) 1155 1156-- | Is this a char literal? We also look through type synonyms. 1157isCharLitTy :: Type -> Maybe Char 1158isCharLitTy ty 1159 | LitTy (CharTyLit s) <- coreFullView ty = Just s 1160 | otherwise = Nothing 1161 1162 1163-- | Is this a type literal (symbol, numeric, or char)? 1164isLitTy :: Type -> Maybe TyLit 1165isLitTy ty 1166 | LitTy l <- coreFullView ty = Just l 1167 | otherwise = Nothing 1168 1169-- | Is this type a custom user error? 1170-- If so, give us the kind and the error message. 1171userTypeError_maybe :: Type -> Maybe Type 1172userTypeError_maybe t 1173 = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t 1174 -- There may be more than 2 arguments, if the type error is 1175 -- used as a type constructor (e.g. at kind `Type -> Type`). 1176 1177 ; guard (tyConName tc == errorMessageTypeErrorFamName) 1178 ; return msg } 1179 1180-- | Render a type corresponding to a user type error into a SDoc. 1181pprUserTypeErrorTy :: Type -> SDoc 1182pprUserTypeErrorTy ty = 1183 case splitTyConApp_maybe ty of 1184 1185 -- Text "Something" 1186 Just (tc,[txt]) 1187 | tyConName tc == typeErrorTextDataConName 1188 , Just str <- isStrLitTy txt -> ftext str 1189 1190 -- ShowType t 1191 Just (tc,[_k,t]) 1192 | tyConName tc == typeErrorShowTypeDataConName -> ppr t 1193 1194 -- t1 :<>: t2 1195 Just (tc,[t1,t2]) 1196 | tyConName tc == typeErrorAppendDataConName -> 1197 pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2 1198 1199 -- t1 :$$: t2 1200 Just (tc,[t1,t2]) 1201 | tyConName tc == typeErrorVAppendDataConName -> 1202 pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2 1203 1204 -- An unevaluated type function 1205 _ -> ppr ty 1206 1207 1208 1209 1210{- 1211--------------------------------------------------------------------- 1212 FunTy 1213 ~~~~~ 1214 1215Note [Representation of function types] 1216~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1217 1218Functions (e.g. Int -> Char) can be thought of as being applications 1219of funTyCon (known in Haskell surface syntax as (->)), (note that 1220`RuntimeRep' quantifiers are left inferred) 1221 1222 (->) :: forall {r1 :: RuntimeRep} {r2 :: RuntimeRep} 1223 (a :: TYPE r1) (b :: TYPE r2). 1224 a -> b -> Type 1225 1226However, for efficiency's sake we represent saturated applications of (->) 1227with FunTy. For instance, the type, 1228 1229 (->) r1 r2 a b 1230 1231is equivalent to, 1232 1233 FunTy (Anon a) b 1234 1235Note how the RuntimeReps are implied in the FunTy representation. For this 1236reason we must be careful when reconstructing the TyConApp representation (see, 1237for instance, splitTyConApp_maybe). 1238 1239In the compiler we maintain the invariant that all saturated applications of 1240(->) are represented with FunTy. 1241 1242See #11714. 1243-} 1244 1245splitFunTy :: Type -> (Mult, Type, Type) 1246-- ^ Attempts to extract the multiplicity, argument and result types from a type, 1247-- and panics if that is not possible. See also 'splitFunTy_maybe' 1248splitFunTy = expectJust "splitFunTy" . splitFunTy_maybe 1249 1250{-# INLINE splitFunTy_maybe #-} 1251splitFunTy_maybe :: Type -> Maybe (Mult, Type, Type) 1252-- ^ Attempts to extract the multiplicity, argument and result types from a type 1253splitFunTy_maybe ty 1254 | FunTy _ w arg res <- coreFullView ty = Just (w, arg, res) 1255 | otherwise = Nothing 1256 1257splitFunTys :: Type -> ([Scaled Type], Type) 1258splitFunTys ty = split [] ty ty 1259 where 1260 -- common case first 1261 split args _ (FunTy _ w arg res) = split ((Scaled w arg):args) res res 1262 split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty' 1263 split args orig_ty _ = (reverse args, orig_ty) 1264 1265funResultTy :: Type -> Type 1266-- ^ Extract the function result type and panic if that is not possible 1267funResultTy ty 1268 | FunTy { ft_res = res } <- coreFullView ty = res 1269 | otherwise = pprPanic "funResultTy" (ppr ty) 1270 1271funArgTy :: Type -> Type 1272-- ^ Extract the function argument type and panic if that is not possible 1273funArgTy ty 1274 | FunTy { ft_arg = arg } <- coreFullView ty = arg 1275 | otherwise = pprPanic "funArgTy" (ppr ty) 1276 1277-- ^ Just like 'piResultTys' but for a single argument 1278-- Try not to iterate 'piResultTy', because it's inefficient to substitute 1279-- one variable at a time; instead use 'piResultTys" 1280piResultTy :: HasDebugCallStack => Type -> Type -> Type 1281piResultTy ty arg = case piResultTy_maybe ty arg of 1282 Just res -> res 1283 Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg) 1284 1285piResultTy_maybe :: Type -> Type -> Maybe Type 1286-- We don't need a 'tc' version, because 1287-- this function behaves the same for Type and Constraint 1288piResultTy_maybe ty arg = case coreFullView ty of 1289 FunTy { ft_res = res } -> Just res 1290 1291 ForAllTy (Bndr tv _) res 1292 -> let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $ 1293 tyCoVarsOfTypes [arg,res] 1294 in Just (substTy (extendTCvSubst empty_subst tv arg) res) 1295 1296 _ -> Nothing 1297 1298-- | (piResultTys f_ty [ty1, .., tyn]) gives the type of (f ty1 .. tyn) 1299-- where f :: f_ty 1300-- 'piResultTys' is interesting because: 1301-- 1. 'f_ty' may have more for-alls than there are args 1302-- 2. Less obviously, it may have fewer for-alls 1303-- For case 2. think of: 1304-- piResultTys (forall a.a) [forall b.b, Int] 1305-- This really can happen, but only (I think) in situations involving 1306-- undefined. For example: 1307-- undefined :: forall a. a 1308-- Term: undefined @(forall b. b->b) @Int 1309-- This term should have type (Int -> Int), but notice that 1310-- there are more type args than foralls in 'undefined's type. 1311 1312-- If you edit this function, you may need to update the GHC formalism 1313-- See Note [GHC Formalism] in GHC.Core.Lint 1314 1315-- This is a heavily used function (e.g. from typeKind), 1316-- so we pay attention to efficiency, especially in the special case 1317-- where there are no for-alls so we are just dropping arrows from 1318-- a function type/kind. 1319piResultTys :: HasDebugCallStack => Type -> [Type] -> Type 1320piResultTys ty [] = ty 1321piResultTys ty orig_args@(arg:args) 1322 | FunTy { ft_res = res } <- ty 1323 = piResultTys res args 1324 1325 | ForAllTy (Bndr tv _) res <- ty 1326 = go (extendTCvSubst init_subst tv arg) res args 1327 1328 | Just ty' <- coreView ty 1329 = piResultTys ty' orig_args 1330 1331 | otherwise 1332 = pprPanic "piResultTys1" (ppr ty $$ ppr orig_args) 1333 where 1334 init_subst = mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes (ty:orig_args)) 1335 1336 go :: TCvSubst -> Type -> [Type] -> Type 1337 go subst ty [] = substTyUnchecked subst ty 1338 1339 go subst ty all_args@(arg:args) 1340 | FunTy { ft_res = res } <- ty 1341 = go subst res args 1342 1343 | ForAllTy (Bndr tv _) res <- ty 1344 = go (extendTCvSubst subst tv arg) res args 1345 1346 | Just ty' <- coreView ty 1347 = go subst ty' all_args 1348 1349 | not (isEmptyTCvSubst subst) -- See Note [Care with kind instantiation] 1350 = go init_subst 1351 (substTy subst ty) 1352 all_args 1353 1354 | otherwise 1355 = -- We have not run out of arguments, but the function doesn't 1356 -- have the right kind to apply to them; so panic. 1357 -- Without the explicit isEmptyVarEnv test, an ill-kinded type 1358 -- would give an infinite loop, which is very unhelpful 1359 -- c.f. #15473 1360 pprPanic "piResultTys2" (ppr ty $$ ppr orig_args $$ ppr all_args) 1361 1362applyTysX :: [TyVar] -> Type -> [Type] -> Type 1363-- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys 1364-- Assumes that (/\tvs. body_ty) is closed 1365applyTysX tvs body_ty arg_tys 1366 = ASSERT2( arg_tys `lengthAtLeast` n_tvs, pp_stuff ) 1367 ASSERT2( tyCoVarsOfType body_ty `subVarSet` mkVarSet tvs, pp_stuff ) 1368 mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty) 1369 (drop n_tvs arg_tys) 1370 where 1371 pp_stuff = vcat [ppr tvs, ppr body_ty, ppr arg_tys] 1372 n_tvs = length tvs 1373 1374 1375 1376{- Note [Care with kind instantiation] 1377~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1378Suppose we have 1379 T :: forall k. k 1380and we are finding the kind of 1381 T (forall b. b -> b) * Int 1382Then 1383 T (forall b. b->b) :: k[ k :-> forall b. b->b] 1384 :: forall b. b -> b 1385So 1386 T (forall b. b->b) * :: (b -> b)[ b :-> *] 1387 :: * -> * 1388 1389In other words we must instantiate the forall! 1390 1391Similarly (#15428) 1392 S :: forall k f. k -> f k 1393and we are finding the kind of 1394 S * (* ->) Int Bool 1395We have 1396 S * (* ->) :: (k -> f k)[ k :-> *, f :-> (* ->)] 1397 :: * -> * -> * 1398So again we must instantiate. 1399 1400The same thing happens in GHC.CoreToIface.toIfaceAppArgsX. 1401 1402--------------------------------------------------------------------- 1403 TyConApp 1404 ~~~~~~~~ 1405-} 1406 1407-- splitTyConApp "looks through" synonyms, because they don't 1408-- mean a distinct type, but all other type-constructor applications 1409-- including functions are returned as Just .. 1410 1411-- | Retrieve the tycon heading this type, if there is one. Does /not/ 1412-- look through synonyms. 1413tyConAppTyConPicky_maybe :: Type -> Maybe TyCon 1414tyConAppTyConPicky_maybe (TyConApp tc _) = Just tc 1415tyConAppTyConPicky_maybe (FunTy {}) = Just funTyCon 1416tyConAppTyConPicky_maybe _ = Nothing 1417 1418 1419-- | The same as @fst . splitTyConApp@ 1420{-# INLINE tyConAppTyCon_maybe #-} 1421tyConAppTyCon_maybe :: Type -> Maybe TyCon 1422tyConAppTyCon_maybe ty = case coreFullView ty of 1423 TyConApp tc _ -> Just tc 1424 FunTy {} -> Just funTyCon 1425 _ -> Nothing 1426 1427tyConAppTyCon :: Type -> TyCon 1428tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr ty) 1429 1430-- | The same as @snd . splitTyConApp@ 1431tyConAppArgs_maybe :: Type -> Maybe [Type] 1432tyConAppArgs_maybe ty = case coreFullView ty of 1433 TyConApp _ tys -> Just tys 1434 FunTy _ w arg res 1435 | Just rep1 <- getRuntimeRep_maybe arg 1436 , Just rep2 <- getRuntimeRep_maybe res 1437 -> Just [w, rep1, rep2, arg, res] 1438 _ -> Nothing 1439 1440tyConAppArgs :: Type -> [Type] 1441tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty) 1442 1443tyConAppArgN :: Int -> Type -> Type 1444-- Executing Nth 1445tyConAppArgN n ty 1446 = case tyConAppArgs_maybe ty of 1447 Just tys -> tys `getNth` n 1448 Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty) 1449 1450-- | Attempts to tease a type apart into a type constructor and the application 1451-- of a number of arguments to that constructor. Panics if that is not possible. 1452-- See also 'splitTyConApp_maybe' 1453splitTyConApp :: Type -> (TyCon, [Type]) 1454splitTyConApp ty = case splitTyConApp_maybe ty of 1455 Just stuff -> stuff 1456 Nothing -> pprPanic "splitTyConApp" (ppr ty) 1457 1458-- | Attempts to tease a type apart into a type constructor and the application 1459-- of a number of arguments to that constructor 1460splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) 1461splitTyConApp_maybe = repSplitTyConApp_maybe . coreFullView 1462 1463-- | Split a type constructor application into its type constructor and 1464-- applied types. Note that this may fail in the case of a 'FunTy' with an 1465-- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind 1466-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your 1467-- type before using this function. 1468-- 1469-- This does *not* split types headed with (=>), as that's not a TyCon in the 1470-- type-checker. 1471-- 1472-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'. 1473tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type]) 1474-- Defined here to avoid module loops between Unify and TcType. 1475tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty' 1476tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) 1477tcSplitTyConApp_maybe (FunTy VisArg w arg res) 1478 | Just arg_rep <- getRuntimeRep_maybe arg 1479 , Just res_rep <- getRuntimeRep_maybe res 1480 = Just (funTyCon, [w, arg_rep, res_rep, arg, res]) 1481tcSplitTyConApp_maybe _ = Nothing 1482 1483------------------- 1484repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) 1485-- ^ Like 'splitTyConApp_maybe', but doesn't look through synonyms. This 1486-- assumes the synonyms have already been dealt with. 1487-- 1488-- Moreover, for a FunTy, it only succeeds if the argument types 1489-- have enough info to extract the runtime-rep arguments that 1490-- the funTyCon requires. This will usually be true; 1491-- but may be temporarily false during canonicalization: 1492-- see Note [Decomposing FunTy] in GHC.Tc.Solver.Canonical 1493-- 1494repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) 1495repSplitTyConApp_maybe (FunTy _ w arg res) 1496 | Just arg_rep <- getRuntimeRep_maybe arg 1497 , Just res_rep <- getRuntimeRep_maybe res 1498 = Just (funTyCon, [w, arg_rep, res_rep, arg, res]) 1499repSplitTyConApp_maybe _ = Nothing 1500 1501------------------- 1502-- | Attempts to tease a list type apart and gives the type of the elements if 1503-- successful (looks through type synonyms) 1504splitListTyConApp_maybe :: Type -> Maybe Type 1505splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of 1506 Just (tc,[e]) | tc == listTyCon -> Just e 1507 _other -> Nothing 1508 1509newTyConInstRhs :: TyCon -> [Type] -> Type 1510-- ^ Unwrap one 'layer' of newtype on a type constructor and its 1511-- arguments, using an eta-reduced version of the @newtype@ if possible. 1512-- This requires tys to have at least @newTyConInstArity tycon@ elements. 1513newTyConInstRhs tycon tys 1514 = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs ) 1515 applyTysX tvs rhs tys 1516 where 1517 (tvs, rhs) = newTyConEtadRhs tycon 1518 1519{- 1520--------------------------------------------------------------------- 1521 CastTy 1522 ~~~~~~ 1523A casted type has its *kind* casted into something new. 1524-} 1525 1526splitCastTy_maybe :: Type -> Maybe (Type, Coercion) 1527splitCastTy_maybe ty 1528 | CastTy ty' co <- coreFullView ty = Just (ty', co) 1529 | otherwise = Nothing 1530 1531-- | Make a 'CastTy'. The Coercion must be nominal. Checks the 1532-- Coercion for reflexivity, dropping it if it's reflexive. 1533-- See Note [Respecting definitional equality] in "GHC.Core.TyCo.Rep" 1534mkCastTy :: Type -> Coercion -> Type 1535mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note 1536-- NB: Do the slow check here. This is important to keep the splitXXX 1537-- functions working properly. Otherwise, we may end up with something 1538-- like (((->) |> something_reflexive_but_not_obviously_so) biz baz) 1539-- fails under splitFunTy_maybe. This happened with the cheaper check 1540-- in test dependent/should_compile/dynamic-paper. 1541 1542mkCastTy (CastTy ty co1) co2 1543 -- (EQ3) from the Note 1544 = mkCastTy ty (co1 `mkTransCo` co2) 1545 -- call mkCastTy again for the reflexivity check 1546 1547mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co 1548 -- (EQ4) from the Note 1549 -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep. 1550 | isTyVar tv 1551 , let fvs = tyCoVarsOfCo co 1552 = -- have to make sure that pushing the co in doesn't capture the bound var! 1553 if tv `elemVarSet` fvs 1554 then let empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs) 1555 (subst, tv') = substVarBndr empty_subst tv 1556 in ForAllTy (Bndr tv' vis) (substTy subst inner_ty `mkCastTy` co) 1557 else ForAllTy (Bndr tv vis) (inner_ty `mkCastTy` co) 1558 1559mkCastTy ty co = CastTy ty co 1560 1561tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder] 1562-- Return the tyConBinders in TyCoBinder form 1563tyConBindersTyCoBinders = map to_tyb 1564 where 1565 to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis) 1566 to_tyb (Bndr tv (AnonTCB af)) = Anon af (tymult (varType tv)) 1567 1568-- | Create the plain type constructor type which has been applied to no type arguments at all. 1569mkTyConTy :: TyCon -> Type 1570mkTyConTy tycon = tyConNullaryTy tycon 1571 -- see Note [Sharing nullary TyConApps] in GHC.Core.TyCon 1572 1573-- | A key function: builds a 'TyConApp' or 'FunTy' as appropriate to 1574-- its arguments. Applies its arguments to the constructor from left to right. 1575mkTyConApp :: TyCon -> [Type] -> Type 1576mkTyConApp tycon tys 1577 | null tys 1578 = mkTyConTy tycon 1579 1580 | isFunTyCon tycon 1581 , [w, _rep1,_rep2,ty1,ty2] <- tys 1582 -- The FunTyCon (->) is always a visible one 1583 = FunTy { ft_af = VisArg, ft_mult = w, ft_arg = ty1, ft_res = ty2 } 1584 1585 -- See Note [Prefer Type over TYPE 'LiftedRep]. 1586 | tycon `hasKey` tYPETyConKey 1587 , [rep] <- tys 1588 = tYPE rep 1589 -- The catch-all case 1590 | otherwise 1591 = TyConApp tycon tys 1592 1593{- 1594Note [Prefer Type over TYPE 'LiftedRep] 1595~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1596The Core of nearly any program will have numerous occurrences of 1597@TYPE 'LiftedRep@ (and, equivalently, 'Type') floating about. Concretely, while 1598investigating #17292 we found that these constituting a majority of TyConApp 1599constructors on the heap: 1600 1601``` 1602(From a sample of 100000 TyConApp closures) 16030x45f3523 - 28732 - `Type` 16040x420b840702 - 9629 - generic type constructors 16050x42055b7e46 - 9596 16060x420559b582 - 9511 16070x420bb15a1e - 9509 16080x420b86c6ba - 9501 16090x42055bac1e - 9496 16100x45e68fd - 538 - `TYPE ...` 1611``` 1612 1613Consequently, we try hard to ensure that operations on such types are 1614efficient. Specifically, we strive to 1615 1616 a. Avoid heap allocation of such types 1617 b. Use a small (shallow in the tree-depth sense) representation 1618 for such types 1619 1620Goal (b) is particularly useful as it makes traversals (e.g. free variable 1621traversal, substitution, and comparison) more efficient. 1622Comparison in particular takes special advantage of nullary type synonym 1623applications (e.g. things like @TyConApp typeTyCon []@), Note [Comparing 1624nullary type synonyms] in "GHC.Core.Type". 1625 1626To accomplish these we use a number of tricks: 1627 1628 1. Instead of representing the lifted kind as 1629 @TyConApp tYPETyCon [liftedRepDataCon]@ we rather prefer to 1630 use the 'GHC.Types.Type' type synonym (represented as a nullary TyConApp). 1631 This serves goal (b) since there are no applied type arguments to traverse, 1632 e.g., during comparison. 1633 1634 2. We have a top-level binding to represent `TyConApp GHC.Types.Type []` 1635 (namely 'GHC.Builtin.Types.Prim.liftedTypeKind'), ensuring that we 1636 don't need to allocate such types (goal (a)). 1637 1638 3. We use the sharing mechanism described in Note [Sharing nullary TyConApps] 1639 in GHC.Core.TyCon to ensure that we never need to allocate such 1640 nullary applications (goal (a)). 1641 1642See #17958. 1643-} 1644 1645 1646-- | Given a @RuntimeRep@, applies @TYPE@ to it. 1647-- See Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim. 1648tYPE :: Type -> Type 1649tYPE rr@(TyConApp tc [arg]) 1650 -- See Note [Prefer Type of TYPE 'LiftedRep] 1651 | tc `hasKey` boxedRepDataConKey 1652 , TyConApp tc' [] <- arg 1653 = if | tc' `hasKey` liftedDataConKey -> liftedTypeKind -- TYPE (BoxedRep 'Lifted) 1654 | tc' `hasKey` unliftedDataConKey -> unliftedTypeKind -- TYPE (BoxedRep 'Unlifted) 1655 | otherwise -> TyConApp tYPETyCon [rr] 1656 | tc == liftedRepTyCon -- TYPE LiftedRep 1657 = liftedTypeKind 1658 | tc == unliftedRepTyCon -- TYPE UnliftedRep 1659 = unliftedTypeKind 1660tYPE rr = TyConApp tYPETyCon [rr] 1661 1662 1663{- 1664-------------------------------------------------------------------- 1665 CoercionTy 1666 ~~~~~~~~~~ 1667CoercionTy allows us to inject coercions into types. A CoercionTy 1668should appear only in the right-hand side of an application. 1669-} 1670 1671mkCoercionTy :: Coercion -> Type 1672mkCoercionTy = CoercionTy 1673 1674isCoercionTy :: Type -> Bool 1675isCoercionTy (CoercionTy _) = True 1676isCoercionTy _ = False 1677 1678isCoercionTy_maybe :: Type -> Maybe Coercion 1679isCoercionTy_maybe (CoercionTy co) = Just co 1680isCoercionTy_maybe _ = Nothing 1681 1682stripCoercionTy :: Type -> Coercion 1683stripCoercionTy (CoercionTy co) = co 1684stripCoercionTy ty = pprPanic "stripCoercionTy" (ppr ty) 1685 1686{- 1687--------------------------------------------------------------------- 1688 SynTy 1689 ~~~~~ 1690 1691Notes on type synonyms 1692~~~~~~~~~~~~~~~~~~~~~~ 1693The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try 1694to return type synonyms wherever possible. Thus 1695 1696 type Foo a = a -> a 1697 1698we want 1699 splitFunTys (a -> Foo a) = ([a], Foo a) 1700not ([a], a -> a) 1701 1702The reason is that we then get better (shorter) type signatures in 1703interfaces. Notably this plays a role in tcTySigs in GHC.Tc.Gen.Bind. 1704 1705 1706--------------------------------------------------------------------- 1707 ForAllTy 1708 ~~~~~~~~ 1709-} 1710 1711-- | Make a dependent forall over an 'Inferred' variable 1712mkTyCoInvForAllTy :: TyCoVar -> Type -> Type 1713mkTyCoInvForAllTy tv ty 1714 | isCoVar tv 1715 , not (tv `elemVarSet` tyCoVarsOfType ty) 1716 = mkVisFunTyMany (varType tv) ty 1717 | otherwise 1718 = ForAllTy (Bndr tv Inferred) ty 1719 1720-- | Like 'mkTyCoInvForAllTy', but tv should be a tyvar 1721mkInfForAllTy :: TyVar -> Type -> Type 1722mkInfForAllTy tv ty = ASSERT( isTyVar tv ) 1723 ForAllTy (Bndr tv Inferred) ty 1724 1725-- | Like 'mkForAllTys', but assumes all variables are dependent and 1726-- 'Inferred', a common case 1727mkTyCoInvForAllTys :: [TyCoVar] -> Type -> Type 1728mkTyCoInvForAllTys tvs ty = foldr mkTyCoInvForAllTy ty tvs 1729 1730-- | Like 'mkTyCoInvForAllTys', but tvs should be a list of tyvar 1731mkInfForAllTys :: [TyVar] -> Type -> Type 1732mkInfForAllTys tvs ty = foldr mkInfForAllTy ty tvs 1733 1734-- | Like 'mkForAllTy', but assumes the variable is dependent and 'Specified', 1735-- a common case 1736mkSpecForAllTy :: TyVar -> Type -> Type 1737mkSpecForAllTy tv ty = ASSERT( isTyVar tv ) 1738 -- covar is always Inferred, so input should be tyvar 1739 ForAllTy (Bndr tv Specified) ty 1740 1741-- | Like 'mkForAllTys', but assumes all variables are dependent and 1742-- 'Specified', a common case 1743mkSpecForAllTys :: [TyVar] -> Type -> Type 1744mkSpecForAllTys tvs ty = foldr mkSpecForAllTy ty tvs 1745 1746-- | Like mkForAllTys, but assumes all variables are dependent and visible 1747mkVisForAllTys :: [TyVar] -> Type -> Type 1748mkVisForAllTys tvs = ASSERT( all isTyVar tvs ) 1749 -- covar is always Inferred, so all inputs should be tyvar 1750 mkForAllTys [ Bndr tv Required | tv <- tvs ] 1751 1752-- | Given a list of type-level vars and the free vars of a result kind, 1753-- makes TyCoBinders, preferring anonymous binders 1754-- if the variable is, in fact, not dependent. 1755-- e.g. mkTyConBindersPreferAnon [(k:*),(b:k),(c:k)] (k->k) 1756-- We want (k:*) Named, (b:k) Anon, (c:k) Anon 1757-- 1758-- All non-coercion binders are /visible/. 1759mkTyConBindersPreferAnon :: [TyVar] -- ^ binders 1760 -> TyCoVarSet -- ^ free variables of result 1761 -> [TyConBinder] 1762mkTyConBindersPreferAnon vars inner_tkvs = ASSERT( all isTyVar vars) 1763 fst (go vars) 1764 where 1765 go :: [TyVar] -> ([TyConBinder], VarSet) -- also returns the free vars 1766 go [] = ([], inner_tkvs) 1767 go (v:vs) | v `elemVarSet` fvs 1768 = ( Bndr v (NamedTCB Required) : binders 1769 , fvs `delVarSet` v `unionVarSet` kind_vars ) 1770 | otherwise 1771 = ( Bndr v (AnonTCB VisArg) : binders 1772 , fvs `unionVarSet` kind_vars ) 1773 where 1774 (binders, fvs) = go vs 1775 kind_vars = tyCoVarsOfType $ tyVarKind v 1776 1777-- | Take a ForAllTy apart, returning the list of tycovars and the result type. 1778-- This always succeeds, even if it returns only an empty list. Note that the 1779-- result type returned may have free variables that were bound by a forall. 1780splitForAllTyCoVars :: Type -> ([TyCoVar], Type) 1781splitForAllTyCoVars ty = split ty ty [] 1782 where 1783 split _ (ForAllTy (Bndr tv _) ty) tvs = split ty ty (tv:tvs) 1784 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs 1785 split orig_ty _ tvs = (reverse tvs, orig_ty) 1786 1787-- | Splits the longest initial sequence of 'ForAllTy's that satisfy 1788-- @argf_pred@, returning the binders transformed by @argf_pred@ 1789splitSomeForAllTyCoVarBndrs :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type) 1790splitSomeForAllTyCoVarBndrs argf_pred ty = split ty ty [] 1791 where 1792 split _ (ForAllTy (Bndr tcv argf) ty) tvs 1793 | Just argf' <- argf_pred argf = split ty ty (Bndr tcv argf' : tvs) 1794 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs 1795 split orig_ty _ tvs = (reverse tvs, orig_ty) 1796 1797-- | Like 'splitForAllTyCoVars', but only splits 'ForAllTy's with 'Required' type 1798-- variable binders. Furthermore, each returned tyvar is annotated with '()'. 1799splitForAllReqTVBinders :: Type -> ([ReqTVBinder], Type) 1800splitForAllReqTVBinders ty = splitSomeForAllTyCoVarBndrs argf_pred ty 1801 where 1802 argf_pred :: ArgFlag -> Maybe () 1803 argf_pred Required = Just () 1804 argf_pred (Invisible {}) = Nothing 1805 1806-- | Like 'splitForAllTyCoVars', but only splits 'ForAllTy's with 'Invisible' type 1807-- variable binders. Furthermore, each returned tyvar is annotated with its 1808-- 'Specificity'. 1809splitForAllInvisTVBinders :: Type -> ([InvisTVBinder], Type) 1810splitForAllInvisTVBinders ty = splitSomeForAllTyCoVarBndrs argf_pred ty 1811 where 1812 argf_pred :: ArgFlag -> Maybe Specificity 1813 argf_pred Required = Nothing 1814 argf_pred (Invisible spec) = Just spec 1815 1816-- | Like 'splitForAllTyCoVars', but split only for tyvars. 1817-- This always succeeds, even if it returns only an empty list. Note that the 1818-- result type returned may have free variables that were bound by a forall. 1819splitForAllTyVars :: Type -> ([TyVar], Type) 1820splitForAllTyVars ty = split ty ty [] 1821 where 1822 split _ (ForAllTy (Bndr tv _) ty) tvs | isTyVar tv = split ty ty (tv:tvs) 1823 split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs 1824 split orig_ty _ tvs = (reverse tvs, orig_ty) 1825 1826-- | Checks whether this is a proper forall (with a named binder) 1827isForAllTy :: Type -> Bool 1828isForAllTy ty 1829 | ForAllTy {} <- coreFullView ty = True 1830 | otherwise = False 1831 1832-- | Like `isForAllTy`, but returns True only if it is a tyvar binder 1833isForAllTy_ty :: Type -> Bool 1834isForAllTy_ty ty 1835 | ForAllTy (Bndr tv _) _ <- coreFullView ty 1836 , isTyVar tv 1837 = True 1838 1839 | otherwise = False 1840 1841-- | Like `isForAllTy`, but returns True only if it is a covar binder 1842isForAllTy_co :: Type -> Bool 1843isForAllTy_co ty 1844 | ForAllTy (Bndr tv _) _ <- coreFullView ty 1845 , isCoVar tv 1846 = True 1847 1848 | otherwise = False 1849 1850-- | Is this a function or forall? 1851isPiTy :: Type -> Bool 1852isPiTy ty = case coreFullView ty of 1853 ForAllTy {} -> True 1854 FunTy {} -> True 1855 _ -> False 1856 1857-- | Is this a function? 1858isFunTy :: Type -> Bool 1859isFunTy ty 1860 | FunTy {} <- coreFullView ty = True 1861 | otherwise = False 1862 1863-- | Take a forall type apart, or panics if that is not possible. 1864splitForAllTyCoVar :: Type -> (TyCoVar, Type) 1865splitForAllTyCoVar ty 1866 | Just answer <- splitForAllTyCoVar_maybe ty = answer 1867 | otherwise = pprPanic "splitForAllTyCoVar" (ppr ty) 1868 1869-- | Drops all ForAllTys 1870dropForAlls :: Type -> Type 1871dropForAlls ty = go ty 1872 where 1873 go (ForAllTy _ res) = go res 1874 go ty | Just ty' <- coreView ty = go ty' 1875 go res = res 1876 1877-- | Attempts to take a forall type apart, but only if it's a proper forall, 1878-- with a named binder 1879splitForAllTyCoVar_maybe :: Type -> Maybe (TyCoVar, Type) 1880splitForAllTyCoVar_maybe ty 1881 | ForAllTy (Bndr tv _) inner_ty <- coreFullView ty = Just (tv, inner_ty) 1882 | otherwise = Nothing 1883 1884-- | Like 'splitForAllTyCoVar_maybe', but only returns Just if it is a tyvar binder. 1885splitForAllTyVar_maybe :: Type -> Maybe (TyCoVar, Type) 1886splitForAllTyVar_maybe ty 1887 | ForAllTy (Bndr tv _) inner_ty <- coreFullView ty 1888 , isTyVar tv 1889 = Just (tv, inner_ty) 1890 1891 | otherwise = Nothing 1892 1893-- | Like 'splitForAllTyCoVar_maybe', but only returns Just if it is a covar binder. 1894splitForAllCoVar_maybe :: Type -> Maybe (TyCoVar, Type) 1895splitForAllCoVar_maybe ty 1896 | ForAllTy (Bndr tv _) inner_ty <- coreFullView ty 1897 , isCoVar tv 1898 = Just (tv, inner_ty) 1899 1900 | otherwise = Nothing 1901 1902-- | Attempts to take a forall type apart; works with proper foralls and 1903-- functions 1904{-# INLINE splitPiTy_maybe #-} -- callers will immediately deconstruct 1905splitPiTy_maybe :: Type -> Maybe (TyCoBinder, Type) 1906splitPiTy_maybe ty = case coreFullView ty of 1907 ForAllTy bndr ty -> Just (Named bndr, ty) 1908 FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res} 1909 -> Just (Anon af (mkScaled w arg), res) 1910 _ -> Nothing 1911 1912-- | Takes a forall type apart, or panics 1913splitPiTy :: Type -> (TyCoBinder, Type) 1914splitPiTy ty 1915 | Just answer <- splitPiTy_maybe ty = answer 1916 | otherwise = pprPanic "splitPiTy" (ppr ty) 1917 1918-- | Split off all TyCoBinders to a type, splitting both proper foralls 1919-- and functions 1920splitPiTys :: Type -> ([TyCoBinder], Type) 1921splitPiTys ty = split ty ty [] 1922 where 1923 split _ (ForAllTy b res) bs = split res res (Named b : bs) 1924 split _ (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) bs 1925 = split res res (Anon af (Scaled w arg) : bs) 1926 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs 1927 split orig_ty _ bs = (reverse bs, orig_ty) 1928 1929-- | Like 'splitPiTys' but split off only /named/ binders 1930-- and returns 'TyCoVarBinder's rather than 'TyCoBinder's 1931splitForAllTyCoVarBinders :: Type -> ([TyCoVarBinder], Type) 1932splitForAllTyCoVarBinders ty = split ty ty [] 1933 where 1934 split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs 1935 split _ (ForAllTy b res) bs = split res res (b:bs) 1936 split orig_ty _ bs = (reverse bs, orig_ty) 1937{-# INLINE splitForAllTyCoVarBinders #-} 1938 1939invisibleTyBndrCount :: Type -> Int 1940-- Returns the number of leading invisible forall'd binders in the type 1941-- Includes invisible predicate arguments; e.g. for 1942-- e.g. forall {k}. (k ~ *) => k -> k 1943-- returns 2 not 1 1944invisibleTyBndrCount ty = length (fst (splitInvisPiTys ty)) 1945 1946-- | Like 'splitPiTys', but returns only *invisible* binders, including constraints. 1947-- Stops at the first visible binder. 1948splitInvisPiTys :: Type -> ([TyCoBinder], Type) 1949splitInvisPiTys ty = split ty ty [] 1950 where 1951 split _ (ForAllTy b res) bs 1952 | Bndr _ vis <- b 1953 , isInvisibleArgFlag vis = split res res (Named b : bs) 1954 split _ (FunTy { ft_af = InvisArg, ft_mult = mult, ft_arg = arg, ft_res = res }) bs 1955 = split res res (Anon InvisArg (mkScaled mult arg) : bs) 1956 split orig_ty ty bs 1957 | Just ty' <- coreView ty = split orig_ty ty' bs 1958 split orig_ty _ bs = (reverse bs, orig_ty) 1959 1960splitInvisPiTysN :: Int -> Type -> ([TyCoBinder], Type) 1961-- ^ Same as 'splitInvisPiTys', but stop when 1962-- - you have found @n@ 'TyCoBinder's, 1963-- - or you run out of invisible binders 1964splitInvisPiTysN n ty = split n ty ty [] 1965 where 1966 split n orig_ty ty bs 1967 | n == 0 = (reverse bs, orig_ty) 1968 | Just ty' <- coreView ty = split n orig_ty ty' bs 1969 | ForAllTy b res <- ty 1970 , Bndr _ vis <- b 1971 , isInvisibleArgFlag vis = split (n-1) res res (Named b : bs) 1972 | FunTy { ft_af = InvisArg, ft_mult = mult, ft_arg = arg, ft_res = res } <- ty 1973 = split (n-1) res res (Anon InvisArg (Scaled mult arg) : bs) 1974 | otherwise = (reverse bs, orig_ty) 1975 1976-- | Given a 'TyCon' and a list of argument types, filter out any invisible 1977-- (i.e., 'Inferred' or 'Specified') arguments. 1978filterOutInvisibleTypes :: TyCon -> [Type] -> [Type] 1979filterOutInvisibleTypes tc tys = snd $ partitionInvisibleTypes tc tys 1980 1981-- | Given a 'TyCon' and a list of argument types, filter out any 'Inferred' 1982-- arguments. 1983filterOutInferredTypes :: TyCon -> [Type] -> [Type] 1984filterOutInferredTypes tc tys = 1985 filterByList (map (/= Inferred) $ tyConArgFlags tc tys) tys 1986 1987-- | Given a 'TyCon' and a list of argument types, partition the arguments 1988-- into: 1989-- 1990-- 1. 'Inferred' or 'Specified' (i.e., invisible) arguments and 1991-- 1992-- 2. 'Required' (i.e., visible) arguments 1993partitionInvisibleTypes :: TyCon -> [Type] -> ([Type], [Type]) 1994partitionInvisibleTypes tc tys = 1995 partitionByList (map isInvisibleArgFlag $ tyConArgFlags tc tys) tys 1996 1997-- | Given a list of things paired with their visibilities, partition the 1998-- things into (invisible things, visible things). 1999partitionInvisibles :: [(a, ArgFlag)] -> ([a], [a]) 2000partitionInvisibles = partitionWith pick_invis 2001 where 2002 pick_invis :: (a, ArgFlag) -> Either a a 2003 pick_invis (thing, vis) | isInvisibleArgFlag vis = Left thing 2004 | otherwise = Right thing 2005 2006-- | Given a 'TyCon' and a list of argument types to which the 'TyCon' is 2007-- applied, determine each argument's visibility 2008-- ('Inferred', 'Specified', or 'Required'). 2009-- 2010-- Wrinkle: consider the following scenario: 2011-- 2012-- > T :: forall k. k -> k 2013-- > tyConArgFlags T [forall m. m -> m -> m, S, R, Q] 2014-- 2015-- After substituting, we get 2016-- 2017-- > T (forall m. m -> m -> m) :: (forall m. m -> m -> m) -> forall n. n -> n -> n 2018-- 2019-- Thus, the first argument is invisible, @S@ is visible, @R@ is invisible again, 2020-- and @Q@ is visible. 2021tyConArgFlags :: TyCon -> [Type] -> [ArgFlag] 2022tyConArgFlags tc = fun_kind_arg_flags (tyConKind tc) 2023 2024-- | Given a 'Type' and a list of argument types to which the 'Type' is 2025-- applied, determine each argument's visibility 2026-- ('Inferred', 'Specified', or 'Required'). 2027-- 2028-- Most of the time, the arguments will be 'Required', but not always. Consider 2029-- @f :: forall a. a -> Type@. In @f Type Bool@, the first argument (@Type@) is 2030-- 'Specified' and the second argument (@Bool@) is 'Required'. It is precisely 2031-- this sort of higher-rank situation in which 'appTyArgFlags' comes in handy, 2032-- since @f Type Bool@ would be represented in Core using 'AppTy's. 2033-- (See also #15792). 2034appTyArgFlags :: Type -> [Type] -> [ArgFlag] 2035appTyArgFlags ty = fun_kind_arg_flags (typeKind ty) 2036 2037-- | Given a function kind and a list of argument types (where each argument's 2038-- kind aligns with the corresponding position in the argument kind), determine 2039-- each argument's visibility ('Inferred', 'Specified', or 'Required'). 2040fun_kind_arg_flags :: Kind -> [Type] -> [ArgFlag] 2041fun_kind_arg_flags = go emptyTCvSubst 2042 where 2043 go subst ki arg_tys 2044 | Just ki' <- coreView ki = go subst ki' arg_tys 2045 go _ _ [] = [] 2046 go subst (ForAllTy (Bndr tv argf) res_ki) (arg_ty:arg_tys) 2047 = argf : go subst' res_ki arg_tys 2048 where 2049 subst' = extendTvSubst subst tv arg_ty 2050 go subst (TyVarTy tv) arg_tys 2051 | Just ki <- lookupTyVar subst tv = go subst ki arg_tys 2052 -- This FunTy case is important to handle kinds with nested foralls, such 2053 -- as this kind (inspired by #16518): 2054 -- 2055 -- forall {k1} k2. k1 -> k2 -> forall k3. k3 -> Type 2056 -- 2057 -- Here, we want to get the following ArgFlags: 2058 -- 2059 -- [Inferred, Specified, Required, Required, Specified, Required] 2060 -- forall {k1}. forall k2. k1 -> k2 -> forall k3. k3 -> Type 2061 go subst (FunTy{ft_af = af, ft_res = res_ki}) (_:arg_tys) 2062 = argf : go subst res_ki arg_tys 2063 where 2064 argf = case af of 2065 VisArg -> Required 2066 InvisArg -> Inferred 2067 go _ _ arg_tys = map (const Required) arg_tys 2068 -- something is ill-kinded. But this can happen 2069 -- when printing errors. Assume everything is Required. 2070 2071-- @isTauTy@ tests if a type has no foralls or (=>) 2072isTauTy :: Type -> Bool 2073isTauTy ty | Just ty' <- coreView ty = isTauTy ty' 2074isTauTy (TyVarTy _) = True 2075isTauTy (LitTy {}) = True 2076isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc 2077isTauTy (AppTy a b) = isTauTy a && isTauTy b 2078isTauTy (FunTy af w a b) = case af of 2079 InvisArg -> False -- e.g., Eq a => b 2080 VisArg -> isTauTy w && isTauTy a && isTauTy b -- e.g., a -> b 2081isTauTy (ForAllTy {}) = False 2082isTauTy (CastTy ty _) = isTauTy ty 2083isTauTy (CoercionTy _) = False -- Not sure about this 2084 2085isAtomicTy :: Type -> Bool 2086-- True if the type is just a single token, and can be printed compactly 2087-- Used when deciding how to lay out type error messages; see the 2088-- call in GHC.Tc.Errors 2089isAtomicTy (TyVarTy {}) = True 2090isAtomicTy (LitTy {}) = True 2091isAtomicTy (TyConApp _ []) = True 2092 2093isAtomicTy ty | isLiftedTypeKind ty = True 2094 -- 'Type' prints compactly as * 2095 -- See GHC.Iface.Type.ppr_kind_type 2096 2097isAtomicTy _ = False 2098 2099{- 2100%************************************************************************ 2101%* * 2102 TyCoBinders 2103%* * 2104%************************************************************************ 2105-} 2106 2107-- | Make an anonymous binder 2108mkAnonBinder :: AnonArgFlag -> Scaled Type -> TyCoBinder 2109mkAnonBinder = Anon 2110 2111-- | Does this binder bind a variable that is /not/ erased? Returns 2112-- 'True' for anonymous binders. 2113isAnonTyCoBinder :: TyCoBinder -> Bool 2114isAnonTyCoBinder (Named {}) = False 2115isAnonTyCoBinder (Anon {}) = True 2116 2117tyCoBinderVar_maybe :: TyCoBinder -> Maybe TyCoVar 2118tyCoBinderVar_maybe (Named tv) = Just $ binderVar tv 2119tyCoBinderVar_maybe _ = Nothing 2120 2121tyCoBinderType :: TyCoBinder -> Type 2122tyCoBinderType (Named tvb) = binderType tvb 2123tyCoBinderType (Anon _ ty) = scaledThing ty 2124 2125tyBinderType :: TyBinder -> Type 2126tyBinderType (Named (Bndr tv _)) 2127 = ASSERT( isTyVar tv ) 2128 tyVarKind tv 2129tyBinderType (Anon _ ty) = scaledThing ty 2130 2131-- | Extract a relevant type, if there is one. 2132binderRelevantType_maybe :: TyCoBinder -> Maybe Type 2133binderRelevantType_maybe (Named {}) = Nothing 2134binderRelevantType_maybe (Anon _ ty) = Just (scaledThing ty) 2135 2136{- 2137************************************************************************ 2138* * 2139\subsection{Type families} 2140* * 2141************************************************************************ 2142-} 2143 2144mkFamilyTyConApp :: TyCon -> [Type] -> Type 2145-- ^ Given a family instance TyCon and its arg types, return the 2146-- corresponding family type. E.g: 2147-- 2148-- > data family T a 2149-- > data instance T (Maybe b) = MkT b 2150-- 2151-- Where the instance tycon is :RTL, so: 2152-- 2153-- > mkFamilyTyConApp :RTL Int = T (Maybe Int) 2154mkFamilyTyConApp tc tys 2155 | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc 2156 , let tvs = tyConTyVars tc 2157 fam_subst = ASSERT2( tvs `equalLength` tys, ppr tc <+> ppr tys ) 2158 zipTvSubst tvs tys 2159 = mkTyConApp fam_tc (substTys fam_subst fam_tys) 2160 | otherwise 2161 = mkTyConApp tc tys 2162 2163-- | Get the type on the LHS of a coercion induced by a type/data 2164-- family instance. 2165coAxNthLHS :: CoAxiom br -> Int -> Type 2166coAxNthLHS ax ind = 2167 mkTyConApp (coAxiomTyCon ax) (coAxBranchLHS (coAxiomNthBranch ax ind)) 2168 2169isFamFreeTy :: Type -> Bool 2170isFamFreeTy ty | Just ty' <- coreView ty = isFamFreeTy ty' 2171isFamFreeTy (TyVarTy _) = True 2172isFamFreeTy (LitTy {}) = True 2173isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc 2174isFamFreeTy (AppTy a b) = isFamFreeTy a && isFamFreeTy b 2175isFamFreeTy (FunTy _ w a b) = isFamFreeTy w && isFamFreeTy a && isFamFreeTy b 2176isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty 2177isFamFreeTy (CastTy ty _) = isFamFreeTy ty 2178isFamFreeTy (CoercionTy _) = False -- Not sure about this 2179 2180-- | Does this type classify a core (unlifted) Coercion? 2181-- At either role nominal or representational 2182-- (t1 ~# t2) or (t1 ~R# t2) 2183-- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep" 2184isCoVarType :: Type -> Bool 2185 -- ToDo: should we check saturation? 2186isCoVarType ty 2187 | Just tc <- tyConAppTyCon_maybe ty 2188 = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey 2189 | otherwise 2190 = False 2191 2192buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind -- ^ /result/ kind 2193 -> [Role] -> KnotTied Type -> TyCon 2194-- This function is here because here is where we have 2195-- isFamFree and isTauTy 2196buildSynTyCon name binders res_kind roles rhs 2197 = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful 2198 where 2199 is_tau = isTauTy rhs 2200 is_fam_free = isFamFreeTy rhs 2201 is_forgetful = any (not . (`elemVarSet` tyCoVarsOfType rhs) . binderVar) binders || 2202 uniqSetAny isForgetfulSynTyCon (tyConsOfType rhs) 2203 -- NB: This is allowed to be conservative, returning True more often 2204 -- than it should. See comments on GHC.Core.TyCon.isForgetfulSynTyCon 2205 2206{- 2207************************************************************************ 2208* * 2209\subsection{Liftedness} 2210* * 2211************************************************************************ 2212-} 2213 2214-- | Returns Just True if this type is surely lifted, Just False 2215-- if it is surely unlifted, Nothing if we can't be sure (i.e., it is 2216-- levity polymorphic), and panics if the kind does not have the shape 2217-- TYPE r. 2218isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool 2219isLiftedType_maybe ty = case coreFullView (getRuntimeRep ty) of 2220 ty' | isLiftedRuntimeRep ty' -> Just True 2221 TyConApp {} -> Just False -- Everything else is unlifted 2222 _ -> Nothing -- levity polymorphic 2223 2224-- | See "Type#type_classification" for what an unlifted type is. 2225-- Panics on levity polymorphic types; See 'mightBeUnliftedType' for 2226-- a more approximate predicate that behaves better in the presence of 2227-- levity polymorphism. 2228isUnliftedType :: HasDebugCallStack => Type -> Bool 2229 -- isUnliftedType returns True for forall'd unlifted types: 2230 -- x :: forall a. Int# 2231 -- I found bindings like these were getting floated to the top level. 2232 -- They are pretty bogus types, mind you. It would be better never to 2233 -- construct them 2234isUnliftedType ty 2235 = not (isLiftedType_maybe ty `orElse` 2236 pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty))) 2237 2238-- | Returns: 2239-- 2240-- * 'False' if the type is /guaranteed/ lifted or 2241-- * 'True' if it is unlifted, OR we aren't sure (e.g. in a levity-polymorphic case) 2242mightBeUnliftedType :: Type -> Bool 2243mightBeUnliftedType ty 2244 = case isLiftedType_maybe ty of 2245 Just is_lifted -> not is_lifted 2246 Nothing -> True 2247 2248-- | See "Type#type_classification" for what a boxed type is. 2249-- Panics on levity polymorphic types; See 'mightBeUnliftedType' for 2250-- a more approximate predicate that behaves better in the presence of 2251-- levity polymorphism. 2252isBoxedType :: Type -> Bool 2253isBoxedType ty = isBoxedRuntimeRep (getRuntimeRep ty) 2254 2255-- | Is this a type of kind RuntimeRep? (e.g. LiftedRep) 2256isRuntimeRepKindedTy :: Type -> Bool 2257isRuntimeRepKindedTy = isRuntimeRepTy . typeKind 2258 2259-- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g. 2260-- dropping 'LiftedRep arguments of unboxed tuple TyCon applications: 2261-- 2262-- dropRuntimeRepArgs [ 'LiftedRep, 'IntRep 2263-- , String, Int# ] == [String, Int#] 2264-- 2265dropRuntimeRepArgs :: [Type] -> [Type] 2266dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy 2267 2268-- | Extract the RuntimeRep classifier of a type. For instance, 2269-- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not 2270-- possible. 2271getRuntimeRep_maybe :: HasDebugCallStack 2272 => Type -> Maybe Type 2273getRuntimeRep_maybe = kindRep_maybe . typeKind 2274 2275-- | Extract the RuntimeRep classifier of a type. For instance, 2276-- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible. 2277getRuntimeRep :: HasDebugCallStack => Type -> Type 2278getRuntimeRep ty 2279 = case getRuntimeRep_maybe ty of 2280 Just r -> r 2281 Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty)) 2282 2283isUnboxedTupleType :: Type -> Bool 2284isUnboxedTupleType ty 2285 = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey 2286 -- NB: Do not use typePrimRep, as that can't tell the difference between 2287 -- unboxed tuples and unboxed sums 2288 2289 2290isUnboxedSumType :: Type -> Bool 2291isUnboxedSumType ty 2292 = tyConAppTyCon (getRuntimeRep ty) `hasKey` sumRepDataConKey 2293 2294-- | See "Type#type_classification" for what an algebraic type is. 2295-- Should only be applied to /types/, as opposed to e.g. partially 2296-- saturated type constructors 2297isAlgType :: Type -> Bool 2298isAlgType ty 2299 = case splitTyConApp_maybe ty of 2300 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc ) 2301 isAlgTyCon tc 2302 _other -> False 2303 2304-- | Check whether a type is a data family type 2305isDataFamilyAppType :: Type -> Bool 2306isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of 2307 Just tc -> isDataFamilyTyCon tc 2308 _ -> False 2309 2310-- | Computes whether an argument (or let right hand side) should 2311-- be computed strictly or lazily, based only on its type. 2312-- Currently, it's just 'isUnliftedType'. Panics on levity-polymorphic types. 2313isStrictType :: HasDebugCallStack => Type -> Bool 2314isStrictType = isUnliftedType 2315 2316isPrimitiveType :: Type -> Bool 2317-- ^ Returns true of types that are opaque to Haskell. 2318isPrimitiveType ty = case splitTyConApp_maybe ty of 2319 Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc ) 2320 isPrimTyCon tc 2321 _ -> False 2322 2323{- 2324************************************************************************ 2325* * 2326\subsection{Join points} 2327* * 2328************************************************************************ 2329-} 2330 2331-- | Determine whether a type could be the type of a join point of given total 2332-- arity, according to the polymorphism rule. A join point cannot be polymorphic 2333-- in its return type, since given 2334-- join j @a @b x y z = e1 in e2, 2335-- the types of e1 and e2 must be the same, and a and b are not in scope for e2. 2336-- (See Note [The polymorphism rule of join points] in "GHC.Core".) Returns False 2337-- also if the type simply doesn't have enough arguments. 2338-- 2339-- Note that we need to know how many arguments (type *and* value) the putative 2340-- join point takes; for instance, if 2341-- j :: forall a. a -> Int 2342-- then j could be a binary join point returning an Int, but it could *not* be a 2343-- unary join point returning a -> Int. 2344-- 2345-- TODO: See Note [Excess polymorphism and join points] 2346isValidJoinPointType :: JoinArity -> Type -> Bool 2347isValidJoinPointType arity ty 2348 = valid_under emptyVarSet arity ty 2349 where 2350 valid_under tvs arity ty 2351 | arity == 0 2352 = tvs `disjointVarSet` tyCoVarsOfType ty 2353 | Just (t, ty') <- splitForAllTyCoVar_maybe ty 2354 = valid_under (tvs `extendVarSet` t) (arity-1) ty' 2355 | Just (_, _, res_ty) <- splitFunTy_maybe ty 2356 = valid_under tvs (arity-1) res_ty 2357 | otherwise 2358 = False 2359 2360{- Note [Excess polymorphism and join points] 2361~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2362In principle, if a function would be a join point except that it fails 2363the polymorphism rule (see Note [The polymorphism rule of join points] in 2364GHC.Core), it can still be made a join point with some effort. This is because 2365all tail calls must return the same type (they return to the same context!), and 2366thus if the return type depends on an argument, that argument must always be the 2367same. 2368 2369For instance, consider: 2370 2371 let f :: forall a. a -> Char -> [a] 2372 f @a x c = ... f @a y 'a' ... 2373 in ... f @Int 1 'b' ... f @Int 2 'c' ... 2374 2375(where the calls are tail calls). `f` fails the polymorphism rule because its 2376return type is [a], where [a] is bound. But since the type argument is always 2377'Int', we can rewrite it as: 2378 2379 let f' :: Int -> Char -> [Int] 2380 f' x c = ... f' y 'a' ... 2381 in ... f' 1 'b' ... f 2 'c' ... 2382 2383and now we can make f' a join point: 2384 2385 join f' :: Int -> Char -> [Int] 2386 f' x c = ... jump f' y 'a' ... 2387 in ... jump f' 1 'b' ... jump f' 2 'c' ... 2388 2389It's not clear that this comes up often, however. TODO: Measure how often and 2390add this analysis if necessary. See #14620. 2391 2392 2393************************************************************************ 2394* * 2395\subsection{Sequencing on types} 2396* * 2397************************************************************************ 2398-} 2399 2400seqType :: Type -> () 2401seqType (LitTy n) = n `seq` () 2402seqType (TyVarTy tv) = tv `seq` () 2403seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2 2404seqType (FunTy _ w t1 t2) = seqType w `seq` seqType t1 `seq` seqType t2 2405seqType (TyConApp tc tys) = tc `seq` seqTypes tys 2406seqType (ForAllTy (Bndr tv _) ty) = seqType (varType tv) `seq` seqType ty 2407seqType (CastTy ty co) = seqType ty `seq` seqCo co 2408seqType (CoercionTy co) = seqCo co 2409 2410seqTypes :: [Type] -> () 2411seqTypes [] = () 2412seqTypes (ty:tys) = seqType ty `seq` seqTypes tys 2413 2414{- 2415************************************************************************ 2416* * 2417 Comparison for types 2418 (We don't use instances so that we know where it happens) 2419* * 2420************************************************************************ 2421 2422Note [Equality on AppTys] 2423~~~~~~~~~~~~~~~~~~~~~~~~~ 2424In our cast-ignoring equality, we want to say that the following two 2425are equal: 2426 2427 (Maybe |> co) (Int |> co') ~? Maybe Int 2428 2429But the left is an AppTy while the right is a TyConApp. The solution is 2430to use repSplitAppTy_maybe to break up the TyConApp into its pieces and 2431then continue. Easy to do, but also easy to forget to do. 2432 2433Note [Comparing nullary type synonyms] 2434~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2435Consider the task of testing equality between two 'Type's of the form 2436 2437 TyConApp tc [] 2438 2439where @tc@ is a type synonym. A naive way to perform this comparison these 2440would first expand the synonym and then compare the resulting expansions. 2441 2442However, this is obviously wasteful and the RHS of @tc@ may be large; it is 2443much better to rather compare the TyCons directly. Consequently, before 2444expanding type synonyms in type comparisons we first look for a nullary 2445TyConApp and simply compare the TyCons if we find one. Of course, if we find 2446that the TyCons are *not* equal then we still need to perform the expansion as 2447their RHSs may still be equal. 2448 2449We perform this optimisation in a number of places: 2450 2451 * GHC.Core.Types.eqType 2452 * GHC.Core.Types.nonDetCmpType 2453 * GHC.Core.Unify.unify_ty 2454 * TcCanonical.can_eq_nc' 2455 * TcUnify.uType 2456 2457This optimisation is especially helpful for the ubiquitous GHC.Types.Type, 2458since GHC prefers to use the type synonym over @TYPE 'LiftedRep@ applications 2459whenever possible. See Note [Prefer Type over TYPE 'LiftedRep] in 2460GHC.Core.TyCo.Rep for details. 2461 2462-} 2463 2464eqType :: Type -> Type -> Bool 2465-- ^ Type equality on source types. Does not look through @newtypes@ or 2466-- 'PredType's, but it does look through type synonyms. 2467-- This first checks that the kinds of the types are equal and then 2468-- checks whether the types are equal, ignoring casts and coercions. 2469-- (The kind check is a recursive call, but since all kinds have type 2470-- @Type@, there is no need to check the types of kinds.) 2471-- See also Note [Non-trivial definitional equality] in "GHC.Core.TyCo.Rep". 2472eqType t1 t2 = isEqual $ nonDetCmpType t1 t2 2473 -- It's OK to use nonDetCmpType here and eqType is deterministic, 2474 -- nonDetCmpType does equality deterministically 2475 2476-- | Compare types with respect to a (presumably) non-empty 'RnEnv2'. 2477eqTypeX :: RnEnv2 -> Type -> Type -> Bool 2478eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX env t1 t2 2479 -- It's OK to use nonDetCmpType here and eqTypeX is deterministic, 2480 -- nonDetCmpTypeX does equality deterministically 2481 2482-- | Type equality on lists of types, looking through type synonyms 2483-- but not newtypes. 2484eqTypes :: [Type] -> [Type] -> Bool 2485eqTypes tys1 tys2 = isEqual $ nonDetCmpTypes tys1 tys2 2486 -- It's OK to use nonDetCmpType here and eqTypes is deterministic, 2487 -- nonDetCmpTypes does equality deterministically 2488 2489eqVarBndrs :: RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2 2490-- Check that the var lists are the same length 2491-- and have matching kinds; if so, extend the RnEnv2 2492-- Returns Nothing if they don't match 2493eqVarBndrs env [] [] 2494 = Just env 2495eqVarBndrs env (tv1:tvs1) (tv2:tvs2) 2496 | eqTypeX env (varType tv1) (varType tv2) 2497 = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2 2498eqVarBndrs _ _ _= Nothing 2499 2500-- Now here comes the real worker 2501 2502{- 2503Note [nonDetCmpType nondeterminism] 2504~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2505nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX 2506uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for 2507ordering leads to nondeterminism. We hit the same problem in the TyVarTy case, 2508comparing type variables is nondeterministic, note the call to nonDetCmpVar in 2509nonDetCmpTypeX. 2510See Note [Unique Determinism] for more details. 2511-} 2512 2513nonDetCmpType :: Type -> Type -> Ordering 2514nonDetCmpType (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 2515 = EQ 2516nonDetCmpType t1 t2 2517 -- we know k1 and k2 have the same kind, because they both have kind *. 2518 = nonDetCmpTypeX rn_env t1 t2 2519 where 2520 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2])) 2521{-# INLINE nonDetCmpType #-} 2522 2523nonDetCmpTypes :: [Type] -> [Type] -> Ordering 2524nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2 2525 where 2526 rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2))) 2527 2528-- | An ordering relation between two 'Type's (known below as @t1 :: k1@ 2529-- and @t2 :: k2@) 2530data TypeOrdering = TLT -- ^ @t1 < t2@ 2531 | TEQ -- ^ @t1 ~ t2@ and there are no casts in either, 2532 -- therefore we can conclude @k1 ~ k2@ 2533 | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so 2534 -- they may differ in kind. 2535 | TGT -- ^ @t1 > t2@ 2536 deriving (Eq, Ord, Enum, Bounded) 2537 2538nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering -- Main workhorse 2539 -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep 2540nonDetCmpTypeX env orig_t1 orig_t2 = 2541 case go env orig_t1 orig_t2 of 2542 -- If there are casts then we also need to do a comparison of the kinds of 2543 -- the types being compared 2544 TEQX -> toOrdering $ go env k1 k2 2545 ty_ordering -> toOrdering ty_ordering 2546 where 2547 k1 = typeKind orig_t1 2548 k2 = typeKind orig_t2 2549 2550 toOrdering :: TypeOrdering -> Ordering 2551 toOrdering TLT = LT 2552 toOrdering TEQ = EQ 2553 toOrdering TEQX = EQ 2554 toOrdering TGT = GT 2555 2556 liftOrdering :: Ordering -> TypeOrdering 2557 liftOrdering LT = TLT 2558 liftOrdering EQ = TEQ 2559 liftOrdering GT = TGT 2560 2561 thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering 2562 thenCmpTy TEQ rel = rel 2563 thenCmpTy TEQX rel = hasCast rel 2564 thenCmpTy rel _ = rel 2565 2566 hasCast :: TypeOrdering -> TypeOrdering 2567 hasCast TEQ = TEQX 2568 hasCast rel = rel 2569 2570 -- Returns both the resulting ordering relation between the two types 2571 -- and whether either contains a cast. 2572 go :: RnEnv2 -> Type -> Type -> TypeOrdering 2573 -- See Note [Comparing nullary type synonyms]. 2574 go _ (TyConApp tc1 []) (TyConApp tc2 []) 2575 | tc1 == tc2 2576 = TEQ 2577 go env t1 t2 2578 | Just t1' <- coreView t1 = go env t1' t2 2579 | Just t2' <- coreView t2 = go env t1 t2' 2580 2581 go env (TyVarTy tv1) (TyVarTy tv2) 2582 = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2 2583 go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2) 2584 = go env (varType tv1) (varType tv2) 2585 `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2 2586 -- See Note [Equality on AppTys] 2587 go env (AppTy s1 t1) ty2 2588 | Just (s2, t2) <- repSplitAppTy_maybe ty2 2589 = go env s1 s2 `thenCmpTy` go env t1 t2 2590 go env ty1 (AppTy s2 t2) 2591 | Just (s1, t1) <- repSplitAppTy_maybe ty1 2592 = go env s1 s2 `thenCmpTy` go env t1 t2 2593 go env (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2) 2594 = go env s1 s2 `thenCmpTy` go env t1 t2 `thenCmpTy` go env w1 w2 2595 -- Comparing multiplicities last because the test is usually true 2596 go env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 2597 = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2 2598 go _ (LitTy l1) (LitTy l2) = liftOrdering (nonDetCmpTyLit l1 l2) 2599 go env (CastTy t1 _) t2 = hasCast $ go env t1 t2 2600 go env t1 (CastTy t2 _) = hasCast $ go env t1 t2 2601 2602 go _ (CoercionTy {}) (CoercionTy {}) = TEQ 2603 2604 -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy 2605 go _ ty1 ty2 2606 = liftOrdering $ (get_rank ty1) `compare` (get_rank ty2) 2607 where get_rank :: Type -> Int 2608 get_rank (CastTy {}) 2609 = pprPanic "nonDetCmpTypeX.get_rank" (ppr [ty1,ty2]) 2610 get_rank (TyVarTy {}) = 0 2611 get_rank (CoercionTy {}) = 1 2612 get_rank (AppTy {}) = 3 2613 get_rank (LitTy {}) = 4 2614 get_rank (TyConApp {}) = 5 2615 get_rank (FunTy {}) = 6 2616 get_rank (ForAllTy {}) = 7 2617 2618 gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering 2619 gos _ [] [] = TEQ 2620 gos _ [] _ = TLT 2621 gos _ _ [] = TGT 2622 gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2 2623 2624------------- 2625nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering 2626nonDetCmpTypesX _ [] [] = EQ 2627nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2 2628 `thenCmp` 2629 nonDetCmpTypesX env tys1 tys2 2630nonDetCmpTypesX _ [] _ = LT 2631nonDetCmpTypesX _ _ [] = GT 2632 2633------------- 2634-- | Compare two 'TyCon's. NB: This should /never/ see 'Constraint' (as 2635-- recognized by Kind.isConstraintKindCon) which is considered a synonym for 2636-- 'Type' in Core. 2637-- See Note [Kind Constraint and kind Type] in "GHC.Core.Type". 2638-- See Note [nonDetCmpType nondeterminism] 2639nonDetCmpTc :: TyCon -> TyCon -> Ordering 2640nonDetCmpTc tc1 tc2 2641 = ASSERT( not (isConstraintKindCon tc1) && not (isConstraintKindCon tc2) ) 2642 u1 `nonDetCmpUnique` u2 2643 where 2644 u1 = tyConUnique tc1 2645 u2 = tyConUnique tc2 2646 2647{- 2648************************************************************************ 2649* * 2650 The kind of a type 2651* * 2652************************************************************************ 2653 2654Note [typeKind vs tcTypeKind] 2655~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2656We have two functions to get the kind of a type 2657 2658 * typeKind ignores the distinction between Constraint and * 2659 * tcTypeKind respects the distinction between Constraint and * 2660 2661tcTypeKind is used by the type inference engine, for which Constraint 2662and * are different; after that we use typeKind. 2663 2664See also Note [coreView vs tcView] 2665 2666Note [Kinding rules for types] 2667~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2668In typeKind we consider Constraint and (TYPE LiftedRep) to be identical. 2669We then have 2670 2671 t1 : TYPE rep1 2672 t2 : TYPE rep2 2673 (FUN) ---------------- 2674 t1 -> t2 : Type 2675 2676 ty : TYPE rep 2677 `a` is not free in rep 2678(FORALL) ----------------------- 2679 forall a. ty : TYPE rep 2680 2681In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct: 2682 2683 t1 : TYPE rep1 2684 t2 : TYPE rep2 2685 (FUN) ---------------- 2686 t1 -> t2 : Type 2687 2688 t1 : Constraint 2689 t2 : TYPE rep 2690 (PRED1) ---------------- 2691 t1 => t2 : Type 2692 2693 t1 : Constraint 2694 t2 : Constraint 2695 (PRED2) --------------------- 2696 t1 => t2 : Constraint 2697 2698 ty : TYPE rep 2699 `a` is not free in rep 2700(FORALL1) ----------------------- 2701 forall a. ty : TYPE rep 2702 2703 ty : Constraint 2704(FORALL2) ------------------------- 2705 forall a. ty : Constraint 2706 2707Note that: 2708* The only way we distinguish '->' from '=>' is by the fact 2709 that the argument is a PredTy. Both are FunTys 2710 2711Note [Phantom type variables in kinds] 2712~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2713Consider 2714 2715 type K (r :: RuntimeRep) = Type -- Note 'r' is unused 2716 data T r :: K r -- T :: forall r -> K r 2717 foo :: forall r. T r 2718 2719The body of the forall in foo's type has kind (K r), and 2720normally it would make no sense to have 2721 forall r. (ty :: K r) 2722because the kind of the forall would escape the binding 2723of 'r'. But in this case it's fine because (K r) exapands 2724to Type, so we explicitly /permit/ the type 2725 forall r. T r 2726 2727To accommodate such a type, in typeKind (forall a.ty) we use 2728occCheckExpand to expand any type synonyms in the kind of 'ty' 2729to eliminate 'a'. See kinding rule (FORALL) in 2730Note [Kinding rules for types] 2731 2732See also 2733 * GHC.Core.Type.occCheckExpand 2734 * GHC.Core.Utils.coreAltsType 2735 * GHC.Tc.Validity.checkEscapingKind 2736all of which grapple with the same problem. 2737 2738See #14939. 2739-} 2740 2741----------------------------- 2742typeKind :: HasDebugCallStack => Type -> Kind 2743-- No need to expand synonyms 2744typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys 2745typeKind (LitTy l) = typeLiteralKind l 2746typeKind (FunTy {}) = liftedTypeKind 2747typeKind (TyVarTy tyvar) = tyVarKind tyvar 2748typeKind (CastTy _ty co) = coercionRKind co 2749typeKind (CoercionTy co) = coercionType co 2750 2751typeKind (AppTy fun arg) 2752 = go fun [arg] 2753 where 2754 -- Accumulate the type arguments, so we can call piResultTys, 2755 -- rather than a succession of calls to piResultTy (which is 2756 -- asymptotically costly as the number of arguments increases) 2757 go (AppTy fun arg) args = go fun (arg:args) 2758 go fun args = piResultTys (typeKind fun) args 2759 2760typeKind ty@(ForAllTy {}) 2761 = case occCheckExpand tvs body_kind of 2762 -- We must make sure tv does not occur in kind 2763 -- As it is already out of scope! 2764 -- See Note [Phantom type variables in kinds] 2765 Just k' -> k' 2766 Nothing -> pprPanic "typeKind" 2767 (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind) 2768 where 2769 (tvs, body) = splitForAllTyVars ty 2770 body_kind = typeKind body 2771 2772--------------------------------------------- 2773-- Utilities to be used in GHC.Core.Unify, 2774-- which uses "tc" functions 2775--------------------------------------------- 2776 2777tcTypeKind :: HasDebugCallStack => Type -> Kind 2778-- No need to expand synonyms 2779tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys 2780tcTypeKind (LitTy l) = typeLiteralKind l 2781tcTypeKind (TyVarTy tyvar) = tyVarKind tyvar 2782tcTypeKind (CastTy _ty co) = coercionRKind co 2783tcTypeKind (CoercionTy co) = coercionType co 2784 2785tcTypeKind (FunTy { ft_af = af, ft_res = res }) 2786 | InvisArg <- af 2787 , tcIsConstraintKind (tcTypeKind res) 2788 = constraintKind -- Eq a => Ord a :: Constraint 2789 | otherwise -- Eq a => a -> a :: TYPE LiftedRep 2790 = liftedTypeKind -- Eq a => Array# Int :: Type LiftedRep (not TYPE PtrRep) 2791 2792tcTypeKind (AppTy fun arg) 2793 = go fun [arg] 2794 where 2795 -- Accumulate the type arguments, so we can call piResultTys, 2796 -- rather than a succession of calls to piResultTy (which is 2797 -- asymptotically costly as the number of arguments increases) 2798 go (AppTy fun arg) args = go fun (arg:args) 2799 go fun args = piResultTys (tcTypeKind fun) args 2800 2801tcTypeKind ty@(ForAllTy {}) 2802 | tcIsConstraintKind body_kind 2803 = constraintKind 2804 2805 | otherwise 2806 = case occCheckExpand tvs body_kind of 2807 -- We must make sure tv does not occur in kind 2808 -- As it is already out of scope! 2809 -- See Note [Phantom type variables in kinds] 2810 Just k' -> k' 2811 Nothing -> pprPanic "tcTypeKind" 2812 (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind) 2813 where 2814 (tvs, body) = splitForAllTyVars ty 2815 body_kind = tcTypeKind body 2816 2817 2818isPredTy :: HasDebugCallStack => Type -> Bool 2819-- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep 2820isPredTy ty = tcIsConstraintKind (tcTypeKind ty) 2821 2822-- tcIsConstraintKind stuff only makes sense in the typechecker 2823-- After that Constraint = Type 2824-- See Note [coreView vs tcView] 2825-- Defined here because it is used in isPredTy and tcRepSplitAppTy_maybe (sigh) 2826tcIsConstraintKind :: Kind -> Bool 2827tcIsConstraintKind ty 2828 | Just (tc, args) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here 2829 , isConstraintKindCon tc 2830 = ASSERT2( null args, ppr ty ) True 2831 2832 | otherwise 2833 = False 2834 2835-- | Like 'kindRep_maybe', but considers 'Constraint' to be distinct 2836-- from 'Type'. For a version that treats them as the same type, see 2837-- 'kindRep_maybe'. 2838tcKindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type 2839tcKindRep_maybe kind 2840 | Just (tc, [arg]) <- tcSplitTyConApp_maybe kind -- Note: tcSplit here 2841 , tc `hasKey` tYPETyConKey = Just arg 2842 | otherwise = Nothing 2843 2844-- | Is this kind equivalent to 'Type'? 2845-- 2846-- This considers 'Constraint' to be distinct from 'Type'. For a version that 2847-- treats them as the same type, see 'isLiftedTypeKind'. 2848tcIsLiftedTypeKind :: Kind -> Bool 2849tcIsLiftedTypeKind kind 2850 = case tcKindRep_maybe kind of 2851 Just rep -> isLiftedRuntimeRep rep 2852 Nothing -> False 2853 2854-- | Is this kind equivalent to @TYPE (BoxedRep l)@ for some @l :: Levity@? 2855-- 2856-- This considers 'Constraint' to be distinct from 'Type'. For a version that 2857-- treats them as the same type, see 'isLiftedTypeKind'. 2858tcIsBoxedTypeKind :: Kind -> Bool 2859tcIsBoxedTypeKind kind 2860 = case tcKindRep_maybe kind of 2861 Just rep -> isBoxedRuntimeRep rep 2862 Nothing -> False 2863 2864-- | Is this kind equivalent to @TYPE r@ (for some unknown r)? 2865-- 2866-- This considers 'Constraint' to be distinct from @*@. 2867tcIsRuntimeTypeKind :: Kind -> Bool 2868tcIsRuntimeTypeKind kind = isJust (tcKindRep_maybe kind) 2869 2870tcReturnsConstraintKind :: Kind -> Bool 2871-- True <=> the Kind ultimately returns a Constraint 2872-- E.g. * -> Constraint 2873-- forall k. k -> Constraint 2874tcReturnsConstraintKind kind 2875 | Just kind' <- tcView kind = tcReturnsConstraintKind kind' 2876tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty 2877tcReturnsConstraintKind (FunTy { ft_res = ty }) = tcReturnsConstraintKind ty 2878tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc 2879tcReturnsConstraintKind _ = False 2880 2881-------------------------- 2882typeLiteralKind :: TyLit -> Kind 2883typeLiteralKind (NumTyLit {}) = naturalTy 2884typeLiteralKind (StrTyLit {}) = typeSymbolKind 2885typeLiteralKind (CharTyLit {}) = charTy 2886 2887-- | Returns True if a type is levity polymorphic. Should be the same 2888-- as (isKindLevPoly . typeKind) but much faster. 2889-- Precondition: The type has kind (TYPE blah) 2890isTypeLevPoly :: Type -> Bool 2891isTypeLevPoly = go 2892 where 2893 go ty@(TyVarTy {}) = check_kind ty 2894 go ty@(AppTy {}) = check_kind ty 2895 go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False 2896 | otherwise = check_kind ty 2897 go (ForAllTy _ ty) = go ty 2898 go (FunTy {}) = False 2899 go (LitTy {}) = False 2900 go ty@(CastTy {}) = check_kind ty 2901 go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty) 2902 2903 check_kind = isKindLevPoly . typeKind 2904 2905-- | Looking past all pi-types, is the end result potentially levity polymorphic? 2906-- Example: True for (forall r (a :: TYPE r). String -> a) 2907-- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type) 2908resultIsLevPoly :: Type -> Bool 2909resultIsLevPoly = isTypeLevPoly . snd . splitPiTys 2910 2911 2912{- ********************************************************************** 2913* * 2914 Occurs check expansion 2915%* * 2916%********************************************************************* -} 2917 2918{- Note [Occurs check expansion] 2919~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2920(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid 2921of occurrences of tv outside type function arguments, if that is 2922possible; otherwise, it returns Nothing. 2923 2924For example, suppose we have 2925 type F a b = [a] 2926Then 2927 occCheckExpand b (F Int b) = Just [Int] 2928but 2929 occCheckExpand a (F a Int) = Nothing 2930 2931We don't promise to do the absolute minimum amount of expanding 2932necessary, but we try not to do expansions we don't need to. We 2933prefer doing inner expansions first. For example, 2934 type F a b = (a, Int, a, [a]) 2935 type G b = Char 2936We have 2937 occCheckExpand b (F (G b)) = Just (F Char) 2938even though we could also expand F to get rid of b. 2939 2940Note [Occurrence checking: look inside kinds] 2941~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2942Suppose we are considering unifying 2943 (alpha :: *) ~ Int -> (beta :: alpha -> alpha) 2944This may be an error (what is that alpha doing inside beta's kind?), 2945but we must not make the mistake of actually unifying or we'll 2946build an infinite data structure. So when looking for occurrences 2947of alpha in the rhs, we must look in the kinds of type variables 2948that occur there. 2949 2950occCheckExpand tries to expand type synonyms to remove 2951unnecessary occurrences of a variable, and thereby get past an 2952occurs-check failure. This is good; but 2953 we can't do it in the /kind/ of a variable /occurrence/ 2954 2955For example #18451 built an infinite type: 2956 type Const a b = a 2957 data SameKind :: k -> k -> Type 2958 type T (k :: Const Type a) = forall (b :: k). SameKind a b 2959 2960We have 2961 b :: k 2962 k :: Const Type a 2963 a :: k (must be same as b) 2964 2965So if we aren't careful, a's kind mentions a, which is bad. 2966And expanding an /occurrence/ of 'a' doesn't help, because the 2967/binding site/ is the master copy and all the occurrences should 2968match it. 2969 2970Here's a related example: 2971 f :: forall a b (c :: Const Type b). Proxy '[a, c] 2972 2973The list means that 'a' gets the same kind as 'c'; but that 2974kind mentions 'b', so the binders are out of order. 2975 2976Bottom line: in occCheckExpand, do not expand inside the kinds 2977of occurrences. See bad_var_occ in occCheckExpand. And 2978see #18451 for more debate. 2979-} 2980 2981occCheckExpand :: [Var] -> Type -> Maybe Type 2982-- See Note [Occurs check expansion] 2983-- We may have needed to do some type synonym unfolding in order to 2984-- get rid of the variable (or forall), so we also return the unfolded 2985-- version of the type, which is guaranteed to be syntactically free 2986-- of the given type variable. If the type is already syntactically 2987-- free of the variable, then the same type is returned. 2988occCheckExpand vs_to_avoid ty 2989 | null vs_to_avoid -- Efficient shortcut 2990 = Just ty -- Can happen, eg. GHC.Core.Utils.mkSingleAltCase 2991 2992 | otherwise 2993 = go (mkVarSet vs_to_avoid, emptyVarEnv) ty 2994 where 2995 go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type 2996 -- The VarSet is the set of variables we are trying to avoid 2997 -- The VarEnv carries mappings necessary 2998 -- because of kind expansion 2999 go (as, env) ty@(TyVarTy tv) 3000 | Just tv' <- lookupVarEnv env tv = return (mkTyVarTy tv') 3001 | bad_var_occ as tv = Nothing 3002 | otherwise = return ty 3003 3004 go _ ty@(LitTy {}) = return ty 3005 go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1 3006 ; ty2' <- go cxt ty2 3007 ; return (mkAppTy ty1' ty2') } 3008 go cxt ty@(FunTy _ w ty1 ty2) 3009 = do { w' <- go cxt w 3010 ; ty1' <- go cxt ty1 3011 ; ty2' <- go cxt ty2 3012 ; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) } 3013 go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty) 3014 = do { ki' <- go cxt (varType tv) 3015 ; let tv' = setVarType tv ki' 3016 env' = extendVarEnv env tv tv' 3017 as' = as `delVarSet` tv 3018 ; body' <- go (as', env') body_ty 3019 ; return (ForAllTy (Bndr tv' vis) body') } 3020 3021 -- For a type constructor application, first try expanding away the 3022 -- offending variable from the arguments. If that doesn't work, next 3023 -- see if the type constructor is a type synonym, and if so, expand 3024 -- it and try again. 3025 go cxt ty@(TyConApp tc tys) 3026 = case mapM (go cxt) tys of 3027 Just tys' -> return (mkTyConApp tc tys') 3028 Nothing | Just ty' <- tcView ty -> go cxt ty' 3029 | otherwise -> Nothing 3030 -- Failing that, try to expand a synonym 3031 3032 go cxt (CastTy ty co) = do { ty' <- go cxt ty 3033 ; co' <- go_co cxt co 3034 ; return (mkCastTy ty' co') } 3035 go cxt (CoercionTy co) = do { co' <- go_co cxt co 3036 ; return (mkCoercionTy co') } 3037 3038 ------------------ 3039 bad_var_occ :: VarSet -> Var -> Bool 3040 -- Works for TyVar and CoVar 3041 -- See Note [Occurrence checking: look inside kinds] 3042 bad_var_occ vs_to_avoid v 3043 = v `elemVarSet` vs_to_avoid 3044 || tyCoVarsOfType (varType v) `intersectsVarSet` vs_to_avoid 3045 3046 ------------------ 3047 go_mco _ MRefl = return MRefl 3048 go_mco ctx (MCo co) = MCo <$> go_co ctx co 3049 3050 ------------------ 3051 go_co cxt (Refl ty) = do { ty' <- go cxt ty 3052 ; return (mkNomReflCo ty') } 3053 go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco 3054 ; ty' <- go cxt ty 3055 ; return (mkGReflCo r ty' mco') } 3056 -- Note: Coercions do not contain type synonyms 3057 go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args 3058 ; return (mkTyConAppCo r tc args') } 3059 go_co cxt (AppCo co arg) = do { co' <- go_co cxt co 3060 ; arg' <- go_co cxt arg 3061 ; return (mkAppCo co' arg') } 3062 go_co cxt@(as, env) (ForAllCo tv kind_co body_co) 3063 = do { kind_co' <- go_co cxt kind_co 3064 ; let tv' = setVarType tv $ 3065 coercionLKind kind_co' 3066 env' = extendVarEnv env tv tv' 3067 as' = as `delVarSet` tv 3068 ; body' <- go_co (as', env') body_co 3069 ; return (ForAllCo tv' kind_co' body') } 3070 go_co cxt (FunCo r w co1 co2) = do { co1' <- go_co cxt co1 3071 ; co2' <- go_co cxt co2 3072 ; w' <- go_co cxt w 3073 ; return (mkFunCo r w' co1' co2') } 3074 go_co (as,env) co@(CoVarCo c) 3075 | Just c' <- lookupVarEnv env c = return (mkCoVarCo c') 3076 | bad_var_occ as c = Nothing 3077 | otherwise = return co 3078 3079 go_co (as,_) co@(HoleCo h) 3080 | bad_var_occ as (ch_co_var h) = Nothing 3081 | otherwise = return co 3082 3083 go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args 3084 ; return (mkAxiomInstCo ax ind args') } 3085 go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p 3086 ; ty1' <- go cxt ty1 3087 ; ty2' <- go cxt ty2 3088 ; return (mkUnivCo p' r ty1' ty2') } 3089 go_co cxt (SymCo co) = do { co' <- go_co cxt co 3090 ; return (mkSymCo co') } 3091 go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1 3092 ; co2' <- go_co cxt co2 3093 ; return (mkTransCo co1' co2') } 3094 go_co cxt (NthCo r n co) = do { co' <- go_co cxt co 3095 ; return (mkNthCo r n co') } 3096 go_co cxt (LRCo lr co) = do { co' <- go_co cxt co 3097 ; return (mkLRCo lr co') } 3098 go_co cxt (InstCo co arg) = do { co' <- go_co cxt co 3099 ; arg' <- go_co cxt arg 3100 ; return (mkInstCo co' arg') } 3101 go_co cxt (KindCo co) = do { co' <- go_co cxt co 3102 ; return (mkKindCo co') } 3103 go_co cxt (SubCo co) = do { co' <- go_co cxt co 3104 ; return (mkSubCo co') } 3105 go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs 3106 ; return (mkAxiomRuleCo ax cs') } 3107 3108 ------------------ 3109 go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co 3110 go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co 3111 go_prov _ p@(PluginProv _) = return p 3112 go_prov _ p@CorePrepProv = return p 3113 3114 3115{- 3116%************************************************************************ 3117%* * 3118 Miscellaneous functions 3119%* * 3120%************************************************************************ 3121 3122-} 3123-- | All type constructors occurring in the type; looking through type 3124-- synonyms, but not newtypes. 3125-- When it finds a Class, it returns the class TyCon. 3126tyConsOfType :: Type -> UniqSet TyCon 3127tyConsOfType ty 3128 = go ty 3129 where 3130 go :: Type -> UniqSet TyCon -- The UniqSet does duplicate elim 3131 go ty | Just ty' <- coreView ty = go ty' 3132 go (TyVarTy {}) = emptyUniqSet 3133 go (LitTy {}) = emptyUniqSet 3134 go (TyConApp tc tys) = go_tc tc `unionUniqSets` go_s tys 3135 go (AppTy a b) = go a `unionUniqSets` go b 3136 go (FunTy _ w a b) = go w `unionUniqSets` 3137 go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon 3138 go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv) 3139 go (CastTy ty co) = go ty `unionUniqSets` go_co co 3140 go (CoercionTy co) = go_co co 3141 3142 go_co (Refl ty) = go ty 3143 go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco 3144 go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args 3145 go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg 3146 go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co 3147 go_co (FunCo _ co_mult co1 co2) = go_co co_mult `unionUniqSets` go_co co1 `unionUniqSets` go_co co2 3148 go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args 3149 go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2 3150 go_co (CoVarCo {}) = emptyUniqSet 3151 go_co (HoleCo {}) = emptyUniqSet 3152 go_co (SymCo co) = go_co co 3153 go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2 3154 go_co (NthCo _ _ co) = go_co co 3155 go_co (LRCo _ co) = go_co co 3156 go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg 3157 go_co (KindCo co) = go_co co 3158 go_co (SubCo co) = go_co co 3159 go_co (AxiomRuleCo _ cs) = go_cos cs 3160 3161 go_mco MRefl = emptyUniqSet 3162 go_mco (MCo co) = go_co co 3163 3164 go_prov (PhantomProv co) = go_co co 3165 go_prov (ProofIrrelProv co) = go_co co 3166 go_prov (PluginProv _) = emptyUniqSet 3167 go_prov CorePrepProv = emptyUniqSet 3168 -- this last case can happen from the tyConsOfType used from 3169 -- checkTauTvUpdate 3170 3171 go_s tys = foldr (unionUniqSets . go) emptyUniqSet tys 3172 go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos 3173 3174 go_tc tc = unitUniqSet tc 3175 go_ax ax = go_tc $ coAxiomTyCon ax 3176 3177-- | Retrieve the free variables in this type, splitting them based 3178-- on whether they are used visibly or invisibly. Invisible ones come 3179-- first. 3180splitVisVarsOfType :: Type -> Pair TyCoVarSet 3181splitVisVarsOfType orig_ty = Pair invis_vars vis_vars 3182 where 3183 Pair invis_vars1 vis_vars = go orig_ty 3184 invis_vars = invis_vars1 `minusVarSet` vis_vars 3185 3186 go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv) 3187 go (AppTy t1 t2) = go t1 `mappend` go t2 3188 go (TyConApp tc tys) = go_tc tc tys 3189 go (FunTy _ w t1 t2) = go w `mappend` go t1 `mappend` go t2 3190 go (ForAllTy (Bndr tv _) ty) 3191 = ((`delVarSet` tv) <$> go ty) `mappend` 3192 (invisible (tyCoVarsOfType $ varType tv)) 3193 go (LitTy {}) = mempty 3194 go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co) 3195 go (CoercionTy co) = invisible $ tyCoVarsOfCo co 3196 3197 invisible vs = Pair vs emptyVarSet 3198 3199 go_tc tc tys = let (invis, vis) = partitionInvisibleTypes tc tys in 3200 invisible (tyCoVarsOfTypes invis) `mappend` foldMap go vis 3201 3202splitVisVarsOfTypes :: [Type] -> Pair TyCoVarSet 3203splitVisVarsOfTypes = foldMap splitVisVarsOfType 3204 3205{- 3206************************************************************************ 3207* * 3208 Functions over Kinds 3209* * 3210************************************************************************ 3211 3212Note [Kind Constraint and kind Type] 3213~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3214The kind Constraint is the kind of classes and other type constraints. 3215The special thing about types of kind Constraint is that 3216 * They are displayed with double arrow: 3217 f :: Ord a => a -> a 3218 * They are implicitly instantiated at call sites; so the type inference 3219 engine inserts an extra argument of type (Ord a) at every call site 3220 to f. 3221 3222However, once type inference is over, there is *no* distinction between 3223Constraint and Type. Indeed we can have coercions between the two. Consider 3224 class C a where 3225 op :: a -> a 3226For this single-method class we may generate a newtype, which in turn 3227generates an axiom witnessing 3228 C a ~ (a -> a) 3229so on the left we have Constraint, and on the right we have Type. 3230See #7451. 3231 3232Because we treat Constraint/Type differently during and after type inference, 3233GHC has two notions of equality that differ in whether they equate 3234Constraint/Type or not: 3235 3236* GHC.Tc.Utils.TcType.tcEqType implements typechecker equality (see 3237 Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType), 3238 which treats Constraint and Type as distinct. This is used during type 3239 inference. See #11715 for issues that arise from this. 3240* GHC.Core.TyCo.Rep.eqType implements definitional equality (see 3241 Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep), which treats 3242 Constraint and Type as equal. This is used after type inference. 3243 3244Bottom line: although 'Type' and 'Constraint' are distinct TyCons, with 3245distinct uniques, they are treated as equal at all times except 3246during type inference. 3247-} 3248 3249-- | Tests whether the given kind (which should look like @TYPE x@) 3250-- is something other than a constructor tree (that is, constructors at every node). 3251-- E.g. True of TYPE k, TYPE (F Int) 3252-- False of TYPE 'LiftedRep 3253isKindLevPoly :: Kind -> Bool 3254isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k ) 3255 -- the isLiftedTypeKind check is necessary b/c of Constraint 3256 go k 3257 where 3258 go ty | Just ty' <- coreView ty = go ty' 3259 go TyVarTy{} = True 3260 go AppTy{} = True -- it can't be a TyConApp 3261 go (TyConApp tc tys) = isFamilyTyCon tc || any go tys 3262 go ForAllTy{} = True 3263 go (FunTy _ w t1 t2) = go w || go t1 || go t2 3264 go LitTy{} = False 3265 go CastTy{} = True 3266 go CoercionTy{} = True 3267 3268 _is_type = classifiesTypeWithValues k 3269 3270----------------------------------------- 3271-- Subkinding 3272-- The tc variants are used during type-checking, where ConstraintKind 3273-- is distinct from all other kinds 3274-- After type-checking (in core), Constraint and liftedTypeKind are 3275-- indistinguishable 3276 3277-- | Does this classify a type allowed to have values? Responds True to things 3278-- like *, #, TYPE Lifted, TYPE v, Constraint. 3279classifiesTypeWithValues :: Kind -> Bool 3280-- ^ True of any sub-kind of OpenTypeKind 3281classifiesTypeWithValues k = isJust (kindRep_maybe k) 3282 3283{- 3284%************************************************************************ 3285%* * 3286 Pretty-printing 3287%* * 3288%************************************************************************ 3289 3290Most pretty-printing is either in GHC.Core.TyCo.Rep or GHC.Iface.Type. 3291 3292-} 3293 3294-- | Does a 'TyCon' (that is applied to some number of arguments) need to be 3295-- ascribed with an explicit kind signature to resolve ambiguity if rendered as 3296-- a source-syntax type? 3297-- (See @Note [When does a tycon application need an explicit kind signature?]@ 3298-- for a full explanation of what this function checks for.) 3299tyConAppNeedsKindSig 3300 :: Bool -- ^ Should specified binders count towards injective positions in 3301 -- the kind of the TyCon? (If you're using visible kind 3302 -- applications, then you want True here. 3303 -> TyCon 3304 -> Int -- ^ The number of args the 'TyCon' is applied to. 3305 -> Bool -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the 3306 -- number of arguments) 3307tyConAppNeedsKindSig spec_inj_pos tc n_args 3308 | LT <- listLengthCmp tc_binders n_args 3309 = False 3310 | otherwise 3311 = let (dropped_binders, remaining_binders) 3312 = splitAt n_args tc_binders 3313 result_kind = mkTyConKind remaining_binders tc_res_kind 3314 result_vars = tyCoVarsOfType result_kind 3315 dropped_vars = fvVarSet $ 3316 mapUnionFV injective_vars_of_binder dropped_binders 3317 3318 in not (subVarSet result_vars dropped_vars) 3319 where 3320 tc_binders = tyConBinders tc 3321 tc_res_kind = tyConResKind tc 3322 3323 -- Returns the variables that would be fixed by knowing a TyConBinder. See 3324 -- Note [When does a tycon application need an explicit kind signature?] 3325 -- for a more detailed explanation of what this function does. 3326 injective_vars_of_binder :: TyConBinder -> FV 3327 injective_vars_of_binder (Bndr tv vis) = 3328 case vis of 3329 AnonTCB VisArg -> injectiveVarsOfType False -- conservative choice 3330 (varType tv) 3331 NamedTCB argf | source_of_injectivity argf 3332 -> unitFV tv `unionFV` 3333 injectiveVarsOfType False (varType tv) 3334 _ -> emptyFV 3335 3336 source_of_injectivity Required = True 3337 -- See Note [Explicit Case Statement for Specificity] 3338 source_of_injectivity (Invisible spec) = case spec of 3339 SpecifiedSpec -> spec_inj_pos 3340 InferredSpec -> False 3341 3342{- 3343Note [Explicit Case Statement for Specificity] 3344~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3345When pattern matching against an `ArgFlag`, you should not pattern match against 3346the pattern synonyms 'Specified' or 'Inferred', as this results in a 3347non-exhaustive pattern match warning. 3348Instead, pattern match against 'Invisible spec' and do another case analysis on 3349this specificity argument. 3350The issue has been fixed in GHC 8.10 (ticket #17876). This hack can thus be 3351dropped once version 8.10 is used as the minimum version for building GHC. 3352 3353Note [When does a tycon application need an explicit kind signature?] 3354~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3355There are a couple of places in GHC where we convert Core Types into forms that 3356more closely resemble user-written syntax. These include: 3357 33581. Template Haskell Type reification (see, for instance, GHC.Tc.Gen.Splice.reify_tc_app) 33592. Converting Types to LHsTypes (such as in Haddock.Convert in haddock) 3360 3361This conversion presents a challenge: how do we ensure that the resulting type 3362has enough kind information so as not to be ambiguous? To better motivate this 3363question, consider the following Core type: 3364 3365 -- Foo :: Type -> Type 3366 type Foo = Proxy Type 3367 3368There is nothing ambiguous about the RHS of Foo in Core. But if we were to, 3369say, reify it into a TH Type, then it's tempting to just drop the invisible 3370Type argument and simply return `Proxy`. But now we've lost crucial kind 3371information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool` 3372or `Proxy Int` or something else! We've inadvertently introduced ambiguity. 3373 3374Unlike in other situations in GHC, we can't just turn on 3375-fprint-explicit-kinds, as we need to produce something which has the same 3376structure as a source-syntax type. Moreover, we can't rely on visible kind 3377application, since the first kind argument to Proxy is inferred, not specified. 3378Our solution is to annotate certain tycons with their kinds whenever they 3379appear in applied form in order to resolve the ambiguity. For instance, we 3380would reify the RHS of Foo like so: 3381 3382 type Foo = (Proxy :: Type -> Type) 3383 3384We need to devise an algorithm that determines precisely which tycons need 3385these explicit kind signatures. We certainly don't want to annotate _every_ 3386tycon with a kind signature, or else we might end up with horribly bloated 3387types like the following: 3388 3389 (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type) 3390 3391We only want to annotate tycons that absolutely require kind signatures in 3392order to resolve some sort of ambiguity, and nothing more. 3393 3394Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type 3395require a kind signature? It might require it when we need to fill in any of 3396T's omitted arguments. By "omitted argument", we mean one that is dropped when 3397reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and 3398specified arguments (e.g., TH reification in GHC.Tc.Gen.Splice), and sometimes the 3399omitted arguments are only the inferred ones (e.g., in situations where 3400specified arguments are reified through visible kind application). 3401Regardless, the key idea is that _some_ arguments are going to be omitted after 3402reification, and the only mechanism we have at our disposal for filling them in 3403is through explicit kind signatures. 3404 3405What do we mean by "fill in"? Let's consider this small example: 3406 3407 T :: forall {k}. Type -> (k -> Type) -> k 3408 3409Moreover, we have this application of T: 3410 3411 T @{j} Int aty 3412 3413When we reify this type, we omit the inferred argument @{j}. Is it fixed by the 3414other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then 3415we'll generate an equality constraint (kappa -> Type) and, assuming we can 3416solve it, that will fix `kappa`. (Here, `kappa` is the unification variable 3417that we instantiate `k` with.) 3418 3419Therefore, for any application of a tycon T to some arguments, the Question We 3420Must Answer is: 3421 3422* Given the first n arguments of T, do the kinds of the non-omitted arguments 3423 fill in the omitted arguments? 3424 3425(This is still a bit hand-wavey, but we'll refine this question incrementally 3426as we explain more of the machinery underlying this process.) 3427 3428Answering this question is precisely the role that the `injectiveVarsOfType` 3429and `injective_vars_of_binder` functions exist to serve. If an omitted argument 3430`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing 3431`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a 3432bit.) 3433 3434More formally, if 3435`a` is in `injectiveVarsOfType ty` 3436and S1(ty) ~ S2(ty), 3437then S1(a) ~ S2(a), 3438where S1 and S2 are arbitrary substitutions. 3439 3440For example, is `F` is a non-injective type family, then 3441 3442 injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c} 3443 3444Now that we know what this function does, here is a second attempt at the 3445Question We Must Answer: 3446 3447* Given the first n arguments of T (ty_1 ... ty_n), consider the binders 3448 of T that are instantiated by non-omitted arguments. Do the injective 3449 variables of these binders fill in the remainder of T's kind? 3450 3451Alright, we're getting closer. Next, we need to clarify what the injective 3452variables of a tycon binder are. This the role that the 3453`injective_vars_of_binder` function serves. Here is what this function does for 3454each form of tycon binder: 3455 3456* Anonymous binders are injective positions. For example, in the promoted data 3457 constructor '(:): 3458 3459 '(:) :: forall a. a -> [a] -> [a] 3460 3461 The second and third tyvar binders (of kinds `a` and `[a]`) are both 3462 anonymous, so if we had '(:) 'True '[], then the kinds of 'True and 3463 '[] would contribute to the kind of '(:) 'True '[]. Therefore, 3464 injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}. 3465 (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.) 3466* Named binders: 3467 - Inferred binders are never injective positions. For example, in this data 3468 type: 3469 3470 data Proxy a 3471 Proxy :: forall {k}. k -> Type 3472 3473 If we had Proxy 'True, then the kind of 'True would not contribute to the 3474 kind of Proxy 'True. Therefore, 3475 injective_vars_of_binder(forall {k}. ...) = {}. 3476 - Required binders are injective positions. For example, in this data type: 3477 3478 data Wurble k (a :: k) :: k 3479 Wurble :: forall k -> k -> k 3480 3481 The first tyvar binder (of kind `forall k`) has required visibility, so if 3482 we had Wurble (Maybe a) Nothing, then the kind of Maybe a would 3483 contribute to the kind of Wurble (Maybe a) Nothing. Hence, 3484 injective_vars_of_binder(forall a -> ...) = {a}. 3485 - Specified binders /might/ be injective positions, depending on how you 3486 approach things. Continuing the '(:) example: 3487 3488 '(:) :: forall a. a -> [a] -> [a] 3489 3490 Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind 3491 of '(:) 'True '[], since it's not explicitly instantiated by the user. But 3492 if visible kind application is enabled, then this is possible, since the 3493 user can write '(:) @Bool 'True '[]. (In that case, 3494 injective_vars_of_binder(forall a. ...) = {a}.) 3495 3496 There are some situations where using visible kind application is appropriate 3497 and others where it is not (e.g., TH 3498 reification), so the `injective_vars_of_binder` function is parametrized by 3499 a Bool which decides if specified binders should be counted towards 3500 injective positions or not. 3501 3502Now that we've defined injective_vars_of_binder, we can refine the Question We 3503Must Answer once more: 3504 3505* Given the first n arguments of T (ty_1 ... ty_n), consider the binders 3506 of T that are instantiated by non-omitted arguments. For each such binder 3507 b_i, take the union of all injective_vars_of_binder(b_i). Is this set a 3508 superset of the free variables of the remainder of T's kind? 3509 3510If the answer to this question is "no", then (T ty_1 ... ty_n) needs an 3511explicit kind signature, since T's kind has kind variables leftover that 3512aren't fixed by the non-omitted arguments. 3513 3514One last sticking point: what does "the remainder of T's kind" mean? You might 3515be tempted to think that it corresponds to all of the arguments in the kind of 3516T that would normally be instantiated by omitted arguments. But this isn't 3517quite right, strictly speaking. Consider the following (silly) example: 3518 3519 S :: forall {k}. Type -> Type 3520 3521And suppose we have this application of S: 3522 3523 S Int Bool 3524 3525The Int argument would be omitted, and 3526injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which 3527might suggest that (S Bool) needs an explicit kind signature. But 3528(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature 3529only affects the /result/ of the application, not all of the individual 3530arguments. So adding a kind signature here won't make a difference. Therefore, 3531the fourth (and final) iteration of the Question We Must Answer is: 3532 3533* Given the first n arguments of T (ty_1 ... ty_n), consider the binders 3534 of T that are instantiated by non-omitted arguments. For each such binder 3535 b_i, take the union of all injective_vars_of_binder(b_i). Is this set a 3536 superset of the free variables of the kind of (T ty_1 ... ty_n)? 3537 3538Phew, that was a lot of work! 3539 3540How can be sure that this is correct? That is, how can we be sure that in the 3541event that we leave off a kind annotation, that one could infer the kind of the 3542tycon application from its arguments? It's essentially a proof by induction: if 3543we can infer the kinds of every subtree of a type, then the whole tycon 3544application will have an inferrable kind--unless, of course, the remainder of 3545the tycon application's kind has uninstantiated kind variables. 3546 3547What happens if T is oversaturated? That is, if T's kind has fewer than n 3548arguments, in the case that the concrete application instantiates a result 3549kind variable with an arrow kind? If we run out of arguments, we do not attach 3550a kind annotation. This should be a rare case, indeed. Here is an example: 3551 3552 data T1 :: k1 -> k2 -> * 3553 data T2 :: k1 -> k2 -> * 3554 3555 type family G (a :: k) :: k 3556 type instance G T1 = T2 3557 3558 type instance F Char = (G T1 Bool :: (* -> *) -> *) -- F from above 3559 3560Here G's kind is (forall k. k -> k), and the desugared RHS of that last 3561instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to 3562the algorithm above, there are 3 arguments to G so we should peel off 3 3563arguments in G's kind. But G's kind has only two arguments. This is the 3564rare special case, and we choose not to annotate the application of G with 3565a kind signature. After all, we needn't do this, since that instance would 3566be reified as: 3567 3568 type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool 3569 3570So the kind of G isn't ambiguous anymore due to the explicit kind annotation 3571on its argument. See #8953 and test th/T8953. 3572-} 3573 3574{- 3575************************************************************************ 3576* * 3577 Multiplicities 3578* * 3579************************************************************************ 3580 3581These functions would prefer to be in GHC.Core.Multiplicity, but 3582they some are used elsewhere in this module, and wanted to bring 3583their friends here with them. 3584-} 3585 3586unrestricted, linear, tymult :: a -> Scaled a 3587 3588-- | Scale a payload by Many 3589unrestricted = Scaled Many 3590 3591-- | Scale a payload by One 3592linear = Scaled One 3593 3594-- | Scale a payload by Many; used for type arguments in core 3595tymult = Scaled Many 3596 3597irrelevantMult :: Scaled a -> a 3598irrelevantMult = scaledThing 3599 3600mkScaled :: Mult -> a -> Scaled a 3601mkScaled = Scaled 3602 3603scaledSet :: Scaled a -> b -> Scaled b 3604scaledSet (Scaled m _) b = Scaled m b 3605 3606pattern One :: Mult 3607pattern One <- (isOneDataConTy -> True) 3608 where One = oneDataConTy 3609 3610pattern Many :: Mult 3611pattern Many <- (isManyDataConTy -> True) 3612 where Many = manyDataConTy 3613 3614isManyDataConTy :: Mult -> Bool 3615isManyDataConTy ty 3616 | Just tc <- tyConAppTyCon_maybe ty 3617 = tc `hasKey` manyDataConKey 3618isManyDataConTy _ = False 3619 3620isOneDataConTy :: Mult -> Bool 3621isOneDataConTy ty 3622 | Just tc <- tyConAppTyCon_maybe ty 3623 = tc `hasKey` oneDataConKey 3624isOneDataConTy _ = False 3625 3626isLinearType :: Type -> Bool 3627-- ^ @isLinear t@ returns @True@ of a if @t@ is a type of (curried) function 3628-- where at least one argument is linear (or otherwise non-unrestricted). We use 3629-- this function to check whether it is safe to eta reduce an Id in CorePrep. It 3630-- is always safe to return 'True', because 'True' deactivates the optimisation. 3631isLinearType ty = case ty of 3632 FunTy _ Many _ res -> isLinearType res 3633 FunTy _ _ _ _ -> True 3634 ForAllTy _ res -> isLinearType res 3635 _ -> False 3636