A hybrid type checker defers parts of the type checking to run time. At compile time, the checker attempts to statically verify as many subtyping constraints as possible. Constraints that cannot be proved by the static checker, are reified as run-time casts in an intermediate language, which is a variant of the blame calculus.

The goal of this work is to simplify casts in the intermediate blame calculus by exploiting context information. To this end, we develop a coercion calculus that corresponds to the blame calculus via a pair of translations and we define the formal framework to simplify these coercions. We give a concrete instance of the calculus and demonstrate that simplification can be regarded as a synthesis problem.