  We describe a new concrete approach to giving predictable error locations for
sequential (flow-sensitive) effect systems. Prior implementations of sequential
effect systems rely on either computing a bottom-up effect and comparing it to
a declaration (e.g., method annotation) or leaning on constraint-based type
inference. These approaches do not necessarily report program locations that
precisely indicate where a program may "go wrong" at runtime.
  Instead of relying on constraint solving, we draw on the notion of a residual
from literature on ordered algebraic structures. Applying these to effect
quantales (a large class of sequential effect systems) yields an implementation
approach which accepts exactly the same program as an original effect quantale,
but for effect-incorrect programs is guaranteed to fail type-checking with
predictable error locations tied to evaluation order. We have implemented this
idea in a generic effect system implementation framework for Java, and report
on experiences applying effect systems from the literature and novel effect
systems to Java programs. We find that the reported error locations with our
technique are significantly closer to the program points that lead to failed
effect checks.
