diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,5 @@
 
-# Extensible effects (![Hackage](https://img.shields.io/hackage/v/extensible-effects.svg))
+# Extensible effects (![Hackage](https://img.shields.io/hackage/v/extensible-effects.svg), ![GHC](https://img.shields.io/badge/GHC-8.2.2%20%7C%208.4.4%20%7C%208.6.3-blue.svg))
 
 [![Build Status](https://travis-ci.org/suhailshergill/extensible-effects.svg?branch=master)](https://travis-ci.org/suhailshergill/extensible-effects)
 [![Join the chat at https://gitter.im/suhailshergill/extensible-effects](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/suhailshergill/extensible-effects?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
@@ -75,11 +75,11 @@
 
 The most common effects used are `Writer`, `Reader`, `Exception` and `State`.
 
-For the `Writer`, `Reader` and `State`, there are lazy and a strict variants.
-Each has its own module that provide the same interface.
-By importing one or the other, it can be controlled if the effect is strict or
-lazy in its inputs and outputs.
-Unless required otherwise, it is suggested to use the lazy variants.
+`Writer`, `Reader` and `State` all provide lazy and strict variants. Each has
+its own module that exposes a common interface. Importing one or the other
+controls whether the effect is strict or lazy in its inputs and outputs. It's
+recommended that you use the lazy variants by default unless you know you need
+strictness.
 
 In this section, only the core functions associated with an effect are
 presented.
@@ -123,9 +123,8 @@
 runState :: s -> Eff (State s ': r) a -> Eff r (a, s)
 ```
 
-The `get` functions accesses the current state and makes it usable within the
-further computation.
-The `put` function sets the state to the given value.
+The `get` function fetches the current state and makes it available within
+subsequent computation. The `put` function sets the state to a given value.
 `modify` updates the state using a mapping function by combining `get` and
 `put`.
 
@@ -147,8 +146,8 @@
 runReader :: e -> Eff (Reader e ': r) a -> Eff r a
 ```
 
-The environment given to the handle the reader effect is the one given during
-the computation if asked for.
+`ask` can be used to retrieve the environment provided to `runReader` from
+within a computation which has the `Reader` effect.
 
 #### The Writer Effect
 
@@ -156,7 +155,7 @@
 import Control.Eff.Writer.{Strict | Lazy}
 ```
 
-The writer effect allows to output messages during a computation.
+The writer effect allows one to collect messages during a computation.
 It is sometimes referred to as write-only state, which gets retrieved at the
 end of the computation.
 
@@ -167,8 +166,8 @@
 ```
 
 Running a writer can be done in several ways.
-The most general function is `runWriter` that folds over all written values.
-However, if you only want to collect the the values written, the `runListWriter`
+The most general function is `runWriter` which folds over all written values.
+However, if you only want to collect the values written, the `runListWriter`
 function does that.
 
 Note that compared to mtl, the value written has no Monoid constraint on it and
@@ -206,8 +205,8 @@
 
 There are several constructs that make it easier to work with the effects.
 
-If only a part of the result is necessary for the further computation, have a
-look at the `eval*` and `exec*` functions, which exist for some effects.
+If only a part of the result is necessary for further computation, have a
+look at the `eval*` and `exec*` functions which exist for some effects.
 The `exec*` functions discard the result of the computation (the `a` type).
 The `eval*` functions discard the final result of the effect.
 
@@ -216,21 +215,23 @@
 possible to use the type operator `<::` and write
 `[ Exc e, State s ] <:: r => ...`, which has the same meaning.
 
-It might be convenient to include the necessary language extensions and the
-disabling of the class-constriant warnings in the cabal-file of your project.
-*Explanation is work in progress*
+It might be convenient to include the necessary language extensions and disable
+class-constraint warnings in your project's `.cabal` file (or `package.yaml` if
+you're using `stack`).
 
+*Explanation is a work in progress.*
+
 ## Other Effects
 
-*work in progress*
+*Work in progress.*
 
 ## Integration with IO
 
-`IO` as well as any other monad can be used as a base type for `Lift` effect.
-There may be at most one instance of `Lift` effect in the effects list, and it
-must be handled the last. `Control.Eff.Lift` exports `runLift` handler and
-`lift` function, that provides an ability to run arbitrary monadic actions.
-Also, there are convenient type aliases, that allow for shorter type constraints.
+`IO` or any other monad can be used as a base type for the `Lift` effect.
+There may be at most one instance of the `Lift` effect in the effects list, and it
+must be handled last. `Control.Eff.Lift` exports the `runLift` handler and
+`lift` function which provide the ability to run arbitrary monadic actions.
+Also, there are convenient type aliases that allow for shorter type constraints.
 
 ```haskell
 f :: IO ()
@@ -247,21 +248,22 @@
 ```
 
 Note that, since `Lift` is a terminal effect, you do not need to use `run` to
-extract pure value. Instead, `runLift` returns a value wrapped in whatever monad
-you chose to use.
+extract pure values. Instead, `runLift` returns a value wrapped in whatever
+monad you chose to use.
 
-In addition, `Lift` effect provides `MonadBase`, `MonadBaseControl`, and `MonadIO`
-instances, that may be useful, especially with packages like [lifted-base](http://hackage.haskell.org/package/lifted-base),
+Additionally, the `Lift` effect provides `MonadBase`, `MonadBaseControl`, and
+`MonadIO` instances that may be useful, especially with packages like
+[lifted-base](http://hackage.haskell.org/package/lifted-base),
 [lifted-async](http://hackage.haskell.org/package/lifted-async), and other
 code that uses those typeclasses.
 
 ## Integration with Monad Transformers
 
-*work in progress*
+*Work in progress.*
 
 ## Writing your own Effects and Handlers
 
-*work in progress*
+*Work in progress.*
 
 ## Other packages
 
@@ -272,7 +274,7 @@
 
 ## Background
 
-extensible-effects is based on the work
+`extensible-effects` is based on the work of
 [Extensible Effects: An Alternative to Monad Transformers](http://okmij.org/ftp/Haskell/extensible/).
 The [paper](http://okmij.org/ftp/Haskell/extensible/exteff.pdf) and
 the followup [freer paper](http://okmij.org/ftp/Haskell/extensible/more.pdf)
@@ -281,9 +283,10 @@
 ## Limitations
 
 ### Ambiguity-Flexibility tradeoff
-The extensibility of `Eff` comes at the cost of some ambiguity. A useful pattern
-to mitigate the ambiguity is to specialize the call to the handler of effects
-using [type application](https://ghc.haskell.org/trac/ghc/wiki/TypeApplication)
+The extensibility of `Eff` comes at the cost of some ambiguity. A useful
+pattern to mitigate this ambiguity is to specialize calls to effect handlers
+using
+[type application](https://ghc.haskell.org/trac/ghc/wiki/TypeApplication)
 or type annotation. Examples of this pattern can be seen in
 [Example/Test.hs](./test/Control/Eff/Example/Test.hs).
 
@@ -293,8 +296,8 @@
 
 Some examples where the cost of extensibility is apparent:
 
-  * Common functions can't be grouped using typeclasses, e.g.
-    the `ask` and `getState` functions can't be grouped with some
+  * Common functions can't be grouped using typeclasses, e.g. the `ask` and
+    `getState` functions can't be grouped in the case of:
 
     ```haskell
     class Get t a where
@@ -305,10 +308,5 @@
     a constraint on `t`, and nothing more. To specify fully, a parameter
     involving the type `t` would need to be added, which would defeat the
     point of having the grouping in the first place.
-  * Code requires greater number of type annotations. For details see
+  * Code requires a greater number of type annotations. For details see
     [#31](https://github.com/suhailshergill/extensible-effects/issues/31).
-
-### Current implementation only supports GHC version 7.8 and above
-This is not a fundamental limitation of the design or the approach, but there is
-an overhead with making the code compatible across a large number of GHC
-versions. If this is needed, patches are welcome :)
diff --git a/benchmark/Benchmarks.hs b/benchmark/Benchmarks.hs
--- a/benchmark/Benchmarks.hs
+++ b/benchmark/Benchmarks.hs
@@ -7,7 +7,7 @@
 import Criterion.Main
 import Control.Eff as E
 import Control.Eff.Exception as E.Er
-import Control.Eff.NdetEff as E.ND
+import Control.Eff.Logic.NDet as E.ND
 import Control.Eff.State.Strict as E.S
 import Control.Monad
 
@@ -43,11 +43,11 @@
                                           , bench "eff" $ whnf mainMax1_Eff 10000
                                           ]
                       ]
-  , bgroup "pyth" [ bgroup "ndet" [ bench "mtl" $ whnf mainN_MTL 20
-                                  , bench "eff" $ whnf mainN_Eff 20
+  , bgroup "pyth" [ bgroup "ndet" [ bench "mtl" $ whnf mainN_MTL 100
+                                  , bench "eff" $ whnf mainN_Eff 100
                                   ]
-                  , bgroup "ndet : st" [ bench "mtl" $ nf mainNS_MTL 15
-                                       , bench "eff" $ nf mainNS_Eff 15
+                  , bgroup "ndet : st" [ bench "mtl" $ nf mainNS_MTL 100
+                                       , bench "eff" $ nf mainNS_Eff 100
                                        ]
                   ]
   ]
@@ -160,7 +160,7 @@
 case_pythr_ndet :: HU.Assertion
 case_pythr_ndet =
   HU.assertEqual "pythr_MTL" pyth20 ((runCont (pyth1 20) (\x -> [x])) :: [(Int,Int,Int)])
-  >> HU.assertEqual "pythr_EFF" pyth20 ((run . E.ND.makeChoiceA $ pyth1 20) :: [(Int,Int,Int)])
+  >> HU.assertEqual "pythr_EFF" pyth20 ((run . E.ND.makeChoice $ pyth1 20) :: [(Int,Int,Int)])
 
 
 -- There is no instance of MonadPlus for ContT
@@ -177,7 +177,7 @@
 
 mainN_MTL n = ((runCont (pyth1 n) (\x -> [x])) :: [(Int,Int,Int)])
 
-mainN_Eff n = ((run . E.ND.makeChoiceA $ pyth1 n) :: [(Int,Int,Int)])
+mainN_Eff n = ((run . E.ND.makeChoice $ pyth1 n) :: [(Int,Int,Int)])
 
 -- Adding state: counting the number of choices
 
@@ -190,7 +190,7 @@
   S.put $! (cnt + 1)
   if x*x + y*y == z*z then return (x,y,z) else mzero
 
-pyth2E :: (Member (E.S.State Int) r, Member NdetEff r) =>
+pyth2E :: (Member (E.S.State Int) r, Member NDet r) =>
           Int -> Eff r (Int, Int, Int)
 pyth2E upbound = do
   x <- iota 1 upbound
@@ -213,4 +213,4 @@
   in ((l::[(Int,Int,Int)]), (cnt::Int))
   where
     pyth2Er :: Int -> ([(Int,Int,Int)],Int)
-    pyth2Er n = run . E.S.runState 0 . E.ND.makeChoiceA $ pyth2E n
+    pyth2Er n = run . E.S.runState 0 . E.ND.makeChoice $ pyth2E n
diff --git a/extensible-effects.cabal b/extensible-effects.cabal
--- a/extensible-effects.cabal
+++ b/extensible-effects.cabal
@@ -6,7 +6,7 @@
 -- PVP summary:      +-+------- breaking API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             3.0.0.0
+version:             5.0.0.1
 
 -- A short (one-line) description of the package.
 synopsis:            An Alternative to Monad Transformers
@@ -41,7 +41,7 @@
 
 category:            Control, Effect
 
-tested-with:         GHC==8.4.1, GHC==8.2.2, GHC==8.0.2, GHC==7.10.3, GHC==7.8.4
+tested-with:         GHC==8.6.3, GHC==8.4.4, GHC==8.2.2
 
 build-type:          Simple
 
@@ -56,23 +56,20 @@
   default: False
   manual: True
 
-flag force-openunion-51
-  description:         Force usage of OpenUnion51.hs implementation
-  default:             False
-  manual:              True
+flag dump-core
+  description: Dump HTML for the core generated by GHC during compilation
+  default:     False
 
 library
-  ghc-options:         -Wall
+  ghc-options:         -Wall -O2
   -- Modules exported by the library.
   exposed-modules:     Control.Eff
-                       Control.Eff.Choose
                        Control.Eff.Coroutine
-                       Control.Eff.Cut
                        Control.Eff.Example
                        Control.Eff.Exception
                        Control.Eff.Fresh
-                       Control.Eff.Lift
-                       Control.Eff.NdetEff
+                       Control.Eff.Logic.Core
+                       Control.Eff.Logic.NDet
                        Control.Eff.Operational
                        Control.Eff.Operational.Example
                        Control.Eff.Reader.Lazy
@@ -90,8 +87,7 @@
   -- Modules included in this library but not exported.
   other-modules:       Control.Eff.Internal
                        Data.FTCQueue
-  if flag(force-openunion-51)
-    cpp-options:       -DFORCE_OU51
+                       Control.Eff.Logic.Experimental
 
   default-extensions:  NoMonomorphismRestriction
                      , MonoLocalBinds
@@ -128,20 +124,13 @@
                        , Trustworthy
                        , TypeOperators
                        , UndecidableInstances
-  if impl(ghc < 7.8.1)
-     other-extensions: OverlappingInstances
-  if impl(ghc >= 8.2)
-     ghc-options:      -Wno-simplifiable-class-constraints
 
   -- Other library packages from which modules are imported.
-  build-depends:       base >= 4.7 && < 4.12
+  build-depends:       base >= 4.7 && < 5
                        -- For MonadBase
-               ,       transformers-base == 0.4.*
+                     , transformers-base == 0.4.*
                        -- For MonadBaseControl
-               ,       monad-control >= 1.0 && < 1.1
-  if impl(ghc < 8.0)
-                       -- For MonadIO
-     build-depends:    transformers >= 0.2.0.0
+                     , monad-control >= 1.0 && < 1.1
 
   -- Directories containing source files.
   hs-source-dirs:      src
@@ -149,25 +138,26 @@
   -- Base language which the package is written in.
   default-language:    Haskell2010
 
-  -- TODO: uncomment when https://github.com/haskell/cabal/issues/2527 is
-  -- resolved
   if flag(lib-Werror)
      ghc-options: -Werror
 
+  if flag(dump-core)
+    build-depends: dump-core
+    ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
+
 test-suite extensible-effects-tests
   type: exitcode-stdio-1.0
   main-is: Test.hs
   hs-source-dirs: test/
   other-modules:  Utils
                 , Control.Eff.Test
-                , Control.Eff.Choose.Test
                 , Control.Eff.Coroutine.Test
-                , Control.Eff.Cut.Test
                 , Control.Eff.Example.Test
                 , Control.Eff.Exception.Test
                 , Control.Eff.Fresh.Test
-                , Control.Eff.Lift.Test
-                , Control.Eff.NdetEff.Test
+                , Control.Eff.Logic.NDet.Bench
+                , Control.Eff.Logic.NDet.Test
+                , Control.Eff.Logic.Test
                 , Control.Eff.Operational.Test
                 , Control.Eff.Reader.Lazy.Test
                 , Control.Eff.Reader.Strict.Test
@@ -186,10 +176,11 @@
      ghc-options:      -fno-warn-type-defaults -fno-warn-missing-signatures -fno-warn-name-shadowing
 
   build-depends:
-                base >= 4.7 && < 4.12
+                base >= 4.7 && < 5
               , QuickCheck
               , HUnit
               , monad-control >= 1.0
+              , mtl
               , silently >= 1.2
               , test-framework == 0.8.*
               , test-framework-hunit == 0.3.*
@@ -216,7 +207,7 @@
   type: exitcode-stdio-1.0
   main-is: Benchmarks.hs
   hs-source-dirs: benchmark/
-  ghc-options: -Wall -O2 -threaded -fdicts-cheap -funbox-strict-fields
+  ghc-options: -Wall -O2 -threaded -rtsopts
   if impl(ghc >= 8.0)
      ghc-options:      -Wno-type-defaults -Wno-missing-signatures
                        -Wno-name-shadowing -Wno-unused-matches
@@ -225,7 +216,7 @@
                        -fno-warn-name-shadowing -fno-warn-unused-matches
 
   build-depends:
-                base >= 4.7 && < 4.12
+                base >= 4.7 && < 5
               , criterion
               , extensible-effects
               , mtl
diff --git a/src/Control/Eff.hs b/src/Control/Eff.hs
--- a/src/Control/Eff.hs
+++ b/src/Control/Eff.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE Safe #-}
 {-# LANGUAGE ExplicitNamespaces #-}
 
 -- | A monadic library for implementing effectful computation in a modular way.
@@ -21,9 +22,14 @@
 --
 
 module Control.Eff
-  ( -- * Effect base-type
+  ( -- * Effect type
     Internal.run
   , Internal.Eff
+    -- * Lift IO computations
+  , Internal.lift, Internal.runLift
+  , Internal.catchDynE
+  , Internal.HandlerDynE(..), Internal.catchesDynE
+  , Internal.Lift(..), Internal.Lifted, Internal.LiftedBase
     -- * Effect list
   , OpenUnion.Member
   , OpenUnion.SetMember
diff --git a/src/Control/Eff/Choose.hs b/src/Control/Eff/Choose.hs
deleted file mode 100644
--- a/src/Control/Eff/Choose.hs
+++ /dev/null
@@ -1,81 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE Safe #-}
--- The following is needed to define MonadPlus instance. It is decidable
--- (there is no recursion!), but GHC cannot see that.
-{-# LANGUAGE UndecidableInstances #-}
-
--- | Nondeterministic choice effect
-module Control.Eff.Choose ( Choose (..)
-                          , choose
-                          , makeChoice
-                          , mzero'
-                          , mplus'
-                          ) where
-
-import Control.Eff
-import Control.Eff.Extend
-import Control.Eff.Lift
-      
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Base
-import Control.Monad.Trans.Control
-
--- ------------------------------------------------------------------------
--- | Non-determinism (choice)
---
--- choose lst non-deterministically chooses one value from the lst
--- choose [] thus corresponds to failure
--- Unlike Reader, Choose is not a GADT because the type of values
--- returned in response to a (Choose a) request is just a, without
--- any constraints.
-newtype Choose a = Choose [a]
-
-instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
-         ) => MonadBaseControl m (Eff (Choose ': r)) where
-    type StM (Eff (Choose ': r)) a = StM (Eff r) [a]
-    liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
-                       f (runInBase . makeChoice)
-    restoreM x = do lst <- raise (restoreM x)
-                    choose lst
-
--- | choose lst non-deterministically chooses one value from the lst
--- choose [] thus corresponds to failure
-choose :: Member Choose r => [a] -> Eff r a
-choose lst = send $ Choose lst
-
--- | MonadPlus-like operators are expressible via choose
-mzero' :: Member Choose r => Eff r a
-mzero' = choose []
-
--- | MonadPlus-like operators are expressible via choose
-mplus' :: Member Choose r => Eff r a -> Eff r a -> Eff r a
-mplus' m1 m2 = join $ choose [m1,m2]
-
--- | MonadPlus-like operators are expressible via choose
-instance Member Choose r => Alternative (Eff r) where
-  empty = mzero'
-  (<|>) = mplus'
-
-instance Member Choose r => MonadPlus (Eff r) where
-  mzero = empty
-  mplus = (<|>)
-
--- | Run a nondeterministic effect, returning all values.
-makeChoice :: forall a r. Eff (Choose ': r) a -> Eff r [a]
-makeChoice = handle_relay
-  (return . (:[]))
-  (\(Choose lst) k -> handle lst k)
-  where
-    handle :: [t] -> (t -> Eff r [a]) -> Eff r [a]
-    handle []  _ = return []
-    handle [x] k = k x
-    handle lst k = fmap concat $ mapM k lst
diff --git a/src/Control/Eff/Coroutine.hs b/src/Control/Eff/Coroutine.hs
--- a/src/Control/Eff/Coroutine.hs
+++ b/src/Control/Eff/Coroutine.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE Safe #-}
 -- | Coroutines implemented with extensible effects
 module Control.Eff.Coroutine( Yield (..)
+                            , withCoroutine
                             , yield
                             , runC
                             , Y (..)
@@ -13,6 +14,8 @@
 import Control.Eff
 import Control.Eff.Extend
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | Co-routines
 -- The interface is intentionally chosen to be the same as in transf.hs
@@ -35,13 +38,16 @@
 --
 --   Type parameter @w@ is the type of the value returned from the
 --   coroutine when it has completed.
-data Y r a w = Y a (w -> Eff r (Y r a w))
+data Y r w a = Y (w -> Eff r (Y r w a)) a
              | Done
 
+-- | Return a pure value
+withCoroutine :: Monad m => b -> m (Y r w a)
+withCoroutine = const $ return Done
+-- | Given a continuation and a request, respond to it
+instance Handle (Yield a b) (Yield a b : r) w (Eff r (Y r b a)) where
+  handle step q (Yield a) = return $ Y (step . (q ^$)) a
 
 -- | Launch a thread and report its status
-runC :: Eff (Yield a b ': r) w -> Eff r (Y r a b)
-runC m = handle_relay
-  (const $ return Done)
-  (\(Yield a) k -> return $ Y a k)
-   m
+runC :: Eff (Yield a b ': r) w -> Eff r (Y r b a)
+runC = fix (handle_relay withCoroutine)
diff --git a/src/Control/Eff/Cut.hs b/src/Control/Eff/Cut.hs
deleted file mode 100644
--- a/src/Control/Eff/Cut.hs
+++ /dev/null
@@ -1,84 +0,0 @@
-{-# LANGUAGE FlexibleContexts, TypeOperators, DataKinds #-}
-{-# LANGUAGE Safe #-}
--- | An example of non-trivial interaction of effects, handling of two
--- effects together
--- Non-determinism with control (cut)
--- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper.
--- Hinze suggests expressing cut in terms of cutfalse:
---
--- > = return () `mplus` cutfalse
--- > where
--- >  cutfalse :: m a
---
--- satisfies the following laws:
---
--- >  cutfalse >>= k  = cutfalse              (F1)
--- >  cutfalse | m    = cutfalse              (F2)
---
--- (note: @m \``mplus`\` cutfalse@ is different from @cutfalse \``mplus`\` m@).
--- In other words, cutfalse is the left zero of both bind and mplus.
---
--- Hinze also introduces the operation @`call` :: m a -> m a@ that
--- delimits the effect of cut: @`call` m@ executes m. If the cut is
--- invoked in m, it discards only the choices made since m was called.
--- Hinze postulates the axioms of `call`:
---
--- >  call false = false                          (C1)
--- >  call (return a | m) = return a | call m     (C2)
--- >  call (m | cutfalse) = call m                (C3)
--- >  call (lift m >>= k) = lift m >>= (call . k) (C4)
---
--- @`call` m@ behaves like @m@ except any cut inside @m@ has only a local effect,
--- he says.
---
--- Hinze noted a problem with the \"mechanical\" derivation of backtracing
--- monad transformer with cut: no axiom specifying the interaction of
--- call with bind; no way to simplify nested invocations of call.
---
--- We use exceptions for cutfalse
--- Therefore, the law @cutfalse >>= k = cutfalse@
--- is satisfied automatically since all exceptions have the above property.
-module Control.Eff.Cut where
-
-import Control.Eff
-import Control.Eff.Extend
-import Control.Eff.Exception
-import Control.Eff.Choose
-
-data CutFalse = CutFalse
-
-cutfalse :: Member (Exc CutFalse) r => Eff r a
-cutfalse = throwError CutFalse
-
--- | The interpreter -- it is like reify . reflect with a twist.  Compare this
--- implementation with the huge implementation of call in Hinze 2000 (Figure 9).
--- Each clause corresponds to the axiom of call or cutfalse.  All axioms are
--- covered.
---
--- The code clearly expresses the intuition that call watches the choice points
--- of its argument computation. When it encounteres a cutfalse request, it
--- discards the remaining choicepoints.  It completely handles CutFalse effects
--- but not non-determinism
-call :: forall a r. Member Choose r => Eff (Exc CutFalse ': r) a -> Eff r a
-call m = loop [] m where
-  loop :: Member Choose r
-       => [Eff (Exc CutFalse ': r) a]
-       -> Eff (Exc CutFalse ': r) a
-       -> Eff r a
-  loop jq (Val x) = return x `mplus'` next jq          -- (C2)
-  loop jq (E u q) = case decomp u of
-    Right (Exc CutFalse) -> mzero'  -- drop jq (F2)
-    Left u0 -> check jq u0 q
-
-  check :: forall b. [Eff (Exc CutFalse ': r) a]
-        -> Union r b -> Arrs (Exc CutFalse ': r) b a -> Eff r a
-  check jq u _ | Just (Choose []) <- prj u  = next jq  -- (C1)
-  check jq u q | Just (Choose [x]) <- prj u = loop jq (q ^$ x)  -- (C3), optim
-  check jq u q | Just (Choose lst) <- prj u = next $ map (q ^$) lst ++ jq -- (C3)
-  check jq u q = loop jq (E (weaken u) q)     -- (C4)
-
-  next :: Member Choose r
-       => [Eff (Exc CutFalse ': r) a]
-       -> Eff r a
-  next []    = mzero'
-  next (h:t) = loop t h
diff --git a/src/Control/Eff/Example.hs b/src/Control/Eff/Example.hs
--- a/src/Control/Eff/Example.hs
+++ b/src/Control/Eff/Example.hs
@@ -82,14 +82,14 @@
 
 handUp :: Eff (Move ': r) a -> Eff r a
 handUp (Val x) = return x
-handUp (E u q) = case decomp u of
+handUp (E q u) = case decomp u of
   Right Move -> handDown $ qApp q ()
   -- Relay other requests
-  Left u0     -> E u0 ident >>= handUp . qApp q
+  Left u0     -> E ident u0 >>= handUp . qApp q
 
 handDown :: Eff (Move ': r) a -> Eff r a
 handDown (Val x) = return x
-handDown (E u q) = case decomp u of
+handDown (E q u) = case decomp u of
   Right Move -> handUp $ qApp q ()
   -- Relay other requests
-  Left u0     -> E u0 ident >>= handDown . qApp q
+  Left u0     -> E ident u0 >>= handDown . qApp q
diff --git a/src/Control/Eff/Exception.hs b/src/Control/Eff/Exception.hs
--- a/src/Control/Eff/Exception.hs
+++ b/src/Control/Eff/Exception.hs
@@ -8,6 +8,8 @@
 {-# LANGUAGE Safe #-}
 -- | Exception-producing and exception-handling effects
 module Control.Eff.Exception ( Exc (..)
+                            , exc
+                            , withException
                             , Fail
                             , throwError
                             , throwError_
@@ -26,21 +28,31 @@
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Monad (void)
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | Exceptions
 --
 -- exceptions of the type e; no resumption
 newtype Exc e v = Exc e
 
+-- | Embed a pure value
+withException :: Monad m => a -> m (Either e a)
+withException = return . Right
+-- | Throw an error
+exc :: Monad m => e -> m (Either e a)
+exc = return . Left
+-- | Given a callback, and an 'Exc' request, respond to it.
+instance Monad m => Handle (Exc e) r a (m (Either e a)) where
+  handle _ _ (Exc e) = exc e
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (Exc e ': r)) where
     type StM (Eff (Exc e ': r)) a = StM (Eff r) (Either e a)
     liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
@@ -69,9 +81,7 @@
 
 -- | Run a computation that might produce an exception.
 runError :: Eff (Exc e ': r) a -> Eff r (Either e a)
-runError = handle_relay
-  (return . Right)
-  (\(Exc e) _k -> return (Left e))
+runError = fix (handle_relay withException)
 
 -- | Runs a failable effect, such that failed computation return 'Nothing', and
 --   'Just' the return value on success.
@@ -84,14 +94,14 @@
 -- exception
 catchError :: Member (Exc e) r =>
         Eff r a -> (e -> Eff r a) -> Eff r a
-catchError m handle = interpose return (\(Exc e) _k -> handle e) m
+catchError m h = fix (respond_relay' (\_ _ (Exc e) -> h e) return) m
 
 -- | Add a default value (i.e. failure handler) to a fallible computation.
 -- This hides the fact that a failure happened.
 onFail :: Eff (Fail ': r) a -- ^ The fallible computation.
        -> Eff r a           -- ^ The computation to run on failure.
        -> Eff r a
-onFail e handle = runFail e >>= maybe handle return
+onFail e handle_ = runFail e >>= maybe handle_ return
 {-# INLINE onFail #-}
 
 -- | Run a computation until it produces an exception,
@@ -100,7 +110,7 @@
            => (e -> e')
            -> Eff (Exc e ': r) a
            -> Eff r a
-rethrowError t eff = runError eff >>= either (throwError . t) return
+rethrowError t e = runError e >>= either (throwError . t) return
 
 -- | Treat Lefts as exceptions and Rights as return values.
 liftEither :: (Member (Exc e) r) => Either e a -> Eff r a
@@ -108,7 +118,7 @@
 {-# INLINE liftEither #-}
 
 -- | `liftEither` in a lifted Monad
-liftEitherM :: (Member (Exc e) r, SetMember Lift (Lift m) r)
+liftEitherM :: (Member (Exc e) r, Lifted m r)
             => m (Either e a)
             -> Eff r a
 liftEitherM m = lift m >>= liftEither
@@ -120,7 +130,7 @@
 {-# INLINE liftMaybe #-}
 
 -- | `liftMaybe` in a lifted Monad
-liftMaybeM :: (Member Fail r, SetMember Lift (Lift m) r)
+liftMaybeM :: (Member Fail r, Lifted m r)
            => m (Maybe a)
            -> Eff r a
 liftMaybeM m = lift m >>= liftMaybe
diff --git a/src/Control/Eff/Extend.hs b/src/Control/Eff/Extend.hs
--- a/src/Control/Eff/Extend.hs
+++ b/src/Control/Eff/Extend.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE PatternSynonyms #-}
+
 -- | This module exports functions, types, and typeclasses necessary for
 -- implementing a custom effect and/or effect handler.
 --
@@ -6,18 +9,24 @@
   ( -- * The effect monad
     Eff(..)
   , run
+  , eff
+    -- * Lifting operations
+  , Lift(..), Lifted, LiftedBase
+  , lift, runLift
+  , catchDynE
+  , HandlerDynE(..), catchesDynE
     -- * Open Unions
   , OpenUnion.Union
   , OpenUnion.Member
   , inj
-  , prj
-  , decomp
+  , prj, pattern OpenUnion.U0'
+  , decomp, pattern OpenUnion.U0, pattern OpenUnion.U1
   , SetMember
   , weaken
   -- * Helper functions that are used for implementing effect-handlers
-  , handle_relay
-  , handle_relay_s
-  , interpose
+  , Handle(..)
+  , Relay(..)
+  , handle_relay', respond_relay'
   , raise
   , send
   -- * Arrow types and compositions
diff --git a/src/Control/Eff/Fresh.hs b/src/Control/Eff/Fresh.hs
--- a/src/Control/Eff/Fresh.hs
+++ b/src/Control/Eff/Fresh.hs
@@ -9,17 +9,18 @@
 {-# LANGUAGE Safe #-}
 -- | Create unique Enumerable values.
 module Control.Eff.Fresh( Fresh (Fresh)
+                        , withFresh
                         , fresh
                         , runFresh'
                         ) where
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
 
 -- There are three possible implementations
 -- The first one uses State Fresh where
@@ -35,14 +36,24 @@
   Fresh :: Fresh Int
   Replace :: !Int -> Fresh ()
 
+-- | Embed a pure value. Note that this is a specialized form of
+-- State's and we could have reused it.
+withFresh :: Monad m => a -> Int -> m (a, Int)
+withFresh x s = return (x, s)
+
+-- | Given a continuation and requests, respond to them
+instance Handle Fresh r a (Int -> k) where
+  handle step q req s = case req of
+    Fresh     -> step (q ^$ s) (s+1)
+    Replace i -> step (q ^$ ()) i
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (Fresh ': r)) where
     type StM (Eff (Fresh ': r)) a = StM (Eff r) (a, Int)
     liftBaseWith f = do i <- fresh
                         raise $ liftBaseWith $ \runInBase ->
-                          f (\k -> runInBase $ runFreshReturn k i)
+                          f (\k -> runInBase $ runFreshReturn i k)
     restoreM x = do (r,i) <- raise (restoreM x)
                     replace i
                     return r
@@ -56,16 +67,12 @@
 replace = send . Replace
 
 -- | Run an effect requiring unique values.
-runFresh' :: Eff (Fresh ': r) w -> Int -> Eff r w
-runFresh' m s = fst `fmap` runFreshReturn m s
+runFresh' :: Int -> Eff (Fresh ': r) w -> Eff r w
+runFresh' s m = fst `fmap` runFreshReturn s m
 
-runFreshReturn :: Eff (Fresh ': r) w -> Int -> Eff r (w,Int)
-runFreshReturn m s =
-  handle_relay_s s (\s' x -> return (x,s'))
-                   (\s' e k -> case e of
-                                 Fresh -> (k $! s' + 1) s'
-                                 Replace i -> k i ())
-                   m
+runFreshReturn :: Int -> Eff (Fresh ': r) w -> Eff r (w,Int)
+runFreshReturn s m = fix (handle_relay withFresh) m s
+
 {-
 -- Finally, the worst implementation but the one that answers
 -- reviewer's question: implementing Fresh in terms of State
diff --git a/src/Control/Eff/Internal.hs b/src/Control/Eff/Internal.hs
--- a/src/Control/Eff/Internal.hs
+++ b/src/Control/Eff/Internal.hs
@@ -7,8 +7,10 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
-
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE LambdaCase #-}
 
 -- ------------------------------------------------------------------------
 -- | A monadic library for communication between a handler and
@@ -24,27 +26,26 @@
 -- effects, consult the tests.
 module Control.Eff.Internal where
 
-#if __GLASGOW_HASKELL__ < 710
-import Control.Applicative
-#endif
 import qualified Control.Arrow as A
 import qualified Control.Category as C
 import Control.Monad.Base (MonadBase(..))
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.Trans.Control (MonadBaseControl(..))
+import qualified Control.Exception as Exc
 import safe Data.OpenUnion
 import safe Data.FTCQueue
 import GHC.Exts (inline)
+import Data.Function (fix)
 
 -- | Effectful arrow type: a function from a to b that also does effects
 -- denoted by r
 type Arr r a b = a -> Eff r b
 
--- | An effectful function from 'a' to 'b' that is a composition of one or more
+-- | An effectful function from @a@ to @b@ that is a composition of one or more
 -- effectful functions. The paremeter r describes the overall effect.
 --
--- The composition members are accumulated in a type-aligned queue.
--- Using a newtype here enables us to define `Category' and `Arrow' instances.
+-- The composition members are accumulated in a type-aligned queue. Using a
+-- newtype here enables us to define `C.Category' and `A.Arrow' instances.
 newtype Arrs r a b = Arrs (FTCQueue (Eff r) a b)
 
 -- | 'Arrs' can be composed and have a natural identity.
@@ -52,7 +53,7 @@
   id = ident
   f . g = comp g f
 
--- | As the name suggests, 'Arrs' also has an 'Arrow' instance.
+-- | As the name suggests, 'Arrs' also has an 'A.Arrow' instance.
 instance A.Arrow (Arrs r) where
   arr = arr
   first = singleK . first . (^$)
@@ -62,20 +63,23 @@
 
 -- | convert single effectful arrow into composable type. i.e., convert 'Arr' to
 -- 'Arrs'
-{-# INLINE singleK #-}
+{-# INLINE [2] singleK #-}
 singleK :: Arr r a b -> Arrs r a b
-singleK = Arrs . tsingleton
+singleK k = Arrs (tsingleton k)
+{-# RULES
+"singleK/qApp" [~2] forall q. singleK (qApp q) = q
+ #-}
 
--- | Application to the `generalized effectful function' Arrs r b w, i.e.,
+-- | Application to the `generalized effectful function' @Arrs r b w@, i.e.,
 -- convert 'Arrs' to 'Arr'
-{-# INLINABLE qApp #-}
+{-# INLINABLE [2] qApp #-}
 qApp :: forall r b w. Arrs r b w -> Arr r b w
 qApp (Arrs q) x = viewlMap (inline tviewl q) ($ x) cons
   where
     cons :: forall x. Arr r b x -> FTCQueue (Eff r) x w -> Eff r w
     cons = \k t -> case k x of
       Val y -> qApp (Arrs t) y
-      E u (Arrs q0) -> E u (Arrs (q0 >< t))
+      E (Arrs q0) u -> E (Arrs (q0 >< t)) u
 {-
 -- A bit more understandable version
 qApp :: Arrs r b w -> b -> Eff r w
@@ -89,8 +93,8 @@
 -}
 
 -- | Syntactic sugar for 'qApp'
-{-# INLINABLE (^$) #-}
-(^$) :: forall r b w. Arrs r b w -> Arr r b w
+{-# INLINE [2] (^$) #-}
+(^$) :: forall r b w. Arrs r b w -> b -> Eff r w
 q ^$ x = q `qApp` x
 
 -- | Lift a function to an arrow
@@ -102,6 +106,7 @@
 ident = arr id
 
 -- | Arrow composition
+{-# INLINE comp #-}
 comp :: Arrs r a b -> Arrs r b c -> Arrs r a c
 comp (Arrs f) (Arrs g) = Arrs (f >< g)
 
@@ -109,162 +114,269 @@
 (^|>) :: Arrs r a b -> Arr r b c -> Arrs r a c
 (Arrs f) ^|> g = Arrs (f |> g)
 
--- | The Eff monad (not a transformer!). It is a fairly standard coroutine monad
--- where the type @r@ is the type of effects that can be handled, and the
--- missing type @a@ (from the type application) is the type of value that is
--- returned.  It is NOT a Free monad! There are no Functor constraints.
+-- | The monad that all effects in this library are based on.
 --
--- The two constructors denote the status of a coroutine (client): done with the
--- value of type a, or sending a request of type Union r with the continuation
--- Arrs r b a. Expressed another way: an `Eff` can either be a value (i.e.,
--- 'Val' case), or an effect of type @`Union` r@ producing another `Eff` (i.e.,
--- 'E' case). The result is that an `Eff` can produce an arbitrarily long chain
--- of @`Union` r@ effects, terminated with a pure value.
+-- An effectful computation is a value of type `Eff r a`.
+-- In this signature, @r@ is a type-level list of effects that are being
+-- requested and need to be handled inside an effectful computation.
+-- @a@ is the computation's result similar to other monads.
 --
--- Potentially, inline Union into E
+-- A computation's result can be retrieved via the 'run' function.
+-- However, all effects used in the computation need to be handled by the use
+-- of the effects' @run*@ functions before unwrapping the final result.
+-- For additional details, see the documentation of the effects you are using.
 data Eff r a = Val a
-             | forall b. E  (Union r b) (Arrs r b a)
+             | forall b. E (Arrs r b a) (Union r b)
+-- | Case analysis for 'Eff' datatype. If the value is @'Val' a@ apply
+-- the first function to @a@; if it is @'E' u q@, apply the second
+-- function.
+{-# INLINE eff #-}
+eff :: (a -> b)
+    -> (forall v. Arrs r v a -> Union r v -> b)
+    -> Eff r a -> b
+eff f _ (Val a) = f a
+eff _ g (E q u) = g q u
 
+-- | The usual 'bind' fnuction with arguments flipped. This is a
+-- common pattern for Eff.
+{-# INLINE bind #-}
+bind :: Arr r a b -> Eff r a -> Eff r b
+bind k e = eff k (E . (^|> k)) e       -- just accumulates continuations
+
 -- | Compose effectful arrows (and possibly change the effect!)
 {-# INLINE qComp #-}
-qComp :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arr r' a c
+qComp :: Arrs r a b -> (Eff r b -> k) -> (a -> k)
 -- qComp g h = (h . (g `qApp`))
-qComp g h = \a -> h $ (g ^$ a)
+qComp g h = \a -> h (g ^$ a)
 
 -- | Compose effectful arrows (and possibly change the effect!)
 {-# INLINE qComps #-}
 qComps :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arrs r' a c
 qComps g h = singleK $ qComp g h
 
--- | Eff is still a monad and a functor (and Applicative)
--- (despite the lack of the Functor constraint)
 instance Functor (Eff r) where
   {-# INLINE fmap #-}
-  fmap f (Val x) = Val (f x)
-  fmap f (E u q) = E u (q ^|> (Val . f)) -- does no mapping yet!
+  fmap f x = bind (Val . f) x
 
 instance Applicative (Eff r) where
   {-# INLINE pure #-}
   pure = Val
-  Val f <*> e = f `fmap` e
-  E u q <*> e = E u (q ^|> (`fmap` e))
+  mf <*> e = bind (`fmap` e) mf
 
 instance Monad (Eff r) where
   {-# INLINE return #-}
   {-# INLINE [2] (>>=) #-}
   return = pure
-  Val x >>= k = k x
-  E u q >>= k = E u (q ^|> k)          -- just accumulates continuations
+  m >>= f = bind f m
 {-
   Val _ >> m = m
-  E u q >> m = E u (q ^|> const m)
+  E q u >> m = E (q ^|> const m) u
 -}
 
-instance (MonadBase b m, SetMember Lift (Lift m) r) => MonadBase b (Eff r) where
-    liftBase = lift . liftBase
-    {-# INLINE liftBase #-}
-
-instance (MonadBase m m)  => MonadBaseControl m (Eff '[Lift m]) where
-    type StM (Eff '[Lift m]) a = a
-    liftBaseWith f = lift (f runLift)
-    {-# INLINE liftBaseWith #-}
-    restoreM = return
-    {-# INLINE restoreM #-}
-
-instance (MonadIO m, SetMember Lift (Lift m) r) => MonadIO (Eff r) where
-    liftIO = lift . liftIO
-    {-# INLINE liftIO #-}
-
 -- | Send a request and wait for a reply (resulting in an effectful
 -- computation).
 {-# INLINE [2] send #-}
 send :: Member t r => t v -> Eff r v
-send t = E (inj t) (singleK Val)
+send t = E (singleK Val) (inj t)
 -- This seems to be a very beneficial rule! On micro-benchmarks, cuts
 -- the needed memory in half and speeds up almost twice.
 {-# RULES
-  "send/bind" [~3] forall t k. send t >>= k = E (inj t) (singleK k)
+  "send/bind" [~3] forall t k. send t >>= k = E (singleK k) (inj t)
  #-}
 
 
 -- ------------------------------------------------------------------------
--- | Get the result from a pure (i.e. no effects) computation.
+-- | Get the result from a pure computation
 --
--- The type of run ensures that all effects must be handled:
--- only pure computations can be run.
+-- A pure computation has type @Eff '[] a@. The empty effect-list indicates that
+-- no further effects need to be handled.
 run :: Eff '[] w -> w
 run (Val x) = x
--- | the other case is unreachable since Union [] a cannot be
--- constructed.
--- Therefore, run is a total function if its argument terminates.
-run (E _ _) = error "extensible-effects: the impossible happened!"
+-- | @Union []@ has no nonbottom values.
+-- Due to laziness it is possible to get into this branch but its union argument
+-- cannot terminate.
+-- To extract the true error, the evaluation of union is forced.
+-- 'run' is a total function if its argument is different from bottom.
+run (E _ union) =
+  union `seq` error "extensible-effects: the impossible happened!"
 
--- | A convenient pattern: given a request (open union), either
--- handle it or relay it.
-{-# INLINE handle_relay #-}
-handle_relay :: (a -> Eff r w) ->
-                (forall v. t v -> Arr r v w -> Eff r w) ->
-                Eff (t ': r) a -> Eff r w
-handle_relay ret h m = loop m
- where
-  loop (Val x)  = ret x
-  loop (E u q)  = case decomp u of
-    Right x -> h x k
-    Left  u0 -> E u0 (singleK k)
-   where k = qComp q loop
+-- | Abstract the recursive 'relay' pattern, i.e., "somebody else's problem".
+class Relay k r where
+  relay :: (v -> k) -> Union r v -> k
+instance Relay (Eff r w) r where
+  {-# INLINABLE relay #-}
+  relay q u = E (singleK q) u
+instance Relay k r => Relay (s -> k) r where
+  {-# INLINABLE relay #-}
+  relay q u s = relay (\x -> q x s) u
 
--- | Parameterized handle_relay
-{-# INLINE handle_relay_s #-}
-handle_relay_s :: s ->
-                (s -> a -> Eff r w) ->
-                (forall v. s -> t v -> (s -> Arr r v w) -> Eff r w) ->
-                Eff (t ': r) a -> Eff r w
-handle_relay_s s ret h m = loop s m
-  where
-    loop s0 (Val x)  = ret s0 x
-    loop s0 (E u q)  = case decomp u of
-      Right x -> h s0 x k
-      Left  u0 -> E u0 (singleK (k s0))
-     where k s1 x = loop s1 $ qApp q x
+-- | Respond to requests of type @t@. The handlers themselves are expressed in
+-- open-recursion style.
+class Handle t r a k where
+  handle :: (Eff r a -> k) -- ^ untied recursive knot
+         -> Arrs r v a -- ^ coroutine awaiting response
+         -> t v -- ^ request
+         -> k
 
--- | Add something like Control.Exception.catches? It could be useful
--- for control with cut.
---
--- Intercept the request and possibly reply to it, but leave it unhandled
--- (that's why we use the same r all throuout)
-{-# INLINE interpose #-}
-interpose :: Member t r =>
-             (a -> Eff r w) -> (forall v. t v -> Arr r v w -> Eff r w) ->
-             Eff r a -> Eff r w
-interpose ret h m = loop m
- where
-   loop (Val x)  = ret x
-   loop (E u q)  = case prj u of
-     Just x -> h x k
-     _      -> E u (singleK k)
-    where k = qComp q loop
+  -- | A convenient pattern: given a request (in an open union), either handle
+  -- it (using default Handler) or relay it.
+  --
+  -- "Handle" implies that all requests of type @t@ are dealt with, i.e., @k@
+  -- (the response type) doesn't have @t@ as part of its effect list. The @Relay
+  -- k r@ constraint ensures that @k@ is an effectful computation (with
+  -- effectlist @r@).
+  --
+  -- Note that we can only handle the leftmost effect type (a consequence of the
+  -- 'Data.OpenUnion' implementation.
+  handle_relay :: r ~ (t ': r') => Relay k r'
+               => (a -> k) -- ^ return
+               -> (Eff r a -> k) -- ^ untied recursive knot
+               -> Eff r a -> k
+  handle_relay ret step m = eff ret
+                            (\q u -> case u of
+                                U0 x -> handle step q x
+                                U1 u' -> relay (qComp q step) u')
+                            m
+  -- | Intercept the request and possibly respond to it, but leave it
+  -- unhandled. The @Relay k r@ constraint ensures that @k@ is an effectful
+  -- computation (with effectlist @r@). As such, the effect type @t@ will show
+  -- up in the response type @k@. There are two natural / commmon options for
+  -- @k@: the implicit effect domain (i.e., Eff r (f a)), or the explicit effect
+  -- domain (i.e., s1 -> s2 -> ... -> sn -> Eff r (f a s1 s2 ... sn)).
+  --
+  -- There are three different ways in which we may want to alter behaviour:
+  --
+  -- 1. __Before__: This work should be done before 'respond_relay' is called.
+  --
+  -- 2. __During__: This work should be done by altering the handler being
+  -- passed to 'respond_relay'. This allows us to modify the requests "in
+  -- flight".
+  --
+  -- 3. __After__: This work should be done be altering the @ret@ being passed
+  -- to 'respond_relay'. This allows us to overwrite changes or discard them
+  -- altogether. If this seems magical, note that we have the flexibility of
+  -- altering the target domain @k@. Specifically, the explicit domain
+  -- representation gives us access to the "effect" realm allowing us to
+  -- manipulate it directly.
+  respond_relay :: Member t r => Relay k r
+                => (a -> k) -- ^ return
+                -> (Eff r a -> k) -- ^ untied recursive knot
+                -> Eff r a -> k
+  respond_relay ret step m = eff ret
+                             (\q u -> case u of
+                                 U0' x -> handle @t step q x
+                                 _     -> relay (qComp q step) u)
+                             m
 
+-- | A less commonly needed variant with an explicit handler (instead
+-- of @Handle t r a k@ constraint).
+{-# INLINE handle_relay' #-}
+handle_relay' :: r ~ (t ': r') => Relay k r'
+              => (forall v. (Eff r a -> k) -> Arrs r v a -> t v -> k) -- ^ handler
+              -> (a -> k) -- ^ return
+              -> (Eff r a -> k) -- ^ untied recursive knot
+              -> Eff r a -> k
+handle_relay' hdl ret step m = eff ret
+                                    (\q u -> case u of
+                                        U0 x -> hdl step q x
+                                        U1 u' -> relay (qComp q step) u')
+                                    m
+
+-- | Variant with an explicit handler (instead of @Handle t r a k@
+-- constraint).
+{-# INLINE respond_relay' #-}
+respond_relay' :: Member t r => Relay k r
+               => (forall v. (Eff r a -> k) -> Arrs r v a -> t v -> k) -- ^ handler
+               -> (a -> k) -- ^ return
+               -> (Eff r a -> k) -- ^ recursive knot
+               -> Eff r a -> k
+respond_relay' hdl ret step m = eff ret
+                                (\q u -> case u of
+                                    U0' x -> hdl step q x
+                                    _     -> relay (qComp q step) u)
+                                m
+
 -- | Embeds a less-constrained 'Eff' into a more-constrained one. Analogous to
 -- MTL's 'lift'.
 raise :: Eff r a -> Eff (e ': r) a
-raise = loop
-  where
-    loop (Val x) = pure x
-    loop (E u q) = E (weaken u) $ qComps q loop
+raise (Val x) = pure x
+raise (E q u) = E k (U1 u)
+  where k = qComps q raise
 {-# INLINE raise #-}
 
 -- ------------------------------------------------------------------------
 -- | Lifting: emulating monad transformers
-newtype Lift m a = Lift (m a)
+newtype Lift m a = Lift { unLift :: m a }
 
--- | We make the Lift layer to be unique, using SetMember
-lift :: (SetMember Lift (Lift m) r) => m a -> Eff r a
+-- |A convenient alias to @SetMember Lift (Lift m) r@, which allows us
+-- to assert that the lifted type occurs ony once in the effect list.
+type Lifted m r = SetMember Lift (Lift m) r
+
+-- |Same as 'Lifted' but with additional 'MonadBaseControl' constraint
+type LiftedBase m r = ( SetMember Lift (Lift m) r
+                      , MonadBaseControl m (Eff r)
+                      )
+
+-- | embed an operation of type `m a` into the `Eff` monad when @Lift m@ is in
+-- a part of the effect-list.
+lift :: Lifted m r => m a -> Eff r a
 lift = send . Lift
 
--- | The handler of Lift requests. It is meant to be terminal:
--- we only allow a single Lifted Monad.
+-- | Handle lifted requests by running them sequentially
+instance Monad m => Handle (Lift m) r a (m k) where
+  handle step q (Lift x) = x >>= (step . (q ^$))
+
+-- | The handler of Lift requests. It is meant to be terminal: we only
+-- allow a single Lifted Monad. Note, too, how this is different from
+-- other handlers.
 runLift :: Monad m => Eff '[Lift m] w -> m w
-runLift (Val x) = return x
-runLift (E u q) = case prj u of
-                  Just (Lift m) -> m >>= runLift . qApp q
-                  Nothing -> error "Impossible: Nothing cannot occur"
+runLift m = fix step m
+  where
+    step :: Monad m => (Eff '[Lift m] w -> m w) -> Eff '[Lift m] w -> m w
+    step next m' = eff return
+                   (\q u -> case u of
+                       U0' x -> handle next q x
+                       _     -> error "Impossible: Nothing to relay!")
+                   m'
+
+-- | Catching of dynamic exceptions
+-- See the problem in
+-- http://okmij.org/ftp/Haskell/misc.html#catch-MonadIO
+catchDynE :: forall e a r.
+             (Lifted IO r, Exc.Exception e) =>
+             Eff r a -> (e -> Eff r a) -> Eff r a
+catchDynE m eh = fix (respond_relay' h return) m
+ where
+   -- Polymorphic local binding: signature is needed
+   h :: (Eff r a -> Eff r a) -> Arrs r v a -> Lift IO v -> Eff r a
+   h step q (Lift em) = lift (Exc.try em) >>= either eh k
+     where k = step . (q ^$)
+
+-- | You need this when using 'catchesDynE'.
+data HandlerDynE r a =
+  forall e. (Exc.Exception e, Lifted IO r) => HandlerDynE (e -> Eff r a)
+
+-- | Catch multiple dynamic exceptions. The implementation follows
+-- that in Control.Exception almost exactly. Not yet tested.
+-- Could this be useful for control with cut?
+catchesDynE :: Lifted IO r => Eff r a -> [HandlerDynE r a] -> Eff r a
+catchesDynE m hs = m `catchDynE` catchesHandler hs where
+  catchesHandler :: Lifted IO r => [HandlerDynE r a] -> Exc.SomeException -> Eff r a
+  catchesHandler handlers e = foldr tryHandler (lift . Exc.throw $ e) handlers
+    where
+      tryHandler (HandlerDynE h) res = maybe res h (Exc.fromException e)
+
+instance (MonadBase b m, Lifted m r) => MonadBase b (Eff r) where
+    liftBase = lift . liftBase
+    {-# INLINE liftBase #-}
+
+instance (MonadBase m m)  => MonadBaseControl m (Eff '[Lift m]) where
+    type StM (Eff '[Lift m]) a = a
+    liftBaseWith f = lift (f runLift)
+    {-# INLINE liftBaseWith #-}
+    restoreM = return
+    {-# INLINE restoreM #-}
+
+instance (MonadIO m, Lifted m r) => MonadIO (Eff r) where
+    liftIO = lift . liftIO
+    {-# INLINE liftIO #-}
diff --git a/src/Control/Eff/Lift.hs b/src/Control/Eff/Lift.hs
deleted file mode 100644
--- a/src/Control/Eff/Lift.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE Safe #-}
--- | Lifting primitive Monad types to effectful computations.
--- We only allow a single Lifted Monad because Monads aren't commutative
--- (e.g. Maybe (IO a) is functionally distinct from IO (Maybe a)).
-module Control.Eff.Lift ( Lift (..)
-                        , Lifted
-                        , LiftedBase
-                        , lift
-                        , runLift
-                        , catchDynE
-                        ) where
-
-import Control.Eff.Internal
-import qualified Control.Exception as Exc
-import Data.OpenUnion
-
-import Control.Monad.Trans.Control (MonadBaseControl)
-
--- |A convenient alias to 'SetMember Lift (Lift m) r'
-type Lifted m r = SetMember Lift (Lift m) r
-
--- |Same as 'Lifted' but with additional 'MonadBaseControl' constraint
-type LiftedBase m r = ( SetMember Lift (Lift m) r
-                      , MonadBaseControl m (Eff r)
-                      )
-
--- | Catching of dynamic exceptions
--- See the problem in
--- http://okmij.org/ftp/Haskell/misc.html#catch-MonadIO
-catchDynE :: forall e a r.
-             (Lifted IO r, Exc.Exception e) =>
-             Eff r a -> (e -> Eff r a) -> Eff r a
-catchDynE m eh = interpose return h m
- where
-   -- Polymorphic local binding: signature is needed
-   h :: Lift IO v -> Arr r v a -> Eff r a
-   h (Lift em) k = lift (Exc.try em) >>= \x -> case x of
-         Right x0 -> k x0
-         Left  e -> eh e
diff --git a/src/Control/Eff/Logic/Core.hs b/src/Control/Eff/Logic/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Eff/Logic/Core.hs
@@ -0,0 +1,174 @@
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE LambdaCase #-}
+
+-- | Logic primitives. See @LogicT@ paper for details.
+--
+-- * [@LogicT@] [LogicT - backtracking monad transformer with fair operations and pruning](http://okmij.org/ftp/Computation/monads.html#LogicT)
+module Control.Eff.Logic.Core where
+
+import Control.Monad
+
+import Control.Eff
+import Control.Eff.Exception
+
+import Data.Function (fix)
+
+-- | The MSplit primitive from LogicT paper.
+class MSplit m where
+  -- | The laws for 'msplit' are:
+  --
+  -- > msplit mzero                = return Nothing
+  -- > msplit (return a `mplus` m) = return (Just(a, m))
+  msplit :: m a -> m (Maybe (a, m a))
+
+-- | Embed a pure value into MSplit
+{-# INLINE withMSplit #-}
+withMSplit :: MonadPlus m => a -> m a -> m (Maybe (a, m a))
+withMSplit a rest = return (Just (a, rest))
+-- The handlers are defined in terms of the specific non-determinism
+-- effects (instead of by way of a distinct MSplit handler
+
+-- | Laws for 'reflect':
+--
+-- > msplit (lift m >> mzero)   >>= reflect = lift m >> mzero
+-- > msplit (lift m `mplus` ma) >>= reflect = lift m `mplus` (msplit ma >>= reflect)
+{-# INLINE reflect #-}
+reflect :: MonadPlus m => Maybe (a, m a) -> m a
+reflect Nothing      = mzero
+reflect (Just (a,m)) = return a `mplus` m
+
+-- Other committed choice primitives can be implemented in terms of msplit
+-- The following implementations are directly from the LogicT paper
+
+-- | Soft-cut: non-deterministic if-then-else, aka Prolog's @*->@
+-- Declaratively,
+--
+-- >  ifte t th el = (t >>= th) `mplus` ((not t) >> el)
+--
+-- However, @t@ is evaluated only once. In other words, @ifte t th el@
+-- is equivalent to @t >>= th@ if @t@ has at least one solution.
+-- If @t@ fails, @ifte t th el@ is the same as @el@. Laws:
+--
+-- > ifte (return a) th el           = th a
+-- > ifte mzero th el                = el
+-- > ifte (return a `mplus` m) th el = th a `mplus` (m >>= th)
+ifte :: (MonadPlus m, MSplit m)
+     => m t -> (t -> m b) -> m b -> m b
+ifte t th el = msplit t >>= check
+ where check Nothing          = el
+       check (Just (sg1,sg2)) = (th sg1) `mplus` (sg2 >>= th)
+
+-- | Another pruning operation (ifte is the other). This selects one
+-- solution out of possibly many.
+once :: (MSplit m, MonadPlus m) => m b -> m b
+once m = msplit m >>= check
+ where check Nothing        = mzero
+       check (Just (sg1,_)) = return sg1
+
+-- | Negation as failure
+gnot :: (MonadPlus m, MSplit m) => m b -> m ()
+gnot m = ifte (once m) (const mzero) (return ())
+
+-- | Fair (i.e., avoids starvation) disjunction. It obeys the
+-- following laws:
+--
+-- > interleave mzero m                  = m
+-- > interleave (return a `mplus` m1) m2 = return a `mplus` (interleave m2 m1)
+--
+-- corollary:
+--
+-- > interleave m mzero = m
+interleave :: (MSplit m, MonadPlus m) => m b -> m b -> m b
+interleave sg1 sg2 =
+  do r <- msplit sg1
+     case r of
+       Nothing -> sg2
+       Just (sg11,sg12) ->
+         (return sg11) `mplus` (interleave sg2 sg12)
+
+-- | Fair (i.e., avoids starvation) conjunction. It obeys the
+-- following laws:
+--
+-- > mzero                >>- k = mzero
+-- > (return a `mplus` m) >>- k = interleave (k a) (m >>- k)
+(>>-) :: (MonadPlus m, MSplit m) => m a -> (a -> m b) -> m b
+sg >>- g =
+  do r <- msplit sg
+     case r of
+       Nothing -> mzero
+       Just (sg1 ,sg2) -> interleave (g sg1) (sg2 >>- g)
+
+-- | Collect all solutions. This is from Hinze's @Backtr@ monad
+-- class. Unsurprisingly, this can be implemented in terms of msplit.
+sols :: (Monad m, MSplit m) => m a -> m [a]
+sols m = (msplit m) >>= (fix step) [] where
+  step _ jq Nothing          = return jq
+  step next jq (Just(a, ma)) = (msplit ma) >>= next (a:jq)
+
+-- | Non-determinism with control (@cut@).
+--
+-- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper:
+--
+-- * [@Backtr@] [Deriving Backtracking Monad Transformers](https://dl.acm.org/citation.cfm?id=351240.351258)
+--
+-- Hinze suggests expressing @cut@ in terms of @cutfalse@:
+--
+-- > = return () `mplus` cutfalse
+-- > where
+-- >  cutfalse :: m a
+--
+-- satisfies the following laws:
+--
+-- >  cutfalse >>= k  = cutfalse              (F1)
+-- >  cutfalse | m    = cutfalse              (F2)
+--
+-- (note: @m \``mplus`\` cutfalse@ is different from @cutfalse \``mplus`\` m@).
+-- In other words, cutfalse is the left zero of both bind and mplus.
+--
+-- Hinze also introduces the operation @`call` :: m a -> m a@ that
+-- delimits the effect of cut: @`call` m@ executes m. If the cut is
+-- invoked in m, it discards only the choices made since m was called.
+-- Hinze postulates the axioms of `call`:
+--
+-- >  call false = false                          (C1)
+-- >  call (return a | m) = return a | call m     (C2)
+-- >  call (m | cutfalse) = call m                (C3)
+-- >  call (lift m >>= k) = lift m >>= (call . k) (C4)
+--
+-- @`call` m@ behaves like @m@ except any cut inside @m@ has only a local effect,
+-- he says.
+--
+-- Hinze noted a problem with the \"mechanical\" derivation of backtracing
+-- monad transformer with cut: no axiom specifying the interaction of
+-- call with bind; no way to simplify nested invocations of call.
+class Call r where
+  -- | Mapping @Backtr@ interface to 'MonadPlus' and using exceptions for
+  -- @cutfalse@, every instance should ensure that the following laws hold:
+  --
+  -- >  cutfalse `mplus` m        = cutfalse                --(F2)
+  -- >  call mzero                = mzero                   --(C1)
+  -- >  call (return a `mplus` m) = return a `mplus` call m --(C2)
+  -- >  call (m `mplus` cutfalse) = call m                  --(C3)
+  -- >  call (lift m >>= k)       = lift m >>= (call . k)   --(C4)
+  call :: MonadPlus (Eff r) => Eff (Exc CutFalse : r) a -> Eff r a
+
+data CutFalse = CutFalse
+
+-- | We use exceptions for cutfalse
+-- Therefore, the law @cutfalse >>= k = cutfalse@
+-- is satisfied automatically since all exceptions have the above property.
+cutfalse :: Member (Exc CutFalse) r => Eff r a
+cutfalse = throwError CutFalse
+
+-- | Prolog @cut@, taken from Hinze 2000 (Deriving backtracking monad
+-- transformers).
+(!) :: (Member (Exc CutFalse) r, MonadPlus (Eff r)) => Eff r ()
+(!) = return () `mplus` cutfalse
+
+-- | Case analysis for lists
+{-# INLINE list #-}
+list :: b -> (a -> [a] -> b)
+     -> [a] -> b
+list z _ [] = z
+list _ k (h:t) = k h t
diff --git a/src/Control/Eff/Logic/Experimental.hs b/src/Control/Eff/Logic/Experimental.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Eff/Logic/Experimental.hs
@@ -0,0 +1,36 @@
+{-# OPTIONS_HADDOCK hide #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module is for some experimental implementations and tinkering. Not
+-- intended to be exposed or depended on.
+module Control.Eff.Logic.Experimental where
+
+import Control.Eff
+import Control.Eff.Extend
+import Control.Eff.Exception
+import Control.Eff.Logic.Core
+import Control.Monad
+
+instance (MonadPlus (Eff (Exc CutFalse : r)), MSplit (Eff (Exc CutFalse : r)))
+  => Call r where
+  call m = loop m [] where
+    loop m' jq = case msplit m' of
+      Val Nothing       -> next jq                        -- (C1)
+      Val (Just (x, q)) -> return x `mplus` next (q : jq) -- (C2)
+      E q u -> case u of
+        U0 (Exc CutFalse) -> next []                      -- drop jq (F2)
+        U1 _              -> loop (E q u >>= reflect) jq  -- (C4?)
+        --_                 -> loop m' jq
+    next jq = list mzero loop jq                          -- (C3?)
+  {-
+  call m = loop (msplit m) [] where
+    loop (Val Nothing) jq       = next jq                        -- (C1)
+    loop (Val (Just (x, q))) jq = return x `mplus` next (q : jq) -- (C2)
+    loop (E q u) jq             = case u of
+      U0 (Exc CutFalse)        -> next []                        -- drop jq (F2)
+      _                        -> loop (E q u) jq          -- (C4?)
+
+    next []    = mzero
+    next (h:t) = loop (msplit h) t                               -- (C3?)
+  -}
diff --git a/src/Control/Eff/Logic/NDet.hs b/src/Control/Eff/Logic/NDet.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Eff/Logic/NDet.hs
@@ -0,0 +1,229 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE Safe #-}
+-- The following is needed to define MonadPlus instance. It is decidable
+-- (there is no recursion!), but GHC cannot see that.
+{-# LANGUAGE UndecidableInstances #-}
+-- The following is needed for pattern-synonym bug in ghc 8.2
+{-# LANGUAGE CPP #-}
+
+-- | Nondeterministic choice effect via MPlus interface directly. In order to
+-- get an understanding of what nondeterministic choice entails the following
+-- papers are recommended:
+--
+-- * [@LogicT@] [LogicT - backtracking monad transformer with fair operations and pruning](http://okmij.org/ftp/Computation/monads.html#LogicT)
+-- * [@Backtr@] [Deriving Backtracking Monad Transformers](https://dl.acm.org/citation.cfm?id=351240.351258)
+--
+-- __TODO__: investigate Fusion regd msplit and associated functions.
+module Control.Eff.Logic.NDet (
+  -- * Main interface
+  NDet
+  , withNDet
+  , left, right
+  , choose
+  , makeChoice
+  , makeChoiceA
+  , module Control.Eff.Logic.Core
+    -- * Additional functions for comparison
+  , msplit'
+  , msplit'_manual
+  , makeChoiceA_manual
+  , makeChoiceA0
+  ) where
+
+import Control.Eff
+import Control.Eff.Extend
+import Control.Eff.Logic.Core
+import Control.Eff.Exception
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Base
+import Control.Monad.Trans.Control
+import Data.Function (fix)
+
+-- | An implementation of non-deterministic choice aka backtracking. The two
+-- requests we need to support are: @false@, @(|)@. We map this to the
+-- 'MonadPlus' (or 'Alternative') interface: @MZero@ stands for @false@, and
+-- @MPlus@ stands for @(|)@.
+--
+-- This creates a branching structure with a fanout of @2@, resulting in @mplus@
+-- node being visited approximately @2x@ (in general, for a fanout of @f@ we'll
+-- have the type of internal node being invoked @f/(f-1)@ times).
+data NDet a where
+  MZero :: NDet a
+  MPlus :: NDet Bool
+
+-- | How to embed a pure value in non-deterministic context
+{-# INLINE withNDet #-}
+withNDet :: Alternative f => Monad m => a -> m (f a)
+withNDet x = return (pure x)
+-- | The left branch
+{-# INLINE left #-}
+left :: Arrs r Bool a -> Eff r a
+left q = q ^$ True
+-- | The right branch
+{-# INLINE right #-}
+right :: Arrs r Bool a -> Eff r a
+right q = q ^$ False
+-- | Given a callback and 'NDet' requests respond to them. Note that this makes
+-- explicit that we rely on @f@ to have enough room to store all possibilities.
+instance Alternative f => Handle NDet r a (Eff r' (f w)) where
+  handle _ _ MZero = return empty
+  handle step q MPlus = liftM2 (<|>) (step $ left q) (step $ right q)
+
+instance Member NDet r => Alternative (Eff r) where
+  empty = mzero
+  (<|>) = mplus
+
+-- | Mapping of 'NDet' requests to 'MonadPlus'. We obey the following laws
+-- (taken from the @Backtr@ and @LogicT papers):
+--
+-- > mzero >>= f = mzero                               -- (L1)
+-- > mzero `mplus` m = m                               -- (L2)
+-- > m `mplus` mzero = m                               -- (L3)
+-- > m `mplus` (n `mplus` o) = (m `mplus` n) `mplus` o -- (L4)
+-- > (m `mplus` n) >>= k = (m >>= k) `mplus` (n >>= k) -- (L5)
+--
+-- - @L1@ is the left-zero law for 'mzero'
+-- - @L2, L3, L4@ are the @Monoid@ laws
+--
+-- __NOTE__ that we do __not__ obey the right-zero law for
+-- 'mzero'. Specifically, we do __not__ obey:
+--
+-- > m >> mzero  = mzero
+instance Member NDet r => MonadPlus (Eff r) where
+  mzero = send MZero
+  -- | Applying L2 and L3
+#if __GLASGOW_HASKELL__ < 804
+  mplus (E _ u) m2 | Just MZero <- prj u = m2
+  mplus m1 (E _ u) | Just MZero <- prj u = m1
+#else
+  mplus (E _ (U0' MZero)) m2 = m2
+  mplus m1 (E _ (U0' MZero)) = m1
+#endif
+  mplus m1 m2 = send MPlus >>= \x -> if x then m1 else m2
+
+instance ( MonadBase m m
+         , LiftedBase m r
+         ) => MonadBaseControl m (Eff (NDet ': r)) where
+    type StM (Eff (NDet ': r)) a = StM (Eff r) [a]
+    liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
+                       f (runInBase . makeChoice)
+    restoreM x = do lst :: [a] <- raise (restoreM x)
+                    choose lst
+
+-- | @'choose' lst@ non-deterministically chooses one value from the
+-- @lst@. @'choose' []@ thus corresponds to failure.
+choose :: Member NDet r => [a] -> Eff r a
+choose lst = msum $ map return lst
+
+-- | An interpreter: The following is very simple, but leaks a lot of memory The
+-- cause probably is mapping every failure to empty It takes then a lot of timne
+-- and space to store those empty. When there aren't a lot of failures, this is
+-- comparable to 'makeChoiceA'.
+makeChoiceA0 :: Alternative f => Eff (NDet ': r) a -> Eff r (f a)
+makeChoiceA0 = fix (handle_relay withNDet)
+
+-- | More performant handler; uses reified job queue
+instance Alternative f => Handle NDet r a ([Eff r a] -> Eff r' (f w)) where
+  handle step _ MZero jq = next step jq
+  handle step q MPlus jq = next step (left q : right q : jq)
+-- instance Handle NDet r a (k -> [Eff r a] -> k) where
+--   handle step _ MZero z jq = list z (flip step z) jq
+--   handle step q MPlus z jq = list z (flip step z) (left q : right q : jq)
+
+{-# INLINE next #-}
+-- | Progressing the cursor in a reified job queue.
+next :: Alternative f => Monad m
+     => (t -> [t] -> m (f a))
+     -> [t] -> m (f a)
+next k jq = list (return empty) k jq
+
+-- | Optimized implementation, faster and taking less memory. The benefit of the
+-- effect framework is that we can have many interpreters.
+makeChoiceA :: Alternative f => Eff (NDet ': r) a -> Eff r (f a)
+makeChoiceA m' = loop m' [] where
+  loop m = fix (handle_relay @NDet ret) m
+  -- single result; optimization: drop spurious empty
+  ret x [] = withNDet x
+  -- definite result and perhaps some others
+  ret x (h:t) = liftM2 (<|>) (withNDet x) (loop h t)
+
+-- | A different implementation, more involved, but similar complexity to
+-- 'makeChoiceA'.
+makeChoiceA_manual :: Alternative f => Eff (NDet ': r) a -> Eff r (f a)
+makeChoiceA_manual m = loop m [] where
+  -- single result; optimization: drop spurious empty
+  loop (Val x) []    = withNDet x
+  -- definite result and perhaps some others
+  loop (Val x) (h:t) = liftM2 (<|>) (withNDet x) (loop h t)
+  loop (E q u) jq    = case decomp u of
+    Right MZero -> next loop jq
+    Right MPlus -> loop (k True) (k False : jq)
+    Left  u0    -> relay (loop . k) u0 jq
+    where
+      k = (q ^$)
+
+-- | Same as 'makeChoiceA', except it has the type hardcoded.
+-- Required for 'MonadBaseControl' instance.
+makeChoice :: Eff (NDet ': r) a -> Eff r [a]
+makeChoice = makeChoiceA
+
+-- | We implement LogicT, the non-determinism reflection, of which soft-cut is
+-- one instance. See the LogicT paper for an explanation.
+instance Member NDet r => MSplit (Eff r) where
+  msplit = msplit'
+
+-- | The implementation of 'MSplit'. Exported as a standalone to make
+-- testing/comparison easier.
+{-# INLINE msplit' #-}
+msplit' :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a))
+msplit' m = fix (respond_relay @NDet (\x jq -> withMSplit x (msum jq))) m []
+
+-- | A different implementation, more involved, but similar complexity to
+-- 'msplit''.
+{-# INLINE msplit'_manual #-}
+msplit'_manual :: Member NDet r => Eff r a -> Eff r (Maybe (a, Eff r a))
+msplit'_manual m' = loop m' [] where
+  -- definite result and perhaps some others
+  loop (Val x) jq = withMSplit x (msum jq)
+  -- not yet definite answer
+  loop (E q u) jq = case u of
+    -- try other choices, if any
+    U0' MZero -> next loop jq
+    -- try left options; add right to job queue
+    U0' MPlus -> loop (k True) (k False : jq)
+    _         -> relay (loop . k) u jq
+    where
+      k x = q ^$ x
+
+-- | The call interpreter -- it is like reify . reflect with a twist. Compare
+-- this implementation with the huge implementation of call in Hinze 2000
+-- (Figure 9). Each clause corresponds to the axiom of call or cutfalse. All
+-- axioms are covered.
+--
+-- The code clearly expresses the intuition that call watches the choice points
+-- of its argument computation. When it encounteres a cutfalse request, it
+-- discards the remaining choicepoints.  It completely handles CutFalse effects
+-- but not non-determinism
+instance Member NDet r => Call r where
+  call m = loop m [] where
+    loop (Val x) jq = return x `mplus` nxt jq          -- (C2)
+    loop (E _ (U0 (Exc CutFalse))) _ = nxt []          -- drop jq (F2)
+    loop (E q (U1 u)) jq = case u of
+        U0' MZero -> nxt jq                            -- (C1)
+        U0' MPlus -> nxt (left q : right q : jq)       -- (C3)
+        _         -> relay (loop . (q ^$)) u jq        -- (C4)
+
+    nxt jq = list mzero loop jq
diff --git a/src/Control/Eff/NdetEff.hs b/src/Control/Eff/NdetEff.hs
deleted file mode 100644
--- a/src/Control/Eff/NdetEff.hs
+++ /dev/null
@@ -1,119 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE Safe #-}
--- The following is needed to define MonadPlus instance. It is decidable
--- (there is no recursion!), but GHC cannot see that.
-{-# LANGUAGE UndecidableInstances #-}
-
--- | Another implementation of nondeterministic choice effect
-module Control.Eff.NdetEff where
-
-import Control.Eff
-import Control.Eff.Extend
-import Control.Eff.Lift
-
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Base
-import Control.Monad.Trans.Control
-import Data.Foldable (foldl')
-
--- | A different implementation, more directly mapping to MonadPlus
--- interface
-data NdetEff a where
-  MZero :: NdetEff a
-  MPlus :: NdetEff Bool
-
-instance Member NdetEff r => Alternative (Eff r) where
-  empty = mzero
-  (<|>) = mplus
-
-instance Member NdetEff r => MonadPlus (Eff r) where
-  mzero = send MZero
-  mplus m1 m2 = send MPlus >>= \x -> if x then m1 else m2
-
-instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
-         ) => MonadBaseControl m (Eff (NdetEff ': r)) where
-    type StM (Eff (NdetEff ': r)) a = StM (Eff r) [a]
-    liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
-                       f (runInBase . makeChoiceLst)
-    restoreM x = do lst :: [a] <- raise (restoreM x)
-                    foldl' (\r a -> r <|> pure a) mzero lst
-
--- | An interpreter
--- The following is very simple, but leaks a lot of memory
--- The cause probably is mapping every failure to empty
--- It takes then a lot of timne and space to store those empty
-makeChoiceA0 :: Alternative f => Eff (NdetEff ': r) a -> Eff r (f a)
-makeChoiceA0 = handle_relay (return . pure) $ \m k -> case m of
-    MZero -> return empty
-    MPlus -> liftM2 (<|>) (k True) (k False)
-
--- | A different implementation, more involved but faster and taking
--- much less (100 times) less memory.
--- The benefit of the effect framework is that we can have many
--- interpreters.
-makeChoiceA :: Alternative f => Eff (NdetEff ': r) a -> Eff r (f a)
-makeChoiceA m = loop [] m
- where
-   loop [] (Val x)    = return (pure x)
-   loop (h:t) (Val x) = loop t h >>= \r -> return (pure x <|> r)
-   loop jq (E u q) = case  decomp u of
-     Right MZero     -> case jq of
-       []    -> return empty
-       (h:t) -> loop t h
-     Right MPlus -> loop (q ^$ False : jq) (q ^$ True)
-     Left  u0 -> E u0 (singleK (\x -> loop jq (q ^$ x)))
-
--- | Same as makeChoiceA, except it has the type hardcoded.
--- Required for MonadBaseControl instance.
-makeChoiceLst :: Eff (NdetEff ': r) a -> Eff r [a]
-makeChoiceLst = makeChoiceA
--- ------------------------------------------------------------------------
--- Soft-cut: non-deterministic if-then-else, aka Prolog's *->
--- Declaratively,
---    ifte t th el = (t >>= th) `mplus` ((not t) >> el)
--- However, t is evaluated only once. In other words, ifte t th el
--- is equivalent to t >>= th if t has at least one solution.
--- If t fails, ifte t th el is the same as el.
-
--- We actually implement LogicT, the non-determinism reflection,
--- of which soft-cut is one instance.
--- See the LogicT paper for an explanation
-msplit :: Member NdetEff r => Eff r a -> Eff r (Maybe (a, Eff r a))
-msplit = loop []
- where
- -- singleK result
- loop [] (Val x)  = return (Just (x,mzero))
- -- definite result and perhaps some others
- loop jq (Val x)  = return (Just (x, msum jq))
- -- not yet definite answer
- loop jq (E u q)  = case prj u of
-  Just MZero -> case jq of
-                   -- no futher choices
-                   []     -> return Nothing
-                   -- other choices remain, try them
-                   (j:jqT) -> loop jqT j
-  Just MPlus -> loop ((q ^$ False):jq) (q ^$ True)
-  _          -> E u (qComps q (loop jq))
-
--- Other committed choice primitives can be implemented in terms of msplit
--- The following implementations are directly from the LogicT paper
-ifte :: Member NdetEff r => Eff r a -> (a -> Eff r b) -> Eff r b -> Eff r b
-ifte t th el = msplit t >>= check
- where check Nothing          = el
-       check (Just (sg1,sg2)) = (th sg1) `mplus` (sg2 >>= th)
-
-once :: Member NdetEff r => Eff r a -> Eff r a
-once m = msplit m >>= check
- where check Nothing        = mzero
-       check (Just (sg1,_)) = return sg1
diff --git a/src/Control/Eff/Operational.hs b/src/Control/Eff/Operational.hs
--- a/src/Control/Eff/Operational.hs
+++ b/src/Control/Eff/Operational.hs
@@ -5,37 +5,48 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE Safe #-}
 
 -- | Operational Monad (<https://wiki.haskell.org/Operational>) implemented with
 -- extensible effects.
 
 module Control.Eff.Operational ( Program (..)
+                               , withOperational, Intrprtr (..)
                                , singleton
                                , runProgram
                                -- * Usage
                                -- $usage
                                ) where
 
-import Control.Eff
+import Control.Eff as E
 import Control.Eff.Extend
 
+import Data.Function (fix)
+
 -- | Lift values to an effect.
 -- You can think this is a generalization of @Lift@.
 data Program instr v where
   Singleton :: instr a -> Program instr a
 
+-- | General form of an interpreter
+newtype Intrprtr f r = Intrprtr { runIntrprtr :: forall x. f x -> Eff r x }
+
+-- | Embed a pure value
+withOperational :: a -> Intrprtr f r -> Eff r a
+withOperational x _ = return x
+-- | Given a continuation and a program, interpret it
+-- Usually, we have @r ~ [Program f : r']@
+instance Handle (Program f) r a (Intrprtr f r' -> Eff r' a) where
+  handle step q (Singleton instr) i = (runIntrprtr i) instr >>=
+    \x -> step (q ^$ x) i
+
 -- | Lift a value to a monad.
 singleton :: (Member (Program instr) r) => instr a -> Eff r a
 singleton = send . Singleton
 
 -- | Convert values using given interpreter to effects.
 runProgram :: forall f r a. (forall x. f x -> Eff r x) -> Eff (Program f ': r) a -> Eff r a
-runProgram advent = handle_relay return h
-  where
-    h :: forall v. Program f v -> (v -> Eff r a) -> Eff r a
-    h (Singleton instr) k = advent instr >>= k
+runProgram advent m = fix (handle_relay withOperational) m (Intrprtr advent)
 
 -- $usage
 --
@@ -48,6 +59,6 @@
 --main :: IO ()
 --main = do
 --    let comp = 'runProgram' adventPure prog
---    putStrLn . fst . 'run' . 'runMonoidWriter' $ 'evalState' comp [\"foo\",\"bar\"]
+--    putStrLn . fst . 'run' . 'E.Writer.Strict.runMonoidWriter' $ 'E.State.Strict.evalState' comp [\"foo\",\"bar\"]
 --    'runLift' $ 'runProgram' adventIO prog
 -- @
diff --git a/src/Control/Eff/Operational/Example.hs b/src/Control/Eff/Operational/Example.hs
--- a/src/Control/Eff/Operational/Example.hs
+++ b/src/Control/Eff/Operational/Example.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE Safe #-}
 
 -- | Example usage of "Control.Eff.Operational".
@@ -8,7 +7,6 @@
 
 import Control.Eff.Operational
 import Control.Eff
-import Control.Eff.Lift
 import Control.Eff.Writer.Lazy
 import Control.Eff.State.Lazy
 
@@ -25,11 +23,11 @@
    singleton $ Print ("the input is " ++ str)
 
 -- | Then, implements interpreters from the data to effects.
-adventIO :: (SetMember Lift (Lift IO) r) => Jail a -> Eff r a
+adventIO :: Lifted IO r => Jail a -> Eff r a
 adventIO (Print a) = lift $ putStrLn a
 adventIO Scan = lift getLine
 
-adventPure :: (Member (Writer String) r, Member (State [String]) r) => Jail a -> Eff r a
+adventPure :: [ Writer String, State [String] ] <:: r => Jail a -> Eff r a
 adventPure (Print a) = tell (a ++ "\n")
 adventPure Scan = do
   x <- get
diff --git a/src/Control/Eff/QuickStart.hs b/src/Control/Eff/QuickStart.hs
--- a/src/Control/Eff/QuickStart.hs
+++ b/src/Control/Eff/QuickStart.hs
@@ -45,11 +45,10 @@
 import           Control.Eff.Exception
 import           Control.Monad                            ( when )
 
-
 -- | an effectful function that can throw an error
 --
 -- @
--- tooBig = do
+-- tooBig i = do
 --   when (i > 100) $ throwError $ show i
 --   return i
 -- @
diff --git a/src/Control/Eff/Reader/Lazy.hs b/src/Control/Eff/Reader/Lazy.hs
--- a/src/Control/Eff/Reader/Lazy.hs
+++ b/src/Control/Eff/Reader/Lazy.hs
@@ -7,8 +7,10 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeApplications #-}
 -- | Lazy read-only state
 module Control.Eff.Reader.Lazy ( Reader (..)
+                              , withReader
                               , ask
                               , local
                               , reader
@@ -17,18 +19,19 @@
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | The Reader monad
 --
 -- The request for a value of type e from the current environment
 -- This can be expressed as a GADT because the type of values
 -- returned in response to a (Reader e a) request is not any a;
--- we expect in reply the value of type 'e', the value from the
+-- we expect in reply the value of type @e@, the value from the
 -- environment. So, the return type is restricted: 'a ~ e'
 data Reader e v where
   Ask :: Reader e e
@@ -46,6 +49,13 @@
 -- ^ In the latter case, when we make the request, we make it as Reader id.
 -- So, strictly speaking, GADTs are not really necessary.
 
+-- | How to interpret a pure value in a reader context
+withReader :: Monad m => a -> e -> m a
+withReader x _ = return x
+-- | Given a value to read, and a callback, how to respond to
+-- requests.
+instance Handle (Reader e) r a (e -> k) where
+  handle step q Ask e = step (q ^$ e) e
 
 -- | Get the current value from a Reader.
 -- The signature is inferred (when using NoMonomorphismRestriction).
@@ -54,10 +64,8 @@
 
 -- | The handler of Reader requests. The return type shows that all Reader
 -- requests are fully handled.
-runReader :: e -> Eff (Reader e ': r) w -> Eff r w
-runReader e = handle_relay
-  return
-  (\Ask -> ($ e))
+runReader :: forall e r w. e -> Eff (Reader e ': r) w -> Eff r w
+runReader e m = fix (handle_relay withReader) m e
 
 -- | Locally rebind the value in the dynamic environment This function is like a
 -- relay; it is both an admin for Reader requests, and a requestor of them.
@@ -65,18 +73,15 @@
          (e -> e) -> Eff r a -> Eff r a
 local f m = do
   e <- reader f
-  let
-    h :: Reader e t -> (t -> Eff r b) -> Eff r b
-    h Ask = ($ e)
-  interpose return h m
+  (fix (respond_relay @(Reader e) withReader)) m e
+  -- note similarity between 'local' and 'State.Lazy.transactionState'
 
 -- | Request the environment value using a transformation function.
 reader :: (Member (Reader e) r) => (e -> a) -> Eff r a
 reader f = f `fmap` ask
 
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) s
-         , MonadBaseControl m (Eff s)
+         , LiftedBase m s
          ) => MonadBaseControl m (Eff (Reader e ': s)) where
     type StM (Eff (Reader e ': s)) a = StM (Eff s) a
     liftBaseWith f = do e <- ask
diff --git a/src/Control/Eff/Reader/Strict.hs b/src/Control/Eff/Reader/Strict.hs
--- a/src/Control/Eff/Reader/Strict.hs
+++ b/src/Control/Eff/Reader/Strict.hs
@@ -7,29 +7,32 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE Safe #-}
 -- | Strict read-only state
 module Control.Eff.Reader.Strict ( Reader (..)
-                              , ask
-                              , local
-                              , reader
-                              , runReader
-                              ) where
+                                 , withReader
+                                 , ask
+                                 , local
+                                 , reader
+                                 , runReader
+                                 ) where
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | The Reader monad
 --
 -- The request for a value of type e from the current environment
 -- This can be expressed as a GADT because the type of values
 -- returned in response to a (Reader e a) request is not any a;
--- we expect in reply the value of type 'e', the value from the
+-- we expect in reply the value of type @e@, the value from the
 -- environment. So, the return type is restricted: 'a ~ e'
 data Reader e v where
   Ask :: Reader e e
@@ -47,6 +50,13 @@
 -- ^ In the latter case, when we make the request, we make it as Reader id.
 -- So, strictly speaking, GADTs are not really necessary.
 
+-- | How to interpret a pure value in a reader context
+withReader :: Monad m => a -> e -> m a
+withReader x _ = return x
+-- | Given a value to read, and a callback, how to respond to
+-- requests.
+instance Handle (Reader e) r a (e -> k) where
+  handle step q Ask e = step (q ^$ e) e
 
 -- | Get the current value from a Reader.
 -- The signature is inferred (when using NoMonomorphismRestriction).
@@ -56,28 +66,23 @@
 -- | The handler of Reader requests. The return type shows that all Reader
 -- requests are fully handled.
 runReader :: e -> Eff (Reader e ': r) w -> Eff r w
-runReader !e = handle_relay
-  return
-  (\Ask -> ($ e))
+runReader !e m = fix (handle_relay withReader) m e
 
 -- | Locally rebind the value in the dynamic environment This function is like a
--- relay; it is both an admin for Reader requests, and a requestor of them
+-- relay; it is both an admin for Reader requests, and a requestor of them.
 local :: forall e a r. Member (Reader e) r =>
          (e -> e) -> Eff r a -> Eff r a
 local f m = do
   e <- reader f
-  let
-    h :: Reader e t -> (t -> Eff r b) -> Eff r b
-    h Ask = ($ e)
-  interpose return h m
+  (fix (respond_relay @(Reader e) withReader)) m e
+  -- note similarity between 'local' and 'State.Strict.transactionState'
 
 -- | Request the environment value using a transformation function.
 reader :: (Member (Reader e) r) => (e -> a) -> Eff r a
 reader f = f `fmap` ask
 
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) s
-         , MonadBaseControl m (Eff s)
+         , LiftedBase m s
          ) => MonadBaseControl m (Eff (Reader e ': s)) where
     type StM (Eff (Reader e ': s)) a = StM (Eff s) a
     liftBaseWith f = do !e <- ask
diff --git a/src/Control/Eff/State/Lazy.hs b/src/Control/Eff/State/Lazy.hs
--- a/src/Control/Eff/State/Lazy.hs
+++ b/src/Control/Eff/State/Lazy.hs
@@ -8,12 +8,12 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
 -- | Lazy state effect
 module Control.Eff.State.Lazy where
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Eff.Writer.Lazy
 import Control.Eff.Reader.Lazy
@@ -21,6 +21,8 @@
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | State, lazy
 --
@@ -42,9 +44,20 @@
   Get :: State s s
   Put :: s -> State s ()
 
+-- | Embed a pure value in a stateful computation, i.e., given an
+-- initial state, how to interpret a pure value in a stateful
+-- computation.
+withState :: Monad m => a -> s -> m (a, s)
+withState x s = return (x, s)
+
+-- | Handle 'State s' requests
+instance Handle (State s) r a (s -> k) where
+  handle step q sreq s = case sreq of
+    Get    -> step (q ^$ s) s
+    Put s' -> step (q ^$ ()) s'
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (State s ': r)) where
     type StM (Eff (State s ': r)) a = StM (Eff r) (a,s)
     liftBaseWith f = do s <- get
@@ -78,25 +91,11 @@
 -- inline get/put, even if I put the INLINE directives and play with phases.
 -- (Inlining works if I use 'inline' explicitly).
 
--- | Run a state effect. compared to the @runState@ function, this is
---   implemented naively and is expected to perform slower.
-runState' :: s -> Eff (State s ': r) a -> Eff r (a, s)
-runState' s =
-  handle_relay_s s (\s0 x -> return (x,s0))
-                   (\s0 sreq k -> case sreq of
-                       Get    -> k s0 s0
-                       Put s1 -> k s1 ())
-
--- | Run a State effect. This variant is a bit optimized compared to
---   @runState'@.
+-- | Run a State effect
 runState :: s                     -- ^ Initial state
          -> Eff (State s ': r) a  -- ^ Effect incorporating State
          -> Eff r (a, s)          -- ^ Effect containing final state and a return value
-runState s (Val x) = return (x,s)
-runState s (E u q) = case decomp u of
-  Right Get     -> runState s (q ^$ s)
-  Right (Put s1) -> runState s1 (q ^$ ())
-  Left  u1 -> E u1 (singleK (\x -> runState s (q ^$ x)))
+runState s m = fix (handle_relay withState) m s
 
 -- | Transform the state with a function.
 modify :: (Member (State s) r) => (s -> s) -> Eff r ()
@@ -113,29 +112,30 @@
 -- | An encapsulated State handler, for transactional semantics
 -- The global state is updated only if the transactionState finished
 -- successfully
-data TxState s = TxState
-transactionState :: forall s r a. Member (State s) r =>
-                    TxState s -> Eff r a -> Eff r a
-transactionState _ m = do s <- get; loop s m
- where
-   loop :: s -> Eff r a -> Eff r a
-   loop s (Val x) = put s >> return x
-   loop s (E (u::Union r b) q) = case prj u :: Maybe (State s b) of
-     Just Get      -> loop s (q ^$ s)
-     Just (Put s') -> loop s'(q ^$ ())
-     _             -> E u (qComps q (loop s))
+data TxState s v where
+  TxState :: TxState s s
+type TxStateT s = TxState s s
 
+-- | Embed Transactional semantics to a stateful computation.
+withTxState :: Member (State s) r => a -> s -> Eff r a
+withTxState x s = put s >> return x
+
+-- | Confer transactional semantics on a stateful computation.
+transactionState :: forall s r a. Member (State s) r
+                 => TxStateT s -> Eff r a -> Eff r a
+transactionState _ m = do
+  s <- get
+  (fix $ respond_relay @(State s) (withTxState @s)) m s
+
 -- | A different representation of State: decomposing State into mutation
 -- (Writer) and Reading. We don't define any new effects: we just handle the
 -- existing ones.  Thus we define a handler for two effects together.
 runStateR :: s -> Eff (Writer s ': Reader s ': r) a -> Eff r (a, s)
-runStateR s m = loop s m
+runStateR = flip loop
  where
-   loop :: s -> Eff (Writer s ': Reader s ': r) a -> Eff r (a, s)
-   loop s0 (Val x) = return (x,s0)
-   loop s0 (E u q) = case decomp u of
-     Right (Tell w) -> k w ()
-     Left  u1  -> case decomp u1 of
-       Right Ask -> k s0 s0
-       Left u2 -> E u2 (singleK (k s0))
-    where k x = qComp q (loop x)
+   loop :: Eff (Writer s ': Reader s ': r) a -> s -> Eff r (a, s)
+   loop (Val x) = withState x
+   loop (E q u) = case u of
+     U0 (Tell w) -> handle loop q (Put w)
+     U1 (U0 Ask) -> handle loop q Get
+     U1 (U1 u') -> relay (qComp q loop) u'
diff --git a/src/Control/Eff/State/OnDemand.hs b/src/Control/Eff/State/OnDemand.hs
--- a/src/Control/Eff/State/OnDemand.hs
+++ b/src/Control/Eff/State/OnDemand.hs
@@ -13,14 +13,16 @@
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Eff.Writer.Lazy
 import Control.Eff.Reader.Lazy
+import qualified Control.Eff.State.Lazy as S
 
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | State, lazy (i.e., on-demand)
 --
@@ -33,9 +35,16 @@
   Put  :: s -> OnDemandState s ()
   Delay :: Eff '[OnDemandState s] a  -> OnDemandState s a --  Eff as a transformer
 
+-- | Given a continuation, respond to requests
+instance Handle (OnDemandState s) r a (s -> k) where
+  handle step q sreq s = case sreq of
+    Get     -> step (q ^$ s) s
+    Put s'  -> step (q ^$ ()) s'
+    Delay m -> let ~(x, s') = run $ (fix (handle_relay S.withState)) m s
+                              in step (q ^$ x) s'
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (OnDemandState s ': r)) where
     type StM (Eff (OnDemandState s ': r)) a = StM (Eff r) (a,s)
     liftBaseWith f = do s <- get
@@ -73,28 +82,11 @@
 onDemand :: Member (OnDemandState s) r => Eff '[OnDemandState s] v -> Eff r v
 onDemand = send . Delay
 
-runState' :: s -> Eff (OnDemandState s ': r) w -> Eff r (w,s)
-runState' s =
-  handle_relay_s s
-  (\s0 x -> return (x,s0))
-  (\s0 sreq k -> case sreq of
-      Get    -> k s0 s0
-      Put s1 -> k s1 ()
-      Delay m1 -> let ~(x,s1) = run $ runState' s0 m1
-                  in k s1 x)
-
--- Since State is so frequently used, we optimize it a bit
 -- | Run a State effect
 runState :: s                            -- ^ Initial state
          -> Eff (OnDemandState s ': r) w -- ^ Effect incorporating State
          -> Eff r (w,s)                  -- ^ Effect containing final state and a return value
-runState s (Val x) = return (x,s)
-runState s0 (E u0 q) = case decomp u0 of
-  Right Get     -> runState s0 (q ^$ s0)
-  Right (Put s1) -> runState s1 (q ^$ ())
-  Right (Delay m1) -> let ~(x,s1) = run $ runState s0 m1
-                      in runState s1 (q ^$ x)
-  Left  u -> E u (singleK (\x -> runState s0 (q ^$ x)))
+runState s m = fix (handle_relay S.withState) m s
 
 -- | Transform the state with a function.
 modify :: (Member (OnDemandState s) r) => (s -> s) -> Eff r ()
@@ -112,52 +104,48 @@
 -- (Writer) and Reading. We don't define any new effects: we just handle the
 -- existing ones.  Thus we define a handler for two effects together.
 runStateR :: s -> Eff (Writer s ': Reader s ': r) w -> Eff r (w,s)
-runStateR s0 m0 = loop s0 m0
- where
-   loop :: s -> Eff (Writer s ': Reader s ': r) w -> Eff r (w,s)
-   loop s (Val x) = return (x,s)
-   loop s (E u0 q) = case decomp u0 of
-     Right (Tell w) -> k w ()
-     Left  u  -> case decomp u of
-       Right Ask -> k s s
-       Left u1 -> E u1 (singleK (k s))
-    where k x = qComp q (loop x)
+runStateR s (Val x) = S.withState x s
+runStateR s (E q u) = case u of
+  U0 (Tell w) -> handle loop q (S.Put w) s
+  U1 (U0 Ask) -> handle loop q S.Get s
+  U1 (U1 u') -> relay (qComp q loop) u' s
+  where loop = flip runStateR
 
 -- | Backwards state
 -- The overall state is represented with two attributes: the inherited
 -- getAttr and the synthesized putAttr.
 -- At the root node, putAttr becomes getAttr, tying the knot.
--- As usual, the inherited attribute is the argument (i.e., the `environment')
+-- As usual, the inherited attribute is the argument (i.e., the @environment@)
 -- and the synthesized is the result of the handler |go| below.
 runStateBack0 :: Eff '[OnDemandState s] a -> (a,s)
 runStateBack0 m =
-  let (x,s) = go s m in
+  let (x,s) = go m s in
   (x,s)
  where
-   go :: s -> Eff '[OnDemandState s] a -> (a,s)
-   go s (Val x) = (x,s)
-   go s0 (E u q) = case decomp u of
-         Right Get      -> go s0 $ (q ^$ s0)
-         Right (Put s1)  -> let ~(x,sp) = go sp $ (q ^$ ()) in (x,s1)
-         Right (Delay m1) -> let ~(x,s1) = go s0 m1 in go s1 $ (q ^$ x)
-         Left _ -> error "Impossible happened: Union []"
+   go :: Eff '[OnDemandState s] a -> s -> (a,s)
+   go (Val x) s = (x,s)
+   go (E q u) s0 = case decomp u of
+     Right Get      -> k s0 s0
+     Right (Put s1)  -> let ~(x,sp) = k () sp in (x,s1)
+     Right (Delay m1) -> let ~(x,s1) = go m1 s0 in k x s1
+     Left _ -> error "Impossible happened: Nothing to relay!"
+     where
+       k = qComp q go
 
 -- | Another implementation, exploring Haskell's laziness to make putAttr
 -- also technically inherited, to accumulate the sequence of
 -- updates. This implementation is compatible with deep handlers, and
--- lets us play with different notions of `backwardness'
+-- lets us play with different notions of backwardness.
 runStateBack :: Eff '[OnDemandState s] a -> (a,s)
 runStateBack m =
-  let (x,(_sg,sp)) = run $ go (sp,[]) m in
+  let (x,(_,sp)) = run $ go m (sp,[]) in
   (x,head sp)
  where
-   go :: ([s],[s]) -> Eff '[OnDemandState s] a -> Eff '[] (a,([s],[s]))
-   go ss = handle_relay_s ss (\ss0 x -> return (x,ss0))
-                   (\ss0@(sg,sp) req k -> case req of
-                       Get    -> k ss0 (head sg)
-                       Put s1  -> k (tail sg,sp++[s1]) ()
-                       Delay m1 -> let ~(x,ss1) = run $ go ss0 m1
-                                   in k ss1 x)
+   go :: Eff '[OnDemandState s] a -> ([s],[s]) -> Eff '[] (a,([s],[s]))
+   go = fix (handle_relay' h S.withState)
+   h step q Get s0@(sg, _) = step (q ^$ head sg) s0
+   h step q (Put s1) (sg, sp) = step (q ^$ ()) (tail sg,sp++[s1])
+   h step q (Delay m1) s0 = let ~(x,s1) = run $ go m1 s0 in step (q ^$ x) s1
 
--- ^ A different notion of `backwards' is realized if we change the Put
--- handler slightly. How?
+-- ^ A different notion of backwards is realized if we change the Put handler
+-- slightly. How?
diff --git a/src/Control/Eff/State/Strict.hs b/src/Control/Eff/State/Strict.hs
--- a/src/Control/Eff/State/Strict.hs
+++ b/src/Control/Eff/State/Strict.hs
@@ -9,12 +9,12 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
 -- | Strict state effect
 module Control.Eff.State.Strict where
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Eff.Writer.Strict
 import Control.Eff.Reader.Strict
@@ -22,6 +22,8 @@
 import Control.Monad.Base
 import Control.Monad.Trans.Control
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | State, strict
 --
@@ -43,9 +45,20 @@
   Get :: State s s
   Put :: !s -> State s ()
 
+-- | Embed a pure value in a stateful computation, i.e., given an
+-- initial state, how to interpret a pure value in a stateful
+-- computation.
+withState :: Monad m => a -> s -> m (a, s)
+withState x s = return (x, s)
+
+-- | Handle 'State s' requests
+instance Handle (State s) r a (s -> k) where
+  handle step q sreq s = case sreq of
+    Get    -> step (q ^$ s) s
+    Put s' -> step (q ^$ ()) s'
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (State s ': r)) where
     type StM (Eff (State s ': r)) a = StM (Eff r) (a,s)
     liftBaseWith f = do s <- get
@@ -80,23 +93,11 @@
 -- inline get/put, even if I put the INLINE directives and play with phases.
 -- (Inlining works if I use 'inline' explicitly).
 
-runState' :: s -> Eff (State s ': r) a -> Eff r (a, s)
-runState' !s =
-  handle_relay_s s (\s0 x -> return (x,s0))
-                   (\s0 sreq k -> case sreq of
-                       Get    -> k s0 s0
-                       Put s1 -> k s1 ())
-
--- Since State is so frequently used, we optimize it a bit
 -- | Run a State effect
-runState :: s                     -- ^ Effect incorporating State
-         -> Eff (State s ': r) a  -- ^ Initial state
+runState :: s                     -- ^ Initial state
+         -> Eff (State s ': r) a  -- ^ Effect incorporating State
          -> Eff r (a, s)          -- ^ Effect containing final state and a return value
-runState !s (Val x) = return (x,s)
-runState !s (E u q) = case decomp u of
-  Right Get     -> runState s (q ^$ s)
-  Right (Put s1) -> runState  s1 (q ^$ ())
-  Left  u1 -> E u1 (singleK (\x -> runState s (q ^$ x)))
+runState !s m = fix (handle_relay withState) m s
 
 -- | Transform the state with a function.
 modify :: (Member (State s) r) => (s -> s) -> Eff r ()
@@ -116,28 +117,27 @@
 -- The global state is updated only if the transactionState finished
 -- successfully
 data TxState s = TxState
-transactionState :: forall s r a. Member (State s) r =>
-                    TxState s -> Eff r a -> Eff r a
-transactionState _ m = do s <- get; loop s m
- where
-   loop :: s -> Eff r a -> Eff r a
-   loop s (Val x) = put s >> return x
-   loop s (E (u::Union r b) q) = case prj u :: Maybe (State s b) of
-     Just Get      -> loop s (q ^$ s)
-     Just (Put s') -> loop s'(q ^$ ())
-     _             -> E u (qComps q (loop s))
 
+-- | Embed Transactional semantics to a stateful computation.
+withTxState :: Member (State s) r => a -> s -> Eff r a
+withTxState x s = put s >> return x
+
+-- | Confer transactional semantics on a stateful computation.
+transactionState :: forall s r a. Member (State s) r
+                 => TxState s -> Eff r a -> Eff r a
+transactionState _ m = do
+  s <- get
+  (fix $ respond_relay @(State s) (withTxState @s)) m s
+
 -- | A different representation of State: decomposing State into mutation
 -- (Writer) and Reading. We don't define any new effects: we just handle the
 -- existing ones.  Thus we define a handler for two effects together.
 runStateR :: s -> Eff (Writer s ': Reader s ': r) a -> Eff r (a, s)
-runStateR !s m = loop s m
+runStateR !s m = loop m s
  where
-   loop :: s -> Eff (Writer s ': Reader s ': r) a -> Eff r (a, s)
-   loop s0 (Val x) = return (x,s0)
-   loop s0 (E u q) = case decomp u of
-     Right (Tell w) -> k w ()
-     Left  u1  -> case decomp u1 of
-       Right Ask -> k s0 s0
-       Left u2 -> E u2 (singleK (k s0))
-    where k x = qComp q (loop x)
+   loop :: Eff (Writer s ': Reader s ': r) a -> s -> Eff r (a, s)
+   loop (Val x) = withState x
+   loop (E q u) = case u of
+     U0 (Tell w) -> handle loop q (Put w)
+     U1 (U0 Ask) -> handle loop q Get
+     U1 (U1 u') -> relay (qComp q loop) u'
diff --git a/src/Control/Eff/Trace.hs b/src/Control/Eff/Trace.hs
--- a/src/Control/Eff/Trace.hs
+++ b/src/Control/Eff/Trace.hs
@@ -5,17 +5,27 @@
 {-# LANGUAGE Safe #-}
 -- | A Trace effect for debugging
 module Control.Eff.Trace( Trace (..)
+                        , withTrace
                         , trace
                         , runTrace
                         ) where
 
 import Control.Eff
 import Control.Eff.Extend
+import Data.Function (fix)
 
 -- | Trace effect for debugging
 data Trace v where
   Trace :: String -> Trace ()
 
+-- | Embed a pure value in Trace context
+withTrace :: a -> IO a
+withTrace = return
+
+-- | Given a callback and request, respond to it
+instance Handle Trace r a (IO k) where
+  handle step q (Trace s) = putStrLn s >> step (q ^$ ())
+
 -- | Print a string as a trace.
 trace :: Member Trace r => String -> Eff r ()
 trace = send . Trace
@@ -23,8 +33,8 @@
 -- | Run a computation producing Traces.
 -- The handler for IO request: a terminal handler
 runTrace :: Eff '[Trace] w -> IO w
-runTrace (Val x) = return x
-runTrace (E u q) = case decomp u of
-     Right (Trace s) -> putStrLn s >> runTrace (q ^$ ())
-     -- Nothing more can occur
-     Left _ -> error "runTrace: the impossible happened!: Union []"
+runTrace = fix step where
+  step next = eff return
+              (\q u -> case u of
+                  U0 x -> handle next q x
+                  _    -> error "Impossible: Nothing to relay!")
diff --git a/src/Control/Eff/Writer/Lazy.hs b/src/Control/Eff/Writer/Lazy.hs
--- a/src/Control/Eff/Writer/Lazy.hs
+++ b/src/Control/Eff/Writer/Lazy.hs
@@ -8,8 +8,10 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeApplications #-}
 -- | Lazy write-only state
 module Control.Eff.Writer.Lazy ( Writer(..)
+                               , withWriter
                                , tell
                                , censor
                                , runWriter
@@ -26,7 +28,6 @@
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Applicative ((<|>))
 
@@ -36,6 +37,8 @@
 import Data.Monoid
 #endif
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | The Writer monad
 --
@@ -46,9 +49,18 @@
 data Writer w v where
   Tell :: w -> Writer w ()
 
+-- | How to interpret a pure value in a writer context, given the
+-- value for mempty.
+withWriter :: Monad m => a -> b -> (w -> b -> b) -> m (a, b)
+withWriter x empty _append = return (x, empty)
+-- | Given a value to write, and a callback (which includes empty and
+-- append), respond to requests.
+instance Monad m => Handle (Writer w) r a (b -> (w -> b -> b) -> m (a, b)) where
+  handle step q (Tell w) e append = step (q ^$ ()) e append >>=
+    \(x, l) -> return (x, w `append` l)
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (Writer w ': r)) where
     type StM (Eff (Writer w ': r)) a = StM (Eff r) (a, [w])
     liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
@@ -63,22 +75,16 @@
 
 -- | Transform the state being produced.
 censor :: forall w a r. Member (Writer w) r => (w -> w) -> Eff r a -> Eff r a
-censor f = interpose return h
+censor f = fix (respond_relay' h return)
   where
-    h :: Writer w t -> (t -> Eff r b) -> Eff r b
-    h (Tell w) k = tell (f w) >>= k
+    h :: (Eff r b -> Eff r b) -> Arrs r v b -> Writer w v -> Eff r b
+    h step q (Tell w) = tell (f w) >>= \x -> step (q ^$ x)
 
 
 -- | Handle Writer requests, using a user-provided function to accumulate
 -- values, hence no Monoid constraints.
 runWriter :: (w -> b -> b) -> b -> Eff (Writer w ': r) a -> Eff r (a, b)
-runWriter accum b = handle_relay
-  (\x -> return (x, b))
-  (\(Tell w) k -> k () >>= \(x, l) -> return (x, w `accum` l))
-  -- the second arg to 'handle_relay' above is same as:
-  -- (\(Tell w) k -> second (accum w) `fmap` k ())
-  -- where
-  --   second f (x, y) = (x, f y)
+runWriter accum b m = fix (handle_relay withWriter) m b accum
 
 -- | Handle Writer requests, using a List to accumulate values.
 runListWriter :: Eff (Writer w ': r) a -> Eff r (a,[w])
diff --git a/src/Control/Eff/Writer/Strict.hs b/src/Control/Eff/Writer/Strict.hs
--- a/src/Control/Eff/Writer/Strict.hs
+++ b/src/Control/Eff/Writer/Strict.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE CPP #-}
 -- | Strict write-only state
 module Control.Eff.Writer.Strict ( Writer(..)
+                               , withWriter
                                , tell
                                , censor
                                , runWriter
@@ -27,7 +28,6 @@
 
 import Control.Eff
 import Control.Eff.Extend
-import Control.Eff.Lift
 
 import Control.Applicative ((<|>))
 
@@ -37,6 +37,8 @@
 import Data.Monoid
 #endif
 
+import Data.Function (fix)
+
 -- ------------------------------------------------------------------------
 -- | The Writer monad
 --
@@ -47,9 +49,18 @@
 data Writer w v where
   Tell :: !w -> Writer w ()
 
+-- | How to interpret a pure value in a writer context, given the
+-- value for mempty.
+withWriter :: Monad m => a -> b -> (w -> b -> b) -> m (a, b)
+withWriter x empty _append = return (x, empty)
+-- | Given a value to write, and a callback (which includes empty and
+-- append), respond to requests.
+instance Monad m => Handle (Writer w) r a (b -> (w -> b -> b) -> m (a, b)) where
+  handle step q (Tell w) e append = step (q ^$ ()) e append >>=
+    \(x, l) -> return (x, w `append` l)
+
 instance ( MonadBase m m
-         , SetMember Lift (Lift m) r
-         , MonadBaseControl m (Eff r)
+         , LiftedBase m r
          ) => MonadBaseControl m (Eff (Writer w ': r)) where
     type StM (Eff (Writer w ': r)) a = StM (Eff r) (a, [w])
     liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
@@ -64,22 +75,16 @@
 
 -- | Transform the state being produced.
 censor :: forall w a r. Member (Writer w) r => (w -> w) -> Eff r a -> Eff r a
-censor f = interpose return h
+censor f = fix (respond_relay' h return)
   where
-    h :: Writer w t -> (t -> Eff r b) -> Eff r b
-    h (Tell w) k = tell (f w) >>= k
+    h :: (Eff r b -> Eff r b) -> Arrs r v b -> Writer w v -> Eff r b
+    h step q (Tell w) = tell (f w) >>= \x -> step (q ^$ x)
 
 
 -- | Handle Writer requests, using a user-provided function to accumulate
 -- values, hence no Monoid constraints.
 runWriter :: (w -> b -> b) -> b -> Eff (Writer w ': r) a -> Eff r (a, b)
-runWriter accum !b = handle_relay
-  (\x -> return (x, b))
-  (\(Tell w) k -> k () >>= \(x, l) -> return (x, w `accum` l))
-  -- the second arg to 'handle_relay' above is same as:
-  -- (\(Tell w) k -> second (accum w) `fmap` k ())
-  -- where
-  --   second f (x, y) = (x, f y)
+runWriter accum !b m = fix (handle_relay withWriter) m b accum
 
 -- | Handle Writer requests, using a List to accumulate values.
 runListWriter :: Eff (Writer w ': r) a -> Eff r (a,[w])
diff --git a/src/Data/FTCQueue.hs b/src/Data/FTCQueue.hs
--- a/src/Data/FTCQueue.hs
+++ b/src/Data/FTCQueue.hs
@@ -2,10 +2,8 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Safe #-}
 
--- | Fast type-aligned queue optimized to effectful functions
--- (a -> m b)
--- (monad continuations have this type).
--- Constant-time append and snoc and
+-- | Fast type-aligned queue optimized to effectful functions @(a -> m b)@
+-- (monad continuations have this type). Constant-time append and snoc and
 -- average constant-time left-edge deconstruction
 module Data.FTCQueue (
   FTCQueue,
@@ -19,7 +17,7 @@
   where
 
 -- | Non-empty tree. Deconstruction operations make it more and more
--- left-leaning
+-- left-leaning.
 data FTCQueue m a b where
   Leaf :: (a -> m b) -> FTCQueue m a b
   Node :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
@@ -27,7 +25,7 @@
 
 -- Exported operations
 
--- | There is no tempty: use (tsingleton return), which works just the same.
+-- | There is no @tempty@: use (@tsingleton return@), which works just the same.
 -- The names are chosen for compatibility with FastTCQueue
 {-# INLINE tsingleton #-}
 tsingleton :: (a -> m b) -> FTCQueue m a b
diff --git a/src/Data/OpenUnion.hs b/src/Data/OpenUnion.hs
--- a/src/Data/OpenUnion.hs
+++ b/src/Data/OpenUnion.hs
@@ -1,7 +1,6 @@
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# OPTIONS_GHC -Wwarn #-}
-
-{-# LANGUAGE CPP #-}
+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}
 
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
@@ -10,15 +9,12 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
-#if __GLASGOW_HASKELL__ < 710 || FORCE_OU51
-{-# LANGUAGE OverlappingInstances #-}
-#endif
-
 -- Only for SetMember below, when emulating Monad Transformers
 {-# LANGUAGE FunctionalDependencies, UndecidableInstances #-}
 
@@ -57,8 +53,8 @@
 -- The interface is the same as of other OpenUnion*.hs
 module Data.OpenUnion ( Union
                       , inj
-                      , prj
-                      , decomp
+                      , prj, pattern U0'
+                      , decomp, pattern U0, pattern U1
                       , Member
                       , SetMember
                       , type(<::)
@@ -67,12 +63,8 @@
 
 import Unsafe.Coerce(unsafeCoerce)
 
-#if __GLASGOW_HASKELL__ > 800
 import Data.Kind (Constraint)
 import GHC.TypeLits
-#else
-import GHC.Exts (Constraint)
-#endif
 
 -- | The data constructors of Union are not exported
 --
@@ -97,27 +89,17 @@
 -- | Typeclass that asserts that effect @t@ is contained inside the effect-list
 -- @r@.
 --
--- The @FindElem@ typeclass is necessary for implementation reasons and is not
--- required for using the effect list.
+-- The @FindElem@ typeclass is an implementation detail and not required for
+-- using the effect list or implementing custom effects.
 class (FindElem t r) => Member (t :: * -> *) r where
   inj :: t v -> Union r v
   prj :: Union r v -> Maybe (t v)
 
-#if __GLASGOW_HASKELL__ < 710 || FORCE_OU51
-{-
--- Optimized specialized instance
-instance Member t '[t] where
-  {-# INLINE inj #-}
-  {-# INLINE prj #-}
-  inj x           = Union 0 x
-  prj (Union _ x) = Just (unsafeCoerce x)
--}
-instance (FindElem t r) => Member t r where
-  {-# INLINE inj #-}
-  {-# INLINE prj #-}
-  inj = inj' (unP $ (elemNo :: P t r))
-  prj = prj' (unP $ (elemNo :: P t r))
-#else
+-- | Pattern synonym to project the union onto the effect @t@.
+pattern U0' :: Member t r => t v -> Union r v
+pattern U0' h <- (prj -> Just h) where
+  U0' h = inj h
+
 -- | Explicit type-level equality condition is a dirty
 -- hack to eliminate the type annotation in the trivial case,
 -- such as @run (runReader () get)@.
@@ -142,29 +124,35 @@
   {-# INLINE prj #-}
   inj = inj' (unP $ (elemNo :: P t r))
   prj = prj' (unP $ (elemNo :: P t r))
-#endif
 
--- | A useful operator for reducing boilerplate.
+-- | A useful operator for reducing boilerplate in signatures.
 --
--- @
--- f :: [Reader Int, Writer String] <:: r
---   => a -> Eff r b
--- @
--- is equal to
+-- The following lines are equivalent.
 --
 -- @
--- f :: (Member (Reader Int) r, Member (Writer String) r)
---   => a -> Eff r b
+-- (Member (Exc e) r, Member (State s) r) => ...
+-- [ Exc e, State s ] <:: r => ...
 -- @
 type family (<::) (ms :: [* -> *]) r where
   (<::) '[] r = (() :: Constraint)
   (<::) (m ': ms) r = (Member m r, (<::) ms r)
 
 {-# INLINE [2] decomp #-}
+-- | Orthogonal decomposition of the union: head and the rest.
 decomp :: Union (t ': r) v -> Either (Union r v) (t v)
 decomp (Union 0 v) = Right $ unsafeCoerce v
 decomp (Union n v) = Left  $ Union (n-1) v
 
+-- | Some helpful pattern synonyms.
+-- U0 : the first element of the union
+pattern U0 :: t v -> Union (t ': r) v
+pattern U0 h <- (decomp -> Right h) where
+  U0 h = inj h
+-- | U1 : everything excluding the first element of the union.
+pattern U1 t <- (decomp -> Left t) where
+  U1 t = weaken t
+{-# COMPLETE U0, U1 #-}
+
 -- Specialized version
 {-# RULES "decomp/singleton"  decomp = decomp0 #-}
 {-# INLINE decomp0 #-}
@@ -175,7 +163,7 @@
 weaken :: Union r w -> Union (any ': r) w
 weaken (Union n v) = Union (n+1) v
 
--- | Find an index of an element in a `list'
+-- | Find the index of an element in a type-level list.
 -- The element must exist
 -- This is essentially a compile-time computation.
 -- Using overlapping instances here is OK since this class is private to this
@@ -185,29 +173,19 @@
 
 instance FindElem t (t ': r) where
   elemNo = P 0
-#if __GLASGOW_HASKELL__ < 710 || FORCE_OU51
-instance FindElem t r => FindElem t (t' ': r) where
-#else
 instance {-# OVERLAPPABLE #-} FindElem t r => FindElem t (t' ': r) where
-#endif
   elemNo = P $ 1 + (unP $ (elemNo :: P t r))
-#if __GLASGOW_HASKELL__ > 800
 instance TypeError ('Text "Cannot unify effect types." ':$$:
                     'Text "Unhandled effect: " ':<>: 'ShowType t ':$$:
                     'Text "Perhaps check the type of effectful computation and the sequence of handlers for concordance?")
   => FindElem t '[] where
   elemNo = error "unreachable"
-#endif
 
 -- | Using overlapping instances here is OK since this class is private to this
 -- module
 class EQU (a :: k) (b :: k) p | a b -> p
 instance EQU a a 'True
-#if __GLASGOW_HASKELL__ < 710 || FORCE_OU51
-instance (p ~ 'False) => EQU a b p
-#else
 instance {-# OVERLAPPABLE #-} (p ~ 'False) => EQU a b p
-#endif
 
 -- | This class is used for emulating monad transformers
 class Member t r => SetMember (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t
diff --git a/test/Control/Eff/Choose/Test.hs b/test/Control/Eff/Choose/Test.hs
deleted file mode 100644
--- a/test/Control/Eff/Choose/Test.hs
+++ /dev/null
@@ -1,61 +0,0 @@
-{-# LANGUAGE FlexibleContexts, AllowAmbiguousTypes #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-module Control.Eff.Choose.Test (testGroups) where
-
-import Test.HUnit hiding (State)
-import Control.Eff
-import Control.Eff.Example
-import Control.Eff.Example.Test (ex2)
-import Control.Eff.Exception
-import Control.Eff.Lift
-import Control.Eff.Choose
-import Utils
-
-import Test.Framework.TH
-import Test.Framework.Providers.HUnit
-
-testGroups = [ $(testGroupGenerator) ]
-
-case_Choose1_exc11 :: Assertion
-case_Choose1_exc11 = [2,3] @=? (run exc11)
-  where
-    exc11 = makeChoice exc1
-    exc1 = return 1 `add` choose [1,2]
-
-case_Choose_ex2 :: Assertion
-case_Choose_ex2 =
-  let ex2_1 = run . makeChoice . runErrBig $ ex2 (choose [5,7,1])
-      ex2_2 = run . runErrBig . makeChoice $ ex2 (choose [5,7,1])
-  in
-    assertEqual "Choose: Combining exceptions and non-determinism: ex2_1"
-    expected1 ex2_1
-    >> assertEqual "Choose: Combining exceptions and non-determinism: ex2_2"
-    expected2 ex2_2
-  where
-    expected1 = [Right 5,Left (TooBig 7),Right 1]
-    expected2 = Left (TooBig 7)
-
-case_Choose_exRec :: Assertion
-case_Choose_exRec =
-  let exRec_1 = run . runErrBig . makeChoice $ exRec (ex2 (choose [5,7,1]))
-      exRec_2 = run . makeChoice . runErrBig $ exRec (ex2 (choose [5,7,1]))
-      exRec_3 = run . runErrBig . makeChoice $ exRec (ex2 (choose [5,7,11,1]))
-  in
-    assertEqual "Choose: error recovery: exRec_1" expected1 exRec_1
-    >> assertEqual "Choose: error recovery: exRec_2" expected2 exRec_2
-    >> assertEqual "Choose: error recovery: exRec_1" expected3 exRec_3
-  where
-    expected1 = Right [5,7,1]
-    expected2 = [Right 5,Right 7,Right 1]
-    expected3 = Left (TooBig 11)
-    -- Errror recovery part
-    -- The code is the same as in transf1.hs. The inferred signatures differ
-    -- Was: exRec :: MonadError TooBig m => m Int -> m Int
-    -- exRec :: Member (Exc TooBig) r => Eff r Int -> Eff r Int
-    exRec m = catchError m handler
-      where handler (TooBig n) | n <= 7 = return n
-            handler e = throwError e
-
-case_Choose_monadBaseControl :: Assertion
-case_Choose_monadBaseControl = runLift (makeChoice $ doThing $ choose [1,2,3]) @=? Just [1,2,3]
diff --git a/test/Control/Eff/Coroutine/Test.hs b/test/Control/Eff/Coroutine/Test.hs
--- a/test/Control/Eff/Coroutine/Test.hs
+++ b/test/Control/Eff/Coroutine/Test.hs
@@ -24,25 +24,25 @@
 case_Coroutines_c1 :: Assertion
 case_Coroutines_c1 = do
   ((), actual) <- catchOutput c1
-  assertEqual
+  assertOutput
     "Coroutine: Simple coroutines using Eff"
-    (unlines ["1", "2", "Done"]) actual
+    ["1", "2", "Done"] actual
   where
     th1 :: Member (Yield Int ()) r => Eff r ()
     th1 = yieldInt 1 >> yieldInt 2
 
     c1 = runTrace (loop =<< runC th1)
-      where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> k () >>= loop
             loop (Done)    = trace ("Done")
 
 case_Coroutines_c2 :: Assertion
 case_Coroutines_c2 = do
   ((), actual1) <- catchOutput c2
-  assertEqual "Coroutine: Add dynamic variables"
-    (unlines ["10", "10", "Done"]) actual1
+  assertOutput "Coroutine: Add dynamic variables"
+    ["10", "10", "Done"] actual1
   ((), actual2) <- catchOutput c21
-  assertEqual "Coroutine: locally changing the dynamic environment for the suspension"
-    (unlines ["10", "11", "Done"]) actual2
+  assertOutput "Coroutine: locally changing the dynamic environment for the suspension"
+    ["10", "11", "Done"] actual2
   where
     -- The code is essentially the same as that in transf.hs (only added
     -- a type specializtion on yield). The inferred signature is different though.
@@ -54,25 +54,25 @@
 
     -- Code is essentially the same as in transf.hs; no liftIO though
     c2 = runTrace $ runReader (10::Int) (loop =<< runC th2)
-      where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> k () >>= loop
             loop Done    = trace "Done"
 
     -- locally changing the dynamic environment for the suspension
     c21 = runTrace $ runReader (10::Int) (loop =<< runC th2)
-      where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
             loop Done    = trace "Done"
 
 case_Coroutines_c3 :: Assertion
 case_Coroutines_c3 = do
   ((), actual1) <- catchOutput c3
-  assertEqual "Coroutine: two sorts of local rebinding"
-    (unlines ["10", "10", "20", "20", "Done"]) actual1
+  assertOutput "Coroutine: two sorts of local rebinding"
+    ["10", "10", "20", "20", "Done"] actual1
   ((), actual2) <- catchOutput c31
-  let expected2 = (unlines ["10", "11", "21", "21", "Done"])
-  assertEqual "Coroutine: locally changing the dynamic environment for the suspension"
+  let expected2 = ["10", "11", "21", "21", "Done"]
+  assertOutput "Coroutine: locally changing the dynamic environment for the suspension"
     expected2 actual2
   ((), actual3) <- catchOutput c4
-  assertEqual "Coroutine: abstracting the client computation"
+  assertOutput "Coroutine: abstracting the client computation"
     expected2 actual3
   where
     th3 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
@@ -80,20 +80,20 @@
       where ay = ask >>= yieldInt
 
     c3 = runTrace $ runReader (10::Int) (loop =<< runC th3)
-      where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> k () >>= loop
             loop Done    = trace "Done"
 
     -- The desired result: the coroutine shares the dynamic environment with its
     -- parent; however, when the environment is locally rebound, it becomes
     -- private to coroutine.
     c31 = runTrace $ runReader (10::Int) (loop =<< runC th3)
-      where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
             loop Done    = trace "Done"
 
     -- We now make explicit that the client computation, run by th4,
     -- is abstract. We abstract it out of th4
     c4 = runTrace $ runReader (10::Int) (loop =<< runC (th4 client))
-      where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
             loop Done    = trace "Done"
 
             -- cl, client, ay are monomorphic bindings
@@ -104,25 +104,25 @@
 case_Corountines_c5 :: Assertion
 case_Corountines_c5 = do
   ((), actual) <- catchOutput c5
-  let expected = unlines ["10"
-                         ,"11"
-                         ,"12"
-                         ,"18"
-                         ,"18"
-                         ,"18"
-                         ,"29"
-                         ,"29"
-                         ,"29"
-                         ,"29"
-                         ,"29"
-                         ,"29"
-                         ,"Done"
-                         ]
-  assertEqual "Corountine: Even more dynamic example"
+  let expected = ["10"
+                 ,"11"
+                 ,"12"
+                 ,"18"
+                 ,"18"
+                 ,"18"
+                 ,"29"
+                 ,"29"
+                 ,"29"
+                 ,"29"
+                 ,"29"
+                 ,"29"
+                 ,"Done"
+                 ]
+  assertOutput "Corountine: Even more dynamic example"
     expected actual
   where
     c5 = runTrace $ runReader (10::Int) (loop =<< runC (th client))
-      where loop (Y x k) = trace (show (x::Int)) >> local (\_y->x+1) (k ()) >>= loop
+      where loop (Y k x) = trace (show (x::Int)) >> local (\_y->x+1) (k ()) >>= loop
             loop Done    = trace "Done"
 
             -- cl, client, ay are monomorphic bindings
@@ -139,32 +139,32 @@
 case_Coroutines_c7 :: Assertion
 case_Coroutines_c7 = do
   ((), actual) <- catchOutput c7
-  let expected = unlines ["1010"
-                         ,"1021"
-                         ,"1032"
-                         ,"1048"
-                         ,"1064"
-                         ,"1080"
-                         ,"1101"
-                         ,"1122"
-                         ,"1143"
-                         ,"1169"
-                         ,"1195"
-                         ,"1221"
-                         ,"1252"
-                         ,"1283"
-                         ,"1314"
-                         ,"1345"
-                         ,"1376"
-                         ,"1407"
-                         ,"Done"
-                         ]
-  assertEqual "Coroutine: And even more dynamic example"
+  let expected = ["1010"
+                 ,"1021"
+                 ,"1032"
+                 ,"1048"
+                 ,"1064"
+                 ,"1080"
+                 ,"1101"
+                 ,"1122"
+                 ,"1143"
+                 ,"1169"
+                 ,"1195"
+                 ,"1221"
+                 ,"1252"
+                 ,"1283"
+                 ,"1314"
+                 ,"1345"
+                 ,"1376"
+                 ,"1407"
+                 ,"Done"
+                 ]
+  assertOutput "Coroutine: And even more dynamic example"
     expected actual
   where
     c7 = runTrace $
           runReader (1000::Double) (runReader (10::Int) (loop =<< runC (th client)))
-     where loop (Y x k) = trace (show (x::Int)) >>
+     where loop (Y k x) = trace (show (x::Int)) >>
                           local (\_y->fromIntegral (x+1)::Double) (k ()) >>= loop
            loop Done    = trace "Done"
 
@@ -183,32 +183,32 @@
 case_Coroutines_c7' :: Assertion
 case_Coroutines_c7' = do
   ((), actual) <- catchOutput c7'
-  let expected = unlines ["1010"
-                         ,"1021"
-                         ,"1032"
-                         ,"1048"
-                         ,"1048"
-                         ,"1048"
-                         ,"1069"
-                         ,"1090"
-                         ,"1111"
-                         ,"1137"
-                         ,"1137"
-                         ,"1137"
-                         ,"1168"
-                         ,"1199"
-                         ,"1230"
-                         ,"1261"
-                         ,"1292"
-                         ,"1323"
-                         ,"Done"
-                         ]
-  assertEqual "Coroutine: And even more dynamic example"
+  let expected = ["1010"
+                 ,"1021"
+                 ,"1032"
+                 ,"1048"
+                 ,"1048"
+                 ,"1048"
+                 ,"1069"
+                 ,"1090"
+                 ,"1111"
+                 ,"1137"
+                 ,"1137"
+                 ,"1137"
+                 ,"1168"
+                 ,"1199"
+                 ,"1230"
+                 ,"1261"
+                 ,"1292"
+                 ,"1323"
+                 ,"Done"
+                 ]
+  assertOutput "Coroutine: And even more dynamic example"
     expected actual
   where
     c7' = runTrace $
           runReader (1000::Double) (runReader (10::Int) (loop =<< runC (th client)))
-     where loop (Y x k) = trace (show (x::Int)) >>
+     where loop (Y k x) = trace (show (x::Int)) >>
                           local (\_y->fromIntegral (x+1)::Double) (k ()) >>= loop
            loop Done    = trace "Done"
 
diff --git a/test/Control/Eff/Cut/Test.hs b/test/Control/Eff/Cut/Test.hs
deleted file mode 100644
--- a/test/Control/Eff/Cut/Test.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-module Control.Eff.Cut.Test (testGroups) where
-
-import Test.HUnit hiding (State)
-import Control.Eff
-import Control.Eff.Choose
-import Control.Eff.Cut
-
-import Test.Framework.TH
-import Test.Framework.Providers.HUnit
-
-testGroups = [ $(testGroupGenerator) ]
-
-case_Cut_tcut :: Assertion
-case_Cut_tcut =
-  let tcut1r = run . makeChoice $ call tcut1
-      tcut2r = run . makeChoice $ call tcut2
-      tcut3r = run . makeChoice $ call tcut3
-      tcut4r = run . makeChoice $ call tcut4
-  in
-    assertEqual "Cut: tcut1" [1,2] tcut1r
-    >> assertEqual "Cut: nested call: tcut2" [1,2,5] tcut2r
-    >> assertEqual "Cut: nested call: tcut3" [1,2,1,2,5] tcut3r
-    >> assertEqual "Cut: nested call: tcut4" [1,2,1,2,5] tcut4r
-  where
-    -- signature is inferred
-    -- tcut1 :: (Member Choose r, Member (Exc CutFalse) r) => Eff r Int
-    tcut1 = (return (1::Int) `mplus'` return 2) `mplus'`
-            ((cutfalse `mplus'` return 4) `mplus'`
-             return 5)
-    -- Here we see nested call. It poses no problems...
-    tcut2 = return (1::Int) `mplus'`
-            call (return 2 `mplus'` (cutfalse `mplus'` return 3) `mplus'`
-                  return 4)
-            `mplus'` return 5
-    tcut3 = call tcut1 `mplus'` call (tcut2 `mplus'` cutfalse)
-    tcut4 = call tcut1 `mplus'`  (tcut2 `mplus'` cutfalse)
diff --git a/test/Control/Eff/Exception/Test.hs b/test/Control/Eff/Exception/Test.hs
--- a/test/Control/Eff/Exception/Test.hs
+++ b/test/Control/Eff/Exception/Test.hs
@@ -9,7 +9,6 @@
 import Test.HUnit hiding (State)
 import Control.Eff
 import Control.Eff.Exception
-import Control.Eff.Lift
 import Control.Eff.Writer.Strict
 #if __GLASGOW_HASKELL__ < 710
 import Data.Monoid
diff --git a/test/Control/Eff/Fresh/Test.hs b/test/Control/Eff/Fresh/Test.hs
--- a/test/Control/Eff/Fresh/Test.hs
+++ b/test/Control/Eff/Fresh/Test.hs
@@ -6,8 +6,8 @@
 module Control.Eff.Fresh.Test (testGroups) where
 
 import Test.HUnit hiding (State)
+import Control.Eff
 import Control.Eff.Fresh
-import Control.Eff.Lift
 import Control.Eff.Trace
 import Utils
 
@@ -19,16 +19,16 @@
 case_Fresh_tfresh' :: Assertion
 case_Fresh_tfresh' = do
   ((), actual) <- catchOutput tfresh'
-  assertEqual "Fresh: test"
-    (unlines ["Fresh 0", "Fresh 1"]) actual
+  assertOutput "Fresh: test"
+    ["Fresh 0", "Fresh 1"] actual
   where
-    tfresh' = runTrace $ flip runFresh' 0 $ do
+    tfresh' = runTrace $ runFresh' 0 $ do
       n <- fresh
       trace $ "Fresh " ++ show n
       n <- fresh
       trace $ "Fresh " ++ show n
 
 case_Fresh_monadBaseControl :: Assertion
-case_Fresh_monadBaseControl = runLift (runFresh' (doThing $ fresh >> fresh) i) @=? Just (i + 1)
+case_Fresh_monadBaseControl = runLift (runFresh' i (doThing $ fresh >> fresh)) @=? Just (i + 1)
   where
     i = 0
diff --git a/test/Control/Eff/Lift/Test.hs b/test/Control/Eff/Lift/Test.hs
deleted file mode 100644
--- a/test/Control/Eff/Lift/Test.hs
+++ /dev/null
@@ -1,220 +0,0 @@
-{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, NoMonomorphismRestriction #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-module Control.Eff.Lift.Test (testGroups) where
-
-import Test.HUnit hiding (State)
-import Control.Eff
-import Control.Eff.Exception
-import Control.Eff.Lift
-import Control.Eff.Reader.Strict
-import Control.Eff.State.Strict
-import qualified Control.Exception as Exc
-import Data.Typeable
-import Utils
-
-import Test.Framework.TH
-import Test.Framework.Providers.HUnit
-
-testGroups = [ $(testGroupGenerator) ]
-
--- | Ensure that https://github.com/RobotGymnast/extensible-effects/issues/11 stays resolved.
-case_Lift_building :: Assertion
-case_Lift_building = runLift possiblyAmbiguous
-  where
-    possiblyAmbiguous :: (Monad m, SetMember Lift (Lift m) r) => Eff r ()
-    possiblyAmbiguous = lift $ return ()
-
-case_Lift_tl1r :: Assertion
-case_Lift_tl1r = do
-  ((), output) <- catchOutput tl1r
-  assertEqual "Test tl1r" (showLn input) output
-  where
-    input = (5::Int)
-    -- tl1r :: IO ()
-    tl1r = runLift (runReader input tl1)
-      where
-        tl1 = ask >>= \(x::Int) -> lift . print $ x
-
-case_Lift_tMd' :: Assertion
-case_Lift_tMd' = do
-  actual <- catchOutput tMd'
-  let expected = (output, (showLines input))
-  assertEqual "Test mapMdebug using Lift" expected actual
-  where
-    input = [1..5]
-    val = (10::Int)
-    output = map (+ val) input
-
-    tMd' = runLift $ runReader val $ mapMdebug' f input
-      where f x = ask `add` return x
-
-    -- Re-implemenation of mapMdebug using Lifting
-    -- The signature is inferred
-    mapMdebug'  :: (Show a, SetMember Lift (Lift IO) r) =>
-                   (a -> Eff r b) -> [a] -> Eff r [b]
-    mapMdebug' _f [] = return []
-    mapMdebug' f (h:t) = do
-      lift $ print h
-      h' <- f h
-      t' <- mapMdebug' f t
-      return (h':t')
-
--- tests from <http://okmij.org/ftp/Haskell/misc.html#catch-MonadIO>
-data MyException = MyException String deriving (Show, Typeable)
-instance Exc.Exception MyException
-
-exfn True = lift . Exc.throw $ (MyException "thrown")
-exfn False = return True
-
-testc m = catchDynE (m >>= return . show) (\ (MyException s) -> return s)
-
-case_catchDynE_test1 :: Assertion
-case_catchDynE_test1 = do
-  ((), actual) <- catchOutput test1
-  let expected = unlines [ "(\"thrown\",[\"begin\"])"
-                         , "(\"True\",[\"end\",\"begin\"])"]
-  assertEqual "catchDynE: test1: exception shouldn't drop Writer's state"
-    expected actual
-  where
-    -- In CatchMonadIO, the result of tf True is ("thrown",[]) --
-    -- that is, an exception will drop the Writer's state, even if that
-    -- exception is caught. Here, the state is preserved!
-    -- So, this is an advantage over MTL!
-    test1 = do runLift (tf True) >>= print; runLift (tf False) >>= print
-    tf x = runReader (x::Bool) . runState ([]::[String]) $ testc m
-    m = do
-      modify ("begin":)
-      x <- ask
-      r <- exfn x
-      modify ("end":)
-      return r
-
--- Let us use an Error effect instead
-case_catchDynE_test1' :: Assertion
-case_catchDynE_test1' = do
-  ((), actual') <- catchOutput test1'
-  let expected' = unlines [ "(Left \"thrown\",[\"begin\"])"
-                         , "(Right \"True\",[\"end\",\"begin\"])"]
-  assertEqual "catchDynE: test1': Error shouldn't drop Writer's state"
-    expected' actual'
-  where
-    -- In CatchMonadIO, the result of tf True is ("thrown",[]) --
-    -- that is, an exception will drop the Writer's state, even if that
-    -- exception is caught. Here, the state is preserved!
-    -- So, this is an advantage over MTL!
-    test1' = do runLift (tf True) >>= print; runLift (tf False) >>= print
-    tf x = runReader (x::Bool) . runState ([]::[String]) $ runErrorStr (testc m)
-    m = do
-      modify ("begin":)
-      x <- ask
-      r <- exfn x
-      modify ("end":)
-      return r
-
-    runErrorStr = asEStr . runError
-    asEStr :: m (Either String a) -> m (Either String a)
-    asEStr = id
-    exfn True = throwError $ ("thrown")
-    exfn False = return True
-
--- Now, the behavior of the dynamic Exception and Error effect is consistent.
--- The state is preserved. Before it wasn't.
-case_catchDynE_test2 :: Assertion
-case_catchDynE_test2 = do
-  ((), actual) <- catchOutput test2
-  let expected = unlines [ "(Left \"thrown\",[\"begin\"])"
-                         , "(Right \"True\",[\"end\",\"begin\"])"]
-  assertEqual "catchDynE: test2: Error shouldn't drop Writer's state"
-    expected actual
-  where
-    test2 = do runLift (tf True) >>= print; runLift (tf False) >>= print
-    tf x = runReader (x::Bool) . runState ([]::[String]) $ runErrorStr (testc m)
-    runErrorStr = asEStr . runError
-    asEStr :: m (Either String a) -> m (Either String a)
-    asEStr = id
-    m = do
-      modify ("begin":)
-      x <- ask
-      r <- exfn x `catchDynE` (\ (MyException s) -> throwError s)
-      modify ("end":)
-      return r
-
--- Full recovery
-case_catchDynE_test2' :: Assertion
-case_catchDynE_test2' = do
-  ((), actual) <- catchOutput test2'
-  let expected = unlines [ "(Right \"False\",[\"end\",\"begin\"])"
-                         , "(Right \"True\",[\"end\",\"begin\"])"]
-  assertEqual "catchDynE: test2': Fully recover from errors"
-    expected actual
-  where
-    test2' = do runLift (tf True) >>= print; runLift (tf False) >>= print
-    tf x = runReader (x::Bool) . runState ([]::[String]) $ runErrorStr (testc m)
-    runErrorStr = asEStr . runError
-    asEStr :: m (Either String a) -> m (Either String a)
-    asEStr = id
-    m = do
-      modify ("begin":)
-      x <- ask
-      r <- exfn x `catchDynE` (\ (MyException _s) -> return False)
-      modify ("end":)
-      return r
-
--- Throwing within a handler
-case_catchDynE_test3 :: Assertion
-case_catchDynE_test3 = do
-  ((), actual) <- catchOutput test3
-  let expected = unlines [ "(Right \"rethrow:thrown\",[\"begin\"])"
-                         , "(Right \"True\",[\"end\",\"begin\"])"]
-  assertEqual "catchDynE: test3: Throwing within a handler"
-    expected actual
-  where
-    test3 = do runLift (tf True) >>= print; runLift (tf False) >>= print
-    tf x = runReader (x::Bool) . runState ([]::[String]) $ runErrorStr (testc m)
-    runErrorStr = asEStr . runError
-    asEStr :: m (Either String a) -> m (Either String a)
-    asEStr = id
-    m = do
-      modify ("begin":)
-      x <- ask
-      r <- exfn x `catchDynE` (\ (MyException s) ->
-                                 lift . Exc.throw . MyException $
-                                 ("rethrow:" ++ s))
-      modify ("end":)
-      return r
-
--- Implement the transactional behavior: when the exception is raised,
--- the state is rolled back to what it existed at the entrance to
--- the catch block.
--- This is the ``scoping behavior'' of `Handlers in action'
-case_catchDynE_tran :: Assertion
-case_catchDynE_tran = do
-  ((), actual) <- catchOutput tran
-  let expected = unlines ["(\"thrown\",[\"init\"])"
-                         ,"(\"True\",[\"end\",\"begin\",\"init\"])"]
-  assertEqual "catchDynE: tran: Transactional behaviour"
-    expected actual
-  where
-    tran = do runLift (tf True) >>= print; runLift (tf False) >>= print
-    tf x = runReader (x :: Bool) . runState ([]::[String]) $ m1
-    m1 = do
-      modify ("init":)
-      testc (transactionState (TxState :: TxState [String]) m)
-    m = do
-      modify ("begin":)
-      x <- ask
-      r <- exfn x
-      modify ("end":)
-      return r
-{- -- without transaction
-("thrown",["begin","init"])
-("True",["end","begin","init"])
--}
-
--- With transaction
-{-
-("thrown",["init"])
-("True",["end","begin","init"])
--}
diff --git a/test/Control/Eff/Logic/NDet/Bench.hs b/test/Control/Eff/Logic/NDet/Bench.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Eff/Logic/NDet/Bench.hs
@@ -0,0 +1,340 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DataKinds #-}
+
+-- A benchmark of shift/reset: Filinski's representing non-determinism monads
+--
+--  The benchmark is taken from Sec 6.1 of
+--    Martin Gasbichler, Michael Sperber: Final Shift for Call/cc: Direct
+--    Implementation of Shift and Reset, ICFP'02, pp. 271-282. 
+--    http://www-pu.informatik.uni-tuebingen.de/users/sperber/papers/shift-reset-direct.pdf
+-- This code is a straightforward translation of bench_nondet.ml
+--
+-- This is a micro-benchmark: it is very non-determinism-intensive. It is
+-- *not* representative: the benchmark does nothing else but
+-- concatenates lists. The List monad does this directly; whereas
+-- continuation monads do the concatenation with more overhead (e.g.,
+-- building the closures representing continuations). Therefore,
+-- the List monad here outperforms all other implementations of 
+-- non-determinism.
+-- It should be stressed that the delimited control is optimized
+-- for the case where control operations are infrequent, so we pay
+-- as we go. The use of the delimited control operators is more
+-- expensive, but the code that does not use delimited control does not
+-- have to pay anything for delimited control. 
+-- Again, in the present micro-benchmark, there is hardly any code that
+-- does not use non-determinism, so the overhead of delimited control
+-- is very noticeable. That is why this benchmark is good at estimating
+-- the overhead of different implementations of delimited control.
+
+-- To compile this code
+-- ghc -O2 -rtsopts -main-is Bench_nondet.main_list5 Bench_nondet.hs
+-- To run this code
+-- GHCRTS="-tstderr" /usr/bin/time ./Bench_nondet
+
+module Control.Eff.Logic.NDet.Bench where
+
+import Control.Eff
+import qualified Control.Eff.Logic.NDet as E
+
+import Data.List (sort)
+-- import Control.Monad.Identity
+-- import Control.Monad (liftM2)
+import Control.Monad (MonadPlus(..), msum)
+import Control.Applicative
+-- import System.CPUTime
+
+-- Small language with non-determinism: just like the one in our DSL-WC paper
+
+int :: MonadPlus repr => Int -> repr Int
+int x = return x
+
+add :: MonadPlus repr => repr Int -> repr Int -> repr Int
+-- add xs ys = liftM2 (+) xs ys
+add xs ys = do {x <- xs; y <- ys; return $! x+y }
+
+lam :: MonadPlus repr => (repr a -> repr b) -> repr (a -> repr b)
+lam f = return $ f . return
+
+app :: MonadPlus repr => repr (a -> repr b) -> (repr a -> repr b)
+app xs ys = do {x <- xs; y <- ys; x y}
+
+amb :: MonadPlus repr => [repr Int] -> repr Int
+amb = msum
+
+-- Benchmark cases
+
+test_ww :: MonadPlus repr => repr Int
+test_ww = 
+ let f = lam (\x ->
+              add (add x (amb [int 6, int 4, int 2, int 8])) 
+                         (amb [int 2, int 4, int 5, int 4, int 1]))
+ in f `app` amb [int 0, int 2, int 3, int 4, int 5, int 32]
+
+ww_answer = 
+ sort [8, 10, 11, 10, 7, 6, 8, 9, 8, 5, 4, 6, 7, 6, 3, 10, 12, 13,
+       12, 9, 10, 12, 13, 12, 9, 8, 10, 11, 10, 7, 6, 8, 9, 8, 5, 12, 14, 15,
+       14, 11, 11, 13, 14, 13, 10, 9, 11, 12, 11, 8, 7, 9, 10, 9, 6, 13, 15,
+       16, 15, 12, 12, 14, 15, 14, 11, 10, 12, 13, 12, 9, 8, 10, 11, 10, 7,
+       14, 16, 17, 16, 13, 13, 15, 16, 15, 12, 11, 13, 14, 13, 10, 9, 11, 12,
+       11, 8, 15, 17, 18, 17, 14, 40, 42, 43, 42, 39, 38, 40, 41, 40, 37, 36,
+       38, 39, 38, 35, 42, 44, 45, 44, 41]
+
+-- Real benchmark cases
+
+test_www :: MonadPlus repr => repr Int
+test_www = 
+ let f = lam (\x ->
+              add (add x (amb [int 6, int 4, int 2, int 8])) 
+                         (amb [int 2, int 4, int 5, int 4, int 1]))
+ in f `app` (f `app` amb [int 0, int 2, int 3, int 4, int 5, int 32])
+
+test_wwww :: MonadPlus repr => repr Int
+test_wwww = 
+ let f = lam (\x ->
+              add (add x (amb [int 6, int 4, int 2, int 8])) 
+                         (amb [int 2, int 4, int 5, int 4, int 1]))
+ in f `app` (f `app` (f `app` amb [int 0, int 2, int 3, int 4, int 5, int 32]))
+
+test_w5 :: MonadPlus repr => repr Int
+test_w5 = 
+ let f = lam (\x ->
+              add (add x (amb [int 6, int 4, int 2, int 8])) 
+                         (amb [int 2, int 4, int 5, int 4, int 1]))
+ in f `app` (f `app` 
+     (f `app` (f `app` amb [int 0, int 2, int 3, int 4, int 5, int 32])))
+
+
+-- Different implementations of our language (MonadPlus)
+
+-- The List monad: Non-determinism monad as a list of successes
+
+run_list :: [Int] -> [Int]
+run_list = id
+
+testl1 = (==) [101, 201, 102, 202] . run_list $
+         add (amb [int 1, int 2]) (amb [int 100, int 200])
+
+testl2 = ww_answer == sort (run_list test_ww)
+
+
+-- CPS-monad, implemented by hand; it must be quite efficient therefore
+-- It is a monad, not a transformer. It cannot do any other effects beside
+-- the non-determinism.
+newtype CPS a = CPS{unCPS:: (a -> [Int]) -> [Int]}
+
+instance Functor CPS where
+  fmap f fa = CPS $ \k -> unCPS fa (k . f)
+instance Applicative CPS where
+  pure x = CPS $ \k -> k x
+  mf <*> fa = CPS $ \k -> unCPS mf (\f -> unCPS fa (k . f))
+instance Monad CPS where
+  return x = CPS $ \k -> k x
+  m >>= f  = CPS $ \k -> unCPS m (\a -> unCPS (f a) k)
+
+instance Alternative CPS where
+  empty = mzero
+  (<|>) = mplus
+instance MonadPlus CPS where
+  mzero = CPS $ \_ -> []
+  mplus m1 m2 = CPS $ \k -> unCPS m1 k ++ unCPS m2 k
+
+run_cps :: CPS Int -> [Int]
+run_cps m = unCPS m (\x -> [x])
+
+
+testc1 = (==) [101, 201, 102, 202] . run_cps $
+         add (amb [int 1, int 2]) (amb [int 100, int 200])
+
+testc2 = ww_answer == sort (run_cps test_ww)
+
+-- ExtEff implementation
+-- Eff is already an instance of MonadPlus. Thus we only need to
+-- define the run instance
+
+-- run_eff :: Eff '[E.Choose] Int -> [Int]
+-- run_eff = run . E.makeChoice
+
+-- More direct interpreter
+-- makeChoiceA :: Eff (E.NDet ': r) a -> Eff r [a]
+-- makeChoiceA = handle_relay (\x -> x `seq` return [x] ) $ \m k -> case m of
+--     E.MZero -> return []
+--     E.MPlus -> liftM2 (++) (k True) (k False)
+
+run_eff :: Eff '[E.NDet] Int -> [Int]
+run_eff = run . E.makeChoiceA
+
+teste2 = ww_answer == sort (run_eff test_ww)
+
+
+data Count a = Count (Maybe a) !Int
+instance Functor Count where
+  fmap f (Count (Just x) n) = Count (Just (f x)) n
+  fmap _ _                  = Count Nothing 0
+  
+instance Applicative Count where
+  pure x = Count (Just x) 1
+  Count (Just f) nf <*> Count (Just x) nx = Count (Just (f x)) (nf + nx)
+  _ <*> _  = Count Nothing 0
+  
+instance Alternative Count where
+  empty = Count Nothing 0
+  Count m1@Just{} n1 <|> Count _ n2 = Count m1 (n1+n2)
+  _ <|> m2 = m2
+
+run_effc :: Eff '[E.NDet] Int -> Int
+run_effc m = let Count _ n = run . E.makeChoiceA $ m in n
+
+  
+teste12 = length ww_answer == run_effc test_ww
+
+{-
+-- CCEx monad
+-- Not a very optimal implementation of mplus (a tree would be better)
+-- But is suffices as a benchmark of different implementations of CC
+instance Monad m => MonadPlus (CC (PS [Int]) m) where
+    mzero = abortP ps (return [])
+    mplus m1 m2 = takeSubCont ps (\k ->
+                     liftM2 (++)
+                       (pushPrompt ps (pushSubCont k m1))
+                       (pushPrompt ps (pushSubCont k m2)))
+
+run_dir :: CC (PS [Int]) Identity Int -> [Int]
+run_dir m = runIdentity . runCC $
+            pushPrompt ps (m >>= return . (:[]))
+
+
+testd1 = (==) [101, 201, 102, 202] . run_dir $
+         add (amb [int 1, int 2]) (amb [int 100, int 200])
+
+testd2 = ww_answer == sort (run_dir test_ww)
+
+-}
+
+
+-- Benchmarks themselves
+
+main_list3 = print $ 2400   == (length . run_list $ test_www)
+main_list4 = print $ 48000  == (length . run_list $ test_wwww)
+main_list5 = print $ 960000 == (length . run_list $ test_w5)
+
+main_cps3 = print $ 2400   == (length . run_cps $ test_www)
+main_cps4 = print $ 48000  == (length . run_cps $ test_wwww)
+main_cps5 = print $ 960000 == (length . run_cps $ test_w5)
+
+-- We expect the direct implementation to be slower since CC is the transformer,
+-- whereas CPS is not. The latter is hand-written for a specific answer-type.
+main_eff3 = print $ 2400   == (length . run_eff $ test_www)
+main_eff4 = print $ 48000  == (length . run_eff $ test_wwww)
+main_eff5 = print $ 960000 == (length . run_eff $ test_w5)
+
+main_eff5c = print $ 960000 == (run_effc $ test_w5)
+
+-- To clarify the effect of building a list
+main_eff5m = print $ ((run . E.makeChoiceA $ test_w5) :: Maybe Int)
+
+{-
+-- Instantiate CC to the IO as the base monad, attempting to quantify the
+-- effect of the Identity transformer
+main_dir5io = do
+              l <- runCC $ pushPrompt ps (test_w5 >>= return . (:[]))
+              print $ length l == 960000
+-}
+
+-- ------------------------------------------------------------------------
+-- Old results, from 2010
+
+{- Median of 5 runs
+
+main_list5
+<<ghc: 186526764 bytes, 356 GCs, 619182/1156760 avg/max bytes residency (3 samples), 4M in use, 0.00 INIT (0.00 elapsed), 0.25 MUT (0.25 elapsed), 0.06 GC (0.06 elapsed) :ghc>>
+        0.30 real         0.30 user         0.00 sys
+
+main_cps5
+<<ghc: 231580040 bytes, 442 GCs, 4017/4104 avg/max bytes residency (24 samples), 2M in use, 0.00 INIT (0.00 elapsed), 0.28 MUT (0.28 elapsed), 0.31 GC (0.33 elapsed) :ghc>>
+        0.60 real         0.58 user         0.01 sys
+
+main_dir5 (CCExc implementation)
+<<ghc: 780415108 bytes, 1489 GCs, 10459973/39033060 avg/max bytes residency (14 samples), 110M in use, 0.00 INIT (0.00 elapsed), 1.30 MUT (1.32 elapsed), 2.92 GC (3.14 elapsed) :ghc>>
+        4.48 real         4.22 user         0.24 sys
+
+main_dir5io (CCExc implementation)
+<<ghc: 1148031880 bytes, 2190 GCs, 10339954/38941944 avg/max bytes residency (14 samples), 108M in use, 0.00 INIT (0.00 elapsed), 2.15 MUT (2.20 elapsed), 3.04 GC (3.24 elapsed) :ghc>>
+        5.45 real         5.18 user         0.21 sys
+
+
+main_dir5 (CCCxe implementation)
+./Bench_nondet +RTS -tstderr 
+True
+<<ghc: 991065016 bytes, 1891 GCs, 10473968/38790660 avg/max bytes residency (14 samples), 110M in use, 0.00 INIT (0.00 elapsed), 1.45 MUT (1.49 elapsed), 2.99 GC (3.20 elapsed) :ghc>>
+        4.70 real         4.44 user         0.23 sys
+
+main_dir5io (CCCxe implementation)
+./Bench_nondet +RTS -tstderr 
+True
+<<ghc: 991065412 bytes, 1891 GCs, 10364029/37920012 avg/max bytes residency (14 samples), 109M in use, 0.00 INIT (0.00 elapsed), 1.46 MUT (1.50 elapsed), 2.99 GC (3.20 elapsed) :ghc>>
+        4.72 real         4.44 user         0.23 sys
+
+main_ref5io (without pushDelimSubCont)
+./Bench_nondet +RTS -tstderr 
+True
+<<ghc: 19050261764 bytes, 36337 GCs, 10620542/49328200 avg/max bytes residency (16 samples), 123M in use, 0.00 INIT (0.00 elapsed), 61.45 MUT (62.70 elapsed), 6.06 GC (6.21 elapsed) :ghc>>
+       68.94 real        67.51 user         1.03 sys
+
+
+main_ref5io (with pushDelimSubCont)
+./Bench_nondet +RTS -tstderr 
+True
+<<ghc: 5666546308 bytes, 10809 GCs, 10538302/46414760 avg/max bytes residency (14 samples), 114M in use, 0.00 INIT (0.00 elapsed), 16.27 MUT (16.68 elapsed), 3.65 GC (3.80 elapsed) :ghc>>
+       20.50 real        19.92 user         0.46 sys
+
+-}
+
+-- ------------------------------------------------------------------------
+-- Newer Benchmarks, July 2015
+
+{-
+main_list5
+True
+<<ghc: 374751856 bytes, 720 GCs, 939265/2386984 avg/max bytes residency (6 samples), 7M in use, 0.00 INIT (0.00 elapsed), 0.11 MUT (0.11 elapsed), 0.02 GC (0.02 elapsed) :ghc>>
+
+main_cps5
+True
+<<ghc: 463450920 bytes, 889 GCs, 36708/44312 avg/max bytes residency (2 samples), 1M in use, 0.00 INIT (0.00 elapsed), 0.14 MUT (0.15 elapsed), 0.00 GC (0.01 elapsed) :ghc>>
+
+-- using makeChoiceA (setting f as an Alternative)
+main_eff5
+True
+<<ghc: 1013337072 bytes, 1944 GCs, 18671465/83300976 avg/max bytes residency (17 samples), 231M in use, 0.00 INIT (0.00 elapsed), 0.36 MUT (0.39 elapsed), 1.08 GC (1.13 elapsed) :ghc>>
+
+With strict add:
+True
+<<ghc: 993935088 bytes, 1906 GCs, 15000238/77154800 avg/max bytes residency (19 samples), 199M in use, 0.00 INIT (0.00 elapsed), 0.37 MUT (0.39 elapsed), 0.95 GC (1.02 elapsed) :ghc>>
+1.32user 0.08system 0:01.40elapsed 99%CPU (0avgtext+0avgdata 819408maxresident)k
+0inputs+0outputs (0major+51485minor)pagefaults 0swaps
+
+It looks like a huge memory leak. Perhaps the list is fully realized?
+
+
+Using the counting Alternative Count
+True
+<<ghc: 591341472 bytes, 1133 GCs, 16603280/76447176 avg/max bytes residency (10 samples), 162M in use, 0.00 INIT (0.00 elapsed), 0.28 MUT (0.28 elapsed), 0.61 GC (0.66 elapsed) :ghc>>
+
+Using Maybe
+Just 32
+<<ghc: 523838824 bytes, 1003 GCs, 16969712/76447176 avg/max bytes residency (9 samples), 150M in use, 0.00 INIT (0.00 elapsed), 0.21 MUT (0.19 elapsed), 0.46 GC (0.52 elapsed) :ghc>>
+0.67user 0.05system 0:00.72elapsed 100%CPU (0avgtext+0avgdata 620752maxresident)k
+0inputs+0outputs (0major+38937minor)pagefaults 0swaps
+
+-- using Maybe, but with the better makeChoice
+Just 32
+<<ghc: 517460016 bytes, 883 GCs, 20215861/91552144 avg/max bytes residency (9 samples), 138M in use, 0.00 INIT (0.00 elapsed), 0.22 MUT (0.24 elapsed), 0.41 GC (0.43 elapsed) :ghc>>
+0.63user 0.04system 0:00.68elapsed 100%CPU (0avgtext+0avgdata 570720maxresident)k
+0inputs+0outputs (0major+35760minor)pagefaults 0swaps
+
+Better makeChoiceA, full list
+True
+<<ghc: 454475112 bytes, 839 GCs, 8700298/33304904 avg/max bytes residency (8 samples), 58M in use, 0.00 INIT (0.00 elapsed), 0.23 MUT (0.23 elapsed), 0.19 GC (0.20 elapsed) :ghc>>
+0.42user 0.02system 0:00.44elapsed 100%CPU (0avgtext+0avgdata 244064maxresident)k
+0inputs+0outputs (0major+15391minor)pagefaults 0swaps
+
+-}
diff --git a/test/Control/Eff/Logic/NDet/Test.hs b/test/Control/Eff/Logic/NDet/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Eff/Logic/NDet/Test.hs
@@ -0,0 +1,191 @@
+{-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-}
+{-# LANGUAGE TypeOperators, DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Control.Eff.Logic.NDet.Test (testGroups, gen_testCA, gen_ifte_test)
+where
+
+import Test.HUnit hiding (State)
+import Control.Applicative
+import Control.Eff
+import Control.Eff.Example
+import Control.Eff.Example.Test (ex2)
+import Control.Eff.Exception
+import Control.Eff.Logic.NDet
+import Control.Eff.Writer.Strict
+import Control.Monad (msum, guard, mzero, mplus)
+import Control.Eff.Logic.Test
+import Utils
+
+import Test.Framework.TH
+import Test.Framework.Providers.HUnit
+
+testGroups = [ $(testGroupGenerator) ]
+
+gen_testCA :: (Integral a) => a -> Eff (NDet ': r) a
+gen_testCA x = do
+  i <- msum . fmap return $ [1..x]
+  guard (i `mod` 2 == 0)
+  return i
+
+case_NDet_testCA :: Assertion
+case_NDet_testCA = [2, 4..10] @=? (run $ makeChoiceA (gen_testCA 10))
+
+case_Choose1_exc11 :: Assertion
+case_Choose1_exc11 = [2,3] @=? (run exc11)
+  where
+    exc11 = makeChoice exc1
+    exc1 = return 1 `add` choose [1,2]
+
+case_Choose_exRec :: Assertion
+case_Choose_exRec =
+  let exRec_1 = run . runErrBig . makeChoice $ exRec (ex2 (choose [5,7,1]))
+      exRec_2 = run . makeChoice . runErrBig $ exRec (ex2 (choose [5,7,1]))
+      exRec_3 = run . runErrBig . makeChoice $ exRec (ex2 (choose [5,7,11,1]))
+      exRec_4 = run . makeChoice . runErrBig $ exRec (ex2 (choose [5,7,11,1]))
+  in
+    assertEqual "Choose: error recovery: exRec_1" expected1 exRec_1
+    >> assertEqual "Choose: error recovery: exRec_2" expected2 exRec_2
+    >> assertEqual "Choose: error recovery: exRec_3" expected3 exRec_3
+    >> assertEqual "Choose: error recovery: exRec_4" expected4 exRec_4
+  where
+    expected1 = Right [5,7,1]
+    expected2 = [Right 5,Right 7,Right 1]
+    expected3 = Left (TooBig 11)
+    expected4 = [Right 5,Right 7,Left (TooBig 11),Right 1]
+    -- Errror recovery part
+    -- The code is the same as in transf1.hs. The inferred signatures differ
+    -- Was: exRec :: MonadError TooBig m => m Int -> m Int
+    -- exRec :: Member (Exc TooBig) r => Eff r Int -> Eff r Int
+    exRec m = catchError m handler
+      where handler (TooBig n) | n <= 7 = return n
+            handler e = throwError e
+
+case_Choose_ex2 :: Assertion
+case_Choose_ex2 =
+  let ex2_1 = run . makeChoice . runErrBig $ ex2 (choose [5,7,1])
+      ex2_2 = run . runErrBig . makeChoice $ ex2 (choose [5,7,1])
+  in
+    assertEqual "Choose: Combining exceptions and non-determinism: ex2_1"
+    expected1 ex2_1
+    >> assertEqual "Choose: Combining exceptions and non-determinism: ex2_2"
+    expected2 ex2_2
+  where
+    expected1 = [Right 5,Left (TooBig 7),Right 1]
+    expected2 = Left (TooBig 7)
+
+gen_ifte_test x = do
+  n <- gen x
+  ifte (do
+           d <- gen x
+           guard $ d < n && n `mod` d == 0
+           -- _ <- trace ("d: " ++ show d) (return ())
+       )
+    (\_ -> mzero)
+    (return n)
+    where gen x = msum . fmap return $ [2..x]
+
+
+case_NDet_ifte :: Assertion
+case_NDet_ifte =
+  let primes = ifte_test_run
+  in
+    assertEqual "NDet: test ifte using primes"
+    [2,3,5,7,11,13,17,19,23,29] primes
+  where
+    ifte_test_run :: [Int]
+    ifte_test_run = run . makeChoiceA $ (gen_ifte_test 30)
+
+
+-- called reflect in the LogicT paper
+case_NDet_reflect :: Assertion
+case_NDet_reflect =
+  let tsplitr10 = run $ runListWriter $ makeChoiceA tsplit
+      tsplitr11 = run $ runListWriter $ makeChoiceA (msplit tsplit >>= reflect)
+      tsplitr20 = run $ makeChoiceA $ runListWriter tsplit
+      tsplitr21 = run $ makeChoiceA $ runListWriter (msplit tsplit >>= reflect)
+  in
+    assertEqual "tsplitr10" expected1 tsplitr10
+    >> assertEqual "tsplitr11" expected1 tsplitr11
+    >> assertEqual "tsplitr20" expected2 tsplitr20
+    >> assertEqual "tsplitr21" expected21 tsplitr21
+  where
+    expected1 = ([1, 2],["begin", "end"])
+    expected2 = [(1, ["begin"]), (2, ["end"])]
+    expected21 = [(1, ["begin"]), (2, ["begin", "end"])]
+
+    tsplit =
+      (tell "begin" >> return 1) `mplus`
+      (tell "end"   >> return 2)
+
+case_NDet_monadBaseControl :: Assertion
+case_NDet_monadBaseControl = runLift (makeChoiceA $ doThing (return 1 <|> return 2)) @=? Just [1,2]
+
+case_Choose_monadBaseControl :: Assertion
+case_Choose_monadBaseControl = runLift (makeChoice $ doThing $ choose [1,2,3]) @=? Just [1,2,3]
+
+case_NDet_cut :: Assertion
+case_NDet_cut = testCut (run . makeChoice)
+
+case_NDet_monadplus :: Assertion
+case_NDet_monadplus =
+  let evalnw = run . (runListWriter @Int) . makeChoice
+      evalwn = run . makeChoice . (runListWriter @Int)
+      casesnw = [
+        -- mplus laws
+          ("0             | NDet, Writer", evalnw t0, nw0)
+        , ("zm0     = 0   | NDet, Writer", evalnw tzm0, nw0)
+        , ("0m1           | NDet, Writer", evalnw t0m1, nw0m1)
+        , ("zm0mzm1 = 0m1 | NDet, Writer", evalnw tzm0mzm1, nw0m1)
+        -- mzero laws
+        , ("z         | NDet, Writer", evalnw tz, nwz)
+        , ("z0    = z | NDet, Writer", evalnw tz0, nwz)
+        , ("0z   /= z | NDet, Writer", evalnw t0z, nw0z)
+        , ("z0m1  = 1 | NDet, Writer", evalnw tz0m1, nw1)
+        , ("0zm1 /= 1 | NDet, Writer", evalnw t0zm1, nw0zm1)
+        ]
+      caseswn = [
+        -- mplus laws
+          ("0             | Writer, NDet", evalwn t0, wn0)
+        , ("zm0     = 0   | Writer, NDet", evalwn tzm0, wn0)
+        , ("0m1           | Writer, NDet", evalwn t0m1, wn0m1)
+        , ("zm0mzm1 = 0m1 | Writer, NDet", evalwn tzm0mzm1, wn0m1)
+        -- mzero laws
+        , ("z        | Writer, NDet", evalwn tz, wnz)
+        , ("z0   = z | Writer, NDet", evalwn tz0, wnz)
+        , ("0z   = z | Writer, NDet", evalwn t0z, wnz)
+        , ("z0m1 = 1 | Writer, NDet", evalwn tz0m1, wn1)
+        , ("0zm1 = 1 | Writer, NDet", evalwn t0zm1, wn1)
+        ]
+  in runAsserts assertEqual casesnw
+  >> runAsserts assertEqual caseswn
+  where
+    nwz = ([]::[Int],[])
+    wnz = [] ::[(Int, [Int])]
+    nw0z = ([]::[Int],[0])
+    nw0 = ([0],[0])
+    nw1 = ([1],[1])
+    nw0zm1 = ([1],[0,1])
+    wn0 = [(0,[0])]
+    wn1 = [(1,[1])]
+
+    nw0m1 = ([0::Int,1],[0,1])
+    wn0m1 = [(0,[0]), (1,[1])]
+
+    t0 = wr @Int 0
+    t1 = wr @Int 1
+
+    tz = mzero
+    tz0 = tz >> t0
+    t0z = t0 >> tz
+    tz0m1 = tz0 `mplus` t1
+    t0zm1 = t0z `mplus` t1
+
+    t0m1 = t0 `mplus` t1
+    tzm0 = tz `mplus` t0
+    tzm1 = tz `mplus` t1
+    tzm0mzm1 = tzm0 `mplus` tzm1
+
+    wr :: forall a r. [Writer a, NDet] <:: r => a -> Eff r a
+    wr i = tell i >> return i
diff --git a/test/Control/Eff/Logic/Test.hs b/test/Control/Eff/Logic/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Control/Eff/Logic/Test.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Control.Eff.Logic.Test where
+
+import Test.HUnit hiding (State)
+import Control.Eff.Logic.Core
+import Control.Monad
+
+-- the inferred signature of testCut is insightful
+testCut runChoice =
+  let cases = [tcut1, tcut2, tcut3, tcut4, tcut5, tcut6, tcut7, tcut8
+              , tcut9]
+      runCall = runChoice . call
+  in
+    forM_ cases $ \(test, result) ->
+                    assertEqual "Cut: tcut" result (runCall test)
+  where
+    -- signature is inferred
+    -- tcut1 :: (Member Choose r, Member (Exc CutFalse) r) => Eff r Int
+    tc1 = (return (1::Int) `mplus` return 2) `mplus`
+          ((cutfalse `mplus` return 4) `mplus`
+            return 5)
+    rc1 = [1,2]
+    tcut1 = (tc1, rc1)
+    -- Here we see nested call. It poses no problems...
+    tc2 = return (1::Int) `mplus`
+          call (return 2 `mplus` (cutfalse `mplus` return 3) `mplus`
+                 return 4)
+          `mplus` return 5
+    rc2 = [1,2,5]
+    tcut2 = (tc2, rc2)
+    tcut3 = ((call tc1 `mplus` call (tc2 `mplus` cutfalse))
+            , rc1 ++ rc2)
+    tcut4 = ((call tc1 `mplus`  (tc2 `mplus` cutfalse))
+            , rc1 ++ rc2)
+    tcut5 = ((call tc1 `mplus`  (cutfalse `mplus` tc2))
+            , rc1)
+    tcut6 = ((call tc1 `mplus` call (cutfalse `mplus` tc2))
+            , rc1)
+    tcut7 = ((call tc1 `mplus`  (cutfalse `mplus` tc2) `mplus` tc2)
+            , rc1)
+    tcut8 = ((call tc1 `mplus` call (cutfalse `mplus` tc2) `mplus` tc2)
+            , rc1 ++ rc2)
+    incrOrDecr = \x -> (return $! x + 1)
+                       `mplus` cutfalse
+                       `mplus` (return $! x - 1)
+    tc9 = tc1 >>= incrOrDecr
+    rc9 = [2]
+    tcut9 = (tc9, rc9)
+    -- tcut10 = ((return rc1 >>= incrOrDecr)
+    --          , rc9)
diff --git a/test/Control/Eff/NdetEff/Test.hs b/test/Control/Eff/NdetEff/Test.hs
deleted file mode 100644
--- a/test/Control/Eff/NdetEff/Test.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-}
-{-# LANGUAGE TypeOperators, DataKinds #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-module Control.Eff.NdetEff.Test (testGroups) where
-
-import Test.HUnit hiding (State)
-import Control.Applicative
-import Control.Eff
-import Control.Eff.Lift
-import Control.Eff.NdetEff
-import Control.Eff.Writer.Strict
-import Control.Monad (msum, guard, mzero, mplus)
-import Utils
-
-import Test.Framework.TH
-import Test.Framework.Providers.HUnit
-
-testGroups = [ $(testGroupGenerator) ]
-
-case_NdetEff_testCA :: Assertion
-case_NdetEff_testCA = [2, 4..10] @=? (run $ makeChoiceA testCA)
-  where
-    testCA :: (Integral a) => Eff (NdetEff ': r) a
-    testCA = do
-      i <- msum . fmap return $ [1..10]
-      guard (i `mod` 2 == 0)
-      return i
-
-case_NdetEff_ifte :: Assertion
-case_NdetEff_ifte =
-  let primes = ifte_test_run
-  in
-    assertEqual "NdetEff: test ifte using primes"
-    [2,3,5,7,11,13,17,19,23,29] primes
-  where
-    ifte_test = do
-      n <- gen
-      ifte (do
-               d <- gen
-               guard $ d < n && n `mod` d == 0
-               -- _ <- trace ("d: " ++ show d) (return ())
-           )
-        (\_ -> mzero)
-        (return n)
-        where gen = msum . fmap return $ [2..30]
-
-    ifte_test_run :: [Int]
-    ifte_test_run = run . makeChoiceA $ ifte_test
-
-
--- called reflect in the LogicT paper
-case_NdetEff_reflect :: Assertion
-case_NdetEff_reflect =
-  let tsplitr10 = run $ runListWriter $ makeChoiceA tsplit
-      tsplitr11 = run $ runListWriter $ makeChoiceA (msplit tsplit >>= unmsplit)
-      tsplitr20 = run $ makeChoiceA $ runListWriter tsplit
-      tsplitr21 = run $ makeChoiceA $ runListWriter (msplit tsplit >>= unmsplit)
-  in
-    assertEqual "tsplitr10" expected1 tsplitr10
-    >> assertEqual "tsplitr11" expected1 tsplitr11
-    >> assertEqual "tsplitr20" expected2 tsplitr20
-    >> assertEqual "tsplitr21" expected21 tsplitr21
-  where
-    expected1 = ([1, 2],["begin", "end"])
-    expected2 = [(1, ["begin"]), (2, ["end"])]
-    expected21 = [(1, ["begin"]), (2, ["begin", "end"])]
-
-    unmsplit :: Member NdetEff r => (Maybe (a, Eff r a)) -> Eff r a
-    unmsplit Nothing      = mzero
-    unmsplit (Just (a,m)) = return a `mplus` m
-
-    tsplit =
-      (tell "begin" >> return 1) `mplus`
-      (tell "end"   >> return 2)
-
-case_NdetEff_monadBaseControl :: Assertion
-case_NdetEff_monadBaseControl = runLift (makeChoiceA $ doThing (return 1 <|> return 2)) @=? Just [1,2]
diff --git a/test/Control/Eff/Reader/Lazy/Test.hs b/test/Control/Eff/Reader/Lazy/Test.hs
--- a/test/Control/Eff/Reader/Lazy/Test.hs
+++ b/test/Control/Eff/Reader/Lazy/Test.hs
@@ -8,7 +8,6 @@
 
 import Test.HUnit hiding (State)
 import Control.Eff
-import Control.Eff.Lift
 import Control.Eff.Reader.Lazy
 import Control.Monad
 import Utils
diff --git a/test/Control/Eff/Reader/Strict/Test.hs b/test/Control/Eff/Reader/Strict/Test.hs
--- a/test/Control/Eff/Reader/Strict/Test.hs
+++ b/test/Control/Eff/Reader/Strict/Test.hs
@@ -7,7 +7,6 @@
 
 import Test.HUnit hiding (State)
 import Control.Eff
-import Control.Eff.Lift
 import Control.Eff.Reader.Strict
 import Utils
 
diff --git a/test/Control/Eff/State/Lazy/Test.hs b/test/Control/Eff/State/Lazy/Test.hs
--- a/test/Control/Eff/State/Lazy/Test.hs
+++ b/test/Control/Eff/State/Lazy/Test.hs
@@ -7,7 +7,6 @@
 
 import Test.HUnit hiding (State)
 import Control.Eff
-import Control.Eff.Lift
 import Control.Eff.State.Lazy
 import Utils
 
diff --git a/test/Control/Eff/State/OnDemand/Test.hs b/test/Control/Eff/State/OnDemand/Test.hs
--- a/test/Control/Eff/State/OnDemand/Test.hs
+++ b/test/Control/Eff/State/OnDemand/Test.hs
@@ -9,7 +9,6 @@
 import Test.HUnit hiding (State)
 import Control.Eff
 import Control.Eff.Exception
-import Control.Eff.Lift
 import Control.Eff.State.OnDemand
 import Utils
 
diff --git a/test/Control/Eff/State/Strict/Test.hs b/test/Control/Eff/State/Strict/Test.hs
--- a/test/Control/Eff/State/Strict/Test.hs
+++ b/test/Control/Eff/State/Strict/Test.hs
@@ -8,7 +8,6 @@
 import Test.HUnit hiding (State)
 import Control.Eff
 import Control.Eff.Exception
-import Control.Eff.Lift
 import Control.Eff.State.Strict
 import Control.Eff.Reader.Strict
 import Control.Eff.Writer.Strict
diff --git a/test/Control/Eff/Test.hs b/test/Control/Eff/Test.hs
--- a/test/Control/Eff/Test.hs
+++ b/test/Control/Eff/Test.hs
@@ -2,14 +2,21 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE TypeOperators, DataKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
 
 module Control.Eff.Test (testGroups) where
 
+import Test.HUnit hiding (State)
 import Test.QuickCheck
 import Control.Eff
 import Control.Eff.Reader.Strict
+import Control.Eff.State.Strict
+import Control.Eff.Exception
+import qualified Control.Exception as Exc
+import Utils
 
 import Test.Framework.TH
+import Test.Framework.Providers.HUnit
 import Test.Framework.Providers.QuickCheck2
 
 testGroups = [ $(testGroupGenerator) ]
@@ -29,3 +36,180 @@
     readerId = do
       x <- ask
       return x
+
+-- | Ensure that https://github.com/RobotGymnast/extensible-effects/issues/11 stays resolved.
+case_Lift_building :: Assertion
+case_Lift_building = runLift possiblyAmbiguous
+  where
+    possiblyAmbiguous :: (Monad m, Lifted m r) => Eff r ()
+    possiblyAmbiguous = lift $ return ()
+
+case_Lift_tl1r :: Assertion
+case_Lift_tl1r = do
+  ((), output) <- catchOutput tl1r
+  assertOutput "Test tl1r" [show input] output
+  where
+    input = (5::Int)
+    -- tl1r :: IO ()
+    tl1r = runLift (runReader input tl1)
+      where
+        tl1 = ask >>= \(x::Int) -> lift . print $ x
+
+case_Lift_tMd' :: Assertion
+case_Lift_tMd' = do
+  (actualResult, actualOutput) <- catchOutput tMd'
+  let expected = (output, map show input)
+  assertEqual "Test mapMdebug using Lift" expected (actualResult, lines actualOutput)
+  where
+    input = [1..5]
+    val = (10::Int)
+    output = map (+ val) input
+
+    tMd' = runLift $ runReader val $ mapMdebug' f input
+      where f x = ask `add` return x
+
+    -- Re-implemenation of mapMdebug using Lifting
+    -- The signature is inferred
+    mapMdebug'  :: (Show a, Lifted IO r) =>
+                   (a -> Eff r b) -> [a] -> Eff r [b]
+    mapMdebug' _f [] = return []
+    mapMdebug' f (h:t) = do
+      lift $ print h
+      h' <- f h
+      t' <- mapMdebug' f t
+      return (h':t')
+
+-- tests from <http://okmij.org/ftp/Haskell/misc.html#catch-MonadIO>
+data MyException = MyException String deriving (Show)
+instance Exc.Exception MyException
+
+exfn :: Lifted IO r => Bool -> Eff r Bool
+exfn True = lift . Exc.throw $ (MyException "thrown")
+exfn False = return True
+
+testc m = catchDynE (m >>= return . show) (\ (MyException s) -> return s)
+test1 m = do runLift (tf m True) >>= print; runLift (tf m False) >>= print
+tf m x = runReader (x::Bool) . runState ([]::[String]) $ m
+
+runErrorStr = runError @String
+
+case_catchDynE_test1 :: Assertion
+case_catchDynE_test1 = do
+  ((), actual) <- catchOutput $ test1 (testc m)
+  let expected = [ "(\"thrown\",[\"begin\"])"
+                 , "(\"True\",[\"end\",\"begin\"])"]
+  assertOutput "catchDynE: test1: exception shouldn't drop Writer's state"
+    expected actual
+  where
+    -- In CatchMonadIO, the result of tf True is ("thrown",[]) --
+    -- that is, an exception will drop the Writer's state, even if that
+    -- exception is caught. Here, the state is preserved!
+    -- So, this is an advantage over MTL!
+    m = do
+      modify ("begin":)
+      x <- ask
+      r <- exfn x
+      modify ("end":)
+      return r
+
+-- Let us use an Error effect instead
+case_catchDynE_test1' :: Assertion
+case_catchDynE_test1' = do
+  ((), actual') <- catchOutput $ test1 (runErrorStr (testc m))
+  let expected' = [ "(Left \"thrown\",[\"begin\"])"
+                  , "(Right \"True\",[\"end\",\"begin\"])"]
+  assertOutput "catchDynE: test1': Error shouldn't drop Writer's state"
+    expected' actual'
+  where
+    -- In CatchMonadIO, the result of tf True is ("thrown",[]) --
+    -- that is, an exception will drop the Writer's state, even if that
+    -- exception is caught. Here, the state is preserved!
+    -- So, this is an advantage over MTL!
+    m = do
+      modify ("begin":)
+      x <- ask
+      r <- exfn x
+      modify ("end":)
+      return r
+
+    exfn True = throwError $ ("thrown")
+    exfn False = return True
+-- Now, the behavior of the dynamic Exception and Error effect is consistent.
+-- The state is preserved. Before it wasn't.
+
+case_catchDynE_test2 :: Assertion
+case_catchDynE_test2 = do
+  ((), actual) <- catchOutput $ test1 (runErrorStr (testc m))
+  let expected = [ "(Left \"thrown\",[\"begin\"])"
+                 , "(Right \"True\",[\"end\",\"begin\"])"]
+  assertOutput "catchDynE: test2: Error shouldn't drop Writer's state"
+    expected actual
+  where
+    m = do
+      modify ("begin":)
+      x <- ask
+      r <- exfn x `catchDynE` (\ (MyException s) -> throwError s)
+      modify ("end":)
+      return r
+
+-- Full recovery
+case_catchDynE_test2' :: Assertion
+case_catchDynE_test2' = do
+  ((), actual) <- catchOutput $ test1 (runErrorStr (testc m))
+  let expected = [ "(Right \"False\",[\"end\",\"begin\"])"
+                 , "(Right \"True\",[\"end\",\"begin\"])"]
+  assertOutput "catchDynE: test2': Fully recover from errors"
+    expected actual
+  where
+    m = do
+      modify ("begin":)
+      x <- ask
+      r <- exfn x `catchDynE` (\ (MyException _s) -> return False)
+      modify ("end":)
+      return r
+
+-- Throwing within a handler
+case_catchDynE_test3 :: Assertion
+case_catchDynE_test3 = do
+  ((), actual) <- catchOutput $ test1 (runErrorStr (testc m))
+  let expected = [ "(Right \"rethrow:thrown\",[\"begin\"])"
+                 , "(Right \"True\",[\"end\",\"begin\"])"]
+  assertOutput "catchDynE: test3: Throwing within a handler"
+    expected actual
+  where
+    m = do
+      modify ("begin":)
+      x <- ask
+      r <- exfn x `catchDynE` (\ (MyException s) ->
+                                 lift . Exc.throw . MyException $
+                                 ("rethrow:" ++ s))
+      modify ("end":)
+      return r
+
+-- Implement the transactional behavior: when the exception is raised,
+-- the state is rolled back to what it existed at the entrance to
+-- the catch block.
+-- This is the ``scoping behavior'' of `Handlers in action'
+case_catchDynE_tran :: Assertion
+case_catchDynE_tran = do
+  ((), actual1) <- catchOutput $ test1 m1
+  ((), actual2) <- catchOutput $ test1 m2
+  let expected1 = ["(\"thrown\",[\"init\"])"
+                  ,"(\"True\",[\"end\",\"begin\",\"init\"])"]
+  let expected2 = ["(\"thrown\",[\"begin\",\"init\"])"
+                  ,"(\"True\",[\"end\",\"begin\",\"init\"])"]
+  assertOutput "catchDynE: tran: Transactional behaviour" expected1 actual1
+    >> assertOutput "catchDynE: tran: usual behaviour" expected2 actual2
+  where
+    m1 = do
+      modify ("init":)
+      testc (transactionState (TxState :: TxState [String]) m)
+    m2 = do
+      modify ("init":)
+      testc m
+    m = do
+      modify ("begin":)
+      x <- ask
+      r <- exfn x
+      modify ("end":)
+      return r
diff --git a/test/Control/Eff/Trace/Test.hs b/test/Control/Eff/Trace/Test.hs
--- a/test/Control/Eff/Trace/Test.hs
+++ b/test/Control/Eff/Trace/Test.hs
@@ -20,7 +20,7 @@
 case_Trace_tdup = do
   ((), actual) <- catchOutput tdup
   assertEqual "Trace: duplicate layers"
-    (unlines ["Asked: 20", "Asked: 10"]) actual
+    ["Asked: 20", "Asked: 10"] (lines actual)
   where
     tdup = runTrace $ runReader (10::Int) m
      where
diff --git a/test/Control/Eff/Writer/Lazy/Test.hs b/test/Control/Eff/Writer/Lazy/Test.hs
--- a/test/Control/Eff/Writer/Lazy/Test.hs
+++ b/test/Control/Eff/Writer/Lazy/Test.hs
@@ -9,7 +9,6 @@
 import Test.QuickCheck
 
 import Control.Eff
-import Control.Eff.Lift
 import Control.Eff.Reader.Lazy
 import Control.Eff.Writer.Lazy
 import Utils
diff --git a/test/Control/Eff/Writer/Strict/Test.hs b/test/Control/Eff/Writer/Strict/Test.hs
--- a/test/Control/Eff/Writer/Strict/Test.hs
+++ b/test/Control/Eff/Writer/Strict/Test.hs
@@ -7,7 +7,6 @@
 
 import Test.HUnit hiding (State)
 import Control.Eff
-import Control.Eff.Lift
 import Control.Eff.Writer.Strict
 import Utils
 
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -1,14 +1,11 @@
 import Test.Framework (defaultMain, Test)
 
 import qualified Control.Eff.Test
-import qualified Control.Eff.Choose.Test
 import qualified Control.Eff.Coroutine.Test
-import qualified Control.Eff.Cut.Test
 import qualified Control.Eff.Example.Test
 import qualified Control.Eff.Exception.Test
 import qualified Control.Eff.Fresh.Test
-import qualified Control.Eff.Lift.Test
-import qualified Control.Eff.NdetEff.Test
+import qualified Control.Eff.Logic.NDet.Test
 import qualified Control.Eff.Operational.Test
 import qualified Control.Eff.Reader.Lazy.Test
 import qualified Control.Eff.Reader.Strict.Test
@@ -28,14 +25,11 @@
 testGroups :: [Test]
 testGroups = []
              ++ Control.Eff.Test.testGroups
-             ++ Control.Eff.Choose.Test.testGroups
              ++ Control.Eff.Coroutine.Test.testGroups
-             ++ Control.Eff.Cut.Test.testGroups
              ++ Control.Eff.Example.Test.testGroups
              ++ Control.Eff.Exception.Test.testGroups
              ++ Control.Eff.Fresh.Test.testGroups
-             ++ Control.Eff.Lift.Test.testGroups
-             ++ Control.Eff.NdetEff.Test.testGroups
+             ++ Control.Eff.Logic.NDet.Test.testGroups
              ++ Control.Eff.Operational.Test.testGroups
              ++ Control.Eff.Reader.Lazy.Test.testGroups
              ++ Control.Eff.Reader.Strict.Test.testGroups
diff --git a/test/Utils.hs b/test/Utils.hs
--- a/test/Utils.hs
+++ b/test/Utils.hs
@@ -14,12 +14,6 @@
 catchOutput :: IO a -> IO (a, String)
 catchOutput f = swap `fmap` capture f
 
-showLn :: Show a => a -> String
-showLn x = unlines $ [show x]
-
-showLines :: Show a => [a] -> String
-showLines xs = unlines $ map show xs
-
 withError :: a -> ErrorCall -> a
 withError a _ = a
 
@@ -28,6 +22,12 @@
 
 assertNoUndefined :: a -> Assertion
 assertNoUndefined a = catch (seq a $ return ()) (withError $ assertFailure "")
+
+assertOutput :: String -> [String] -> String -> Assertion
+assertOutput msg expected actual = assertEqual msg expected (lines actual)
+
+runAsserts :: (String -> a -> e -> Assertion) -> [(String, e, a)] -> Assertion
+runAsserts run cases = forM_ cases $ \(prop, test, res) -> run prop res test
 
 allEqual :: Eq a => [a] -> Bool
 allEqual = all (uncurry (==)) . pairs