Improve users guide documentation on rewrite rules with case expression

Summary

I'm trying to see if I could write a rewrite rule to push one of my own functions into the right hand side of a case statement. GHC doesn't complain when I define such a rewrite rule, but it doesn't seem to do anything.

Steps to reproduce

Here is a minimal example:

module Test where

test :: a -> b -> (a, b)
test a b = (a, b)
{-# NOINLINE test #-}

prog :: (Int, Int) -> (Int, Int)
prog x = test (case x of (l, r) -> l) 0

{-# RULES
   "test/case-tup" forall (x :: (Int, Int)) (y :: Int) (z :: Int).
      test (case x of (l, r) -> y) z = case x of (l, r) -> test y z
  #-}

Expected behavior

I would expect the "test/case-tup" rule to fire when compiled with ghc -O and produce the following code:

prog :: (Int, Int) -> (Int, Int)
prog x = case x of (l, r) -> test l 0

However, I couldn't find examples of rewrite rules with case statements in the documentation, so I don't really know what to expect.

Environment

• GHC version used: 8.10.4

Optional:

• Operating System: NixOS 21.05
• System Architecture: x86_64