This is the main thing functional programming theorists get excited about when going off the deep end about sufficiently smart compilers. (That and "proving a program is correct" which is a related problem). Basically all FP optimisations would instead work by automatically transforming a program.
The idea behind all these type systems is really to allow automated transforms which preserve the integrity of the program.
It's really too bad that Haskell, with it's referential transparency, doesn't have a way to rewrite things programmatically (well, none that I know of). Rewriting terms would be great in a language like that. It seems that when a typeclass has some laws, and you want to show that an instance of it obeys the laws, you have to bust out the pen and paper. Nothing wrong with that, but it seems like a language like that could support computer-aided rewriting.
Then there are languages whose evaluation is based on term rewriting, like the language Pure.
EDIT: You do have HLint, and the bot that rewrites expressions to point-free style.
I agree that functionally pure code could allow for amazing programmatic rewriting. Imagine coupling that with homoiconic syntax. Not necessarily to have Lisp-style macros, but rather so you could offer repl-based programmatic rewriting/refactoring tools, where the tools know that your code is pure and thus can be "reasoned about mathematically."
The idea behind all these type systems is really to allow automated transforms which preserve the integrity of the program.