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