1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 4 5\section[TcType]{Types used in the typechecker} 6 7This module provides the Type interface for front-end parts of the 8compiler. These parts 9 10 * treat "source types" as opaque: 11 newtypes, and predicates are meaningful. 12 * look through usage types 13 14The "tc" prefix is for "TypeChecker", because the type checker 15is the principal client. 16-} 17 18{-# LANGUAGE CPP, ScopedTypeVariables, MultiWayIf, FlexibleContexts #-} 19 20module TcType ( 21 -------------------------------- 22 -- Types 23 TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 24 TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, 25 TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcTyCon, 26 KnotTied, 27 28 ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType, 29 30 SyntaxOpType(..), synKnownType, mkSynFunTys, 31 32 -- TcLevel 33 TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, 34 strictlyDeeperThan, sameDepthAs, 35 tcTypeLevel, tcTyVarLevel, maxTcLevel, 36 promoteSkolem, promoteSkolemX, promoteSkolemsX, 37 -------------------------------- 38 -- MetaDetails 39 TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv, 40 MetaDetails(Flexi, Indirect), MetaInfo(..), 41 isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, 42 tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar, 43 isFskTyVar, isFmvTyVar, isFlattenTyVar, 44 isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo, 45 isFlexi, isIndirect, isRuntimeUnkSkol, 46 metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, 47 isTouchableMetaTyVar, 48 isFloatedTouchableMetaTyVar, 49 findDupTyVarTvs, mkTyVarNamePairs, 50 51 -------------------------------- 52 -- Builders 53 mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy, 54 mkTcAppTy, mkTcAppTys, mkTcCastTy, 55 56 -------------------------------- 57 -- Splitters 58 -- These are important because they do not look through newtypes 59 getTyVar, 60 tcSplitForAllTy_maybe, 61 tcSplitForAllTys, tcSplitForAllTysSameVis, 62 tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs, 63 tcSplitPhiTy, tcSplitPredFunTy_maybe, 64 tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN, 65 tcSplitFunTysN, 66 tcSplitTyConApp, tcSplitTyConApp_maybe, 67 tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs, 68 tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe, 69 tcRepGetNumAppTys, 70 tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole, 71 tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe, 72 73 --------------------------------- 74 -- Predicates. 75 -- Again, newtypes are opaque 76 eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX, 77 pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis, 78 isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy, 79 isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, 80 isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred, 81 hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 82 isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck, 83 checkValidClsArgs, hasTyVarHead, 84 isRigidTy, isAlmostFunctionFree, 85 86 --------------------------------- 87 -- Misc type manipulators 88 89 deNoteType, 90 orphNamesOfType, orphNamesOfCo, 91 orphNamesOfTypes, orphNamesOfCoCon, 92 getDFunTyKey, evVarPred, 93 94 --------------------------------- 95 -- Predicate types 96 mkMinimalBySCs, transSuperClasses, 97 pickQuantifiablePreds, pickCapturedPreds, 98 immSuperClasses, boxEqPred, 99 isImprovementPred, 100 101 -- * Finding type instances 102 tcTyFamInsts, tcTyFamInstsAndVis, tcTyConAppTyFamInstsAndVis, isTyFamFree, 103 104 -- * Finding "exact" (non-dead) type variables 105 exactTyCoVarsOfType, exactTyCoVarsOfTypes, 106 anyRewritableTyVar, 107 108 --------------------------------- 109 -- Foreign import and export 110 isFFIArgumentTy, -- :: DynFlags -> Safety -> Type -> Bool 111 isFFIImportResultTy, -- :: DynFlags -> Type -> Bool 112 isFFIExportResultTy, -- :: Type -> Bool 113 isFFIExternalTy, -- :: Type -> Bool 114 isFFIDynTy, -- :: Type -> Type -> Bool 115 isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool 116 isFFIPrimResultTy, -- :: DynFlags -> Type -> Bool 117 isFFILabelTy, -- :: Type -> Bool 118 isFFITy, -- :: Type -> Bool 119 isFunPtrTy, -- :: Type -> Bool 120 tcSplitIOType_maybe, -- :: Type -> Maybe Type 121 122 -------------------------------- 123 -- Rexported from Kind 124 Kind, tcTypeKind, 125 liftedTypeKind, 126 constraintKind, 127 isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues, 128 129 -------------------------------- 130 -- Rexported from Type 131 Type, PredType, ThetaType, TyCoBinder, 132 ArgFlag(..), AnonArgFlag(..), ForallVisFlag(..), 133 134 mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy, 135 mkInvForAllTy, mkInvForAllTys, 136 mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTys, 137 mkTyConApp, mkAppTy, mkAppTys, 138 mkTyConTy, mkTyVarTy, mkTyVarTys, 139 mkTyCoVarTy, mkTyCoVarTys, 140 141 isClassPred, isEqPrimPred, isIPPred, isEqPred, isEqPredClass, 142 mkClassPred, 143 tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy, 144 isRuntimeRepVar, isKindLevPoly, 145 isVisibleBinder, isInvisibleBinder, 146 147 -- Type substitutions 148 TCvSubst(..), -- Representation visible to a few friends 149 TvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst, 150 zipTvSubst, 151 mkTvSubstPrs, notElemTCvSubst, unionTCvSubst, 152 getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope, 153 extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope, 154 Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr, 155 Type.extendTvSubst, 156 isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv, 157 Type.substTy, substTys, substTyWith, substTyWithCoVars, 158 substTyAddInScope, 159 substTyUnchecked, substTysUnchecked, substThetaUnchecked, 160 substTyWithUnchecked, 161 substCoUnchecked, substCoWithUnchecked, 162 substTheta, 163 164 isUnliftedType, -- Source types are always lifted 165 isUnboxedTupleType, -- Ditto 166 isPrimitiveType, 167 168 tcView, coreView, 169 170 tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds, 171 tyCoFVsOfType, tyCoFVsOfTypes, 172 tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet, 173 tyCoVarsOfTypeList, tyCoVarsOfTypesList, 174 noFreeVarsOfType, 175 176 -------------------------------- 177 pprKind, pprParendKind, pprSigmaType, 178 pprType, pprParendType, pprTypeApp, pprTyThingCategory, tyThingCategory, 179 pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred, 180 pprTCvBndr, pprTCvBndrs, 181 182 TypeSize, sizeType, sizeTypes, scopedSort, 183 184 --------------------------------- 185 -- argument visibility 186 tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible 187 188 ) where 189 190#include "GhclibHsVersions.h" 191 192-- friends: 193import GhcPrelude 194 195import TyCoRep 196import TyCoSubst ( mkTvSubst, substTyWithCoVars ) 197import TyCoFVs 198import TyCoPpr 199import Class 200import Var 201import ForeignCall 202import VarSet 203import Coercion 204import Type 205import Predicate 206import RepType 207import TyCon 208 209-- others: 210import DynFlags 211import CoreFVs 212import Name -- hiding (varName) 213 -- We use this to make dictionaries for type literals. 214 -- Perhaps there's a better way to do this? 215import NameSet 216import VarEnv 217import PrelNames 218import TysWiredIn( coercibleClass, eqClass, heqClass, unitTyCon, unitTyConKey 219 , listTyCon, constraintKind ) 220import BasicTypes 221import Util 222import Maybes 223import ListSetOps ( getNth, findDupsEq ) 224import Outputable 225import FastString 226import ErrUtils( Validity(..), MsgDoc, isValid ) 227import qualified GHC.LanguageExtensions as LangExt 228 229import Data.List ( mapAccumL ) 230-- import Data.Functor.Identity( Identity(..) ) 231import Data.IORef 232import Data.List.NonEmpty( NonEmpty(..) ) 233 234{- 235************************************************************************ 236* * 237 Types 238* * 239************************************************************************ 240 241The type checker divides the generic Type world into the 242following more structured beasts: 243 244sigma ::= forall tyvars. phi 245 -- A sigma type is a qualified type 246 -- 247 -- Note that even if 'tyvars' is empty, theta 248 -- may not be: e.g. (?x::Int) => Int 249 250 -- Note that 'sigma' is in prenex form: 251 -- all the foralls are at the front. 252 -- A 'phi' type has no foralls to the right of 253 -- an arrow 254 255phi :: theta => rho 256 257rho ::= sigma -> rho 258 | tau 259 260-- A 'tau' type has no quantification anywhere 261-- Note that the args of a type constructor must be taus 262tau ::= tyvar 263 | tycon tau_1 .. tau_n 264 | tau_1 tau_2 265 | tau_1 -> tau_2 266 267-- In all cases, a (saturated) type synonym application is legal, 268-- provided it expands to the required form. 269 270Note [TcTyVars and TyVars in the typechecker] 271~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 272The typechecker uses a lot of type variables with special properties, 273notably being a unification variable with a mutable reference. These 274use the 'TcTyVar' variant of Var.Var. 275 276Note, though, that a /bound/ type variable can (and probably should) 277be a TyVar. E.g 278 forall a. a -> a 279Here 'a' is really just a deBruijn-number; it certainly does not have 280a signficant TcLevel (as every TcTyVar does). So a forall-bound type 281variable should be TyVars; and hence a TyVar can appear free in a TcType. 282 283The type checker and constraint solver can also encounter /free/ type 284variables that use the 'TyVar' variant of Var.Var, for a couple of 285reasons: 286 287 - When typechecking a class decl, say 288 class C (a :: k) where 289 foo :: T a -> Int 290 We have first kind-check the header; fix k and (a:k) to be 291 TyVars, bring 'k' and 'a' into scope, and kind check the 292 signature for 'foo'. In doing so we call solveEqualities to 293 solve any kind equalities in foo's signature. So the solver 294 may see free occurrences of 'k'. 295 296 See calls to tcExtendTyVarEnv for other places that ordinary 297 TyVars are bought into scope, and hence may show up in the types 298 and kinds generated by TcHsType. 299 300 - The pattern-match overlap checker calls the constraint solver, 301 long afer TcTyVars have been zonked away 302 303It's convenient to simply treat these TyVars as skolem constants, 304which of course they are. We give them a level number of "outermost", 305so they behave as global constants. Specifically: 306 307* Var.tcTyVarDetails succeeds on a TyVar, returning 308 vanillaSkolemTv, as well as on a TcTyVar. 309 310* tcIsTcTyVar returns True for both TyVar and TcTyVar variants 311 of Var.Var. The "tc" prefix means "a type variable that can be 312 encountered by the typechecker". 313 314This is a bit of a change from an earlier era when we remoselessly 315insisted on real TcTyVars in the type checker. But that seems 316unnecessary (for skolems, TyVars are fine) and it's now very hard 317to guarantee, with the advent of kind equalities. 318 319Note [Coercion variables in free variable lists] 320~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 321There are several places in the GHC codebase where functions like 322tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type 323variables of a type. The "Co" part of these functions' names shouldn't be 324dismissed, as it is entirely possible that they will include coercion variables 325in addition to type variables! As a result, there are some places in TcType 326where we must take care to check that a variable is a _type_ variable (using 327isTyVar) before calling tcTyVarDetails--a partial function that is not defined 328for coercion variables--on the variable. Failing to do so led to 329GHC #12785. 330-} 331 332-- See Note [TcTyVars and TyVars in the typechecker] 333type TcCoVar = CoVar -- Used only during type inference 334type TcType = Type -- A TcType can have mutable type variables 335type TcTyCoVar = Var -- Either a TcTyVar or a CoVar 336 -- Invariant on ForAllTy in TcTypes: 337 -- forall a. T 338 -- a cannot occur inside a MutTyVar in T; that is, 339 -- T is "flattened" before quantifying over a 340 341type TcTyVarBinder = TyVarBinder 342type TcTyCon = TyCon -- these can be the TcTyCon constructor 343 344-- These types do not have boxy type variables in them 345type TcPredType = PredType 346type TcThetaType = ThetaType 347type TcSigmaType = TcType 348type TcRhoType = TcType -- Note [TcRhoType] 349type TcTauType = TcType 350type TcKind = Kind 351type TcTyVarSet = TyVarSet 352type TcTyCoVarSet = TyCoVarSet 353type TcDTyVarSet = DTyVarSet 354type TcDTyCoVarSet = DTyCoVarSet 355 356{- ********************************************************************* 357* * 358 ExpType: an "expected type" in the type checker 359* * 360********************************************************************* -} 361 362-- | An expected type to check against during type-checking. 363-- See Note [ExpType] in TcMType, where you'll also find manipulators. 364data ExpType = Check TcType 365 | Infer !InferResult 366 367data InferResult 368 = IR { ir_uniq :: Unique -- For debugging only 369 370 , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in TcMType 371 372 , ir_inst :: Bool 373 -- True <=> deeply instantiate before returning 374 -- i.e. return a RhoType 375 -- False <=> do not instantiate before returning 376 -- i.e. return a SigmaType 377 -- See Note [Deep instantiation of InferResult] in TcUnify 378 379 , ir_ref :: IORef (Maybe TcType) } 380 -- The type that fills in this hole should be a Type, 381 -- that is, its kind should be (TYPE rr) for some rr 382 383type ExpSigmaType = ExpType 384type ExpRhoType = ExpType 385 386instance Outputable ExpType where 387 ppr (Check ty) = text "Check" <> braces (ppr ty) 388 ppr (Infer ir) = ppr ir 389 390instance Outputable InferResult where 391 ppr (IR { ir_uniq = u, ir_lvl = lvl 392 , ir_inst = inst }) 393 = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst) 394 395-- | Make an 'ExpType' suitable for checking. 396mkCheckExpType :: TcType -> ExpType 397mkCheckExpType = Check 398 399 400{- ********************************************************************* 401* * 402 SyntaxOpType 403* * 404********************************************************************* -} 405 406-- | What to expect for an argument to a rebindable-syntax operator. 407-- Quite like 'Type', but allows for holes to be filled in by tcSyntaxOp. 408-- The callback called from tcSyntaxOp gets a list of types; the meaning 409-- of these types is determined by a left-to-right depth-first traversal 410-- of the 'SyntaxOpType' tree. So if you pass in 411-- 412-- > SynAny `SynFun` (SynList `SynFun` SynType Int) `SynFun` SynAny 413-- 414-- you'll get three types back: one for the first 'SynAny', the /element/ 415-- type of the list, and one for the last 'SynAny'. You don't get anything 416-- for the 'SynType', because you've said positively that it should be an 417-- Int, and so it shall be. 418-- 419-- This is defined here to avoid defining it in TcExpr.hs-boot. 420data SyntaxOpType 421 = SynAny -- ^ Any type 422 | SynRho -- ^ A rho type, deeply skolemised or instantiated as appropriate 423 | SynList -- ^ A list type. You get back the element type of the list 424 | SynFun SyntaxOpType SyntaxOpType 425 -- ^ A function. 426 | SynType ExpType -- ^ A known type. 427infixr 0 `SynFun` 428 429-- | Like 'SynType' but accepts a regular TcType 430synKnownType :: TcType -> SyntaxOpType 431synKnownType = SynType . mkCheckExpType 432 433-- | Like 'mkFunTys' but for 'SyntaxOpType' 434mkSynFunTys :: [SyntaxOpType] -> ExpType -> SyntaxOpType 435mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys 436 437 438{- 439Note [TcRhoType] 440~~~~~~~~~~~~~~~~ 441A TcRhoType has no foralls or contexts at the top, or to the right of an arrow 442 YES (forall a. a->a) -> Int 443 NO forall a. a -> Int 444 NO Eq a => a -> a 445 NO Int -> forall a. a -> Int 446 447 448************************************************************************ 449* * 450 TyVarDetails, MetaDetails, MetaInfo 451* * 452************************************************************************ 453 454TyVarDetails gives extra info about type variables, used during type 455checking. It's attached to mutable type variables only. 456It's knot-tied back to Var.hs. There is no reason in principle 457why Var.hs shouldn't actually have the definition, but it "belongs" here. 458 459Note [Signature skolems] 460~~~~~~~~~~~~~~~~~~~~~~~~ 461A TyVarTv is a specialised variant of TauTv, with the following invarints: 462 463 * A TyVarTv can be unified only with a TyVar, 464 not with any other type 465 466 * Its MetaDetails, if filled in, will always be another TyVarTv 467 or a SkolemTv 468 469TyVarTvs are only distinguished to improve error messages. 470Consider this 471 472 data T (a:k1) = MkT (S a) 473 data S (b:k2) = MkS (T b) 474 475When doing kind inference on {S,T} we don't want *skolems* for k1,k2, 476because they end up unifying; we want those TyVarTvs again. 477 478 479Note [TyVars and TcTyVars during type checking] 480~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 481The Var type has constructors TyVar and TcTyVar. They are used 482as follows: 483 484* TcTyVar: used /only/ during type checking. Should never appear 485 afterwards. May contain a mutable field, in the MetaTv case. 486 487* TyVar: is never seen by the constraint solver, except locally 488 inside a type like (forall a. [a] ->[a]), where 'a' is a TyVar. 489 We instantiate these with TcTyVars before exposing the type 490 to the constraint solver. 491 492I have swithered about the latter invariant, excluding TyVars from the 493constraint solver. It's not strictly essential, and indeed 494(historically but still there) Var.tcTyVarDetails returns 495vanillaSkolemTv for a TyVar. 496 497But ultimately I want to seeparate Type from TcType, and in that case 498we would need to enforce the separation. 499-} 500 501-- A TyVarDetails is inside a TyVar 502-- See Note [TyVars and TcTyVars] 503data TcTyVarDetails 504 = SkolemTv -- A skolem 505 TcLevel -- Level of the implication that binds it 506 -- See TcUnify Note [Deeper level on the left] for 507 -- how this level number is used 508 Bool -- True <=> this skolem type variable can be overlapped 509 -- when looking up instances 510 -- See Note [Binding when looking up instances] in InstEnv 511 512 | RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi 513 -- interactive context 514 515 | MetaTv { mtv_info :: MetaInfo 516 , mtv_ref :: IORef MetaDetails 517 , mtv_tclvl :: TcLevel } -- See Note [TcLevel and untouchable type variables] 518 519vanillaSkolemTv, superSkolemTv :: TcTyVarDetails 520-- See Note [Binding when looking up instances] in InstEnv 521vanillaSkolemTv = SkolemTv topTcLevel False -- Might be instantiated 522superSkolemTv = SkolemTv topTcLevel True -- Treat this as a completely distinct type 523 -- The choice of level number here is a bit dodgy, but 524 -- topTcLevel works in the places that vanillaSkolemTv is used 525 526instance Outputable TcTyVarDetails where 527 ppr = pprTcTyVarDetails 528 529pprTcTyVarDetails :: TcTyVarDetails -> SDoc 530-- For debugging 531pprTcTyVarDetails (RuntimeUnk {}) = text "rt" 532pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl 533pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl 534pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl }) 535 = ppr info <> colon <> ppr tclvl 536 537----------------------------- 538data MetaDetails 539 = Flexi -- Flexi type variables unify to become Indirects 540 | Indirect TcType 541 542data MetaInfo 543 = TauTv -- This MetaTv is an ordinary unification variable 544 -- A TauTv is always filled in with a tau-type, which 545 -- never contains any ForAlls. 546 547 | TyVarTv -- A variant of TauTv, except that it should not be 548 -- unified with a type, only with a type variable 549 -- See Note [Signature skolems] 550 551 | FlatMetaTv -- A flatten meta-tyvar 552 -- It is a meta-tyvar, but it is always untouchable, with level 0 553 -- See Note [The flattening story] in TcFlatten 554 555 | FlatSkolTv -- A flatten skolem tyvar 556 -- Just like FlatMetaTv, but is comletely "owned" by 557 -- its Given CFunEqCan. 558 -- It is filled in /only/ by unflattenGivens 559 -- See Note [The flattening story] in TcFlatten 560 561instance Outputable MetaDetails where 562 ppr Flexi = text "Flexi" 563 ppr (Indirect ty) = text "Indirect" <+> ppr ty 564 565instance Outputable MetaInfo where 566 ppr TauTv = text "tau" 567 ppr TyVarTv = text "tyv" 568 ppr FlatMetaTv = text "fmv" 569 ppr FlatSkolTv = text "fsk" 570 571{- ********************************************************************* 572* * 573 Untouchable type variables 574* * 575********************************************************************* -} 576 577newtype TcLevel = TcLevel Int deriving( Eq, Ord ) 578 -- See Note [TcLevel and untouchable type variables] for what this Int is 579 -- See also Note [TcLevel assignment] 580 581{- 582Note [TcLevel and untouchable type variables] 583~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 584* Each unification variable (MetaTv) 585 and each Implication 586 has a level number (of type TcLevel) 587 588* INVARIANTS. In a tree of Implications, 589 590 (ImplicInv) The level number (ic_tclvl) of an Implication is 591 STRICTLY GREATER THAN that of its parent 592 593 (SkolInv) The level number of the skolems (ic_skols) of an 594 Implication is equal to the level of the implication 595 itself (ic_tclvl) 596 597 (GivenInv) The level number of a unification variable appearing 598 in the 'ic_given' of an implication I should be 599 STRICTLY LESS THAN the ic_tclvl of I 600 601 (WantedInv) The level number of a unification variable appearing 602 in the 'ic_wanted' of an implication I should be 603 LESS THAN OR EQUAL TO the ic_tclvl of I 604 See Note [WantedInv] 605 606* A unification variable is *touchable* if its level number 607 is EQUAL TO that of its immediate parent implication, 608 and it is a TauTv or TyVarTv (but /not/ FlatMetaTv or FlatSkolTv) 609 610Note [WantedInv] 611~~~~~~~~~~~~~~~~ 612Why is WantedInv important? Consider this implication, where 613the constraint (C alpha[3]) disobeys WantedInv: 614 615 forall[2] a. blah => (C alpha[3]) 616 (forall[3] b. alpha[3] ~ b) 617 618We can unify alpha:=b in the inner implication, because 'alpha' is 619touchable; but then 'b' has excaped its scope into the outer implication. 620 621Note [Skolem escape prevention] 622~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 623We only unify touchable unification variables. Because of 624(WantedInv), there can be no occurrences of the variable further out, 625so the unification can't cause the skolems to escape. Example: 626 data T = forall a. MkT a (a->Int) 627 f x (MkT v f) = length [v,x] 628We decide (x::alpha), and generate an implication like 629 [1]forall a. (a ~ alpha[0]) 630But we must not unify alpha:=a, because the skolem would escape. 631 632For the cases where we DO want to unify, we rely on floating the 633equality. Example (with same T) 634 g x (MkT v f) = x && True 635We decide (x::alpha), and generate an implication like 636 [1]forall a. (Bool ~ alpha[0]) 637We do NOT unify directly, bur rather float out (if the constraint 638does not mention 'a') to get 639 (Bool ~ alpha[0]) /\ [1]forall a.() 640and NOW we can unify alpha. 641 642The same idea of only unifying touchables solves another problem. 643Suppose we had 644 (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1]) 645In this example, beta is touchable inside the implication. The 646first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside 647the implication where a new constraint 648 uf ~ beta 649emerges. If we (wrongly) spontaneously solved it to get uf := beta, 650the whole implication disappears but when we pop out again we are left with 651(F Int ~ uf) which will be unified by our final zonking stage and 652uf will get unified *once more* to (F Int). 653 654Note [TcLevel assignment] 655~~~~~~~~~~~~~~~~~~~~~~~~~ 656We arrange the TcLevels like this 657 658 0 Top level 659 1 First-level implication constraints 660 2 Second-level implication constraints 661 ...etc... 662-} 663 664maxTcLevel :: TcLevel -> TcLevel -> TcLevel 665maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b) 666 667topTcLevel :: TcLevel 668-- See Note [TcLevel assignment] 669topTcLevel = TcLevel 0 -- 0 = outermost level 670 671isTopTcLevel :: TcLevel -> Bool 672isTopTcLevel (TcLevel 0) = True 673isTopTcLevel _ = False 674 675pushTcLevel :: TcLevel -> TcLevel 676-- See Note [TcLevel assignment] 677pushTcLevel (TcLevel us) = TcLevel (us + 1) 678 679strictlyDeeperThan :: TcLevel -> TcLevel -> Bool 680strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl) 681 = tv_tclvl > ctxt_tclvl 682 683sameDepthAs :: TcLevel -> TcLevel -> Bool 684sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl) 685 = ctxt_tclvl == tv_tclvl -- NB: invariant ctxt_tclvl >= tv_tclvl 686 -- So <= would be equivalent 687 688checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool 689-- Checks (WantedInv) from Note [TcLevel and untouchable type variables] 690checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl) 691 = ctxt_tclvl >= tv_tclvl 692 693-- Returns topTcLevel for non-TcTyVars 694tcTyVarLevel :: TcTyVar -> TcLevel 695tcTyVarLevel tv 696 = case tcTyVarDetails tv of 697 MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl 698 SkolemTv tv_lvl _ -> tv_lvl 699 RuntimeUnk -> topTcLevel 700 701 702tcTypeLevel :: TcType -> TcLevel 703-- Max level of any free var of the type 704tcTypeLevel ty 705 = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty) 706 where 707 add v lvl 708 | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v 709 | otherwise = lvl 710 711instance Outputable TcLevel where 712 ppr (TcLevel us) = ppr us 713 714promoteSkolem :: TcLevel -> TcTyVar -> TcTyVar 715promoteSkolem tclvl skol 716 | tclvl < tcTyVarLevel skol 717 = ASSERT( isTcTyVar skol && isSkolemTyVar skol ) 718 setTcTyVarDetails skol (SkolemTv tclvl (isOverlappableTyVar skol)) 719 720 | otherwise 721 = skol 722 723-- | Change the TcLevel in a skolem, extending a substitution 724promoteSkolemX :: TcLevel -> TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar) 725promoteSkolemX tclvl subst skol 726 = ASSERT( isTcTyVar skol && isSkolemTyVar skol ) 727 (new_subst, new_skol) 728 where 729 new_skol 730 | tclvl < tcTyVarLevel skol 731 = setTcTyVarDetails (updateTyVarKind (substTy subst) skol) 732 (SkolemTv tclvl (isOverlappableTyVar skol)) 733 | otherwise 734 = updateTyVarKind (substTy subst) skol 735 new_subst = extendTvSubstWithClone subst skol new_skol 736 737promoteSkolemsX :: TcLevel -> TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar]) 738promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl) 739 740{- ********************************************************************* 741* * 742 Finding type family instances 743* * 744************************************************************************ 745-} 746 747-- | Finds outermost type-family applications occurring in a type, 748-- after expanding synonyms. In the list (F, tys) that is returned 749-- we guarantee that tys matches F's arity. For example, given 750-- type family F a :: * -> * (arity 1) 751-- calling tcTyFamInsts on (Maybe (F Int Bool) will return 752-- (F, [Int]), not (F, [Int,Bool]) 753-- 754-- This is important for its use in deciding termination of type 755-- instances (see #11581). E.g. 756-- type instance G [Int] = ...(F Int <big type>)... 757-- we don't need to take <big type> into account when asking if 758-- the calls on the RHS are smaller than the LHS 759tcTyFamInsts :: Type -> [(TyCon, [Type])] 760tcTyFamInsts = map (\(_,b,c) -> (b,c)) . tcTyFamInstsAndVis 761 762-- | Like 'tcTyFamInsts', except that the output records whether the 763-- type family and its arguments occur as an /invisible/ argument in 764-- some type application. This information is useful because it helps GHC know 765-- when to turn on @-fprint-explicit-kinds@ during error reporting so that 766-- users can actually see the type family being mentioned. 767-- 768-- As an example, consider: 769-- 770-- @ 771-- class C a 772-- data T (a :: k) 773-- type family F a :: k 774-- instance C (T @(F Int) (F Bool)) 775-- @ 776-- 777-- There are two occurrences of the type family `F` in that `C` instance, so 778-- @'tcTyFamInstsAndVis' (C (T \@(F Int) (F Bool)))@ will return: 779-- 780-- @ 781-- [ ('True', F, [Int]) 782-- , ('False', F, [Bool]) ] 783-- @ 784-- 785-- @F Int@ is paired with 'True' since it appears as an /invisible/ argument 786-- to @C@, whereas @F Bool@ is paired with 'False' since it appears an a 787-- /visible/ argument to @C@. 788-- 789-- See also @Note [Kind arguments in error messages]@ in "TcErrors". 790tcTyFamInstsAndVis :: Type -> [(Bool, TyCon, [Type])] 791tcTyFamInstsAndVis = tcTyFamInstsAndVisX False 792 793tcTyFamInstsAndVisX 794 :: Bool -- ^ Is this an invisible argument to some type application? 795 -> Type -> [(Bool, TyCon, [Type])] 796tcTyFamInstsAndVisX = go 797 where 798 go is_invis_arg ty 799 | Just exp_ty <- tcView ty = go is_invis_arg exp_ty 800 go _ (TyVarTy _) = [] 801 go is_invis_arg (TyConApp tc tys) 802 | isTypeFamilyTyCon tc 803 = [(is_invis_arg, tc, take (tyConArity tc) tys)] 804 | otherwise 805 = tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys 806 go _ (LitTy {}) = [] 807 go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr) 808 ++ go is_invis_arg ty 809 go is_invis_arg (FunTy _ ty1 ty2) = go is_invis_arg ty1 810 ++ go is_invis_arg ty2 811 go is_invis_arg ty@(AppTy _ _) = 812 let (ty_head, ty_args) = splitAppTys ty 813 ty_arg_flags = appTyArgFlags ty_head ty_args 814 in go is_invis_arg ty_head 815 ++ concat (zipWith (\flag -> go (isInvisibleArgFlag flag)) 816 ty_arg_flags ty_args) 817 go is_invis_arg (CastTy ty _) = go is_invis_arg ty 818 go _ (CoercionTy _) = [] -- don't count tyfams in coercions, 819 -- as they never get normalized, 820 -- anyway 821 822-- | In an application of a 'TyCon' to some arguments, find the outermost 823-- occurrences of type family applications within the arguments. This function 824-- will not consider the 'TyCon' itself when checking for type family 825-- applications. 826-- 827-- See 'tcTyFamInstsAndVis' for more details on how this works (as this 828-- function is called inside of 'tcTyFamInstsAndVis'). 829tcTyConAppTyFamInstsAndVis :: TyCon -> [Type] -> [(Bool, TyCon, [Type])] 830tcTyConAppTyFamInstsAndVis = tcTyConAppTyFamInstsAndVisX False 831 832tcTyConAppTyFamInstsAndVisX 833 :: Bool -- ^ Is this an invisible argument to some type application? 834 -> TyCon -> [Type] -> [(Bool, TyCon, [Type])] 835tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys = 836 let (invis_tys, vis_tys) = partitionInvisibleTypes tc tys 837 in concat $ map (tcTyFamInstsAndVisX True) invis_tys 838 ++ map (tcTyFamInstsAndVisX is_invis_arg) vis_tys 839 840isTyFamFree :: Type -> Bool 841-- ^ Check that a type does not contain any type family applications. 842isTyFamFree = null . tcTyFamInsts 843 844anyRewritableTyVar :: Bool -- Ignore casts and coercions 845 -> EqRel -- Ambient role 846 -> (EqRel -> TcTyVar -> Bool) 847 -> TcType -> Bool 848-- (anyRewritableTyVar ignore_cos pred ty) returns True 849-- if the 'pred' returns True of any free TyVar in 'ty' 850-- Do not look inside casts and coercions if 'ignore_cos' is True 851-- See Note [anyRewritableTyVar must be role-aware] 852anyRewritableTyVar ignore_cos role pred ty 853 = go role emptyVarSet ty 854 where 855 go_tv rl bvs tv | tv `elemVarSet` bvs = False 856 | otherwise = pred rl tv 857 858 go rl bvs (TyVarTy tv) = go_tv rl bvs tv 859 go _ _ (LitTy {}) = False 860 go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys 861 go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg 862 go rl bvs (FunTy _ arg res) = go rl bvs arg || go rl bvs res 863 go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty 864 go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co 865 go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check 866 867 go_tc NomEq bvs _ tys = any (go NomEq bvs) tys 868 go_tc ReprEq bvs tc tys = any (go_arg bvs) 869 (tyConRolesRepresentational tc `zip` tys) 870 871 go_arg bvs (Nominal, ty) = go NomEq bvs ty 872 go_arg bvs (Representational, ty) = go ReprEq bvs ty 873 go_arg _ (Phantom, _) = False -- We never rewrite with phantoms 874 875 go_co rl bvs co 876 | ignore_cos = False 877 | otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co) 878 -- We don't have an equivalent of anyRewritableTyVar for coercions 879 -- (at least not yet) so take the free vars and test them 880 881{- Note [anyRewritableTyVar must be role-aware] 882~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 883anyRewritableTyVar is used during kick-out from the inert set, 884to decide if, given a new equality (a ~ ty), we should kick out 885a constraint C. Rather than gather free variables and see if 'a' 886is among them, we instead pass in a predicate; this is just efficiency. 887 888Moreover, consider 889 work item: [G] a ~R f b 890 inert item: [G] b ~R f a 891We use anyRewritableTyVar to decide whether to kick out the inert item, 892on the grounds that the work item might rewrite it. Well, 'a' is certainly 893free in [G] b ~R f a. But because the role of a type variable ('f' in 894this case) is nominal, the work item can't actually rewrite the inert item. 895Moreover, if we were to kick out the inert item the exact same situation 896would re-occur and we end up with an infinite loop in which each kicks 897out the other (#14363). 898-} 899 900{- 901************************************************************************ 902* * 903 Predicates 904* * 905************************************************************************ 906-} 907 908tcIsTcTyVar :: TcTyVar -> Bool 909-- See Note [TcTyVars and TyVars in the typechecker] 910tcIsTcTyVar tv = isTyVar tv 911 912isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool 913isTouchableMetaTyVar ctxt_tclvl tv 914 | isTyVar tv -- See Note [Coercion variables in free variable lists] 915 , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv 916 , not (isFlattenInfo info) 917 = ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl, 918 ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl ) 919 tv_tclvl `sameDepthAs` ctxt_tclvl 920 921 | otherwise = False 922 923isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool 924isFloatedTouchableMetaTyVar ctxt_tclvl tv 925 | isTyVar tv -- See Note [Coercion variables in free variable lists] 926 , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv 927 , not (isFlattenInfo info) 928 = tv_tclvl `strictlyDeeperThan` ctxt_tclvl 929 930 | otherwise = False 931 932isImmutableTyVar :: TyVar -> Bool 933isImmutableTyVar tv = isSkolemTyVar tv 934 935isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar, 936 isMetaTyVar, isAmbiguousTyVar, 937 isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar -> Bool 938 939isTyConableTyVar tv 940 -- True of a meta-type variable that can be filled in 941 -- with a type constructor application; in particular, 942 -- not a TyVarTv 943 | isTyVar tv -- See Note [Coercion variables in free variable lists] 944 = case tcTyVarDetails tv of 945 MetaTv { mtv_info = TyVarTv } -> False 946 _ -> True 947 | otherwise = True 948 949isFmvTyVar tv 950 = ASSERT2( tcIsTcTyVar tv, ppr tv ) 951 case tcTyVarDetails tv of 952 MetaTv { mtv_info = FlatMetaTv } -> True 953 _ -> False 954 955isFskTyVar tv 956 = ASSERT2( tcIsTcTyVar tv, ppr tv ) 957 case tcTyVarDetails tv of 958 MetaTv { mtv_info = FlatSkolTv } -> True 959 _ -> False 960 961-- | True of both given and wanted flatten-skolems (fmv and fsk) 962isFlattenTyVar tv 963 = ASSERT2( tcIsTcTyVar tv, ppr tv ) 964 case tcTyVarDetails tv of 965 MetaTv { mtv_info = info } -> isFlattenInfo info 966 _ -> False 967 968isSkolemTyVar tv 969 = ASSERT2( tcIsTcTyVar tv, ppr tv ) 970 case tcTyVarDetails tv of 971 MetaTv {} -> False 972 _other -> True 973 974isOverlappableTyVar tv 975 | isTyVar tv -- See Note [Coercion variables in free variable lists] 976 = case tcTyVarDetails tv of 977 SkolemTv _ overlappable -> overlappable 978 _ -> False 979 | otherwise = False 980 981isMetaTyVar tv 982 | isTyVar tv -- See Note [Coercion variables in free variable lists] 983 = case tcTyVarDetails tv of 984 MetaTv {} -> True 985 _ -> False 986 | otherwise = False 987 988-- isAmbiguousTyVar is used only when reporting type errors 989-- It picks out variables that are unbound, namely meta 990-- type variables and the RuntimUnk variables created by 991-- RtClosureInspect.zonkRTTIType. These are "ambiguous" in 992-- the sense that they stand for an as-yet-unknown type 993isAmbiguousTyVar tv 994 | isTyVar tv -- See Note [Coercion variables in free variable lists] 995 = case tcTyVarDetails tv of 996 MetaTv {} -> True 997 RuntimeUnk {} -> True 998 _ -> False 999 | otherwise = False 1000 1001isMetaTyVarTy :: TcType -> Bool 1002isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv 1003isMetaTyVarTy _ = False 1004 1005metaTyVarInfo :: TcTyVar -> MetaInfo 1006metaTyVarInfo tv 1007 = case tcTyVarDetails tv of 1008 MetaTv { mtv_info = info } -> info 1009 _ -> pprPanic "metaTyVarInfo" (ppr tv) 1010 1011isFlattenInfo :: MetaInfo -> Bool 1012isFlattenInfo FlatMetaTv = True 1013isFlattenInfo FlatSkolTv = True 1014isFlattenInfo _ = False 1015 1016metaTyVarTcLevel :: TcTyVar -> TcLevel 1017metaTyVarTcLevel tv 1018 = case tcTyVarDetails tv of 1019 MetaTv { mtv_tclvl = tclvl } -> tclvl 1020 _ -> pprPanic "metaTyVarTcLevel" (ppr tv) 1021 1022metaTyVarTcLevel_maybe :: TcTyVar -> Maybe TcLevel 1023metaTyVarTcLevel_maybe tv 1024 = case tcTyVarDetails tv of 1025 MetaTv { mtv_tclvl = tclvl } -> Just tclvl 1026 _ -> Nothing 1027 1028metaTyVarRef :: TyVar -> IORef MetaDetails 1029metaTyVarRef tv 1030 = case tcTyVarDetails tv of 1031 MetaTv { mtv_ref = ref } -> ref 1032 _ -> pprPanic "metaTyVarRef" (ppr tv) 1033 1034setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar 1035setMetaTyVarTcLevel tv tclvl 1036 = case tcTyVarDetails tv of 1037 details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl }) 1038 _ -> pprPanic "metaTyVarTcLevel" (ppr tv) 1039 1040isTyVarTyVar :: Var -> Bool 1041isTyVarTyVar tv 1042 = case tcTyVarDetails tv of 1043 MetaTv { mtv_info = TyVarTv } -> True 1044 _ -> False 1045 1046isFlexi, isIndirect :: MetaDetails -> Bool 1047isFlexi Flexi = True 1048isFlexi _ = False 1049 1050isIndirect (Indirect _) = True 1051isIndirect _ = False 1052 1053isRuntimeUnkSkol :: TyVar -> Bool 1054-- Called only in TcErrors; see Note [Runtime skolems] there 1055isRuntimeUnkSkol x 1056 | RuntimeUnk <- tcTyVarDetails x = True 1057 | otherwise = False 1058 1059mkTyVarNamePairs :: [TyVar] -> [(Name,TyVar)] 1060-- Just pair each TyVar with its own name 1061mkTyVarNamePairs tvs = [(tyVarName tv, tv) | tv <- tvs] 1062 1063findDupTyVarTvs :: [(Name,TcTyVar)] -> [(Name,Name)] 1064-- If we have [...(x1,tv)...(x2,tv)...] 1065-- return (x1,x2) in the result list 1066findDupTyVarTvs prs 1067 = concatMap mk_result_prs $ 1068 findDupsEq eq_snd prs 1069 where 1070 eq_snd (_,tv1) (_,tv2) = tv1 == tv2 1071 mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs 1072 1073{- 1074************************************************************************ 1075* * 1076\subsection{Tau, sigma and rho} 1077* * 1078************************************************************************ 1079-} 1080 1081mkSigmaTy :: [TyCoVarBinder] -> [PredType] -> Type -> Type 1082mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau) 1083 1084-- | Make a sigma ty where all type variables are 'Inferred'. That is, 1085-- they cannot be used with visible type application. 1086mkInfSigmaTy :: [TyCoVar] -> [PredType] -> Type -> Type 1087mkInfSigmaTy tyvars theta ty = mkSigmaTy (mkTyCoVarBinders Inferred tyvars) theta ty 1088 1089-- | Make a sigma ty where all type variables are "specified". That is, 1090-- they can be used with visible type application 1091mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type 1092mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyCoVarBinders Specified tyvars) preds ty 1093 1094mkPhiTy :: [PredType] -> Type -> Type 1095mkPhiTy = mkInvisFunTys 1096 1097--------------- 1098getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to 1099 -- construct a dictionary function name 1100getDFunTyKey ty | Just ty' <- coreView ty = getDFunTyKey ty' 1101getDFunTyKey (TyVarTy tv) = getOccName tv 1102getDFunTyKey (TyConApp tc _) = getOccName tc 1103getDFunTyKey (LitTy x) = getDFunTyLitKey x 1104getDFunTyKey (AppTy fun _) = getDFunTyKey fun 1105getDFunTyKey (FunTy {}) = getOccName funTyCon 1106getDFunTyKey (ForAllTy _ t) = getDFunTyKey t 1107getDFunTyKey (CastTy ty _) = getDFunTyKey ty 1108getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t) 1109 1110getDFunTyLitKey :: TyLit -> OccName 1111getDFunTyLitKey (NumTyLit n) = mkOccName Name.varName (show n) 1112getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm 1113 1114{- ********************************************************************* 1115* * 1116 Building types 1117* * 1118********************************************************************* -} 1119 1120-- ToDo: I think we need Tc versions of these 1121-- Reason: mkCastTy checks isReflexiveCastTy, which checks 1122-- for equality; and that has a different answer 1123-- depending on whether or not Type = Constraint 1124 1125mkTcAppTys :: Type -> [Type] -> Type 1126mkTcAppTys = mkAppTys 1127 1128mkTcAppTy :: Type -> Type -> Type 1129mkTcAppTy = mkAppTy 1130 1131mkTcCastTy :: Type -> Coercion -> Type 1132mkTcCastTy = mkCastTy -- Do we need a tc version of mkCastTy? 1133 1134{- 1135************************************************************************ 1136* * 1137\subsection{Expanding and splitting} 1138* * 1139************************************************************************ 1140 1141These tcSplit functions are like their non-Tc analogues, but 1142 *) they do not look through newtypes 1143 1144However, they are non-monadic and do not follow through mutable type 1145variables. It's up to you to make sure this doesn't matter. 1146-} 1147 1148-- | Splits a forall type into a list of 'TyBinder's and the inner type. 1149-- Always succeeds, even if it returns an empty list. 1150tcSplitPiTys :: Type -> ([TyBinder], Type) 1151tcSplitPiTys ty 1152 = ASSERT( all isTyBinder (fst sty) ) sty 1153 where sty = splitPiTys ty 1154 1155-- | Splits a type into a TyBinder and a body, if possible. Panics otherwise 1156tcSplitPiTy_maybe :: Type -> Maybe (TyBinder, Type) 1157tcSplitPiTy_maybe ty 1158 = ASSERT( isMaybeTyBinder sty ) sty 1159 where 1160 sty = splitPiTy_maybe ty 1161 isMaybeTyBinder (Just (t,_)) = isTyBinder t 1162 isMaybeTyBinder _ = True 1163 1164tcSplitForAllTy_maybe :: Type -> Maybe (TyVarBinder, Type) 1165tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty' 1166tcSplitForAllTy_maybe (ForAllTy tv ty) = ASSERT( isTyVarBinder tv ) Just (tv, ty) 1167tcSplitForAllTy_maybe _ = Nothing 1168 1169-- | Like 'tcSplitPiTys', but splits off only named binders, 1170-- returning just the tycovars. 1171tcSplitForAllTys :: Type -> ([TyVar], Type) 1172tcSplitForAllTys ty 1173 = ASSERT( all isTyVar (fst sty) ) sty 1174 where sty = splitForAllTys ty 1175 1176-- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if 1177-- @'sameVis' argf supplied_argf@ is 'True', where @argf@ is the visibility 1178-- of the @ForAllTy@'s binder and @supplied_argf@ is the visibility provided 1179-- as an argument to this function. 1180tcSplitForAllTysSameVis :: ArgFlag -> Type -> ([TyVar], Type) 1181tcSplitForAllTysSameVis supplied_argf ty = ASSERT( all isTyVar (fst sty) ) sty 1182 where sty = splitForAllTysSameVis supplied_argf ty 1183 1184-- | Like 'tcSplitForAllTys', but splits off only named binders. 1185tcSplitForAllVarBndrs :: Type -> ([TyVarBinder], Type) 1186tcSplitForAllVarBndrs ty = ASSERT( all isTyVarBinder (fst sty)) sty 1187 where sty = splitForAllVarBndrs ty 1188 1189-- | Is this a ForAllTy with a named binder? 1190tcIsForAllTy :: Type -> Bool 1191tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty' 1192tcIsForAllTy (ForAllTy {}) = True 1193tcIsForAllTy _ = False 1194 1195tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type) 1196-- Split off the first predicate argument from a type 1197tcSplitPredFunTy_maybe ty 1198 | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty' 1199tcSplitPredFunTy_maybe (FunTy { ft_af = InvisArg 1200 , ft_arg = arg, ft_res = res }) 1201 = Just (arg, res) 1202tcSplitPredFunTy_maybe _ 1203 = Nothing 1204 1205tcSplitPhiTy :: Type -> (ThetaType, Type) 1206tcSplitPhiTy ty 1207 = split ty [] 1208 where 1209 split ty ts 1210 = case tcSplitPredFunTy_maybe ty of 1211 Just (pred, ty) -> split ty (pred:ts) 1212 Nothing -> (reverse ts, ty) 1213 1214-- | Split a sigma type into its parts. 1215tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type) 1216tcSplitSigmaTy ty = case tcSplitForAllTys ty of 1217 (tvs, rho) -> case tcSplitPhiTy rho of 1218 (theta, tau) -> (tvs, theta, tau) 1219 1220-- | Split a sigma type into its parts, going underneath as many @ForAllTy@s 1221-- as possible. For example, given this type synonym: 1222-- 1223-- @ 1224-- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t 1225-- @ 1226-- 1227-- if you called @tcSplitSigmaTy@ on this type: 1228-- 1229-- @ 1230-- forall s t a b. Each s t a b => Traversal s t a b 1231-- @ 1232-- 1233-- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But 1234-- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return 1235-- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@. 1236tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type) 1237-- NB: This is basically a pure version of deeplyInstantiate (from Inst) that 1238-- doesn't compute an HsWrapper. 1239tcSplitNestedSigmaTys ty 1240 -- If there's a forall, split it apart and try splitting the rho type 1241 -- underneath it. 1242 | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty 1243 = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1 1244 in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2) 1245 -- If there's no forall, we're done. 1246 | otherwise = ([], [], ty) 1247 1248----------------------- 1249tcDeepSplitSigmaTy_maybe 1250 :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType) 1251-- Looks for a *non-trivial* quantified type, under zero or more function arrows 1252-- By "non-trivial" we mean either tyvars or constraints are non-empty 1253 1254tcDeepSplitSigmaTy_maybe ty 1255 | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty 1256 , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty 1257 = Just (arg_ty:arg_tys, tvs, theta, rho) 1258 1259 | (tvs, theta, rho) <- tcSplitSigmaTy ty 1260 , not (null tvs && null theta) 1261 = Just ([], tvs, theta, rho) 1262 1263 | otherwise = Nothing 1264 1265----------------------- 1266tcTyConAppTyCon :: Type -> TyCon 1267tcTyConAppTyCon ty 1268 = case tcTyConAppTyCon_maybe ty of 1269 Just tc -> tc 1270 Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty) 1271 1272-- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'. 1273tcTyConAppTyCon_maybe :: Type -> Maybe TyCon 1274tcTyConAppTyCon_maybe ty 1275 | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty' 1276tcTyConAppTyCon_maybe (TyConApp tc _) 1277 = Just tc 1278tcTyConAppTyCon_maybe (FunTy { ft_af = VisArg }) 1279 = Just funTyCon -- (=>) is /not/ a TyCon in its own right 1280 -- C.f. tcRepSplitAppTy_maybe 1281tcTyConAppTyCon_maybe _ 1282 = Nothing 1283 1284tcTyConAppArgs :: Type -> [Type] 1285tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of 1286 Just (_, args) -> args 1287 Nothing -> pprPanic "tcTyConAppArgs" (pprType ty) 1288 1289tcSplitTyConApp :: Type -> (TyCon, [Type]) 1290tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of 1291 Just stuff -> stuff 1292 Nothing -> pprPanic "tcSplitTyConApp" (pprType ty) 1293 1294----------------------- 1295tcSplitFunTys :: Type -> ([Type], Type) 1296tcSplitFunTys ty = case tcSplitFunTy_maybe ty of 1297 Nothing -> ([], ty) 1298 Just (arg,res) -> (arg:args, res') 1299 where 1300 (args,res') = tcSplitFunTys res 1301 1302tcSplitFunTy_maybe :: Type -> Maybe (Type, Type) 1303tcSplitFunTy_maybe ty 1304 | Just ty' <- tcView ty = tcSplitFunTy_maybe ty' 1305tcSplitFunTy_maybe (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) 1306 | VisArg <- af = Just (arg, res) 1307tcSplitFunTy_maybe _ = Nothing 1308 -- Note the VisArg guard 1309 -- Consider (?x::Int) => Bool 1310 -- We don't want to treat this as a function type! 1311 -- A concrete example is test tc230: 1312 -- f :: () -> (?p :: ()) => () -> () 1313 -- 1314 -- g = f () () 1315 1316tcSplitFunTysN :: Arity -- n: Number of desired args 1317 -> TcRhoType 1318 -> Either Arity -- Number of missing arrows 1319 ([TcSigmaType], -- Arg types (always N types) 1320 TcSigmaType) -- The rest of the type 1321-- ^ Split off exactly the specified number argument types 1322-- Returns 1323-- (Left m) if there are 'm' missing arrows in the type 1324-- (Right (tys,res)) if the type looks like t1 -> ... -> tn -> res 1325tcSplitFunTysN n ty 1326 | n == 0 1327 = Right ([], ty) 1328 | Just (arg,res) <- tcSplitFunTy_maybe ty 1329 = case tcSplitFunTysN (n-1) res of 1330 Left m -> Left m 1331 Right (args,body) -> Right (arg:args, body) 1332 | otherwise 1333 = Left n 1334 1335tcSplitFunTy :: Type -> (Type, Type) 1336tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty) 1337 1338tcFunArgTy :: Type -> Type 1339tcFunArgTy ty = fst (tcSplitFunTy ty) 1340 1341tcFunResultTy :: Type -> Type 1342tcFunResultTy ty = snd (tcSplitFunTy ty) 1343 1344-- | Strips off n *visible* arguments and returns the resulting type 1345tcFunResultTyN :: HasDebugCallStack => Arity -> Type -> Type 1346tcFunResultTyN n ty 1347 | Right (_, res_ty) <- tcSplitFunTysN n ty 1348 = res_ty 1349 | otherwise 1350 = pprPanic "tcFunResultTyN" (ppr n <+> ppr ty) 1351 1352----------------------- 1353tcSplitAppTy_maybe :: Type -> Maybe (Type, Type) 1354tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty' 1355tcSplitAppTy_maybe ty = tcRepSplitAppTy_maybe ty 1356 1357tcSplitAppTy :: Type -> (Type, Type) 1358tcSplitAppTy ty = case tcSplitAppTy_maybe ty of 1359 Just stuff -> stuff 1360 Nothing -> pprPanic "tcSplitAppTy" (pprType ty) 1361 1362tcSplitAppTys :: Type -> (Type, [Type]) 1363tcSplitAppTys ty 1364 = go ty [] 1365 where 1366 go ty args = case tcSplitAppTy_maybe ty of 1367 Just (ty', arg) -> go ty' (arg:args) 1368 Nothing -> (ty,args) 1369 1370-- | Returns the number of arguments in the given type, without 1371-- looking through synonyms. This is used only for error reporting. 1372-- We don't look through synonyms because of #11313. 1373tcRepGetNumAppTys :: Type -> Arity 1374tcRepGetNumAppTys = length . snd . repSplitAppTys 1375 1376----------------------- 1377-- | If the type is a tyvar, possibly under a cast, returns it, along 1378-- with the coercion. Thus, the co is :: kind tv ~N kind type 1379tcGetCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN) 1380tcGetCastedTyVar_maybe ty | Just ty' <- tcView ty = tcGetCastedTyVar_maybe ty' 1381tcGetCastedTyVar_maybe (CastTy (TyVarTy tv) co) = Just (tv, co) 1382tcGetCastedTyVar_maybe (TyVarTy tv) = Just (tv, mkNomReflCo (tyVarKind tv)) 1383tcGetCastedTyVar_maybe _ = Nothing 1384 1385tcGetTyVar_maybe :: Type -> Maybe TyVar 1386tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty' 1387tcGetTyVar_maybe (TyVarTy tv) = Just tv 1388tcGetTyVar_maybe _ = Nothing 1389 1390tcGetTyVar :: String -> Type -> TyVar 1391tcGetTyVar msg ty 1392 = case tcGetTyVar_maybe ty of 1393 Just tv -> tv 1394 Nothing -> pprPanic msg (ppr ty) 1395 1396tcIsTyVarTy :: Type -> Bool 1397tcIsTyVarTy ty | Just ty' <- tcView ty = tcIsTyVarTy ty' 1398tcIsTyVarTy (CastTy ty _) = tcIsTyVarTy ty -- look through casts, as 1399 -- this is only used for 1400 -- e.g., FlexibleContexts 1401tcIsTyVarTy (TyVarTy _) = True 1402tcIsTyVarTy _ = False 1403 1404----------------------- 1405tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type]) 1406-- Split the type of a dictionary function 1407-- We don't use tcSplitSigmaTy, because a DFun may (with NDP) 1408-- have non-Pred arguments, such as 1409-- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m 1410-- 1411-- Also NB splitFunTys, not tcSplitFunTys; 1412-- the latter specifically stops at PredTy arguments, 1413-- and we don't want to do that here 1414tcSplitDFunTy ty 1415 = case tcSplitForAllTys ty of { (tvs, rho) -> 1416 case splitFunTys rho of { (theta, tau) -> 1417 case tcSplitDFunHead tau of { (clas, tys) -> 1418 (tvs, theta, clas, tys) }}} 1419 1420tcSplitDFunHead :: Type -> (Class, [Type]) 1421tcSplitDFunHead = getClassPredTys 1422 1423tcSplitMethodTy :: Type -> ([TyVar], PredType, Type) 1424-- A class method (selector) always has a type like 1425-- forall as. C as => blah 1426-- So if the class looks like 1427-- class C a where 1428-- op :: forall b. (Eq a, Ix b) => a -> b 1429-- the class method type looks like 1430-- op :: forall a. C a => forall b. (Eq a, Ix b) => a -> b 1431-- 1432-- tcSplitMethodTy just peels off the outer forall and 1433-- that first predicate 1434tcSplitMethodTy ty 1435 | (sel_tyvars,sel_rho) <- tcSplitForAllTys ty 1436 , Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho 1437 = (sel_tyvars, first_pred, local_meth_ty) 1438 | otherwise 1439 = pprPanic "tcSplitMethodTy" (ppr ty) 1440 1441 1442{- ********************************************************************* 1443* * 1444 Type equalities 1445* * 1446********************************************************************* -} 1447 1448tcEqKind :: HasDebugCallStack => TcKind -> TcKind -> Bool 1449tcEqKind = tcEqType 1450 1451tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool 1452-- tcEqType is a proper implements the same Note [Non-trivial definitional 1453-- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* == 1454-- Constraint), and that is NOT what we want in the type checker! 1455tcEqType ty1 ty2 1456 = tc_eq_type False False ki1 ki2 1457 && tc_eq_type False False ty1 ty2 1458 where 1459 ki1 = tcTypeKind ty1 1460 ki2 = tcTypeKind ty2 1461 1462-- | Just like 'tcEqType', but will return True for types of different kinds 1463-- as long as their non-coercion structure is identical. 1464tcEqTypeNoKindCheck :: TcType -> TcType -> Bool 1465tcEqTypeNoKindCheck ty1 ty2 1466 = tc_eq_type False False ty1 ty2 1467 1468-- | Like 'tcEqType', but returns True if the /visible/ part of the types 1469-- are equal, even if they are really unequal (in the invisible bits) 1470tcEqTypeVis :: TcType -> TcType -> Bool 1471tcEqTypeVis ty1 ty2 = tc_eq_type False True ty1 ty2 1472 1473-- | Like 'pickyEqTypeVis', but returns a Bool for convenience 1474pickyEqType :: TcType -> TcType -> Bool 1475-- Check when two types _look_ the same, _including_ synonyms. 1476-- So (pickyEqType String [Char]) returns False 1477-- This ignores kinds and coercions, because this is used only for printing. 1478pickyEqType ty1 ty2 = tc_eq_type True False ty1 ty2 1479 1480 1481 1482-- | Real worker for 'tcEqType'. No kind check! 1483tc_eq_type :: Bool -- ^ True <=> do not expand type synonyms 1484 -> Bool -- ^ True <=> compare visible args only 1485 -> Type -> Type 1486 -> Bool 1487-- Flags False, False is the usual setting for tc_eq_type 1488tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 1489 = go orig_env orig_ty1 orig_ty2 1490 where 1491 go :: RnEnv2 -> Type -> Type -> Bool 1492 go env t1 t2 | not keep_syns, Just t1' <- tcView t1 = go env t1' t2 1493 go env t1 t2 | not keep_syns, Just t2' <- tcView t2 = go env t1 t2' 1494 1495 go env (TyVarTy tv1) (TyVarTy tv2) 1496 = rnOccL env tv1 == rnOccR env tv2 1497 1498 go _ (LitTy lit1) (LitTy lit2) 1499 = lit1 == lit2 1500 1501 go env (ForAllTy (Bndr tv1 vis1) ty1) 1502 (ForAllTy (Bndr tv2 vis2) ty2) 1503 = vis1 == vis2 1504 && (vis_only || go env (varType tv1) (varType tv2)) 1505 && go (rnBndr2 env tv1 tv2) ty1 ty2 1506 1507 -- Make sure we handle all FunTy cases since falling through to the 1508 -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked 1509 -- kind variable, which causes things to blow up. 1510 go env (FunTy _ arg1 res1) (FunTy _ arg2 res2) 1511 = go env arg1 arg2 && go env res1 res2 1512 go env ty (FunTy _ arg res) = eqFunTy env arg res ty 1513 go env (FunTy _ arg res) ty = eqFunTy env arg res ty 1514 1515 -- See Note [Equality on AppTys] in Type 1516 go env (AppTy s1 t1) ty2 1517 | Just (s2, t2) <- tcRepSplitAppTy_maybe ty2 1518 = go env s1 s2 && go env t1 t2 1519 go env ty1 (AppTy s2 t2) 1520 | Just (s1, t1) <- tcRepSplitAppTy_maybe ty1 1521 = go env s1 s2 && go env t1 t2 1522 1523 go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) 1524 = tc1 == tc2 && gos env (tc_vis tc1) ts1 ts2 1525 1526 go env (CastTy t1 _) t2 = go env t1 t2 1527 go env t1 (CastTy t2 _) = go env t1 t2 1528 go _ (CoercionTy {}) (CoercionTy {}) = True 1529 1530 go _ _ _ = False 1531 1532 gos _ _ [] [] = True 1533 gos env (ig:igs) (t1:ts1) (t2:ts2) = (ig || go env t1 t2) 1534 && gos env igs ts1 ts2 1535 gos _ _ _ _ = False 1536 1537 tc_vis :: TyCon -> [Bool] -- True for the fields we should ignore 1538 tc_vis tc | vis_only = inviss ++ repeat False -- Ignore invisibles 1539 | otherwise = repeat False -- Ignore nothing 1540 -- The repeat False is necessary because tycons 1541 -- can legitimately be oversaturated 1542 where 1543 bndrs = tyConBinders tc 1544 inviss = map isInvisibleTyConBinder bndrs 1545 1546 orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2] 1547 1548 -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is 1549 -- sometimes hard to know directly because @ty@ might have some casts 1550 -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't 1551 -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or 1552 -- res is unzonked/unflattened. Thus this function, which handles this 1553 -- corner case. 1554 eqFunTy :: RnEnv2 -> Type -> Type -> Type -> Bool 1555 -- Last arg is /not/ FunTy 1556 eqFunTy env arg res ty@(AppTy{}) = get_args ty [] 1557 where 1558 get_args :: Type -> [Type] -> Bool 1559 get_args (AppTy f x) args = get_args f (x:args) 1560 get_args (CastTy t _) args = get_args t args 1561 get_args (TyConApp tc tys) args 1562 | tc == funTyCon 1563 , [_, _, arg', res'] <- tys ++ args 1564 = go env arg arg' && go env res res' 1565 get_args _ _ = False 1566 eqFunTy _ _ _ _ = False 1567 1568{- ********************************************************************* 1569* * 1570 Predicate types 1571* * 1572************************************************************************ 1573 1574Deconstructors and tests on predicate types 1575 1576Note [Kind polymorphic type classes] 1577~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1578 class C f where... -- C :: forall k. k -> Constraint 1579 g :: forall (f::*). C f => f -> f 1580 1581Here the (C f) in the signature is really (C * f), and we 1582don't want to complain that the * isn't a type variable! 1583-} 1584 1585isTyVarClassPred :: PredType -> Bool 1586isTyVarClassPred ty = case getClassPredTys_maybe ty of 1587 Just (_, tys) -> all isTyVarTy tys 1588 _ -> False 1589 1590------------------------- 1591checkValidClsArgs :: Bool -> Class -> [KindOrType] -> Bool 1592-- If the Bool is True (flexible contexts), return True (i.e. ok) 1593-- Otherwise, check that the type (not kind) args are all headed by a tyvar 1594-- E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected 1595-- This function is here rather than in TcValidity because it is 1596-- called from TcSimplify, which itself is imported by TcValidity 1597checkValidClsArgs flexible_contexts cls kts 1598 | flexible_contexts = True 1599 | otherwise = all hasTyVarHead tys 1600 where 1601 tys = filterOutInvisibleTypes (classTyCon cls) kts 1602 1603hasTyVarHead :: Type -> Bool 1604-- Returns true of (a t1 .. tn), where 'a' is a type variable 1605hasTyVarHead ty -- Haskell 98 allows predicates of form 1606 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn) 1607 | otherwise -- where a is a type variable 1608 = case tcSplitAppTy_maybe ty of 1609 Just (ty, _) -> hasTyVarHead ty 1610 Nothing -> False 1611 1612evVarPred :: EvVar -> PredType 1613evVarPred var = varType var 1614 -- Historical note: I used to have an ASSERT here, 1615 -- checking (isEvVarType (varType var)). But with something like 1616 -- f :: c => _ -> _ 1617 -- we end up with (c :: kappa), and (kappa ~ Constraint). Until 1618 -- we solve and zonk (which there is no particular reason to do for 1619 -- partial signatures, (isEvVarType kappa) will return False. But 1620 -- nothing is wrong. So I just removed the ASSERT. 1621 1622------------------ 1623-- | When inferring types, should we quantify over a given predicate? 1624-- Generally true of classes; generally false of equality constraints. 1625-- Equality constraints that mention quantified type variables and 1626-- implicit variables complicate the story. See Notes 1627-- [Inheriting implicit parameters] and [Quantifying over equality constraints] 1628pickQuantifiablePreds 1629 :: TyVarSet -- Quantifying over these 1630 -> TcThetaType -- Proposed constraints to quantify 1631 -> TcThetaType -- A subset that we can actually quantify 1632-- This function decides whether a particular constraint should be 1633-- quantified over, given the type variables that are being quantified 1634pickQuantifiablePreds qtvs theta 1635 = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without 1636 -- -XFlexibleContexts: see #10608, #10351 1637 -- flex_ctxt <- xoptM Opt_FlexibleContexts 1638 mapMaybe (pick_me flex_ctxt) theta 1639 where 1640 pick_me flex_ctxt pred 1641 = case classifyPredType pred of 1642 1643 ClassPred cls tys 1644 | Just {} <- isCallStackPred cls tys 1645 -- NEVER infer a CallStack constraint. Otherwise we let 1646 -- the constraints bubble up to be solved from the outer 1647 -- context, or be defaulted when we reach the top-level. 1648 -- See Note [Overview of implicit CallStacks] 1649 -> Nothing 1650 1651 | isIPClass cls 1652 -> Just pred -- See note [Inheriting implicit parameters] 1653 1654 | pick_cls_pred flex_ctxt cls tys 1655 -> Just pred 1656 1657 EqPred eq_rel ty1 ty2 1658 | quantify_equality eq_rel ty1 ty2 1659 , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2 1660 -- boxEqPred: See Note [Lift equality constaints when quantifying] 1661 , pick_cls_pred flex_ctxt cls tys 1662 -> Just (mkClassPred cls tys) 1663 1664 IrredPred ty 1665 | tyCoVarsOfType ty `intersectsVarSet` qtvs 1666 -> Just pred 1667 1668 _ -> Nothing 1669 1670 1671 pick_cls_pred flex_ctxt cls tys 1672 = tyCoVarsOfTypes tys `intersectsVarSet` qtvs 1673 && (checkValidClsArgs flex_ctxt cls tys) 1674 -- Only quantify over predicates that checkValidType 1675 -- will pass! See #10351. 1676 1677 -- See Note [Quantifying over equality constraints] 1678 quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2 1679 quantify_equality ReprEq _ _ = True 1680 1681 quant_fun ty 1682 = case tcSplitTyConApp_maybe ty of 1683 Just (tc, tys) | isTypeFamilyTyCon tc 1684 -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs 1685 _ -> False 1686 1687boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type]) 1688-- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version 1689-- (t1 ~ t2) or (t1 `Coercible` t2) 1690boxEqPred eq_rel ty1 ty2 1691 = case eq_rel of 1692 NomEq | homo_kind -> Just (eqClass, [k1, ty1, ty2]) 1693 | otherwise -> Just (heqClass, [k1, k2, ty1, ty2]) 1694 ReprEq | homo_kind -> Just (coercibleClass, [k1, ty1, ty2]) 1695 | otherwise -> Nothing -- Sigh: we do not have hererogeneous Coercible 1696 -- so we can't abstract over it 1697 -- Nothing fundamental: we could add it 1698 where 1699 k1 = tcTypeKind ty1 1700 k2 = tcTypeKind ty2 1701 homo_kind = k1 `tcEqType` k2 1702 1703pickCapturedPreds 1704 :: TyVarSet -- Quantifying over these 1705 -> TcThetaType -- Proposed constraints to quantify 1706 -> TcThetaType -- A subset that we can actually quantify 1707-- A simpler version of pickQuantifiablePreds, used to winnow down 1708-- the inferred constraints of a group of bindings, into those for 1709-- one particular identifier 1710pickCapturedPreds qtvs theta 1711 = filter captured theta 1712 where 1713 captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs) 1714 1715 1716-- Superclasses 1717 1718type PredWithSCs a = (PredType, [PredType], a) 1719 1720mkMinimalBySCs :: forall a. (a -> PredType) -> [a] -> [a] 1721-- Remove predicates that 1722-- 1723-- - are the same as another predicate 1724-- 1725-- - can be deduced from another by superclasses, 1726-- 1727-- - are a reflexive equality (e.g * ~ *) 1728-- (see Note [Remove redundant provided dicts] in TcPatSyn) 1729-- 1730-- The result is a subset of the input. 1731-- The 'a' is just paired up with the PredType; 1732-- typically it might be a dictionary Id 1733mkMinimalBySCs get_pred xs = go preds_with_scs [] 1734 where 1735 preds_with_scs :: [PredWithSCs a] 1736 preds_with_scs = [ (pred, pred : transSuperClasses pred, x) 1737 | x <- xs 1738 , let pred = get_pred x ] 1739 1740 go :: [PredWithSCs a] -- Work list 1741 -> [PredWithSCs a] -- Accumulating result 1742 -> [a] 1743 go [] min_preds 1744 = reverse (map thdOf3 min_preds) 1745 -- The 'reverse' isn't strictly necessary, but it 1746 -- means that the results are returned in the same 1747 -- order as the input, which is generally saner 1748 go (work_item@(p,_,_) : work_list) min_preds 1749 | EqPred _ t1 t2 <- classifyPredType p 1750 , t1 `tcEqType` t2 -- See TcPatSyn 1751 -- Note [Remove redundant provided dicts] 1752 = go work_list min_preds 1753 | p `in_cloud` work_list || p `in_cloud` min_preds 1754 = go work_list min_preds 1755 | otherwise 1756 = go work_list (work_item : min_preds) 1757 1758 in_cloud :: PredType -> [PredWithSCs a] -> Bool 1759 in_cloud p ps = or [ p `tcEqType` p' | (_, scs, _) <- ps, p' <- scs ] 1760 1761transSuperClasses :: PredType -> [PredType] 1762-- (transSuperClasses p) returns (p's superclasses) not including p 1763-- Stop if you encounter the same class again 1764-- See Note [Expanding superclasses] 1765transSuperClasses p 1766 = go emptyNameSet p 1767 where 1768 go :: NameSet -> PredType -> [PredType] 1769 go rec_clss p 1770 | ClassPred cls tys <- classifyPredType p 1771 , let cls_nm = className cls 1772 , not (cls_nm `elemNameSet` rec_clss) 1773 , let rec_clss' | isCTupleClass cls = rec_clss 1774 | otherwise = rec_clss `extendNameSet` cls_nm 1775 = [ p' | sc <- immSuperClasses cls tys 1776 , p' <- sc : go rec_clss' sc ] 1777 | otherwise 1778 = [] 1779 1780immSuperClasses :: Class -> [Type] -> [PredType] 1781immSuperClasses cls tys 1782 = substTheta (zipTvSubst tyvars tys) sc_theta 1783 where 1784 (tyvars,sc_theta,_,_) = classBigSig cls 1785 1786isImprovementPred :: PredType -> Bool 1787-- Either it's an equality, or has some functional dependency 1788isImprovementPred ty 1789 = case classifyPredType ty of 1790 EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2) 1791 EqPred ReprEq _ _ -> False 1792 ClassPred cls _ -> classHasFds cls 1793 IrredPred {} -> True -- Might have equalities after reduction? 1794 ForAllPred {} -> False 1795 1796-- | Is the equality 1797-- a ~r ...a.... 1798-- definitely insoluble or not? 1799-- a ~r Maybe a -- Definitely insoluble 1800-- a ~N ...(F a)... -- Not definitely insoluble 1801-- -- Perhaps (F a) reduces to Int 1802-- a ~R ...(N a)... -- Not definitely insoluble 1803-- -- Perhaps newtype N a = MkN Int 1804-- See Note [Occurs check error] in 1805-- TcCanonical for the motivation for this function. 1806isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool 1807isInsolubleOccursCheck eq_rel tv ty 1808 = go ty 1809 where 1810 go ty | Just ty' <- tcView ty = go ty' 1811 go (TyVarTy tv') = tv == tv' || go (tyVarKind tv') 1812 go (LitTy {}) = False 1813 go (AppTy t1 t2) = case eq_rel of -- See Note [AppTy and ReprEq] 1814 NomEq -> go t1 || go t2 1815 ReprEq -> go t1 1816 go (FunTy _ t1 t2) = go t1 || go t2 1817 go (ForAllTy (Bndr tv' _) inner_ty) 1818 | tv' == tv = False 1819 | otherwise = go (varType tv') || go inner_ty 1820 go (CastTy ty _) = go ty -- ToDo: what about the coercion 1821 go (CoercionTy _) = False -- ToDo: what about the coercion 1822 go (TyConApp tc tys) 1823 | isGenerativeTyCon tc role = any go tys 1824 | otherwise = any go (drop (tyConArity tc) tys) 1825 -- (a ~ F b a), where F has arity 1, 1826 -- has an insoluble occurs check 1827 1828 role = eqRelRole eq_rel 1829 1830{- Note [Expanding superclasses] 1831~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1832When we expand superclasses, we use the following algorithm: 1833 1834transSuperClasses( C tys ) returns the transitive superclasses 1835 of (C tys), not including C itself 1836 1837For example 1838 class C a b => D a b 1839 class D b a => C a b 1840 1841Then 1842 transSuperClasses( Ord ty ) = [Eq ty] 1843 transSuperClasses( C ta tb ) = [D tb ta, C tb ta] 1844 1845Notice that in the recursive-superclass case we include C again at 1846the end of the chain. One could exclude C in this case, but 1847the code is more awkward and there seems no good reason to do so. 1848(However C.f. TcCanonical.mk_strict_superclasses, which /does/ 1849appear to do so.) 1850 1851The algorithm is expand( so_far, pred ): 1852 1853 1. If pred is not a class constraint, return empty set 1854 Otherwise pred = C ts 1855 2. If C is in so_far, return empty set (breaks loops) 1856 3. Find the immediate superclasses constraints of (C ts) 1857 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss ) 1858 1859Notice that 1860 1861 * With normal Haskell-98 classes, the loop-detector will never bite, 1862 so we'll get all the superclasses. 1863 1864 * We need the loop-breaker in case we have UndecidableSuperClasses on 1865 1866 * Since there is only a finite number of distinct classes, expansion 1867 must terminate. 1868 1869 * The loop breaking is a bit conservative. Notably, a tuple class 1870 could contain many times without threatening termination: 1871 (Eq a, (Ord a, Ix a)) 1872 And this is try of any class that we can statically guarantee 1873 as non-recursive (in some sense). For now, we just make a special 1874 case for tuples. Something better would be cool. 1875 1876See also TcTyDecls.checkClassCycles. 1877 1878Note [Lift equality constaints when quantifying] 1879~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1880We can't quantify over a constraint (t1 ~# t2) because that isn't a 1881predicate type; see Note [Types for coercions, predicates, and evidence] 1882in TyCoRep. 1883 1884So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted 1885to Coercible. 1886 1887This tiresome lifting is the reason that pick_me (in 1888pickQuantifiablePreds) returns a Maybe rather than a Bool. 1889 1890Note [Quantifying over equality constraints] 1891~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1892Should we quantify over an equality constraint (s ~ t)? In general, we don't. 1893Doing so may simply postpone a type error from the function definition site to 1894its call site. (At worst, imagine (Int ~ Bool)). 1895 1896However, consider this 1897 forall a. (F [a] ~ Int) => blah 1898Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call 1899site we will know 'a', and perhaps we have instance F [Bool] = Int. 1900So we *do* quantify over a type-family equality where the arguments mention 1901the quantified variables. 1902 1903Note [Inheriting implicit parameters] 1904~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1905Consider this: 1906 1907 f x = (x::Int) + ?y 1908 1909where f is *not* a top-level binding. 1910From the RHS of f we'll get the constraint (?y::Int). 1911There are two types we might infer for f: 1912 1913 f :: Int -> Int 1914 1915(so we get ?y from the context of f's definition), or 1916 1917 f :: (?y::Int) => Int -> Int 1918 1919At first you might think the first was better, because then 1920?y behaves like a free variable of the definition, rather than 1921having to be passed at each call site. But of course, the WHOLE 1922IDEA is that ?y should be passed at each call site (that's what 1923dynamic binding means) so we'd better infer the second. 1924 1925BOTTOM LINE: when *inferring types* you must quantify over implicit 1926parameters, *even if* they don't mention the bound type variables. 1927Reason: because implicit parameters, uniquely, have local instance 1928declarations. See pickQuantifiablePreds. 1929 1930Note [Quantifying over equality constraints] 1931~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1932Should we quantify over an equality constraint (s ~ t)? In general, we don't. 1933Doing so may simply postpone a type error from the function definition site to 1934its call site. (At worst, imagine (Int ~ Bool)). 1935 1936However, consider this 1937 forall a. (F [a] ~ Int) => blah 1938Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call 1939site we will know 'a', and perhaps we have instance F [Bool] = Int. 1940So we *do* quantify over a type-family equality where the arguments mention 1941the quantified variables. 1942 1943************************************************************************ 1944* * 1945 Classifying types 1946* * 1947************************************************************************ 1948-} 1949 1950isSigmaTy :: TcType -> Bool 1951-- isSigmaTy returns true of any qualified type. It doesn't 1952-- *necessarily* have any foralls. E.g 1953-- f :: (?x::Int) => Int -> Int 1954isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty' 1955isSigmaTy (ForAllTy {}) = True 1956isSigmaTy (FunTy { ft_af = InvisArg }) = True 1957isSigmaTy _ = False 1958 1959isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType] 1960isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty' 1961isRhoTy (ForAllTy {}) = False 1962isRhoTy (FunTy { ft_af = VisArg, ft_res = r }) = isRhoTy r 1963isRhoTy _ = True 1964 1965-- | Like 'isRhoTy', but also says 'True' for 'Infer' types 1966isRhoExpTy :: ExpType -> Bool 1967isRhoExpTy (Check ty) = isRhoTy ty 1968isRhoExpTy (Infer {}) = True 1969 1970isOverloadedTy :: Type -> Bool 1971-- Yes for a type of a function that might require evidence-passing 1972-- Used only by bindLocalMethods 1973isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty' 1974isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty 1975isOverloadedTy (FunTy { ft_af = InvisArg }) = True 1976isOverloadedTy _ = False 1977 1978isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy, 1979 isUnitTy, isCharTy, isAnyTy :: Type -> Bool 1980isFloatTy = is_tc floatTyConKey 1981isDoubleTy = is_tc doubleTyConKey 1982isIntegerTy = is_tc integerTyConKey 1983isIntTy = is_tc intTyConKey 1984isWordTy = is_tc wordTyConKey 1985isBoolTy = is_tc boolTyConKey 1986isUnitTy = is_tc unitTyConKey 1987isCharTy = is_tc charTyConKey 1988isAnyTy = is_tc anyTyConKey 1989 1990-- | Does a type represent a floating-point number? 1991isFloatingTy :: Type -> Bool 1992isFloatingTy ty = isFloatTy ty || isDoubleTy ty 1993 1994-- | Is a type 'String'? 1995isStringTy :: Type -> Bool 1996isStringTy ty 1997 = case tcSplitTyConApp_maybe ty of 1998 Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty 1999 _ -> False 2000 2001-- | Is a type a 'CallStack'? 2002isCallStackTy :: Type -> Bool 2003isCallStackTy ty 2004 | Just tc <- tyConAppTyCon_maybe ty 2005 = tc `hasKey` callStackTyConKey 2006 | otherwise 2007 = False 2008 2009-- | Is a 'PredType' a 'CallStack' implicit parameter? 2010-- 2011-- If so, return the name of the parameter. 2012isCallStackPred :: Class -> [Type] -> Maybe FastString 2013isCallStackPred cls tys 2014 | [ty1, ty2] <- tys 2015 , isIPClass cls 2016 , isCallStackTy ty2 2017 = isStrLitTy ty1 2018 | otherwise 2019 = Nothing 2020 2021is_tc :: Unique -> Type -> Bool 2022-- Newtypes are opaque to this 2023is_tc uniq ty = case tcSplitTyConApp_maybe ty of 2024 Just (tc, _) -> uniq == getUnique tc 2025 Nothing -> False 2026 2027-- | Does the given tyvar appear at the head of a chain of applications 2028-- (a t1 ... tn) 2029isTyVarHead :: TcTyVar -> TcType -> Bool 2030isTyVarHead tv (TyVarTy tv') = tv == tv' 2031isTyVarHead tv (AppTy fun _) = isTyVarHead tv fun 2032isTyVarHead tv (CastTy ty _) = isTyVarHead tv ty 2033isTyVarHead _ (TyConApp {}) = False 2034isTyVarHead _ (LitTy {}) = False 2035isTyVarHead _ (ForAllTy {}) = False 2036isTyVarHead _ (FunTy {}) = False 2037isTyVarHead _ (CoercionTy {}) = False 2038 2039 2040{- Note [AppTy and ReprEq] 2041~~~~~~~~~~~~~~~~~~~~~~~~~~ 2042Consider a ~R# b a 2043 a ~R# a b 2044 2045The former is /not/ a definite error; we might instantiate 'b' with Id 2046 newtype Id a = MkId a 2047but the latter /is/ a definite error. 2048 2049On the other hand, with nominal equality, both are definite errors 2050-} 2051 2052isRigidTy :: TcType -> Bool 2053isRigidTy ty 2054 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal 2055 | Just {} <- tcSplitAppTy_maybe ty = True 2056 | isForAllTy ty = True 2057 | otherwise = False 2058 2059 2060-- | Is this type *almost function-free*? See Note [Almost function-free] 2061-- in TcRnTypes 2062isAlmostFunctionFree :: TcType -> Bool 2063isAlmostFunctionFree ty | Just ty' <- tcView ty = isAlmostFunctionFree ty' 2064isAlmostFunctionFree (TyVarTy {}) = True 2065isAlmostFunctionFree (AppTy ty1 ty2) = isAlmostFunctionFree ty1 && 2066 isAlmostFunctionFree ty2 2067isAlmostFunctionFree (TyConApp tc args) 2068 | isTypeFamilyTyCon tc = False 2069 | otherwise = all isAlmostFunctionFree args 2070isAlmostFunctionFree (ForAllTy bndr _) = isAlmostFunctionFree (binderType bndr) 2071isAlmostFunctionFree (FunTy _ ty1 ty2) = isAlmostFunctionFree ty1 && 2072 isAlmostFunctionFree ty2 2073isAlmostFunctionFree (LitTy {}) = True 2074isAlmostFunctionFree (CastTy ty _) = isAlmostFunctionFree ty 2075isAlmostFunctionFree (CoercionTy {}) = True 2076 2077{- 2078************************************************************************ 2079* * 2080\subsection{Misc} 2081* * 2082************************************************************************ 2083 2084Note [Visible type application] 2085~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2086GHC implements a generalisation of the algorithm described in the 2087"Visible Type Application" paper (available from 2088http://www.cis.upenn.edu/~sweirich/publications.html). A key part 2089of that algorithm is to distinguish user-specified variables from inferred 2090variables. For example, the following should typecheck: 2091 2092 f :: forall a b. a -> b -> b 2093 f = const id 2094 2095 g = const id 2096 2097 x = f @Int @Bool 5 False 2098 y = g 5 @Bool False 2099 2100The idea is that we wish to allow visible type application when we are 2101instantiating a specified, fixed variable. In practice, specified, fixed 2102variables are either written in a type signature (or 2103annotation), OR are imported from another module. (We could do better here, 2104for example by doing SCC analysis on parts of a module and considering any 2105type from outside one's SCC to be fully specified, but this is very confusing to 2106users. The simple rule above is much more straightforward and predictable.) 2107 2108So, both of f's quantified variables are specified and may be instantiated. 2109But g has no type signature, so only id's variable is specified (because id 2110is imported). We write the type of g as forall {a}. a -> forall b. b -> b. 2111Note that the a is in braces, meaning it cannot be instantiated with 2112visible type application. 2113 2114Tracking specified vs. inferred variables is done conveniently by a field 2115in TyBinder. 2116 2117-} 2118 2119deNoteType :: Type -> Type 2120-- Remove all *outermost* type synonyms and other notes 2121deNoteType ty | Just ty' <- coreView ty = deNoteType ty' 2122deNoteType ty = ty 2123 2124{- 2125Find the free tycons and classes of a type. This is used in the front 2126end of the compiler. 2127-} 2128 2129{- 2130************************************************************************ 2131* * 2132\subsection[TysWiredIn-ext-type]{External types} 2133* * 2134************************************************************************ 2135 2136The compiler's foreign function interface supports the passing of a 2137restricted set of types as arguments and results (the restricting factor 2138being the ) 2139-} 2140 2141tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type) 2142-- (tcSplitIOType_maybe t) returns Just (IO,t',co) 2143-- if co : t ~ IO t' 2144-- returns Nothing otherwise 2145tcSplitIOType_maybe ty 2146 = case tcSplitTyConApp_maybe ty of 2147 Just (io_tycon, [io_res_ty]) 2148 | io_tycon `hasKey` ioTyConKey -> 2149 Just (io_tycon, io_res_ty) 2150 _ -> 2151 Nothing 2152 2153isFFITy :: Type -> Bool 2154-- True for any TyCon that can possibly be an arg or result of an FFI call 2155isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty) 2156 2157isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity 2158-- Checks for valid argument type for a 'foreign import' 2159isFFIArgumentTy dflags safety ty 2160 = checkRepTyCon (legalOutgoingTyCon dflags safety) ty 2161 2162isFFIExternalTy :: Type -> Validity 2163-- Types that are allowed as arguments of a 'foreign export' 2164isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty 2165 2166isFFIImportResultTy :: DynFlags -> Type -> Validity 2167isFFIImportResultTy dflags ty 2168 = checkRepTyCon (legalFIResultTyCon dflags) ty 2169 2170isFFIExportResultTy :: Type -> Validity 2171isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty 2172 2173isFFIDynTy :: Type -> Type -> Validity 2174-- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of 2175-- either, and the wrapped function type must be equal to the given type. 2176-- We assume that all types have been run through normaliseFfiType, so we don't 2177-- need to worry about expanding newtypes here. 2178isFFIDynTy expected ty 2179 -- Note [Foreign import dynamic] 2180 -- In the example below, expected would be 'CInt -> IO ()', while ty would 2181 -- be 'FunPtr (CDouble -> IO ())'. 2182 | Just (tc, [ty']) <- splitTyConApp_maybe ty 2183 , tyConUnique tc `elem` [ptrTyConKey, funPtrTyConKey] 2184 , eqType ty' expected 2185 = IsValid 2186 | otherwise 2187 = NotValid (vcat [ text "Expected: Ptr/FunPtr" <+> pprParendType expected <> comma 2188 , text " Actual:" <+> ppr ty ]) 2189 2190isFFILabelTy :: Type -> Validity 2191-- The type of a foreign label must be Ptr, FunPtr, or a newtype of either. 2192isFFILabelTy ty = checkRepTyCon ok ty 2193 where 2194 ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey 2195 = IsValid 2196 | otherwise 2197 = NotValid (text "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)") 2198 2199isFFIPrimArgumentTy :: DynFlags -> Type -> Validity 2200-- Checks for valid argument type for a 'foreign import prim' 2201-- Currently they must all be simple unlifted types, or the well-known type 2202-- Any, which can be used to pass the address to a Haskell object on the heap to 2203-- the foreign function. 2204isFFIPrimArgumentTy dflags ty 2205 | isAnyTy ty = IsValid 2206 | otherwise = checkRepTyCon (legalFIPrimArgTyCon dflags) ty 2207 2208isFFIPrimResultTy :: DynFlags -> Type -> Validity 2209-- Checks for valid result type for a 'foreign import prim' Currently 2210-- it must be an unlifted type, including unboxed tuples, unboxed 2211-- sums, or the well-known type Any. 2212isFFIPrimResultTy dflags ty 2213 | isAnyTy ty = IsValid 2214 | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty 2215 2216isFunPtrTy :: Type -> Bool 2217isFunPtrTy ty 2218 | Just (tc, [_]) <- splitTyConApp_maybe ty 2219 = tc `hasKey` funPtrTyConKey 2220 | otherwise 2221 = False 2222 2223-- normaliseFfiType gets run before checkRepTyCon, so we don't 2224-- need to worry about looking through newtypes or type functions 2225-- here; that's already been taken care of. 2226checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity 2227checkRepTyCon check_tc ty 2228 = case splitTyConApp_maybe ty of 2229 Just (tc, tys) 2230 | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix)) 2231 | otherwise -> case check_tc tc of 2232 IsValid -> IsValid 2233 NotValid extra -> NotValid (msg $$ extra) 2234 Nothing -> NotValid (quotes (ppr ty) <+> text "is not a data type") 2235 where 2236 msg = quotes (ppr ty) <+> text "cannot be marshalled in a foreign call" 2237 mk_nt_reason tc tys 2238 | null tys = text "because its data constructor is not in scope" 2239 | otherwise = text "because the data constructor for" 2240 <+> quotes (ppr tc) <+> text "is not in scope" 2241 nt_fix = text "Possible fix: import the data constructor to bring it into scope" 2242 2243{- 2244Note [Foreign import dynamic] 2245~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2246A dynamic stub must be of the form 'FunPtr ft -> ft' where ft is any foreign 2247type. Similarly, a wrapper stub must be of the form 'ft -> IO (FunPtr ft)'. 2248 2249We use isFFIDynTy to check whether a signature is well-formed. For example, 2250given a (illegal) declaration like: 2251 2252foreign import ccall "dynamic" 2253 foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO () 2254 2255isFFIDynTy will compare the 'FunPtr' type 'CDouble -> IO ()' with the curried 2256result type 'CInt -> IO ()', and return False, as they are not equal. 2257 2258 2259---------------------------------------------- 2260These chaps do the work; they are not exported 2261---------------------------------------------- 2262-} 2263 2264legalFEArgTyCon :: TyCon -> Validity 2265legalFEArgTyCon tc 2266 -- It's illegal to make foreign exports that take unboxed 2267 -- arguments. The RTS API currently can't invoke such things. --SDM 7/2000 2268 = boxedMarshalableTyCon tc 2269 2270legalFIResultTyCon :: DynFlags -> TyCon -> Validity 2271legalFIResultTyCon dflags tc 2272 | tc == unitTyCon = IsValid 2273 | otherwise = marshalableTyCon dflags tc 2274 2275legalFEResultTyCon :: TyCon -> Validity 2276legalFEResultTyCon tc 2277 | tc == unitTyCon = IsValid 2278 | otherwise = boxedMarshalableTyCon tc 2279 2280legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity 2281-- Checks validity of types going from Haskell -> external world 2282legalOutgoingTyCon dflags _ tc 2283 = marshalableTyCon dflags tc 2284 2285legalFFITyCon :: TyCon -> Validity 2286-- True for any TyCon that can possibly be an arg or result of an FFI call 2287legalFFITyCon tc 2288 | isUnliftedTyCon tc = IsValid 2289 | tc == unitTyCon = IsValid 2290 | otherwise = boxedMarshalableTyCon tc 2291 2292marshalableTyCon :: DynFlags -> TyCon -> Validity 2293marshalableTyCon dflags tc 2294 | isUnliftedTyCon tc 2295 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc) 2296 , not (null (tyConPrimRep tc)) -- Note [Marshalling void] 2297 = validIfUnliftedFFITypes dflags 2298 | otherwise 2299 = boxedMarshalableTyCon tc 2300 2301boxedMarshalableTyCon :: TyCon -> Validity 2302boxedMarshalableTyCon tc 2303 | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey 2304 , int32TyConKey, int64TyConKey 2305 , wordTyConKey, word8TyConKey, word16TyConKey 2306 , word32TyConKey, word64TyConKey 2307 , floatTyConKey, doubleTyConKey 2308 , ptrTyConKey, funPtrTyConKey 2309 , charTyConKey 2310 , stablePtrTyConKey 2311 , boolTyConKey 2312 ] 2313 = IsValid 2314 2315 | otherwise = NotValid empty 2316 2317legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity 2318-- Check args of 'foreign import prim', only allow simple unlifted types. 2319-- Strictly speaking it is unnecessary to ban unboxed tuples and sums here since 2320-- currently they're of the wrong kind to use in function args anyway. 2321legalFIPrimArgTyCon dflags tc 2322 | isUnliftedTyCon tc 2323 , not (isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc) 2324 = validIfUnliftedFFITypes dflags 2325 | otherwise 2326 = NotValid unlifted_only 2327 2328legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity 2329-- Check result type of 'foreign import prim'. Allow simple unlifted 2330-- types and also unboxed tuple and sum result types. 2331legalFIPrimResultTyCon dflags tc 2332 | isUnliftedTyCon tc 2333 , isUnboxedTupleTyCon tc || isUnboxedSumTyCon tc 2334 || not (null (tyConPrimRep tc)) -- Note [Marshalling void] 2335 = validIfUnliftedFFITypes dflags 2336 2337 | otherwise 2338 = NotValid unlifted_only 2339 2340unlifted_only :: MsgDoc 2341unlifted_only = text "foreign import prim only accepts simple unlifted types" 2342 2343validIfUnliftedFFITypes :: DynFlags -> Validity 2344validIfUnliftedFFITypes dflags 2345 | xopt LangExt.UnliftedFFITypes dflags = IsValid 2346 | otherwise = NotValid (text "To marshal unlifted types, use UnliftedFFITypes") 2347 2348{- 2349Note [Marshalling void] 2350~~~~~~~~~~~~~~~~~~~~~~~ 2351We don't treat State# (whose PrimRep is VoidRep) as marshalable. 2352In turn that means you can't write 2353 foreign import foo :: Int -> State# RealWorld 2354 2355Reason: the back end falls over with panic "primRepHint:VoidRep"; 2356 and there is no compelling reason to permit it 2357-} 2358 2359{- 2360************************************************************************ 2361* * 2362 The "Paterson size" of a type 2363* * 2364************************************************************************ 2365-} 2366 2367{- 2368Note [Paterson conditions on PredTypes] 2369~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2370We are considering whether *class* constraints terminate 2371(see Note [Paterson conditions]). Precisely, the Paterson conditions 2372would have us check that "the constraint has fewer constructors and variables 2373(taken together and counting repetitions) than the head.". 2374 2375However, we can be a bit more refined by looking at which kind of constraint 2376this actually is. There are two main tricks: 2377 2378 1. It seems like it should be OK not to count the tuple type constructor 2379 for a PredType like (Show a, Eq a) :: Constraint, since we don't 2380 count the "implicit" tuple in the ThetaType itself. 2381 2382 In fact, the Paterson test just checks *each component* of the top level 2383 ThetaType against the size bound, one at a time. By analogy, it should be 2384 OK to return the size of the *largest* tuple component as the size of the 2385 whole tuple. 2386 2387 2. Once we get into an implicit parameter or equality we 2388 can't get back to a class constraint, so it's safe 2389 to say "size 0". See #4200. 2390 2391NB: we don't want to detect PredTypes in sizeType (and then call 2392sizePred on them), or we might get an infinite loop if that PredType 2393is irreducible. See #5581. 2394-} 2395 2396type TypeSize = IntWithInf 2397 2398sizeType :: Type -> TypeSize 2399-- Size of a type: the number of variables and constructors 2400-- Ignore kinds altogether 2401sizeType = go 2402 where 2403 go ty | Just exp_ty <- tcView ty = go exp_ty 2404 go (TyVarTy {}) = 1 2405 go (TyConApp tc tys) 2406 | isTypeFamilyTyCon tc = infinity -- Type-family applications can 2407 -- expand to any arbitrary size 2408 | otherwise = sizeTypes (filterOutInvisibleTypes tc tys) + 1 2409 -- Why filter out invisible args? I suppose any 2410 -- size ordering is sound, but why is this better? 2411 -- I came across this when investigating #14010. 2412 go (LitTy {}) = 1 2413 go (FunTy _ arg res) = go arg + go res + 1 2414 go (AppTy fun arg) = go fun + go arg 2415 go (ForAllTy (Bndr tv vis) ty) 2416 | isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1 2417 | otherwise = go ty + 1 2418 go (CastTy ty _) = go ty 2419 go (CoercionTy {}) = 0 2420 2421sizeTypes :: [Type] -> TypeSize 2422sizeTypes tys = sum (map sizeType tys) 2423 2424----------------------------------------------------------------------------------- 2425----------------------------------------------------------------------------------- 2426----------------------- 2427-- | For every arg a tycon can take, the returned list says True if the argument 2428-- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to 2429-- allow for oversaturation. 2430tcTyConVisibilities :: TyCon -> [Bool] 2431tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True 2432 where 2433 tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc) 2434 tc_return_kind_viss = map isVisibleBinder (fst $ tcSplitPiTys (tyConResKind tc)) 2435 2436-- | If the tycon is applied to the types, is the next argument visible? 2437isNextTyConArgVisible :: TyCon -> [Type] -> Bool 2438isNextTyConArgVisible tc tys 2439 = tcTyConVisibilities tc `getNth` length tys 2440 2441-- | Should this type be applied to a visible argument? 2442isNextArgVisible :: TcType -> Bool 2443isNextArgVisible ty 2444 | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisibleBinder bndr 2445 | otherwise = True 2446 -- this second case might happen if, say, we have an unzonked TauTv. 2447 -- But TauTvs can't range over types that take invisible arguments 2448