import GHC.Builtin.Types

 import GHC.Builtin.Types.Prim

 import GHC.Tc.Solver.InertSet (InertSet, emptyInert)

 import GHC.Types.CompleteMatch

 import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit

                             , fractionalLitFromRational

   ppr (TySt n inert) = ppr n <+> ppr inert

 initTyState :: TyState

 -- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These

 -- entries are possibly shared when we figure out that two variables must be

        ; let psig_theta = concatMap sig_inst_theta partial_sigs

        -- First do full-blown solving

        ; ev_binds_var <- TcM.newTcEvBinds

        ; psig_evs     <- newWanteds AnnOrigin psig_theta

        ; wanted_transformed

                solveWanteds (mkSimpleWC psig_evs `andWC` wanteds)

                -- psig_evs : see Note [Add signature contexts as wanteds]

        -- Find quant_pred_candidates, the predicates that

        -- we'll consider quantifying over

              -- Step 1 of Note [decideAndPromoteTyVars]

              -- Get candidate constraints, decide which we can potentially quantify

              can_quant = ctsPreds can_quant_cts

              -- Step 2 of Note [decideAndPromoteTyVars]

              -- Apply the monomorphism restriction

              (post_mr_quant, mr_no_quant) = applyMR dflags infer_mode can_quant

              -- The co_var_tvs are tvs mentioned in the types of covars or

              -- coercion holes. We can't quantify over these covars, so we

                                          ++ tau_tys ++ post_mr_quant)

              co_var_tvs = closeOverKinds co_vars

              -- We definitely can't quantify over them

              outer_tvs = outerLevelTyVars rhs_tclvl $

              -- Identify mono_tvs: the type variables that we must not quantify over

              mono_tvs_without_mr

              mono_tvs_with_mr

                = -- Even at top level, we don't quantify over type variables

                  -- mentioned in constraints that the MR tells us not to quantify

                  -- See Note [decideAndPromoteTyVars] (DP2)

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

              -- Step 4 of Note [decideAndPromoteTyVars]

              -- Use closeWrtFunDeps to find any other variables that are determined by mono_tvs

                  -- Why delVarSetList psig_qtvs?

                  -- If the user has explicitly asked for quantification, then that

                  -- request "wins" over the MR.

                  -- (i.e. says "no" to isQuantifiableTv)? That's OK: explanation

                  -- in Step 2 of Note [Deciding quantification].

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

              -- Step 5 of Note [decideAndPromoteTyVars]

            , text "newly_mono_tvs =" <+> ppr newly_mono_tvs

            , text "can_quant =" <+> ppr can_quant

            , text "post_mr_quant =" <+> ppr post_mr_quant

            , text "mr_no_quant =" <+> ppr mr_no_quant

            , text "final_quant =" <+> ppr final_quant

            , text "co_vars =" <+> ppr co_vars ]

   The body of z tries to unify the type of x (call it alpha[1]) with

   (beta[2] -> gamma[2]). This unification fails because alpha is untouchable, leaving

        [W] alpha[1] ~ (beta[2] -> gamma[2])

   Another example. Suppose we have

       class C a b | a -> b

   promote type variables.  But for bindings affected by the MR we have no choice

   but to promote.

 Note [The top-level Any principle]

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

 Most /top level/ bindings have a type signature, so none of this arises.  But

 where a top-level binding lacks a signature, we don't want to infer a type like

 bad bad.  Better to report an error, which is what may well happen if we

 quantify over alpha instead.

 For /nested/ bindings, a monomorphic type like `f :: alpha[0] -> Int` is fine,

 because we can see all the call sites of `f`, and they will probably fix

 `alpha`.  In contrast, we can't see all of (or perhaps any of) the calls of

 top-level (exported) functions, reducing the worries about "spooky action at a

 Note [Do not quantify over constraints that determine a variable]

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

          where

            dicts = bagToList (dictsToBag solved_dicts)

   = IC { inert_eqs          = emptyTyEqs

        , inert_funeqs       = emptyFunEqs

        , inert_given_eqs    = False

        , inert_dicts        = emptyDictMap

        , inert_safehask     = emptyDictMap

        , inert_insts        = []

        , inert_irreds       = emptyBag }

        , inert_cycle_breakers = emptyBag :| []

        , inert_famapp_cache   = emptyFunEqs

        , inert_solved_dicts   = emptyDictMap }

    imply nominal ones. For example, if (G a ~R G b) and G's argument's

    role is nominal, then we can deduce a ~N b.

 Historical note: prior to #24938 we also ignored Given equalities that

 did not mention an "outer" type variable.  But that is wrong, as #24938

 showed. Another example is immortalised in test LocalGivenEqs2

     runTcSSpecPrag,

     failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,

     runTcSEqualities,

     emitImplicationTcS, emitTvImplicationTcS,

     emitImplication,

     emitFunDepWanteds,

 -- | See Note [TcSMode]

 data TcSMode

   = TcSVanilla    -- ^ Normal constraint solving

   | TcSEarlyAbort -- ^ Abort early on insoluble constraints

   deriving (Eq)

 {- Note [TcSMode]

 * TcSVanilla: Normal constraint solving mode. This is the default.

 * TcSEarlyAbort: Abort (fail in the monad) as soon as we come across an

   insoluble constraint. This is used to fail-fast when checking for hole-fits.

   See Note [Speeding up valid hole-fits].

 runTcSEarlyAbort :: TcS a -> TcM a

 runTcSEarlyAbort tcs

   = do { ev_binds_var <- TcM.newTcEvBinds

 -- | Run the 'TcS' monad in 'TcSSpecPrag' mode, which either fully solves

 -- individual Wanted quantified constraints or leaves them alone.

 -- See Note [TcSSpecPrag].

 runTcSSpecPrag :: EvBindsVar -> TcS a -> TcM a

 runTcSSpecPrag ev_binds_var tcs

 {- Note [TcSSpecPrag]

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

 runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)

 runTcSInerts inerts tcs = do

   ev_binds_var <- TcM.newTcEvBinds

     setInertSet inerts

     a <- tcs

     new_inerts <- getInertSet

 runTcSWithEvBinds :: EvBindsVar

                   -> TcS a

                   -> TcM a

                    -> EvBindsVar

                    -> TcS a

                    -> TcM a

   = do { unified_var <- TcM.newTcRef 0

        ; unif_lvl_var <- TcM.newTcRef Nothing

        ; let env = TcSEnv { tcs_ev_binds           = ev_binds_var

                           , tcs_unified            = unified_var

        ; when (count > 0) $

          csTraceTcM $ return (text "Constraint solver steps =" <+> int count)

 #if defined(DEBUG)

        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var

 setEvBindsTcS ref (TcS thing_inside)

  = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })

 nestImplicTcS :: EvBindsVar

               -> TcLevel -> TcS a

               -> TcS a

 ************************************************************************

 -}

 approximateWC :: Bool -> WantedConstraints -> Bag Ct

 approximateWC include_non_quantifiable cts

 -- The "X" means "extended";

 --    we return both quantifiable and non-quantifiable constraints

 -- See Note [ApproximateWC]

 -- See Note [floatKindEqualities vs approximateWC]

   where

     float_wc :: Bool           -- True <=> there are enclosing equalities

              -> TcTyCoVarSet   -- Enclosing skolem binders

            -- There can be (insoluble) Given constraints in wc_simple,

            -- there so that we get error reports for unreachable code

            -- See `given_insols` in GHC.Tc.Solver.Solve.solveImplication

            -- See the classification in Note [ApproximateWC]

            EqPred eq_rel ty1 ty2

            ClassPred cls tys

              | Just {} <- isCallStackPred cls tys

                -- the constraints bubble up to be solved from the outer

                -- context, or be defaulted when we reach the top-level.

                -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence

              | otherwise

     -- See Note [Quantifying over equality constraints]

     quantify_equality NomEq  ty1 ty2 = quant_fun ty1 || quant_fun ty2

 Wrinkle (W1)

   When inferring most-general types (in simplifyInfer), we

   equality constraints, because that defeats the OutsideIn story.

   Consider data T a where { TInt :: T Int; MkT :: T a }

          f TInt = 3::Int

       ‘t’ is a rigid type variable bound by

         the type signature for:

           z :: forall t. Id t

       ‘p’ is a rigid type variable bound by

         the inferred type of cast1 :: p -> a

         at T7453.hs:(7,1)-(10,30)

     • Relevant bindings include

         z :: Id t (bound at T7453.hs:9:11)

         v :: p (bound at T7453.hs:7:7)

         cast1 :: p -> a (bound at T7453.hs:7:1)

       ‘t1’ is a rigid type variable bound by

         the type signature for:

           z :: forall t1. () -> t1

       ‘p’ is a rigid type variable bound by

         the inferred type of cast2 :: p -> t

         at T7453.hs:(13,1)-(16,33)

     • Relevant bindings include

         z :: () -> t1 (bound at T7453.hs:15:11)

         v :: p (bound at T7453.hs:13:7)

         cast2 :: p -> t (bound at T7453.hs:13:1)

         z :: t1 (bound at T7453.hs:21:11)

         v :: p (bound at T7453.hs:19:7)

         cast3 :: p -> t (bound at T7453.hs:19:1)

 test('T25325', normal, compile_fail, [''])

 test('T25004', normal, compile_fail, [''])

 test('T25004k', normal, compile_fail, [''])