    -- (c) The University of Glasgow 2006

    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE LambdaCase #-}

    module GHC.Tc.Types.Evidence (

      -- * HsWrapper
      HsWrapper(..),
      (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
      mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
      collectHsWrapBinders,
      idHsWrapper, isIdHsWrapper,
      pprHsWrapper, hsWrapDictBinders,

      -- * Evidence bindings
      TcEvBinds(..), EvBindsVar(..),
      EvBindMap(..), emptyEvBindMap, extendEvBinds,
      lookupEvBind, evBindMapBinds,
      foldEvBindMap, nonDetStrictFoldEvBindMap,
      filterEvBindMap,
      isEmptyEvBindMap,
      evBindMapToVarSet,
      varSetMinusEvBindMap,
      EvBindInfo(..), EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
      evBindVar, isCoEvBindsVar,

      -- * EvTerm (already a CoreExpr)
      EvTerm(..), EvExpr,
      evId, evCoercion, evCast, evDFunApp,  evDataConApp, evSelector,
      mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,

      evTermCoercion, evTermCoercion_maybe,
      EvCallStack(..),
      EvTypeable(..),

      -- * HoleExprRef
      HoleExprRef(..),

      -- * TcCoercion
      TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
      TcMCoercion, TcMCoercionN, TcMCoercionR, MultiplicityCheckCoercions,
      Role(..), LeftOrRight(..), pickLR,
      maybeSymCo,
      unwrapIP, wrapIP,

      -- * QuoteWrapper
      QuoteWrapper(..), applyQuoteWrapper, quoteWrapperTyVarTy
      ) where

    import GHC.Prelude

    import GHC.Types.Unique.DFM
    import GHC.Types.Unique.FM
    import GHC.Types.Var
    import GHC.Types.Id( idScaledType )
    import GHC.Core.Coercion.Axiom
    import GHC.Core.Coercion
    import GHC.Core.Ppr ()   -- Instance OutputableBndr TyVar
    import GHC.Tc.Utils.TcType
    import GHC.Core.Type
    import GHC.Core.TyCon
    import GHC.Core.DataCon ( DataCon, dataConWrapId )
    import GHC.Builtin.Names
    import GHC.Types.Var.Env
    import GHC.Types.Var.Set
    import GHC.Core.Predicate
    import GHC.Types.Basic

    import GHC.Core
    import GHC.Core.Class (Class, classSCSelId )
    import GHC.Core.FVs   ( exprSomeFreeVars )
    import GHC.Core.InstEnv ( CanonicalEvidence(..) )

    import GHC.Utils.Misc
    import GHC.Utils.Panic
    import GHC.Utils.Outputable

    import GHC.Data.Bag
    import GHC.Data.FastString

    import qualified Data.Data as Data
    import GHC.Types.SrcLoc
    import Data.IORef( IORef )
    import GHC.Types.Unique.Set
    import GHC.Core.Multiplicity

    import qualified Data.Semigroup as S

    {-
    Note [TcCoercions]
    ~~~~~~~~~~~~~~~~~~
    | TcCoercions are a hack used by the typechecker. Normally,
    Coercions have free variables of type (a ~# b): we call these
    CoVars. However, the type checker passes around equality evidence
    (boxed up) at type (a ~ b).

    An TcCoercion is simply a Coercion whose free variables have may be either
    boxed or unboxed. After we are done with typechecking the desugarer finds the
    boxed free variables, unboxes them, and creates a resulting real Coercion with
    kosher free variables.

    -}

    type TcCoercion   = Coercion
    type TcCoercionN  = CoercionN    -- A Nominal          coercion ~N
    type TcCoercionR  = CoercionR    -- A Representational coercion ~R
    type TcCoercionP  = CoercionP    -- a phantom coercion
    type TcMCoercion  = MCoercion
    type TcMCoercionN = MCoercionN  -- nominal
    type TcMCoercionR = MCoercionR  -- representational

    type MultiplicityCheckCoercions = [TcCoercion]
    -- Coercions which must all be reflexivity after zonking.
    -- See Note [Coercions returned from tcSubMult] in GHC.Tc.Utils.Unify.

    -- | If a 'SwapFlag' is 'IsSwapped', flip the orientation of a coercion
    maybeSymCo :: SwapFlag -> TcCoercion -> TcCoercion
    maybeSymCo :: SwapFlag -> TcCoercion -> TcCoercion
    maybeSymCo SwapFlag
    IsSwapped  TcCoercion
    co = TcCoercion -> TcCoercion
    mkSymCo TcCoercion
    co
    maybeSymCo SwapFlag
    NotSwapped TcCoercion
    co = TcCoercion
    co

    {-
    %************************************************************************
    %*                                                                      *
                      HsWrapper
    *                                                                      *
    ************************************************************************
    -}

    -- We write    wrap :: t1 ~> t2
    -- if       wrap[ e::t1 ] :: t2
    data HsWrapper
      = WpHole                      -- The identity coercion

      | WpCompose HsWrapper HsWrapper
           -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
           --
           -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
           -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
           --
           -- If wrap1 :: t2 ~> t3
           --    wrap2 :: t1 ~> t2
           --- Then (wrap1 `WpCompose` wrap2) :: t1 ~> t3

      | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR)
           -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
           -- So note that if  e     :: act_arg -> act_res
           --                  wrap1 :: exp_arg ~> act_arg
           --                  wrap2 :: act_res ~> exp_res
           --           then   WpFun wrap1 wrap2 : (act_arg -> arg_res) ~> (exp_arg -> exp_res)
           -- This isn't the same as for mkFunCo, but it has to be this way
           -- because we can't use 'sym' to flip around these HsWrappers
           -- The TcType is the "from" type of the first wrapper;
           --     it always a Type, not a Constraint
           --
           -- NB: a WpFun is always for a (->) function arrow
           --
           -- Use 'mkWpFun' to construct such a wrapper.

      | WpCast TcCoercionR        -- A cast:  [] `cast` co
                                  -- Guaranteed not the identity coercion
                                  -- At role Representational

            -- Evidence abstraction and application
            -- (both dictionaries and coercions)
            -- Both WpEvLam and WpEvApp abstract and apply values
            --      of kind CONSTRAINT rep
      | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable
      | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint

            -- Kind and Type abstraction and application
      | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)
      | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)

      | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,
                                    -- so that the identity coercion is always exactly WpHole

      | WpMultCoercion Coercion     -- Require that a Coercion be reflexive; otherwise,
                                    -- error in the desugarer. See GHC.Tc.Utils.Unify
                                    -- Note [Coercions returned from tcSubMult]
      deriving Typeable HsWrapper
    Typeable HsWrapper =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c HsWrapper)
    -> (HsWrapper -> Constr)
    -> (HsWrapper -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c HsWrapper))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper))
    -> ((forall b. Data b => b -> b) -> HsWrapper -> HsWrapper)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r)
    -> (forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> HsWrapper -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper)
    -> Data HsWrapper
    HsWrapper -> Constr
    HsWrapper -> DataType
    (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> HsWrapper -> u
    forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HsWrapper
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HsWrapper)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> HsWrapper -> c HsWrapper
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HsWrapper
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HsWrapper
    $ctoConstr :: HsWrapper -> Constr
    toConstr :: HsWrapper -> Constr
    $cdataTypeOf :: HsWrapper -> DataType
    dataTypeOf :: HsWrapper -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HsWrapper)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HsWrapper)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HsWrapper)
    $cgmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper
    gmapT :: (forall b. Data b => b -> b) -> HsWrapper -> HsWrapper
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HsWrapper -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> HsWrapper -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HsWrapper -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HsWrapper -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HsWrapper -> m HsWrapper
    Data.Data

    -- | The Semigroup instance is a bit fishy, since @WpCompose@, as a data
    -- constructor, is "syntactic" and not associative. Concretely, if @a@, @b@,
    -- and @c@ aren't @WpHole@:
    --
    -- > (a <> b) <> c ?= a <> (b <> c)
    --
    -- ==>
    --
    -- > (a `WpCompose` b) `WpCompose` c /= @ a `WpCompose` (b `WpCompose` c)
    --
    -- However these two associations are are "semantically equal" in the sense
    -- that they produce equal functions when passed to
    -- @GHC.HsToCore.Binds.dsHsWrapper@.
    instance S.Semigroup HsWrapper where
      <> :: HsWrapper -> HsWrapper -> HsWrapper
    (<>) = HsWrapper -> HsWrapper -> HsWrapper
    (<.>)

    instance Monoid HsWrapper where
      mempty :: HsWrapper
    mempty = HsWrapper
    WpHole

    (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
    HsWrapper
    WpHole <.> :: HsWrapper -> HsWrapper -> HsWrapper
    <.> HsWrapper
    c = HsWrapper
    c
    HsWrapper
    c <.> HsWrapper
    WpHole = HsWrapper
    c
    HsWrapper
    c1 <.> HsWrapper
    c2    = HsWrapper
    c1 HsWrapper -> HsWrapper -> HsWrapper
    `WpCompose` HsWrapper
    c2

    -- | Smart constructor to create a 'WpFun' 'HsWrapper'.
    --
    -- PRECONDITION: the "from" type of the first wrapper must have a syntactically
    -- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
    mkWpFun :: HsWrapper -> HsWrapper
            -> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
                                -- MUST have a fixed RuntimeRep
            -> TcType           -- ^ Either "from" type or "to" type of the second wrapper
                                --   (used only when the second wrapper is the identity)
            -> HsWrapper
      -- NB: we can't check that the argument type has a fixed RuntimeRep with an assertion,
      -- because of [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]
      -- in GHC.Tc.Utils.Concrete.
    mkWpFun :: HsWrapper -> HsWrapper -> Scaled Mult -> Mult -> HsWrapper
    mkWpFun HsWrapper
    WpHole       HsWrapper
    WpHole       Scaled Mult
    _             Mult
    _  = HsWrapper
    WpHole
    mkWpFun HsWrapper
    WpHole       (WpCast TcCoercion
    co2) (Scaled Mult
    w Mult
    t1) Mult
    _  = TcCoercion -> HsWrapper
    WpCast (Mult -> TcCoercion -> TcCoercion -> TcCoercion
    mk_wp_fun_co Mult
    w (Mult -> TcCoercion
    mkRepReflCo Mult
    t1) TcCoercion
    co2)
    mkWpFun (WpCast TcCoercion
    co1) HsWrapper
    WpHole       (Scaled Mult
    w Mult
    _)  Mult
    t2 = TcCoercion -> HsWrapper
    WpCast (Mult -> TcCoercion -> TcCoercion -> TcCoercion
    mk_wp_fun_co Mult
    w (TcCoercion -> TcCoercion
    mkSymCo TcCoercion
    co1)    (Mult -> TcCoercion
    mkRepReflCo Mult
    t2))
    mkWpFun (WpCast TcCoercion
    co1) (WpCast TcCoercion
    co2) (Scaled Mult
    w Mult
    _)  Mult
    _  = TcCoercion -> HsWrapper
    WpCast (Mult -> TcCoercion -> TcCoercion -> TcCoercion
    mk_wp_fun_co Mult
    w (TcCoercion -> TcCoercion
    mkSymCo TcCoercion
    co1)    TcCoercion
    co2)
    mkWpFun HsWrapper
    co1          HsWrapper
    co2          Scaled Mult
    t1            Mult
    _  = HsWrapper -> HsWrapper -> Scaled Mult -> HsWrapper
    WpFun HsWrapper
    co1 HsWrapper
    co2 Scaled Mult
    t1

    mkWpEta :: [Id] -> HsWrapper -> HsWrapper
    -- (mkWpEta [x1, x2] wrap) [e]
    --   = \x1. \x2.  wrap[e x1 x2]
    -- Just generates a bunch of WpFuns
    mkWpEta :: [Id] -> HsWrapper -> HsWrapper
    mkWpEta [Id]
    xs HsWrapper
    wrap = (Id -> HsWrapper -> HsWrapper) -> HsWrapper -> [Id] -> HsWrapper
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Id -> HsWrapper -> HsWrapper
    eta_one HsWrapper
    wrap [Id]
    xs
      where
        eta_one :: Id -> HsWrapper -> HsWrapper
    eta_one Id
    x HsWrapper
    wrap = HsWrapper -> HsWrapper -> Scaled Mult -> HsWrapper
    WpFun HsWrapper
    idHsWrapper HsWrapper
    wrap (Id -> Scaled Mult
    idScaledType Id
    x)

    mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
    mk_wp_fun_co :: Mult -> TcCoercion -> TcCoercion -> TcCoercion
    mk_wp_fun_co Mult
    mult TcCoercion
    arg_co TcCoercion
    res_co
      = Role
    -> FunTyFlag
    -> TcCoercion
    -> TcCoercion
    -> TcCoercion
    -> TcCoercion
    mkNakedFunCo Role
    Representational FunTyFlag
    FTF_T_T (Mult -> TcCoercion
    multToCo Mult
    mult) TcCoercion
    arg_co TcCoercion
    res_co
        -- FTF_T_T: WpFun is always (->)

    mkWpCastR :: TcCoercionR -> HsWrapper
    mkWpCastR :: TcCoercion -> HsWrapper
    mkWpCastR TcCoercion
    co
      | TcCoercion -> Bool
    isReflCo TcCoercion
    co = HsWrapper
    WpHole
      | Bool
    otherwise   = Bool -> SDoc -> HsWrapper -> HsWrapper
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (TcCoercion -> Role
    coercionRole TcCoercion
    co Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Representational) (TcCoercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcCoercion
    co) (HsWrapper -> HsWrapper) -> HsWrapper -> HsWrapper
    forall a b. (a -> b) -> a -> b
    $
                      TcCoercion -> HsWrapper
    WpCast TcCoercion
    co

    mkWpCastN :: TcCoercionN -> HsWrapper
    mkWpCastN :: TcCoercion -> HsWrapper
    mkWpCastN TcCoercion
    co
      | TcCoercion -> Bool
    isReflCo TcCoercion
    co = HsWrapper
    WpHole
      | Bool
    otherwise   = Bool -> SDoc -> HsWrapper -> HsWrapper
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (TcCoercion -> Role
    coercionRole TcCoercion
    co Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Nominal) (TcCoercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcCoercion
    co) (HsWrapper -> HsWrapper) -> HsWrapper -> HsWrapper
    forall a b. (a -> b) -> a -> b
    $
                      TcCoercion -> HsWrapper
    WpCast (HasDebugCallStack => TcCoercion -> TcCoercion
    TcCoercion -> TcCoercion
    mkSubCo TcCoercion
    co)
        -- The mkTcSubCo converts Nominal to Representational

    mkWpTyApps :: [Type] -> HsWrapper
    mkWpTyApps :: [Mult] -> HsWrapper
    mkWpTyApps [Mult]
    tys = (Mult -> HsWrapper) -> [Mult] -> HsWrapper
    forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_app_fn Mult -> HsWrapper
    WpTyApp [Mult]
    tys

    mkWpEvApps :: [EvTerm] -> HsWrapper
    mkWpEvApps :: [EvTerm] -> HsWrapper
    mkWpEvApps [EvTerm]
    args = (EvTerm -> HsWrapper) -> [EvTerm] -> HsWrapper
    forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_app_fn EvTerm -> HsWrapper
    WpEvApp [EvTerm]
    args

    mkWpEvVarApps :: [EvVar] -> HsWrapper
    mkWpEvVarApps :: [Id] -> HsWrapper
    mkWpEvVarApps [Id]
    vs = (EvTerm -> HsWrapper) -> [EvTerm] -> HsWrapper
    forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_app_fn EvTerm -> HsWrapper
    WpEvApp ((Id -> EvTerm) -> [Id] -> [EvTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map (EvExpr -> EvTerm
    EvExpr (EvExpr -> EvTerm) -> (Id -> EvExpr) -> Id -> EvTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Id -> EvExpr
    evId) [Id]
    vs)

    mkWpTyLams :: [TyVar] -> HsWrapper
    mkWpTyLams :: [Id] -> HsWrapper
    mkWpTyLams [Id]
    ids = (Id -> HsWrapper) -> [Id] -> HsWrapper
    forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_lam_fn Id -> HsWrapper
    WpTyLam [Id]
    ids

    -- mkWpForAllCast [tv{vis}] constructs a cast
    --   forall tv. res  ~R#   forall tv{vis} res`.
    -- See Note [Required foralls in Core] in GHC.Core.TyCo.Rep
    --
    -- It's a no-op if all binders are invisible;
    -- but in that case we refrain from calling it.
    mkWpForAllCast :: [ForAllTyBinder] -> Type -> HsWrapper
    mkWpForAllCast :: [ForAllTyBinder] -> Mult -> HsWrapper
    mkWpForAllCast [ForAllTyBinder]
    bndrs Mult
    res_ty
      = TcCoercion -> HsWrapper
    mkWpCastR ([ForAllTyBinder] -> TcCoercion
    go [ForAllTyBinder]
    bndrs)
      where
        go :: [ForAllTyBinder] -> TcCoercion
    go []                 = Mult -> TcCoercion
    mkRepReflCo Mult
    res_ty
        go (Bndr Id
    tv ForAllTyFlag
    vis : [ForAllTyBinder]
    bs) = HasDebugCallStack =>
    Id
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> TcCoercion
    -> TcCoercion
    -> TcCoercion
    Id
    -> ForAllTyFlag
    -> ForAllTyFlag
    -> TcCoercion
    -> TcCoercion
    -> TcCoercion
    mkForAllCo Id
    tv ForAllTyFlag
    coreTyLamForAllTyFlag ForAllTyFlag
    vis TcCoercion
    kind_co ([ForAllTyBinder] -> TcCoercion
    go [ForAllTyBinder]
    bs)
          where
            kind_co :: TcCoercion
    kind_co = Mult -> TcCoercion
    mkNomReflCo (Id -> Mult
    varType Id
    tv)

    mkWpEvLams :: [Var] -> HsWrapper
    mkWpEvLams :: [Id] -> HsWrapper
    mkWpEvLams [Id]
    ids = (Id -> HsWrapper) -> [Id] -> HsWrapper
    forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_lam_fn Id -> HsWrapper
    WpEvLam [Id]
    ids

    mkWpLet :: TcEvBinds -> HsWrapper
    -- This no-op is a quite a common case
    mkWpLet :: TcEvBinds -> HsWrapper
    mkWpLet (EvBinds Bag EvBind
    b) | Bag EvBind -> Bool
    forall a. Bag a -> Bool
    isEmptyBag Bag EvBind
    b = HsWrapper
    WpHole
    mkWpLet TcEvBinds
    ev_binds                   = TcEvBinds -> HsWrapper
    WpLet TcEvBinds
    ev_binds

    mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_lam_fn :: forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_lam_fn a -> HsWrapper
    f [a]
    as = (a -> HsWrapper -> HsWrapper) -> HsWrapper -> [a] -> HsWrapper
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\a
    x HsWrapper
    wrap -> a -> HsWrapper
    f a
    x HsWrapper -> HsWrapper -> HsWrapper
    <.> HsWrapper
    wrap) HsWrapper
    WpHole [a]
    as

    mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
    -- For applications, the *first* argument must
    -- come *last* in the composition sequence
    mk_co_app_fn :: forall a. (a -> HsWrapper) -> [a] -> HsWrapper
    mk_co_app_fn a -> HsWrapper
    f [a]
    as = (a -> HsWrapper -> HsWrapper) -> HsWrapper -> [a] -> HsWrapper
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\a
    x HsWrapper
    wrap -> HsWrapper
    wrap HsWrapper -> HsWrapper -> HsWrapper
    <.> a -> HsWrapper
    f a
    x) HsWrapper
    WpHole [a]
    as

    idHsWrapper :: HsWrapper
    idHsWrapper :: HsWrapper
    idHsWrapper = HsWrapper
    WpHole

    isIdHsWrapper :: HsWrapper -> Bool
    isIdHsWrapper :: HsWrapper -> Bool
    isIdHsWrapper HsWrapper
    WpHole = Bool
    True
    isIdHsWrapper HsWrapper
    _      = Bool
    False

    hsWrapDictBinders :: HsWrapper -> Bag DictId
    -- ^ Identifies the /lambda-bound/ dictionaries of an 'HsWrapper'. This is used
    -- (only) to allow the pattern-match overlap checker to know what Given
    -- dictionaries are in scope.
    --
    -- We specifically do not collect dictionaries bound in a 'WpLet'. These are
    -- either superclasses of lambda-bound ones, or (extremely numerous) results of
    -- binding Wanted dictionaries.  We definitely don't want all those cluttering
    -- up the Given dictionaries for pattern-match overlap checking!
    hsWrapDictBinders :: HsWrapper -> Bag Id
    hsWrapDictBinders HsWrapper
    wrap = HsWrapper -> Bag Id
    go HsWrapper
    wrap
     where
       go :: HsWrapper -> Bag Id
    go (WpEvLam Id
    dict_id)   = Id -> Bag Id
    forall a. a -> Bag a
    unitBag Id
    dict_id
       go (HsWrapper
    w1 `WpCompose` HsWrapper
    w2) = HsWrapper -> Bag Id
    go HsWrapper
    w1 Bag Id -> Bag Id -> Bag Id
    forall a. Bag a -> Bag a -> Bag a
    `unionBags` HsWrapper -> Bag Id
    go HsWrapper
    w2
       go (WpFun HsWrapper
    _ HsWrapper
    w Scaled Mult
    _)       = HsWrapper -> Bag Id
    go HsWrapper
    w
       go HsWrapper
    WpHole              = Bag Id
    forall a. Bag a
    emptyBag
       go (WpCast  {})        = Bag Id
    forall a. Bag a
    emptyBag
       go (WpEvApp {})        = Bag Id
    forall a. Bag a
    emptyBag
       go (WpTyLam {})        = Bag Id
    forall a. Bag a
    emptyBag
       go (WpTyApp {})        = Bag Id
    forall a. Bag a
    emptyBag
       go (WpLet   {})        = Bag Id
    forall a. Bag a
    emptyBag
       go (WpMultCoercion {}) = Bag Id
    forall a. Bag a
    emptyBag

    collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
    -- Collect the outer lambda binders of a HsWrapper,
    -- stopping as soon as you get to a non-lambda binder
    collectHsWrapBinders :: HsWrapper -> ([Id], HsWrapper)
    collectHsWrapBinders HsWrapper
    wrap = HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
    go HsWrapper
    wrap []
      where
        -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
        go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
        go :: HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
    go (WpEvLam Id
    v)       [HsWrapper]
    wraps = Id -> ([Id], HsWrapper) -> ([Id], HsWrapper)
    forall {a} {b}. a -> ([a], b) -> ([a], b)
    add_lam Id
    v ([HsWrapper] -> ([Id], HsWrapper)
    gos [HsWrapper]
    wraps)
        go (WpTyLam Id
    v)       [HsWrapper]
    wraps = Id -> ([Id], HsWrapper) -> ([Id], HsWrapper)
    forall {a} {b}. a -> ([a], b) -> ([a], b)
    add_lam Id
    v ([HsWrapper] -> ([Id], HsWrapper)
    gos [HsWrapper]
    wraps)
        go (WpCompose HsWrapper
    w1 HsWrapper
    w2) [HsWrapper]
    wraps = HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
    go HsWrapper
    w1 (HsWrapper
    w2HsWrapper -> [HsWrapper] -> [HsWrapper]
    forall a. a -> [a] -> [a]
    :[HsWrapper]
    wraps)
        go HsWrapper
    wrap              [HsWrapper]
    wraps = ([], (HsWrapper -> HsWrapper -> HsWrapper)
    -> HsWrapper -> [HsWrapper] -> HsWrapper
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' HsWrapper -> HsWrapper -> HsWrapper
    (<.>) HsWrapper
    wrap [HsWrapper]
    wraps)

        gos :: [HsWrapper] -> ([Id], HsWrapper)
    gos []     = ([], HsWrapper
    WpHole)
        gos (HsWrapper
    w:[HsWrapper]
    ws) = HsWrapper -> [HsWrapper] -> ([Id], HsWrapper)
    go HsWrapper
    w [HsWrapper]
    ws

        add_lam :: a -> ([a], b) -> ([a], b)
    add_lam a
    v ([a]
    vs,b
    w) = (a
    va -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    vs, b
    w)

    {-
    ************************************************************************
    *                                                                      *
                      Evidence bindings
    *                                                                      *
    ************************************************************************
    -}

    data TcEvBinds
      = TcEvBinds           -- Mutable evidence bindings
           EvBindsVar       -- Mutable because they are updated "later"
                            --    when an implication constraint is solved

      | EvBinds             -- Immutable after zonking
           (Bag EvBind)

    data EvBindsVar
      = EvBindsVar {
          EvBindsVar -> Unique
    ebv_uniq :: Unique,
             -- The Unique is for debug printing only

          EvBindsVar -> IORef EvBindMap
    ebv_binds :: IORef EvBindMap,
          -- The main payload: the value-level evidence bindings
          --     (dictionaries etc)
          -- Some Given, some Wanted

          EvBindsVar -> IORef CoVarSet
    ebv_tcvs :: IORef CoVarSet
          -- The free Given coercion vars needed by Wanted coercions that
          -- are solved by filling in their HoleDest in-place. Since they
          -- don't appear in ebv_binds, we keep track of their free
          -- variables so that we can report unused given constraints
          -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
        }

      | CoEvBindsVar {  -- See Note [Coercion evidence only]

          -- See above for comments on ebv_uniq, ebv_tcvs
          ebv_uniq :: Unique,
          ebv_tcvs :: IORef CoVarSet
        }

    instance Data.Data TcEvBinds where
      -- Placeholder; we can't travers into TcEvBinds
      toConstr :: TcEvBinds -> Constr
    toConstr TcEvBinds
    _   = String -> Constr
    abstractConstr String
    "TcEvBinds"
      gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TcEvBinds
    gunfold forall b r. Data b => c (b -> r) -> c r
    _ forall r. r -> c r
    _  = String -> Constr -> c TcEvBinds
    forall a. HasCallStack => String -> a
    error String
    "gunfold"
      dataTypeOf :: TcEvBinds -> DataType
    dataTypeOf TcEvBinds
    _ = String -> DataType
    Data.mkNoRepType String
    "TcEvBinds"

    {- Note [Coercion evidence only]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Class constraints etc give rise to /term/ bindings for evidence, and
    we have nowhere to put term bindings in /types/.  So in some places we
    use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
    evidence bindings are allowed.  Notably ():

      - Places in types where we are solving kind constraints (all of which
        are equalities); see solveEqualities

      - When unifying forall-types
    -}

    isCoEvBindsVar :: EvBindsVar -> Bool
    isCoEvBindsVar :: EvBindsVar -> Bool
    isCoEvBindsVar (CoEvBindsVar {}) = Bool
    True
    isCoEvBindsVar (EvBindsVar {})   = Bool
    False

    -----------------
    newtype EvBindMap
      = EvBindMap {
           EvBindMap -> DVarEnv EvBind
    ev_bind_varenv :: DVarEnv EvBind
        }       -- Map from evidence variables to evidence terms
                -- We use @DVarEnv@ here to get deterministic ordering when we
                -- turn it into a Bag.
                -- If we don't do that, when we generate let bindings for
                -- dictionaries in dsTcEvBinds they will be generated in random
                -- order.
                --
                -- For example:
                --
                -- let $dEq = GHC.Classes.$fEqInt in
                -- let $$dNum = GHC.Num.$fNumInt in ...
                --
                -- vs
                --
                -- let $dNum = GHC.Num.$fNumInt in
                -- let $dEq = GHC.Classes.$fEqInt in ...
                --
                -- See Note [Deterministic UniqFM] in GHC.Types.Unique.DFM for explanation why
                -- @UniqFM@ can lead to nondeterministic order.

    emptyEvBindMap :: EvBindMap
    emptyEvBindMap :: EvBindMap
    emptyEvBindMap = EvBindMap { ev_bind_varenv :: DVarEnv EvBind
    ev_bind_varenv = DVarEnv EvBind
    forall a. DVarEnv a
    emptyDVarEnv }

    extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
    extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
    extendEvBinds EvBindMap
    bs EvBind
    ev_bind
      = EvBindMap { ev_bind_varenv :: DVarEnv EvBind
    ev_bind_varenv = DVarEnv EvBind -> Id -> EvBind -> DVarEnv EvBind
    forall a. DVarEnv a -> Id -> a -> DVarEnv a
    extendDVarEnv (EvBindMap -> DVarEnv EvBind
    ev_bind_varenv EvBindMap
    bs)
                                                   (EvBind -> Id
    eb_lhs EvBind
    ev_bind)
                                                   EvBind
    ev_bind }

    isEmptyEvBindMap :: EvBindMap -> Bool
    isEmptyEvBindMap :: EvBindMap -> Bool
    isEmptyEvBindMap (EvBindMap DVarEnv EvBind
    m) = DVarEnv EvBind -> Bool
    forall a. DVarEnv a -> Bool
    isEmptyDVarEnv DVarEnv EvBind
    m

    lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
    lookupEvBind :: EvBindMap -> Id -> Maybe EvBind
    lookupEvBind EvBindMap
    bs = DVarEnv EvBind -> Id -> Maybe EvBind
    forall a. DVarEnv a -> Id -> Maybe a
    lookupDVarEnv (EvBindMap -> DVarEnv EvBind
    ev_bind_varenv EvBindMap
    bs)

    evBindMapBinds :: EvBindMap -> Bag EvBind
    evBindMapBinds :: EvBindMap -> Bag EvBind
    evBindMapBinds = (EvBind -> Bag EvBind -> Bag EvBind)
    -> Bag EvBind -> EvBindMap -> Bag EvBind
    forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
    foldEvBindMap EvBind -> Bag EvBind -> Bag EvBind
    forall a. a -> Bag a -> Bag a
    consBag Bag EvBind
    forall a. Bag a
    emptyBag

    foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
    foldEvBindMap :: forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
    foldEvBindMap EvBind -> a -> a
    k a
    z EvBindMap
    bs = (EvBind -> a -> a) -> a -> DVarEnv EvBind -> a
    forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
    foldDVarEnv EvBind -> a -> a
    k a
    z (EvBindMap -> DVarEnv EvBind
    ev_bind_varenv EvBindMap
    bs)

    -- See Note [Deterministic UniqFM] to learn about nondeterminism.
    -- If you use this please provide a justification why it doesn't introduce
    -- nondeterminism.
    nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
    nonDetStrictFoldEvBindMap :: forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
    nonDetStrictFoldEvBindMap EvBind -> a -> a
    k a
    z EvBindMap
    bs = (EvBind -> a -> a) -> a -> DVarEnv EvBind -> a
    forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
    nonDetStrictFoldDVarEnv EvBind -> a -> a
    k a
    z (EvBindMap -> DVarEnv EvBind
    ev_bind_varenv EvBindMap
    bs)

    filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
    filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
    filterEvBindMap EvBind -> Bool
    k (EvBindMap { ev_bind_varenv :: EvBindMap -> DVarEnv EvBind
    ev_bind_varenv = DVarEnv EvBind
    env })
      = EvBindMap { ev_bind_varenv :: DVarEnv EvBind
    ev_bind_varenv = (EvBind -> Bool) -> DVarEnv EvBind -> DVarEnv EvBind
    forall a. (a -> Bool) -> DVarEnv a -> DVarEnv a
    filterDVarEnv EvBind -> Bool
    k DVarEnv EvBind
    env }

    evBindMapToVarSet :: EvBindMap -> VarSet
    evBindMapToVarSet :: EvBindMap -> CoVarSet
    evBindMapToVarSet (EvBindMap DVarEnv EvBind
    dve) = UniqFM Id Id -> CoVarSet
    forall a. UniqFM a a -> UniqSet a
    unsafeUFMToUniqSet ((EvBind -> Id) -> UniqFM Id EvBind -> UniqFM Id Id
    forall {k} elt1 elt2 (key :: k).
    (elt1 -> elt2) -> UniqFM key elt1 -> UniqFM key elt2
    mapUFM EvBind -> Id
    evBindVar (DVarEnv EvBind -> UniqFM Id EvBind
    forall {k} (key :: k) elt. UniqDFM key elt -> UniqFM key elt
    udfmToUfm DVarEnv EvBind
    dve))

    varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet
    varSetMinusEvBindMap :: CoVarSet -> EvBindMap -> CoVarSet
    varSetMinusEvBindMap CoVarSet
    vs (EvBindMap DVarEnv EvBind
    dve) = CoVarSet
    vs CoVarSet -> DVarEnv EvBind -> CoVarSet
    forall key b. UniqSet key -> UniqDFM key b -> UniqSet key
    `uniqSetMinusUDFM` DVarEnv EvBind
    dve

    instance Outputable EvBindMap where
      ppr :: EvBindMap -> SDoc
    ppr (EvBindMap DVarEnv EvBind
    m) = DVarEnv EvBind -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr DVarEnv EvBind
    m

    data EvBindInfo
      = EvBindGiven { -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
        }
      | EvBindWanted { EvBindInfo -> CanonicalEvidence
    ebi_canonical :: CanonicalEvidence -- See Note [Desugaring non-canonical evidence]
        }

    -----------------
    -- All evidence is bound by EvBinds; no side effects
    data EvBind
      = EvBind { EvBind -> Id
    eb_lhs  :: EvVar
               , EvBind -> EvTerm
    eb_rhs  :: EvTerm
               , EvBind -> EvBindInfo
    eb_info :: EvBindInfo
        }

    evBindVar :: EvBind -> EvVar
    evBindVar :: EvBind -> Id
    evBindVar = EvBind -> Id
    eb_lhs

    mkWantedEvBind :: EvVar -> CanonicalEvidence -> EvTerm -> EvBind
    mkWantedEvBind :: Id -> CanonicalEvidence -> EvTerm -> EvBind
    mkWantedEvBind Id
    ev CanonicalEvidence
    c EvTerm
    tm = EvBind { eb_info :: EvBindInfo
    eb_info = CanonicalEvidence -> EvBindInfo
    EvBindWanted CanonicalEvidence
    c, eb_lhs :: Id
    eb_lhs = Id
    ev, eb_rhs :: EvTerm
    eb_rhs = EvTerm
    tm }

    -- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
    mkGivenEvBind :: EvVar -> EvTerm -> EvBind
    mkGivenEvBind :: Id -> EvTerm -> EvBind
    mkGivenEvBind Id
    ev EvTerm
    tm = EvBind { eb_info :: EvBindInfo
    eb_info = EvBindInfo
    EvBindGiven, eb_lhs :: Id
    eb_lhs = Id
    ev, eb_rhs :: EvTerm
    eb_rhs = EvTerm
    tm }

    -- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
    -- Unfortunately, we cannot just do
    --   type EvTerm  = CoreExpr
    -- Because of staging problems issues around EvTypeable
    data EvTerm
      = EvExpr EvExpr

      | EvTypeable Type EvTypeable   -- Dictionary for (Typeable ty)

      | EvFun     -- /\as \ds. let binds in v
          { EvTerm -> [Id]
    et_tvs   :: [TyVar]
          , EvTerm -> [Id]
    et_given :: [EvVar]
          , EvTerm -> TcEvBinds
    et_binds :: TcEvBinds -- This field is why we need an EvFun
                                  -- constructor, and can't just use EvExpr
          , EvTerm -> Id
    et_body  :: EvVar }

      deriving Typeable EvTerm
    Typeable EvTerm =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> EvTerm -> c EvTerm)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c EvTerm)
    -> (EvTerm -> Constr)
    -> (EvTerm -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c EvTerm))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm))
    -> ((forall b. Data b => b -> b) -> EvTerm -> EvTerm)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> EvTerm -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> EvTerm -> r)
    -> (forall u. (forall d. Data d => d -> u) -> EvTerm -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> EvTerm -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm)
    -> Data EvTerm
    EvTerm -> Constr
    EvTerm -> DataType
    (forall b. Data b => b -> b) -> EvTerm -> EvTerm
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> EvTerm -> u
    forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTerm
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvTerm -> c EvTerm
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTerm)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvTerm -> c EvTerm
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvTerm -> c EvTerm
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTerm
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTerm
    $ctoConstr :: EvTerm -> Constr
    toConstr :: EvTerm -> Constr
    $cdataTypeOf :: EvTerm -> DataType
    dataTypeOf :: EvTerm -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTerm)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTerm)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTerm)
    $cgmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm
    gmapT :: (forall b. Data b => b -> b) -> EvTerm -> EvTerm
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EvTerm -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> EvTerm -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTerm -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTerm -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTerm -> m EvTerm
    Data.Data

    type EvExpr = CoreExpr

    -- An EvTerm is (usually) constructed by any of the constructors here
    -- and those more complicated ones who were moved to module GHC.Tc.Types.EvTerm

    -- | Any sort of evidence Id, including coercions
    evId ::  EvId -> EvExpr
    evId :: Id -> EvExpr
    evId = Id -> EvExpr
    forall b. Id -> Expr b
    Var

    -- coercion bindings
    -- See Note [Coercion evidence terms]
    evCoercion :: TcCoercion -> EvTerm
    evCoercion :: TcCoercion -> EvTerm
    evCoercion TcCoercion
    co = EvExpr -> EvTerm
    EvExpr (TcCoercion -> EvExpr
    forall b. TcCoercion -> Expr b
    Coercion TcCoercion
    co)

    -- | d |> co
    evCast :: EvExpr -> TcCoercion -> EvTerm
    evCast :: EvExpr -> TcCoercion -> EvTerm
    evCast EvExpr
    et TcCoercion
    tc | TcCoercion -> Bool
    isReflCo TcCoercion
    tc = EvExpr -> EvTerm
    EvExpr EvExpr
    et
                 | Bool
    otherwise   = EvExpr -> EvTerm
    EvExpr (EvExpr -> TcCoercion -> EvExpr
    forall b. Expr b -> TcCoercion -> Expr b
    Cast EvExpr
    et TcCoercion
    tc)

    -- Dictionary instance application
    evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
    evDFunApp :: Id -> [Mult] -> [EvExpr] -> EvTerm
    evDFunApp Id
    df [Mult]
    tys [EvExpr]
    ets = EvExpr -> EvTerm
    EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
    forall a b. (a -> b) -> a -> b
    $ Id -> EvExpr
    forall b. Id -> Expr b
    Var Id
    df EvExpr -> [Mult] -> EvExpr
    forall b. Expr b -> [Mult] -> Expr b
    `mkTyApps` [Mult]
    tys EvExpr -> [EvExpr] -> EvExpr
    forall b. Expr b -> [Expr b] -> Expr b
    `mkApps` [EvExpr]
    ets

    evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
    evDataConApp :: DataCon -> [Mult] -> [EvExpr] -> EvTerm
    evDataConApp DataCon
    dc [Mult]
    tys [EvExpr]
    ets = Id -> [Mult] -> [EvExpr] -> EvTerm
    evDFunApp (DataCon -> Id
    dataConWrapId DataCon
    dc) [Mult]
    tys [EvExpr]
    ets

    -- Selector id plus the types at which it
    -- should be instantiated, used for HasField
    -- dictionaries; see Note [HasField instances]
    -- in TcInterface
    evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
    evSelector :: Id -> [Mult] -> [EvExpr] -> EvExpr
    evSelector Id
    sel_id [Mult]
    tys [EvExpr]
    tms = Id -> EvExpr
    forall b. Id -> Expr b
    Var Id
    sel_id EvExpr -> [Mult] -> EvExpr
    forall b. Expr b -> [Mult] -> Expr b
    `mkTyApps` [Mult]
    tys EvExpr -> [EvExpr] -> EvExpr
    forall b. Expr b -> [Expr b] -> Expr b
    `mkApps` [EvExpr]
    tms

    -- Dictionary for (Typeable ty)
    evTypeable :: Type -> EvTypeable -> EvTerm
    evTypeable :: Mult -> EvTypeable -> EvTerm
    evTypeable = Mult -> EvTypeable -> EvTerm
    EvTypeable

    -- | Instructions on how to make a 'Typeable' dictionary.
    -- See Note [Typeable evidence terms]
    data EvTypeable
      = EvTypeableTyCon TyCon [EvTerm]
        -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
        -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
        -- the applied kinds..

      | EvTypeableTyApp EvTerm EvTerm
        -- ^ Dictionary for @Typeable (s t)@,
        -- given a dictionaries for @s@ and @t@.

      | EvTypeableTrFun EvTerm EvTerm EvTerm
        -- ^ Dictionary for @Typeable (s % w -> t)@,
        -- given a dictionaries for @w@, @s@, and @t@.

      | EvTypeableTyLit EvTerm
        -- ^ Dictionary for a type literal,
        -- e.g. @Typeable "foo"@ or @Typeable 3@
        -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
        -- (see #10348)
      deriving Typeable EvTypeable
    Typeable EvTypeable =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c EvTypeable)
    -> (EvTypeable -> Constr)
    -> (EvTypeable -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c EvTypeable))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c EvTypeable))
    -> ((forall b. Data b => b -> b) -> EvTypeable -> EvTypeable)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r)
    -> (forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> EvTypeable -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable)
    -> Data EvTypeable
    EvTypeable -> Constr
    EvTypeable -> DataType
    (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> EvTypeable -> u
    forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTypeable
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvTypeable -> c EvTypeable
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTypeable
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvTypeable
    $ctoConstr :: EvTypeable -> Constr
    toConstr :: EvTypeable -> Constr
    $cdataTypeOf :: EvTypeable -> DataType
    dataTypeOf :: EvTypeable -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvTypeable)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EvTypeable)
    $cgmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
    gmapT :: (forall b. Data b => b -> b) -> EvTypeable -> EvTypeable
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvTypeable -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> EvTypeable -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTypeable -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvTypeable -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvTypeable -> m EvTypeable
    Data.Data

    -- | Evidence for @CallStack@ implicit parameters.
    data EvCallStack
      -- See Note [Overview of implicit CallStacks]
      = EvCsEmpty
      | EvCsPushCall
            FastString   -- Usually the name of the function being called
                         --   but can also be "the literal 42"
                         --   or "an if-then-else expression", etc
            RealSrcSpan  -- Location of the call
            EvExpr       -- Rest of the stack
        -- ^ @EvCsPushCall origin loc stk@ represents a call from @origin@,
        --  occurring at @loc@, in a calling context @stk@.
      deriving Typeable EvCallStack
    Typeable EvCallStack =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c EvCallStack)
    -> (EvCallStack -> Constr)
    -> (EvCallStack -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c EvCallStack))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c EvCallStack))
    -> ((forall b. Data b => b -> b) -> EvCallStack -> EvCallStack)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r)
    -> (forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> EvCallStack -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack)
    -> Data EvCallStack
    EvCallStack -> Constr
    EvCallStack -> DataType
    (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> EvCallStack -> u
    forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvCallStack
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EvCallStack)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> EvCallStack -> c EvCallStack
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvCallStack
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EvCallStack
    $ctoConstr :: EvCallStack -> Constr
    toConstr :: EvCallStack -> Constr
    $cdataTypeOf :: EvCallStack -> DataType
    dataTypeOf :: EvCallStack -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EvCallStack)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EvCallStack)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EvCallStack)
    $cgmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
    gmapT :: (forall b. Data b => b -> b) -> EvCallStack -> EvCallStack
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EvCallStack -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> EvCallStack -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvCallStack -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EvCallStack -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EvCallStack -> m EvCallStack
    Data.Data

    {-
    ************************************************************************
    *                                                                      *
             Evidence for holes
    *                                                                      *
    ************************************************************************
    -}

    -- | Where to store evidence for expression holes
    -- See Note [Holes] in GHC.Tc.Types.Constraint
    data HoleExprRef = HER (IORef EvTerm)   -- ^ where to write the erroring expression
                           TcType           -- ^ expected type of that expression
                           Unique           -- ^ for debug output only

    instance Outputable HoleExprRef where
      ppr :: HoleExprRef -> SDoc
    ppr (HER IORef EvTerm
    _ Mult
    _ Unique
    u) = Unique -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Unique
    u

    instance Data.Data HoleExprRef where
      -- Placeholder; we can't traverse into HoleExprRef
      toConstr :: HoleExprRef -> Constr
    toConstr HoleExprRef
    _   = String -> Constr
    abstractConstr String
    "HoleExprRef"
      gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HoleExprRef
    gunfold forall b r. Data b => c (b -> r) -> c r
    _ forall r. r -> c r
    _  = String -> Constr -> c HoleExprRef
    forall a. HasCallStack => String -> a
    error String
    "gunfold"
      dataTypeOf :: HoleExprRef -> DataType
    dataTypeOf HoleExprRef
    _ = String -> DataType
    Data.mkNoRepType String
    "HoleExprRef"

    {-
    Note [Typeable evidence terms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The EvTypeable data type looks isomorphic to Type, but the EvTerms
    inside can be EvIds.  Eg
        f :: forall a. Typeable a => a -> TypeRep
        f x = typeRep (undefined :: Proxy [a])
    Here for the (Typeable [a]) dictionary passed to typeRep we make
    evidence
        dl :: Typeable [a] = EvTypeable [a]
                                (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
    where
        d :: Typeable a
    is the lambda-bound dictionary passed into f.

    Note [Coercion evidence terms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    A "coercion evidence term" takes one of these forms
       co_tm ::= EvId v           where v :: t1 ~# t2
               | EvCoercion co
               | EvCast co_tm co

    We do quite often need to get a TcCoercion from an EvTerm; see
    'evTermCoercion'.

    INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
    a coercion evidence term.  Consider for example
        [G] d :: F Int a
    If we have
        ax7 a :: F Int a ~ (a ~ Bool)
    then we do NOT generate the constraint
        [G] (d |> ax7 a) :: a ~ Bool
    because that does not satisfy the invariant (d is not a coercion variable).
    Instead we make a binding
        g1 :: a~Bool = g |> ax7 a
    and the constraint
        [G] g1 :: a~Bool
    See #7238 and Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint

    Note [EvBinds/EvTerm]
    ~~~~~~~~~~~~~~~~~~~~~
    How evidence is created and updated. Bindings for dictionaries,
    and coercions and implicit parameters are carried around in TcEvBinds
    which during constraint generation and simplification is always of the
    form (TcEvBinds ref). After constraint simplification is finished it
    will be transformed to t an (EvBinds ev_bag).

    Evidence for coercions *SHOULD* be filled in using the TcEvBinds
    However, all EvVars that correspond to *wanted* coercion terms in
    an EvBind must be mutable variables so that they can be readily
    inlined (by zonking) after constraint simplification is finished.

    Conclusion: a new wanted coercion variable should be made mutable.
    [Notice though that evidence variables that bind coercion terms
     from super classes will be "given" and hence rigid]

    Note [Overview of implicit CallStacks]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    (See https://gitlab.haskell.org/ghc/ghc/wikis/explicit-call-stack/implicit-locations)

    The goal of CallStack evidence terms is to reify locations
    in the program source as runtime values, without any support
    from the RTS. We accomplish this by assigning a special meaning
    to constraints of type GHC.Stack.Types.HasCallStack, an alias

      type HasCallStack = (?callStack :: CallStack)

    Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
    important) are solved in three steps:

    1. Explicit, user-written occurrences of `?stk :: CallStack`
       which have IPOccOrigin, are solved directly from the given IP,
       just like a regular IP; see GHC.Tc.Solver.Dict.tryInertDicts.

       For example, the occurrence of `?stk` in

         error :: (?stk :: CallStack) => String -> a
         error s = raise (ErrorCall (s ++ prettyCallStack ?stk))

       will be solved for the `?stk` in `error`s context as before.

    2. In a function call, instead of simply passing the given IP, we first
       append the current call-site to it. For example, consider a
       call to the callstack-aware `error` above.

         foo :: (?stk :: CallStack) => a
         foo = error "undefined!"

       Here we want to take the given `?stk` and append the current
       call-site, before passing it to `error`. In essence, we want to
       rewrite `foo "undefined!"` to

         let ?stk = pushCallStack <foo's location> ?stk
         in foo "undefined!"

       We achieve this as follows:

       * At a call of foo :: (?stk :: CallStack) => blah
         we emit a Wanted
            [W] d1 : IP "stk" CallStack
         with CtOrigin = OccurrenceOf "foo"

       * We /solve/ this constraint, in GHC.Tc.Solver.Dict.canDictNC
         by emitting a NEW Wanted
            [W] d2 :: IP "stk" CallStack
         with CtOrigin = IPOccOrigin

         and solve d1 = EvCsPushCall "foo" <foo's location> (EvId d1)

       * The new Wanted, for `d2` will be solved per rule (1), ie as a regular IP.

    3. We use the predicate isPushCallStackOrigin to identify whether we
       want to do (1) solve directly, or (2) push and then solve directly.
       Key point (see #19918): the CtOrigin where we want to push an item on the
       call stack can include IfThenElseOrigin etc, when RebindableSyntax is
       involved.  See the defn of fun_orig in GHC.Tc.Gen.App.tcInstFun; it is
       this CtOrigin that is pinned on the constraints generated by functions
       in the "expansion" for rebindable syntax. c.f. GHC.Rename.Expr
       Note [Handling overloaded and rebindable constructs]

    4. We default any insoluble CallStacks to the empty CallStack. Suppose
       `undefined` did not request a CallStack, ie

         undefinedNoStk :: a
         undefinedNoStk = error "undefined!"

       Under the usual IP rules, the new wanted from rule (2) would be
       insoluble as there's no given IP from which to solve it, so we
       would get an "unbound implicit parameter" error.

       We don't ever want to emit an insoluble CallStack IP, so we add a
       defaulting pass to default any remaining wanted CallStacks to the
       empty CallStack with the evidence term

         EvCsEmpty

       (see GHC.Tc.Solver.simplifyTopWanteds and GHC.Tc.Solver.defaultCallStacks)

    This provides a lightweight mechanism for building up call-stacks
    explicitly, but is notably limited by the fact that the stack will
    stop at the first function whose type does not include a CallStack IP.
    For example, using the above definition of `undefined`:

      head :: [a] -> a
      head []    = undefined
      head (x:_) = x

      g = head []

    the resulting CallStack will include the call to `undefined` in `head`
    and the call to `error` in `undefined`, but *not* the call to `head`
    in `g`, because `head` did not explicitly request a CallStack.

    Important Details:
    - GHC should NEVER report an insoluble CallStack constraint.

    - GHC should NEVER infer a CallStack constraint unless one was requested
      with a partial type signature (See GHC.Tc.Solver..pickQuantifiablePreds).

    - A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
      where the String is the name of the binder that is used at the
      SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
      package/module/file name, as well as the full source-span. Both
      CallStack and SrcLoc are kept abstract so only GHC can construct new
      values.

    - We will automatically solve any wanted CallStack regardless of the
      name of the IP, i.e.

        f = show (?stk :: CallStack)
        g = show (?loc :: CallStack)

      are both valid. However, we will only push new SrcLocs onto existing
      CallStacks when the IP names match, e.g. in

        head :: (?loc :: CallStack) => [a] -> a
        head [] = error (show (?stk :: CallStack))

      the printed CallStack will NOT include head's call-site. This reflects the
      standard scoping rules of implicit-parameters.

    - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
      The desugarer will need to unwrap the IP newtype before pushing a new
      call-site onto a given stack (See GHC.HsToCore.Binds.dsEvCallStack)

    - When we emit a new wanted CallStack from rule (2) we set its origin to
      `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
      (see GHC.Tc.Solver.Dict.tryInertDicts).

      This is a bit shady, but is how we ensure that the new wanted is
      solved like a regular IP.

    -}

    mkEvCast :: EvExpr -> TcCoercion -> EvTerm
    mkEvCast :: EvExpr -> TcCoercion -> EvTerm
    mkEvCast EvExpr
    ev TcCoercion
    lco
      | Bool -> SDoc -> Bool -> Bool
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr (TcCoercion -> Role
    coercionRole TcCoercion
    lco Role -> Role -> Bool
    forall a. Eq a => a -> a -> Bool
    == Role
    Representational)
                  ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Coercion of wrong role passed to mkEvCast:", EvExpr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvExpr
    ev, TcCoercion -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcCoercion
    lco]) (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $
        TcCoercion -> Bool
    isReflCo TcCoercion
    lco = EvExpr -> EvTerm
    EvExpr EvExpr
    ev
      | Bool
    otherwise    = EvExpr -> TcCoercion -> EvTerm
    evCast EvExpr
    ev TcCoercion
    lco

    mkEvScSelectors         -- Assume   class (..., D ty, ...) => C a b
      :: Class -> [TcType]  -- C ty1 ty2
      -> [(TcPredType,      -- D ty[ty1/a,ty2/b]
           EvExpr)          -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b]
         ]
    mkEvScSelectors :: Class -> [Mult] -> [(Mult, EvExpr)]
    mkEvScSelectors Class
    cls [Mult]
    tys
       = (Mult -> Int -> (Mult, EvExpr))
    -> [Mult] -> [Int] -> [(Mult, EvExpr)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Mult -> Int -> (Mult, EvExpr)
    mk_pr (Class -> [Mult] -> [Mult]
    immSuperClasses Class
    cls [Mult]
    tys) [Int
    0..]
      where
        mk_pr :: Mult -> Int -> (Mult, EvExpr)
    mk_pr Mult
    pred Int
    i = (Mult
    pred, Id -> EvExpr
    forall b. Id -> Expr b
    Var Id
    sc_sel_id EvExpr -> [Mult] -> EvExpr
    forall b. Expr b -> [Mult] -> Expr b
    `mkTyApps` [Mult]
    tys)
          where
            sc_sel_id :: Id
    sc_sel_id  = Class -> Int -> Id
    classSCSelId Class
    cls Int
    i -- Zero-indexed

    emptyTcEvBinds :: TcEvBinds
    emptyTcEvBinds :: TcEvBinds
    emptyTcEvBinds = Bag EvBind -> TcEvBinds
    EvBinds Bag EvBind
    forall a. Bag a
    emptyBag

    isEmptyTcEvBinds :: TcEvBinds -> Bool
    isEmptyTcEvBinds :: TcEvBinds -> Bool
    isEmptyTcEvBinds (EvBinds Bag EvBind
    b)    = Bag EvBind -> Bool
    forall a. Bag a -> Bool
    isEmptyBag Bag EvBind
    b
    isEmptyTcEvBinds (TcEvBinds {}) = String -> Bool
    forall a. HasCallStack => String -> a
    panic String
    "isEmptyTcEvBinds"

    evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
    -- Applied only to EvTerms of type (s~t)
    -- See Note [Coercion evidence terms]
    evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
    evTermCoercion_maybe EvTerm
    ev_term
      | EvExpr EvExpr
    e <- EvTerm
    ev_term = EvExpr -> Maybe TcCoercion
    go EvExpr
    e
      | Bool
    otherwise           = Maybe TcCoercion
    forall a. Maybe a
    Nothing
      where
        go :: EvExpr -> Maybe TcCoercion
        go :: EvExpr -> Maybe TcCoercion
    go (Var Id
    v)       = TcCoercion -> Maybe TcCoercion
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Id -> TcCoercion
    mkCoVarCo Id
    v)
        go (Coercion TcCoercion
    co) = TcCoercion -> Maybe TcCoercion
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TcCoercion
    co
        go (Cast EvExpr
    tm TcCoercion
    co)  = do { co' <- EvExpr -> Maybe TcCoercion
    go EvExpr
    tm
                              ; return (mkCoCast co' co) }
        go EvExpr
    _             = Maybe TcCoercion
    forall a. Maybe a
    Nothing

    evTermCoercion :: EvTerm -> TcCoercion
    evTermCoercion :: EvTerm -> TcCoercion
    evTermCoercion EvTerm
    tm = case EvTerm -> Maybe TcCoercion
    evTermCoercion_maybe EvTerm
    tm of
                          Just TcCoercion
    co -> TcCoercion
    co
                          Maybe TcCoercion
    Nothing -> String -> SDoc -> TcCoercion
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "evTermCoercion" (EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    tm)

    {- *********************************************************************
    *                                                                      *
                      Free variables
    *                                                                      *
    ********************************************************************* -}

    findNeededEvVars :: EvBindMap -> VarSet -> VarSet
    -- Find all the Given evidence needed by seeds,
    -- looking transitively through binds
    findNeededEvVars :: EvBindMap -> CoVarSet -> CoVarSet
    findNeededEvVars EvBindMap
    ev_binds CoVarSet
    seeds
      = (CoVarSet -> CoVarSet) -> CoVarSet -> CoVarSet
    transCloVarSet CoVarSet -> CoVarSet
    also_needs CoVarSet
    seeds
      where
       also_needs :: VarSet -> VarSet
       also_needs :: CoVarSet -> CoVarSet
    also_needs CoVarSet
    needs = (Id -> CoVarSet -> CoVarSet) -> CoVarSet -> CoVarSet -> CoVarSet
    forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
    nonDetStrictFoldUniqSet Id -> CoVarSet -> CoVarSet
    add CoVarSet
    emptyVarSet CoVarSet
    needs
         -- It's OK to use a non-deterministic fold here because we immediately
         -- forget about the ordering by creating a set

       add :: Var -> VarSet -> VarSet
       add :: Id -> CoVarSet -> CoVarSet
    add Id
    v CoVarSet
    needs
         | Just EvBind
    ev_bind <- EvBindMap -> Id -> Maybe EvBind
    lookupEvBind EvBindMap
    ev_binds Id
    v
         , EvBind { eb_info :: EvBind -> EvBindInfo
    eb_info = EvBindInfo
    EvBindGiven, eb_rhs :: EvBind -> EvTerm
    eb_rhs = EvTerm
    rhs } <- EvBind
    ev_bind
         = EvTerm -> CoVarSet
    evVarsOfTerm EvTerm
    rhs CoVarSet -> CoVarSet -> CoVarSet
    `unionVarSet` CoVarSet
    needs
         | Bool
    otherwise
         = CoVarSet
    needs

    evVarsOfTerm :: EvTerm -> VarSet
    evVarsOfTerm :: EvTerm -> CoVarSet
    evVarsOfTerm (EvExpr EvExpr
    e)         = InterestingVarFun -> EvExpr -> CoVarSet
    exprSomeFreeVars InterestingVarFun
    isEvVar EvExpr
    e
    evVarsOfTerm (EvTypeable Mult
    _ EvTypeable
    ev)  = EvTypeable -> CoVarSet
    evVarsOfTypeable EvTypeable
    ev
    evVarsOfTerm (EvFun {})         = CoVarSet
    emptyVarSet -- See Note [Free vars of EvFun]

    evVarsOfTerms :: [EvTerm] -> VarSet
    evVarsOfTerms :: [EvTerm] -> CoVarSet
    evVarsOfTerms = (EvTerm -> CoVarSet) -> [EvTerm] -> CoVarSet
    forall a. (a -> CoVarSet) -> [a] -> CoVarSet
    mapUnionVarSet EvTerm -> CoVarSet
    evVarsOfTerm

    evVarsOfTypeable :: EvTypeable -> VarSet
    evVarsOfTypeable :: EvTypeable -> CoVarSet
    evVarsOfTypeable EvTypeable
    ev =
      case EvTypeable
    ev of
        EvTypeableTyCon TyCon
    _ [EvTerm]
    e      -> (EvTerm -> CoVarSet) -> [EvTerm] -> CoVarSet
    forall a. (a -> CoVarSet) -> [a] -> CoVarSet
    mapUnionVarSet EvTerm -> CoVarSet
    evVarsOfTerm [EvTerm]
    e
        EvTypeableTyApp EvTerm
    e1 EvTerm
    e2    -> [EvTerm] -> CoVarSet
    evVarsOfTerms [EvTerm
    e1,EvTerm
    e2]
        EvTypeableTrFun EvTerm
    em EvTerm
    e1 EvTerm
    e2 -> [EvTerm] -> CoVarSet
    evVarsOfTerms [EvTerm
    em,EvTerm
    e1,EvTerm
    e2]
        EvTypeableTyLit EvTerm
    e        -> EvTerm -> CoVarSet
    evVarsOfTerm EvTerm
    e

    {- Note [Free vars of EvFun]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Finding the free vars of an EvFun is made tricky by the fact the
    bindings et_binds may be a mutable variable.  Fortunately, we
    can just squeeze by.  Here's how.

    * evVarsOfTerm is used only by GHC.Tc.Solver.neededEvVars.
    * Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
      ic_binds field of an Implication
    * So we can track usage via the processing for that implication,
      (see Note [Tracking redundant constraints] in GHC.Tc.Solver).
      We can ignore usage from the EvFun altogether.

    ************************************************************************
    *                                                                      *
                      Pretty printing
    *                                                                      *
    ************************************************************************
    -}

    instance Outputable HsWrapper where
      ppr :: HsWrapper -> SDoc
    ppr HsWrapper
    co_fn = HsWrapper -> (Bool -> SDoc) -> SDoc
    pprHsWrapper HsWrapper
    co_fn (SDoc -> Bool -> SDoc
    no_parens (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "<>"))

    pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
    -- With -fprint-typechecker-elaboration, print the wrapper
    --   otherwise just print what's inside
    -- The pp_thing_inside function takes Bool to say whether
    --    it's in a position that needs parens for a non-atomic thing
    pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
    pprHsWrapper HsWrapper
    wrap Bool -> SDoc
    pp_thing_inside
      = (SDocContext -> Bool) -> (Bool -> SDoc) -> SDoc
    forall a. (SDocContext -> a) -> (a -> SDoc) -> SDoc
    sdocOption SDocContext -> Bool
    sdocPrintTypecheckerElaboration ((Bool -> SDoc) -> SDoc) -> (Bool -> SDoc) -> SDoc
    forall a b. (a -> b) -> a -> b
    $ \case
          Bool
    True  -> (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    help Bool -> SDoc
    pp_thing_inside HsWrapper
    wrap Bool
    False
          Bool
    False -> Bool -> SDoc
    pp_thing_inside Bool
    False
      where
        help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
        -- True  <=> appears in function application position
        -- False <=> appears as body of let or lambda
        help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    help Bool -> SDoc
    it HsWrapper
    WpHole             = Bool -> SDoc
    it
        help Bool -> SDoc
    it (WpCompose HsWrapper
    f1 HsWrapper
    f2)  = (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    help ((Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    help Bool -> SDoc
    it HsWrapper
    f2) HsWrapper
    f1
        help Bool -> SDoc
    it (WpFun HsWrapper
    f1 HsWrapper
    f2 (Scaled Mult
    w Mult
    t1)) = SDoc -> Bool -> SDoc
    add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "\\(x" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc
    dcolon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    brackets (Mult -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Mult
    w) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> Mult -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Mult
    t1 SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ")." SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+>
                                                (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    help (\Bool
    _ -> Bool -> SDoc
    it Bool
    True SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
    help (\Bool
    _ -> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "x") HsWrapper
    f1 Bool
    True) HsWrapper
    f2 Bool
    False
        help Bool -> SDoc
    it (WpCast TcCoercion
    co)   = SDoc -> Bool -> SDoc
    add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [Bool -> SDoc
    it Bool
    False, Int -> SDoc -> SDoc
    nest Int
    2 (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "|>"
                                                  SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> TcCoercion -> SDoc
    pprParendCo TcCoercion
    co)]
        help Bool -> SDoc
    it (WpEvApp EvTerm
    id)  = SDoc -> Bool -> SDoc
    no_parens  (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [Bool -> SDoc
    it Bool
    True, Int -> SDoc -> SDoc
    nest Int
    2 (EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    id)]
        help Bool -> SDoc
    it (WpTyApp Mult
    ty)  = SDoc -> Bool -> SDoc
    no_parens  (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [Bool -> SDoc
    it Bool
    True, String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "@" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> Mult -> SDoc
    pprParendType Mult
    ty]
        help Bool -> SDoc
    it (WpEvLam Id
    id)  = SDoc -> Bool -> SDoc
    add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "\\" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> Id -> SDoc
    pprLamBndr Id
    id SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc
    forall doc. IsLine doc => doc
    dot, Bool -> SDoc
    it Bool
    False]
        help Bool -> SDoc
    it (WpTyLam Id
    tv)  = SDoc -> Bool -> SDoc
    add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "/\\" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> Id -> SDoc
    pprLamBndr Id
    tv SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc
    forall doc. IsLine doc => doc
    dot, Bool -> SDoc
    it Bool
    False]
        help Bool -> SDoc
    it (WpLet TcEvBinds
    binds) = SDoc -> Bool -> SDoc
    add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "let" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    braces (TcEvBinds -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcEvBinds
    binds), Bool -> SDoc
    it Bool
    False]
        help Bool -> SDoc
    it (WpMultCoercion TcCoercion
    co)   = SDoc -> Bool -> SDoc
    add_parens (SDoc -> Bool -> SDoc) -> SDoc -> Bool -> SDoc
    forall a b. (a -> b) -> a -> b
    $ [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [Bool -> SDoc
    it Bool
    False, Int -> SDoc -> SDoc
    nest Int
    2 (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "<multiplicity coercion>"
                                                  SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> TcCoercion -> SDoc
    pprParendCo TcCoercion
    co)]

    pprLamBndr :: Id -> SDoc
    pprLamBndr :: Id -> SDoc
    pprLamBndr Id
    v = BindingSite -> Id -> SDoc
    forall a. OutputableBndr a => BindingSite -> a -> SDoc
    pprBndr BindingSite
    LambdaBind Id
    v

    add_parens, no_parens :: SDoc -> Bool -> SDoc
    add_parens :: SDoc -> Bool -> SDoc
    add_parens SDoc
    d Bool
    True  = SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    parens SDoc
    d
    add_parens SDoc
    d Bool
    False = SDoc
    d
    no_parens :: SDoc -> Bool -> SDoc
    no_parens SDoc
    d Bool
    _ = SDoc
    d

    instance Outputable TcEvBinds where
      ppr :: TcEvBinds -> SDoc
    ppr (TcEvBinds EvBindsVar
    v) = EvBindsVar -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvBindsVar
    v
      ppr (EvBinds Bag EvBind
    bs)  = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "EvBinds" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    braces ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat ((EvBind -> SDoc) -> [EvBind] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map EvBind -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Bag EvBind -> [EvBind]
    forall a. Bag a -> [a]
    bagToList Bag EvBind
    bs)))

    instance Outputable EvBindsVar where
      ppr :: EvBindsVar -> SDoc
    ppr (EvBindsVar { ebv_uniq :: EvBindsVar -> Unique
    ebv_uniq = Unique
    u })
         = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "EvBindsVar" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    angleBrackets (Unique -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Unique
    u)
      ppr (CoEvBindsVar { ebv_uniq :: EvBindsVar -> Unique
    ebv_uniq = Unique
    u })
         = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "CoEvBindsVar" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    angleBrackets (Unique -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Unique
    u)

    instance Uniquable EvBindsVar where
      getUnique :: EvBindsVar -> Unique
    getUnique = EvBindsVar -> Unique
    ebv_uniq

    instance Outputable EvBind where
      ppr :: EvBind -> SDoc
    ppr (EvBind { eb_lhs :: EvBind -> Id
    eb_lhs = Id
    v, eb_rhs :: EvBind -> EvTerm
    eb_rhs = EvTerm
    e, eb_info :: EvBind -> EvBindInfo
    eb_info = EvBindInfo
    info })
         = [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep [ SDoc
    pp_gw SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    v
               , Int -> SDoc -> SDoc
    nest Int
    2 (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $ SDoc
    forall doc. IsLine doc => doc
    equals SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    e ]
          -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
         where
           pp_gw :: SDoc
    pp_gw = SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    brackets (SDoc -> SDoc) -> SDoc -> SDoc
    forall a b. (a -> b) -> a -> b
    $ case EvBindInfo
    info of
               EvBindGiven{}  -> Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    'G'
               EvBindWanted{} -> Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    'W'

    instance Outputable EvTerm where
      ppr :: EvTerm -> SDoc
    ppr (EvExpr EvExpr
    e)         = EvExpr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvExpr
    e
      ppr (EvTypeable Mult
    ty EvTypeable
    ev) = EvTypeable -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTypeable
    ev SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    dcolon SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Typeable" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Mult -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Mult
    ty
      ppr (EvFun { et_tvs :: EvTerm -> [Id]
    et_tvs = [Id]
    tvs, et_given :: EvTerm -> [Id]
    et_given = [Id]
    gs, et_binds :: EvTerm -> TcEvBinds
    et_binds = TcEvBinds
    bs, et_body :: EvTerm -> Id
    et_body = Id
    w })
          = SDoc -> Int -> SDoc -> SDoc
    hang (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "\\" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [SDoc] -> SDoc
    forall doc. IsLine doc => [doc] -> doc
    sep ((Id -> SDoc) -> [Id] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map Id -> SDoc
    pprLamBndr ([Id]
    tvs [Id] -> [Id] -> [Id]
    forall a. [a] -> [a] -> [a]
    ++ [Id]
    gs)) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    arrow)
               Int
    2 (TcEvBinds -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcEvBinds
    bs SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Id -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Id
    w)   -- Not very pretty

    instance Outputable EvCallStack where
      ppr :: EvCallStack -> SDoc
    ppr EvCallStack
    EvCsEmpty
        = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "[]"
      ppr (EvCsPushCall FastString
    orig RealSrcSpan
    loc EvExpr
    tm)
        = (FastString, RealSrcSpan) -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (FastString
    orig,RealSrcSpan
    loc) SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    ":" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> EvExpr -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvExpr
    tm

    instance Outputable EvTypeable where
      ppr :: EvTypeable -> SDoc
    ppr (EvTypeableTyCon TyCon
    ts [EvTerm]
    _)     = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "TyCon" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> TyCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyCon
    ts
      ppr (EvTypeableTyApp EvTerm
    t1 EvTerm
    t2)    = SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    parens (EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    t1 SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    t2)
      ppr (EvTypeableTyLit EvTerm
    t1)       = String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "TyLit" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <> EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    t1
      ppr (EvTypeableTrFun EvTerm
    tm EvTerm
    t1 EvTerm
    t2) = SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc
    parens (EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    t1 SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    arr SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    t2)
        where
          arr :: SDoc
    arr = FunTyFlag -> Either Bool SDoc -> SDoc
    pprArrowWithMultiplicity FunTyFlag
    visArgTypeLike (SDoc -> Either Bool SDoc
    forall a b. b -> Either a b
    Right (EvTerm -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr EvTerm
    tm))

    ----------------------------------------------------------------------
    -- Helper functions for dealing with IP newtype-dictionaries
    ----------------------------------------------------------------------

    -- | Create a 'Coercion' that unwraps an implicit-parameter
    -- dictionary to expose the underlying value.
    -- We expect the 'Type' to have the form `IP sym ty`,
    -- and return a 'Coercion' `co :: IP sym ty ~ ty`
    unwrapIP :: Type -> CoercionR
    unwrapIP :: Mult -> TcCoercion
    unwrapIP Mult
    ty =
      case TyCon -> Maybe ([Id], Mult, CoAxiom Unbranched)
    unwrapNewTyCon_maybe TyCon
    tc of
        Just ([Id]
    _,Mult
    _,CoAxiom Unbranched
    ax) -> Role -> CoAxiom Unbranched -> [Mult] -> [TcCoercion] -> TcCoercion
    mkUnbranchedAxInstCo Role
    Representational CoAxiom Unbranched
    ax [Mult]
    tys []
        Maybe ([Id], Mult, CoAxiom Unbranched)
    Nothing       -> String -> SDoc -> TcCoercion
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "unwrapIP" (SDoc -> TcCoercion) -> SDoc -> TcCoercion
    forall a b. (a -> b) -> a -> b
    $
                           String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "The dictionary for" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc -> SDoc
    quotes (TyCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyCon
    tc)
                             SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "is not a newtype!"
      where
      (TyCon
    tc, [Mult]
    tys) = Mult -> (TyCon, [Mult])
    splitTyConApp Mult
    ty

    -- | Create a 'Coercion' that wraps a value in an implicit-parameter
    -- dictionary. See 'unwrapIP'.
    wrapIP :: Type -> CoercionR
    wrapIP :: Mult -> TcCoercion
    wrapIP Mult
    ty = TcCoercion -> TcCoercion
    mkSymCo (Mult -> TcCoercion
    unwrapIP Mult
    ty)

    ----------------------------------------------------------------------
    -- A datatype used to pass information when desugaring quotations
    ----------------------------------------------------------------------

    -- We have to pass a `EvVar` and `Type` into `dsBracket` so that the
    -- correct evidence and types are applied to all the TH combinators.
    -- This data type bundles them up together with some convenience methods.
    --
    -- The EvVar is evidence for `Quote m`
    -- The Type is a metavariable for `m`
    --
    data QuoteWrapper = QuoteWrapper EvVar Type deriving Typeable QuoteWrapper
    Typeable QuoteWrapper =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c QuoteWrapper)
    -> (QuoteWrapper -> Constr)
    -> (QuoteWrapper -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c QuoteWrapper))
    -> ((forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r)
    -> (forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper)
    -> Data QuoteWrapper
    QuoteWrapper -> Constr
    QuoteWrapper -> DataType
    (forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u
    forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QuoteWrapper
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c QuoteWrapper)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> QuoteWrapper -> c QuoteWrapper
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QuoteWrapper
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QuoteWrapper
    $ctoConstr :: QuoteWrapper -> Constr
    toConstr :: QuoteWrapper -> Constr
    $cdataTypeOf :: QuoteWrapper -> DataType
    dataTypeOf :: QuoteWrapper -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QuoteWrapper)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c QuoteWrapper)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c QuoteWrapper)
    $cgmapT :: (forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper
    gmapT :: (forall b. Data b => b -> b) -> QuoteWrapper -> QuoteWrapper
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> QuoteWrapper -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> QuoteWrapper -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QuoteWrapper -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QuoteWrapper -> m QuoteWrapper
    Data.Data

    quoteWrapperTyVarTy :: QuoteWrapper -> Type
    quoteWrapperTyVarTy :: QuoteWrapper -> Mult
    quoteWrapperTyVarTy (QuoteWrapper Id
    _ Mult
    t) = Mult
    t

    -- | Convert the QuoteWrapper into a normal HsWrapper which can be used to
    -- apply its contents.
    applyQuoteWrapper :: QuoteWrapper -> HsWrapper
    applyQuoteWrapper :: QuoteWrapper -> HsWrapper
    applyQuoteWrapper (QuoteWrapper Id
    ev_var Mult
    m_var)
      = [Id] -> HsWrapper
    mkWpEvVarApps [Id
    ev_var] HsWrapper -> HsWrapper -> HsWrapper
    <.> [Mult] -> HsWrapper
    mkWpTyApps [Mult
    m_var]