    {-# LANGUAGE DerivingStrategies #-}

    {-

    Describes predicates as they are considered by the solver.

    -}

    module GHC.Core.Predicate (
      Pred(..), classifyPredType,
      isPredTy, isEvVarType,

      -- Equality predicates
      EqRel(..), eqRelRole,
      isEqPrimPred, isEqPred,
      getEqPredTys, getEqPredTys_maybe, getEqPredRole,
      predTypeEqRel,
      mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
      mkNomPrimEqPred,

      -- Class predicates
      mkClassPred, isDictTy, typeDeterminesValue,
      isClassPred, isEqualityClass, isCTupleClass,
      getClassPredTys, getClassPredTys_maybe,
      classMethodTy, classMethodInstTy,

      -- Implicit parameters
      isIPLikePred, mentionsIP, isIPTyCon, isIPClass,
      isCallStackTy, isCallStackPred, isCallStackPredTy,
      isExceptionContextPred, isExceptionContextTy,
      isIPPred_maybe,

      -- Evidence variables
      DictId, isEvVar, isDictId

      ) where

    import GHC.Prelude

    import GHC.Core.Type
    import GHC.Core.Class
    import GHC.Core.TyCon
    import GHC.Core.TyCon.RecWalk
    import GHC.Types.Var
    import GHC.Core.Coercion
    import GHC.Core.Multiplicity ( scaledThing )

    import GHC.Builtin.Names

    import GHC.Utils.Outputable
    import GHC.Utils.Misc
    import GHC.Utils.Panic
    import GHC.Data.FastString

    -- | A predicate in the solver. The solver tries to prove Wanted predicates
    -- from Given ones.
    data Pred

      -- | A typeclass predicate.
      = ClassPred Class [Type]

      -- | A type equality predicate.
      | EqPred EqRel Type Type

      -- | An irreducible predicate.
      | IrredPred PredType

      -- | A quantified predicate.
      --
      -- See Note [Quantified constraints] in GHC.Tc.Solver.Solve
      | ForAllPred [TyVar] [PredType] PredType

      -- NB: There is no TuplePred case
      --     Tuple predicates like (Eq a, Ord b) are just treated
      --     as ClassPred, as if we had a tuple class with two superclasses
      --        class (c1, c2) => CTuple2 c1 c2

    classifyPredType :: PredType -> Pred
    classifyPredType :: PredType -> Pred
    classifyPredType PredType
    ev_ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
    PredType -> Maybe (TyCon, [PredType])
    splitTyConApp_maybe PredType
    ev_ty of
        Just (TyCon
    tc, [PredType
    _, PredType
    _, PredType
    ty1, PredType
    ty2])
          | TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqReprPrimTyConKey -> EqRel -> PredType -> PredType -> Pred
    EqPred EqRel
    ReprEq PredType
    ty1 PredType
    ty2
          | TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqPrimTyConKey     -> EqRel -> PredType -> PredType -> Pred
    EqPred EqRel
    NomEq PredType
    ty1 PredType
    ty2

        Just (TyCon
    tc, [PredType]
    tys)
          | Just Class
    clas <- TyCon -> Maybe Class
    tyConClass_maybe TyCon
    tc
          -> Class -> [PredType] -> Pred
    ClassPred Class
    clas [PredType]
    tys

        Maybe (TyCon, [PredType])
    _ | ([TyCoVar]
    tvs, PredType
    rho) <- PredType -> ([TyCoVar], PredType)
    splitForAllTyCoVars PredType
    ev_ty
          , ([Scaled PredType]
    theta, PredType
    pred) <- PredType -> ([Scaled PredType], PredType)
    splitFunTys PredType
    rho
          , Bool -> Bool
    not ([TyCoVar] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TyCoVar]
    tvs Bool -> Bool -> Bool
    && [Scaled PredType] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Scaled PredType]
    theta)
          -> [TyCoVar] -> [PredType] -> PredType -> Pred
    ForAllPred [TyCoVar]
    tvs ((Scaled PredType -> PredType) -> [Scaled PredType] -> [PredType]
    forall a b. (a -> b) -> [a] -> [b]
    map Scaled PredType -> PredType
    forall a. Scaled a -> a
    scaledThing [Scaled PredType]
    theta) PredType
    pred

          | Bool
    otherwise
          -> PredType -> Pred
    IrredPred PredType
    ev_ty

    -- --------------------- Dictionary types ---------------------------------

    mkClassPred :: Class -> [Type] -> PredType
    mkClassPred :: Class -> [PredType] -> PredType
    mkClassPred Class
    clas [PredType]
    tys = TyCon -> [PredType] -> PredType
    mkTyConApp (Class -> TyCon
    classTyCon Class
    clas) [PredType]
    tys

    isDictTy :: Type -> Bool
    -- True of dictionaries (Eq a) and
    --         dictionary functions (forall a. Eq a => Eq [a])
    -- See Note [Type determines value]
    -- See #24370 (and the isDictId call in GHC.HsToCore.Binds.decomposeRuleLhs)
    --     for why it's important to catch dictionary bindings
    isDictTy :: PredType -> Bool
    isDictTy PredType
    ty = PredType -> Bool
    isClassPred PredType
    pred
      where
        ([PiTyBinder]
    _, PredType
    pred) = PredType -> ([PiTyBinder], PredType)
    splitInvisPiTys PredType
    ty

    typeDeterminesValue :: Type -> Bool
    -- See Note [Type determines value]
    typeDeterminesValue :: PredType -> Bool
    typeDeterminesValue PredType
    ty = PredType -> Bool
    isDictTy PredType
    ty Bool -> Bool -> Bool
    && Bool -> Bool
    not (PredType -> Bool
    isIPLikePred PredType
    ty)

    getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
    getClassPredTys :: HasDebugCallStack => PredType -> (Class, [PredType])
    getClassPredTys PredType
    ty = case PredType -> Maybe (Class, [PredType])
    getClassPredTys_maybe PredType
    ty of
            Just (Class
    clas, [PredType]
    tys) -> (Class
    clas, [PredType]
    tys)
            Maybe (Class, [PredType])
    Nothing          -> String -> SDoc -> (Class, [PredType])
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "getClassPredTys" (PredType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PredType
    ty)

    getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
    getClassPredTys_maybe :: PredType -> Maybe (Class, [PredType])
    getClassPredTys_maybe PredType
    ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
    PredType -> Maybe (TyCon, [PredType])
    splitTyConApp_maybe PredType
    ty of
            Just (TyCon
    tc, [PredType]
    tys) | Just Class
    clas <- TyCon -> Maybe Class
    tyConClass_maybe TyCon
    tc -> (Class, [PredType]) -> Maybe (Class, [PredType])
    forall a. a -> Maybe a
    Just (Class
    clas, [PredType]
    tys)
            Maybe (TyCon, [PredType])
    _ -> Maybe (Class, [PredType])
    forall a. Maybe a
    Nothing

    classMethodTy :: Id -> Type
    -- Takes a class selector op :: forall a. C a => meth_ty
    -- and returns the type of its method, meth_ty
    -- The selector can be a superclass selector, in which case
    -- you get back a superclass
    classMethodTy :: TyCoVar -> PredType
    classMethodTy TyCoVar
    sel_id
      = HasDebugCallStack => PredType -> PredType
    PredType -> PredType
    funResultTy (PredType -> PredType) -> PredType -> PredType
    forall a b. (a -> b) -> a -> b
    $        -- meth_ty
        PredType -> PredType
    dropForAlls (PredType -> PredType) -> PredType -> PredType
    forall a b. (a -> b) -> a -> b
    $        -- C a => meth_ty
        TyCoVar -> PredType
    varType TyCoVar
    sel_id        -- forall a. C n => meth_ty

    classMethodInstTy :: Id -> [Type] -> Type
    -- Takes a class selector op :: forall a b. C a b => meth_ty
    -- and the types [ty1, ty2] at which it is instantiated,
    -- returns the instantiated type of its method, meth_ty[t1/a,t2/b]
    -- The selector can be a superclass selector, in which case
    -- you get back a superclass
    classMethodInstTy :: TyCoVar -> [PredType] -> PredType
    classMethodInstTy TyCoVar
    sel_id [PredType]
    arg_tys
      = HasDebugCallStack => PredType -> PredType
    PredType -> PredType
    funResultTy (PredType -> PredType) -> PredType -> PredType
    forall a b. (a -> b) -> a -> b
    $
        HasDebugCallStack => PredType -> [PredType] -> PredType
    PredType -> [PredType] -> PredType
    piResultTys (TyCoVar -> PredType
    varType TyCoVar
    sel_id) [PredType]
    arg_tys

    {- Note [Type determines value]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Only specialise on non-impicit-parameter predicates, because these
    are the ones whose *type* determines their *value*.  In particular,
    with implicit params, the type args *don't* say what the value of the
    implicit param is!  See #7101.

    So we treat implicit params just like ordinary arguments for the
    purposes of specialisation.  Note that we still want to specialise
    functions with implicit params if they have *other* dicts which are
    class params; see #17930.
    -}

    -- --------------------- Equality predicates ---------------------------------

    -- | A choice of equality relation. This is separate from the type 'Role'
    -- because 'Phantom' does not define a (non-trivial) equality relation.
    data EqRel = NomEq | ReprEq
      deriving (EqRel -> EqRel -> Bool
    (EqRel -> EqRel -> Bool) -> (EqRel -> EqRel -> Bool) -> Eq EqRel
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: EqRel -> EqRel -> Bool
    == :: EqRel -> EqRel -> Bool
    $c/= :: EqRel -> EqRel -> Bool
    /= :: EqRel -> EqRel -> Bool
    Eq, Eq EqRel
    Eq EqRel =>
    (EqRel -> EqRel -> Ordering)
    -> (EqRel -> EqRel -> Bool)
    -> (EqRel -> EqRel -> Bool)
    -> (EqRel -> EqRel -> Bool)
    -> (EqRel -> EqRel -> Bool)
    -> (EqRel -> EqRel -> EqRel)
    -> (EqRel -> EqRel -> EqRel)
    -> Ord EqRel
    EqRel -> EqRel -> Bool
    EqRel -> EqRel -> Ordering
    EqRel -> EqRel -> EqRel
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: EqRel -> EqRel -> Ordering
    compare :: EqRel -> EqRel -> Ordering
    $c< :: EqRel -> EqRel -> Bool
    < :: EqRel -> EqRel -> Bool
    $c<= :: EqRel -> EqRel -> Bool
    <= :: EqRel -> EqRel -> Bool
    $c> :: EqRel -> EqRel -> Bool
    > :: EqRel -> EqRel -> Bool
    $c>= :: EqRel -> EqRel -> Bool
    >= :: EqRel -> EqRel -> Bool
    $cmax :: EqRel -> EqRel -> EqRel
    max :: EqRel -> EqRel -> EqRel
    $cmin :: EqRel -> EqRel -> EqRel
    min :: EqRel -> EqRel -> EqRel
    Ord)

    instance Outputable EqRel where
      ppr :: EqRel -> SDoc
    ppr EqRel
    NomEq  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "nominal equality"
      ppr EqRel
    ReprEq = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "representational equality"

    eqRelRole :: EqRel -> Role
    eqRelRole :: EqRel -> Role
    eqRelRole EqRel
    NomEq  = Role
    Nominal
    eqRelRole EqRel
    ReprEq = Role
    Representational

    getEqPredTys :: PredType -> (Type, Type)
    getEqPredTys :: PredType -> (PredType, PredType)
    getEqPredTys PredType
    ty
      = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
    PredType -> Maybe (TyCon, [PredType])
    splitTyConApp_maybe PredType
    ty of
          Just (TyCon
    tc, [PredType
    _, PredType
    _, PredType
    ty1, PredType
    ty2])
            |  TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqPrimTyConKey
            Bool -> Bool -> Bool
    || TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqReprPrimTyConKey
            -> (PredType
    ty1, PredType
    ty2)
          Maybe (TyCon, [PredType])
    _ -> String -> SDoc -> (PredType, PredType)
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "getEqPredTys" (PredType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr PredType
    ty)

    getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
    getEqPredTys_maybe :: PredType -> Maybe (Role, PredType, PredType)
    getEqPredTys_maybe PredType
    ty
      = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
    PredType -> Maybe (TyCon, [PredType])
    splitTyConApp_maybe PredType
    ty of
          Just (TyCon
    tc, [PredType
    _, PredType
    _, PredType
    ty1, PredType
    ty2])
            | TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqPrimTyConKey     -> (Role, PredType, PredType) -> Maybe (Role, PredType, PredType)
    forall a. a -> Maybe a
    Just (Role
    Nominal, PredType
    ty1, PredType
    ty2)
            | TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqReprPrimTyConKey -> (Role, PredType, PredType) -> Maybe (Role, PredType, PredType)
    forall a. a -> Maybe a
    Just (Role
    Representational, PredType
    ty1, PredType
    ty2)
          Maybe (TyCon, [PredType])
    _ -> Maybe (Role, PredType, PredType)
    forall a. Maybe a
    Nothing

    getEqPredRole :: PredType -> Role
    getEqPredRole :: PredType -> Role
    getEqPredRole PredType
    ty = EqRel -> Role
    eqRelRole (PredType -> EqRel
    predTypeEqRel PredType
    ty)

    -- | Get the equality relation relevant for a pred type.
    predTypeEqRel :: PredType -> EqRel
    predTypeEqRel :: PredType -> EqRel
    predTypeEqRel PredType
    ty
      | Just (TyCon
    tc, [PredType]
    _) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
    PredType -> Maybe (TyCon, [PredType])
    splitTyConApp_maybe PredType
    ty
      , TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqReprPrimTyConKey
      = EqRel
    ReprEq
      | Bool
    otherwise
      = EqRel
    NomEq

    {-------------------------------------------
    Predicates on PredType
    --------------------------------------------}

    {-
    Note [Evidence for quantified constraints]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The superclass mechanism in GHC.Tc.Solver.Dict.makeSuperClasses risks
    taking a quantified constraint like
       (forall a. C a => a ~ b)
    and generate superclass evidence
       (forall a. C a => a ~# b)

    This is a funny thing: neither isPredTy nor isCoVarType are true
    of it.  So we are careful not to generate it in the first place:
    see Note [Equality superclasses in quantified constraints]
    in GHC.Tc.Solver.Dict.
    -}

    isEvVarType :: Type -> Bool
    -- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
    --         (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
    -- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
    -- See Note [Evidence for quantified constraints]
    isEvVarType :: PredType -> Bool
    isEvVarType PredType
    ty = PredType -> Bool
    isCoVarType PredType
    ty Bool -> Bool -> Bool
    || HasDebugCallStack => PredType -> Bool
    PredType -> Bool
    isPredTy PredType
    ty

    isClassPred :: PredType -> Bool
    isClassPred :: PredType -> Bool
    isClassPred PredType
    ty = case PredType -> Maybe TyCon
    tyConAppTyCon_maybe PredType
    ty of
        Just TyCon
    tc -> TyCon -> Bool
    isClassTyCon TyCon
    tc
        Maybe TyCon
    _       -> Bool
    False

    isEqPred :: PredType -> Bool
    isEqPred :: PredType -> Bool
    isEqPred PredType
    ty  -- True of (a ~ b) and (a ~~ b)
                 -- ToDo: should we check saturation?
      | Just TyCon
    tc <- PredType -> Maybe TyCon
    tyConAppTyCon_maybe PredType
    ty
      , Just Class
    cls <- TyCon -> Maybe Class
    tyConClass_maybe TyCon
    tc
      = Class -> Bool
    isEqualityClass Class
    cls
      | Bool
    otherwise
      = Bool
    False

    isEqPrimPred :: PredType -> Bool
    isEqPrimPred :: PredType -> Bool
    isEqPrimPred PredType
    ty = PredType -> Bool
    isCoVarType PredType
    ty
      -- True of (a ~# b) (a ~R# b)

    isEqualityClass :: Class -> Bool
    -- True of (~), (~~), and Coercible
    -- These all have a single primitive-equality superclass, either (~N# or ~R#)
    isEqualityClass :: Class -> Bool
    isEqualityClass Class
    cls
      = Class
    cls Class -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    heqTyConKey
        Bool -> Bool -> Bool
    || Class
    cls Class -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    eqTyConKey
        Bool -> Bool -> Bool
    || Class
    cls Class -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    coercibleTyConKey

    isCTupleClass :: Class -> Bool
    isCTupleClass :: Class -> Bool
    isCTupleClass Class
    cls = TyCon -> Bool
    isTupleTyCon (Class -> TyCon
    classTyCon Class
    cls)

    {- *********************************************************************
    *                                                                      *
                  Implicit parameters
    *                                                                      *
    ********************************************************************* -}

    isIPTyCon :: TyCon -> Bool
    isIPTyCon :: TyCon -> Bool
    isIPTyCon TyCon
    tc = TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    ipClassKey
      -- Class and its corresponding TyCon have the same Unique

    isIPClass :: Class -> Bool
    isIPClass :: Class -> Bool
    isIPClass Class
    cls = Class
    cls Class -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    ipClassKey

    -- | Decomposes a predicate if it is an implicit parameter. Does not look in
    -- superclasses. See also [Local implicit parameters].
    isIPPred_maybe :: Class -> [Type] -> Maybe (Type, Type)
    isIPPred_maybe :: Class -> [PredType] -> Maybe (PredType, PredType)
    isIPPred_maybe Class
    cls [PredType]
    tys
      | Class -> Bool
    isIPClass Class
    cls
      , [PredType
    t1,PredType
    t2] <- [PredType]
    tys
      = (PredType, PredType) -> Maybe (PredType, PredType)
    forall a. a -> Maybe a
    Just (PredType
    t1,PredType
    t2)
      | Bool
    otherwise
      = Maybe (PredType, PredType)
    forall a. Maybe a
    Nothing

    -- --------------------- ExceptionContext predicates --------------------------

    -- | Is a 'PredType' an @ExceptionContext@ implicit parameter?
    --
    -- If so, return the name of the parameter.
    isExceptionContextPred :: Class -> [Type] -> Maybe FastString
    isExceptionContextPred :: Class -> [PredType] -> Maybe FastString
    isExceptionContextPred Class
    cls [PredType]
    tys
      | [PredType
    ty1, PredType
    ty2] <- [PredType]
    tys
      , Class -> Bool
    isIPClass Class
    cls
      , PredType -> Bool
    isExceptionContextTy PredType
    ty2
      = PredType -> Maybe FastString
    isStrLitTy PredType
    ty1
      | Bool
    otherwise
      = Maybe FastString
    forall a. Maybe a
    Nothing

    -- | Is a type an 'ExceptionContext'?
    isExceptionContextTy :: Type -> Bool
    isExceptionContextTy :: PredType -> Bool
    isExceptionContextTy PredType
    ty
      | Just TyCon
    tc <- PredType -> Maybe TyCon
    tyConAppTyCon_maybe PredType
    ty
      = TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    exceptionContextTyConKey
      | Bool
    otherwise
      = Bool
    False

    -- --------------------- CallStack predicates ---------------------------------

    isCallStackPredTy :: Type -> Bool
    -- True of HasCallStack, or IP "blah" CallStack
    isCallStackPredTy :: PredType -> Bool
    isCallStackPredTy PredType
    ty
      | Just (TyCon
    tc, [PredType]
    tys) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
    PredType -> Maybe (TyCon, [PredType])
    splitTyConApp_maybe PredType
    ty
      , Just Class
    cls <- TyCon -> Maybe Class
    tyConClass_maybe TyCon
    tc
      , Just {} <- Class -> [PredType] -> Maybe FastString
    isCallStackPred Class
    cls [PredType]
    tys
      = Bool
    True
      | Bool
    otherwise
      = Bool
    False

    -- | Is a 'PredType' a 'CallStack' implicit parameter?
    --
    -- If so, return the name of the parameter.
    isCallStackPred :: Class -> [Type] -> Maybe FastString
    isCallStackPred :: Class -> [PredType] -> Maybe FastString
    isCallStackPred Class
    cls [PredType]
    tys
      | [PredType
    ty1, PredType
    ty2] <- [PredType]
    tys
      , Class -> Bool
    isIPClass Class
    cls
      , PredType -> Bool
    isCallStackTy PredType
    ty2
      = PredType -> Maybe FastString
    isStrLitTy PredType
    ty1
      | Bool
    otherwise
      = Maybe FastString
    forall a. Maybe a
    Nothing

    -- | Is a type a 'CallStack'?
    isCallStackTy :: Type -> Bool
    isCallStackTy :: PredType -> Bool
    isCallStackTy PredType
    ty
      | Just TyCon
    tc <- PredType -> Maybe TyCon
    tyConAppTyCon_maybe PredType
    ty
      = TyCon
    tc TyCon -> Unique -> Bool
    forall a. Uniquable a => a -> Unique -> Bool
    `hasKey` Unique
    callStackTyConKey
      | Bool
    otherwise
      = Bool
    False

    -- --------------------- isIPLike and mentionsIP  --------------------------
    --                 See Note [Local implicit parameters]

    isIPLikePred :: Type -> Bool
    -- Is `pred`, or any of its superclasses, an implicit parameter?
    -- See Note [Local implicit parameters]
    isIPLikePred :: PredType -> Bool
    isIPLikePred PredType
    pred =
      RecTcChecker
    -> (PredType -> Bool) -> (PredType -> Bool) -> PredType -> Bool
    mentions_ip_pred RecTcChecker
    initIPRecTc (Bool -> PredType -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (Bool -> PredType -> Bool
    forall a b. a -> b -> a
    const Bool
    True) PredType
    pred

    mentionsIP :: (Type -> Bool) -- ^ predicate on the string
               -> (Type -> Bool) -- ^ predicate on the type
               -> Class
               -> [Type] -> Bool
    -- ^ @'mentionsIP' str_cond ty_cond cls tys@ returns @True@ if:
    --
    --    - @cls tys@ is of the form @IP str ty@, where @str_cond str@ and @ty_cond ty@
    --      are both @True@,
    --    - or any superclass of @cls tys@ has this property.
    --
    -- See Note [Local implicit parameters]
    mentionsIP :: (PredType -> Bool)
    -> (PredType -> Bool) -> Class -> [PredType] -> Bool
    mentionsIP = RecTcChecker
    -> (PredType -> Bool)
    -> (PredType -> Bool)
    -> Class
    -> [PredType]
    -> Bool
    mentions_ip RecTcChecker
    initIPRecTc

    mentions_ip :: RecTcChecker -> (Type -> Bool) -> (Type -> Bool) -> Class -> [Type] -> Bool
    mentions_ip :: RecTcChecker
    -> (PredType -> Bool)
    -> (PredType -> Bool)
    -> Class
    -> [PredType]
    -> Bool
    mentions_ip RecTcChecker
    rec_clss PredType -> Bool
    str_cond PredType -> Bool
    ty_cond Class
    cls [PredType]
    tys
      | Just (PredType
    str_ty, PredType
    ty) <- Class -> [PredType] -> Maybe (PredType, PredType)
    isIPPred_maybe Class
    cls [PredType]
    tys
      = PredType -> Bool
    str_cond PredType
    str_ty Bool -> Bool -> Bool
    && PredType -> Bool
    ty_cond PredType
    ty
      | Bool
    otherwise
      = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or [ RecTcChecker
    -> (PredType -> Bool) -> (PredType -> Bool) -> PredType -> Bool
    mentions_ip_pred RecTcChecker
    rec_clss PredType -> Bool
    str_cond PredType -> Bool
    ty_cond (TyCoVar -> [PredType] -> PredType
    classMethodInstTy TyCoVar
    sc_sel_id [PredType]
    tys)
           | TyCoVar
    sc_sel_id <- Class -> [TyCoVar]
    classSCSelIds Class
    cls ]

    mentions_ip_pred :: RecTcChecker -> (Type -> Bool) -> (Type -> Bool) -> Type -> Bool
    mentions_ip_pred :: RecTcChecker
    -> (PredType -> Bool) -> (PredType -> Bool) -> PredType -> Bool
    mentions_ip_pred RecTcChecker
    rec_clss PredType -> Bool
    str_cond PredType -> Bool
    ty_cond PredType
    ty
      | Just (Class
    cls, [PredType]
    tys) <- PredType -> Maybe (Class, [PredType])
    getClassPredTys_maybe PredType
    ty
      , let tc :: TyCon
    tc = Class -> TyCon
    classTyCon Class
    cls
      , Just RecTcChecker
    rec_clss' <- if TyCon -> Bool
    isTupleTyCon TyCon
    tc then RecTcChecker -> Maybe RecTcChecker
    forall a. a -> Maybe a
    Just RecTcChecker
    rec_clss
                          else RecTcChecker -> TyCon -> Maybe RecTcChecker
    checkRecTc RecTcChecker
    rec_clss TyCon
    tc
      = RecTcChecker
    -> (PredType -> Bool)
    -> (PredType -> Bool)
    -> Class
    -> [PredType]
    -> Bool
    mentions_ip RecTcChecker
    rec_clss' PredType -> Bool
    str_cond PredType -> Bool
    ty_cond Class
    cls [PredType]
    tys
      | Bool
    otherwise
      = Bool
    False -- Includes things like (D []) where D is
              -- a Constraint-ranged family; #7785

    initIPRecTc :: RecTcChecker
    initIPRecTc :: RecTcChecker
    initIPRecTc = Int -> RecTcChecker -> RecTcChecker
    setRecTcMaxBound Int
    1 RecTcChecker
    initRecTc

    {- Note [Local implicit parameters]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    See also wrinkle (SIP1) in Note [Shadowing of implicit parameters] in
    GHC.Tc.Solver.Dict.

    The function isIPLikePred tells if this predicate, or any of its
    superclasses, is an implicit parameter.

    Why are implicit parameters special?  Unlike normal classes, we can
    have local instances for implicit parameters, in the form of
       let ?x = True in ...
    So in various places we must be careful not to assume that any value
    of the right type will do; we must carefully look for the innermost binding.
    So isIPLikePred checks whether this is an implicit parameter, or has
    a superclass that is an implicit parameter.

    Several wrinkles

    * We must be careful with superclasses, as #18649 showed.  Haskell
      doesn't allow an implicit parameter as a superclass
        class (?x::a) => C a where ...
      but with a constraint tuple we might have
         (% Eq a, ?x::Int %)
      and /its/ superclasses, namely (Eq a) and (?x::Int), /do/ include an
      implicit parameter.

      With ConstraintKinds this can apply to /any/ class, e.g.
         class sc => C sc where ...
      Then (C (?x::Int)) has (?x::Int) as a superclass.  So we must
      instantiate and check each superclass, one by one, in
      hasIPSuperClasses.

    * With -XUndecidableSuperClasses, the superclass hunt can go on forever,
      so we need a RecTcChecker to cut it off.

    * Another apparent additional complexity involves type families. For
      example, consider
             type family D (v::*->*) :: Constraint
             type instance D [] = ()
             f :: D v => v Char -> Int
      If we see a call (f "foo"), we'll pass a "dictionary"
        () |> (g :: () ~ D [])
      and it's good to specialise f at this dictionary.

    So the question is: can an implicit parameter "hide inside" a
    type-family constraint like (D a).  Well, no.  We don't allow
            type instance D Maybe = ?x:Int
    Hence the umbrella 'otherwise' case in is_ip_like_pred.  See #7785.

    Small worries (Sept 20):
    * I don't see what stops us having that 'type instance'. Indeed I
      think nothing does.
    * I'm a little concerned about type variables; such a variable might
      be instantiated to an implicit parameter.  I don't think this
      matters in the cases for which isIPLikePred is used, and it's pretty
      obscure anyway.
    * The superclass hunt stops when it encounters the same class again,
      but in principle we could have the same class, differently instantiated,
      and the second time it could have an implicit parameter
    I'm going to treat these as problems for another day. They are all exotic.

    Note [Using typesAreApart when calling mentionsIP]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We call 'mentionsIP' in two situations:

      (1) to check that a predicate does not contain any implicit parameters
          IP str ty, for a fixed literal str and any type ty,
      (2) to check that a predicate does not contain any HasCallStack or
          HasExceptionContext constraints.

    In both of these cases, we want to be sure, so we should be conservative:

      For (1), the predicate might contain an implicit parameter IP Str a, where
      Str is a type family such as:

        type family MyStr where MyStr = "abc"

      To safeguard against this (niche) situation, instead of doing a simple
      type equality check, we use 'typesAreApart'. This allows us to recognise
      that 'IP MyStr a' contains an implicit parameter of the form 'IP "abc" ty'.

      For (2), we similarly might have

        type family MyCallStack where MyCallStack = CallStack

      Again, here we use 'typesAreApart'. This allows us to see that

        (?foo :: MyCallStack)

      is indeed a CallStack constraint, hidden under a type family.
    -}

    {- *********************************************************************
    *                                                                      *
                  Evidence variables
    *                                                                      *
    ********************************************************************* -}

    isEvVar :: Var -> Bool
    isEvVar :: TyCoVar -> Bool
    isEvVar TyCoVar
    var = PredType -> Bool
    isEvVarType (TyCoVar -> PredType
    varType TyCoVar
    var)

    isDictId :: Id -> Bool
    isDictId :: TyCoVar -> Bool
    isDictId TyCoVar
    id = PredType -> Bool
    isDictTy (TyCoVar -> PredType
    varType TyCoVar
    id)