Fix a minor crash.
This fixes a crash when doing free synthesis on an inner type.
Fix some expansion bugs.
We no longer generate expressions of the form x - (-y).
Moved checking if the user cancelled inside some loops so we respond faster.
When expanding, we check the depth only at the end, not for each component.  This both helps us find expressions we missed before (e.g., we would not expand tree into x.parent because the latter has greater depth, whatever the target depth) and stops us from showing the user expressions of greater depth (e.g., due to heuristics).