Normalise size expressions during unification.

[athas]

This allows arithmetic expressions involving constant integers to be considered equal, e.g. 3+2 now unifies with 5 (or with 6-1 for that matter).

This is a fairly safe extension, because it only applies to cases that would previously have been an error, and it only makes size expressions smaller. It is also conservative in the sense that it does not constrain future extensions to e.g. allow algebraic rearrangement of sizes during unification.