data StaticFlag

   = IsStatic | NotStatic

   -- IsStatic <=> this binding consists only code; all free

   --              vars are top level (or themselves static).

   --              So it can be moved to top level

  | null redundant_evs

  = return ()

  -- When dealing with a user-written type signature,

  -- we want to add "In the type signature for f".

  = report_redundant_msg True (setCtLocEnvLoc env (redundantConstraintsSpan user_ctxt))

     find [] _ _ = []

     find (implic:implics) seen_eqs tv

        | tv `elem` ic_skols implic

        , seen_eqs

        = map fst prs

        | otherwise

   , isTyVarClassPred pred   -- Don't suggest adding (Eq T) to the context, say

   , (skol:skols) <- usefulContext implics pred

   , let what | null skols

              = text "\"required\""

              | otherwise

              = empty

     go :: [Implication] -> [SkolemInfoAnon]

     go [] = []

     go (ic : ics)

          -- Stop at a static form, because all outer Givens are irrelevant

          -- See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable

        | implausible ic               = rest

       | implausible_info (ic_info ic) = True

       | otherwise                     = False

     implausible_info _                             = False

     -- Do not suggest adding constraints to an *inferred* type signature

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

 tidySkolemInfoAnon :: TidyEnv -> SkolemInfoAnon -> SkolemInfoAnon

 tidySkolemInfoAnon env (DerivSkol ty)         = DerivSkol (tidyType env ty)

 tidySkolemInfoAnon env (UnifyForAllSkol ty)   = UnifyForAllSkol (tidyType env ty)

 tidySkolemInfoAnon _   info                   = info

             -> TcType -> [(Name,TcTyVar)] -> SkolemInfoAnon

 -- We need to take special care when tidying SigSkol

 -- See Note [SigSkol SkolemInfo] in "GHC.Tc.Types.Origin"

   where

     tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs

     inst_env = mkNameEnv tv_prs'

   | otherwise

   = givens

   where

 -- | An error reported after constraint solving.

        ; let final_closed = adjustClosedForUnlifted closed ids

        ; thing <- tcExtendLetEnv top_lvl sig_fn final_closed ids thing_inside

        ; return ( (NonRecursive, bind', sendToTopLevel final_closed), thing ) }

 tc_nonrec_group _ _ _ binds _   -- Non-rec groups should always be a singleton

 -- Knows nothing about the scope of the bindings

 -- None of the bindings are pattern synonyms

   = setSrcSpan loc                              $

     recoverM (recoveryCode binder_names sig_fn) $ do

         -- Set up main recover; take advantage of any type sigs

     { traceTc "------------------------------------------------" Outputable.empty

     ; traceTc "Bindings for {" (ppr binder_names)

     ; dflags   <- getDynFlags

     ; traceTc "Generalisation plan" (ppr plan)

     ; result@(_, scaled_poly_ids) <- case plan of

     ; let poly_ids = map scaledThing scaled_poly_ids

 *                                                                      *

 ********************************************************************* -}

             -> LHsBind GhcRn   -- Must be a FunBind

             -> TcM (LHsBinds GhcTc, [Scaled TcId])

 -- There is just one binding,

 --   it is a FunBind

 --   it has a complete type signature,

             sig@(CSig { sig_bndr = poly_id, sig_ctxt = ctxt })

             (L bind_loc (FunBind { fun_id = L nm_loc name

                                  , fun_matches = matches }))

        ; mult <- newMultiplicityVar

        ; (wrap_gen, (wrap_res, matches'))

                 let mono_id = mkLocalId mono_name (idMult poly_id) rho_ty in

                 tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $

        ; return ([abs_bind], [Scaled mult poly_id]) }

   = pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)

 funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]

 -}

 tcPolyInfer

   -> RecFlag       -- Whether it's recursive after breaking

                    -- dependencies based on type signatures

   -> TcPragEnv -> TcSigFun

   -> [LHsBind GhcRn]

   -> TcM (LHsBinds GhcTc, [Scaled TcId])

   = do { (tclvl, wanted, (binds', mono_infos))

              <- pushLevelAndCaptureConstraints  $

                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list

        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)

        ; ((qtvs, givens, ev_binds, insoluble), residual)

        ; let inferred_theta = map evVarPred givens

        ; scaled_exports <- checkNoErrs $

   ppr (CheckGen _ s) = text "CheckGen" <+> ppr s

 decideGeneralisationPlan

    -> [LHsBind GhcRn] -> GeneralisationPlan

   | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig

   | generalise_binds                         = InferGen

   | otherwise                                = NoGen

   where

     generalise_binds

       | has_mult_anns_and_pats = False

         -- See (NVP1) and (NVP4) in Note [Non-variable pattern bindings aren't linear]

         -- free vars have ClosedTypeId=True; so we can ignore

         -- -XMonoLocalBinds, and generalise anyway.

       | has_partial_sigs = True

         -- See Note [Partial type signatures and generalisation]

 isClosedBndrGroup :: TcTypeEnv -> [LHsBind GhcRn] -> IsGroupClosed

 isClosedBndrGroup type_env binds

   where

     fv_env :: NameEnv NameSet

     fv_env = mkNameEnv $ [ (b,fvs) | (bs,fvs) <- bind_fvs, b <-bs ]

     id_is_static name

       | Just thing <- lookupNameEnv type_env name

       = case thing of

       | otherwise  -- Imported Ids

       = True

                -- Ditto class method etc from the current module

 adjustClosedForUnlifted :: IsGroupClosed -> [Scaled TcId] -> IsGroupClosed

   where

 sendToTopLevel :: IsGroupClosed -> StaticFlag

 lHsBindFreeVars :: LHsBind GhcRn -> NameSet

 lHsBindFreeVars (L _ (FunBind { fun_ext = fvs })) = fvs

 lHsBindFreeVars _                                 = emptyNameSet

 It is very confusing to apply NoGen to a top level binding. Consider (#20123):

    module M where

      x = 5

      f y = (x, y)

 NoGen is good when we have call sites, but not at top level, where the

 function may be exported.  And it's easier to grok "MonoLocalBinds" as

       = do { (wrap, expr') <- tcSkolemiseExpectedType ty thing_inside

            ; return (mkHsWrap wrap expr') }

     outer_skolemise (Right sig) thing_inside

            ; return (mkHsWrap wrap expr') }

     -- inner_skolemise is used when we do not have a lambda

                         = NoRestrictions

        ; ((qtvs, givens, ev_binds, _), residual)

            <- captureConstraints $

        ; emitConstraints residual

        ; tau <- liftZonkM $ zonkTcType tau

   VarPat x (L l name) -> do

         { (wrap, id) <- tcPatBndr penv name pat_ty

                               tcExtendIdEnv1 name id thing_inside

         ; pat_ty <- readExpType (scaledThing pat_ty)

         ; return (mkHsWrapPat wrap (VarPat x (L l id)) pat_ty, res) }

     checkConstraints skol_info [] []  $  -- Builds an implication if necessary

     thing_inside                         -- e.g. with -fdefer-type-errors

   where

 {- Note [Dealing with main]

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

     let { fresh_it = itName uniq (getLocA rdr_expr) } ;

     ((qtvs, dicts, _, _), residual)

          <- captureConstraints $

                           []    {- No sig vars -}

                           [(fresh_it, res_ty)]

                           lie ;

 import GHC.Tc.Types.Origin

 import GHC.Tc.Utils.TcType

 import GHC.Core.Predicate

 import GHC.Core.Type

 import GHC.Core.Ppr

   ppr EagerDefaulting = text "EagerDefaulting"

   ppr NoRestrictions  = text "NoRestrictions"

               -> TcLevel               -- Used when generating the constraints

               -> InferMode

               -> [TcIdSigInst]         -- Any signatures (possibly partial)

                       TcEvBinds,    -- ... binding these evidence variables

                       Bool)         -- True <=> the residual constraints are insoluble

   | isEmptyWC wanteds

    = do { -- When quantifying, we want to preserve any order of variables as they

           -- appear in partial signatures. cf. decideQuantifiedTyVars

        ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)

        ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars dep_vars

        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)

        ; return (qtkvs, [], emptyTcEvBinds, False) }

              ; bound_theta_vars <- mapM TcM.newEvVar bound_theta

              ; let full_theta = map idType bound_theta_vars

                                           | (name, ty) <- name_taus ]

                  -- mkPhiTy: we don't add the quantified variables here, because

                  -- they are also bound in ic_skols and we want them to be tidied

       -- start with a completely empty inert set; in particular, no Givens

       -- See (SF3) in Note [Grand plan for static forms]

       -- in GHC.Iface.Tidy.StaticPtrTable

       = emptyInertSet inner_tclvl

       | otherwise

       = any isImprovementPred (pred : transSuperClasses pred)

 warnRedundantGivens :: SkolemInfoAnon -> Bool

   = case ctxt of

        FunSigCtxt _ rrc -> reportRedundantConstraints rrc

        ExprSigCtxt rrc  -> reportRedundantConstraints rrc

        ; (ev_binds, (tc_bind, _))

                <- checkConstraints skol_info tyvars [this_dict] $

                               (L bind_loc lm_bind)

        ; let export = ABE { abe_poly  = global_dm_id

                                    , sig_ctxt = ctxt

                                    , sig_loc  = getLocA hs_sig_ty }

        ; let export = ABE { abe_poly  = local_meth_id

                           , abe_mono  = inner_id

               --      instance C [c] where { op = <rhs> }

               -- In <rhs>, 'c' is scope but 'b' is not!

        ; return tc_bind }

   where

        ; ((univ_tvs, req_dicts, ev_binds, _), residual)

                <- captureConstraints $

        ; top_ev_binds <- checkNoErrs (simplifyTop residual)

        ; addTopEvBinds top_ev_binds $

        ; checkTc (all (isManyTy . scaledMult) arg_tys) $

            TcRnLinearPatSyn sig_body_ty

                          -- The type here is a bit bogus, but we do not print

                          -- the type for PatSynCtxt, so it doesn't matter

                          -- See Note [Skolem info for pattern synonyms] in "GHC.Tc.Types.Origin"

        ; traceTc "tcPatSynBuilderBind {" $

          vcat [ ppr patsyn

               , ppr builder_id <+> dcolon <+> ppr (idType builder_id) ]

        ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds

        ; return builder_binds } } }

     = NotLetBound

     | LetBound

              -- IsStatic <=> this binding may safely be moved to top level

              -- E.g   f x = let ys = reverse [1,2]

              --                 zs = reverse ys

              -- all free vars of `e` have lb_clos=ClosedTypeId

         }

 data IsGroupClosed

   = IsGroupClosed

 type RhsNames = NameSet   -- Names of variables, mentioned on the RHS of

                           -- a definition, that are not Global or ClosedLet

 instance Outputable IdBindingInfo where

   ppr NotLetBound = text "NotLetBound"

     = text "LetBound" <> braces (sep [ ppr top_lvl, text "closed-type=" <+> ppr cls

                                      , ppr fvs ])

     get acc [] = acc

     get acc (implic : implics)

       = acc  -- For static forms, ignore all outer givens

              -- See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable

 -- So it doesn't matter much if its's incomplete

 checkSkolInfoAnon sk1 sk2 = go sk1 sk2

   where

     go (SigTypeSkol cx1)    (SigTypeSkol cx2)    = cx1==cx2

     go (ForAllSkol _)       (ForAllSkol _)       = True

     go (SpecESkol n1)       (SpecESkol n2)       = n1==n2

     go (PatSkol c1 _)       (PatSkol c2 _)       = getName c1 == getName c2

        -- Too tedious to compare the HsMatchContexts

     go (UnifyForAllSkol t1) (UnifyForAllSkol t2) = t1 `tcEqType` t2

     go ReifySkol            ReifySkol            = True

     go RuntimeUnkSkol       RuntimeUnkSkol       = True

   ReportRedundantConstraints(..), reportRedundantConstraints,

   redundantConstraintsSpan,

   SkolemInfo(..), SkolemInfoAnon(..), mkSkolemInfo, getSkolemInfo, pprSigSkolInfo, pprSkolInfo,

   -- * CtOrigin

   CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,

             -- a programmer-supplied type signature

             -- Location of the binding site is on the TyVar

             -- See Note [SigSkol SkolemInfo]

        UserTypeCtxt        -- What sort of signature

        TcType              -- Original type signature (before skolemisation)

        [(Name,TcTyVar)]    -- Maps the original name of the skolemised tyvar

                            -- to its instantiated version

   | SigTypeSkol UserTypeCtxt

                  -- like SigSkol, but when we're kind-checking the *type*

                  -- hence, we have less info

   | RuleSkol RuleName   -- The LHS of a RULE

   | SpecESkol Name      -- A SPECIALISE pragma

   | BracketSkol         -- Template Haskell bracket

   | UnifyForAllSkol     -- We are unifying two for-all types

 pprSkolInfo :: SkolemInfoAnon -> SDoc

 -- Complete the sentence "is a rigid type variable bound by..."

 pprSkolInfo (SigTypeSkol cx)  = pprUserTypeCtxt cx

 pprSkolInfo (ForAllSkol tvs)  = text "an explicit forall" <+> ppr tvs

 pprSkolInfo (IPSkol ips)      = text "the implicit-parameter binding" <> plural ips <+> text "for"

 pprSkolInfo (SpecESkol name)  = text "a SPECIALISE pragma for" <+> quotes (ppr name)

 pprSkolInfo (PatSkol cl mc)   = sep [ pprPatSkolInfo cl

                                     , text "in" <+> pprMatchContext mc ]

                                    2 (vcat [ ppr name <+> dcolon <+> ppr ty

                                            | (name,ty) <- ids ])

 pprSkolInfo (UnifyForAllSkol ty)  = text "the type" <+> ppr ty

   the instantiated skolems lying  around in other types.

 -}

 {- *********************************************************************

 *                                                                      *

             CtOrigin

 import GHC.Tc.Errors.Types

 import GHC.Tc.Utils.Monad

 import GHC.Tc.Utils.TcType

 import GHC.Tc.Types.LclEnv

 import GHC.Core.InstEnv

 tcExtendRecIds pairs thing_inside

   = tc_extend_local_env NotTopLevel

           [ (name, ATcId { tct_id   = let_id

                                                , lb_fvs = emptyNameSet

                                                , lb_closed = False } })

           | (name, let_id) <- pairs ] $

                               , tct_info = info })

           | id <- sig_ids

           , let closed = isTypeClosedLetBndr id

                                   , lb_fvs = emptyNameSet

                                   , lb_closed = closed } ]

      thing_inside

 -- Used for both top-level value bindings and nested let/where-bindings

 -- Used for a single NonRec or a single Rec

 -- Adds to the TcBinderStack too

                ids thing_inside

   = tcExtendBinderStack [TcIdBndr id top_lvl | Scaled _ id <- ids] $

     tc_extend_local_env top_lvl

           [ (idName id, ATcId { tct_id   = id

                               , tct_info = mk_tct_info id })

           | Scaled _ id <- ids ] $

   where

     mk_tct_info id

                  , lb_fvs = lookupNameEnv fv_env (idName id) `orElse` emptyNameSet

                  , lb_closed = isTypeClosedLetBndr id }

 tcExtendIdEnv :: [TcId] -> TcM a -> TcM a

 -- For lambda-bound and case-bound Ids

 -- Extends the TcBinderStack as well

 -- | @tcCheckUsage name mult thing_inside@ runs @thing_inside@, checks that the

 -- usage of @name@ is a submultiplicity of @mult@, and removes @name@ from the

 -- usage environment.

   = do { (local_usage, result) <- tcCollectingUsage thing_inside

        ; check_usage (lookupUE local_usage name)

        ; tcEmitBindingUsage (deleteUE local_usage name)

        ; return result }

     where

     check_usage :: Usage -> TcM ()

     -- Checks that the usage of the newly introduced binder is compatible with

     -- its multiplicity.

 tcSkolemiseGeneral

   :: DeepSubsumptionFlag

   -> UserTypeCtxt

   -> TcType -> TcType   -- top_ty and expected_ty

         -- Here, top_ty      is the type we started to skolemise; used only in SigSkol

         -- keeping the same top_ty, but successively smaller expected_tys

   -> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)

   -> TcM (HsWrapper, result)

   | isRhoTyDS ds_flag expected_ty

     -- Fast path for a very very common case: no skolemisation to do

     -- But still call checkConstraints in case we need an implication regardless

        ; (ev_binds, result) <- checkConstraints sig_skol [] [] $

                                thing_inside [] expected_ty

        ; return (mkWpLet ev_binds, result) }

        ; rec { (wrap, tv_prs, given, rho_ty) <- case ds_flag of

                     Deep    -> deeplySkolemise skol_info expected_ty

                     Shallow -> topSkolemise skol_info expected_ty

              ; skol_info <- mkSkolemInfo sig_skol }

        ; let skol_tvs = map (binderVar . snd) tv_prs

          -- often empty, in which case mkWpLet is a no-op

 tcSkolemiseCompleteSig :: TcCompleteSig

                        -> ([ExpPatType] -> TcRhoType -> TcM result)

                        -> TcM (HsWrapper, result)