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