Eta reduction based on evaluation context (#21261)

I completely rewrote our Notes surrounding eta-reduction. The new entry point is
`Note [Eta reduction makes sense]`.

Then I went on to extend the Simplifier to maintain an evaluation context in the
form of a `SubDemand` inside a `SimplCont`. That `SubDemand` is useful for doing
eta reduction according to `Note [Eta reduction based on evaluation context]`,
which describes how Demand analysis, Simplifier and `tryEtaReduce` interact to
facilitate eta reduction in more scenarios.

Thus we fix #21261.

ghc/alloc perf marginally improves (-0.0%). A medium-sized win is when compiling
T3064 (-3%). It seems that haddock improves by 0.6% to 1.0%, too.

Metric Decrease:
    T3064

5 files changed, 181 insertions, 0 deletions

diff --git a/testsuite/tests/simplCore/should_compile/T20040.hs b/testsuite/tests/simplCore/should_compile/T20040.hs
new file mode 100644
index 0000000000..a50323175f
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T20040.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE BangPatterns        #-}
+
+module T20040 where
+
+import Data.Coerce
+
+data Nat = Z | S Nat
+
+data Vec n a where
+  Nil  :: Vec 'Z a
+  Cons :: a -> Vec n a -> Vec ('S n) a
+
+newtype Succ b n = Succ { unSucc :: b (S n) }
+
+ifoldl' :: forall b n a. (forall m. b m -> a -> b ('S m)) -> b 'Z -> Vec n a -> b n
+ifoldl' f  z Nil = z
+ifoldl' f !z (Cons x xs) = unSucc $ ifoldl' (\(Succ m) a -> Succ (f m a)) (Succ $ f z x) xs
diff --git a/testsuite/tests/simplCore/should_compile/T20040.stderr b/testsuite/tests/simplCore/should_compile/T20040.stderr
new file mode 100644
index 0000000000..3d4e827cbd
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T20040.stderr
@@ -0,0 +1,32 @@
+
+==================== Final STG: ====================
+$WNil = CCS_DONT_CARE Nil! [];
+
+$WCons = \r [conrep conrep] Cons [conrep conrep];
+
+unSucc1 = \r [ds] ds;
+
+unSucc = \r [eta] unSucc1 eta;
+
+Rec {
+ifoldl' =
+    \r [f z ds]
+        case ds of {
+          Nil -> z;
+          Cons ipv2 ipv3 ->
+              case z of z1 {
+              __DEFAULT ->
+              case f z1 ipv2 of sat { __DEFAULT -> ifoldl' f sat ipv3; };
+              };
+        };
+end Rec }
+
+Nil = \r [void] Nil [];
+
+Cons = \r [void eta eta] Cons [eta eta];
+
+Z = CCS_DONT_CARE Z! [];
+
+S = \r [eta] S [eta];
+
+
diff --git a/testsuite/tests/simplCore/should_compile/T21261.hs b/testsuite/tests/simplCore/should_compile/T21261.hs
new file mode 100644
index 0000000000..ae39c4b7d4
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T21261.hs
@@ -0,0 +1,47 @@
+module T21261 where
+
+-- README: The convention here is that bindings starting with 'yes' should be
+-- eta-reduced and become trivial, while bindings starting with 'no' should not
+-- be eta-reduced.
+
+f1 :: (Int -> Int -> Int) -> Int
+f1 c = c 1 2 + c 3 4
+{-# NOINLINE f1 #-}
+yes1 :: (Int -> Int -> Int) -> Int
+yes1 c = f1 (\x -> c x)
+
+f2 :: (Int -> Int -> Int) -> Int
+f2 c = c 1 `seq` c 3 4
+{-# NOINLINE f2 #-}
+yes1or2 :: (Int -> Int -> Int) -> Int
+yes1or2 c = f2 c
+
+f3 :: (Int -> Int -> Int) -> Int
+f3 c = c 1 2 + c 3 4
+{-# NOINLINE f3 #-}
+yes2 :: (Int -> Int -> Int) -> Int
+yes2 c = f3 (\x y -> c x y)
+
+f4 :: (Int -> Int -> Int -> Int) -> Int
+f4 c = c 1 2 `seq` c 3 4 `seq` 42
+{-# NOINLINE f4 #-}
+no3 :: (Int -> Int -> Int -> Int) -> Int
+no3 c = f4 (\x y z -> c x y z)
+
+f5 :: (Int -> Int -> Int) -> Maybe Int
+f5 c = Just (c 1 2 + c 3 4)
+{-# NOINLINE f5 #-}
+yes2_lazy :: (Int -> Int -> Int) -> Maybe Int
+yes2_lazy c = f5 (\x y -> c x y)
+
+f6 :: (Int -> Int -> Int) -> Maybe Int
+f6 c = Just (c 1 `seq` c 3 4)
+{-# NOINLINE f6 #-}
+no2_lazy :: (Int -> Int -> Int) -> Maybe Int
+no2_lazy c = f6 (\x y -> c x y)
+
+f7 :: (Int -> Int -> Int) -> Int
+f7 c = c 1 `seq` c 2 3
+{-# NOINLINE f7 #-}
+not_quite_eta :: (Int -> Int -> Int) -> Int
+not_quite_eta c = f7 (\x y -> c x y)
diff --git a/testsuite/tests/simplCore/should_compile/T21261.stderr b/testsuite/tests/simplCore/should_compile/T21261.stderr
new file mode 100644
index 0000000000..779f769e43
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T21261.stderr
@@ -0,0 +1,73 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 192, types: 201, coercions: 0, joins: 0/0}
+
+lvl = I# 3#
+
+lvl1 = I# 4#
+
+lvl2 = I# 1#
+
+f2 = \ c -> case c lvl2 of { __DEFAULT -> c lvl lvl1 }
+
+yes1or2 = f2
+
+lvl3 = I# 2#
+
+$wf4
+  = \ c ->
+      case c lvl2 lvl3 of { __DEFAULT ->
+      case c lvl lvl1 of { __DEFAULT -> 42# }
+      }
+
+f4 = \ c -> case $wf4 c of ww { __DEFAULT -> I# ww }
+
+no3
+  = \ c ->
+      case $wf4 (\ x y z -> c x y z) of ww { __DEFAULT -> I# ww }
+
+$wf6 = \ c -> (# case c lvl2 of { __DEFAULT -> c lvl lvl1 } #)
+
+f6 = \ c -> case $wf6 c of { (# ww #) -> Just ww }
+
+no2_lazy
+  = \ c -> case $wf6 (\ x y -> c x y) of { (# ww #) -> Just ww }
+
+f7 = \ c -> case c lvl2 of { __DEFAULT -> c lvl3 lvl }
+
+not_quite_eta = \ c -> f7 (\ x y -> c x y)
+
+$wf5
+  = \ c ->
+      (# case c lvl2 lvl3 of { I# x ->
+         case c lvl lvl1 of { I# y -> I# (+# x y) }
+         } #)
+
+f5 = \ c -> case $wf5 c of { (# ww #) -> Just ww }
+
+yes2_lazy
+  = \ c -> case $wf5 (\ x y -> c x y) of { (# ww #) -> Just ww }
+
+$wf3
+  = \ c ->
+      case c lvl2 lvl3 of { I# x ->
+      case c lvl lvl1 of { I# y -> +# x y }
+      }
+
+f3 = \ c -> case $wf3 c of ww { __DEFAULT -> I# ww }
+
+yes2 = f3
+
+$wf1
+  = \ c ->
+      case c lvl2 lvl3 of { I# x ->
+      case c lvl lvl1 of { I# y -> +# x y }
+      }
+
+f1 = \ c -> case $wf1 c of ww { __DEFAULT -> I# ww }
+
+yes1 = f1
+
+
+
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 5a23e84c75..8cdf5a5417 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -392,3 +392,10 @@ test('OpaqueNoWW', normal, compile, ['-O -ddump-simpl -dsuppress-uniques'])
 
 test('T21144',  normal, compile, ['-O'])
 
+# Key here is that the argument to ifoldl' is eta-reduced in Core to
+#   `/\m. f @(S m)`
+# which will erase completely in STG
+test('T20040', [ grep_errmsg(r'ifoldl\''), expect_broken(20040) ], compile, ['-O -ddump-stg-final -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])
+
+# Key here is that yes* become visibly trivial due to eta-reduction, while no* are not eta-reduced.
+test('T21261', [ grep_errmsg(r'^(yes|no)') ], compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-all -dsuppress-uniques'])