That's quite old, but interesting. I should have asked at the International Conference on Functional Programming last week, what became out of the Supercompilation idea for Haskell. It was not mentioned, though.
IIRC from the "Binary Translation Using Peephole Superoptimizers" presentation from OSDI 2008 (Google found a summary at http://eurosys.org/blog/?p=109), supercompilation is a brute force approach. Making it perform is, no doubt, challenging.
Can anyone explain the notation he uses for the termination check?