Is there any plan to have effect types like in koka, where the effects that a function performs are visible in the type, and handling an effect eliminates it from the function's type?
The medium-term plan is indeed to have such a typed effect system. This one of the reason why the effect system is still considered to be experimental: we expect to see some breaking changes once effects become typed.