-- Step 1 of Note [decideAndPromoteTyVars]

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

              can_quant = ctsPreds can_quant_cts

              can_quant_tvs = tyCoVarsOfTypes can_quant

              -- 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

              -- Step 3 of Note [decideAndPromoteTyVars], (a-c)

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

              mono_tvs_without_mr

                | otherwise    = outer_tvs                    -- (a)

                                 `unionVarSet` no_quant_tvs   -- (b)

                                 `unionVarSet` co_var_tvs     -- (c)

                = -- 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]

            , 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 ]

   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]

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

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

 -}

 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

       ‘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, [''])