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