Since the example leads with:

> Many features that make the Bosque IR amenable for automated reasoning involve simplifying and removing sources of irregularity in the semantics.

I do find it strange that it both shows a bug in the logic which causes an irregularity, but also that this irregularity is allowed because of the need of a second check, rather than failing to compile because the type would be narrowed by the initial constraint (if the op argument is add/sub then arg2 MUST be non-none).