3.2.3 Static typing judgment

"the input literals '3' and '5' have type integer,"
    Delete "input"?

"so the variable $v also has type integer."
    You don't need to know that 5 has type integer to infer $v's type.

"statEnv |- if Expr1 then ..."
    Add parentheses around Expr1

"The "left half" (the part before the :) of the expression below the line"
    Change "expression" to "judgment".

"corresponds to some [expression/query], for which a type is computed."
    Well, except that the "statEnv |-" isn't part of the expression/query.
    Maybe say that the part between the turnstile and the colon
    corresponds to some expression/query.

"The expression usually has patterns in it"
    Change "expression" to "judgment".

"The expressions above the line"
    Change "expressions" to "judgments".

"the expressions on each side"
    On each side of what? Maybe just change to "those expressions" (or
    "those sub-expressions").

"At each point in the recursion, an appropriate matching inference rule is
sought"
    Maybe clarify what an "appropriate matching" rule is. (A rule whose
    conclusion has a structure that matches that of the premise in
    question.)

"if at any point there is no applicable rule, then static type inference
has failed"
    Not quite. It means that that particular avenue of inference has
    failed; however, an alternative avenue might succeed.

    And actually, I think you've written the spec so that, if failure
    happens, it shouldn't be for lack of a matching rule -- that would
    indicate incompleteness of the spec. Instead, failure of (an avenue
    of) inference should only happen when one is unable to satisfy the
    premises of a rule.

    Some of this discussion might fit back in section 2.1.5.