-- ----------------------------------------------------

 data LiftingContext = LC Subst LiftCoEnv

   -- See Note [Optimising InstCo] in GHC.Core.Coercion.Opt

   -- We thus propagate the substitution from GHC.Core.Coercion.Opt here.

 -- (c) The University of Glasgow 2006

 {-# LANGUAGE CPP #-}

 where

 import GHC.Prelude

 Note [Coercion optimisation]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~

    Evidence normalization in Systtem FV (RTA'13)

    https://simon.peytonjones.org/evidence-normalization/

 The paper is also in the GHC repo, in docs/opt-coercion.

 * In the Simplifier, function `rebuild_go`, we use `isReflexiveCo` (which

   computes the type of the coercion) to eliminate reflexive coercion, just

   before we build a cast (e |> co).

 * We have a whole pass, `optCoProgram` that runs the coercion optimiser on all

   the coercions in the program.

   - We run it early in the optimisation pipeline

     (see GHC.Core.Opt.Pipeline.getCoreToDo).

 Note [Optimising coercion optimisation]

                                        (map (optCoAlt (is `extendInScopeSet` b)) alts)

 optCo :: InScopeSet -> Coercion -> Coercion

 optCoAlt :: InScopeSet -> CoreAlt -> CoreAlt

 optCoAlt is (Alt k bs e)

 %*                                                                      *

 %********************************************************************* -}

 -- ^ optCoercion applies a substitution to a coercion,

 --   *and* optimises it to reduce its size

   | debugIsOn

   = let out_co = opt_co1 lc NotSwapped co

         (Pair in_ty1  in_ty2,  in_role)  = coercionKindRole co

         CoreDoPasses [ simpl_gently

                      , runWhen do_specialise CoreDoSpecialising ],

         -- With -O do this after one run of the Simplifier.

         -- Without -O, just take what the desugarer produced

         runWhen do_co_opt CoreOptCoercion,

         if full_laziness then

         SimplPhase(..), isActive,

         seArityOpts, seCaseCase, seCaseFolding, seCaseMerge, seCastSwizzle,

         seDoEtaReduction, seEtaExpand, seFloatEnable, seInline, seNames,

         seRuleOpts, seRules, seUnfoldingOpts,

         mkSimplEnv, extendIdSubst, extendCvIdSubst,

         extendTvSubst, extendCvSubst,

 import GHC.Prelude

 import GHC.Core.FamInstEnv ( FamInstEnv )

 import GHC.Core.Opt.Arity ( ArityOpts(..) )

 import GHC.Core.Opt.Simplify.Monad

 seNames :: SimplEnv -> [String]

 seNames env = sm_names (seMode env)

 sePhase :: SimplEnv -> SimplPhase

 sePhase env = sm_phase (seMode env)

   , sm_rule_opts :: !RuleOpts

   , sm_case_folding :: !Bool

   , sm_case_merge :: !Bool

   }

 -- | See Note [SimplPhase]

       TickIt t cont    -> rebuild_go env (mkTick t expr) cont

       CastIt { sc_co = co, sc_cont = cont }

         | isReflexiveCoIgnoringMultiplicity co

         -> rebuild_go env expr cont

         | otherwise

         -> rebuild_go env (mkCast expr co) cont

            -- NB: mkCast implements the (Coercion co |> g) optimisation

   Now, if that binding is inlined, so that a=b=Int, we'd get

     RULE forall (c :: Int~Int). f (x |> c) = e

   and now when we simplify the LHS (GHC.Core.Opt.Simplify.Iteration.simplRules),

     RULE forall (c :: Int~Int). f (x |> <Int>) = e

   and then perhaps drop it altogether.  Now 'c' is unbound.

 Note [Cloning the template binders]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 -- | Subsystem configuration

 module GHC.Driver.Config

    , initEvalOpts

    , EvalStep(..)

    )

 import GHC.Driver.DynFlags

 import GHC.Core.SimpleOpt

 import GHCi.Message (EvalOpts(..))

 -- | Initialise Simple optimiser configuration from DynFlags

 initSimpleOpts :: DynFlags -> SimpleOpts

 initSimpleOpts dflags = SimpleOpts

 import GHC.Core.Opt.Simplify.Env ( FloatEnable(..), SimplMode(..), SimplPhase(..) )

 import GHC.Core.Opt.Simplify.Monad ( TopEnvConfig(..) )

 import GHC.Driver.Config.Core.Lint ( initLintPassResultConfig )

 import GHC.Driver.Config.Core.Rules ( initRuleOpts )

 import GHC.Driver.Config.Core.Opt.Arity ( initArityOpts )

   , sm_rule_opts = initRuleOpts dflags

   , sm_case_folding = gopt Opt_CaseFolding dflags

   , sm_case_merge = gopt Opt_CaseMerge dflags

   }

 initGentleSimplMode :: DynFlags -> SimplMode

         Language(..),

         FatalMessager, FlushOut(..),

         ProfAuto(..),

         dopt, dopt_set, dopt_unset,

         gopt, gopt_set, gopt_unset,

         wopt, wopt_set, wopt_unset,

 hasNoStateHack :: DynFlags -> Bool

 hasNoStateHack = gopt Opt_G_NoStateHack

 -- | Test whether a 'DumpFlag' is set

 dopt :: DumpFlag -> DynFlags -> Bool

 dopt = getDumpFlagFrom verbosity dumpFlags

         FatalMessager, FlushOut(..),

         ProfAuto(..),

         glasgowExtsFlags,

         dopt, dopt_set, dopt_unset,

         gopt, gopt_set, gopt_unset, setGeneralFlag', unSetGeneralFlag',

         wopt, wopt_set, wopt_unset,

 GHC.Core.Class

 GHC.Core.Coercion

 GHC.Core.Coercion.Axiom

 GHC.Core.ConLike

 GHC.Core.DataCon

 GHC.Core.FVs

 GHC.Core.Class

 GHC.Core.Coercion

 GHC.Core.Coercion.Axiom

 GHC.Core.ConLike

 GHC.Core.DataCon

 GHC.Core.FVs

       = ($fApplicativeReaderT6 @s @r)

         `cast` (forall (a ::~ <*>_N) (b ::~ <*>_N).

                 <a>_R

                 :: Coercible

                      (forall a b. a -> ReaderT r (ST s) b -> r -> STRep s a)

                      (forall a b. a -> ReaderT r (ST s) b -> ReaderT r (ST s) a))

       = ($fApplicativeReaderT1 @s @r)

         `cast` (forall (a ::~ <*>_N) (b ::~ <*>_N).

                 <ReaderT r (ST s) a>_R

                 :: Coercible

                      (forall a b.

                       ReaderT r (ST s) a -> ReaderT r (ST s) b -> r -> STRep s a)

       = ($fApplicativeReaderT7 @s @r)

         `cast` (forall (a ::~ <*>_N) (b ::~ <*>_N).

                 <a -> b>_R

                 :: Coercible

                      (forall a b. (a -> b) -> ReaderT r (ST s) a -> r -> STRep s b)

                      (forall a b. (a -> b) -> ReaderT r (ST s) a -> ReaderT r (ST s) b))

         `cast` (forall (a ::~ <*>_N) (b ::~ <*>_N) (c ::~ <*>_N).

                 <a -> b -> c>_R

                 ->_R <ReaderT r (ST s) a>_R

                 :: Coercible

                      (forall a b c.

                       (a -> b -> c)

       $fApplicativeReaderT_$cpure @(ST s) @r $dApplicative

       = ($fApplicativeReaderT5 @s @r)

         `cast` (forall (a ::~ <*>_N).

                 :: Coercible

                      (forall a. a -> r -> STRep s a)

                      (forall a. a -> ReaderT r (ST s) a))

       $fMonadReaderT_$creturn @(ST s) @r $dMonad

       = ($fApplicativeReaderT5 @s @r)

         `cast` (forall (a ::~ <*>_N).

                 :: Coercible

                      (forall a. a -> r -> STRep s a)

                      (forall a. a -> ReaderT r (ST s) a))

            ($dMonadAbstractIOST :: MonadAbstractIOST (ReaderT Int (ST s))).

       useAbstractMonad @(ReaderT Int (ST s)) $dMonadAbstractIOST

       = (useAbstractMonad1 @s)

                 :: Coercible

                      (Int -> Int -> STRep s Int) (Int -> ReaderT Int (ST s) Int))