Has anyone succeeded in implementing or designing a type-system that combines both type-state (linear types) and effect types (e.g. Koka)?
Edwin Brady has done some work in that area using dependent types in IDRIS. Take a look at his work, in particular Programming and Reasoning with Algebraic Effects and Dependent Types and Resource-dependent Algebraic Effects.
A lot of work on types for $\pi$-calculus does this. See e.g. (1) for a unified system. Sequential languages can be embedded into $\pi$-calculus, so this work also applies to sequential languages.
(1) A Uniform Type Structure for Secure Information Flow, K Honda and N Yoshida.