Note [Which type variables to abstract over]

GHC/Core/Opt/Simplify/Utils.hs:2122 compiler 3 tickets

Abstract only over the type variables free in the rhs wrt which the
new binding is abstracted.  Several points worth noting

(AB1) The naive approach of abstracting wrt the
      tyvars free in the Id's /type/ fails. Consider:
          /\ a b -> let t :: (a,b) = (e1, e2)
                        x :: a     = fst t
                    in ...
      Here, b isn't free in x's type, but we must nevertheless
      abstract wrt b as well, because t's type mentions b.
      Since t is floated too, we'd end up with the bogus:
           poly_t = /\ a b -> (e1, e2)
           poly_x = /\ a   -> fst (poly_t a *b*)

(AB2) We must do closeOverKinds.  Example (#10934):
       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)
      which is obviously bogus.

(AB3) We get the variables to abstract over by filtering down the
      the main_tvs for the original function, picking only ones
      mentioned in the abstracted body. This means:
      - they are automatically in dependency order, because main_tvs is
      - there is no issue about non-determinism
      - we don't gratuitously change order, which may help (in a tiny
        way) with CSE and/or the compiler-debugging experience

(AB4) For a recursive group, it's a bit of a pain to work out the minimal
      set of tyvars over which to abstract:
           /\ a b c.  let x = ...a... in
                      letrec { p = ...x...q...
                               q = .....p...b... } in
                      ...
      Since 'x' is abstracted over 'a', the {p,q} group must be abstracted
      over 'a' (because x is replaced by (poly_x a)) as well as 'b'.
      Remember this bizarre case too:
           x::a = x
      Here, we must abstract 'x' over 'a'.

      Why is it worth doing this?  Partly tidiness; and partly #22459
      which showed that it's harder to do polymorphic specialisation well
      if there are dictionaries abstracted over unnecessary type variables.
      See Note [Weird special case for SpecDict] in GHC.Core.Opt.Specialise

(AB5) We do dependency analysis on recursive groups prior to determining
      which variables to abstract over.
      This is useful, because ANFisation in prepareBinding may float out
      values out of a complex recursive binding, e.g.,
          letrec { xs = g @a "blah"# ((:) 1 []) xs } in ...
        ==> { prepareBinding }
          letrec { foo = "blah"#
                   bar = [42]
                   xs = g @a foo bar xs } in
          ...
      and we don't want to abstract foo and bar over @a.

      (Why is it OK to float the unlifted `foo` there?
      See Note [Core top-level string literals] in GHC.Core;
      it is controlled by GHC.Core.Opt.Simplify.Env.unitLetFloat.)

      It is also necessary to do dependency analysis, because
      otherwise (in #24551) we might get `foo = \@_ -> "missing"#` at the
      top-level, and that triggers a CoreLint error because `foo` is *not*
      manifestly a literal string.

References 2

Referenced by 5