> This may be too much advanced type theory for a useful language.

I think a lot of things taken for granted these days were considered "too complicated" some time ago: think of how widespread pattern matching, closures, generics, or functional idioms in imperative languages are, and compare to e.g. Java 1.0.

My feeling is that the "acceptable level of complexity" for programming languages goes up over time, so probably stuff like effect types will be almost everywhere in another 10 years.