qrczak@knm.org.pl (Marcin 'Qrczak' Kowalczyk) further clarifies my clarification:
case ERROR of x -> expr => ERROR glb expr[?/x]
The subject of errors vs. bottoms is discussed in http://research.microsoft.com/~simonpj/papers/imprecise-exceptions.ps.gz
Indeed. I crawled through my stack of electronic papers, and couldn't find the reference. As I noted in my earlier messages, I was deliberately dodging the issue of *catching* exceptions, as it really requires a thorough treatment. :-) The "?" in the above reduction is their special 0 term. They equate divergence with exceptional convergence within the functional calculus for the reasons I outlined [I reconstructed those reasons from memory and my own experience, so differences are due to my faulty recollection]. Their notion of refinement justifies the reduction I mentioned in my mail:
case ERROR of x -> expr => ERROR
In all, an excellent paper for those who are interested in this topic. -Jan-Willem Maessen