Note [Casts and lambdas]

GHC/Core/Opt/Simplify/Utils.hs:1866 compiler

Consider
        (\(x:tx). (\(y:ty). e) `cast` co)

We float the cast out, thus
        (\(x:tx) (y:ty). e) `cast` (tx -> co)

We do this for at least three reasons:

1. There is a danger here that the two lambdas look separated, and the
   full laziness pass might float an expression to between the two.

2. The occurrence analyser will mark x as InsideLam if the Lam nodes
   are separated (see the Lam case of occAnal).  By floating the cast
   out we put the two Lams together, so x can get a vanilla Once
   annotation.  If this lambda is the RHS of a let, which we inline,
   we can do preInlineUnconditionally on that x=arg binding.  With the
   InsideLam OccInfo, we can't do that, which results in an extra
   iteration of the Simplifier.

3. It may cancel with another cast.  E.g
      (\x. e |> co1) |> co2
   If we float out co1 it might cancel with co2.  Similarly
      let f = (\x. e |> co1) in ...
   If we float out co1, and then do cast worker/wrapper, we get
      let f1 = \x.e; f = f1 |> co1 in ...
   and now we can inline f, hoping that co1 may cancel at a call site.

TL;DR: put the lambdas together if at all possible.

In general, here's the transformation:
        \x. e `cast` co   ===>   (\x. e) `cast` (tx -> co)
        /\a. e `cast` co  ===>   (/\a. e) `cast` (/\a. co)
        /\g. e `cast` co  ===>   (/\g. e) `cast` (/\g. co)
                          (if not (g `in` co))

We call this "cast swizzling". It is controlled by sm_cast_swizzle.
See also Note [Cast swizzling on rule LHSs]

Wrinkles

* Notice that it works regardless of 'e'.  Originally it worked only
  if 'e' was itself a lambda, but in some cases that resulted in
  fruitless iteration in the simplifier.  A good example was when
  compiling Text.ParserCombinators.ReadPrec, where we had a definition
  like    (\x. Get `cast` g)
  where Get is a constructor with nonzero arity.  Then mkLam eta-expanded
  the Get, and the next iteration eta-reduced it, and then eta-expanded
  it again.

* Note also the side condition for the case of coercion binders, namely
  not (any bad bndrs).  It does not make sense to transform
          /\g. e `cast` g  ==>  (/\g.e) `cast` (/\g.g)
  because the latter is not well-kinded.


************************************************************************
*                                                                      *
              Eta expansion
*                                                                      *
************************************************************************

References 1

Referenced by 2