First, approaches like Eff take pure functional computation as a basis and layer effects like call/cc or concurrency on top of that. I think it's better to go the other way and take concurrency, or, if you want to start sequential, a lambda-calculus with jumps a la call/cc or lambda-mu, as a basis see pure functional computation as a restriction of the base calculus.

Second, it's unclear that effects should be reflected in types for reasoning. That road leads to complicated typing systems without type inferences (see also dependent types). I think the following alternative is more appealing: stick with lightweight types (think Hindley-Milner), and leave reasoning to an external calculus (variants of Hoare logic).