[xxpor]

If you can derive this and prove it, shouldn't this optimization be done (theoretically) completely automatically by the compiler?

[quchen]

Computers are good at verifying things, but bad at coming up with them.

(An example for something computers can come up with is free theorems, but in this case that wouldn't have helped.)

[Kutta]

The rewriting part - if not the comping up with proofs part - is done automatically in quite a few libraries. You can specify the expression rewriting rules in pragmas in your source and GHC will carry them out.