diff --git a/BinderAnn.cabal b/BinderAnn.cabal
new file mode 100644
--- /dev/null
+++ b/BinderAnn.cabal
@@ -0,0 +1,82 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: ce149fc6e75cfeb949194627c460f9c65a8f20b122a9cd208e22ad08c9000c7e
+
+name:           BinderAnn
+version:        0.1.0.0
+synopsis:       Source-to-source plugin for enhancing EDSLs with static annotations
+description:    Please see the README on GitHub at <https://github.com/OctopiChalmers/BinderAnn#readme>
+category:       Compiler Plugin
+homepage:       https://github.com/OctopiChalmers/BinderAnn#readme
+bug-reports:    https://github.com/OctopiChalmers/BinderAnn/issues
+author:         Agustín Mista
+maintainer:     mista@chalmers.se
+copyright:      2019 Agustín Mista
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/OctopiChalmers/BinderAnn
+
+library
+  exposed-modules:
+      BinderAnn.Pure
+      BinderAnn.Monadic
+      BinderAnn.Generic
+      Data.Annotated.Pure
+      Data.Annotated.Monadic
+      Data.Annotated.Generic.Safe
+      Data.Annotated.Generic.Unsafe
+      Control.Monad.Annotated.Class
+      System.Mem.StableMap
+  other-modules:
+      BinderAnn.Common
+      BinderAnn.SrcInfo
+      BinderAnn.Wrapped
+      Data.Annotated.Generic
+      Paths_BinderAnn
+  hs-source-dirs:
+      src
+  ghc-options: -Wall
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , ghc
+    , ghc-prim
+    , mtl
+    , split
+    , syb
+    , transformers
+  default-language: Haskell2010
+
+test-suite test-plugin
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      Generic
+      Monadic
+      Pure
+      Paths_BinderAnn
+  hs-source-dirs:
+      test
+  ghc-options: -Wall
+  build-depends:
+      BinderAnn
+    , base >=4.7 && <5
+    , containers
+    , ghc
+    , ghc-prim
+    , mtl
+    , split
+    , syb
+    , transformers
+  default-language: Haskell2010
diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for BinderMinder
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Agustín Mista (c) 2019
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Agustín Mista nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,1 @@
+# BinderAnn: Automated Reification of Source Annotations for Monadic EDSLs
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/src/BinderAnn/Common.hs b/src/BinderAnn/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/BinderAnn/Common.hs
@@ -0,0 +1,370 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE FlexibleContexts #-}
+module BinderAnn.Common
+  ( binderann_Pure
+  , binderann_Monadic
+  , binderann_Generic
+  ) where
+
+import Data.List.Split
+import Data.Generics (mkM, everywhereM, listify)
+
+import FastString as FS
+import HsSyn      as GHC
+import GhcPlugins as GHC hiding (Auto)
+import OccName    as Name
+
+
+----------------------------------------
+-- | The plugin versions
+
+binderann_Pure    :: [CommandLineOption] -> HsParsedModule -> Hsc HsParsedModule
+binderann_Pure    = binderann __annotateM_Pure__
+binderann_Monadic :: [CommandLineOption] -> HsParsedModule -> Hsc HsParsedModule
+binderann_Monadic = binderann __annotateM_Monadic__
+binderann_Generic :: [CommandLineOption] -> HsParsedModule -> Hsc HsParsedModule
+binderann_Generic = binderann __annotateM_Generic__
+
+----------------------------------------
+-- | The plugin itself, parameterized by the annotating function
+
+binderann :: RdrName -> [CommandLineOption] -> HsParsedModule -> Hsc HsParsedModule
+binderann ann_fun opts parsed = do
+  message $ "starting plugin"
+
+  flags <- getDynFlags
+  let L loc hsMod = hpm_module parsed
+
+  annHsMod <- case runMode opts of
+    Auto -> do
+      message $ "run mode: auto"
+
+      message $ "annotating every do expression..."
+      hsMod' <- mkM (annotateDo flags ann_fun) `everywhereM` hsMod
+      message $ "done"
+
+      return hsMod'
+
+    Manual ann_tok -> do
+      let ann_op = mkRdrName ann_tok
+      let anns = extractAnn <$> listify (isAnn flags) hsMod
+
+      message $ "run mode: manual"
+      message $ "infix annotation token: " ++ show ann_tok
+
+      message $ "annotating top level definitions..."
+      hsMod' <- mkM (annotateTopLevel flags ann_fun anns) `everywhereM` hsMod
+      message $ "done"
+
+      message $ "annotating infix tokens..."
+      hsMod'' <- mkM (annotateInfix flags ann_fun ann_op) `everywhereM` hsMod'
+      message $ "done"
+
+      return hsMod''
+
+  message $ "plugin finished!"
+  return parsed { hpm_module = L loc annHsMod }
+
+----------------------------------------
+-- | Annotate a normal do expression
+
+annotateDo
+  :: DynFlags
+  -> RdrName
+  -> LHsExpr GhcPs
+  -> Hsc (LHsExpr GhcPs)
+annotateDo flags ann_fun = \case
+
+  -- annotate every do statemtent within a do expression
+  L l (HsDo  _ y (L z doStmts)) -> do
+    message $ "+ annotating do expression at " ++ showPpr flags l
+    doStmts' <- mapM (annotateStmt flags ann_fun) doStmts
+    return (L l (HsDo noExt y (L z doStmts')))
+
+  -- otherwise, just return the match unchanged
+  expr -> return expr
+
+----------------------------------------
+-- | Annotate a do expression defined in a top-level binding:
+--
+-- {-# ANN foo SrcInfo #-}
+-- foo = do ...
+--
+annotateTopLevel
+  :: DynFlags
+  -> RdrName
+  -> [RdrName]
+  -> Match GhcPs (LHsExpr GhcPs)
+  -> Hsc (Match GhcPs (LHsExpr GhcPs))
+annotateTopLevel flags ann_fun anns = \case
+
+  -- annotate match statements that appear in the module annotations pragmas
+  Match m_x m_ctx m_ps
+    (GRHSs grhss_x
+      [L l (GRHS grhs_x grhs_guards
+             (L l' (HsDo do_x do_cxt (L l'' doStmts))))] lbs)
+    | isFunRhs m_ctx && unLoc (mc_fun m_ctx) `elem` anns -> do
+        message $ "+ annotating do expression at " ++ showPpr flags l
+
+        doStmts' <- mapM (annotateStmt flags ann_fun) doStmts
+        return (Match m_x m_ctx m_ps
+                 (GRHSs grhss_x
+                   [L l (GRHS grhs_x grhs_guards
+                          (L l' (HsDo do_x do_cxt (L l'' doStmts'))))] lbs))
+
+  -- otherwise, just return the match unchanged
+  match -> return match
+
+
+----------------------------------------
+-- | Annotated do expressions at the right hand side of the annotation token:
+--
+-- some expression <ann_tok> do ...
+--
+annotateInfix
+  :: DynFlags
+  -> RdrName
+  -> RdrName
+  -> LHsExpr GhcPs
+  -> Hsc (LHsExpr GhcPs)
+annotateInfix flags ann_fun ann_tok = \case
+
+  -- annotate do expression prefixed with the annotation token
+  L l (OpApp _
+        lhs
+        (L _ (HsVar _   (L _ tok)))
+        (L _ (HsDo  _ y (L z doStmts))))
+    | showPpr flags tok == showPpr flags ann_tok -> do
+        message $ "+ annotating do expression at " ++ showPpr flags l
+
+        doStmts' <- mapM (annotateStmt flags ann_fun) doStmts
+        let do' = L l (HsDo noExt y (L z doStmts'))
+        let expr' = paren lhs & paren do'
+
+        return expr'
+
+  -- otherwise, return the expression unchanged
+  expr -> return expr
+
+
+----------------------------------------
+-- | Annotate a single do statement
+annotateStmt
+  :: DynFlags
+  -> RdrName
+  -> ExprLStmt GhcPs
+  -> Hsc (ExprLStmt GhcPs)
+annotateStmt flags ann_fun = \case
+
+  -- bind statements where the lhs is a variable pattern
+  L l (BindStmt x pat@(L _ (VarPat _ (L _ bind))) body y z) -> do
+
+    let body' =
+          var ann_fun
+          & paren body
+          & paren (var __Info__
+                   & paren (var __Just__
+                            & varPatToLitStr flags pat)
+                   & paren (mkLocExpr l))
+
+    message $ "  * found single bind ("++ render bind ++ ") at " ++ render l
+    return (L l (BindStmt x pat body' y z))
+
+  -- bind statements where the lhs is a single type constructor
+  L l (BindStmt x pat@(L _ (ConPatIn (L _ _) argP)) body y z) ->
+    case hsConPatArgs argP of
+      [p] -> do
+        let body' =
+              var ann_fun
+              & paren body
+              & paren (var __Info__
+                      & paren (var __Just__
+                               & varPatToLitStr flags p)
+                      & paren (mkLocExpr l))
+
+        message $ "  * found constructor bind ("++ render pat ++ ") at " ++ render l
+        return (L l (BindStmt x pat body' y z))
+
+      _ -> do
+        message $ "  * skipping constructor bind ("++ render pat ++ ") at " ++ render l
+        return (L l (BindStmt x pat body y z))
+
+  -- bind statements where the lhs is a tuple pattern
+  L l (BindStmt x pat@(L _ (TuplePat _ binds _)) body y z)
+    | length binds > 1 && length binds <= 5 && all isVarPat binds -> do
+
+        let bindStrs = varPatToLitStr flags <$> binds
+        let body' =
+              var (__lift_tuple__ (length binds))
+              & mkAnnTuple ann_fun l bindStrs
+              & paren body
+
+        message $ "  * found tuple bind ("++ render pat ++ ") at " ++ render l
+        return (L l (BindStmt x pat body' y z))
+
+  -- body statements
+  L l (BodyStmt x body y z) -> do
+
+    let body' =
+          var ann_fun
+          & paren body
+          & paren (var __Info__
+                   & var __Nothing__
+                   & paren (mkLocExpr l))
+
+    message $ "  * found body statement at " ++ render l
+    return (L l (BodyStmt x body' y z))
+
+  -- everything else is left unchanged
+  stmt -> return stmt
+
+  where render :: forall a. Outputable a => a -> String
+        render = showPpr flags
+
+----------------------------------------
+-- | Command line options
+
+defaultInfixOperator :: String
+defaultInfixOperator = "|$|"
+
+data RunMode = Auto | Manual String
+  deriving Show
+
+runMode :: [String] -> RunMode
+runMode opts
+  | Just op <- optInfixOperator opts = Manual op
+  | optManual opts = Manual defaultInfixOperator
+  | otherwise = Auto
+
+optInfixOperator :: [String] -> Maybe String
+optInfixOperator = \case
+  [] -> Nothing
+  (o:_) | ["infix", tok] <- splitOn "=" o -> Just tok
+  (_:os) -> optInfixOperator os
+
+optManual :: [String] -> Bool
+optManual = any ("manual"==)
+
+----------------------------------------
+-- | Helper functions
+
+-- | Print a message to the console
+message :: String -> Hsc ()
+message str = liftIO $ putStrLn $ "[BinderAnn] " ++ str
+
+-- | Create a name from a string
+mkRdrName :: String -> RdrName
+mkRdrName = mkUnqual Name.varName . mkFastString
+
+-- | Create a Loc tuple from a SrcSpan
+mkLocExpr :: SrcSpan -> LHsExpr GhcPs
+mkLocExpr (UnhelpfulSpan {}) =
+  var __Nothing__
+mkLocExpr (RealSrcSpan loc) =
+  paren (var __Just__ &
+         tuple [ strLit (srcSpanFile loc)
+               , numLit (srcSpanStartLine loc)
+               , numLit (srcSpanStartCol loc) ])
+
+-- | Create a tuple of the shape:
+-- (ann_fun name1 loc1, ann_fun name2 loc2, ...)
+mkAnnTuple :: RdrName -> SrcSpan -> [LHsExpr GhcPs] -> LHsExpr GhcPs
+mkAnnTuple ann_fun loc bindStrs =
+  tuple (mkElem <$> bindStrs)
+  where mkElem bindStrLit =
+         var __flip__
+         & var ann_fun
+         & paren (var __Info__
+                  & paren (var __Just__ & bindStrLit)
+                  & paren (mkLocExpr loc))
+
+-- | Transform a variable pattern into its corresponding string expression
+varPatToLitStr :: DynFlags -> LPat GhcPs -> LHsExpr GhcPs
+varPatToLitStr flags (L _ (VarPat _ name)) = strLit (fsLit (showPpr flags name))
+varPatToLitStr _     _                     = error "this should not happen"
+
+
+-- | Is this pattern a variable?
+isVarPat :: LPat GhcPs -> Bool
+isVarPat (L _ (VarPat {})) = True
+isVarPat _                 =  False
+
+-- | Is this a patter matching an argument of a function binding?
+isFunRhs :: HsMatchContext id -> Bool
+isFunRhs (FunRhs {}) = True
+isFunRhs _           = False
+
+-- | Check whether an annotation pragma is of the shape:
+-- | {-# ANN ident SrcInfo #-}
+pattern HsAnn :: RdrName -> RdrName -> AnnDecl GhcPs
+pattern HsAnn lhs rhs <-
+  HsAnnotation _ _
+  (ValueAnnProvenance (L _ lhs))
+  (L _ (HsVar _ (L _ rhs)))
+
+isAnn :: DynFlags -> AnnDecl GhcPs -> Bool
+isAnn flags (HsAnn _ rhs) = showPpr flags rhs == showPpr flags __SrcInfoTag__
+isAnn _     _             = False
+
+extractAnn :: AnnDecl GhcPs -> RdrName
+extractAnn (HsAnn target _) = target
+extractAnn _                = error "this should not happen"
+
+----------------------------------------
+-- | Located expressions builder interface
+
+app :: LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
+app x y = noLoc (HsApp noExt x y)
+
+(&) :: LHsExpr GhcPs -> LHsExpr GhcPs -> LHsExpr GhcPs
+(&) = app
+infixl 4 &
+
+paren :: LHsExpr GhcPs -> LHsExpr GhcPs
+paren x = noLoc (HsPar noExt x)
+
+var :: RdrName -> LHsExpr GhcPs
+var x = noLoc (HsVar noExt (noLoc x))
+
+numLit :: Int -> LHsExpr GhcPs
+numLit n = noLoc (HsLit noExt (HsInt noExt (mkIntegralLit n)))
+
+strLit :: FastString -> LHsExpr GhcPs
+strLit s = noLoc (HsLit noExt (HsString NoSourceText s))
+
+tuple :: [LHsExpr GhcPs] -> LHsExpr GhcPs
+tuple exprs = noLoc (ExplicitTuple noExt (noLoc . Present noExt <$> exprs) Boxed)
+
+
+----------------------------------------
+-- | Name wrappers
+
+-- | Wrapped names
+__SrcInfoTag__ :: RdrName
+__SrcInfoTag__ = mkRdrName "SrcInfo"
+
+__Just__ :: RdrName
+__Just__ = mkRdrName "__Just__"
+
+__Nothing__ :: RdrName
+__Nothing__ = mkRdrName "__Nothing__"
+
+__Info__ :: RdrName
+__Info__ = mkRdrName "__Info__"
+
+__flip__ :: RdrName
+__flip__ = mkRdrName "__flip__"
+
+__annotateM_Pure__ :: RdrName
+__annotateM_Pure__ = mkRdrName "__annotateM_Pure__"
+
+__annotateM_Monadic__ :: RdrName
+__annotateM_Monadic__ = mkRdrName "__annotateM_Monadic__"
+
+__annotateM_Generic__ :: RdrName
+__annotateM_Generic__ = mkRdrName "__annotateM_Generic__"
+
+__lift_tuple__ :: Int -> RdrName
+__lift_tuple__ n = mkRdrName $ "__lift_tuple_"++ show n ++"__"
diff --git a/src/BinderAnn/Generic.hs b/src/BinderAnn/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/BinderAnn/Generic.hs
@@ -0,0 +1,19 @@
+module BinderAnn.Generic
+  ( module BinderAnn.SrcInfo
+  , module BinderAnn.Wrapped
+  , module Data.Annotated.Generic
+  , plugin
+  ) where
+
+import GhcPlugins as GHC
+
+import BinderAnn.Common
+import BinderAnn.SrcInfo
+import BinderAnn.Wrapped
+import Data.Annotated.Generic
+
+----------------------------------------
+-- The entry point of this version of the plugin
+
+plugin :: Plugin
+plugin = defaultPlugin { parsedResultAction = const . binderann_Generic }
diff --git a/src/BinderAnn/Monadic.hs b/src/BinderAnn/Monadic.hs
new file mode 100644
--- /dev/null
+++ b/src/BinderAnn/Monadic.hs
@@ -0,0 +1,19 @@
+module BinderAnn.Monadic
+  ( module BinderAnn.SrcInfo
+  , module BinderAnn.Wrapped
+  , module Data.Annotated.Monadic
+  , plugin
+  ) where
+
+import GhcPlugins as GHC
+
+import BinderAnn.Common
+import BinderAnn.SrcInfo
+import BinderAnn.Wrapped
+import Data.Annotated.Monadic
+
+----------------------------------------
+-- The entry point of this version of the plugin
+
+plugin :: Plugin
+plugin = defaultPlugin { parsedResultAction = const . binderann_Monadic }
diff --git a/src/BinderAnn/Pure.hs b/src/BinderAnn/Pure.hs
new file mode 100644
--- /dev/null
+++ b/src/BinderAnn/Pure.hs
@@ -0,0 +1,19 @@
+module BinderAnn.Pure
+  ( module BinderAnn.SrcInfo
+  , module BinderAnn.Wrapped
+  , module Data.Annotated.Pure
+  , plugin
+  ) where
+
+import GhcPlugins as GHC
+
+import BinderAnn.Common
+import BinderAnn.SrcInfo
+import BinderAnn.Wrapped
+import Data.Annotated.Pure
+
+----------------------------------------
+-- The entry point of this version of the plugin
+
+plugin :: Plugin
+plugin = defaultPlugin { parsedResultAction = const . binderann_Pure }
diff --git a/src/BinderAnn/SrcInfo.hs b/src/BinderAnn/SrcInfo.hs
new file mode 100644
--- /dev/null
+++ b/src/BinderAnn/SrcInfo.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+module BinderAnn.SrcInfo where
+
+import Data.Generics (Data)
+
+-- | A simple location in a file
+type Loc = (FilePath, Int, Int) -- file, line and column
+
+-- | The source information of a do statement
+data SrcInfo = Info (Maybe String) (Maybe Loc)
+  deriving (Show, Read, Eq, Ord)
+
+-- | A tag constructor for SrcInfo that can be used with annotation pragmas
+data SrcInfoName = SrcInfo
+  deriving Data
diff --git a/src/BinderAnn/Wrapped.hs b/src/BinderAnn/Wrapped.hs
new file mode 100644
--- /dev/null
+++ b/src/BinderAnn/Wrapped.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+module BinderAnn.Wrapped where
+
+import BinderAnn.SrcInfo
+import qualified Data.Annotated.Pure    as Pure
+import qualified Data.Annotated.Monadic as Monadic
+import qualified Data.Annotated.Generic as Generic
+
+----------------------------------------
+-- | Name wrappers
+
+-- I don't want to deal with names clashes, and since the plugin can only deal
+-- with raw names (RdrName), I wrap every name it uses with a weird one. Also,
+-- dealing with data constructor names is a pain in the ass, so I wrap them up
+-- with variable names as well. :)
+
+-- BinderAnn.Info
+__Info__ :: Maybe String -> Maybe Loc -> SrcInfo
+__Info__ = Info
+
+-- Data.Annotated.annotateM
+__annotateM_Pure__ :: (Monad m, Pure.Annotated a) => m a -> SrcInfo -> m a
+__annotateM_Pure__ = Pure.annotateM
+
+-- Data.Annotated.Monadic.annotateM
+__annotateM_Monadic__ :: Monadic.AnnotatedM m a => m a -> SrcInfo -> m a
+__annotateM_Monadic__ = Monadic.annotateM
+
+  -- Control.Monad.Annotated.Class.annotateM
+__annotateM_Generic__ :: Generic.MonadAnnotated m => m a -> SrcInfo -> m a
+__annotateM_Generic__ = Generic.annotateM
+
+-- Prelude.flip
+__flip__ :: (a -> b -> c) -> (b -> a -> c)
+__flip__ = flip
+
+-- Prelude.Just
+__Just__ :: a -> Maybe a
+__Just__ = Just
+
+-- Prelude.Nothing
+__Nothing__ :: Maybe a
+__Nothing__ = Nothing
+
+-- | Tuple liftings
+__lift_tuple_2__
+  :: Monad m
+  => (m a -> m a', m b -> m b')
+  -> m (a, b)
+  -> m (a', b')
+__lift_tuple_2__ (fa, fb) m = do
+  (a, b) <- m
+  a' <- fa (return a)
+  b' <- fb (return b)
+  return (a', b')
+
+__lift_tuple_3__
+  :: Monad m
+  => (m a -> m a', m b -> m b', m c -> m c')
+  -> m (a, b, c)
+  -> m (a', b', c')
+__lift_tuple_3__ (fa, fb, fc) m = do
+  (a, b, c) <- m
+  a' <- fa (return a)
+  b' <- fb (return b)
+  c' <- fc (return c)
+  return (a', b', c')
+
+__lift_tuple_4__
+  :: Monad m
+  => (m a -> m a', m b -> m b', m c -> m c', m d -> m d')
+  -> m (a, b, c, d)
+  -> m (a', b', c', d')
+__lift_tuple_4__ (fa, fb, fc, fd) m = do
+  (a, b, c, d) <- m
+  a' <- fa (return a)
+  b' <- fb (return b)
+  c' <- fc (return c)
+  d' <- fd (return d)
+  return (a', b', c', d')
+
+__lift_tuple_5__
+  :: Monad m
+  => (m a -> m a', m b -> m b', m c -> m c', m d -> m d', m e -> m e')
+  -> m (a, b, c, d, e)
+  -> m (a', b', c', d', e')
+__lift_tuple_5__ (fa, fb, fc, fd, fe) m = do
+  (a, b, c, d, e) <- m
+  a' <- fa (return a)
+  b' <- fb (return b)
+  c' <- fc (return c)
+  d' <- fd (return d)
+  e' <- fe (return e)
+  return (a', b', c', d', e')
diff --git a/src/Control/Monad/Annotated/Class.hs b/src/Control/Monad/Annotated/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Annotated/Class.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+module Control.Monad.Annotated.Class where
+
+import Control.Monad.Trans.Class (lift)
+import Control.Monad.Trans.Cont
+import Control.Monad.Trans.Except
+import Control.Monad.Trans.Identity
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Reader
+import Control.Monad.Trans.Writer.Lazy as LazyW
+import Control.Monad.Trans.Writer.Strict as StrictW
+import Control.Monad.Trans.State.Lazy as LazyS
+import Control.Monad.Trans.State.Strict as StrictS
+import Control.Monad.Trans.RWS.Lazy as LazyRWS
+import Control.Monad.Trans.RWS.Strict as StrictRWS
+
+import BinderAnn.SrcInfo
+
+----------------------------------------
+-- The annotation monadic effect
+
+class Monad m => MonadAnnotated m where
+  createAnn :: a -> SrcInfo -> m ()
+  lookupAnn :: a -> m (Maybe SrcInfo)
+
+-- Annotate the return value of a monadic computation
+annotateM :: MonadAnnotated m => m a -> SrcInfo -> m a
+annotateM ma ann = do
+  a <- ma
+  createAnn a ann
+  return a
+
+----------------------------------------
+-- Instances for other mtl transformers
+
+instance MonadAnnotated m => MonadAnnotated (ContT r m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance MonadAnnotated m => MonadAnnotated (ExceptT e m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance MonadAnnotated m => MonadAnnotated (IdentityT m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance MonadAnnotated m => MonadAnnotated (MaybeT m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance MonadAnnotated m => MonadAnnotated (ReaderT r m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance (Monoid w, MonadAnnotated m) => MonadAnnotated (LazyW.WriterT w m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance (Monoid w, MonadAnnotated m) => MonadAnnotated (StrictW.WriterT w m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance MonadAnnotated m => MonadAnnotated (LazyS.StateT s m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance MonadAnnotated m => MonadAnnotated (StrictS.StateT s m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance (MonadAnnotated m, Monoid w) => MonadAnnotated (LazyRWS.RWST r w s m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
+
+instance (MonadAnnotated m, Monoid w) => MonadAnnotated (StrictRWS.RWST r w s m) where
+  createAnn a = lift . createAnn a
+  lookupAnn = lift . lookupAnn
diff --git a/src/Data/Annotated/Generic.hs b/src/Data/Annotated/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Annotated/Generic.hs
@@ -0,0 +1,5 @@
+module Data.Annotated.Generic
+  ( module Data.Annotated.Generic.Safe
+  ) where
+
+import Data.Annotated.Generic.Safe
diff --git a/src/Data/Annotated/Generic/Safe.hs b/src/Data/Annotated/Generic/Safe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Annotated/Generic/Safe.hs
@@ -0,0 +1,155 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE BangPatterns #-}
+module Data.Annotated.Generic.Safe
+  ( Annotated
+  , runAnnotated, evalAnnotated, execAnnotated
+  , AnnotatedT(..)
+  , runAnnotatedT, evalAnnotatedT, execAnnotatedT
+  , module Control.Monad
+  , module Control.Monad.Fix
+  , module Control.Monad.Annotated.Class
+  ) where
+
+import Data.Functor.Contravariant
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Signatures
+import Control.Monad.Fix
+import Control.Monad.State
+import Control.Monad.Fail
+import Control.Monad.Identity (Identity, runIdentity)
+
+import Control.Monad.Cont.Class
+import Control.Monad.Error.Class
+import Control.Monad.Reader.Class
+import Control.Monad.Writer.Class
+import Control.Monad.RWS.Class
+
+import System.Mem.StableMap
+import Control.Monad.Annotated.Class
+
+import BinderAnn.SrcInfo
+
+-----------------------------------------------------------------------------
+-- | An annotation monad parameterized by the type @ann@ of the annotation to
+-- carry.
+
+type Annotated a = AnnotatedT Identity a
+
+runAnnotated :: forall a. Annotated a -> (a, StableMap SrcInfo)
+runAnnotated = runIdentity . runAnnotatedT
+
+evalAnnotated :: forall a. Annotated a -> a
+evalAnnotated = fst . runAnnotated
+
+execAnnotated :: forall a. Annotated a -> StableMap SrcInfo
+execAnnotated = snd . runAnnotated
+
+----------------------------------------
+-- The mighty AnnotatedT monad transformer!
+
+newtype AnnotatedT m a =
+  AnnotatedT { unAnnotateT :: StateT (StableMap SrcInfo) m a }
+  deriving
+    ( Functor, Contravariant
+    , Applicative, Alternative
+    , Monad, MonadIO, MonadFail, MonadFix, MonadTrans
+    )
+
+-- runners
+runAnnotatedT :: forall m a. AnnotatedT m a -> m (a, StableMap SrcInfo)
+runAnnotatedT = flip runStateT emptyStableMap . unAnnotateT
+
+evalAnnotatedT :: forall m a. Monad m => AnnotatedT m a -> m a
+evalAnnotatedT m = fst <$> runAnnotatedT m
+
+execAnnotatedT :: forall m a. Monad m => AnnotatedT m a -> m (StableMap SrcInfo)
+execAnnotatedT m = snd <$> runAnnotatedT m
+
+-- actions over annotations
+createAnn_ :: MonadIO m => a -> SrcInfo -> AnnotatedT m ()
+createAnn_ a ann = do
+  AnnotatedT . StateT $ \anns -> do
+    anns' <- liftIO (insertStableName a ann anns)
+    return ((), anns')
+
+lookupAnn_ :: MonadIO m => a -> AnnotatedT m (Maybe SrcInfo)
+lookupAnn_ !a = do
+  AnnotatedT . StateT $ \anns -> do
+    ann <- lookupStableName a anns
+    return (ann, anns)
+
+instance MonadIO m => MonadAnnotated (AnnotatedT m) where
+  createAnn = createAnn_
+  lookupAnn = lookupAnn_
+
+----------------------------------------
+-- Lifting AnnotatedT to support other effects
+
+{-# INLINE liftCallCC #-}
+liftCallCC :: CallCC m (a, StableMap SrcInfo) (b, StableMap SrcInfo)
+           -> CallCC (AnnotatedT m) a b
+liftCallCC callCC_ f = AnnotatedT . StateT $ \s ->
+  callCC_ $ \c ->
+  runStateT (unAnnotateT (f (\a -> AnnotatedT . StateT $ \s' -> c (a, s')))) s
+
+{-# INLINE liftCatch #-}
+liftCatch :: Catch e m (a, StableMap SrcInfo) -> Catch e (AnnotatedT m) a
+liftCatch catchE m h = AnnotatedT . StateT $ \ s ->
+  runStateT (unAnnotateT m) s `catchE` \ e -> runStateT (unAnnotateT (h e)) s
+
+
+{-# INLINE mapAnnotatedT #-}
+mapAnnotatedT :: (m (a, StableMap SrcInfo) -> n (b, StableMap SrcInfo))
+              -> AnnotatedT m a
+              -> AnnotatedT n b
+mapAnnotatedT f m = AnnotatedT . StateT $ \anns ->
+  f (runStateT (unAnnotateT m) anns)
+
+{-# INLINE liftListen #-}
+liftListen :: Monad m
+           => Listen w m (a, StableMap SrcInfo)
+           -> Listen w (AnnotatedT m) a
+liftListen listen_ m = AnnotatedT . StateT $ \anns -> do
+  ~((a, anns'), w) <- listen_ (runStateT (unAnnotateT m) anns)
+  return ((a, w), anns')
+
+{-# INLINE liftPass #-}
+liftPass :: Monad m
+         => Pass w m (a, StableMap SrcInfo)
+         -> Pass w (AnnotatedT m) a
+liftPass pass_ m = AnnotatedT . StateT $ \anns -> pass_ $ do
+    ~((a, f), anns') <- runStateT (unAnnotateT m) anns
+    return ((a, anns'), f)
+
+instance MonadCont m => MonadCont (AnnotatedT m) where
+    callCC = liftCallCC callCC
+
+instance MonadError e m => MonadError e (AnnotatedT m) where
+  throwError = lift . throwError
+  catchError = liftCatch catchError
+
+instance MonadReader r m => MonadReader r (AnnotatedT m) where
+  ask   = lift ask
+  local = mapAnnotatedT . local
+  reader = lift . reader
+
+instance MonadWriter w m => MonadWriter w (AnnotatedT m) where
+  writer = lift . writer
+  tell   = lift . tell
+  listen = liftListen listen
+  pass   = liftPass pass
+
+instance MonadState s m => MonadState s (AnnotatedT m) where
+  get = lift get
+  put = lift . put
+  state = lift . state
+
+instance MonadRWS r w s m => MonadRWS r w s (AnnotatedT m)
diff --git a/src/Data/Annotated/Generic/Unsafe.hs b/src/Data/Annotated/Generic/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Annotated/Generic/Unsafe.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE BangPatterns #-}
+module Data.Annotated.Generic.Unsafe
+  ( Annotated
+  , runAnnotated, evalAnnotated, execAnnotated
+  , AnnotatedT(..)
+  , runAnnotatedT, evalAnnotatedT, execAnnotatedT
+  , module Control.Monad
+  , module Control.Monad.Fix
+  , module Control.Monad.Annotated.Class
+  ) where
+
+import Data.Functor.Contravariant
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Signatures
+import Control.Monad.Fix
+import Control.Monad.State
+import Control.Monad.Fail
+import Control.Monad.Identity (Identity, runIdentity)
+
+import Control.Monad.Cont.Class
+import Control.Monad.Error.Class
+import Control.Monad.Reader.Class
+import Control.Monad.Writer.Class
+import Control.Monad.RWS.Class
+
+import System.Mem.StableMap
+import Control.Monad.Annotated.Class
+
+import BinderAnn.SrcInfo
+
+-----------------------------------------------------------------------------
+-- | An annotation monad parameterized by the type @ann@ of the annotation to
+-- carry.
+
+type Annotated a = AnnotatedT Identity a
+
+runAnnotated :: forall a. Annotated a -> (a, StableMap SrcInfo)
+runAnnotated = runIdentity . runAnnotatedT
+
+evalAnnotated :: forall a. Annotated a -> a
+evalAnnotated = fst . runAnnotated
+
+execAnnotated :: forall a. Annotated a -> StableMap SrcInfo
+execAnnotated = snd . runAnnotated
+
+----------------------------------------
+-- The mighty AnnotatedT monad transformer!
+
+newtype AnnotatedT m a =
+  AnnotatedT { unAnnotateT :: StateT (StableMap SrcInfo) m a }
+  deriving
+    ( Functor, Contravariant
+    , Applicative, Alternative
+    , Monad, MonadIO, MonadFail, MonadFix, MonadTrans
+    )
+
+-- runners
+runAnnotatedT :: forall m a. AnnotatedT m a -> m (a, StableMap SrcInfo)
+runAnnotatedT = flip runStateT emptyStableMap . unAnnotateT
+
+evalAnnotatedT :: forall m a. Monad m => AnnotatedT m a -> m a
+evalAnnotatedT m = fst <$> runAnnotatedT m
+
+execAnnotatedT :: forall m a. Monad m => AnnotatedT m a -> m (StableMap SrcInfo)
+execAnnotatedT m = snd <$> runAnnotatedT m
+
+-- actions over annotations
+createAnn_ :: Monad m => a -> SrcInfo -> AnnotatedT m ()
+createAnn_ !a ann = AnnotatedT . StateT $ \anns ->
+  return ((), insertStableNameUnsafe a ann anns)
+
+lookupAnn_ :: Monad m => a -> AnnotatedT m (Maybe SrcInfo)
+lookupAnn_ !a = AnnotatedT . StateT $ \anns ->
+  return (lookupStableNameUnsafe a anns, anns)
+
+instance Monad m => MonadAnnotated (AnnotatedT m) where
+  createAnn = createAnn_
+  lookupAnn = lookupAnn_
+
+----------------------------------------
+-- Lifting AnnotatedT to support other effects
+
+{-# INLINE liftCallCC #-}
+liftCallCC :: CallCC m (a, StableMap SrcInfo) (b, StableMap SrcInfo)
+           -> CallCC (AnnotatedT m) a b
+liftCallCC callCC_ f = AnnotatedT . StateT $ \s ->
+  callCC_ $ \c ->
+  runStateT (unAnnotateT (f (\a -> AnnotatedT . StateT $ \s' -> c (a, s')))) s
+
+{-# INLINE liftCatch #-}
+liftCatch :: Catch e m (a, StableMap SrcInfo) -> Catch e (AnnotatedT m) a
+liftCatch catchE m h = AnnotatedT . StateT $ \ s ->
+  runStateT (unAnnotateT m) s `catchE` \ e -> runStateT (unAnnotateT (h e)) s
+
+
+{-# INLINE mapAnnotatedT #-}
+mapAnnotatedT :: (m (a, StableMap SrcInfo) -> n (b, StableMap SrcInfo))
+              -> AnnotatedT m a
+              -> AnnotatedT n b
+mapAnnotatedT f m = AnnotatedT . StateT $ \anns ->
+  f (runStateT (unAnnotateT m) anns)
+
+{-# INLINE liftListen #-}
+liftListen :: Monad m
+           => Listen w m (a, StableMap SrcInfo)
+           -> Listen w (AnnotatedT m) a
+liftListen listen_ m = AnnotatedT . StateT $ \anns -> do
+  ~((a, anns'), w) <- listen_ (runStateT (unAnnotateT m) anns)
+  return ((a, w), anns')
+
+{-# INLINE liftPass #-}
+liftPass :: Monad m
+         => Pass w m (a, StableMap SrcInfo)
+         -> Pass w (AnnotatedT m) a
+liftPass pass_ m = AnnotatedT . StateT $ \anns -> pass_ $ do
+    ~((a, f), anns') <- runStateT (unAnnotateT m) anns
+    return ((a, anns'), f)
+
+instance MonadCont m => MonadCont (AnnotatedT m) where
+    callCC = liftCallCC callCC
+
+instance MonadError e m => MonadError e (AnnotatedT m) where
+  throwError = lift . throwError
+  catchError = liftCatch catchError
+
+instance MonadReader r m => MonadReader r (AnnotatedT m) where
+  ask   = lift ask
+  local = mapAnnotatedT . local
+  reader = lift . reader
+
+instance MonadWriter w m => MonadWriter w (AnnotatedT m) where
+  writer = lift . writer
+  tell   = lift . tell
+  listen = liftListen listen
+  pass   = liftPass pass
+
+instance MonadState s m => MonadState s (AnnotatedT m) where
+  get = lift get
+  put = lift . put
+  state = lift . state
+
+instance MonadRWS r w s m => MonadRWS r w s (AnnotatedT m)
diff --git a/src/Data/Annotated/Monadic.hs b/src/Data/Annotated/Monadic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Annotated/Monadic.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Data.Annotated.Monadic where
+
+import BinderAnn.SrcInfo
+
+----------------------------------------
+-- Monadic types that can be annotated using some effect
+
+class Monad m => AnnotatedM m a where
+  annotateM :: m a -> SrcInfo -> m a
+
+instance {-# INCOHERENT #-} Monad m => AnnotatedM m a where
+  annotateM ma _ = ma
diff --git a/src/Data/Annotated/Pure.hs b/src/Data/Annotated/Pure.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Annotated/Pure.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Data.Annotated.Pure where
+
+import BinderAnn.SrcInfo
+
+----------------------------------------
+-- Pure types that can be annotated by default
+
+class Annotated a where
+  annotate :: a -> SrcInfo -> a
+
+instance {-# INCOHERENT #-} Annotated a where
+  annotate a _ = a
+
+-- Annotate the return value of a monadic computation
+annotateM :: (Monad m, Annotated a) => m a -> SrcInfo -> m a
+annotateM ma ann = do
+  a <- ma
+  return (annotate a ann)
diff --git a/src/System/Mem/StableMap.hs b/src/System/Mem/StableMap.hs
new file mode 100644
--- /dev/null
+++ b/src/System/Mem/StableMap.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE MagicHash #-}
+module System.Mem.StableMap where
+
+import Control.Monad.IO.Class
+import System.Mem.StableName
+import System.IO.Unsafe
+import Unsafe.Coerce
+import GHC.Types (Any)
+
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+
+-- import GHC.Base (stableNameToInt#)
+
+----------------------------------------
+-- Dynamic stable names
+
+newtype DynStableName = DynStableName (StableName Any)
+
+instance Eq DynStableName where
+  DynStableName sn == DynStableName sn' = sn `eqStableName` sn'
+
+makeDynStableName :: MonadIO m => a -> m DynStableName
+makeDynStableName a =
+  liftIO (wrapStableName <$> makeStableName a)
+
+makeDynStableNameUnsafe :: a -> DynStableName
+makeDynStableNameUnsafe a =
+  unsafePerformIO (wrapStableName <$> makeStableName a)
+
+wrapStableName :: StableName a -> DynStableName
+wrapStableName s = DynStableName (unsafeCoerce s)
+
+hashDynStableName :: DynStableName -> Int
+hashDynStableName (DynStableName sn) = hashStableName sn
+
+----------------------------------------
+-- Stable maps
+
+type StableMap a = IntMap [(DynStableName, a)]
+
+emptyStableMap :: StableMap v
+emptyStableMap = IntMap.empty
+
+insertStableName :: MonadIO m => a -> b -> StableMap b -> m (StableMap b)
+insertStableName a b sm = do
+  sna <- makeDynStableName a
+  return (IntMap.insertWith (<>) (hashDynStableName sna) [(sna,b)] sm)
+
+lookupStableName :: MonadIO m => a -> StableMap b -> m (Maybe b)
+lookupStableName a sm = do
+  sna <- makeDynStableName a
+  case IntMap.lookup (hashDynStableName sna) sm of
+    Just pairs -> return (Prelude.lookup sna pairs)
+    Nothing    -> return Nothing
+
+insertStableNameUnsafe :: a -> b -> StableMap b -> StableMap b
+insertStableNameUnsafe a b sm =
+  let sna = makeDynStableNameUnsafe a
+  in IntMap.insertWith insertReplace' (hashDynStableName sna) [(sna,b)] sm
+
+
+lookupStableNameUnsafe :: a -> StableMap b -> Maybe b
+lookupStableNameUnsafe a sm =
+  let sna = makeDynStableNameUnsafe a
+  in case IntMap.lookup (hashDynStableName sna) sm of
+       Just pairs -> Prelude.lookup sna pairs
+       Nothing    -> Nothing
+
+insertReplace' :: [(DynStableName, a)] -> [(DynStableName, a)] -> [(DynStableName, a)]
+insertReplace' ((k,v):_) = insertReplace k v
+insertReplace' _         = id
+
+insertReplace :: DynStableName -> a -> [(DynStableName, a)] -> [(DynStableName, a)]
+insertReplace k v [] = [(k, v)]
+insertReplace k v ((k', v') : xs)
+ | k == k'   = (k, v)   : xs
+ | otherwise = (k', v') : insertReplace k v xs
diff --git a/test/Generic.hs b/test/Generic.hs
new file mode 100644
--- /dev/null
+++ b/test/Generic.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC
+  -fplugin     BinderAnn.Generic
+  -fplugin-opt BinderAnn.Generic:manual
+#-}
+
+module Generic where
+
+import Control.Monad.State
+import Control.Monad.Except
+
+import BinderAnn.Generic
+
+----------------------------------------
+-- Example 1: Arithmetic expressions
+----------------------------------------
+
+data EvalError =
+  DivByZero (Maybe SrcInfo)
+  deriving Show
+
+type MonadEval m =
+  ( MonadAnnotated           m
+  , MonadError     EvalError m
+  , MonadIO                  m
+  )
+
+type Eval = AnnotatedT (ExceptT EvalError IO)
+
+runEval :: Eval a -> IO (Either EvalError a)
+runEval = runExceptT . evalAnnotatedT
+
+divByZeroError :: MonadEval m => a -> m b
+divByZeroError x = lookupAnn x >>= throwError . DivByZero
+
+-- the DSL
+
+lit :: MonadEval m => Int -> m Int
+lit = return
+
+(|+|) :: MonadEval m => Int -> Int -> m Int
+(|+|) x y = lit (x + y)
+
+(|-|) :: MonadEval m => Int -> Int -> m Int
+(|-|) x y = lit (x - y)
+
+(|*|) :: MonadEval m => Int -> Int -> m Int
+(|*|) x y = lit (x * y)
+
+(|/|) :: MonadEval m => Int -> Int -> m Int
+(|/|) x y | y == 0    = divByZeroError y
+          | otherwise = lit (x `div` y)
+
+
+-- some tests
+{-# ANN test1 SrcInfo #-}
+test1 :: MonadEval m => m Int
+test1 = do
+  zero <- lit 0
+  one  <- lit 1
+  false <- return False
+  liftIO $ print (zero, one)
+  one |/| zero
+
+----------------------------------------
+-- entry point
+----------------------------------------
+
+tests :: IO ()
+tests = do
+  putStrLn "test1:"
+  runEval test1 >>= print
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,15 @@
+module Main where
+
+import qualified Pure
+import qualified Monadic
+import qualified Generic
+
+main :: IO ()
+main = do
+  putStrLn "\n== Pure ================================\n"
+  Pure.tests
+  putStrLn "\n== Monadic =============================\n"
+  Monadic.tests
+  putStrLn "\n== Generic =============================\n"
+  Generic.tests
+  putStrLn "\n========================================\n"
diff --git a/test/Monadic.hs b/test/Monadic.hs
new file mode 100644
--- /dev/null
+++ b/test/Monadic.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ConstraintKinds #-}
+
+{-# OPTIONS_GHC
+  -fplugin     BinderAnn.Monadic
+  -fplugin-opt BinderAnn.Monadic:manual
+#-}
+
+module Monadic where
+
+import Prelude hiding (lookup)
+import qualified Data.List as List
+
+import Control.Monad.State
+import Control.Monad.Except
+
+import BinderAnn.Monadic
+
+----------------------------------------
+-- Example 1: Statefull arithmetic evaluator
+----------------------------------------
+
+-- the state layer
+newtype Var = Var Int deriving (Show, Eq)
+type Env = [(Var, Double)]
+type CallStack = [SrcInfo]
+
+data EvalState =
+  EvalState
+  { st_uniq   :: Var
+  , st_env    :: Env
+  , st_stack  :: CallStack
+  } deriving Show
+
+emptyState :: EvalState
+emptyState = EvalState (Var 0) [] []
+
+-- the error handling layer
+data EvalError =
+  VarNotFound CallStack Var
+  | DivByZero CallStack
+  deriving Show
+
+----------------------------------------
+-- the evaluation monad
+
+type MonadEval m =
+  ( MonadState EvalState m
+  , MonadError EvalError m
+  )
+
+type Eval = StateT EvalState (ExceptT EvalError IO)
+
+runEval :: Eval Double -> IO (Either EvalError Double)
+runEval = runExceptT . flip evalStateT emptyState
+
+getEnv :: MonadEval m => m Env
+getEnv = gets st_env
+
+getCallStack :: MonadEval m => m CallStack
+getCallStack = gets st_stack
+
+lookup :: MonadEval m => Var -> m Double
+lookup i = do
+  e <- getEnv
+  case List.lookup i e of
+    Just n  -> return n
+    Nothing -> do
+      stack <- getCallStack
+      throwError (VarNotFound stack i)
+
+store :: MonadEval m => Double -> m Var
+store n = state $ \(EvalState (Var u) e p) ->
+  (Var u, EvalState (Var (u + 1)) ((Var u, n) : e) p)
+
+binop :: MonadEval m => (Double -> Double -> Double) -> m Var -> m Var -> m Var
+binop f ex ey = do
+  x <- lookup =<< ex
+  y <- lookup =<< ey
+  store (f x y)
+
+----------------------------------------
+-- annotation support
+
+instance AnnotatedM Eval a where
+  annotateM m info =
+    -- Note; using a do statement here will produce an infinite annotation loop!
+    -- In practice this shouldn't happen, as this instance won't appear in a
+    -- module using the plugin.
+    modify (\st -> st { st_stack = info : st_stack st }) >> m
+
+----------------------------------------
+-- the DSL
+
+var :: MonadEval m => Var -> m Var
+var = return
+
+lit :: MonadEval m => Double -> m Var
+lit = store
+
+ret :: MonadEval m => m Var -> m Double
+ret ex = lookup =<< ex
+
+(.+) :: MonadEval m => m Var -> m Var -> m Var
+(.+) = binop (+)
+(.-) :: MonadEval m => m Var -> m Var -> m Var
+(.-) = binop subtract
+(.*) :: MonadEval m => m Var -> m Var -> m Var
+(.*) = binop (*)
+
+(./) :: MonadEval m => m Var -> m Var -> m Var
+(./) ex ey = do
+  y <- ey
+  vy <- lookup y
+  if vy /= 0
+    then binop (/) ex ey
+    else do
+      stack <- getCallStack
+      throwError (DivByZero stack)
+
+----------------------------------------
+-- tests
+
+{-# ANN test1 SrcInfo #-}
+test1 :: Eval Double
+test1 = do
+  x <- lit 0
+  y <- lit 3 .+ var x
+  ret (var y ./ var x)
+
+{-# ANN test2 SrcInfo #-}
+test2 :: Eval Double
+test2 = do
+  x <- lit 3 .+ var (Var 123)
+  ret (var x)
+
+-- a test for Maciej's use case
+newtype Foo a = Foo a
+
+litFoo :: Double -> Eval (Foo Var)
+litFoo x = Foo <$> lit x
+
+{-# ANN test3 SrcInfo #-}
+test3 :: Eval Double
+test3 = do
+  Foo x <- litFoo 42
+  ret (var x ./ lit 0)
+
+----------------------------------------
+-- entry point
+----------------------------------------
+
+tests :: IO ()
+tests = do
+  putStrLn "test1:"
+  runEval test1 >>= print
+  putStrLn "test2:"
+  runEval test2 >>= print
+  putStrLn "test3:"
+  runEval test3 >>= print
+  return ()
diff --git a/test/Pure.hs b/test/Pure.hs
new file mode 100644
--- /dev/null
+++ b/test/Pure.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-# OPTIONS_GHC
+  -fplugin     BinderAnn.Pure
+  -fplugin-opt BinderAnn.Pure:infix=@@
+#-}
+
+module Pure where
+
+import Control.Monad.Writer
+import Control.Monad.Identity
+
+import BinderAnn.Pure
+
+data Exp =
+    Val Int
+  | Add Exp Exp
+  | Ann Exp SrcInfo
+  deriving Show
+
+type Eval = WriterT [SrcInfo] Identity
+
+instance Annotated Exp where
+  annotate = Ann
+
+runEval :: Eval Exp -> (Int, [SrcInfo])
+runEval e = runIdentity (runWriterT (eval =<< e))
+
+runEval' :: Eval Exp -> Exp
+runEval' = fst . runIdentity . runWriterT
+
+eval :: Exp -> Eval Int
+eval (Val n) = return n
+eval (Add x y) = liftM2 (+) (eval x) (eval y)
+eval (Ann x a) = tell [a] >> eval x
+
+val :: Int -> Eval Exp
+val n = return (Val n)
+
+(|+|) :: Exp -> Exp -> Eval Exp
+x |+| y = return (Add x y)
+
+
+test1 = runEval @@ do
+  (x, y) <- (,) <$> val 10 <*> val 5
+  z  <- return False
+  w  <- (if z then val 1 else val 2)
+  s1 <- x |+| y
+  s1 |+| w
+
+tests :: IO ()
+tests = do
+  putStrLn "test1:"
+  print test1