On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr <timon.gehr@gmx.ch> wrote:

Please see Sec
10.2 Unique supply trees -- you might see some familiar code. Although
my example was derived independently, it has the same kernel of
badness as the example in Launchbury and Peyton-Jones. The authors
point out a subtlety in the code, admitting that they fell into the
trap themselves.

They informally note that the final result depends on the order of evaluation and is therefore not always uniquely determined. (because the order of evaluation is only loosely specified.)

If the final result depends on the order of evaluation, then the context in which the result is defined is not referentially transparent. If a context is referentially opaque, then equational reasoning "can fail" -- i.e., it is no longer a valid technique of analysis, since the axioms on which it depends are no longer satisfied:

"It is necessary that four and four is eight"

"The number of planets is eight"

does not imply

"It is necessary that the number of planets is eight", as "equational reasoning" (or, better put, "substitution of equals", the first order axiom for equality witnessing Leibniz equality) requires.

In particular, quotation marks, necessity, and unsafeInterleaveST are referentially opaque contexts.