update the implementation of inferAndCheckExpr in Checker.scala

[ivoysey]

from the comment at the top of the function:

      * TODO: document the invariants of this function. at several call sites, we assume that the
      *   annotation in the expression returned matches the type returned (and therefore to not call
      *   ParserUtil.updateExprType to enforce that). That invariant is held in some of the returns
      *   below, but not all of them. It should be all of them, and that should be documented here.
      *   It's possible that changing the code to enforce that may break test cases, but unlikely.
      *   The typechecker tests we have now do not have perfect coverage; I believe many of them
      *   would fail because of the lack of this invariant if it was larger.