I think you would want both: algebraic effects and very fine-grained effect reasoning. For example, in all most all languages it is vital that functions such as

I think you would want both: algebraic effects and very fine-grained effect reasoning. For example, in all most all languages it is vital that functions such as "equal" and "hash" are pure. It is an open problem how to combine our fine-grained Boolean unification-based effect system with other algebraic effect systems (e.g. row polymorphic ones). I hope the future will tell :)