Two alternatives that I think might be pretty effective at tightening the bound:
We can tighten the local upper bound at each location using any arguments that have already been decided. I think this information might already be freely available so it might be cheap. Even though final abstractions tend to take very small arguments, bigger abstractions might not
If you dont do the above bound tightening, then the bound is equal to the subtree size meaning ancestor match locations subsume lower ones so you can discard the lower ones and not include them in the bound since they cant improve it any more than "delete the parent tree"
Two alternatives that I think might be pretty effective at tightening the bound: