Thomas Davie wrote:
the only change is that computations resulting in the
unit type *can't* non terminate, because we can always optimize them
down to ().
No. "Optimizing them down to ()" changes the semantics of the
computation. This is incorrect behavior.