It seems to me that the best answer, rather than constraining equational reasoning, is to recognize what we're doing. We start out with a specification for the program we're writing (this could be a Haskell script for a previous version of the program, or just a set of equations (or other properties) we hope it satisfies). This specification is a predicate on (denotations of) Haskell functions, say S(f). We then derive an implementation of the program. This implementation is also a predicate, I(f). By saying we have derived this implementation, we mean that S(f) => I(f). By contrast, the program is correct (our reasoning was pointful) iff I(f) => S(f). This can be guaranteed given the two conditions set forth by John Hughes in "The Design of a Pretty-Printing Library", consistency of the specification and termination of the implementation. More precisely, we want the two conditions: (1) There is at least one function f such that S(f). (2) There is at most one function f such that I(f). Given (2), we know that {f | I(f)} is either a singleton set or the null set. In either case, the powerset P({f | I(f)}) = {{}, {f | I(f)}}. Now, S(f) => I(f), so {f | S(f)} subset {f | I(f)}; thus, {f | S(f)} is either {} or {f | I(f)}. If there is at least one f such that S(f), then {f | S(f)} /= {}, so {f | S(f)} = {f | I(f)}, or equivalently S(f) = I(f), so I(f) => S(f). So if our specification is consistent and our implementation is as total as possible (which is equivalent to (2)), the derivation/re-factoring/whatever we're doing succeeds. Otherwise we've got either a bad specification or a bad implementation, anyway, so we'll need to investigate the issue in greater detail. Jonathan Cast http://sourceforge.net/projects/fid-core http://sourceforge.net/projects/fid-emacs