A manifest contract calculus is a lambda-calculus with software
contracts and dynamic contract checking, where software contracts are
part of type information and dynamic contract checking is performed by
casts from one type to another.  Previous work for manifest contract
calculi has studied an optimization to eliminate upcasts, and the
correctness of the optimization by giving logical relations. However,
all proofs of soundness of the logical relations w.r.t. contextual
equivalence are incomplete.

We fix this unfortunate situation and even go further: we extend a
polymorphic manifest contract calculus with a fixed-point operator,
give logical relations for the extended calculus, and show their
soundness with respect to what we call semi-typed contextual
equivalence and that an upcast is logically related to an identity
function.