module GHC.Core.FVs (

         -- * Free variables of expressions and binding groups

         exprFreeVars,     exprsFreeVars,

         exprFreeVarsList, exprsFreeVarsList,

         exprFreeIds,      exprsFreeIds,

         exprFreeIdsDSet,  exprsFreeIdsDSet,

         exprFreeIdsList,  exprsFreeIdsList,

         bindFreeVars,

         InterestingVarFun,

         exprSomeFreeVars, exprsSomeFreeVars,

         exprSomeFreeVarsList, exprsSomeFreeVarsList, exprsSomeFreeVarsDSet,

         -- * Free variables of Rules, Vars and Ids

         bndrTypeTyCoFVs, bndrFVs, dBndrFreeVars,

 import GHC.Builtin.WiredIn.Prim( fUNTyCon )

 import GHC.Data.Maybe( orElse )

 import GHC.Utils.Misc

 import GHC.Utils.Panic.Plain

 {-

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

 *                                                                      *

 *                                                                      *

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

 Note [Free variables of an expression]

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

 -- | Find all locally-defined free Ids or type variables in an expression

 -- returning a non-deterministic set.

 exprFreeVars :: CoreExpr -> VarSet

 exprFreeVars = dVarSetToVarSet . exprFreeVarsDSet

 -- | Find all locally-defined free Ids or type variables in an expression

 -- returning a deterministic set.

 exprFreeVarsDSet :: CoreExpr -> DVarSet

 exprFreeVarsDSet = runFVSelective isLocalVar . exprFVs

 -- returning a non-deterministic set.

 exprsFreeVars :: [CoreExpr] -> VarSet

 exprsFreeVars = dVarSetToVarSet . exprsFreeVarsDSet

 -- returning a deterministically ordered list.

 exprsFreeVarsList :: [CoreExpr] -> [Var]

 exprsFreeVarsList = runFVSelectiveList isLocalVar . exprsFVs

 exprsFreeVarsDSet :: [CoreExpr] -> DVarSet

 exprsFreeVarsDSet = runFVSelective isLocalVar . exprsFVs

 -- | Find all locally-defined free Ids or type variables in an expression

 -- returning a deterministically ordered list.

 exprFreeVarsList :: CoreExpr -> [Var]

 exprFreeVarsList = dVarSetElems . exprFreeVarsDSet

 exprFreeIds = dVarSetToVarSet . exprFreeIdsDSet

 exprsFreeIds = dVarSetToVarSet . exprsFreeIdsDSet

 -- | Find all locally-defined free Ids in an expression

 -- returning a deterministic set.

 exprFreeIdsDSet = runFVSelective isLocalId . exprFVs

 -- | Find all locally-defined free Ids in several expressions

 -- returning a deterministic set.

 exprsFreeIdsDSet = runFVSelective isLocalId . exprsFVs

 -- | Find all locally-defined free Ids in an expression

 -- returning a deterministically ordered list.

 exprFreeIdsList = dVarSetElems . exprFreeIdsDSet

 -- | Find all locally-defined free Ids in several expressions

 -- returning a deterministically ordered list.

 exprsFreeIdsList = dVarSetElems . exprsFreeIdsDSet

 bindFreeVars :: CoreBind -> VarSet

 bindFreeVars = runFVSelectiveSet isLocalVar . bind_fvs

                         mapUnionFV rhs_fvs prs

 -- | Finds free variables in an expression selected by a predicate

 exprSomeFreeVars :: InterestingVarFun   -- ^ Says which 'Var's are interesting

                  -> CoreExpr

                  -> VarSet

 addCoreBndrsFV bndrs fv = foldr addCoreBndrFV fv bndrs

 unitFV :: Var -> SelectiveDFV

 exprsFVs :: [CoreExpr] -> SelectiveDFV

 exprsFVs = mapUnionFV exprFVs

 exprFVs :: CoreExpr -> SelectiveDFV

 exprFVs (Var var)       = unitFV var

 exprFVs (Lit _)         = mempty

 exprFVs (Tick t expr)   = tickish_fvs t `mappend` exprFVs expr

 exprFVs (App fun arg)   = exprFVs fun `mappend` exprFVs arg

 exprFVs (Lam bndr body) = addCoreBndrFV bndr (exprFVs body)

 exprFVs (Case scrut bndr ty alts)

     addCoreBndrFV bndr (mapUnionFV alt_fvs alts)

   where

     alt_fvs (Alt _ bndrs rhs) = addCoreBndrsFV bndrs (exprFVs rhs)

 ---------

 bndrTypeTyCoFVs :: Var -> SelectiveDFV

 -- In the case of ids, don't forget the multiplicity field!

 bndrTypeTyCoFVs var

   where

     mult_fvs = case varMultMaybe var of

                  Nothing   -> mempty

 dBndrTypeTyCoVars :: Var -> DTyCoVarSet

                   dBndrFreeVars id

 dBndrFreeVars :: Id -> DVarSet

 dBndrFreeVars id = runFVSelective isLocalVar $ bndrFVs id

 bndrFVs :: Id -> SelectiveDFV

 bndrFVs id = assert (isId id) $

              bndrTypeTyCoFVs id `mappend`

              bndrRuleAndUnfoldingFVs id

 Invariant: a FVAnn, say S, is closed:

   That is: if v is in S,

            then freevars( v's type/kind ) is also in S

 -}

 type FVAnn = DVarSet  -- See Note [The FVAnn invariant]

   where

     go :: CoreExpr -> CoreExprWithFVs

     go (Var v)

     go (Lit lit) = (emptyDVarSet, AnnLit lit)

     go (Lam b body)

       where

         body'@(body_fvs, _) = go body

     go (App fun arg)

       = ( freeVarsOf fun' `unionDVarSet` freeVarsOf arg'

         , AnnTick tickish expr2 )

       where

         expr2 = go expr

     go (Type ty)     = (tyCoVarsOfTypeDSet ty, AnnType ty)

     go (Coercion co) = (tyCoVarsOfCoDSet co, AnnCoercion co)

   where

     rule_doc = text "Rule" <+> doubleQuotes (ftext name) <> colon

     rhs_fvs = exprFreeVarsDSet rhs

     is_bad_bndr :: Var -> Bool

                                          ppr body $$ ppr (exprType body)

     body_ty = exprType body

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

 freshEtaId :: Int -> Subst -> Scaled Type -> (Subst, Id)

            poly_t = /\ a b -> (e1, e2)

            poly_x = /\ a   -> fst (poly_t a *b*)

        f = /\k (f:k->*) (a:k). let t = AccFailure @ (f a) in ...

       Here we want to float 't', but we must remember to abstract over

       'k' as well, even though it is not explicitly mentioned in the RHS,

       otherwise we get

          t = /\ (f:k->*) (a:k). AccFailure @ (f a)

 (AB3) We get the variables to abstract over by filtering down the

       the main_tvs for the original function, picking only ones

         rhs' = GHC.Core.Subst.substExpr subst rhs

         -- tvs_here: see Note [Which type variables to abstract over]

     abstract subst (CyclicSCC trpls)

       = do { (poly_ids, poly_apps) <- mapAndUnzipM (mk_poly1 tvs_here) ids

                           --    because it has a non-CoVar precondition

            | Just poly_app <- GHC.Core.Subst.lookupIdSubst_maybe subst var

            = -- 'var' is like 'x' in (AB4)

            | otherwise

            = free_tvs

     choose_tvs free_tvs

     mk_poly1 :: [TyVar] -> Id -> SimplM (Id, CoreExpr)

     mk_poly1 tvs_here var

 import GHC.Data.Maybe     ( fromMaybe, orElse, catMaybes, isJust, isNothing )

 import GHC.Data.FastString

 import GHC.Utils.Misc

 import GHC.Utils.Outputable

 Note [Free type variables of the qvar types]

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

 In a call (f @a x True), that we want to specialise, what variables should

 Note [SpecConstr call patterns]

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

 * The list of argument patterns, cp_args, is no longer than the

   visible lambdas of the binding, ri_arg_occs.  This is done via

 * The list of argument patterns can certainly be shorter than the

   lambdas in the function definition (under-saturated).  For example

 callToPat env bndr_occs call@(Call fn args con_env)

   = do  { let in_scope = substInScopeSet (sc_subst env)

                    -- the lambdas in the function definition (bndr_occs)

           -- Drop boring patterns from the end

                 -- See Note [Shadowing in SpecConstr] at the top

               (qktvs, qids) = partition isTyVar qvars

                 -- Order into kind variables, type variables, term variables

                 -- The kind of a type variable may mention a kind variable

                 -- and the type of a term variable may mention a type variable

         -- Check for bad coercion variables: see Note [SpecConstr and casts]

         ; let bad_covars = filter isCoVar qids

         ; warnPprTrace (not (null bad_covars))

                   ; return (Just cp_res) }

           else return Nothing }

 argToPat :: ScEnv

                                         -- See Note [SpecConstr and strict fields]

          -> UniqSM (Bool, CoreArg, [Id])

 --              lvl7         --> (True, lvl7)      if lvl7 is bound

 --                                                 somewhere further out

   = do

     -- pprTraceM "argToPatIn" (ppr arg)

     -- pprTraceM "argToPatOut" (ppr res)

     return res

 argToPat1 :: ScEnv

   -> InScopeSet

   -> ValueEnv

   -> Expr CoreBndr

   -> ArgOcc

   -> StrictnessMark

   -> UniqSM (Bool, Expr CoreBndr, [Id])

   = return (False, arg, [])

         -- Note [Tick annotations in call patterns]

         -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

         -- Ignore Notes.  In particular, we want to ignore any InlineMe notes

         -- ride roughshod over them all for now.

         --- See Note [Tick annotations in RULE matching] in GHC.Core.Rules

         -- See Note [Matching lets] in "GHC.Core.Rules"

         -- Look through let expressions

         -- e.g.         f (let v = rhs in (v,w))

         -- because the rule-matcher will look through the let.

    -- Casts: see Note [SpecConstr and casts]

   | not (ignoreType env ty2)

         ; if not interesting then

           else

                 return (interesting, Cast arg' co, strict_args) }

   where

   -- Check for a constructor application

   -- NB: this *precedes* the Var case, so that we catch nullary constrs

   | Just (ConVal _wf (DataAlt dc) args) <- isValue val_env arg

     -- Ignore `_wf` here; see Note [ConVal work-free-ness] (2)

   , not (ignoreDataCon env dc)        -- See Note [NoSpecConstr]

   , Just arg_occs <- mb_scrut dc

   = do { let (ty_args, rest_args) = splitAtList (dataConUnivTyVars dc) args

              -- con_str corresponds 1-1 with the /value/ arguments

              con_str = dataConRepStrictness dc

       --  ; pprTraceM "bangs" (ppr (length rest_args == length con_str) $$

       --       ppr dc $$

       --       ppr con_str $$

       --       ppr rest_args $$

       --       ppr (map isTypeArg rest_args))

        ; let args' = map sndOf3 prs :: [CoreArg]

        ; assertPpr (length con_str == length (filter isRuntimeArg rest_args))

             ( ppr con_str $$ ppr rest_args $$

                             -> Just (repeat UnkOcc)

                             | otherwise

                             -> Nothing

   -- Check if the argument is a variable that

   --    (a) is used in an interesting way in the function body

   --         business of absence analysis, not SpecConstr.)

   --    (b) we know what its value is

   -- In that case it counts as "interesting"

   | sc_force env || specialisableArgOcc arg_occ  -- (a)

     -- See Note [Forcing specialisation], point (FS3)

   , is_value                                     -- (b)

   -- The default case: make a wild-card

   -- We use this for coercions too

 -- | wildCardPats are always boring

 wildCardPat :: Type -> StrictnessMark -> UniqSM (Bool, CoreArg, [Id])

 defeated specialisation!  Hence the use of collectBindersPushingCo.

 Note [Evidence foralls]

 Suppose (#12212) that we are specialising

    f :: forall a b. (Num a, F a ~# F b) => blah

 with a=b=Int. Then the RULE will be something like

 where that `g` is really (Coercion (CoVar g)), since `g` is a

 coercion variable and can't appear as (Var g).

    RULE forall (d:Num Int) (g :: F Int ~ F Int).

         f Int Int d <F Int> = f_spec

 Note [Orphans and auto-generated rules]

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

   ppr UnspecArg     = text "UnspecArg"

 specArgsFVs :: InterestingVarFun -> [SpecArg] -> VarSet

 specArgsFVs interesting args

   = runFVSelectiveSet interesting $

     mapUnionFV get args

   where

     get :: SpecArg -> SelectiveDFV

     get (SpecDict dx)   = exprFVs dx

     get UnspecType      = mempty

     get UnspecArg       = mempty

              <- specHeader subst1 bndrs args

        ; let dummy_arg = varToCoreExpr bndr'

        ; pure ( useful, subst2

 -- | Binds a dictionary argument to a fresh name, to preserve sharing

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

 substDVarSet :: HasDebugCallStack => Subst -> DVarSet -> DVarSet

 -- Apply the substitution to the vars in the set,

 substDVarSet subst@(Subst _ _ tv_env cv_env) fvs

   = runFVSelective isLocalVar $

     strictFoldDVarSet (mappend . do_one) mempty fvs

   where

   do_one :: Var -> SelectiveDFV

   do_one fv

      | otherwise  = exprFVs (lookupIdSubst subst fv)

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

         coVarsOfCo, coVarsOfCos,

         coVarsOfCoDSet, coVarsOfCosDSet,

         -- Almost devoid

         almostDevoidCoVarOfCo,

         occCheckExpand,

         -- * Closing over kinds

         closeOverKinds,

   ) where

   forall (a:(k:Type)). a   {k}        {k}

   (a:k->Type) (b:k)        {a,b}      {a,b,k}

 Note [Computing deep free variables]

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

   AND add on the free vars of its kind `k`.

   BUT in this latter step, start with an empty BoundVars set.

 Side note: the free-variable binder would still work even without (NoTypeShadowing).

 Consider:

 (deepTypeFV, deepTypesFV, deepCoFV, deepCosFV) = foldTyCo deepTcvFolder

 deepTcvFolder :: TyCoFolder TyCoFV

 -- It's important that we use a one-shot EndoOS, to ensure that all

 -- the free-variable finders are eta-expanded.  Lacking the one-shot-ness

 -- led to some big slow downs.  See Note [The one-shot state monad trick]

 -- in GHC.Utils.Monad

                      -- We don't collect the CoercionHole itself, but we /do/

                      -- need to collect the free variables of its /kind/

                      -- See Note [CoercionHoles and coercion free variables]

 -- See Note [Computing deep free variables]

   = \v -> MkFV (\bvs -> EndoOS (do_it bvs v))

   where

     do_it :: BoundVars -> TyCoVar -> TyCoVarSet -> TyCoVarSet

     do_it bvs v acc | v `elemVarSet` bvs = acc

                     | v `elemVarSet` acc = acc

                                            `extendVarSet` v