STA / rule 1
    This rule doesn't say what you mean. The prose says (roughly):
        error = (Expr has empty type) and not(Expr is an exception)
    which means (via one of De Morgan's laws)
        not(error) = not(Expr has empty type) or (Expr is an exception)
    which is not at all what the rule says.

    Specifically, if Expr is one of the exceptions, then (regardless of
    its type!), the prose says that it is *not* an error, but the rule
    says that it *is* an error (because premise 2 fails to hold, and so
    the rule fails to hold, and so supposedly an error is raised).

    All of which is moot, because the rule's conclusion is the same as
    premise 1, so an inference procedure would have no need to apply the
    rule. (So whether it fails or not is inconsequential.)

    It seems to me that the more straightforward way to write the rule is:

        statEnv |- Expr : Type
        Type = empty
        not( Expr is an exception )
        ---------------------------
        statEnv |- Expr raises error

    although it's unclear whether the inference procedure is obliged to
    try to satisfy the rule.

    A more robust alternative would be to go to the STA for each
    expression other than the exceptions, and add a
        not(Type = empty)
    premise (if it's not already implied by other premises).