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:             2.0.0.2
+version:             2.0.1.0
 
 -- A short (one-line) description of the package.
 synopsis:            An Alternative to Monad Transformers
@@ -69,6 +69,7 @@
   exposed-modules:     Control.Eff
                        Control.Eff.Choose
                        Control.Eff.Coroutine
+                       Control.Eff.Cut
                        Control.Eff.Example
                        Control.Eff.Exception
                        Control.Eff.Fresh
diff --git a/src/Control/Eff.hs b/src/Control/Eff.hs
--- a/src/Control/Eff.hs
+++ b/src/Control/Eff.hs
@@ -8,7 +8,11 @@
 
 {-# LANGUAGE CPP #-}
 
--- | Original work available at <http://okmij.org/ftp/Haskell/extensible/tutorial.html>.
+-- ------------------------------------------------------------------------
+-- | A monadic library for communication between a handler and
+-- its client, the administered computation
+--
+-- Original work available at <http://okmij.org/ftp/Haskell/extensible/tutorial.html>.
 -- This module implements extensible effects as an alternative to monad transformers,
 -- as described in <http://okmij.org/ftp/Haskell/extensible/exteff.pdf> and
 -- <http://okmij.org/ftp/Haskell/extensible/more.pdf>.
@@ -25,20 +29,17 @@
 import safe Data.FTCQueue
 import GHC.Exts (inline)
 
--- ------------------------------------------------------------------------
--- | A monadic library for communication between a handler and
--- its client, the administered computation
---
--- Effectful arrow type: a function from a to b that also does effects
+-- | 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
 
-arr :: (a -> b) -> Arrs r a b
-arr f = tsingleton (Val . f)
-
-ident :: Arrs r a a
-ident = arr id
+-- | An effectful function from 'a' to 'b' that is a composition
+-- of several effectful functions. The paremeter r describes the overall
+-- effect.
+-- The composition members are accumulated in a type-aligned queue
+type Arrs r a b = FTCQueue (Eff r) a b
 
+{-# INLINE single #-}
 single :: Arr r a b -> Arrs r a b
 single = tsingleton
 
@@ -46,15 +47,15 @@
 first :: Arr r a b -> Arr r (a, c) (b, c)
 first x = \(a,c) -> (, c) `fmap` x a
 
+arr :: (a -> b) -> Arrs r a b
+arr f = single (Val . f)
+
+ident :: Arrs r a a
+ident = arr id
+
 comp :: Arrs r a b -> Arrs r b c -> Arrs r a c
 comp = (><)
 
--- | An effectful function from 'a' to 'b' that is a composition
--- of several effectful functions. The paremeter r describes the overall
--- effect.
--- The composition members are accumulated in a type-aligned queue
-type Arrs r a b = FTCQueue (Eff r) a b
-
 -- | 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
@@ -135,20 +136,6 @@
 {-# RULES
   "send/bind" [~3] forall t k. send t >>= k = E (inj t) (tsingleton k)
  #-}
-
-
-{-
--- The opposite of admin, occasionally useful
--- See the soft-cut for an example
--- It is currently quite inefficient. There are better ways
-reflect :: VE a r -> Eff r a
-reflect (Val x) = return x
-reflect (E u) = Eff (\k -> E $ fmap (loop k) u)
- where
- loop :: (a -> VE w r) -> VE a r -> VE w r
- loop k (Val x) = k x
- loop k (E u)   = E $ fmap (loop k) u
--}
 
 
 -- ------------------------------------------------------------------------
diff --git a/src/Control/Eff/Cut.hs b/src/Control/Eff/Cut.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Eff/Cut.hs
@@ -0,0 +1,82 @@
+{-# 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.Exception
+import Control.Eff.Choose
+import Data.OpenUnion
+
+data CutFalse = CutFalse
+
+cutfalse :: Member (Exc CutFalse) r => Eff r a
+cutfalse = throwExc 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 :: 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 jq u _ | Just (Choose []) <- prj u  = next jq  -- (C1)
+  check jq u q | Just (Choose [x]) <- prj u = loop jq (qApp q x)  -- (C3), optim
+  check jq u q | Just (Choose lst) <- prj u = next $ map (qApp 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/Data/OpenUnion.hs b/src/Data/OpenUnion.hs
--- a/src/Data/OpenUnion.hs
+++ b/src/Data/OpenUnion.hs
@@ -20,7 +20,7 @@
 #else
 #endif
 
--- Only for MemberU below, when emulating Monad Transformers
+-- Only for SetMember below, when emulating Monad Transformers
 {-# LANGUAGE FunctionalDependencies, UndecidableInstances #-}
 
 -- | Open unions (type-indexed co-products) for extensible effects
@@ -62,8 +62,8 @@
 
 import Unsafe.Coerce(unsafeCoerce)
 
--- The data constructors of Union are not exported
-
+-- | The data constructors of Union are not exported
+--
 -- Strong Sum (Existential with the evidence) is an open union
 -- t is can be a GADT and hence not necessarily a Functor.
 -- Int is the index of t in the list r; that is, the index of t in the
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -42,6 +42,7 @@
 import Control.Eff.Operational.Example as Op.Eg
 import Control.Eff.Trace
 import Control.Eff.Coroutine
+import Control.Eff.Cut
 
 -- {{{ utils: TODO: move them out
 
@@ -90,14 +91,7 @@
 -- }}}
 
 main :: IO ()
-main = defaultMain tests
-
-tests = [
-  $(testGroupGenerator)
-#if __GLASGOW_HASKELL__ >= 708
-  , testProperty "Test nested Eff." testNestedEff
-#endif
-        ]
+main = $(defaultMainGenerator)
 
 -- {{{ Documentation example
 
@@ -618,8 +612,8 @@
 
 -- {{{ Nested Eff
 
-testNestedEff :: Property
-testNestedEff = forAll arbitrary (\x -> property (qu x == x))
+prop_NestedEff :: Property
+prop_NestedEff = forAll arbitrary (\x -> property (qu x == x))
   where
     qu :: Bool -> Bool
     qu x = run $ StrictR.runReader (readerAp x) readerId
@@ -1070,5 +1064,34 @@
         LazierS.lput ((1::Int):s)
   in
     assertEqual "LazyState ones" [1,1,1,1,1] (take 5 ones)
+
+-- }}}
+
+-- {{{ Cut
+
+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)
 
 -- }}}