Let me jump in on this a little bit, since much of the code in this area was originally written by me.
> Are all sizetype (sub-)expressions always of value in that range? > What do we do about the fact that sizetype is unsigned, so -x always > overflows for x != 0? Thus, do we need to disable all a - b -> a + > -b kind of foldings for sizetypes? (we don't) The basic idea is that an overflow of sizetype is either: (1) Detected at a higher level (e.g., testing for maximum sizes of objects) or; (2) Is an undetected error and hence the result of such overflow is undefined. What this means from a practical point of view (but indeed a bit hard to define from a formal point of view) is that the normal addition and subtraction operations (on a 2's complement machines, which all are now) will "do the right thing" in all cases so we can perform all those sorts of folding operations.