    module GHC.Tc.Solver.Rewrite(
       rewrite, rewriteForErrors, rewriteArgsNom,
       rewriteType
     ) where

    import GHC.Prelude

    import GHC.Core.TyCo.Ppr ( pprTyVar )
    import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters),
                          TcPluginRewriter, TcPluginRewriteResult(..),
                          RewriteEnv(..),
                          runTcPluginM )
    import GHC.Tc.Types.Constraint
    import GHC.Core.Predicate
    import GHC.Tc.Utils.TcType
    import GHC.Core.Type
    import GHC.Tc.Types.Evidence
    import GHC.Core.TyCon
    import GHC.Core.TyCo.Rep   -- performs delicate algorithm on types
    import GHC.Core.Coercion
    import GHC.Core.Reduction
    import GHC.Types.Unique.FM
    import GHC.Types.Var
    import GHC.Types.Var.Set
    import GHC.Types.Var.Env
    import GHC.Driver.DynFlags
    import GHC.Utils.Outputable
    import GHC.Utils.Panic
    import GHC.Tc.Solver.Monad as TcS

    import GHC.Utils.Misc
    import GHC.Data.Maybe
    import GHC.Exts (oneShot)
    import Control.Monad
    import Control.Applicative (liftA3)
    import GHC.Builtin.Types (tYPETyCon)
    import Data.List ( find )
    import GHC.Data.List.Infinite (Infinite)
    import GHC.Data.Bag( listToBag )
    import qualified GHC.Data.List.Infinite as Inf

    {-
    ************************************************************************
    *                                                                      *
    *                RewriteEnv & RewriteM
    *             The rewriting environment & monad
    *                                                                      *
    ************************************************************************
    -}

    -- | The 'RewriteM' monad is a wrapper around 'TcS' with a 'RewriteEnv'
    newtype RewriteM a
      = RewriteM { forall a. RewriteM a -> RewriteEnv -> TcS a
    runRewriteM :: RewriteEnv -> TcS a }

    -- | Smart constructor for 'RewriteM', as describe in Note [The one-shot state
    -- monad trick] in "GHC.Utils.Monad".
    mkRewriteM :: (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM :: forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM RewriteEnv -> TcS a
    f = (RewriteEnv -> TcS a) -> RewriteM a
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    RewriteM ((RewriteEnv -> TcS a) -> RewriteEnv -> TcS a
    forall a b. (a -> b) -> a -> b
    oneShot RewriteEnv -> TcS a
    f)
    {-# INLINE mkRewriteM #-}

    instance Monad RewriteM where
      RewriteM a
    m >>= :: forall a b. RewriteM a -> (a -> RewriteM b) -> RewriteM b
    >>= a -> RewriteM b
    k  = (RewriteEnv -> TcS b) -> RewriteM b
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b)
    -> (RewriteEnv -> TcS b) -> RewriteM b
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env ->
                 do { a  <- RewriteM a -> RewriteEnv -> TcS a
    forall a. RewriteM a -> RewriteEnv -> TcS a
    runRewriteM RewriteM a
    m RewriteEnv
    env
                    ; runRewriteM (k a) env }

    instance Applicative RewriteM where
      pure :: forall a. a -> RewriteM a
    pure a
    x = (RewriteEnv -> TcS a) -> RewriteM a
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
    -> (RewriteEnv -> TcS a) -> RewriteM a
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    _ -> a -> TcS a
    forall a. a -> TcS a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x
      <*> :: forall a b. RewriteM (a -> b) -> RewriteM a -> RewriteM b
    (<*>) = RewriteM (a -> b) -> RewriteM a -> RewriteM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Functor RewriteM where
      fmap :: forall a b. (a -> b) -> RewriteM a -> RewriteM b
    fmap a -> b
    f (RewriteM RewriteEnv -> TcS a
    x) = (RewriteEnv -> TcS b) -> RewriteM b
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS b) -> RewriteM b)
    -> (RewriteEnv -> TcS b) -> RewriteM b
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env -> (a -> b) -> TcS a -> TcS b
    forall a b. (a -> b) -> TcS a -> TcS b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f (RewriteEnv -> TcS a
    x RewriteEnv
    env)

    instance HasDynFlags RewriteM where
      getDynFlags :: RewriteM DynFlags
    getDynFlags = TcS DynFlags -> RewriteM DynFlags
    forall a. TcS a -> RewriteM a
    liftTcS TcS DynFlags
    forall (m :: * -> *). HasDynFlags m => m DynFlags
    getDynFlags

    liftTcS :: TcS a -> RewriteM a
    liftTcS :: forall a. TcS a -> RewriteM a
    liftTcS TcS a
    thing_inside
      = (RewriteEnv -> TcS a) -> RewriteM a
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
    -> (RewriteEnv -> TcS a) -> RewriteM a
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    _ -> TcS a
    thing_inside

    -- convenient wrapper when you have a CtEvidence describing
    -- the rewriting operation
    runRewriteCtEv :: CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
    runRewriteCtEv :: forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
    runRewriteCtEv CtEvidence
    ev
      = CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
    forall a.
    CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
    runRewrite (CtEvidence -> CtLoc
    ctEvLoc CtEvidence
    ev) (CtEvidence -> CtFlavour
    ctEvFlavour CtEvidence
    ev) (CtEvidence -> EqRel
    ctEvEqRel CtEvidence
    ev)

    -- Run thing_inside (which does the rewriting)
    -- Also returns the set of Wanteds which rewrote a Wanted;
    -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
    runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
    runRewrite :: forall a.
    CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
    runRewrite CtLoc
    loc CtFlavour
    flav EqRel
    eq_rel RewriteM a
    thing_inside
      = do { rewriters_ref <- RewriterSet -> TcS (TcRef RewriterSet)
    forall a. a -> TcS (TcRef a)
    newTcRef RewriterSet
    emptyRewriterSet
           ; let fmode = RE { re_loc :: CtLoc
    re_loc       = CtLoc
    loc
                            , re_flavour :: CtFlavour
    re_flavour   = CtFlavour
    flav
                            , re_eq_rel :: EqRel
    re_eq_rel    = EqRel
    eq_rel
                            , re_rewriters :: TcRef RewriterSet
    re_rewriters = TcRef RewriterSet
    rewriters_ref }
           ; res <- runRewriteM thing_inside fmode
           ; rewriters <- readTcRef rewriters_ref
           ; return (res, rewriters) }

    traceRewriteM :: String -> SDoc -> RewriteM ()
    traceRewriteM :: String -> SDoc -> RewriteM ()
    traceRewriteM String
    herald SDoc
    doc = TcS () -> RewriteM ()
    forall a. TcS a -> RewriteM a
    liftTcS (TcS () -> RewriteM ()) -> TcS () -> RewriteM ()
    forall a b. (a -> b) -> a -> b
    $ String -> SDoc -> TcS ()
    traceTcS String
    herald SDoc
    doc
    {-# INLINE traceRewriteM #-}  -- see Note [INLINE conditional tracing utilities]

    getRewriteEnv :: RewriteM RewriteEnv
    getRewriteEnv :: RewriteM RewriteEnv
    getRewriteEnv
      = (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv)
    -> (RewriteEnv -> TcS RewriteEnv) -> RewriteM RewriteEnv
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env -> RewriteEnv -> TcS RewriteEnv
    forall a. a -> TcS a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RewriteEnv
    env

    getRewriteEnvField :: (RewriteEnv -> a) -> RewriteM a
    getRewriteEnvField :: forall a. (RewriteEnv -> a) -> RewriteM a
    getRewriteEnvField RewriteEnv -> a
    accessor
      = (RewriteEnv -> TcS a) -> RewriteM a
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
    -> (RewriteEnv -> TcS a) -> RewriteM a
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env -> a -> TcS a
    forall a. a -> TcS a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RewriteEnv -> a
    accessor RewriteEnv
    env)

    getEqRel :: RewriteM EqRel
    getEqRel :: RewriteM EqRel
    getEqRel = (RewriteEnv -> EqRel) -> RewriteM EqRel
    forall a. (RewriteEnv -> a) -> RewriteM a
    getRewriteEnvField RewriteEnv -> EqRel
    re_eq_rel

    getRole :: RewriteM Role
    getRole :: RewriteM Role
    getRole = EqRel -> Role
    eqRelRole (EqRel -> Role) -> RewriteM EqRel -> RewriteM Role
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RewriteM EqRel
    getEqRel

    getFlavour :: RewriteM CtFlavour
    getFlavour :: RewriteM CtFlavour
    getFlavour = (RewriteEnv -> CtFlavour) -> RewriteM CtFlavour
    forall a. (RewriteEnv -> a) -> RewriteM a
    getRewriteEnvField RewriteEnv -> CtFlavour
    re_flavour

    getFlavourRole :: RewriteM CtFlavourRole
    getFlavourRole :: RewriteM CtFlavourRole
    getFlavourRole
      = do { flavour <- RewriteM CtFlavour
    getFlavour
           ; eq_rel <- getEqRel
           ; return (flavour, eq_rel) }

    getLoc :: RewriteM CtLoc
    getLoc :: RewriteM CtLoc
    getLoc = (RewriteEnv -> CtLoc) -> RewriteM CtLoc
    forall a. (RewriteEnv -> a) -> RewriteM a
    getRewriteEnvField RewriteEnv -> CtLoc
    re_loc

    checkStackDepth :: Type -> RewriteM ()
    checkStackDepth :: Xi -> RewriteM ()
    checkStackDepth Xi
    ty
      = do { loc <- RewriteM CtLoc
    getLoc
           ; liftTcS $ checkReductionDepth loc ty }

    -- | Change the 'EqRel' in a 'RewriteM'.
    setEqRel :: EqRel -> RewriteM a -> RewriteM a
    setEqRel :: forall a. EqRel -> RewriteM a -> RewriteM a
    setEqRel EqRel
    new_eq_rel RewriteM a
    thing_inside
      = (RewriteEnv -> TcS a) -> RewriteM a
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
    -> (RewriteEnv -> TcS a) -> RewriteM a
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env ->
        if EqRel
    new_eq_rel EqRel -> EqRel -> Bool
    forall a. Eq a => a -> a -> Bool
    == RewriteEnv -> EqRel
    re_eq_rel RewriteEnv
    env
        then RewriteM a -> RewriteEnv -> TcS a
    forall a. RewriteM a -> RewriteEnv -> TcS a
    runRewriteM RewriteM a
    thing_inside RewriteEnv
    env
        else RewriteM a -> RewriteEnv -> TcS a
    forall a. RewriteM a -> RewriteEnv -> TcS a
    runRewriteM RewriteM a
    thing_inside (RewriteEnv
    env { re_eq_rel = new_eq_rel })
    {-# INLINE setEqRel #-}

    bumpDepth :: RewriteM a -> RewriteM a
    bumpDepth :: forall a. RewriteM a -> RewriteM a
    bumpDepth (RewriteM RewriteEnv -> TcS a
    thing_inside)
      = (RewriteEnv -> TcS a) -> RewriteM a
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    mkRewriteM ((RewriteEnv -> TcS a) -> RewriteM a)
    -> (RewriteEnv -> TcS a) -> RewriteM a
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env -> do
          -- bumpDepth can be called a lot during rewriting so we force the
          -- new env to avoid accumulating thunks.
          { let !env' :: RewriteEnv
    env' = RewriteEnv
    env { re_loc = bumpCtLocDepth (re_loc env) }
          ; RewriteEnv -> TcS a
    thing_inside RewriteEnv
    env' }

    -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
    -- Precondition: the CtEvidence is a CtWanted of an equality
    recordRewriter :: CtEvidence -> RewriteM ()
    recordRewriter :: CtEvidence -> RewriteM ()
    recordRewriter (CtWanted { ctev_dest :: CtEvidence -> TcEvDest
    ctev_dest = HoleDest CoercionHole
    hole })
      = (RewriteEnv -> TcS ()) -> RewriteM ()
    forall a. (RewriteEnv -> TcS a) -> RewriteM a
    RewriteM ((RewriteEnv -> TcS ()) -> RewriteM ())
    -> (RewriteEnv -> TcS ()) -> RewriteM ()
    forall a b. (a -> b) -> a -> b
    $ \RewriteEnv
    env -> TcRef RewriterSet -> (RewriterSet -> RewriterSet) -> TcS ()
    forall a. TcRef a -> (a -> a) -> TcS ()
    updTcRef (RewriteEnv -> TcRef RewriterSet
    re_rewriters RewriteEnv
    env) (RewriterSet -> CoercionHole -> RewriterSet
    `addRewriter` CoercionHole
    hole)
    recordRewriter CtEvidence
    other = String -> SDoc -> RewriteM ()
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "recordRewriter" (CtEvidence -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CtEvidence
    other)

    {-
    Note [Rewriter EqRels]
    ~~~~~~~~~~~~~~~~~~~~~~~
    When rewriting, we need to know which equality relation -- nominal
    or representation -- we should be respecting. The only difference is
    that we rewrite variables by representational equalities when re_eq_rel
    is ReprEq, and that we unwrap newtypes when rewriting w.r.t.
    representational equality.

    Note [Rewriter CtLoc]
    ~~~~~~~~~~~~~~~~~~~~~~
    The rewriter does eager type-family reduction.
    Type families might loop, and we
    don't want GHC to do so. A natural solution is to have a bounded depth
    to these processes. A central difficulty is that such a solution isn't
    quite compositional. For example, say it takes F Int 10 steps to get to Bool.
    How many steps does it take to get from F Int -> F Int to Bool -> Bool?
    10? 20? What about getting from Const Char (F Int) to Char? 11? 1? Hard to
    know and hard to track. So, we punt, essentially. We store a CtLoc in
    the RewriteEnv and just update the environment when recurring. In the
    TyConApp case, where there may be multiple type families to rewrite,
    we just copy the current CtLoc into each branch. If any branch hits the
    stack limit, then the whole thing fails.

    A consequence of this is that setting the stack limits appropriately
    will be essentially impossible. So, the official recommendation if a
    stack limit is hit is to disable the check entirely. Otherwise, there
    will be baffling, unpredictable errors.

    Note [Phantoms in the rewriter]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Suppose we have

    data Proxy p = Proxy

    and we're rewriting (Proxy ty) w.r.t. ReprEq. Then, we know that `ty`
    is really irrelevant -- it will be ignored when solving for representational
    equality later on. So, we omit rewriting `ty` entirely. This may
    violate the expectation of "xi"s for a bit, but the canonicaliser will
    soon throw out the phantoms when decomposing a TyConApp. (Or, the
    canonicaliser will emit an insoluble, in which case we get
    a better error message anyway.)

    -}

    {- *********************************************************************
    *                                                                      *
    *      Externally callable rewriting functions                         *
    *                                                                      *
    ************************************************************************
    -}

    -- | See Note [Rewriting].
    -- If (xi, co, rewriters) <- rewrite mode ev ty, then co :: xi ~r ty
    -- where r is the role in @ev@.
    -- rewriters is the set of coercion holes that have been used to rewrite
    -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
    rewrite :: CtEvidence -> TcType
            -> TcS (Reduction, RewriterSet)
    rewrite :: CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
    rewrite CtEvidence
    ev Xi
    ty
      = do { String -> SDoc -> TcS ()
    traceTcS String
    "rewrite {" (Xi -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Xi
    ty)
           ; result@(redn, _) <- CtEvidence -> RewriteM Reduction -> TcS (Reduction, RewriterSet)
    forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
    runRewriteCtEv CtEvidence
    ev (Xi -> RewriteM Reduction
    rewrite_one Xi
    ty)
           ; traceTcS "rewrite }" (ppr $ reductionReducedType redn)
           ; return result }

    -- | See Note [Rewriting]
    -- `rewriteForErrors` is a variant of 'rewrite' that rewrites
    -- w.r.t. nominal equality only, as this is better than full rewriting
    -- for error messages. (This was important when we flirted with rewriting
    -- newtypes but perhaps less so now.)
    rewriteForErrors :: CtEvidence -> TcType
                     -> TcS (Reduction, RewriterSet)
    rewriteForErrors :: CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
    rewriteForErrors CtEvidence
    ev Xi
    ty
      = do { String -> SDoc -> TcS ()
    traceTcS String
    "rewriteForErrors {" (Xi -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Xi
    ty)
           ; result@(redn, rewriters) <-
               CtLoc
    -> CtFlavour
    -> EqRel
    -> RewriteM Reduction
    -> TcS (Reduction, RewriterSet)
    forall a.
    CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
    runRewrite (CtEvidence -> CtLoc
    ctEvLoc CtEvidence
    ev) (CtEvidence -> CtFlavour
    ctEvFlavour CtEvidence
    ev) EqRel
    NomEq (Xi -> RewriteM Reduction
    rewrite_one Xi
    ty)
           ; traceTcS "rewriteForErrors }" (ppr $ reductionReducedType redn)
           ; return $ case ctEvEqRel ev of
               EqRel
    NomEq -> (Reduction, RewriterSet)
    result
               EqRel
    ReprEq -> (Reduction -> Reduction
    mkSubRedn Reduction
    redn, RewriterSet
    rewriters) }

    -- See Note [Rewriting]
    rewriteArgsNom :: CtEvidence -> TyCon -> [TcType]
                   -> TcS (Reductions, RewriterSet)
    -- Externally-callable, hence runRewrite
    -- Rewrite a vector of types all at once; in fact they are
    -- always the arguments of type family or class, so
    --      ctEvFlavour ev = Nominal
    -- and we want to rewrite all at nominal role
    -- The kind passed in is the kind of the type family or class, call it T
    -- The kind of T args must be constant (i.e. not depend on the args)
    --
    -- Final return value returned which Wanteds rewrote another Wanted
    -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
    rewriteArgsNom :: CtEvidence -> TyCon -> [Xi] -> TcS (Reductions, RewriterSet)
    rewriteArgsNom CtEvidence
    ev TyCon
    tc [Xi]
    tys
      = do { String -> SDoc -> TcS ()
    traceTcS String
    "rewrite_args {" ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat ((Xi -> SDoc) -> [Xi] -> [SDoc]
    forall a b. (a -> b) -> [a] -> [b]
    map Xi -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Xi]
    tys))
           ; (ArgsReductions redns@(Reductions _ tys') kind_co, rewriters)
               <- CtEvidence
    -> RewriteM ArgsReductions -> TcS (ArgsReductions, RewriterSet)
    forall a. CtEvidence -> RewriteM a -> TcS (a, RewriterSet)
    runRewriteCtEv CtEvidence
    ev (TyCon -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions
    rewrite_args_tc TyCon
    tc Maybe (Infinite Role)
    forall a. Maybe a
    Nothing [Xi]
    tys)
           ; massert (isReflMCo kind_co)
           ; traceTcS "rewrite }" (vcat (map ppr tys'))
           ; return (redns, rewriters) }

    -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite
    -- a type w.r.t. any givens. It does not do type-family reduction. This
    -- will never emit new constraints. Call this when the inert set contains
    -- only givens.
    rewriteType :: CtLoc -> TcType -> TcS TcType
    rewriteType :: CtLoc -> Xi -> TcS Xi
    rewriteType CtLoc
    loc Xi
    ty
      = do { (redn, _) <- CtLoc
    -> CtFlavour
    -> EqRel
    -> RewriteM Reduction
    -> TcS (Reduction, RewriterSet)
    forall a.
    CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
    runRewrite CtLoc
    loc CtFlavour
    Given EqRel
    NomEq (RewriteM Reduction -> TcS (Reduction, RewriterSet))
    -> RewriteM Reduction -> TcS (Reduction, RewriterSet)
    forall a b. (a -> b) -> a -> b
    $
                           Xi -> RewriteM Reduction
    rewrite_one Xi
    ty
                         -- use Given flavor so that it is rewritten
                         -- only w.r.t. Givens, never Wanteds
                         -- (Shouldn't matter, if only Givens are present
                         -- anyway)
           ; return $ reductionReducedType redn }

    {- *********************************************************************
    *                                                                      *
    *           The main rewriting functions
    *                                                                      *
    ********************************************************************* -}

    {- Note [Rewriting]
    ~~~~~~~~~~~~~~~~~~~~
      rewrite ty  ==>  Reduction co xi
        where
          xi has no reducible type functions
             has no skolems that are mapped in the inert set
             has no filled-in metavariables
          co :: ty ~ xi (coercions in reductions are always left-to-right)

    Key invariants:
      (F0) co :: zonk(ty') ~ xi   where zonk(ty') ~ zonk(ty)
      (F1) typeKind(xi) succeeds and returns a fully zonked kind
      (F2) typeKind(xi) `eqType` zonk(typeKind(ty))

    Note that it is rewrite's job to try to reduce *every type function it sees*.

    Rewriting also:
      * zonks, removing any metavariables, and
      * applies the substitution embodied in the inert set

    Because rewriting zonks and the returned coercion ("co" above) is also
    zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead,
    we can rely on this fact:

      (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty)

    Note that the right-hand type of co is *always* precisely xi. The left-hand
    type may or may not be ty, however: if ty has unzonked filled-in metavariables,
    then the left-hand type of co will be the zonk-equal to ty.
    It is for this reason that we occasionally have to explicitly zonk,
    when (co :: ty ~ xi) is important even before we zonk the whole program.
    For example, see the RTRNotFollowed case in rewriteTyVar.

    Why have these invariants on rewriting? Because we sometimes use typeKind
    during canonicalisation, and we want this kind to be zonked (e.g., see
    GHC.Tc.Solver.Equality.canEqCanLHS).

    Rewriting is always homogeneous. That is, the kind of the result of rewriting is
    always the same as the kind of the input, modulo zonking. More formally:

      (F2) zonk(typeKind(ty)) `eqType` typeKind(xi)

    This invariant means that the kind of a rewritten type might not itself be rewritten.

    Note that we prefer to leave type synonyms unexpanded when possible,
    so when the rewriter encounters one, it first asks whether its
    transitive expansion contains any type function applications or is
    forgetful -- that is, omits one or more type variables in its RHS.  If so,
    it expands the synonym and proceeds; if not, it simply returns the
    unexpanded synonym. See also Note [Rewriting synonyms].

    Where do we actually perform rewriting within a type? See Note [Rewritable] in
    GHC.Tc.Solver.InertSet.

    Note [rewrite_args performance]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    In programs with lots of type-level evaluation, rewrite_args becomes
    part of a tight loop. For example, see test perf/compiler/T9872a, which
    calls rewrite_args a whopping 7,106,808 times. It is thus important
    that rewrite_args be efficient.

    Performance testing showed that the current implementation is indeed
    efficient. It's critically important that zipWithAndUnzipM be
    specialized to TcS, and it's also quite helpful to actually `inline`
    it. On test T9872a, here are the allocation stats (Dec 16, 2014):

     * Unspecialized, uninlined:     8,472,613,440 bytes allocated in the heap
     * Specialized, uninlined:       6,639,253,488 bytes allocated in the heap
     * Specialized, inlined:         6,281,539,792 bytes allocated in the heap

    To improve performance even further, rewrite_args_nom is split off
    from rewrite_args, as nominal equality is the common case. This would
    be natural to write using mapAndUnzipM, but even inlined, that function
    is not as performant as a hand-written loop.

     * mapAndUnzipM, inlined:        7,463,047,432 bytes allocated in the heap
     * hand-written recursion:       5,848,602,848 bytes allocated in the heap

    If you make any change here, pay close attention to the T9872{a,b,c} tests
    and T5321Fun.

    If we need to make this yet more performant, a possible way forward is to
    duplicate the rewriter code for the nominal case, and make that case
    faster. This doesn't seem quite worth it, yet.

    Note [rewrite_exact_fam_app performance]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Once we've got a rewritten rhs, we extend the famapp-cache to record
    the result. Doing so can save lots of work when the same redex shows up more
    than once. Note that we record the link from the redex all the way to its
    *final* value, not just the single step reduction.

    If we can reduce the family application right away (the first call
    to try_to_reduce), we do *not* add to the cache. There are two possibilities
    here: 1) we just read the result from the cache, or 2) we used one type
    family instance. In either case, recording the result in the cache doesn't
    save much effort the next time around. And adding to the cache here is
    actually disastrous: it more than doubles the allocations for T9872a. So
    we skip adding to the cache here.
    -}

    {-# INLINE rewrite_args_tc #-}
    rewrite_args_tc
      :: TyCon         -- T
      -> Maybe (Infinite Role)  -- Nothing: ambient role is Nominal; all args are Nominal
                       -- Otherwise: no assumptions; use roles provided
      -> [Type]
      -> RewriteM ArgsReductions -- See the commentary on rewrite_args
    rewrite_args_tc :: TyCon -> Maybe (Infinite Role) -> [Xi] -> RewriteM ArgsReductions
    rewrite_args_tc TyCon
    tc = [PiTyBinder]
    -> Bool
    -> Xi
    -> TcTyCoVarSet
    -> Maybe (Infinite Role)
    -> [Xi]
    -> RewriteM ArgsReductions
    rewrite_args [PiTyBinder]
    all_bndrs Bool
    any_named_bndrs Xi
    inner_ki TcTyCoVarSet
    emptyVarSet
      -- NB: TyCon kinds are always closed
      where
      -- There are many bang patterns in here. It's been observed that they
      -- greatly improve performance of an optimized build.
      -- The T9872 test cases are good witnesses of this fact.

        ([PiTyBinder]
    bndrs, Bool
    named)
          = [TyConBinder] -> ([PiTyBinder], Bool)
    ty_con_binders_ty_binders' (TyCon -> [TyConBinder]
    tyConBinders TyCon
    tc)
        -- it's possible that the result kind has arrows (for, e.g., a type family)
        -- so we must split it
        ([PiTyBinder]
    inner_bndrs, Xi
    inner_ki, Bool
    inner_named) = Xi -> ([PiTyBinder], Xi, Bool)
    split_pi_tys' (TyCon -> Xi
    tyConResKind TyCon
    tc)
        !all_bndrs :: [PiTyBinder]
    all_bndrs                           = [PiTyBinder]
    bndrs [PiTyBinder] -> [PiTyBinder] -> [PiTyBinder]
    forall a. [a] -> [a] -> [a]
    `chkAppend` [PiTyBinder]
    inner_bndrs
        !any_named_bndrs :: Bool
    any_named_bndrs                     = Bool
    named Bool -> Bool -> Bool
    || Bool
    inner_named
        -- NB: Those bangs there drop allocations in T9872{a,c,d} by 8%.

    {-# INLINE rewrite_args #-}
    rewrite_args :: [PiTyBinder] -> Bool -- Binders, and True iff any of them are
                                         -- named.
                 -> Kind -> TcTyCoVarSet -- function kind; kind's free vars
                 -> Maybe (Infinite Role) -> [Type]    -- these are in 1-to-1 correspondence
                                              -- Nothing: use all Nominal
                 -> RewriteM ArgsReductions
    -- This function returns ArgsReductions (Reductions cos xis) res_co
    --   coercions: co_i :: ty_i ~ xi_i, at roles given
    --   types:     xi_i
    --   coercion:  res_co :: typeKind(fun tys) ~N typeKind(fun xis)
    -- That is, the result coercion relates the kind of some function (whose kind is
    -- passed as the first parameter) instantiated at tys to the kind of that
    -- function instantiated at the xis. This is useful in keeping rewriting
    -- homogeneous. The list of roles must be at least as long as the list of
    -- types.
    rewrite_args :: [PiTyBinder]
    -> Bool
    -> Xi
    -> TcTyCoVarSet
    -> Maybe (Infinite Role)
    -> [Xi]
    -> RewriteM ArgsReductions
    rewrite_args [PiTyBinder]
    orig_binders
                 Bool
    any_named_bndrs
                 Xi
    orig_inner_ki
                 TcTyCoVarSet
    orig_fvs
                 Maybe (Infinite Role)
    orig_m_roles
                 [Xi]
    orig_tys
      = case (Maybe (Infinite Role)
    orig_m_roles, Bool
    any_named_bndrs) of
          (Maybe (Infinite Role)
    Nothing, Bool
    False) -> [Xi] -> RewriteM ArgsReductions
    rewrite_args_fast [Xi]
    orig_tys
          (Maybe (Infinite Role), Bool)
    _ -> [PiTyBinder]
    -> Xi
    -> TcTyCoVarSet
    -> Infinite Role
    -> [Xi]
    -> RewriteM ArgsReductions
    rewrite_args_slow [PiTyBinder]
    orig_binders Xi
    orig_inner_ki TcTyCoVarSet
    orig_fvs Infinite Role
    orig_roles [Xi]
    orig_tys
            where orig_roles :: Infinite Role
    orig_roles = Infinite Role -> Maybe (Infinite Role) -> Infinite Role
    forall a. a -> Maybe a -> a
    fromMaybe (Role -> Infinite Role
    forall a. a -> Infinite a
    Inf.repeat Role
    Nominal) Maybe (Infinite Role)
    orig_m_roles

    {-# INLINE rewrite_args_fast #-}
    -- | fast path rewrite_args, in which none of the binders are named and
    -- therefore we can avoid tracking a lifting context.
    rewrite_args_fast :: [Type] -> RewriteM ArgsReductions
    rewrite_args_fast :: [Xi] -> RewriteM ArgsReductions
    rewrite_args_fast [Xi]
    orig_tys
      = (Reductions -> ArgsReductions)
    -> RewriteM Reductions -> RewriteM ArgsReductions
    forall a b. (a -> b) -> RewriteM a -> RewriteM b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Reductions -> ArgsReductions
    finish ([Xi] -> RewriteM Reductions
    iterate [Xi]
    orig_tys)
      where

        iterate :: [Type] -> RewriteM Reductions
        iterate :: [Xi] -> RewriteM Reductions
    iterate (Xi
    ty : [Xi]
    tys) = do
          Reduction  co  xi  <- Xi -> RewriteM Reduction
    rewrite_one Xi
    ty
          Reductions cos xis <- iterate tys
          pure $ Reductions (co : cos) (xi : xis)
        iterate [] = Reductions -> RewriteM Reductions
    forall a. a -> RewriteM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Reductions -> RewriteM Reductions)
    -> Reductions -> RewriteM Reductions
    forall a b. (a -> b) -> a -> b
    $ [Coercion] -> [Xi] -> Reductions
    Reductions [] []

        {-# INLINE finish #-}
        finish :: Reductions -> ArgsReductions
        finish :: Reductions -> ArgsReductions
    finish Reductions
    redns = Reductions -> MCoercionN -> ArgsReductions
    ArgsReductions Reductions
    redns MCoercionN
    MRefl

    {-# INLINE rewrite_args_slow #-}
    -- | Slow path, compared to rewrite_args_fast, because this one must track
    -- a lifting context.
    rewrite_args_slow :: [PiTyBinder] -> Kind -> TcTyCoVarSet
                      -> Infinite Role -> [Type]
                      -> RewriteM ArgsReductions
    rewrite_args_slow :: [PiTyBinder]
    -> Xi
    -> TcTyCoVarSet
    -> Infinite Role
    -> [Xi]
    -> RewriteM ArgsReductions
    rewrite_args_slow [PiTyBinder]
    binders Xi
    inner_ki TcTyCoVarSet
    fvs Infinite Role
    roles [Xi]
    tys
      = do { rewritten_args <- (Role -> Xi -> RewriteM Reduction)
    -> [Role] -> [Xi] -> RewriteM [Reduction]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Role -> Xi -> RewriteM Reduction
    rw (Infinite Role -> [Role]
    forall a. Infinite a -> [a]
    Inf.toList Infinite Role
    roles) [Xi]
    tys
           ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) }
      where
        {-# INLINE rw #-}
        rw :: Role -> Type -> RewriteM Reduction
        rw :: Role -> Xi -> RewriteM Reduction
    rw Role
    Nominal Xi
    ty
          = EqRel -> RewriteM Reduction -> RewriteM Reduction
    forall a. EqRel -> RewriteM a -> RewriteM a
    setEqRel EqRel
    NomEq (RewriteM Reduction -> RewriteM Reduction)
    -> RewriteM Reduction -> RewriteM Reduction
    forall a b. (a -> b) -> a -> b
    $
            Xi -> RewriteM Reduction
    rewrite_one Xi
    ty

        rw Role
    Representational Xi
    ty
          = EqRel -> RewriteM Reduction -> RewriteM Reduction
    forall a. EqRel -> RewriteM a -> RewriteM a
    setEqRel EqRel
    ReprEq (RewriteM Reduction -> RewriteM Reduction)
    -> RewriteM Reduction -> RewriteM Reduction
    forall a b. (a -> b) -> a -> b
    $
            Xi -> RewriteM Reduction
    rewrite_one Xi
    ty

        rw Role
    Phantom Xi
    ty
        -- See Note [Phantoms in the rewriter]
          = do { ty <- TcS Xi -> RewriteM Xi
    forall a. TcS a -> RewriteM a
    liftTcS (TcS Xi -> RewriteM Xi) -> TcS Xi -> RewriteM Xi
    forall a b. (a -> b) -> a -> b
    $ Xi -> TcS Xi
    zonkTcType Xi
    ty
               ; return $ mkReflRedn Phantom ty }

    ------------------
    rewrite_one :: TcType -> RewriteM Reduction
    -- Rewrite a type to get rid of type function applications, returning
    -- the new type-function-free type, and a collection of new equality
    -- constraints.  See Note [Rewriting] for more detail.
    --
    -- Postcondition:
    -- the role on the result coercion matches the EqRel in the RewriteEnv

    rewrite_one :: Xi -> RewriteM Reduction
    rewrite_one Xi
    ty
      | Just Xi
    ty' <- Xi -> Maybe Xi
    rewriterView Xi
    ty  -- See Note [Rewriting synonyms]
      = Xi -> RewriteM Reduction
    rewrite_one Xi
    ty'

    rewrite_one xi :: Xi
    xi@(LitTy {})
      = do { role <- RewriteM Role
    getRole
           ; return $ mkReflRedn role xi }

    rewrite_one (TyVarTy TcTyVar
    tv)
      = TcTyVar -> RewriteM Reduction
    rewriteTyVar TcTyVar
    tv

    rewrite_one (AppTy Xi
    ty1 Xi
    ty2)
      = Xi -> [Xi] -> RewriteM Reduction
    rewrite_app_tys Xi
    ty1 [Xi
    ty2]

    rewrite_one (TyConApp TyCon
    tc [Xi]
    tys)
      -- If it's a type family application, try to reduce it
      | TyCon -> Bool
    isTypeFamilyTyCon TyCon
    tc
      = TyCon -> [Xi] -> RewriteM Reduction
    rewrite_fam_app TyCon
    tc [Xi]
    tys

      | Bool
    otherwise -- We just recursively rewrite the arguments.
                  -- See Note [Do not rewrite newtypes]
      = TyCon -> [Xi] -> RewriteM Reduction
    rewrite_ty_con_app TyCon
    tc [Xi]
    tys

    rewrite_one (FunTy { ft_af :: Xi -> FunTyFlag
    ft_af = FunTyFlag
    vis, ft_mult :: Xi -> Xi
    ft_mult = Xi
    mult, ft_arg :: Xi -> Xi
    ft_arg = Xi
    ty1, ft_res :: Xi -> Xi
    ft_res = Xi
    ty2 })
      = do { arg_redn <- Xi -> RewriteM Reduction
    rewrite_one Xi
    ty1
           ; res_redn <- rewrite_one ty2

            -- Important: look at the *reduced* type, so that any unzonked variables
            -- in kinds are gone and the getRuntimeRep succeeds.
            -- cf. Note [Decomposing FunTy] in GHC.Tc.Solver.Equality.
           ; let arg_rep = HasDebugCallStack => Xi -> Xi
    Xi -> Xi
    getRuntimeRep (Reduction -> Xi
    reductionReducedType Reduction
    arg_redn)
                 res_rep = HasDebugCallStack => Xi -> Xi
    Xi -> Xi
    getRuntimeRep (Reduction -> Xi
    reductionReducedType Reduction
    res_redn)

           ; (w_redn, arg_rep_redn, res_rep_redn) <- setEqRel NomEq $
               liftA3 (,,) (rewrite_one mult)
                           (rewrite_one arg_rep)
                           (rewrite_one res_rep)
           ; role <- getRole

           ; let arg_rep_co = Reduction -> Coercion
    reductionCoercion Reduction
    arg_rep_redn
                    -- :: arg_rep ~ arg_rep_xi
                 arg_ki_co  = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    tYPETyCon [Coercion
    arg_rep_co]
                    -- :: TYPE arg_rep ~ TYPE arg_rep_xi
                 casted_arg_redn = Role -> Reduction -> Coercion -> Reduction
    mkCoherenceRightRedn Role
    role Reduction
    arg_redn Coercion
    arg_ki_co
                    -- :: ty1 ~> arg_xi |> arg_ki_co

                 res_rep_co = Reduction -> Coercion
    reductionCoercion Reduction
    res_rep_redn
                 res_ki_co  = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    tYPETyCon [Coercion
    res_rep_co]
                 casted_res_redn = Role -> Reduction -> Coercion -> Reduction
    mkCoherenceRightRedn Role
    role Reduction
    res_redn Coercion
    res_ki_co

              -- We must rewrite the representations, because that's what would
              -- be done if we used TyConApp instead of FunTy. These rewritten
              -- representations are seen only in casts of the arg and res, below.
              -- Forgetting this caused #19677.
           ; return $ mkFunRedn role vis w_redn casted_arg_redn casted_res_redn }

    rewrite_one ty :: Xi
    ty@(ForAllTy {})
    -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of
    -- the bound tyvar. Doing so will require carrying around a substitution
    -- and the usual substTyVarBndr-like silliness. Argh.

    -- We allow for-alls when, but only when, no type function
    -- applications inside the forall involve the bound type variables.
      = do { let ([TyVarBinder]
    bndrs, Xi
    rho) = Xi -> ([TyVarBinder], Xi)
    tcSplitForAllTyVarBinders Xi
    ty
           ; redn <- Xi -> RewriteM Reduction
    rewrite_one Xi
    rho
           ; return $ mkHomoForAllRedn bndrs redn }

    rewrite_one (CastTy Xi
    ty Coercion
    g)
      = do { redn <- Xi -> RewriteM Reduction
    rewrite_one Xi
    ty
           ; g'   <- rewrite_co g
           ; role <- getRole
           ; return $ mkCastRedn1 role ty g' redn }
          -- This calls castCoercionKind1.
          -- It makes a /big/ difference to call castCoercionKind1 not
          -- the more general castCoercionKind2.
          -- See Note [castCoercionKind1] in GHC.Core.Coercion

    rewrite_one (CoercionTy Coercion
    co)
      = do { co' <- Coercion -> RewriteM Coercion
    rewrite_co Coercion
    co
           ; role <- getRole
           ; return $ mkReflCoRedn role co' }

    -- | "Rewrite" a coercion. Really, just zonk it so we can uphold
    -- (F1) of Note [Rewriting]
    rewrite_co :: Coercion -> RewriteM Coercion
    rewrite_co :: Coercion -> RewriteM Coercion
    rewrite_co Coercion
    co = TcS Coercion -> RewriteM Coercion
    forall a. TcS a -> RewriteM a
    liftTcS (TcS Coercion -> RewriteM Coercion)
    -> TcS Coercion -> RewriteM Coercion
    forall a b. (a -> b) -> a -> b
    $ Coercion -> TcS Coercion
    zonkCo Coercion
    co

    -- | Rewrite a reduction, composing the resulting coercions.
    rewrite_reduction :: Reduction -> RewriteM Reduction
    rewrite_reduction :: Reduction -> RewriteM Reduction
    rewrite_reduction (Reduction Coercion
    co Xi
    xi)
      = do { redn <- RewriteM Reduction -> RewriteM Reduction
    forall a. RewriteM a -> RewriteM a
    bumpDepth (RewriteM Reduction -> RewriteM Reduction)
    -> RewriteM Reduction -> RewriteM Reduction
    forall a b. (a -> b) -> a -> b
    $ Xi -> RewriteM Reduction
    rewrite_one Xi
    xi
           ; return $ co `mkTransRedn` redn }

    -- rewrite (nested) AppTys
    rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction
    -- commoning up nested applications allows us to look up the function's kind
    -- only once. Without commoning up like this, we would spend a quadratic amount
    -- of time looking up functions' types
    rewrite_app_tys :: Xi -> [Xi] -> RewriteM Reduction
    rewrite_app_tys (AppTy Xi
    ty1 Xi
    ty2) [Xi]
    tys = Xi -> [Xi] -> RewriteM Reduction
    rewrite_app_tys Xi
    ty1 (Xi
    ty2Xi -> [Xi] -> [Xi]
    forall a. a -> [a] -> [a]
    :[Xi]
    tys)
    rewrite_app_tys Xi
    fun_ty [Xi]
    arg_tys
      = do { redn <- Xi -> RewriteM Reduction
    rewrite_one Xi
    fun_ty
           ; rewrite_app_ty_args redn arg_tys }

    -- Given a rewritten function (with the coercion produced by rewriting) and
    -- a bunch of unrewritten arguments, rewrite the arguments and apply.
    -- The coercion argument's role matches the role stored in the RewriteM monad.
    --
    -- The bang patterns used here were observed to improve performance. If you
    -- wish to remove them, be sure to check for regressions in allocations.
    rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction
    rewrite_app_ty_args :: Reduction -> [Xi] -> RewriteM Reduction
    rewrite_app_ty_args Reduction
    redn []
      -- this will be a common case when called from rewrite_fam_app, so shortcut
      = Reduction -> RewriteM Reduction
    forall a. a -> RewriteM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Reduction
    redn
    rewrite_app_ty_args fun_redn :: Reduction
    fun_redn@(Reduction Coercion
    fun_co Xi
    fun_xi) [Xi]
    arg_tys
      = do { het_redn <- case HasCallStack => Xi -> Maybe (TyCon, [Xi])
    Xi -> Maybe (TyCon, [Xi])
    tcSplitTyConApp_maybe Xi
    fun_xi of
               Just (TyCon
    tc, [Xi]
    xis) ->
                 do { let tc_roles :: Infinite Role
    tc_roles  = TyCon -> Infinite Role
    tyConRolesRepresentational TyCon
    tc
                          arg_roles :: Infinite Role
    arg_roles = [Xi] -> Infinite Role -> Infinite Role
    forall a b. [a] -> Infinite b -> Infinite b
    Inf.dropList [Xi]
    xis Infinite Role
    tc_roles
                    ; ArgsReductions (Reductions arg_cos arg_xis) kind_co
                        <- Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions
    rewrite_vector (HasDebugCallStack => Xi -> Xi
    Xi -> Xi
    typeKind Xi
    fun_xi) Infinite Role
    arg_roles [Xi]
    arg_tys

                      -- We start with a reduction of the form
                      --   fun_co :: ty ~ T xi_1 ... xi_n
                      -- and further arguments a_1, ..., a_m.
                      -- We rewrite these arguments, and obtain coercions:
                      --   arg_co_i :: a_i ~ zeta_i
                      -- Now, we need to apply fun_co to the arg_cos. The problem is
                      -- that using mkAppCo is wrong because that function expects
                      -- its second coercion to be Nominal, and the arg_cos might
                      -- not be. The solution is to use transitivity:
                      -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m
                    ; eq_rel <- getEqRel
                    ; let app_xi = TyCon -> [Xi] -> Xi
    mkTyConApp TyCon
    tc ([Xi]
    xis [Xi] -> [Xi] -> [Xi]
    forall a. [a] -> [a] -> [a]
    ++ [Xi]
    arg_xis)
                          app_co = case EqRel
    eq_rel of
                            EqRel
    NomEq  -> Coercion -> [Coercion] -> Coercion
    mkAppCos Coercion
    fun_co [Coercion]
    arg_cos
                            EqRel
    ReprEq -> Coercion -> [Coercion] -> Coercion
    mkAppCos Coercion
    fun_co ((Xi -> Coercion) -> [Xi] -> [Coercion]
    forall a b. (a -> b) -> [a] -> [b]
    map Xi -> Coercion
    mkNomReflCo [Xi]
    arg_tys)
                                      Coercion -> Coercion -> Coercion
    `mkTransCo`
                                      HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Representational TyCon
    tc
                                        ((Role -> Xi -> Coercion) -> [Role] -> [Xi] -> [Coercion]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Role -> Xi -> Coercion
    mkReflCo (Infinite Role -> [Role]
    forall a. Infinite a -> [a]
    Inf.toList Infinite Role
    tc_roles) [Xi]
    xis [Coercion] -> [Coercion] -> [Coercion]
    forall a. [a] -> [a] -> [a]
    ++ [Coercion]
    arg_cos)

                    ; return $
                        mkHetReduction
                          (mkReduction app_co app_xi )
                          kind_co }
               Maybe (TyCon, [Xi])
    Nothing ->
                 do { ArgsReductions redns kind_co
                        <- Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions
    rewrite_vector (HasDebugCallStack => Xi -> Xi
    Xi -> Xi
    typeKind Xi
    fun_xi) (Role -> Infinite Role
    forall a. a -> Infinite a
    Inf.repeat Role
    Nominal) [Xi]
    arg_tys
                    ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co }

           ; role <- getRole
           ; return (homogeniseHetRedn role het_redn) }

    rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction
    rewrite_ty_con_app :: TyCon -> [Xi] -> RewriteM Reduction
    rewrite_ty_con_app TyCon
    tc [Xi]
    tys
      = do { role <- RewriteM Role
    getRole
           ; let m_roles | Role
    Nominal <- Role
    role = Maybe (Infinite Role)
    forall a. Maybe a
    Nothing
                         | Bool
    otherwise       = Infinite Role -> Maybe (Infinite Role)
    forall a. a -> Maybe a
    Just (Infinite Role -> Maybe (Infinite Role))
    -> Infinite Role -> Maybe (Infinite Role)
    forall a b. (a -> b) -> a -> b
    $ Role -> TyCon -> Infinite Role
    tyConRolesX Role
    role TyCon
    tc
           ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys
           ; let tyconapp_redn
                    = Reduction -> MCoercionN -> HetReduction
    mkHetReduction
                        (Role -> TyCon -> Reductions -> Reduction
    mkTyConAppRedn Role
    role TyCon
    tc Reductions
    redns)
                        MCoercionN
    kind_co
           ; return $ homogeniseHetRedn role tyconapp_redn }

    -- Rewrite a vector (list of arguments).
    rewrite_vector :: Kind   -- of the function being applied to these arguments
                   -> Infinite Role -- If we're rewriting w.r.t. ReprEq, what roles do the
                             -- args have?
                   -> [Type] -- the args to rewrite
                   -> RewriteM ArgsReductions
    rewrite_vector :: Xi -> Infinite Role -> [Xi] -> RewriteM ArgsReductions
    rewrite_vector Xi
    ki Infinite Role
    roles [Xi]
    tys
      = do { eq_rel <- RewriteM EqRel
    getEqRel
           ; let mb_roles = case EqRel
    eq_rel of { EqRel
    NomEq -> Maybe (Infinite Role)
    forall a. Maybe a
    Nothing; EqRel
    ReprEq -> Infinite Role -> Maybe (Infinite Role)
    forall a. a -> Maybe a
    Just Infinite Role
    roles }
           ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys
           }
      where
        ([PiTyBinder]
    bndrs, Xi
    inner_ki, Bool
    any_named_bndrs) = Xi -> ([PiTyBinder], Xi, Bool)
    split_pi_tys' Xi
    ki
        fvs :: TcTyCoVarSet
    fvs                                = Xi -> TcTyCoVarSet
    tyCoVarsOfType Xi
    ki
    {-# INLINE rewrite_vector #-}

    {- Note [Do not rewrite newtypes]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We flirted with unwrapping newtypes in the rewriter -- see GHC.Tc.Solver.Equality
    Note [Unwrap newtypes first]. But that turned out to be a bad idea because
    of recursive newtypes, as that Note says.  So be careful if you re-add it!

    Note [Rewriting synonyms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~
    Not expanding synonyms aggressively improves error messages, and
    keeps types smaller. But we need to take care.

    Suppose
       type Syn a = Int
       type instance F Bool = Syn (F Bool)
       [G] F Bool ~ Syn (F Bool)

    If we don't expand the synonym, we'll get a spurious occurs-check
    failure. This is normally what occCheckExpand takes care of, but
    the LHS is a type family application, and occCheckExpand (already
    complex enough as it is) does not know how to expand to avoid
    a type family application.

    In addition, expanding the forgetful synonym like this
    will generally yield a *smaller* type. To wit, if we spot
    S ( ... F tys ... ), where S is forgetful, we don't want to bother
    doing hard work simplifying (F tys). We thus expand forgetful
    synonyms, but not others.

    isForgetfulSynTyCon returns True more often than it needs to, so
    we err on the side of more expansion.

    We also, of course, must expand type synonyms that mention type families,
    so those families can get reduced.

    ************************************************************************
    *                                                                      *
                 Rewriting a type-family application
    *                                                                      *
    ************************************************************************

    Note [How to normalise a family application]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Given an exactly saturated family application, how should we normalise it?
    This Note spells out the algorithm and its reasoning.

    First, we attempt to directly rewrite the type family application,
    without simplifying any of the arguments first, in an attempt to avoid
    doing unnecessary work.

    STEP 1a. Call the rewriting plugins. If any plugin rewrites the type family
    application, jump to FINISH.

    STEP 1b. Try the famapp-cache. If we get a cache hit, jump to FINISH.

    STEP 1c. Try top-level instances. Remember: we haven't simplified the arguments
      yet. Example:
        type instance F (Maybe a) = Int
        target: F (Maybe (G Bool))
      Instead of first trying to simplify (G Bool), we use the instance first. This
      avoids the work of simplifying G Bool.

      If an instance is found, jump to FINISH.

    STEP 2: At this point we rewrite all arguments. This might expose more
      information, which might allow plugins to make progress, or allow us to
      pick up a top-level instance.

    STEP 3. Try the inerts. Note that we try the inerts *after* rewriting the
      arguments, because the inerts will have rewritten LHSs.

      If an inert is found, jump to FINISH.

    Next, we try STEP 1 again, as we might be able to make further progress after
    having rewritten the arguments:

    STEP 4a. Query the rewriting plugins again.

      If any plugin supplies a rewriting, jump to FINISH.

    STEP 4b. Try the famapp-cache again.

      If we get a cache hit, jump to FINISH.

    STEP 4c. Try top-level instances again.

      If an instance is found, jump to FINISH.

    STEP 5: GIVEUP. No progress to be made. Return what we have. (Do not FINISH.)

    FINISH 1. We've made a reduction, but the new type may still have more
      work to do. So rewrite the new type.

    FINISH 2. Add the result to the famapp-cache, connecting the type we started
      with to the one we ended with.

    Because STEP 1{a,b,c} and STEP 4{a,b,c} happen the same way, they are abstracted into
    try_to_reduce.

    FINISH is naturally implemented in `finish`. But, Note [rewrite_exact_fam_app performance]
    tells us that we should not add to the famapp-cache after STEP 1. So `finish`
    is inlined in that case, and only FINISH 1 is performed.

    -}

    rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
      --   rewrite_fam_app            can be over-saturated
      --   rewrite_exact_fam_app      lifts out the application to top level
      -- Postcondition: Coercion :: Xi ~ F tys
    rewrite_fam_app :: TyCon -> [Xi] -> RewriteM Reduction
    rewrite_fam_app TyCon
    tc [Xi]
    tys  -- Can be over-saturated
        = Bool -> SDoc -> RewriteM Reduction -> RewriteM Reduction
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr ([Xi]
    tys [Xi] -> Arity -> Bool
    forall a. [a] -> Arity -> Bool
    `lengthAtLeast` TyCon -> Arity
    tyConArity TyCon
    tc)
                    (TyCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyCon
    tc SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Arity -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (TyCon -> Arity
    tyConArity TyCon
    tc) SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ [Xi] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Xi]
    tys) (RewriteM Reduction -> RewriteM Reduction)
    -> RewriteM Reduction -> RewriteM Reduction
    forall a b. (a -> b) -> a -> b
    $

                     -- Type functions are saturated
                     -- The type function might be *over* saturated
                     -- in which case the remaining arguments should
                     -- be dealt with by AppTys
          do { let ([Xi]
    tys1, [Xi]
    tys_rest) = Arity -> [Xi] -> ([Xi], [Xi])
    forall a. Arity -> [a] -> ([a], [a])
    splitAt (TyCon -> Arity
    tyConArity TyCon
    tc) [Xi]
    tys
             ; redn <- TyCon -> [Xi] -> RewriteM Reduction
    rewrite_exact_fam_app TyCon
    tc [Xi]
    tys1
             ; rewrite_app_ty_args redn tys_rest }

    -- the [TcType] exactly saturate the TyCon
    -- See Note [How to normalise a family application]
    rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction
    rewrite_exact_fam_app :: TyCon -> [Xi] -> RewriteM Reduction
    rewrite_exact_fam_app TyCon
    tc [Xi]
    tys
      = do { Xi -> RewriteM ()
    checkStackDepth (TyCon -> [Xi] -> Xi
    mkTyConApp TyCon
    tc [Xi]
    tys)

           -- Query the typechecking plugins for all their rewriting functions
           -- which apply to a type family application headed by the TyCon 'tc'.
           ; tc_rewriters <- TyCon -> RewriteM [TcPluginRewriter]
    getTcPluginRewritersForTyCon TyCon
    tc

           -- STEP 1. Try to reduce without reducing arguments first.
           ; result1 <- try_to_reduce tc tys tc_rewriters
           ; case result1 of
                 -- Don't use the cache;
                 -- See Note [rewrite_exact_fam_app performance]
             { Just Reduction
    redn -> Bool -> Reduction -> RewriteM Reduction
    finish Bool
    False Reduction
    redn
             ; Maybe Reduction
    Nothing ->

            -- That didn't work. So reduce the arguments, in STEP 2.
        do { eq_rel <- RewriteM EqRel
    getEqRel
              -- checking eq_rel == NomEq saves ~0.5% in T9872a
           ; ArgsReductions (Reductions cos xis) kind_co <-
                if eq_rel == NomEq
                then rewrite_args_tc tc Nothing tys
                else setEqRel NomEq $
                     rewrite_args_tc tc Nothing tys

             -- If we manage to rewrite the type family application after
             -- rewriting the arguments, we will need to compose these
             -- reductions.
             --
             -- We have:
             --
             --   arg_co_i :: ty_i ~ xi_i
             --   fam_co :: F xi_1 ... xi_n ~ zeta
             --
             -- The full reduction is obtained as a composite:
             --
             --   full_co :: F ty_1 ... ty_n ~ zeta
             --   full_co = F co_1 ... co_n ;; fam_co
           ; let
               role    = EqRel -> Role
    eqRelRole EqRel
    eq_rel
               args_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    role TyCon
    tc [Coercion]
    cos
           ;  let homogenise :: Reduction -> Reduction
                  homogenise Reduction
    redn
                    = Role -> HetReduction -> Reduction
    homogeniseHetRedn Role
    role
                    (HetReduction -> Reduction) -> HetReduction -> Reduction
    forall a b. (a -> b) -> a -> b
    $ Reduction -> MCoercionN -> HetReduction
    mkHetReduction
                        (Coercion
    args_co Coercion -> Reduction -> Reduction
    `mkTransRedn` Reduction
    redn)
                        MCoercionN
    kind_co

                  give_up :: Reduction
                  give_up = Reduction -> Reduction
    homogenise (Reduction -> Reduction) -> Reduction -> Reduction
    forall a b. (a -> b) -> a -> b
    $ Role -> Xi -> Reduction
    mkReflRedn Role
    role Xi
    reduced
                    where reduced :: Xi
    reduced = TyCon -> [Xi] -> Xi
    mkTyConApp TyCon
    tc [Xi]
    xis

             -- STEP 3: try the inerts
           ; flavour <- getFlavour
           ; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis
           ; case result2 of
             { Just (Reduction
    redn, (CtFlavour
    inert_flavour, EqRel
    inert_eq_rel))
                 -> do { String -> SDoc -> RewriteM ()
    traceRewriteM String
    "rewrite family application with inert"
                                    (TyCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyCon
    tc SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [Xi] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Xi]
    xis SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ Reduction -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Reduction
    redn)
                       ; Bool -> Reduction -> RewriteM Reduction
    finish (CtFlavour
    inert_flavour CtFlavour -> CtFlavour -> Bool
    forall a. Eq a => a -> a -> Bool
    == CtFlavour
    Given) (Reduction -> Reduction
    homogenise Reduction
    downgraded_redn) }
                   -- this will sometimes duplicate an inert in the cache,
                   -- but avoiding doing so had no impact on performance, and
                   -- it seems easier not to weed out that special case
                 where
                   inert_role :: Role
    inert_role      = EqRel -> Role
    eqRelRole EqRel
    inert_eq_rel
                   role :: Role
    role            = EqRel -> Role
    eqRelRole EqRel
    eq_rel
                   downgraded_redn :: Reduction
    downgraded_redn = Role -> Role -> Reduction -> Reduction
    downgradeRedn Role
    role Role
    inert_role Reduction
    redn

             ; Maybe (Reduction, CtFlavourRole)
    _ ->

             -- inerts didn't work. Try to reduce again, in STEP 4.
        do { result3 <- TyCon -> [Xi] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
    try_to_reduce TyCon
    tc [Xi]
    xis [TcPluginRewriter]
    tc_rewriters
           ; case result3 of
               Just Reduction
    redn -> Bool -> Reduction -> RewriteM Reduction
    finish Bool
    True (Reduction -> Reduction
    homogenise Reduction
    redn)
               -- we have made no progress at all: STEP 5 (GIVEUP).
               Maybe Reduction
    _         -> Reduction -> RewriteM Reduction
    forall a. a -> RewriteM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Reduction
    give_up }}}}}
      where
          -- call this if the above attempts made progress.
          -- This recursively rewrites the result and then adds to the cache
        finish :: Bool  -- add to the cache?
                        -- Precondition: True ==> input coercion has
                        --                        no coercion holes
               -> Reduction -> RewriteM Reduction
        finish :: Bool -> Reduction -> RewriteM Reduction
    finish Bool
    use_cache Reduction
    redn
          = do { -- rewrite the result: FINISH 1
                 final_redn <- Reduction -> RewriteM Reduction
    rewrite_reduction Reduction
    redn
               ; eq_rel <- getEqRel

                 -- extend the cache: FINISH 2
               ; when (use_cache && eq_rel == NomEq) $
                 -- the cache only wants Nominal eqs
                 liftTcS $ extendFamAppCache tc tys final_redn
               ; return final_redn }
        {-# INLINE finish #-}

    -- Returned coercion is input ~r output, where r is the role in the RewriteM monad
    -- See Note [How to normalise a family application]
    try_to_reduce :: TyCon -> [TcType] -> [TcPluginRewriter]
                  -> RewriteM (Maybe Reduction)
    try_to_reduce :: TyCon -> [Xi] -> [TcPluginRewriter] -> RewriteM (Maybe Reduction)
    try_to_reduce TyCon
    tc [Xi]
    tys [TcPluginRewriter]
    tc_rewriters
      = do { rewrite_env <- RewriteM RewriteEnv
    getRewriteEnv
           ; result <-
                liftTcS $ firstJustsM
                  [ runTcPluginRewriters rewrite_env tc_rewriters tys -- STEP 1a & STEP 4a
                  , lookupFamAppCache tc tys                          -- STEP 1b & STEP 4b
                  , matchFam tc tys ]                                 -- STEP 1c & STEP 4c
           ; traverse downgrade result }
      where
        -- The result above is always Nominal. We might want a Representational
        -- coercion; this downgrades (and prints, out of convenience).
        downgrade :: Reduction -> RewriteM Reduction
        downgrade :: Reduction -> RewriteM Reduction
    downgrade Reduction
    redn
          = do { String -> SDoc -> RewriteM ()
    traceRewriteM String
    "Eager T.F. reduction success" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
    forall a b. (a -> b) -> a -> b
    $
                 [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ TyCon -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TyCon
    tc
                      , [Xi] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Xi]
    tys
                      , Reduction -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Reduction
    redn
                      ]
               ; eq_rel <- RewriteM EqRel
    getEqRel
                  -- manually doing it this way avoids allocation in the vastly
                  -- common NomEq case
               ; case eq_rel of
                   EqRel
    NomEq  -> Reduction -> RewriteM Reduction
    forall a. a -> RewriteM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Reduction
    redn
                   EqRel
    ReprEq -> Reduction -> RewriteM Reduction
    forall a. a -> RewriteM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduction -> RewriteM Reduction)
    -> Reduction -> RewriteM Reduction
    forall a b. (a -> b) -> a -> b
    $ Reduction -> Reduction
    mkSubRedn Reduction
    redn }

    -- Retrieve all type-checking plugins that can rewrite a (saturated) type-family application
    -- headed by the given 'TyCon`.
    getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
    getTcPluginRewritersForTyCon :: TyCon -> RewriteM [TcPluginRewriter]
    getTcPluginRewritersForTyCon TyCon
    tc
      = TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]
    forall a. TcS a -> RewriteM a
    liftTcS (TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter])
    -> TcS [TcPluginRewriter] -> RewriteM [TcPluginRewriter]
    forall a b. (a -> b) -> a -> b
    $ do { rewriters <- TcGblEnv -> UniqFM TyCon [TcPluginRewriter]
    tcg_tc_plugin_rewriters (TcGblEnv -> UniqFM TyCon [TcPluginRewriter])
    -> TcS TcGblEnv -> TcS (UniqFM TyCon [TcPluginRewriter])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TcS TcGblEnv
    getGblEnv
                     ; return (lookupWithDefaultUFM rewriters [] tc) }

    -- Run a collection of rewriting functions obtained from type-checking plugins,
    -- querying in sequence if any plugin wants to rewrite the type family
    -- applied to the given arguments.
    --
    -- Note that the 'TcPluginRewriter's provided all pertain to the same type family
    -- (the 'TyCon' of which has been obtained ahead of calling this function).
    runTcPluginRewriters :: RewriteEnv
                         -> [TcPluginRewriter]
                         -> [TcType]
                         -> TcS (Maybe Reduction)
    runTcPluginRewriters :: RewriteEnv -> [TcPluginRewriter] -> [Xi] -> TcS (Maybe Reduction)
    runTcPluginRewriters RewriteEnv
    rewriteEnv [TcPluginRewriter]
    rewriterFunctions [Xi]
    tys
      | [TcPluginRewriter] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TcPluginRewriter]
    rewriterFunctions
      = Maybe Reduction -> TcS (Maybe Reduction)
    forall a. a -> TcS a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Reduction
    forall a. Maybe a
    Nothing -- short-circuit for common case
      | Bool
    otherwise
      = do { givens <- TcS [Ct]
    getInertGivens
           ; runRewriters givens rewriterFunctions }
      where
      runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
      runRewriters :: [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
    runRewriters [Ct]
    _ []
        = Maybe Reduction -> TcS (Maybe Reduction)
    forall a. a -> TcS a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Reduction
    forall a. Maybe a
    Nothing
      runRewriters [Ct]
    givens (TcPluginRewriter
    rewriter:[TcPluginRewriter]
    rewriters)
        = do
            rewriteResult <- TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult
    forall a. TcM a -> TcS a
    wrapTcS (TcM TcPluginRewriteResult -> TcS TcPluginRewriteResult)
    -> (TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult)
    -> TcPluginM TcPluginRewriteResult
    -> TcS TcPluginRewriteResult
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TcPluginM TcPluginRewriteResult -> TcM TcPluginRewriteResult
    forall a. TcPluginM a -> TcM a
    runTcPluginM (TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult)
    -> TcPluginM TcPluginRewriteResult -> TcS TcPluginRewriteResult
    forall a b. (a -> b) -> a -> b
    $ TcPluginRewriter
    rewriter RewriteEnv
    rewriteEnv [Ct]
    givens [Xi]
    tys
            case rewriteResult of
               TcPluginRewriteTo
                 { tcPluginReduction :: TcPluginRewriteResult -> Reduction
    tcPluginReduction    = Reduction
    redn
                 , tcRewriterNewWanteds :: TcPluginRewriteResult -> [Ct]
    tcRewriterNewWanteds = [Ct]
    wanteds
                 } -> do { Cts -> TcS ()
    emitWork ([Ct] -> Cts
    forall a. [a] -> Bag a
    listToBag [Ct]
    wanteds); Maybe Reduction -> TcS (Maybe Reduction)
    forall a. a -> TcS a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Reduction -> TcS (Maybe Reduction))
    -> Maybe Reduction -> TcS (Maybe Reduction)
    forall a b. (a -> b) -> a -> b
    $ Reduction -> Maybe Reduction
    forall a. a -> Maybe a
    Just Reduction
    redn }
               TcPluginNoRewrite {} -> [Ct] -> [TcPluginRewriter] -> TcS (Maybe Reduction)
    runRewriters [Ct]
    givens [TcPluginRewriter]
    rewriters

    {-
    ************************************************************************
    *                                                                      *
                 Rewriting a type variable
    *                                                                      *
    ********************************************************************* -}

    -- | The result of rewriting a tyvar "one step".
    data RewriteTvResult
      = RTRNotFollowed
          -- ^ The inert set doesn't make the tyvar equal to anything else

      | RTRFollowed !Reduction
          -- ^ The tyvar rewrites to a not-necessarily rewritten other type.
          -- The role is determined by the RewriteEnv.
          --
          -- With Quick Look, the returned TcType can be a polytype;
          -- that is, in the constraint solver, a unification variable
          -- can contain a polytype.  See GHC.Tc.Gen.App
          -- Note [Instantiation variables are short lived]

    rewriteTyVar :: TyVar -> RewriteM Reduction
    rewriteTyVar :: TcTyVar -> RewriteM Reduction
    rewriteTyVar TcTyVar
    tv
      = do { mb_yes <- TcTyVar -> RewriteM RewriteTvResult
    rewrite_tyvar1 TcTyVar
    tv
           ; case mb_yes of
               RTRFollowed Reduction
    redn -> Reduction -> RewriteM Reduction
    rewrite_reduction Reduction
    redn

               RewriteTvResult
    RTRNotFollowed   -- Done, but make sure the kind is zonked
                                -- Note [Rewriting] invariant (F0) and (F1)
                 -> do { tv' <- TcS TcTyVar -> RewriteM TcTyVar
    forall a. TcS a -> RewriteM a
    liftTcS (TcS TcTyVar -> RewriteM TcTyVar)
    -> TcS TcTyVar -> RewriteM TcTyVar
    forall a b. (a -> b) -> a -> b
    $ (Xi -> TcS Xi) -> TcTyVar -> TcS TcTyVar
    forall (m :: * -> *).
    Monad m =>
    (Xi -> m Xi) -> TcTyVar -> m TcTyVar
    updateTyVarKindM Xi -> TcS Xi
    zonkTcType TcTyVar
    tv
                       ; role <- getRole
                       ; let ty' = TcTyVar -> Xi
    mkTyVarTy TcTyVar
    tv'
                       ; return $ mkReflRedn role ty' } }

    rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
    -- "Rewriting" a type variable means to apply the substitution to it
    -- Specifically, look up the tyvar in
    --   * the internal MetaTyVar box
    --   * the inerts
    -- See also the documentation for RewriteTvResult

    rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult
    rewrite_tyvar1 TcTyVar
    tv
      = do { mb_ty <- TcS (Maybe Xi) -> RewriteM (Maybe Xi)
    forall a. TcS a -> RewriteM a
    liftTcS (TcS (Maybe Xi) -> RewriteM (Maybe Xi))
    -> TcS (Maybe Xi) -> RewriteM (Maybe Xi)
    forall a b. (a -> b) -> a -> b
    $ TcTyVar -> TcS (Maybe Xi)
    isFilledMetaTyVar_maybe TcTyVar
    tv
           ; case mb_ty of
               Just Xi
    ty -> do { String -> SDoc -> RewriteM ()
    traceRewriteM String
    "Following filled tyvar"
                                 (TcTyVar -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcTyVar
    tv SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    forall doc. IsLine doc => doc
    equals SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Xi -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Xi
    ty)
                             ; role <- RewriteM Role
    getRole
                             ; return $ RTRFollowed $
                                 mkReflRedn role ty }
               Maybe Xi
    Nothing -> do { String -> SDoc -> RewriteM ()
    traceRewriteM String
    "Unfilled tyvar" (TcTyVar -> SDoc
    pprTyVar TcTyVar
    tv)
                             ; fr <- RewriteM CtFlavourRole
    getFlavourRole
                             ; rewrite_tyvar2 tv fr } }

    rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
    -- The tyvar is not a filled-in meta-tyvar
    -- Try in the inert equalities
    -- See Definition [Applying a generalised substitution] in GHC.Tc.Solver.Monad
    -- See Note [Stability of rewriting] in GHC.Tc.Solver.Monad

    rewrite_tyvar2 :: TcTyVar -> CtFlavourRole -> RewriteM RewriteTvResult
    rewrite_tyvar2 TcTyVar
    tv fr :: CtFlavourRole
    fr@(CtFlavour
    _, EqRel
    eq_rel)
      = do { ieqs <- TcS InertEqs -> RewriteM InertEqs
    forall a. TcS a -> RewriteM a
    liftTcS (TcS InertEqs -> RewriteM InertEqs)
    -> TcS InertEqs -> RewriteM InertEqs
    forall a b. (a -> b) -> a -> b
    $ TcS InertEqs
    getInertEqs
           ; case lookupDVarEnv ieqs tv of
               Just EqualCtList
    equal_ct_list
                 | Just EqCt
    ct <- (EqCt -> Bool) -> EqualCtList -> Maybe EqCt
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find EqCt -> Bool
    can_rewrite EqualCtList
    equal_ct_list
                 , EqCt { eq_ev :: EqCt -> CtEvidence
    eq_ev = CtEvidence
    ctev, eq_lhs :: EqCt -> CanEqLHS
    eq_lhs = TyVarLHS TcTyVar
    tv
                        , eq_rhs :: EqCt -> Xi
    eq_rhs = Xi
    rhs_ty, eq_eq_rel :: EqCt -> EqRel
    eq_eq_rel = EqRel
    ct_eq_rel } <- EqCt
    ct
                 -> do { let wrw :: Bool
    wrw = CtEvidence -> Bool
    isWanted CtEvidence
    ctev
                       ; String -> SDoc -> RewriteM ()
    traceRewriteM String
    "Following inert tyvar" (SDoc -> RewriteM ()) -> SDoc -> RewriteM ()
    forall a b. (a -> b) -> a -> b
    $
                            [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ TcTyVar -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr TcTyVar
    tv SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    forall doc. IsLine doc => doc
    equals SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Xi -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Xi
    rhs_ty
                                 , CtEvidence -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr CtEvidence
    ctev
                                 , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "wanted_rewrite_wanted:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Bool -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Bool
    wrw ]
                       ; Bool -> RewriteM () -> RewriteM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    wrw (RewriteM () -> RewriteM ()) -> RewriteM () -> RewriteM ()
    forall a b. (a -> b) -> a -> b
    $ CtEvidence -> RewriteM ()
    recordRewriter CtEvidence
    ctev

                       ; let rewriting_co1 :: Coercion
    rewriting_co1 = HasDebugCallStack => CtEvidence -> Coercion
    CtEvidence -> Coercion
    ctEvCoercion CtEvidence
    ctev
                             rewriting_co :: Coercion
    rewriting_co  = case (EqRel
    ct_eq_rel, EqRel
    eq_rel) of
                                (EqRel
    ReprEq, EqRel
    _rel)  -> Bool -> Coercion -> Coercion
    forall a. HasCallStack => Bool -> a -> a
    assert (EqRel
    _rel EqRel -> EqRel -> Bool
    forall a. Eq a => a -> a -> Bool
    == EqRel
    ReprEq)
                                        -- if this assert fails, then
                                        -- eqCanRewriteFR answered incorrectly
                                                   Coercion
    rewriting_co1
                                (EqRel
    NomEq, EqRel
    NomEq)  -> Coercion
    rewriting_co1
                                (EqRel
    NomEq, EqRel
    ReprEq) -> HasDebugCallStack => Coercion -> Coercion
    Coercion -> Coercion
    mkSubCo Coercion
    rewriting_co1

                       ; RewriteTvResult -> RewriteM RewriteTvResult
    forall a. a -> RewriteM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RewriteTvResult -> RewriteM RewriteTvResult)
    -> RewriteTvResult -> RewriteM RewriteTvResult
    forall a b. (a -> b) -> a -> b
    $ Reduction -> RewriteTvResult
    RTRFollowed (Reduction -> RewriteTvResult) -> Reduction -> RewriteTvResult
    forall a b. (a -> b) -> a -> b
    $ Coercion -> Xi -> Reduction
    mkReduction Coercion
    rewriting_co Xi
    rhs_ty }

               Maybe EqualCtList
    _other -> RewriteTvResult -> RewriteM RewriteTvResult
    forall a. a -> RewriteM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RewriteTvResult
    RTRNotFollowed }

      where
        can_rewrite :: EqCt -> Bool
        can_rewrite :: EqCt -> Bool
    can_rewrite EqCt
    ct = EqCt -> CtFlavourRole
    eqCtFlavourRole EqCt
    ct CtFlavourRole -> CtFlavourRole -> Bool
    `eqCanRewriteFR` CtFlavourRole
    fr
          -- This is THE key call of eqCanRewriteFR

    {-
    Note [An alternative story for the inert substitution]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    (This entire note is just background, left here in case we ever want
     to return the previous state of affairs)

    We used (GHC 7.8) to have this story for the inert substitution inert_eqs

     * 'a' is not in fvs(ty)
     * They are *inert* in the weaker sense that there is no infinite chain of
       (i1 `eqCanRewrite` i2), (i2 `eqCanRewrite` i3), etc

    This means that rewriting must be recursive, but it does allow
      [G] a ~ [b]
      [G] b ~ Maybe c

    This avoids "saturating" the Givens, which can save a modest amount of work.
    It is easy to implement, in GHC.Tc.Solver.InertSet.kickOutRewritableLHS, by
    only kicking out an inert only if
            (a) the work item can rewrite the inert AND
            (b) the inert cannot rewrite the work item

    This is significantly harder to think about. It can save a LOT of work
    in occurs-check cases, but we don't care about them much.  #5837
    is an example, but it causes trouble only with the old (pre-Fall 2020)
    rewriting story. It is unclear if there is any gain w.r.t. to
    the new story.

    -}

    --------------------------------------
    -- Utilities

    -- | Like 'splitPiTys'' but comes with a 'Bool' which is 'True' iff there is at
    -- least one named binder.
    split_pi_tys' :: Type -> ([PiTyBinder], Type, Bool)
    split_pi_tys' :: Xi -> ([PiTyBinder], Xi, Bool)
    split_pi_tys' Xi
    ty = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
    split Xi
    ty Xi
    ty
      where
         -- put common cases first
      split :: Xi -> Xi -> ([PiTyBinder], Xi, Bool)
    split Xi
    _       (ForAllTy TyVarBinder
    b Xi
    res) = let -- This bang is necessary lest we see rather
                                           -- terrible reboxing, as noted in #19102.
                                           !([PiTyBinder]
    bs, Xi
    ty, Bool
    _) = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
    split Xi
    res Xi
    res
                                       in  (TyVarBinder -> PiTyBinder
    Named TyVarBinder
    b PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
    forall a. a -> [a] -> [a]
    : [PiTyBinder]
    bs, Xi
    ty, Bool
    True)
      split Xi
    _       (FunTy { ft_af :: Xi -> FunTyFlag
    ft_af = FunTyFlag
    af, ft_mult :: Xi -> Xi
    ft_mult = Xi
    w, ft_arg :: Xi -> Xi
    ft_arg = Xi
    arg, ft_res :: Xi -> Xi
    ft_res = Xi
    res })
                                     = let -- See #19102
                                           !([PiTyBinder]
    bs, Xi
    ty, Bool
    named) = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
    split Xi
    res Xi
    res
                                       in  (Scaled Xi -> FunTyFlag -> PiTyBinder
    Anon (Xi -> Xi -> Scaled Xi
    forall a. Xi -> a -> Scaled a
    mkScaled Xi
    w Xi
    arg) FunTyFlag
    af PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
    forall a. a -> [a] -> [a]
    : [PiTyBinder]
    bs, Xi
    ty, Bool
    named)

      split Xi
    orig_ty Xi
    ty | Just Xi
    ty' <- Xi -> Maybe Xi
    coreView Xi
    ty = Xi -> Xi -> ([PiTyBinder], Xi, Bool)
    split Xi
    orig_ty Xi
    ty'
      split Xi
    orig_ty Xi
    _                = ([], Xi
    orig_ty, Bool
    False)
    {-# INLINE split_pi_tys' #-}

    -- | Like 'tyConBindersPiTyBinders' but you also get a 'Bool' which is true iff
    -- there is at least one named binder.
    ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool)
    ty_con_binders_ty_binders' :: [TyConBinder] -> ([PiTyBinder], Bool)
    ty_con_binders_ty_binders' = (TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool))
    -> ([PiTyBinder], Bool) -> [TyConBinder] -> ([PiTyBinder], Bool)
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool)
    go ([], Bool
    False)
      where
        go :: TyConBinder -> ([PiTyBinder], Bool) -> ([PiTyBinder], Bool)
    go (Bndr TcTyVar
    tv (NamedTCB ForAllTyFlag
    vis)) ([PiTyBinder]
    bndrs, Bool
    _)
          = (TyVarBinder -> PiTyBinder
    Named (TcTyVar -> ForAllTyFlag -> TyVarBinder
    forall var argf. var -> argf -> VarBndr var argf
    Bndr TcTyVar
    tv ForAllTyFlag
    vis) PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
    forall a. a -> [a] -> [a]
    : [PiTyBinder]
    bndrs, Bool
    True)
        go (Bndr TcTyVar
    tv TyConBndrVis
    AnonTCB)   ([PiTyBinder]
    bndrs, Bool
    n)
          = (Scaled Xi -> FunTyFlag -> PiTyBinder
    Anon (Xi -> Scaled Xi
    forall a. a -> Scaled a
    tymult (TcTyVar -> Xi
    tyVarKind TcTyVar
    tv)) FunTyFlag
    FTF_T_T PiTyBinder -> [PiTyBinder] -> [PiTyBinder]
    forall a. a -> [a] -> [a]
    : [PiTyBinder]
    bndrs, Bool
    n)
        {-# INLINE go #-}
    {-# INLINE ty_con_binders_ty_binders' #-}