Why do the reverse binder swap transformation?

[Rodrigo Mesquita]

Dear GHC devs,

I’m wondering about the reverse binder swap transformation, the one in which we substitute occurrences of the case binder by occurrences of the scrutinee (when the scrut. is a variable):

	case x of z { r -> e }
        ===>
	case x of z { r -> e[x/z] }

My question is: why do we do this transformation? An example in which this transformation is beneficial would be great too.

The Note I’ve found about it, Note [Binder-swap during float-out], wasn’t entirely clear to me:

	4. Note [Binder-swap during float-out]
	   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	   In the expression
	        case x of wild { p -> ...wild... }
	   we substitute x for wild in the RHS of the case alternatives:
	        case x of wild { p -> ...x... }
	   This means that a sub-expression involving x is not "trapped" inside the RHS.
	   And it's not inconvenient because we already have a substitution.

	  Note that this is EXACTLY BACKWARDS from the what the simplifier does.
	  The simplifier tries to get rid of occurrences of x, in favour of wild,
	  in the hope that there will only be one remaining occurrence of x, namely
	  the scrutinee of the case, and we can inline it.

Many thanks,
Rodrigo