Some extensions of CBPV annotate effects on F A instead of U B . These systems isolate ef- fects so that they need not be tracked by the typing judgement. Extended Call-by-Push-Value (ECBPV) [ McDermott and Mycroft 2019 ] adds call-by-need evaluation to CBPV and layers an ef- fect system to augment equational reasoning. This system uses an operation 〈 𝜙 〉 𝐵 to extend the effect annotation to other computation types, combining effects in returner types and pushing ef- fects to the result type of functions and inside with-products. Rioux and Zdancewic [ 2020 ] tracks divergence. In this system, the sequencing operation requires that the annotation on the returner type be less than or equal to any annotation on the result of the continuation.