diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,11 @@
+# 0.2.1
+
+- Add `Overloaded:Categories`, which makes `Arrows` notation desugar to
+  categories, a bit like in Conal Elliot's *Compiling to Categories*.
+- Add `Overloaded:Do`, which is like *Local Do*
+- Add `Overloaded:Unit`, which overloads value `()` to be whatever you want
+- GHC-8.10 support
+
 # 0.2
 
 - Make infixr 5 cons
diff --git a/example/AD.hs b/example/AD.hs
new file mode 100644
--- /dev/null
+++ b/example/AD.hs
@@ -0,0 +1,232 @@
+{-# LANGUAGE Arrows              #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Categories #-}
+module Main where
+
+import Numeric (showFFloat)
+
+import qualified Control.Category
+import qualified Numeric.LinearAlgebra as LA
+
+import Overloaded.Categories
+import VectorSpace
+
+evalL :: (HasDim a, HasDim b) => L a b -> LA.Matrix Double
+evalL (L f) = toRawMatrix (f LI)
+
+-- | A Function which computes value and derivative at the point.
+newtype AD a b = AD (a -> (b, L a b))
+
+instance Category AD where
+    id = AD (\x -> (x, L id))
+
+    AD g . AD f = AD $ \a ->
+        let (b, L f') = f a
+            (c, L g') = g b
+        in (c, L (g' . f'))
+
+instance CategoryWith1 AD where
+    type Terminal AD = ()
+
+    terminal = AD (const ((), terminal))
+
+instance CartesianCategory AD where
+    type Product AD = (,)
+
+    proj1 = AD (\x -> (fst x, proj1))
+    proj2 = AD (\x -> (snd x, proj2))
+
+    fanout (AD f) (AD g) = AD $ \a ->
+        let (b, f') = f a
+            (c, g') = g a
+        in ((b, c), fanout f' g')
+
+instance GeneralizedElement AD where
+    type Object AD a = a
+
+    konst x = AD (\_ -> (x, L $ \_ -> LZ))
+
+ladd :: LinMap r (a, a) -> LinMap r a
+ladd (LH f g) = LA f g
+ladd (LV f g) = LV (ladd f) (ladd g)
+ladd (LA a b) = LA (ladd a) (ladd b)
+ladd (LK k f) = LK k (ladd f)
+ladd LZ       = LZ
+ladd LI       = LV LI LI
+
+lmult :: Double -> Double -> LinMap r (a, a) -> LinMap r a
+lmult x y (LH f g) = LA (LK y f) (LK x g)
+lmult x y (LV f g) = LV (lmult x y f) (lmult x y g)
+lmult x y (LA f g) = LA (lmult x y f) (lmult x y g)
+lmult x y (LK k f) = LK k (lmult x y f)
+lmult _ _ LZ       = LZ
+lmult x y LI       = LV (LK y LI) (LK x LI)
+
+plus :: AD (Double, Double) Double
+plus = AD $ \(x,y) -> (x + y, L ladd)
+
+minus :: AD (Double, Double) Double
+minus = AD $ \(x,y) -> (x - y, L $ lmult (-1) 1)
+
+mult :: AD (Double, Double) Double
+mult = AD $ \(x,y) -> (x * y, L $ lmult x y)
+
+scale :: Double -> AD Double Double
+scale k = AD $ \x -> (k * x, linear k)
+
+evaluateAD :: (HasDim a, HasDim b) => AD a b -> a -> (b, LA.Matrix Double)
+evaluateAD (AD f) x = let (y, f') = f x in (y, evalL f')
+
+-------------------------------------------------------------------------------
+-- Simple examples
+-------------------------------------------------------------------------------
+
+ex1 :: AD Double Double
+ex1 = plus %% fanout identity identity
+
+ex2 :: AD Double Double
+ex2 = mult %% fanout identity identity
+
+-------------------------------------------------------------------------------
+-- Quadratic function
+-------------------------------------------------------------------------------
+
+quad :: AD (Double, Double) Double
+quad = proc (x, y) -> do
+    x2  <- mult    -< (x, x)
+    y2  <- mult    -< (y, y)
+    tmp <- plus    -< (x2, y2)
+    z   <- konst 5 -< ()
+    plus -< (tmp, z)
+
+-------------------------------------------------------------------------------
+-- Newton
+-------------------------------------------------------------------------------
+
+findZero :: AD Double Double -> Double -> [Double]
+findZero f x0 = take 10 results
+  where
+    results = iterate go x0
+
+    go :: Double -> Double
+    go x =
+        let (y, m) = evaluateAD f x
+            [[y']] = LA.toLists m
+        in x - gamma * (y / y')
+
+    gamma = 0.1
+
+-------------------------------------------------------------------------------
+-- Gradient descent
+-------------------------------------------------------------------------------
+
+gradDesc :: forall a. VectorSpace a => AD a Double -> a -> [a]
+gradDesc f = iterate go where
+    go :: a -> a
+    go x =
+        let (_, m) = evaluateAD f x
+            [grad] = LA.toLists $ LA.tr $ LA.scale gamma m
+
+        in fromVector $ zipWith (-) (toVector x) grad
+
+    gamma = 0.1
+
+-------------------------------------------------------------------------------
+-- ML stuff
+-------------------------------------------------------------------------------
+
+tanhAD :: AD Double Double
+tanhAD = AD $ \x ->
+    let y = tanh x
+    in (y, linear (1 - y * y))
+
+sigmoidAD :: AD Double Double
+sigmoidAD = AD $ \x ->
+    let y = 1 / (1 + exp (- x))
+    in (x, linear (y * (1 - y)))
+
+
+-- no biases
+type Weights = ((((Double, Double), (Double, Double)), ((Double, Double), (Double, Double))), Double)
+
+startWeights :: Weights
+startWeights = ((((0.1, 0.2), (0.3, 0.4)), ((0.5, 0.6), (0.7, 0.8))), 0.9)
+
+--
+-- @
+-- x ----> u ---,
+--     X        output
+-- y ----> v ---^
+-- @
+network :: AD (Weights, (Double, Double)) Double
+network = proc (((((w11,w12),(w21,w22)),((b1, b2), (z1, z2))), bend), (x, y)) -> do
+    x1 <- mult   -< (x, w11)
+    y1 <- mult   -< (y, w12)
+    u0 <- plus   -< (x1, y1)
+    u1 <- plus   -< (u0, b1)
+    u2 <- tanhAD -< u1
+
+    x2 <- mult   -< (x, w21)
+    y2 <- mult   -< (y, w22)
+    v0 <- plus   -< (x2, y2)
+    v1 <- plus   -< (v0, b2)
+    v2 <- tanhAD -< v1
+
+    u <- mult -< (u2, z1)
+    v <- mult -< (v2, z2)
+
+    output' <- plus -< (u, v)
+    output <- plus -< (bend, output')
+    tanhAD -< output
+
+networkError :: AD Weights Double
+networkError = proc ws -> do
+    -- xor!
+    s1 <- ex 1 1 0 -< ws
+    s2 <- ex 0 0 0 -< ws
+    s3 <- ex 1 0 1 -< ws
+    s4 <- ex 0 1 1 -< ws
+
+    tmp1 <- plus -< (s1, s2)
+    tmp2 <- plus -< (s3, s4)
+    plus -< (tmp1, tmp2)
+
+  where
+    ex :: Double -> Double -> Double -> AD Weights Double
+    ex x y z = proc ws -> do
+         x1 <- konst x -< ()
+         y1 <- konst y -< ()
+         e1 <- konst z -< ()
+         a1 <- network -< (ws, (x1, y1))
+         r1 <- minus   -< (e1, a1)
+         mult    -< (r1, r1)
+
+train :: Weights
+train = gradDesc networkError startWeights !! 500
+
+-------------------------------------------------------------------------------
+-- Main
+-------------------------------------------------------------------------------
+
+main :: IO ()
+main = do
+    putStrLn $ "quad (2,3) = " ++ show (evaluateAD quad (2,3))
+    putStrLn $ "gradDesc quad (2,3) = " ++ show (gradDesc quad (2,3) !! 30)
+
+    print $ evaluateAD tanhAD 1
+    print $ evaluateAD sigmoidAD 1
+
+    putStrLn "Training the net (for xor)"
+    let ws = train
+    putStrLn $ "Parameters = " ++ show (toVector ws)
+    putStrLn $ "Error = " ++ show (fst $ evaluateAD networkError ws)
+    let example xy =
+          putStrLn $ "eval " ++ show xy ++ " = " ++ showFFloat (Just 2) (fst $ evaluateAD network (ws, xy)) ""
+    example (0, 0)
+    example (0, 1)
+    example (1, 0)
+    example (1, 1)
diff --git a/example/Boring.hs b/example/Boring.hs
new file mode 100644
--- /dev/null
+++ b/example/Boring.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TypeOperators    #-}
+{-# OPTIONS -fplugin=Overloaded
+            -fplugin-opt=Overloaded:Unit=Data.Boring.boring #-}
+module Main (main) where
+
+import Data.Constraint    (Dict (..))
+import Data.Type.Equality ((:~:) (..))
+import Data.Void          (Void)
+import Test.HUnit         ((@?=))
+
+main :: IO ()
+main = do
+    -- vanilla unit
+    let ex1 :: ()
+        ex1 = ()
+    () @?= ex1
+
+    -- Boring instances
+    let ex2 :: [Void]
+        ex2 = ()
+
+    [] @?= ex2
+
+    let ex3 :: Dict (Ord [(Int, Char)])
+        ex3 = ()
+
+    let ex4 :: (Int :~: Int, ())
+        ex4 = ()
+    (Refl, ()) @?= ex4
diff --git a/example/LocalDo.hs b/example/LocalDo.hs
new file mode 100644
--- /dev/null
+++ b/example/LocalDo.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Do #-}
+module Main (main) where
+
+import Data.Kind (Type)
+import Overloaded
+import System.Timeout (timeout)
+import Data.Maybe (fromMaybe)
+
+-- Idea / example by Vladislav Zavialov (int-inded) from:
+-- https://github.com/ghc-proposals/ghc-proposals/pull/216#issuecomment-614771416
+
+main :: IO ()
+main = do
+    putStrLn "Enter string, you have 10 seconds..."
+    str <- fromMaybe "timed out..." <$> timeout 10000000 getLine
+    let customIO :: forall (method :: DoMethod) ty. CustomIO method ty => ty 
+        customIO = makeCustomIO @method @ty str
+    customIO.do
+        putStrLn "Hello"
+        putStrLn "World"
+
+-------------------------------------------------------------------------------
+-- CustomDo
+-------------------------------------------------------------------------------
+
+class CustomIO (method :: DoMethod) (ty :: Type) where
+    makeCustomIO :: String -> ty
+
+instance (ty ~ (a -> IO a)                  ) => CustomIO 'Pure ty where
+    makeCustomIO _   = pure
+instance (ty ~ (IO a -> IO b -> IO b)       ) => CustomIO 'Then ty where
+    makeCustomIO str x y = do
+        _ <- x
+        putStrLn $ "--- " ++ str ++ " ---"
+        y
+instance (ty ~ (IO a -> (a -> IO b) -> IO b)) => CustomIO 'Bind ty where
+    makeCustomIO str m k = do
+        x <- m
+        putStrLn $ "--- " ++ str ++ " ---"
+        k x
diff --git a/example/VectorSpace.hs b/example/VectorSpace.hs
new file mode 100644
--- /dev/null
+++ b/example/VectorSpace.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall #-}
+-- | This module is wrongly named.
+module VectorSpace (
+    LinMap (..),
+    HasDim(Dim, dimDict),
+    toRawMatrix,
+    L (..),
+    linear,
+    VectorSpace (..),
+    toVector,
+    fromVector,
+) where
+
+import Data.Constraint       ((:-), Dict (..), withDict)
+import Data.Proxy            (Proxy (..))
+import GHC.TypeLits
+import Overloaded.Categories
+
+import qualified Control.Category
+import qualified Data.Constraint.Nat   as C
+import qualified Numeric.LinearAlgebra as L
+
+-- import qualified Numeric.LinearAlgebra.Static as LS
+
+data LinMap a b where
+    LZ :: LinMap a b
+    LI :: LinMap a a
+    LH :: LinMap a b -> LinMap a c -> LinMap a (b, c)
+    LV :: LinMap a c -> LinMap b c -> LinMap (a, b) c
+    LA :: LinMap a b -> LinMap a b -> LinMap a b
+    LK :: Double -> LinMap a b -> LinMap a b
+
+deriving instance Show (LinMap a b)
+
+lcomp :: LinMap b c -> LinMap a b -> LinMap a c
+lcomp LZ       _        = LZ
+lcomp _        LZ       = LZ
+lcomp LI       h        = h
+lcomp h        LI       = h
+lcomp (LK k f) (LK l g) = LK (k * l) (lcomp f g)
+lcomp (LK k f) h        = LK k (lcomp f h)
+lcomp f        (LK k h) = LK k (lcomp f h)
+lcomp (LA f g) h        = LA (lcomp f h) (lcomp g h)
+lcomp f        (LA g h) = LA (lcomp f g) (lcomp f h)
+lcomp (LH f g) h        = LH (lcomp f h) (lcomp g h)
+lcomp h        (LV f g) = LV (lcomp h f) (lcomp h g)
+lcomp (LV f g) (LH u v) = LA (lcomp f u) (lcomp g v)
+
+instance Category LinMap where
+    id = LI
+    (.) = lcomp
+
+instance CategoryWith1 LinMap where
+    type Terminal LinMap = ()
+    terminal = LZ
+
+instance CartesianCategory LinMap where
+    type Product LinMap = (,)
+    proj1  = LV LI LZ
+    proj2  = LV LZ LI
+    fanout = LH
+
+instance CocartesianCategory LinMap where
+    type Coproduct LinMap = (,)
+    inl   = LH LI LZ
+    inr   = LH LZ LI
+    fanin = LV
+
+instance BicartesianCategory LinMap where
+    distr = LH
+        (LH (LV (LV LI LZ) LZ) (LV LZ LI))
+        (LH (LV (LV LZ LI) LZ) (LV LZ LI))
+
+newtype L a b = L (forall r. LinMap r a -> LinMap r b)
+
+lfst :: LinMap a (b, c) -> LinMap a b
+lfst (LA f g) = LA (lfst f) (lfst g)
+lfst (LK k f) = LK k (lfst f)
+lfst (LH f _) = f
+lfst (LV f g) = LV (lfst f) (lfst g)
+lfst LZ       = LZ
+lfst LI       = LV LI LZ
+
+lsnd :: LinMap a (b, c) -> LinMap a c
+lsnd (LH _ g)     = g
+lsnd (LA f g)   = LA (lsnd f) (lsnd g)
+lsnd (LK k f) = LK k (lsnd f)
+lsnd (LV f g)     = LV (lsnd f) (lsnd g)
+lsnd LZ           = LZ
+lsnd LI           = LV LZ LI
+
+linear :: Double -> L a a
+linear k = L $ LK k
+
+-- lmult :: Double -> Double -> LinMap r (a, a) -> LinMap r a
+-- lmult x y (LH f g) = LA (LK y f) (LK x g)
+-- lmult x y (LV f g) = LV (lmult x y f) (lmult x y g)
+-- lmult x y (LA f g) = LA (lmult x y f) (lmult x y g)
+-- lmult x y (LK k f) = LK k (lmult x y f)
+-- lmult _ _ LZ       = LZ
+-- lmult x y LI       = LV (LK y LI) (LK x LI)
+
+instance Category L where
+    id = L id
+    L f . L g = L (f . g)
+
+instance CategoryWith1 L where
+    type Terminal L = ()
+
+    terminal = L (\_ -> LZ)
+
+instance CartesianCategory L where
+    type Product L = (,)
+
+    proj1 = L lfst
+    proj2 = L lsnd
+
+    fanout (L f) (L g) = L $ \x -> LH (f x) (g x)
+
+-- Is this correct?
+instance CocartesianCategory L where
+    type Coproduct L = (,)
+
+    inl = L $ \f -> LH f LZ
+    inr = L $ \g -> LH LZ g
+
+    fanin (L f) (L g) = L $ \x -> LA (f (lfst x)) (g (lsnd x))
+
+class HasDim a where
+    type Dim a :: Nat
+
+    dimDict :: Proxy a -> Dict (KnownNat (Dim a))
+
+    splitPair :: (a ~ (b, c)) => (Dict (HasDim b), Dict (HasDim c))
+    splitPair = error "impossible: splitPair"
+
+instance HasDim () where
+    type Dim () = 0
+    dimDict _ = Dict
+
+instance HasDim Double where
+    type Dim Double = 1
+    dimDict _ = Dict
+
+instance (HasDim a, HasDim b) => HasDim (a, b) where
+    type Dim (a, b) = Dim a + Dim b
+
+    dimDict _ =
+        withDimDict (Proxy :: Proxy a) $
+        withDimDict (Proxy :: Proxy b) $
+        withDict (C.plusNat :: (KnownNat (Dim a), KnownNat (Dim b)) :- KnownNat (Dim a + Dim b))
+        Dict
+
+    splitPair = (Dict, Dict)
+
+
+withDimDict :: HasDim a => Proxy a -> (KnownNat (Dim a) => r) -> r
+withDimDict p = withDict (dimDict p)
+
+dim :: forall a. HasDim a => Proxy a -> Int
+dim p = withDimDict p $ fromInteger $ natVal (Proxy :: Proxy (Dim a))
+
+toRawMatrix :: forall a b. (HasDim a, HasDim b) => LinMap a b -> L.Matrix Double
+toRawMatrix LZ       = (dim (Proxy :: Proxy a) L.>< dim (Proxy :: Proxy b)) (repeat 0)
+toRawMatrix LI       = L.ident (dim (Proxy :: Proxy a))
+toRawMatrix (LA f g) = L.add (toRawMatrix f) (toRawMatrix g)
+toRawMatrix (LK k f) = L.scale k (toRawMatrix f)
+toRawMatrix (LH f g) = go splitPair f g where
+    go :: (Dict (HasDim x), Dict (HasDim y)) -> LinMap a x -> LinMap a y -> L.Matrix Double
+    go (Dict, Dict) f' g' = toRawMatrix f' L.||| toRawMatrix g'
+toRawMatrix (LV f g) = go splitPair f g where
+    go :: (Dict (HasDim x), Dict (HasDim y)) -> LinMap x b -> LinMap y b -> L.Matrix Double
+    go (Dict, Dict) f' g' = toRawMatrix f' L.=== toRawMatrix g'
+
+-- toStaticMatrix :: forall a b. (HasDim a, HasDim b) => LinMap a b -> LS.L (Dim a) (Dim b)
+-- toStaticMatrix LZ =
+--     withDimDict (Proxy :: Proxy a) $
+--     withDimDict (Proxy :: Proxy b) 0
+-- toStaticMatrix LI =
+--     withDimDict (Proxy :: Proxy a) LS.eye
+-- toStaticMatrix (LA f g) =
+--     withDimDict (Proxy :: Proxy a) $
+--     withDimDict (Proxy :: Proxy b) $
+--     L.add (toStaticMatrix f) (toStaticMatrix g)
+-- toStaticMatrix (LK k f) =
+--     withDimDict (Proxy :: Proxy a) $
+--     withDimDict (Proxy :: Proxy b) $
+--     toStaticMatrix f LS.<> LS.diag (LS.konst k)
+-- toStaticMatrix (LH f g) = go splitPair f g where
+--     go :: forall x y. (x,y) ~ b => (Dict (HasDim x), Dict (HasDim y)) -> LinMap a x -> LinMap a y -> LS.L (Dim a) (Dim x + Dim y)
+--     go (Dict, Dict) f' g' =
+--         withDimDict (Proxy :: Proxy a) $
+--         withDimDict (Proxy :: Proxy b) $
+--         withDimDict (Proxy :: Proxy x) $
+--         withDimDict (Proxy :: Proxy y) $
+--         toStaticMatrix f' LS.||| toStaticMatrix g'
+-- toStaticMatrix (LV f g) = go splitPair f g where
+--     go :: forall x y. (x,y) ~ a => (Dict (HasDim x), Dict (HasDim y)) -> LinMap x b -> LinMap y b -> LS.L (Dim x + Dim y) (Dim b)
+--     go (Dict, Dict) f' g' =
+--         withDimDict (Proxy :: Proxy a) $
+--         withDimDict (Proxy :: Proxy b) $
+--         withDimDict (Proxy :: Proxy x) $
+--         withDimDict (Proxy :: Proxy y) $
+--         toStaticMatrix f' LS.=== toStaticMatrix g'
+
+-------------------------------------------------------------------------------
+-- Vector space
+-------------------------------------------------------------------------------
+
+class HasDim a => VectorSpace a where
+    toVector' :: a -> [Double] -> [Double]
+
+    fromVector' :: [Double] -> (a -> [Double] -> r) -> r
+
+toVector :: VectorSpace a => a -> [Double]
+toVector x = toVector' x []
+
+fromVector :: VectorSpace a => [Double] -> a
+fromVector ds = fromVector' ds const
+
+instance VectorSpace Double where
+    toVector' d = (d :)
+
+    fromVector' []     k = k 0 []
+    fromVector' (d:ds) k = k d ds
+
+instance (VectorSpace a, VectorSpace b) => VectorSpace (a, b) where
+    toVector' (a, b) = toVector' a . toVector' b
+
+    fromVector' xs k =
+        fromVector' xs $ \a ys ->
+        fromVector' ys $ \b zs ->
+        k (a, b) zs
diff --git a/overloaded.cabal b/overloaded.cabal
--- a/overloaded.cabal
+++ b/overloaded.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               overloaded
-version:            0.2
+version:            0.2.1
 synopsis:           Overloaded pragmas as a plugin
 description:
   Implement @Overloaded@ pragmas as a source plugin
@@ -23,7 +23,7 @@
 maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
 category:           Plugin
 extra-source-files: CHANGELOG.md
-tested-with:        GHC ==8.6.5 || ==8.8.1
+tested-with:        GHC ==8.6.5 || ==8.8.3 || ==8.10.1
 
 source-repository head
   type:     git
@@ -35,7 +35,9 @@
   ghc-options:      -Wall
   exposed-modules:
     Overloaded
+    Overloaded.Categories
     Overloaded.Chars
+    Overloaded.Do
     Overloaded.If
     Overloaded.Lists
     Overloaded.Lists.Bidi
@@ -46,17 +48,30 @@
     Overloaded.TypeNats
     Overloaded.TypeSymbols
 
+  other-modules:
+    GHC.Compat.All
+    GHC.Compat.Expr
+    Overloaded.Plugin.Categories
+    Overloaded.Plugin.Diagnostics
+    Overloaded.Plugin.HasField
+    Overloaded.Plugin.IdiomBrackets
+    Overloaded.Plugin.LocalDo
+    Overloaded.Plugin.Names
+    Overloaded.Plugin.Rewrite
+    Overloaded.Plugin.V
+
   -- GHC boot dependencies
   build-depends:
-    , base        ^>=4.12.0.0 || ^>=4.13.0.0
+    , base        ^>=4.12.0.0 || ^>=4.13.0.0 || ^>=4.14.0.0
     , bytestring  ^>=0.10.8.2
     , containers  ^>=0.6.0.1
-    , ghc         ^>=8.6 || ^>=8.8
+    , ghc         ^>=8.6 || ^>=8.8 || ^>=8.10
     , text        ^>=1.2.3.0
     , time        ^>=1.8.0.2 || ^>=1.9.3
 
   -- other dependencies
   build-depends:
+    , assoc            ^>=1.0.1
     , bin              ^>=0.1
     , fin              ^>=0.1
     , ral              ^>=0.1
@@ -124,6 +139,48 @@
     , tasty
     , tasty-hunit
 
+test-suite example-boring
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   example
+  main-is:          Boring.hs
+
+  -- inherited dependencies
+  build-depends:
+    , base
+    , overloaded
+
+  -- test dependencies
+  build-depends:
+    , boring       ^>=0.1.3
+    , constraints  >=0.11.2  && <0.13
+    , HUnit        ^>=1.6.0.0
+    , tasty
+    , tasty-hunit
+
+test-suite example-local-do
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   example
+  main-is:          LocalDo.hs
+
+  -- inherited dependencies
+  build-depends:
+    , base
+    , overloaded
+
+test-suite example-ad
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   example
+  main-is:          AD.hs
+  other-modules:    VectorSpace
+  build-depends:
+    , base
+    , constraints  ^>=0.12
+    , hmatrix      ^>=0.20.0.0
+    , overloaded
+
 library optics-hasfield
   default-language: Haskell2010
   hs-source-dirs:   optics-hasfield
@@ -139,7 +196,11 @@
   hs-source-dirs:   test
   main-is:          Tests.hs
   other-modules:
+    AD
+    IxMonad
+    Overloaded.Test.Categories
     Overloaded.Test.Chars
+    Overloaded.Test.Do
     Overloaded.Test.If
     Overloaded.Test.Labels
     Overloaded.Test.Labels.GenericLens
@@ -153,9 +214,11 @@
     Overloaded.Test.TypeSymbols
     Regexp.Term
     Regexp.Type
+    STLC
 
   -- inherited dependencies
   build-depends:
+    , assoc
     , base
     , bin
     , bytestring
@@ -174,8 +237,10 @@
 
   -- test dependencies
   build-depends:
-    , generic-lens    ^>=1.2.0.0
-    , lens            ^>=4.18
-    , singleton-bool  ^>=0.1.5
-    , tasty           ^>=1.2.3
-    , tasty-hunit     ^>=0.10.0.2
+    , generic-lens-lite  ^>=0.1
+    , lens               ^>=4.18 || ^>=4.19.1
+    , QuickCheck         ^>=2.14
+    , singleton-bool     ^>=0.1.5
+    , tasty              ^>=1.2.3
+    , tasty-hunit        ^>=0.10.0.2
+    , tasty-quickcheck   ^>=0.10.1.1
diff --git a/src/GHC/Compat/All.hs b/src/GHC/Compat/All.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Compat/All.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE CPP #-}
+module GHC.Compat.All (
+module X,
+-- * Extras
+mkFunTy,
+) where
+
+#if MIN_VERSION_ghc(8,10,0)
+import Constraint as X
+import Predicate  as X
+import Type       as X
+#else
+import Type as X hiding (mkFunTy)
+#endif
+
+import BasicTypes as X
+import Class      as X
+import CoreSyn    as X
+import DataCon    as X
+import DynFlags   as X
+import ErrUtils   as X
+import FamInst    as X
+import FamInstEnv as X
+import Finder     as X
+import GHC        as X (HscEnv)
+import Id         as X
+import IfaceEnv   as X
+import MkCore     as X
+import Module     as X
+import Name       as X
+import Outputable as X
+import RdrName    as X
+import TcEnv      as X
+import TcEvidence as X
+import TcMType    as X
+import TcRnMonad  as X
+import TyCon      as X
+import TyCoRep    as X hiding (mkFunTy)
+import TysWiredIn as X
+
+import qualified TyCoRep as GHC
+
+-------------------------------------------------------------------------------
+-- Compat functions
+-------------------------------------------------------------------------------
+
+mkFunTy :: X.Type -> X.Type -> X.Type
+mkFunTy =
+#if MIN_VERSION_ghc(8,10,0)
+    GHC.mkFunTy X.VisArg
+#else
+    GHC.mkFunTy
+#endif
diff --git a/src/GHC/Compat/Expr.hs b/src/GHC/Compat/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Compat/Expr.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE CPP #-}
+-- | THis module re-exports 'HsExpr' and few related data types.
+module GHC.Compat.Expr (
+    -- * Expression
+    HsExpr (..),
+    LHsExpr,
+    HsBracket (..),
+    HsStmtContext (..),
+    StmtLR (..),
+    ExprLStmt,
+    MatchGroup (..),
+    Match (..),
+    GRHSs (..),
+    GRHS (..),
+    HsMatchContext (..),
+    HsLocalBindsLR (..),
+    -- ** Constructors
+    hsVar,
+    hsApps,
+    hsTyApp,
+    hsTyVar,
+    hsPar,
+    hsOpApp,
+    -- * Accessors
+    hsConPatArgs,
+    -- * Patterns
+    LPat,
+    Pat (..),
+    -- * Proc commands
+    HsCmdTop (..),
+    HsCmd (..),
+    LHsCmd,
+    CmdLStmt,
+    HsArrAppType (..),
+    -- * Tuples
+    HsTupArg (..),
+    -- * Literals
+    HsLit (..),
+    HsTyLit (..),
+    HsOverLit (..),
+    OverLitVal (..),
+    -- * Type
+    HsType (..),
+    LHsType,
+    HsWildCardBndrs (..),
+#if MIN_VERSION_ghc(8,8,0)
+    PromotionFlag (..),
+#else
+    Promoted (..),
+#endif
+    -- * Statements
+    HsGroup,
+    -- * Reader phase
+    GhcRn,
+    -- * SourceSpan
+    Located,
+    GenLocated (..),
+    SrcSpan (..),
+    RealSrcSpan,
+    noSrcSpan,
+    srcSpanStartLine,
+    srcSpanEndLine,
+    srcSpanStartCol,
+    srcSpanEndCol,
+    -- * Extensions
+    noExtField,
+    -- * Names
+    nameToString,
+) where
+
+#if MIN_VERSION_ghc(8,10,0)
+import GHC.Hs
+#else
+import HsSyn
+#endif
+
+#if MIN_VERSION_ghc(8,8,0)
+import BasicTypes (PromotionFlag (..))
+#endif
+
+import Data.List (foldl')
+import SrcLoc
+       (GenLocated (..), Located, RealSrcSpan, SrcSpan (..), noSrcSpan,
+       srcSpanEndCol, srcSpanEndLine, srcSpanStartCol, srcSpanStartLine)
+
+import qualified GHC.Compat.All as GHC
+
+#if !(MIN_VERSION_ghc(8,10,0))
+noExtField  :: NoExt
+noExtField = noExt
+#endif
+
+hsVar :: SrcSpan -> GHC.Name -> LHsExpr GhcRn
+hsVar l n = L l (HsVar noExtField (L l n))
+
+hsTyVar :: SrcSpan -> GHC.Name -> HsType GhcRn
+hsTyVar l n = HsTyVar noExtField NotPromoted (L l n)
+
+hsApps :: SrcSpan -> LHsExpr GhcRn -> [LHsExpr GhcRn] -> LHsExpr GhcRn
+hsApps l = foldl' app where
+    app :: LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
+    app f x = L l (HsApp noExtField f x)
+
+hsOpApp :: SrcSpan -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
+hsOpApp l x op y = L l (OpApp GHC.defaultFixity x op y)
+
+hsTyApp :: SrcSpan -> LHsExpr GhcRn -> HsType GhcRn -> LHsExpr GhcRn
+#if MIN_VERSION_ghc(8,8,0)
+hsTyApp l x ty = L l $ HsAppType noExtField x (HsWC [] (L l ty))
+#else
+hsTyApp l x ty = L l $ HsAppType (HsWC [] (L l ty)) x
+#endif
+
+hsPar :: SrcSpan -> LHsExpr GhcRn -> LHsExpr GhcRn
+hsPar l e = L l (HsPar noExtField e)
+
+nameToString :: GHC.Name -> String
+nameToString = GHC.occNameString . GHC.occName
+
+
diff --git a/src/Overloaded.hs b/src/Overloaded.hs
--- a/src/Overloaded.hs
+++ b/src/Overloaded.hs
@@ -35,11 +35,25 @@
     -- * Overloaded:TypeSymbols
     FromTypeSymbolC (..),
 
+    -- * Overloaded:Do
+    DoMethod (..), Pure, Then, Bind, Monad' (..),
+
+    -- * Overloaded:Categories
+    Category,
+    identity,
+    (%%),
+    CartesianCategory (..),
+    CocartesianCategory (..),
+    BicartesianCategory (..),
+    CCC (..),
+
     -- * Overloaded:RecordFields
     -- | See "GHC.Records.Compat"  from @record-hasfield@ package.
   ) where
 
+import Overloaded.Categories
 import Overloaded.Chars
+import Overloaded.Do
 import Overloaded.If
 import Overloaded.Lists
 import Overloaded.Naturals
diff --git a/src/Overloaded/Categories.hs b/src/Overloaded/Categories.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Categories.hs
@@ -0,0 +1,251 @@
+{-# LANGUAGE CPP          #-}
+{-# LANGUAGE PolyKinds    #-}
+{-# LANGUAGE TypeFamilies #-}
+-- | Overloaded Categories, desugar @Arrow@ into classes in this module.
+--
+-- == Enabled with
+--
+-- @
+-- {-\# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Categories #-}
+-- @
+--
+-- == Description
+--
+-- @Arrows@ notation - [GHC manual chapter](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/glasgow_exts.html#arrow-notation) -
+-- is cool, but it desugars into /"wrong"/ classes.
+-- The 'arr' combinator is used for plumbing. We should desugar to proper
+-- type-classes:
+--
+-- * 'CartesianCategory', not 'Arrow'
+-- * 'CocartesianCategory', not 'ArrowChoice' (implementation relies on 'BicartesianCategory')
+-- * 'CCC', not 'ArrowApply' (not implemented yet)
+--
+-- == Examples
+--
+-- Expression like
+--
+-- @
+-- catAssoc
+--     :: 'CartesianCategory' cat
+--     => cat ('Product' cat ('Product' cat a b) c) ('Product' cat a ('Product' cat b c))
+-- catAssoc = proc ((x, y), z) -> 'identity' -< (x, (y, z))
+-- @
+--
+-- are desugared to (a mess which is)
+--
+-- @
+-- 'fanout' ('proj1' '%%' 'proj1') ('fanout' ('proj2' '%%' 'proj1') 'proj2')
+-- @
+--
+-- If you are familiar with arrows-operators, this is similar to
+--
+-- @
+-- ('fst' . 'fst') '&&&' ('snd' . 'fst' '&&&' 'snd')
+-- @
+--
+-- expression.
+--
+-- The @catAssoc@ could be instantiated to @cat = (->)@,
+-- or more interestingly for example instantiate it to STLC morphisms to get an expression
+-- like:
+--
+-- @
+-- Lam (Pair (Fst (Fst (Var Here))) (Pair (Snd (Fst (Var Here))) (Snd (Var Here))))
+-- @
+--
+-- @proc@ notation is nicer than writing de Bruijn indices.
+--
+-- This is very similar idea to Conal Elliott's [Compiling to Categories](http://conal.net/papers/compiling-to-categories/) work. 
+-- This approach is syntactically more heavy, but works in more correct
+-- stage of compiler, before actual desugarer.
+--
+-- As one more example, we implement the automatic differentiation,
+-- as in Conal's paper(s).
+-- To keep things simple we use
+--
+-- @
+-- newtype AD a b = AD (a -> (b, a -> b))
+-- @
+--
+-- representation, i.e. use ordinary maps to represent linear maps.
+-- We then define a function
+--
+-- @
+-- evaluateAD :: Functor f => AD a b -> a -> f a -> (b, f b)
+-- evaluateAD (AD f) x xs = let (y, f') = f x in (y, fmap f' xs)
+-- @
+--
+-- which would allow to calculuate function value and 
+-- derivatives in given directions. Then we can define
+-- simple quadratic function:
+--
+-- @
+-- quad :: AD (Double, Double) Double
+-- quad = proc (x, y) -> do
+--     x2 <- mult -< (x, x)
+--     y2 <- mult -< (y, y)
+--     plus -< (x2, y2)
+-- @
+--
+-- It's not as simple as writing @quad x y = x * x + y * y@,
+-- but not /too far/.
+--
+-- Then we can play with it. At origo everything is zero:
+--
+-- @
+-- let sqrthf = 1 / sqrt 2
+-- in evaluateAD quad (0, 0) [(1,0), (0,1), (sqrthf, sqrthf)] = (0.0,[0.0,0.0,0.0])
+-- @
+--
+-- If we evaluate at some other point, we see things working:
+--
+-- @
+-- evaluateAD quad (1, 2) [(1,0), (0,1), (sqrthf, sqrthf)] = (5.0,[2.0,4.0,4.242640687119285])
+-- @
+--
+-- Obviously, if we would use inspectable representation for linear maps,
+-- as Conal describe, we'd get more benefits. And then 'arr' wouldn't
+-- be definable!
+--
+module Overloaded.Categories (
+    C.Category,
+    identity,
+    (%%),
+    CategoryWith1 (..),
+    CartesianCategory (..),
+    CocartesianCategory (..),
+    BicartesianCategory (..),
+    CCC (..),
+    GeneralizedElement (..),
+    ) where
+
+import qualified Control.Category as C
+import           Data.Kind        (Type)
+
+#ifdef __HADDOCK__
+import Control.Arrow
+#endif
+
+-------------------------------------------------------------------------------
+-- Category
+-------------------------------------------------------------------------------
+
+-- | A non-clashing name for 'C.id'.
+identity :: C.Category cat => cat a a
+identity = C.id
+{-# INLINE identity #-}
+
+-- | A non-clashing name for @('C..')@.
+(%%) :: C.Category cat => cat b c -> cat a b -> cat a c
+(%%) = (C..)
+{-# INLINE (%%) #-}
+infixr 9 %%
+
+-------------------------------------------------------------------------------
+-- Monoidal
+-------------------------------------------------------------------------------
+
+-- TODO
+
+-------------------------------------------------------------------------------
+-- Product
+-------------------------------------------------------------------------------
+
+-- | Category with terminal object.
+class C.Category cat => CategoryWith1 (cat :: k -> k -> Type) where
+    type Terminal cat :: k
+    
+    terminal :: cat a (Terminal cat)
+
+-- | Cartesian category is a monoidal category
+-- where monoidal product is the categorical product.
+--
+class CategoryWith1 cat => CartesianCategory (cat :: k -> k -> Type) where
+    type Product cat :: k -> k -> k
+
+    proj1 :: cat (Product cat a b) a
+    proj2 :: cat (Product cat a b) b
+
+    -- | @'fanout' f g@ is written as \(\langle f, g \rangle\) in category theory literature.
+    fanout :: cat a b -> cat a c -> cat a (Product cat b c)
+
+instance CategoryWith1 (->) where
+    type Terminal (->) = ()
+
+    terminal _ = ()
+
+instance CartesianCategory (->) where
+    type Product (->) = (,)
+
+    proj1 = fst
+    proj2 = snd
+    fanout f g x = (f x , g x)
+
+-------------------------------------------------------------------------------
+-- Coproduct
+-------------------------------------------------------------------------------
+
+-- | Cocartesian category is a monoidal category
+-- where monoidal product is the categorical coproduct.
+--
+class C.Category cat => CocartesianCategory (cat :: k -> k -> Type) where
+    type Coproduct cat :: k -> k -> k
+
+    inl :: cat a (Coproduct cat a b)
+    inr :: cat b (Coproduct cat a b)
+
+    -- | @'fanin' f g@ is written as \([f, g]\) in category theory literature.
+    fanin :: cat a c -> cat b c -> cat (Coproduct cat a b) c
+
+instance CocartesianCategory (->) where
+    type Coproduct (->) = Either
+
+    inl = Left
+    inr = Right
+    fanin = either
+
+-- | Bicartesian category is category which is
+-- both cartesian and cocartesian.
+--
+-- We also require distributive morpism.
+class (CartesianCategory cat, CocartesianCategory cat) => BicartesianCategory cat where
+    distr :: cat (Product cat (Coproduct cat a b) c)
+                 (Coproduct cat (Product cat a c) (Product cat b c))
+
+instance BicartesianCategory (->) where
+    distr (Left x,  z) = Left (x, z)
+    distr (Right y, z) = Right (y, z)
+
+-------------------------------------------------------------------------------
+-- Exponential
+-------------------------------------------------------------------------------
+
+-- | Closed cartesian category.
+--
+class CartesianCategory cat => CCC (cat :: k -> k -> Type) where
+    -- | @'Exponential' cat a b@ represents \(B^A\). This is due how (->) works.
+    type Exponential cat :: k -> k -> k
+
+    eval :: cat (Product cat (Exponential cat a b) a) b
+
+    transpose :: cat (Product cat a b) c -> cat a (Exponential cat b c)
+
+instance CCC (->) where
+    type Exponential (->) = (->)
+
+    eval      = uncurry ($)
+    transpose = curry
+
+-------------------------------------------------------------------------------
+-- Generalized Element
+-------------------------------------------------------------------------------
+
+class C.Category cat => GeneralizedElement (cat :: k -> k -> Type) where
+    type Object cat (a :: k) :: Type
+
+    konst :: Object cat a -> cat x a
+
+instance GeneralizedElement (->) where
+    type Object (->) a = a
+
+    konst = const
diff --git a/src/Overloaded/Do.hs b/src/Overloaded/Do.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Do.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE UndecidableInstances  #-}
+-- | Overloaded "local" @do@-blocks.
+--
+-- Inspired by [Local Do GHC-proposal](https://github.com/ghc-proposals/ghc-proposals/pull/216).
+-- Yet because we do desugaring in reader phase, we must have
+-- a bit more complicated setup.
+--
+-- The expressions like
+--
+-- @
+-- ex2d :: IxStateT Identity Int String ()
+-- ex2d = ixmonad.do
+--     _unused <- ixmodify show
+--     ixmodify reverse
+-- @
+--
+-- are desugared into
+--
+-- @
+-- ex2b :: IxStateT Identity Int String ()
+-- ex2b =
+--     ixmonad \@Bind (ixmodify show) $ \\_unused ->
+--     ixmodify reverse
+-- @
+--
+-- Allowing to locally overload what @do@ desugars to.
+--
+-- The 'monad' in this module is an example how to define a desugaring.
+-- We need to it this way, so the names are easily accessible in renamer phase.
+-- (I.e. constant, then transformation is pure, as we don't need to lookup them for each do-block).
+--
+-- Enabled with:
+--
+-- @
+-- {-\# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Do #-}
+-- @
+--
+module Overloaded.Do (
+-- * Do desugaring methods
+DoMethod (..),
+-- * Type aliases
+Pure, Then, Bind,
+-- * Default Monad desugaring
+Monad' (..),
+) where
+
+import Data.Kind (Type)
+
+-------------------------------------------------------------------------------
+-- Definitions
+-------------------------------------------------------------------------------
+
+data DoMethod
+    = Pure  -- ^ 'return'
+    | Then  -- ^ '>>'
+    | Bind  -- ^ '>>='
+
+type Pure = 'Pure
+type Then   = 'Then
+type Bind   = 'Bind
+
+-------------------------------------------------------------------------------
+-- Default Monad
+-------------------------------------------------------------------------------
+
+class Monad' (method :: DoMethod) (ty :: Type) where
+    monad :: ty
+
+instance (ty ~ (a -> m a),                 Applicative m) => Monad' 'Pure ty where monad = pure
+instance (ty ~ (m a -> m b -> m b),        Applicative m) => Monad' 'Then ty where monad = (*>)
+instance (ty ~ (m a -> (a -> m b) -> m b), Monad m)       => Monad' 'Bind ty where monad = (>>=)
diff --git a/src/Overloaded/Plugin.hs b/src/Overloaded/Plugin.hs
--- a/src/Overloaded/Plugin.hs
+++ b/src/Overloaded/Plugin.hs
@@ -1,37 +1,30 @@
-{-# LANGUAGE CPP                 #-}
 {-# LANGUAGE RecordWildCards     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 -- | Overloaded plugin, which makes magic possible.
 module Overloaded.Plugin (plugin) where
 
-import Control.Applicative    ((<|>))
-import Control.Monad          (foldM, forM, guard, unless, when)
+import Control.Monad          (foldM, when)
 import Control.Monad.IO.Class (MonadIO (..))
-import Data.List              (elemIndex, foldl', intercalate)
-import Data.List.NonEmpty     (NonEmpty (..))
+import Data.List              (intercalate)
 import Data.List.Split        (splitOn)
-import Data.Maybe             (catMaybes, mapMaybe)
+import Data.Maybe             (catMaybes)
 
 import qualified Data.Generics as SYB
 
 -- GHC stuff
-import qualified Class
-import qualified ErrUtils   as Err
-import qualified FamInst
-import qualified FamInstEnv
-import qualified Finder
-import qualified GhcPlugins as GHC
-import           HsSyn      as GHC
-import qualified IfaceEnv
-import qualified RdrName
-import           SrcLoc
-import qualified TcEnv
-import qualified TcEvidence as Tc
-import qualified TcMType
-import qualified TcPluginM  as TC
-import qualified TcRnMonad  as TcM
-import qualified TcRnTypes
+import qualified GHC.Compat.All  as GHC
+import           GHC.Compat.Expr
+import qualified GhcPlugins      as Plugins
 
+import Overloaded.Plugin.Categories
+import Overloaded.Plugin.Diagnostics
+import Overloaded.Plugin.HasField
+import Overloaded.Plugin.IdiomBrackets
+import Overloaded.Plugin.LocalDo
+import Overloaded.Plugin.Names
+import Overloaded.Plugin.Rewrite
+import Overloaded.Plugin.V
+
 -------------------------------------------------------------------------------
 -- Plugin
 -------------------------------------------------------------------------------
@@ -66,11 +59,14 @@
 -- * @Strings@ works like built-in @OverloadedStrings@ (but you can use different method than 'Data.String.fromString')
 -- * @Numerals@ desugars literal numbers to @'Overloaded.Numerals.fromNumeral' \@nat@
 -- * @Naturals@ desugars literal numbers to @'Overloaded.Naturals.fromNatural' nat@ (i.e. like 'Data.String.fromString')
--- * @Chars@ desugars literal characters to @'Overloaded.Chars.fromChars' c@. /Note:/ there isn't type-level alternative: we cannot promote 'Char's.
+-- * @Chars@ desugars literal characters to @'Overloaded.Chars.fromChars' c@. /Note:/ there isn't type-level alternative: we cannot promote 'Char's
 -- * @Lists@ __is not__ like built-in @OverloadedLists@, but desugars explicit lists to 'Overloaded.Lists.cons' and 'Overloaded.Lists.nil'
 -- * @If@ desugars @if@-expressions to @'Overloaded.If.ifte' b t e@
+-- * @Unit@ desugars @()@-expressions to @'Overloaded.Lists.nil'@ (but you can use different method, e.g. @boring@ from <https://hackage.haskell.org/package/boring-0.1.3/docs/Data-Boring.html Data.Boring>)
 -- * @Labels@ works like built-in @OverloadedLabels@ (you should enable @OverloadedLabels@ so parser recognises the syntax)
--- * @TypeNats@ and @TypeSymbols@ desugar type-level literals into @'Overloaded.TypeNats.FromNat'@ and @'Overloaded.TypeSymbols.FromTypeSymbol'@ respectively.
+-- * @TypeNats@ and @TypeSymbols@ desugar type-level literals into @'Overloaded.TypeNats.FromNat'@ and @'Overloaded.TypeSymbols.FromTypeSymbol'@ respectively
+-- * @Do@ desugar in /Local Do/ fashion. See examples.
+-- * @Categories@ change @Arrows@ desugaring to use /"correct"/ category classes.
 --
 -- == Known limitations
 --
@@ -140,11 +136,11 @@
 --     'traverse' f (Branch l r) = [| Branch ('traverse' f l) ('traverse' f r) |]
 -- @
 --
-plugin :: GHC.Plugin
-plugin = GHC.defaultPlugin
-    { GHC.renamedResultAction = pluginImpl
-    , GHC.tcPlugin            = enabled tcPlugin
-    , GHC.pluginRecompile     = GHC.purePlugin
+plugin :: Plugins.Plugin
+plugin = Plugins.defaultPlugin
+    { Plugins.renamedResultAction = pluginImpl
+    , Plugins.tcPlugin            = enabled tcPlugin
+    , Plugins.pluginRecompile     = Plugins.purePlugin
     }
   where
     enabled p args'
@@ -154,13 +150,13 @@
         args = concatMap (splitOn ":") args'
 
 pluginImpl
-    :: [GHC.CommandLineOption]
-    -> TcRnTypes.TcGblEnv
+    :: [Plugins.CommandLineOption]
+    -> GHC.TcGblEnv
     -> HsGroup GhcRn
-    -> TcRnTypes.TcM (TcRnTypes.TcGblEnv, HsGroup GhcRn)
+    -> GHC.TcM (GHC.TcGblEnv, HsGroup GhcRn)
 pluginImpl args' env gr = do
     dflags <- GHC.getDynFlags
-    topEnv <- TcM.getTopEnv
+    topEnv <- GHC.getTopEnv
 
     debug $ show args
     debug $ GHC.showPpr dflags gr
@@ -170,8 +166,8 @@
     when (opts == defaultOptions) $
         warn dflags noSrcSpan $ GHC.text "No Overloaded features enabled"
 
-    let transformNoOp :: a -> Maybe a
-        transformNoOp _ = Nothing
+    let transformNoOp :: a -> Rewrite a
+        transformNoOp _ = NoRewrite
 
     trStr <- case optStrings of
         NoStr         -> return transformNoOp
@@ -228,6 +224,24 @@
         False -> return transformNoOp
         True  -> return $ transformIdiomBrackets names
 
+    trDo <- case optDo of
+        False -> return transformNoOp
+        True  -> return $ transformDo names
+
+    trCategories <- case optCategories of
+        Off          -> return transformNoOp
+        On Nothing   -> return $ transformCategories names
+        On (Just mn) -> do
+            catNames' <- getCatNames dflags topEnv (GHC.mkModuleName mn)
+            return $ transformCategories $ names { catNames = catNames' }
+
+    trUnit <- case optUnit of
+        Off        -> return transformNoOp
+        On Nothing -> return $ transformUnit names
+        On (Just vn) -> do
+            n <- lookupVarName dflags topEnv vn
+            return $ transformUnit $ names { unitName = n }
+
     trTypeNats <- case optTypeNats of
         Off          -> return transformNoOp
         On Nothing   -> return $ transformTypeNats names
@@ -242,8 +256,8 @@
             n <- lookupTypeName dflags topEnv vn
             return $ transformTypeSymbols $ names { fromTypeSymbolName = n }
 
-    let tr  = trStr /\ trNum /\ trChr /\ trLists /\ trIf /\ trLabel /\ trBrackets
-    let trT = trTypeNats /\ trTypeSymbols
+    let tr  = trStr <> trNum <> trChr <> trLists <> trIf <> trLabel <> trBrackets <> trDo <> trCategories <> trUnit
+    let trT = trTypeNats <> trTypeSymbols
 
     gr' <- transformType dflags trT gr
     gr'' <- transform dflags tr gr'
@@ -252,11 +266,6 @@
   where
     args = concatMap (splitOn ":") args'
 
-    (/\) :: (a -> Maybe b) -> (a -> Maybe b) -> a -> Maybe b
-    f /\ g = \x -> f x <|> g x
-
-    infixr 9 /\ -- hello CPP
-
 -------------------------------------------------------------------------------
 -- Args parsing
 -------------------------------------------------------------------------------
@@ -312,6 +321,9 @@
     go opts "If"       vns = do
         mvn <- oneName "If" vns
         return $ opts { optIf = On mvn }
+    go opts "Unit"       vns = do
+        mvn <- oneName "Unit" vns
+        return $ opts { optUnit = On mvn }
     go opts "Labels"   vns = do
         mvn <- oneName "Symbols" vns
         return $ opts { optLabels = On mvn }
@@ -325,11 +337,17 @@
         return $ opts { optRecordFields = True }
     go opts "IdiomBrackets" _ =
         return $ opts { optIdiomBrackets = True }
+    go opts "Do" _ =
+        return $ opts { optDo = True }
+    go opts "Categories" vns = do
+        mvn <- oneName "Categories" vns
+        return $ opts { optCategories = On $ fmap (\(VN x _) -> x) mvn }
 
     go opts s _ = do
         warn dflags noSrcSpan $ GHC.text $ "Unknown Overloaded option " ++  show s
         return opts
 
+    oneName :: [Char] -> [a] -> m (Maybe a)
     oneName arg vns = case vns of
         []     -> return Nothing
         [vn]   -> return (Just vn)
@@ -367,10 +385,13 @@
     , optLists         :: OnOff (V2 VarName)
     , optIf            :: OnOff VarName
     , optLabels        :: OnOff VarName
+    , optUnit          :: OnOff VarName
     , optTypeNats      :: OnOff VarName
     , optTypeSymbols   :: OnOff VarName
     , optRecordFields  :: Bool
     , optIdiomBrackets :: Bool
+    , optDo            :: Bool
+    , optCategories    :: OnOff String -- module name
     }
   deriving (Eq, Show)
 
@@ -384,8 +405,11 @@
     , optLabels        = Off
     , optTypeNats      = Off
     , optTypeSymbols   = Off
+    , optUnit          = Off
     , optRecordFields  = False
     , optIdiomBrackets = False
+    , optDo            = False
+    , optCategories    = Off
     }
 
 data StrSym
@@ -425,65 +449,66 @@
 -- OverloadedStrings
 -------------------------------------------------------------------------------
 
-transformStrings :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformStrings :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformStrings Names {..} e@(L l (HsLit _ (HsString _ _fs))) =
-    Just $ hsApps l (hsVar l fromStringName) [e]
+    Rewrite $ hsApps l (hsVar l fromStringName) [e]
 
-transformStrings _ _ = Nothing
+transformStrings _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedSymbols
 -------------------------------------------------------------------------------
 
-transformSymbols :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformSymbols :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformSymbols Names {..} (L l (HsLit _ (HsString _ fs))) = do
     let name' = hsVar l fromSymbolName
-    let inner = hsTyApp l name' (HsTyLit noExt (HsStrTy GHC.NoSourceText fs))
-    Just inner
+    let inner = hsTyApp l name' (HsTyLit noExtField (HsStrTy GHC.NoSourceText fs))
+    Rewrite inner
 
-transformSymbols _ _ = Nothing
+transformSymbols _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedNumerals
 -------------------------------------------------------------------------------
 
-transformNumerals :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformNumerals :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformNumerals Names {..} (L l (HsOverLit _ (OverLit _ (HsIntegral (GHC.IL _ n i)) _)))
     | not n, i >= 0 = do
         let name' = hsVar l fromNumeralName
-        let inner = hsTyApp l name' (HsTyLit noExt (HsNumTy GHC.NoSourceText i))
-        Just inner
+        let inner = hsTyApp l name' (HsTyLit noExtField (HsNumTy GHC.NoSourceText i))
+        Rewrite inner
 
-transformNumerals _ _ = Nothing
+transformNumerals _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedNaturals
 -------------------------------------------------------------------------------
 
-transformNaturals :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformNaturals :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformNaturals Names {..} e@(L l (HsOverLit _ (OverLit _ (HsIntegral (GHC.IL _ n i)) _)))
-    | not n, i >= 0 = do
-    Just $ hsApps l (hsVar l fromNaturalName) [e]
+    | not n
+    , i >= 0
+    = Rewrite $ hsApps l (hsVar l fromNaturalName) [e]
 
-transformNaturals _ _ = Nothing
+transformNaturals _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedChars
 -------------------------------------------------------------------------------
 
-transformChars :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformChars :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformChars Names {..} e@(L l (HsLit _ (HsChar _ _))) =
-    Just $ hsApps l (hsVar l fromCharName) [e]
+    Rewrite $ hsApps l (hsVar l fromCharName) [e]
 
-transformChars _ _ = Nothing
+transformChars _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedLists
 -------------------------------------------------------------------------------
 
-transformLists :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformLists :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformLists Names {..} (L l (ExplicitList _ Nothing xs)) =
-    Just $ foldr cons' nil' xs
+    Rewrite $ foldr cons' nil' xs
   where
     cons' :: LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
     cons' y ys = hsApps l (hsVar l consName) [y, ys]
@@ -492,51 +517,63 @@
     nil' = hsVar l nilName
 
     -- otherwise: leave intact
-transformLists _ _ = Nothing
+transformLists _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedIf
 -------------------------------------------------------------------------------
 
-transformIf :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
-transformIf Names {..} (L l (HsIf _ _ co th el)) = Just val4 where
-    val4 = L l $ HsApp noExt val3 el
-    val3 = L l $ HsApp noExt val2 th
-    val2 = L l $ HsApp noExt val1 co
-    val1 = L l $ HsVar noExt $ L l ifteName
-transformIf _ _ = Nothing
+transformIf :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
+transformIf Names {..} (L l (HsIf _ _ co th el)) = Rewrite val4 where
+    val4 = L l $ HsApp noExtField val3 el
+    val3 = L l $ HsApp noExtField val2 th
+    val2 = L l $ HsApp noExtField val1 co
+    val1 = L l $ HsVar noExtField $ L l ifteName
+transformIf _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedLabels
 -------------------------------------------------------------------------------
 
-transformLabels :: Names -> LHsExpr GhcRn -> Maybe (LHsExpr GhcRn)
+transformLabels :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
 transformLabels Names {..} (L l (HsOverLabel _ Nothing fs)) = do
     let name' = hsVar l fromLabelName
-    let inner = hsTyApp l name' (HsTyLit noExt (HsStrTy GHC.NoSourceText fs))
-    Just inner
+    let inner = hsTyApp l name' (HsTyLit noExtField (HsStrTy GHC.NoSourceText fs))
+    Rewrite inner
 
-transformLabels _ _ = Nothing
+transformLabels _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
+-- OverloadedUnit
+-------------------------------------------------------------------------------
+
+transformUnit :: Names -> LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn)
+transformUnit Names {..} (L l (HsVar _ (L _ name')))
+    | name' == ghcUnitName = Rewrite (hsVar l unitName)
+  where
+    ghcUnitName = GHC.getName (GHC.tupleDataCon GHC.Boxed 0)
+
+transformUnit _ _ = NoRewrite
+
+-------------------------------------------------------------------------------
 -- OverloadedTypeNats
 -------------------------------------------------------------------------------
 
-transformTypeNats :: Names -> LHsType GhcRn -> Maybe  (LHsType GhcRn)
+transformTypeNats :: Names -> LHsType GhcRn -> Rewrite (LHsType GhcRn)
 transformTypeNats Names {..} e@(L l (HsTyLit _ (HsNumTy _ _))) = do
-    let name' = L l $ HsTyVar noExt GHC.NotPromoted $ L l fromTypeNatName
-    Just $ L l $ HsAppTy noExt name' e
-transformTypeNats _ _ = Nothing
+    let name' = L l $ HsTyVar noExtField NotPromoted $ L l fromTypeNatName
+    Rewrite $ L l $ HsAppTy noExtField name' e
+transformTypeNats _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- OverloadedTypeSymbols
 -------------------------------------------------------------------------------
 
-transformTypeSymbols :: Names -> LHsType GhcRn -> Maybe  (LHsType GhcRn)
+transformTypeSymbols :: Names -> LHsType GhcRn -> Rewrite (LHsType GhcRn)
 transformTypeSymbols Names {..} e@(L l (HsTyLit _ (HsStrTy _ _))) = do
-    let name' = L l $ HsTyVar noExt GHC.NotPromoted $ L l fromTypeSymbolName
-    Just $ L l $ HsAppTy noExt name' e
-transformTypeSymbols _ _ = Nothing
+    let name' = L l $ HsTyVar noExtField NotPromoted $ L l fromTypeSymbolName
+    Rewrite $ L l $ HsAppTy noExtField name' e
+transformTypeSymbols _ _ = NoRewrite
 
 -------------------------------------------------------------------------------
 -- Transform
@@ -544,470 +581,32 @@
 
 transform
     :: GHC.DynFlags
-    -> (LHsExpr GhcRn -> Maybe (LHsExpr GhcRn))
+    -> (LHsExpr GhcRn -> Rewrite (LHsExpr GhcRn))
     -> HsGroup GhcRn
-    -> TcRnTypes.TcM (HsGroup GhcRn)
-transform _dflags f = SYB.everywhereM (SYB.mkM transform') where
-    transform' :: LHsExpr GhcRn -> TcRnTypes.TcM (LHsExpr GhcRn)
-    transform' e =
-        return $ case f e of
-            Just e' -> e'
-            Nothing -> e
+    -> GHC.TcM (HsGroup GhcRn)
+transform dflags f = SYB.everywhereM (SYB.mkM transform') where
+    transform' :: LHsExpr GhcRn -> GHC.TcM (LHsExpr GhcRn)
+    transform' e@(L _l _) = do
+        -- liftIO $ GHC.putLogMsg _dflags GHC.NoReason GHC.SevWarning _l (GHC.defaultErrStyle _dflags) $
+        --     GHC.text "Expr" GHC.<+> GHC.ppr e GHC.<+> GHC.text (SYB.gshow e)
+        case f e of
+            Rewrite e' -> return e'
+            NoRewrite  -> return e
+            Error err  -> do
+                liftIO $ err dflags
+                fail "Error in Overloaded plugin"
 
 transformType
     :: GHC.DynFlags
-    -> (LHsType GhcRn -> Maybe (LHsType GhcRn))
+    -> (LHsType GhcRn -> Rewrite (LHsType GhcRn))
     -> HsGroup GhcRn
-    -> TcRnTypes.TcM (HsGroup GhcRn)
-transformType _dflags f = SYB.everywhereM (SYB.mkM transform') where
-    transform' :: LHsType GhcRn -> TcRnTypes.TcM (LHsType GhcRn)
+    -> GHC.TcM (HsGroup GhcRn)
+transformType dflags f = SYB.everywhereM (SYB.mkM transform') where
+    transform' :: LHsType GhcRn -> GHC.TcM (LHsType GhcRn)
     transform' e = do
-        return $ case f e of
-            Just e' -> e'
-            Nothing -> e
-
--------------------------------------------------------------------------------
--- Constructors
--------------------------------------------------------------------------------
-
-hsVar :: SrcSpan -> GHC.Name -> LHsExpr GhcRn
-hsVar l n = L l (HsVar noExt (L l n))
-
-hsApps :: SrcSpan -> LHsExpr GhcRn -> [LHsExpr GhcRn] -> LHsExpr GhcRn
-hsApps l = foldl' app where
-    app :: LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
-    app f x = L l (HsApp noExt f x)
-
-hsTyApp :: SrcSpan -> LHsExpr GhcRn -> HsType GhcRn -> LHsExpr GhcRn
-#if MIN_VERSION_ghc(8,8,0)
-hsTyApp l x ty = L l $ HsAppType noExt x (HsWC [] (L l ty))
-#else
-hsTyApp l x ty = L l $ HsAppType (HsWC [] (L l ty)) x
-#endif
-
--------------------------------------------------------------------------------
--- ModuleNames
--------------------------------------------------------------------------------
-
-dataStringMN :: GHC.ModuleName
-dataStringMN =  GHC.mkModuleName "Data.String"
-
-overloadedCharsMN :: GHC.ModuleName
-overloadedCharsMN =  GHC.mkModuleName "Overloaded.Chars"
-
-overloadedSymbolsMN :: GHC.ModuleName
-overloadedSymbolsMN =  GHC.mkModuleName "Overloaded.Symbols"
-
-overloadedNaturalsMN :: GHC.ModuleName
-overloadedNaturalsMN =  GHC.mkModuleName "Overloaded.Naturals"
-
-overloadedNumeralsMN :: GHC.ModuleName
-overloadedNumeralsMN =  GHC.mkModuleName "Overloaded.Numerals"
-
-overloadedListsMN :: GHC.ModuleName
-overloadedListsMN =  GHC.mkModuleName "Overloaded.Lists"
-
-overloadedIfMN :: GHC.ModuleName
-overloadedIfMN =  GHC.mkModuleName "Overloaded.If"
-
-ghcOverloadedLabelsMN :: GHC.ModuleName
-ghcOverloadedLabelsMN =  GHC.mkModuleName "GHC.OverloadedLabels"
-
-overloadedTypeNatsMN :: GHC.ModuleName
-overloadedTypeNatsMN =  GHC.mkModuleName "Overloaded.TypeNats"
-
-overloadedTypeSymbolsMN :: GHC.ModuleName
-overloadedTypeSymbolsMN =  GHC.mkModuleName "Overloaded.TypeSymbols"
-
-ghcRecordsCompatMN :: GHC.ModuleName
-ghcRecordsCompatMN =  GHC.mkModuleName "GHC.Records.Compat"
-
-ghcBaseMN :: GHC.ModuleName
-ghcBaseMN = GHC.mkModuleName "GHC.Base"
-
-dataFunctorMN :: GHC.ModuleName
-dataFunctorMN = GHC.mkModuleName "Data.Functor"
-
--------------------------------------------------------------------------------
--- Names
--------------------------------------------------------------------------------
-
-data Names = Names
-    { fromStringName     :: GHC.Name
-    , fromSymbolName     :: GHC.Name
-    , fromNumeralName    :: GHC.Name
-    , fromNaturalName    :: GHC.Name
-    , fromCharName       :: GHC.Name
-    , nilName            :: GHC.Name
-    , consName           :: GHC.Name
-    , ifteName           :: GHC.Name
-    , fromLabelName      :: GHC.Name
-    , fromTypeNatName    :: GHC.Name
-    , fromTypeSymbolName :: GHC.Name
-    , fmapName           :: GHC.Name
-    , pureName           :: GHC.Name
-    , apName             :: GHC.Name
-    , birdName           :: GHC.Name
-    , voidName           :: GHC.Name
-    }
-
-getNames :: GHC.DynFlags -> GHC.HscEnv -> TcRnTypes.TcM Names
-getNames dflags env = do
-    fromStringName  <- lookupName dflags env dataStringMN "fromString"
-    fromSymbolName  <- lookupName dflags env overloadedSymbolsMN "fromSymbol"
-    fromNumeralName <- lookupName dflags env overloadedNumeralsMN "fromNumeral"
-    fromNaturalName <- lookupName dflags env overloadedNaturalsMN "fromNatural"
-    fromCharName    <- lookupName dflags env overloadedCharsMN "fromChar"
-    nilName         <- lookupName dflags env overloadedListsMN "nil"
-    consName        <- lookupName dflags env overloadedListsMN "cons"
-    ifteName        <- lookupName dflags env overloadedIfMN "ifte"
-    fromLabelName   <- lookupName dflags env ghcOverloadedLabelsMN "fromLabel"
-
-    fromTypeNatName    <- lookupName' dflags env overloadedTypeNatsMN "FromNat"
-    fromTypeSymbolName <- lookupName' dflags env overloadedTypeSymbolsMN "FromTypeSymbol"
-
-    fmapName <- lookupName dflags env ghcBaseMN "fmap"
-    pureName <- lookupName dflags env ghcBaseMN "pure"
-    apName   <- lookupName dflags env ghcBaseMN "<*>"
-    birdName <- lookupName dflags env ghcBaseMN "<*"
-    voidName <- lookupName dflags env dataFunctorMN "void"
-
-    return Names {..}
-
-lookupName :: GHC.DynFlags -> GHC.HscEnv -> GHC.ModuleName -> String -> TcM.TcM GHC.Name
-lookupName dflags env mn vn = do
-    res <-  liftIO $ Finder.findImportedModule env mn Nothing
-    case res of
-        GHC.Found _ md -> IfaceEnv.lookupOrig md (GHC.mkVarOcc vn)
-        _              -> do
-            liftIO $ GHC.putLogMsg dflags GHC.NoReason Err.SevError noSrcSpan (GHC.defaultErrStyle dflags) $
-                GHC.text "Cannot find module" GHC.<+> GHC.ppr mn
-            fail "panic!"
-
-lookupName' :: GHC.DynFlags -> GHC.HscEnv -> GHC.ModuleName -> String -> TcM.TcM GHC.Name
-lookupName' dflags env mn vn = do
-    res <-  liftIO $ Finder.findImportedModule env mn Nothing
-    case res of
-        GHC.Found _ md -> IfaceEnv.lookupOrig md (GHC.mkTcOcc vn)
-        _              -> do
-            liftIO $ GHC.putLogMsg dflags GHC.NoReason Err.SevError noSrcSpan (GHC.defaultErrStyle dflags) $
-                GHC.text "Cannot find module" GHC.<+> GHC.ppr mn
-            fail "panic!"
-
--- | Module name and variable name
-data VarName = VN String String
-  deriving (Eq, Show)
-
-lookupVarName :: GHC.DynFlags -> GHC.HscEnv -> VarName -> TcM.TcM GHC.Name
-lookupVarName dflags env (VN vn mn) = lookupName dflags env (GHC.mkModuleName vn) mn
-
-lookupTypeName :: GHC.DynFlags -> GHC.HscEnv -> VarName -> TcM.TcM GHC.Name
-lookupTypeName dflags env (VN vn mn) = lookupName' dflags env (GHC.mkModuleName vn) mn
-
--------------------------------------------------------------------------------
--- diagnostics
--------------------------------------------------------------------------------
-
-warn :: MonadIO m => GHC.DynFlags -> SrcSpan -> GHC.SDoc -> m ()
-warn dflags l doc =
-    liftIO $ GHC.putLogMsg dflags GHC.NoReason Err.SevWarning l (GHC.defaultErrStyle dflags) doc
-        --     GHC.text "parsed string"
-        --     GHC.$$
-        --     GHC.ppr fs
-
-debug :: MonadIO m => String -> m ()
--- debug = liftIO . putStrLn
-debug _ = pure ()
-
--------------------------------------------------------------------------------
--- V2 and V4
--------------------------------------------------------------------------------
-
-data V2 a = V2 a a
-  deriving (Eq, Show)
-
-data V4 a = V4 a a a a
-  deriving (Eq, Show)
-
--------------------------------------------------------------------------------
--- Idioms brackets
--------------------------------------------------------------------------------
-
-transformIdiomBrackets
-    :: Names
-    -> LHsExpr GhcRn
-    -> Maybe (LHsExpr GhcRn)
-transformIdiomBrackets names (L _l (HsRnBracketOut _ (ExpBr _ e) _))
-    = Just (transformIdiomBrackets' names e)
-transformIdiomBrackets _ _ = Nothing
-
-transformIdiomBrackets'
-    :: Names
-    -> LHsExpr GhcRn
-    -> LHsExpr GhcRn
-transformIdiomBrackets' names expr@(L _e OpApp {}) = do
-    let bt = matchOp expr
-    let result = idiomBT names bt
-    result
-transformIdiomBrackets' names expr = do
-    let (f :| args) = matchApp expr
-    let f' = pureExpr names f
-    let result = foldl' (applyExpr names) f' args
-    result
-
--------------------------------------------------------------------------------
--- Function application maching
--------------------------------------------------------------------------------
-
--- | Match nested function applications, 'HsApp':
--- f x y z ~> f :| [x,y,z]
---
-matchApp :: LHsExpr p -> NonEmpty (LHsExpr p)
-matchApp (L _ (HsApp _ f x)) = neSnoc (matchApp f) x
-matchApp e = pure e
-
-neSnoc :: NonEmpty a -> a -> NonEmpty a
-neSnoc (x :| xs) y = x :| xs ++ [y]
-
--------------------------------------------------------------------------------
--- Operator application matching
--------------------------------------------------------------------------------
-
--- | Match nested operator applications, 'OpApp'.
--- x + y * z ~>  Branch (+) (Leaf x) (Branch (*) (Leaf y) (Leaf z))
-matchOp :: LHsExpr p -> BT (LHsExpr p)
-matchOp (L _ (OpApp _  lhs op rhs)) = Branch (matchOp lhs) op (matchOp rhs)
-matchOp x = Leaf x
-
--- | Non-empty binary tree, with elements at branches too.
-data BT a = Leaf a | Branch (BT a) a (BT a)
-
--- flatten: note that leaf is returned as is.
-idiomBT :: Names -> BT (LHsExpr GhcRn) -> LHsExpr GhcRn
-idiomBT _     (Leaf x)            = x
-idiomBT names (Branch lhs op rhs) = fmapExpr names op (idiomBT names lhs) `ap` idiomBT names rhs
-  where
-    ap = apExpr names
-
--------------------------------------------------------------------------------
--- Idioms related constructors
--------------------------------------------------------------------------------
-
-applyExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
-applyExpr names f (L _ (HsPar _ (L _ (HsApp _ (L _ (HsVar _ (L _ voidName'))) x))))
-    | voidName' == voidName names = birdExpr names f x
-applyExpr names f x               = apExpr names f x
-
-apExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
-apExpr Names {..} f x = hsApps l' (hsVar l' apName) [f, x] where
-    l' = GHC.noSrcSpan
-
-birdExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
-birdExpr Names {..} f x = hsApps l' (hsVar l' birdName) [f, x] where
-    l' = GHC.noSrcSpan
-
-fmapExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
-fmapExpr Names {..} f x = hsApps l' (hsVar l' fmapName) [f, x] where
-    l' = GHC.noSrcSpan
-
-pureExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn
-pureExpr Names {..} x = hsApps l' (hsVar l' pureName) [x] where
-    l' = GHC.noSrcSpan
-
--------------------------------------------------------------------------------
--- Type-checker plugin
--------------------------------------------------------------------------------
-
-newtype PluginCtx = PluginCtx
-    { hasPolyFieldCls :: Class.Class
-    }
-
-tcPlugin :: TcM.TcPlugin
-tcPlugin = TcM.TcPlugin
-    { TcM.tcPluginInit  = tcPluginInit
-    , TcM.tcPluginSolve = tcPluginSolve
-    , TcM.tcPluginStop  = const (return ())
-    }
-
-tcPluginInit :: TC.TcPluginM PluginCtx
-tcPluginInit = do
-    -- TODO: don't fail
-    res <- TC.findImportedModule ghcRecordsCompatMN Nothing
-    cls <- case res of
-        GHC.Found _ md -> TC.tcLookupClass =<< TC.lookupOrig md (GHC.mkTcOcc "HasField")
-        _              -> do
-            dflags <- TC.unsafeTcPluginTcM GHC.getDynFlags
-            TC.tcPluginIO $ GHC.putLogMsg dflags GHC.NoReason Err.SevError noSrcSpan (GHC.defaultErrStyle dflags) $
-                GHC.text "Cannot find module" GHC.<+> GHC.ppr ghcRecordsCompatMN
-            fail "panic!"
-
-    return PluginCtx
-        { hasPolyFieldCls = cls
-        }
-
--- HasPolyField "petName" Pet Pet [Char] [Char]
-tcPluginSolve :: PluginCtx -> TcRnTypes.TcPluginSolver
-tcPluginSolve PluginCtx {..} _ _ wanteds = do
-    -- acquire context
-    dflags      <- TC.unsafeTcPluginTcM GHC.getDynFlags
-    famInstEnvs <- TC.getFamInstEnvs
-    rdrEnv      <- TC.unsafeTcPluginTcM TcM.getGlobalRdrEnv
-
-    solved <- forM wantedsHasPolyField $ \(ct, tys@(V4 _k _name _s a)) -> do
-        -- TC.tcPluginIO $ warn dflags noSrcSpan $
-        --     GHC.text "wanted" GHC.<+> GHC.ppr ct
-
-        m <- TC.unsafeTcPluginTcM $ matchHasField dflags famInstEnvs rdrEnv tys
-        fmap (\evTerm -> (evTerm, ct)) $ forM m $ \(tc, dc, args, fl, _sel_id) -> do
-            -- get location
-            let ctloc = TcM.ctLoc ct
-            -- let l = GHC.RealSrcSpan $ TcM.ctLocSpan ctloc
-
-            -- debug print
-            -- TC.tcPluginIO $ warn dflags l $ GHC.text "DEBUG" GHC.$$ GHC.ppr dbg
-
-            let s' = GHC.mkTyConApp tc args
-
-            let (exist, theta, xs) = GHC.dataConInstSig dc args
-            let fls                = GHC.dataConFieldLabels dc
-            unless (length xs == length fls) $ fail "|tys| /= |fls|"
-
-            idx <- case elemIndex fl fls of
-                Nothing  -> fail "field selector not in dataCon"
-                Just idx -> return idx
-
-            -- variables we can bind to
-            let exist' = exist
-            let exist_ = map GHC.mkTyVarTy exist'
-
-            theta' <- traverse (makeVar "dict") $ GHC.substTysWith exist exist_ theta
-            xs'   <- traverse (makeVar "x") $ GHC.substTysWith exist exist_ xs
-
-            let a' = xs !! idx
-            let b' = a'
-            let t' = s'
-
-            bName <- TC.unsafeTcPluginTcM $ TcM.newName (GHC.mkVarOcc "b")
-            let bBndr   = GHC.mkLocalId bName $ xs !! idx
-
-            -- (\b -> DC b x1 x2, x0)
-            let rhs = GHC.mkConApp (GHC.tupleDataCon GHC.Boxed 2)
-                    [ GHC.Type $ GHC.mkFunTy b' t'
-                    , GHC.Type a'
-                    , GHC.mkCoreLams [bBndr] $ GHC.mkConApp2 dc (args ++ exist_) $ theta' ++ replace idx bBndr xs'
-                    , GHC.Var $ xs' !! idx
-                    ]
-
-            -- (a -> r, r)
-            let caseType = GHC.mkTyConApp (GHC.tupleTyCon GHC.Boxed 2)
-                    [ GHC.mkFunTy b' t'
-                    , a'
-                    ]
-
-            -- DC x0 x1 x2 -> (\b -> DC b x1 x2, x0)
-            let caseBranch = (GHC.DataAlt dc, exist' ++ theta' ++ xs', rhs)
-
-            -- TC.tcPluginIO $ warn dflags l $
-            --     GHC.text "cases"
-            --     GHC.$$
-            --     GHC.ppr caseType
-            --     GHC.$$
-            --     GHC.ppr caseBranch
-
-
-            -- \s -> case s of DC x0 x1 x2 -> (\b -> DC b x1 x2, x0)
-            sName <- TC.unsafeTcPluginTcM $ TcM.newName (GHC.mkVarOcc "s")
-            let sBndr   = GHC.mkLocalId sName s'
-            let expr   = GHC.mkCoreLams [sBndr] $ GHC.Case (GHC.Var sBndr) sBndr caseType [caseBranch]
-            let evterm = makeEvidence4 hasPolyFieldCls expr tys
-
-            -- wanteds
-            ctEvidence <- TC.newWanted ctloc $ GHC.mkPrimEqPred a a'
-
-            return (evterm, [ TcM.mkNonCanonical ctEvidence -- a ~ a'
-                            ])
-
-    return $ TcRnTypes.TcPluginOk (mapMaybe extractA solved) (concat $ mapMaybe extractB solved)
-  where
-    wantedsHasPolyField = mapMaybe (findClassConstraint4 hasPolyFieldCls) wanteds
-
-    extractA (Nothing, _)     = Nothing
-    extractA (Just (a, _), b) = Just (a, b)
-
-    extractB (Nothing, _)      = Nothing
-    extractB (Just (_, ct), _) = Just ct
-
-replace :: Int -> a -> [a] -> [a]
-replace _ _ []     = []
-replace 0 y (_:xs) = y:xs
-replace n y (x:xs) = x : replace (pred n) y xs
-
-makeVar :: String -> GHC.Type -> TcRnTypes.TcPluginM GHC.Var
-makeVar n ty = do
-    name <- TC.unsafeTcPluginTcM $ TcM.newName (GHC.mkVarOcc n)
-    return (GHC.mkLocalId name ty)
-
--------------------------------------------------------------------------------
--- Simple Ct operations
--------------------------------------------------------------------------------
-
-findClassConstraint4 :: Class.Class -> TcM.Ct -> Maybe (TcM.Ct, V4 GHC.Type)
-findClassConstraint4 cls ct = do
-   (cls', [k, x, s, a]) <- GHC.getClassPredTys_maybe (TcM.ctPred ct)
-   guard (cls' == cls)
-   return (ct, V4 k x s a)
-
--- | Make newtype class evidence
-makeEvidence4 :: Class.Class -> GHC.CoreExpr -> V4 GHC.Type -> Tc.EvTerm
-makeEvidence4 cls e (V4 k x s a) = Tc.EvExpr appDc where
-    tyCon = Class.classTyCon cls
-    dc    = GHC.tyConSingleDataCon tyCon
-    appDc = GHC.mkCoreConApps dc
-        [ GHC.Type k
-        , GHC.Type x
-        , GHC.Type s
-        , GHC.Type a
-        , e
-        ]
--------------------------------------------------------------------------------
--- Adopted from GHC
--------------------------------------------------------------------------------
-
-matchHasField
-    :: GHC.DynFlags
-    -> (FamInstEnv.FamInstEnv, FamInstEnv.FamInstEnv)
-    -> RdrName.GlobalRdrEnv
-    -> V4 GHC.Type
-    -> TcM.TcM (Maybe (GHC.TyCon, GHC.DataCon, [GHC.Type], GHC.FieldLabel, GHC.Id))
-matchHasField _dflags famInstEnvs rdrEnv (V4 _k x s _a)
-    -- x should be a literal string
-    | Just xStr <- GHC.isStrLitTy x
-    -- s should be an applied type constructor
-    , Just (tc, args) <- GHC.tcSplitTyConApp_maybe s
-    -- use representation tycon (if data family); it has the fields
-    , let s_tc = fstOf3 (FamInst.tcLookupDataFamInst famInstEnvs tc args)
-    -- x should be a field of r
-    , Just fl <- GHC.lookupTyConFieldLabel xStr s_tc
-    -- the field selector should be in scope
-    , Just _gre <- RdrName.lookupGRE_FieldLabel rdrEnv fl
-    -- and the type should have only single data constructor (for simplicity)
-    , Just [dc] <- GHC.tyConDataCons_maybe tc
-    = do
-        sel_id <- TcEnv.tcLookupId (GHC.flSelector fl)
-        (_tv_prs, _preds, sel_ty) <- TcMType.tcInstType TcMType.newMetaTyVars sel_id
-
-        -- The selector must not be "naughty" (i.e. the field
-        -- cannot have an existentially quantified type), and
-        -- it must not be higher-rank.
-        if not (GHC.isNaughtyRecordSelector sel_id) && GHC.isTauTy sel_ty
-        then return $ Just (tc, dc, args, fl, sel_id)
-        else return Nothing
-
-matchHasField _ _ _ _ = return Nothing
-
--------------------------------------------------------------------------------
--- Utils
--------------------------------------------------------------------------------
-
-fstOf3 :: (a, b, c) -> a
-fstOf3 (a, _, _) =  a
+        case f e of
+            Rewrite e' -> return e'
+            NoRewrite  -> return e
+            Error err  -> do
+                liftIO $ err dflags
+                fail "Error in Overloaded plugin"
diff --git a/src/Overloaded/Plugin/Categories.hs b/src/Overloaded/Plugin/Categories.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/Categories.hs
@@ -0,0 +1,466 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds          #-}
+{-# LANGUAGE DeriveFunctor      #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE KindSignatures     #-}
+{-# LANGUAGE RecordWildCards    #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module Overloaded.Plugin.Categories where
+
+import Data.Bifunctor       (Bifunctor (..))
+import Data.Bifunctor.Assoc (Assoc (..))
+import Data.Kind            (Type)
+import Data.Map.Strict      (Map)
+import Data.Void            (Void, absurd)
+
+import qualified Data.Generics   as SYB
+import qualified Data.Map.Strict as Map
+import qualified GHC.Compat.All  as GHC
+import           GHC.Compat.Expr
+import qualified GhcPlugins      as Plugins
+
+import Overloaded.Plugin.Diagnostics
+import Overloaded.Plugin.Names
+import Overloaded.Plugin.Rewrite
+
+-------------------------------------------------------------------------------
+-- Rewriter
+-------------------------------------------------------------------------------
+
+transformCategories
+    :: Names
+    -> LHsExpr GhcRn
+    -> Rewrite (LHsExpr GhcRn)
+transformCategories names (L _l (HsProc _ pat (L _ (HsCmdTop _ cmd)))) = do
+    SomePattern pat' <- parsePat pat
+    kont <- parseCmd names (patternMap pat') cmd
+    let proc :: Proc (LHsExpr GhcRn) Void
+        proc = Proc (nameToString <$> pat') kont
+
+        morp :: Morphism (LHsExpr GhcRn)
+        morp = desugar absurd proc
+
+        expr :: LHsExpr GhcRn
+        expr = generate names morp
+
+    -- _ <- Error $ \dflags -> putError dflags _l $ GHC.text "DEBUG"
+    --     GHC.$$ GHC.text (show $ first (GHC.showPpr dflags) proc)
+    --     GHC.$$ GHC.text (show $ fmap  (GHC.showPpr dflags) morp)
+    --     GHC.$$ GHC.ppr expr
+
+    return expr
+
+transformCategories _ _ = NoRewrite
+
+-------------------------------------------------------------------------------
+-- Parsing
+-------------------------------------------------------------------------------
+
+parsePat :: LPat GhcRn -> Rewrite (SomePattern GHC.Name)
+#if MIN_VERSION_ghc(8,8,0) && !MIN_VERSION_ghc(8,10,1)
+parsePat (XPat (L l pat)) = parsePat' l pat
+parsePat pat              = parsePat' noSrcSpan pat
+#else
+parsePat (L l pat) = parsePat' l pat
+#endif
+
+parsePat' :: SrcSpan -> Pat GhcRn -> Rewrite (SomePattern GHC.Name)
+parsePat' _ WildPat {} =
+    return $ SomePattern PatternWild
+parsePat' _ (VarPat _ (L _ name)) =
+    return $ SomePattern $ PatternVar name
+parsePat' _ (TuplePat _ [x, y] Plugins.Boxed) = do
+    SomePattern x' <- parsePat x
+    SomePattern y' <- parsePat y
+    return $ SomePattern $ PatternTuple x' y'
+parsePat' l TuplePat {} = Error $ \dflags ->
+    putError dflags l $ GHC.text "Overloaded:Categories: only boxed tuples of arity 2 are supported"
+parsePat' l pat = Error $ \dflags ->
+    putError dflags l $ GHC.text "Cannot parse pattern for Overloaded:Categories"
+        GHC.$$ GHC.ppr pat
+        GHC.$$ GHC.text (SYB.gshow pat)
+
+parseExpr
+    :: Names
+    -> Map GHC.Name b
+    -> LHsExpr GhcRn
+    -> Rewrite (Expression (Var b a))
+parseExpr names ctx (L _ (HsPar _ expr)) =
+    parseExpr names ctx expr
+parseExpr _     ctx (L _ (HsVar _ (L l name)))
+    | name == GHC.getName (GHC.tupleDataCon GHC.Boxed 0)
+    = return ExpressionUnit
+    | otherwise
+    = case Map.lookup name ctx of
+        Nothing -> Error $ \dflags ->
+            putError dflags l $ GHC.text "Overloaded:Categories: Unbound variable" GHC.<+> GHC.ppr name
+        Just b -> return $ ExpressionVar (B b)
+parseExpr names ctx (L _ (ExplicitTuple _ [L _ (Present _ x), L _ (Present _ y)] Plugins.Boxed)) = do
+    x' <- parseExpr names ctx x
+    y' <- parseExpr names ctx y
+    return (ExpressionTuple x' y')
+parseExpr _     _ (L l ExplicitTuple {}) = Error $ \dflags ->
+    putError dflags l $ GHC.text "Overloaded:Categories: only boxed tuples of arity 2 are supported"
+parseExpr names ctx (L _ (HsApp _ (L _ (HsVar _ (L l fName))) x))
+    | fName == conLeftName names = do
+        x' <- parseExpr names ctx x
+        return (ExpressionLeft x')
+    | fName == conRightName names = do
+        x' <- parseExpr names ctx x
+        return (ExpressionRight x')
+    | otherwise = Error $ \dflags ->
+        putError dflags l $ GHC.text "Overloaded:Categories: only applications of Left and Right are supported"
+parseExpr _     _   (L l expr) = Error $ \dflags ->
+    putError dflags l $ GHC.text "Cannot parse -< right-hand-side for Overloaded:Categories"
+        GHC.$$ GHC.ppr expr
+        GHC.$$ GHC.text (SYB.gshow expr)
+
+parseCmd
+    :: Names
+    -> Map GHC.Name b
+    -> LHsCmd GhcRn
+    -> Rewrite (Continuation (LHsExpr GhcRn) (Var b a))
+parseCmd names ctx (L _ (HsCmdDo _ (L l stmts))) =
+    parseStmts names ctx l stmts
+parseCmd names ctx (L _ (HsCmdArrApp _ morp expr HsFirstOrderApp _)) = do
+    morp' <- parseTerm names morp
+    expr' <- parseExpr names ctx expr
+    return $ Last (Right morp') expr'
+parseCmd names ctx (L _ (HsCmdArrApp _ morp expr HsHigherOrderApp _)) = do
+    morp' <- parseExpr names ctx morp
+    expr' <- parseExpr names ctx expr
+    return $ Last (Left morp') expr'
+parseCmd names ctx (L _ (HsCmdCase _ expr matchGroup)) =
+    case mg_alts matchGroup of
+#if MIN_VERSION_ghc(8,8,0) && !MIN_VERSION_ghc(8,10,1)
+        L _ [ L _ Match { m_pats = [XPat (L _ (ConPatIn (L _ acon) aargs))], m_grhss = abody' }
+            , L _ Match { m_pats = [XPat (L _ (ConPatIn (L _ bcon) bargs))], m_grhss = bbody' }
+            ]
+#else
+        L _ [ L _ Match { m_pats = [L _ (ConPatIn (L _ acon) aargs)], m_grhss = abody' }
+            , L _ Match { m_pats = [L _ (ConPatIn (L _ bcon) bargs)], m_grhss = bbody' }
+            ]
+#endif
+            -- Left and Right, or Right and Left
+            |  [acon,bcon] == [conLeftName names,conRightName names]
+            || [acon,bcon] == [conRightName names,conLeftName names]
+            -- only one argument
+            , [aarg] <- hsConPatArgs aargs
+            , [barg] <- hsConPatArgs bargs
+            -- and simple bodies
+            , Just abody <- simpleGRHSs abody'
+            , Just bbody <- simpleGRHSs bbody'
+
+            -> do
+                expr' <- parseExpr names ctx expr
+
+                SomePattern apat <- parsePat aarg
+                SomePattern bpat <- parsePat barg
+
+                acont <- parseCmd names (combineMaps ctx apat) abody
+                bcont <- parseCmd names (combineMaps ctx bpat) bbody
+
+                -- Error $ \dflags -> putError dflags noSrcSpan $ GHC.text "TODO"
+                --     GHC.$$ GHC.ppr acon
+                --     GHC.$$ GHC.ppr bcon
+                --     GHC.$$ GHC.ppr aarg
+                --     GHC.$$ GHC.ppr barg
+                --     GHC.$$ GHC.ppr abody
+                --     GHC.$$ GHC.ppr bbody
+
+                return $ caseCont expr' apat bpat (second assoc acont) (second assoc bcont)
+
+        L l _ -> Error $ \dflags ->
+            putError dflags l $ GHC.text "Overloaded:Categories only case of Left and Right are supported"
+                GHC.$$ GHC.text (SYB.gshow (mg_alts matchGroup))
+parseCmd _     _   (L l cmd) =
+    Error $ \dflags ->
+        putError dflags l $ GHC.text "Unsupported command in proc for Overloaded:Categories"
+            GHC.$$ GHC.ppr cmd
+            GHC.$$ GHC.text (SYB.gshow cmd)
+
+simpleGRHSs :: GRHSs GhcRn body -> Maybe body
+simpleGRHSs (GRHSs _ [L _ (GRHS _ [] body)] (L _ (EmptyLocalBinds _))) = Just body
+simpleGRHSs _ = Nothing
+
+parseTerm
+    :: Names
+    -> LHsExpr GhcRn
+    -> Rewrite (Morphism (LHsExpr GhcRn))
+parseTerm Names {catNames = CatNames {..}} (L _ (HsVar _ (L _ name)))
+    | name == catIdentityName = return MId
+parseTerm _ term = return (MTerm term)
+
+parseStmts
+    :: Names
+    -> Map GHC.Name b
+    -> SrcSpan
+    -> [CmdLStmt GhcRn]
+    -> Rewrite (Continuation (LHsExpr GhcRn) (Var b a))
+parseStmts names ctx _ (L l (BindStmt _ pat body _ _) : next) = do
+    SomePattern pat' <- parsePat pat
+    cont1 <- parseCmd names ctx body
+    cont2 <- parseStmts names (combineMaps ctx pat') l next
+    return $ compCont (nameToString <$> pat') cont1 (second assoc cont2)
+parseStmts names ctx _ [L _ (LastStmt _ body _ _)] =
+    parseCmd names ctx body
+parseStmts _     _   _ (L l stmt : _) =
+    Error $ \dflags ->
+        putError dflags l $ GHC.text "Unsupported statement in proc-do for Overloaded:Categories"
+            GHC.$$ GHC.ppr stmt
+            GHC.$$ GHC.text (SYB.gshow stmt)
+parseStmts _     _   l [] =
+    Error $ \dflags ->
+        putError dflags l $ GHC.text "Empty do block in proc"
+
+-------------------------------------------------------------------------------
+-- Variables
+-------------------------------------------------------------------------------
+
+data Var b a
+    = B b
+    | F a
+  deriving (Show, Functor)
+
+instance Bifunctor Var where
+    bimap f _ (B b) = B (f b)
+    bimap _ g (F a) = F (g a)
+
+instance Assoc Var where
+    assoc (B (B x)) = B x
+    assoc (B (F y)) = F (B y)
+    assoc (F z)     = F (F z)
+
+    unassoc (B x)     = B (B x)
+    unassoc (F (B y)) = B (F y)
+    unassoc (F (F z)) = F z
+
+unvar :: (b -> c) -> (a -> c) -> Var b a -> c
+unvar f _ (B b) = f b
+unvar _ g (F a) = g a
+
+-------------------------------------------------------------------------------
+-- A subset of Arrow notation syntax we support.
+-------------------------------------------------------------------------------
+
+-- | Proc syntax
+data Proc term a where
+    Proc :: Pattern sh String -> Continuation term (Var (Index sh) a) -> Proc term a
+
+deriving instance (Show a, Show term) => Show (Proc term a)
+
+instance Bifunctor Proc where
+    bimap f g (Proc p c) = Proc p (bimap f (fmap g) c)
+
+data Continuation term a where
+    Last :: Either (Expression a) (Morphism term) -> Expression a -> Continuation term a
+      -- ^ term -< y
+    Edge
+        :: Pattern sh String
+        -> Either (Expression a) (Morphism term)
+        -> Expression a
+        -> Continuation term (Var (Index sh) a)
+        -> Continuation term a
+      -- ^ x <- term -< y
+
+    Split
+        :: Expression a
+        -> Pattern shA String
+        -> Pattern shB String
+        -> Continuation term (Var (Index shA) a)
+        -> Continuation term (Var (Index shB) a)
+        -> Continuation term a
+
+deriving instance (Show a, Show term) => Show (Continuation term a)
+
+instance Bifunctor Continuation where
+    bimap f g (Last term e)         = Last (bimap (fmap g) (fmap f) term) (fmap g e)
+    bimap f g (Edge p term e c)     = Edge p (bimap (fmap g) (fmap f) term) (fmap g e) (bimap f (fmap g) c)
+    bimap f g (Split e pa pb ca cb) = Split (fmap g e) pa pb
+        (bimap f (fmap g) ca)
+        (bimap f (fmap g) cb)
+
+instance Functor (Continuation term) where
+    fmap = second
+
+compCont
+    :: Pattern sh String
+    -> Continuation term a
+    -> Continuation term (Var (Index sh) a)
+    -> Continuation term a
+compCont pat (Last term expr) c
+    = Edge pat term expr c
+compCont pat (Edge pat' term expr c') c
+    = Edge pat' term expr
+    $ compCont pat c' (weaken1 c)
+compCont pat (Split expr patA patB contA contB) c
+    = Split expr patA patB
+        (compCont pat contA (weaken1 c))
+        (compCont pat contB (weaken1 c))
+
+weaken1 :: Functor f => f (Var a b) -> f (Var a (Var c b))
+weaken1 = fmap (unvar B (F . F))
+
+caseCont
+    :: Expression a
+    -> Pattern shA Plugins.Name
+    -> Pattern shB Plugins.Name
+    -> Continuation (LHsExpr GhcRn) (Var (Index shA) a)
+    -> Continuation (LHsExpr GhcRn) (Var (Index shB) a)
+    -> Continuation (LHsExpr GhcRn) a
+caseCont e patA patB =
+    Split e (fmap nameToString patA) (fmap nameToString patB)
+
+-------------------------------------------------------------------------------
+-- Patterns
+-------------------------------------------------------------------------------
+
+data Shape = One | Two Shape Shape
+
+data Pattern :: Shape -> Type -> Type where
+    PatternVar   :: a -> Pattern 'One a
+    PatternWild  :: Pattern 'One a
+    PatternTuple :: Pattern l a -> Pattern r a -> Pattern ('Two l r) a
+
+deriving instance Show a => Show (Pattern sh a)
+deriving instance Functor (Pattern sh)
+
+data SomePattern :: Type -> Type where
+    SomePattern :: Pattern sh a -> SomePattern a
+
+data Index :: Shape -> Type where
+    Here :: Index 'One
+    InL  :: Index x -> Index ('Two x y)
+    InR  :: Index y -> Index ('Two x y)
+
+deriving instance Show (Index sh)
+
+patternMap :: Ord a => Pattern sh a -> Map a (Index sh)
+patternMap (PatternVar x)     = Map.singleton x Here
+patternMap PatternWild        = Map.empty
+patternMap (PatternTuple l r) = Map.union
+    (Map.map InL (patternMap l))
+    (Map.map InR (patternMap r))
+
+combineMaps
+    :: Map Plugins.Name b
+    -> Pattern sh Plugins.Name
+    -> Map Plugins.Name (Var (Index sh) b)
+combineMaps m pat = Map.union (Map.map F m) (Map.map B (patternMap pat))
+
+-------------------------------------------------------------------------------
+-- Expressions
+-------------------------------------------------------------------------------
+
+data Expression a
+    = ExpressionVar a
+    | ExpressionUnit
+    | ExpressionTuple (Expression a) (Expression a)
+    | ExpressionLeft (Expression a)
+    | ExpressionRight (Expression a)
+  deriving (Show, Functor)
+
+-------------------------------------------------------------------------------
+-- Skeleton of syntax we desugar arrow notation to
+-------------------------------------------------------------------------------
+
+-- | Note: morpisms don't have variables!
+data Morphism term
+    = MId
+    | MCompose (Morphism term) (Morphism term)
+    | MProduct (Morphism term) (Morphism term)
+    | MTerminal
+    | MProj1
+    | MProj2
+    | MInL
+    | MInR
+    | MCase (Morphism term) (Morphism term)
+    | MDistr
+    | MEval
+    | MTerm term
+  deriving (Show, Functor)
+
+instance Semigroup (Morphism term) where
+    MTerminal <> _            = MTerminal
+    MId       <> m            = m
+    m         <> MId          = m
+    MProj1    <> MProduct f _ = f
+    MProj2    <> MProduct _ g = g
+    MCase f _ <> MInL         = f
+    MCase _ g <> MInR         = g
+    f         <> g            = MCompose f g
+
+instance Monoid (Morphism term) where
+    mempty  = MId
+    mappend = (<>)
+
+-------------------------------------------------------------------------------
+-- Desugaring
+-------------------------------------------------------------------------------
+
+desugar :: (a -> Morphism term) -> Proc term a -> Morphism term
+desugar ctx (Proc p k) = desugarC (unvar (desugarP p) ctx) k
+
+desugarC :: (a -> Morphism term) -> Continuation term a -> Morphism term
+desugarC ctx (Last (Right term) e) = mconcat
+    [ term
+    , desugarE ctx e
+    ]
+desugarC ctx (Last (Left f) e) = mconcat
+    [ MEval
+    , MProduct (desugarE ctx f) (desugarE ctx e)
+    ]
+desugarC ctx (Edge p (Right term) e k) = mconcat
+    [ desugarC (unvar (\x -> desugarP p x <> MProj1) (\y -> ctx y <> MProj2)) k
+    , MProduct
+        (term <> desugarE ctx e)
+        MId
+    ]
+desugarC ctx (Edge p (Left f) e k) = mconcat
+    [ desugarC (unvar (\x -> desugarP p x <> MEval <> MProj1) (\y -> ctx y <> MProj2)) k
+    , MProduct
+        (MProduct (desugarE ctx f) (desugarE ctx e))
+        MId
+    ]
+desugarC ctx (Split e pa pb ka kb) = mconcat
+    [ MCase
+        (desugarC (unvar (\x -> desugarP pa x <> MProj1) (\y -> ctx y <> MProj2)) ka)
+        (desugarC (unvar (\x -> desugarP pb x <> MProj1) (\y -> ctx y <> MProj2)) kb)
+    , MDistr
+    , MProduct
+        (desugarE ctx e)
+        MId
+    ]
+
+desugarP :: Pattern sh name -> Index sh -> Morphism term
+desugarP (PatternVar _)     Here    = MId
+desugarP PatternWild        Here    = MId
+desugarP (PatternTuple l _) (InL i) = desugarP l i <> MProj1
+desugarP (PatternTuple _ r) (InR i) = desugarP r i <> MProj2
+
+desugarE :: (a -> Morphism term) -> Expression a -> Morphism term
+desugarE ctx = go where
+    go ExpressionUnit        = MTerminal
+    go (ExpressionVar a)     = ctx a
+    go (ExpressionTuple x y) = MProduct (go x) (go y)
+    go (ExpressionLeft x)    = MInL <> go x
+    go (ExpressionRight y)   = MInR <> go y
+
+-------------------------------------------------------------------------------
+-- Generating
+-------------------------------------------------------------------------------
+
+generate :: Names -> Morphism (LHsExpr GhcRn) -> LHsExpr GhcRn
+generate Names {catNames = CatNames {..}} = go where
+    go MId            = hsVar noSrcSpan catIdentityName
+    go (MCompose f g) = hsPar noSrcSpan $ hsOpApp noSrcSpan (go f) (hsVar noSrcSpan catComposeName) (go g)
+    go (MTerm term)   = term
+    go MTerminal      = hsVar noSrcSpan catTerminalName
+    go MProj1         = hsVar noSrcSpan catProj1Name
+    go MProj2         = hsVar noSrcSpan catProj2Name
+    go (MProduct f g) = hsPar noSrcSpan $ hsApps noSrcSpan (hsVar noSrcSpan catFanoutName) [go f, go g]
+    go MInL           = hsVar noSrcSpan catInlName
+    go MInR           = hsVar noSrcSpan catInrName
+    go MDistr         = hsVar noSrcSpan catDistrName
+    go MEval          = hsVar noSrcSpan catEvalName
+    go (MCase f g)    = hsPar noSrcSpan $ hsApps noSrcSpan (hsVar noSrcSpan catFaninName) [go f, go g]
diff --git a/src/Overloaded/Plugin/Diagnostics.hs b/src/Overloaded/Plugin/Diagnostics.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/Diagnostics.hs
@@ -0,0 +1,22 @@
+module Overloaded.Plugin.Diagnostics where
+
+import Control.Monad.IO.Class (MonadIO (..))
+
+import qualified GHC.Compat.All  as GHC
+import           GHC.Compat.Expr
+
+-------------------------------------------------------------------------------
+-- Doesn't really belong here
+-------------------------------------------------------------------------------
+
+putError :: MonadIO m => GHC.DynFlags -> SrcSpan -> GHC.SDoc -> m ()
+putError dflags l doc =
+    liftIO $ GHC.putLogMsg dflags GHC.NoReason GHC.SevError l (GHC.defaultErrStyle dflags) doc
+
+warn :: MonadIO m => GHC.DynFlags -> SrcSpan -> GHC.SDoc -> m ()
+warn dflags l doc =
+    liftIO $ GHC.putLogMsg dflags GHC.NoReason GHC.SevWarning l (GHC.defaultErrStyle dflags) doc
+
+debug :: MonadIO m => String -> m ()
+-- debug = liftIO . putStrLn
+debug _ = pure ()
diff --git a/src/Overloaded/Plugin/HasField.hs b/src/Overloaded/Plugin/HasField.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/HasField.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE RecordWildCards #-}
+module Overloaded.Plugin.HasField where
+
+import Control.Monad (forM, guard, unless)
+import Data.List     (elemIndex)
+import Data.Maybe    (mapMaybe)
+
+import qualified GHC.Compat.All  as GHC
+import           GHC.Compat.Expr
+import qualified TcPluginM       as Plugins
+
+import Overloaded.Plugin.Names
+import Overloaded.Plugin.V
+
+newtype PluginCtx = PluginCtx
+    { hasPolyFieldCls :: GHC.Class
+    }
+
+tcPlugin :: GHC.TcPlugin
+tcPlugin = GHC.TcPlugin
+    { GHC.tcPluginInit  = tcPluginInit
+    , GHC.tcPluginSolve = tcPluginSolve
+    , GHC.tcPluginStop  = const (return ())
+    }
+
+tcPluginInit :: GHC.TcPluginM PluginCtx
+tcPluginInit = do
+    -- TODO: don't fail
+    res <- Plugins.findImportedModule ghcRecordsCompatMN Nothing
+    cls <- case res of
+        GHC.Found _ md -> Plugins.tcLookupClass =<< Plugins.lookupOrig md (GHC.mkTcOcc "HasField")
+        _              -> do
+            dflags <- GHC.unsafeTcPluginTcM GHC.getDynFlags
+            Plugins.tcPluginIO $ GHC.putLogMsg dflags GHC.NoReason GHC.SevError noSrcSpan (GHC.defaultErrStyle dflags) $
+                GHC.text "Cannot find module" GHC.<+> GHC.ppr ghcRecordsCompatMN
+            fail "panic!"
+
+    return PluginCtx
+        { hasPolyFieldCls = cls
+        }
+
+-- HasPolyField "petName" Pet Pet [Char] [Char]
+tcPluginSolve :: PluginCtx -> GHC.TcPluginSolver
+tcPluginSolve PluginCtx {..} _ _ wanteds = do
+    -- acquire context
+    dflags      <- Plugins.unsafeTcPluginTcM GHC.getDynFlags
+    famInstEnvs <- Plugins.getFamInstEnvs
+    rdrEnv      <- Plugins.unsafeTcPluginTcM GHC.getGlobalRdrEnv
+
+    solved <- forM wantedsHasPolyField $ \(ct, tys@(V4 _k _name _s a)) -> do
+        -- GHC.tcPluginIO $ warn dflags noSrcSpan $
+        --     GHC.text "wanted" GHC.<+> GHC.ppr ct
+
+        m <- GHC.unsafeTcPluginTcM $ matchHasField dflags famInstEnvs rdrEnv tys
+        fmap (\evTerm -> (evTerm, ct)) $ forM m $ \(tc, dc, args, fl, _sel_id) -> do
+            -- get location
+            let ctloc = GHC.ctLoc ct
+            -- let l = GHC.RealSrcSpan $ GHC.ctLocSpan ctloc
+
+            -- debug print
+            -- GHC.tcPluginIO $ warn dflags l $ GHC.text "DEBUG" GHC.$$ GHC.ppr dbg
+
+            let s' = GHC.mkTyConApp tc args
+
+            let (exist, theta, xs) = GHC.dataConInstSig dc args
+            let fls                = GHC.dataConFieldLabels dc
+            unless (length xs == length fls) $ fail "|tys| /= |fls|"
+
+            idx <- case elemIndex fl fls of
+                Nothing  -> fail "field selector not in dataCon"
+                Just idx -> return idx
+
+            -- variables we can bind to
+            let exist' = exist
+            let exist_ = map GHC.mkTyVarTy exist'
+
+            theta' <- traverse (makeVar "dict") $ GHC.substTysWith exist exist_ theta
+            xs'   <- traverse (makeVar "x") $ GHC.substTysWith exist exist_ xs
+
+            let a' = xs !! idx
+            let b' = a'
+            let t' = s'
+
+            bName <- GHC.unsafeTcPluginTcM $ GHC.newName (GHC.mkVarOcc "b")
+            let bBndr   = GHC.mkLocalId bName $ xs !! idx
+
+            -- (\b -> DC b x1 x2, x0)
+            let rhs = GHC.mkConApp (GHC.tupleDataCon GHC.Boxed 2)
+                    [ GHC.Type $ GHC.mkFunTy b' t'
+                    , GHC.Type a'
+                    , GHC.mkCoreLams [bBndr] $ GHC.mkConApp2 dc (args ++ exist_) $ theta' ++ replace idx bBndr xs'
+                    , GHC.Var $ xs' !! idx
+                    ]
+
+            -- (a -> r, r)
+            let caseType = GHC.mkTyConApp (GHC.tupleTyCon GHC.Boxed 2)
+                    [ GHC.mkFunTy b' t'
+                    , a'
+                    ]
+
+            -- DC x0 x1 x2 -> (\b -> DC b x1 x2, x0)
+            let caseBranch = (GHC.DataAlt dc, exist' ++ theta' ++ xs', rhs)
+
+            -- GHC.tcPluginIO $ warn dflags l $
+            --     GHC.text "cases"
+            --     GHC.$$
+            --     GHC.ppr caseType
+            --     GHC.$$
+            --     GHC.ppr caseBranch
+
+
+            -- \s -> case s of DC x0 x1 x2 -> (\b -> DC b x1 x2, x0)
+            sName <- GHC.unsafeTcPluginTcM $ GHC.newName (GHC.mkVarOcc "s")
+            let sBndr   = GHC.mkLocalId sName s'
+            let expr   = GHC.mkCoreLams [sBndr] $ GHC.Case (GHC.Var sBndr) sBndr caseType [caseBranch]
+            let evterm = makeEvidence4 hasPolyFieldCls expr tys
+
+            -- wanteds
+            ctEvidence <- Plugins.newWanted ctloc $ GHC.mkPrimEqPred a a'
+
+            return (evterm, [ GHC.mkNonCanonical ctEvidence -- a ~ a'
+                            ])
+
+    return $ GHC.TcPluginOk (mapMaybe extractA solved) (concat $ mapMaybe extractB solved)
+  where
+    wantedsHasPolyField = mapMaybe (findClassConstraint4 hasPolyFieldCls) wanteds
+
+    extractA (Nothing, _)     = Nothing
+    extractA (Just (a, _), b) = Just (a, b)
+
+    extractB (Nothing, _)      = Nothing
+    extractB (Just (_, ct), _) = Just ct
+
+replace :: Int -> a -> [a] -> [a]
+replace _ _ []     = []
+replace 0 y (_:xs) = y:xs
+replace n y (x:xs) = x : replace (pred n) y xs
+
+makeVar :: String -> GHC.Type -> GHC.TcPluginM GHC.Var
+makeVar n ty = do
+    name <- GHC.unsafeTcPluginTcM $ GHC.newName (GHC.mkVarOcc n)
+    return (GHC.mkLocalId name ty)
+
+-------------------------------------------------------------------------------
+-- Simple Ct operations
+-------------------------------------------------------------------------------
+
+findClassConstraint4 :: GHC.Class -> GHC.Ct -> Maybe (GHC.Ct, V4 GHC.Type)
+findClassConstraint4 cls ct = do
+   (cls', [k, x, s, a]) <- GHC.getClassPredTys_maybe (GHC.ctPred ct)
+   guard (cls' == cls)
+   return (ct, V4 k x s a)
+
+-- | Make newtype class evidence
+makeEvidence4 :: GHC.Class -> GHC.CoreExpr -> V4 GHC.Type -> GHC.EvTerm
+makeEvidence4 cls e (V4 k x s a) = GHC.EvExpr appDc where
+    tyCon = GHC.classTyCon cls
+    dc    = GHC.tyConSingleDataCon tyCon
+    appDc = GHC.mkCoreConApps dc
+        [ GHC.Type k
+        , GHC.Type x
+        , GHC.Type s
+        , GHC.Type a
+        , e
+        ]
+
+-------------------------------------------------------------------------------
+-- Adopted from GHC
+-------------------------------------------------------------------------------
+
+matchHasField
+    :: GHC.DynFlags
+    -> (GHC.FamInstEnv, GHC.FamInstEnv)
+    -> GHC.GlobalRdrEnv
+    -> V4 GHC.Type
+    -> GHC.TcM (Maybe (GHC.TyCon, GHC.DataCon, [GHC.Type], GHC.FieldLabel, GHC.Id))
+matchHasField _dflags famInstEnvs rdrEnv (V4 _k x s _a)
+    -- x should be a literal string
+    | Just xStr <- GHC.isStrLitTy x
+    -- s should be an applied type constructor
+    , Just (tc, args) <- GHC.tcSplitTyConApp_maybe s
+    -- use representation tycon (if data family); it has the fields
+    , let s_tc = fstOf3 (GHC.tcLookupDataFamInst famInstEnvs tc args)
+    -- x should be a field of r
+    , Just fl <- GHC.lookupTyConFieldLabel xStr s_tc
+    -- the field selector should be in scope
+    , Just _gre <- GHC.lookupGRE_FieldLabel rdrEnv fl
+    -- and the type should have only single data constructor (for simplicity)
+    , Just [dc] <- GHC.tyConDataCons_maybe tc
+    = do
+        sel_id <- GHC.tcLookupId (GHC.flSelector fl)
+        (_tv_prs, _preds, sel_ty) <- GHC.tcInstType GHC.newMetaTyVars sel_id
+
+        -- The selector must not be "naughty" (i.e. the field
+        -- cannot have an existentially quantified type), and
+        -- it must not be higher-rank.
+        if not (GHC.isNaughtyRecordSelector sel_id) && GHC.isTauTy sel_ty
+        then return $ Just (tc, dc, args, fl, sel_id)
+        else return Nothing
+
+matchHasField _ _ _ _ = return Nothing
+
+-------------------------------------------------------------------------------
+-- Utils
+-------------------------------------------------------------------------------
+
+fstOf3 :: (a, b, c) -> a
+fstOf3 (a, _, _) =  a
diff --git a/src/Overloaded/Plugin/IdiomBrackets.hs b/src/Overloaded/Plugin/IdiomBrackets.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/IdiomBrackets.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE RecordWildCards #-}
+module Overloaded.Plugin.IdiomBrackets where
+
+import Data.List          (foldl')
+import Data.List.NonEmpty (NonEmpty (..))
+
+import GHC.Compat.Expr
+
+import Overloaded.Plugin.Rewrite
+import Overloaded.Plugin.Names
+
+transformIdiomBrackets
+    :: Names
+    -> LHsExpr GhcRn
+    -> Rewrite (LHsExpr GhcRn)
+transformIdiomBrackets names (L _l (HsRnBracketOut _ (ExpBr _ e) _))
+    = Rewrite (transformIdiomBrackets' names e)
+transformIdiomBrackets _ _ = NoRewrite
+
+transformIdiomBrackets'
+    :: Names
+    -> LHsExpr GhcRn
+    -> LHsExpr GhcRn
+transformIdiomBrackets' names expr@(L _e OpApp {}) = do
+    let bt = matchOp expr
+    let result = idiomBT names bt
+    result
+transformIdiomBrackets' names expr = do
+    let (f :| args) = matchApp expr
+    let f' = pureExpr names f
+    let result = foldl' (applyExpr names) f' args
+    result
+
+-------------------------------------------------------------------------------
+-- Function application maching
+-------------------------------------------------------------------------------
+
+-- | Match nested function applications, 'HsApp':
+-- f x y z ~> f :| [x,y,z]
+--
+matchApp :: LHsExpr p -> NonEmpty (LHsExpr p)
+matchApp (L _ (HsApp _ f x)) = neSnoc (matchApp f) x
+matchApp e = pure e
+
+neSnoc :: NonEmpty a -> a -> NonEmpty a
+neSnoc (x :| xs) y = x :| xs ++ [y]
+
+-------------------------------------------------------------------------------
+-- Operator application matching
+-------------------------------------------------------------------------------
+
+-- | Match nested operator applications, 'OpApp'.
+-- x + y * z ~>  Branch (+) (Leaf x) (Branch (*) (Leaf y) (Leaf z))
+matchOp :: LHsExpr p -> BT (LHsExpr p)
+matchOp (L _ (OpApp _  lhs op rhs)) = Branch (matchOp lhs) op (matchOp rhs)
+matchOp x = Leaf x
+
+-- | Non-empty binary tree, with elements at branches too.
+data BT a = Leaf a | Branch (BT a) a (BT a)
+
+-- flatten: note that leaf is returned as is.
+idiomBT :: Names -> BT (LHsExpr GhcRn) -> LHsExpr GhcRn
+idiomBT _     (Leaf x)            = x
+idiomBT names (Branch lhs op rhs) = fmapExpr names op (idiomBT names lhs) `ap` idiomBT names rhs
+  where
+    ap = apExpr names
+
+-------------------------------------------------------------------------------
+-- Idioms related constructors
+-------------------------------------------------------------------------------
+
+applyExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
+applyExpr names f (L _ (HsPar _ (L _ (HsApp _ (L _ (HsVar _ (L _ voidName'))) x))))
+    | voidName' == voidName names = birdExpr names f x
+applyExpr names f x               = apExpr names f x
+
+apExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
+apExpr Names {..} f x = hsApps l' (hsVar l' apName) [f, x] where
+    l' = noSrcSpan
+
+birdExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
+birdExpr Names {..} f x = hsApps l' (hsVar l' birdName) [f, x] where
+    l' = noSrcSpan
+
+fmapExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn -> LHsExpr GhcRn
+fmapExpr Names {..} f x = hsApps l' (hsVar l' fmapName) [f, x] where
+    l' = noSrcSpan
+
+pureExpr :: Names -> LHsExpr GhcRn -> LHsExpr GhcRn
+pureExpr Names {..} x = hsApps l' (hsVar l' pureName) [x] where
+    l' = noSrcSpan
diff --git a/src/Overloaded/Plugin/LocalDo.hs b/src/Overloaded/Plugin/LocalDo.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/LocalDo.hs
@@ -0,0 +1,64 @@
+module Overloaded.Plugin.LocalDo where
+
+import qualified Data.Generics   as SYB
+import qualified GHC.Compat.All  as GHC
+import           GHC.Compat.Expr
+import qualified GhcPlugins      as Plugins
+
+import Overloaded.Plugin.Diagnostics
+import Overloaded.Plugin.Names
+import Overloaded.Plugin.Rewrite
+
+transformDo
+    :: Names
+    -> LHsExpr GhcRn
+    -> Rewrite (LHsExpr GhcRn)
+transformDo names (L l (OpApp _ (L (RealSrcSpan l1) (HsVar _ (L _ doName)))
+                                (L (RealSrcSpan l2) (HsVar _ (L _ compName')))
+                                (L (RealSrcSpan l3) (HsDo _ DoExpr (L _ stmts)))))
+    | spanNextTo l1 l2
+    , spanNextTo l2 l3
+    , compName' == composeName names
+    = case transformDo' names doName l stmts of
+        Right x  -> Rewrite x
+        Left err -> Error err
+transformDo _ _ = NoRewrite
+
+transformDo' :: Names -> GHC.Name -> SrcSpan -> [ExprLStmt GhcRn] -> Either (GHC.DynFlags -> IO ()) (LHsExpr GhcRn)
+transformDo' _names _doName l [] = Left $ \dflags ->
+    putError dflags l $ GHC.text "Empty do"
+transformDo'  names  doName _ (L l (BindStmt _ pat body _ _) : next) = do
+    next' <- transformDo' names doName l next
+    return $ hsApps l bind [ body, kont next' ]
+  where
+    bind  = hsTyApp l (hsVar l doName) (hsTyVar l (doBindName names))
+    kont next' = L l $ HsLam noExtField MG
+        { mg_ext    = noExtField
+        , mg_alts   = L l $ pure $ L l Match
+            { m_ext   = noExtField
+            , m_ctxt  = LambdaExpr
+            , m_pats  = [pat]
+            , m_grhss = GRHSs
+                { grhssExt        = noExtField
+                , grhssGRHSs      = [ L noSrcSpan $ GRHS noExtField [] $ next' ]
+                , grhssLocalBinds = L noSrcSpan $ EmptyLocalBinds noExtField
+                }
+            }
+        , mg_origin = Plugins.Generated
+        }
+transformDo'  names  doName _ (L l (BodyStmt _ body _ _) : next) = do
+    next' <- transformDo' names doName l next
+    return $ hsApps l then_ [ body, next' ]
+  where
+    then_ = hsTyApp l (hsVar l doName) (hsTyVar l (doThenName names))
+
+transformDo' _ _ _ [L _ (LastStmt _ body _ _)] = return body
+transformDo' _ _ _ (L l stmt : _) = Left $ \dflags ->
+    putError dflags l $ GHC.text "Unsupported statement in do"
+        GHC.$$ GHC.ppr stmt
+        GHC.$$ GHC.text (SYB.gshow stmt)
+
+spanNextTo :: RealSrcSpan -> RealSrcSpan -> Bool
+spanNextTo x y
+    = srcSpanStartLine y == srcSpanEndLine x
+    && srcSpanStartCol y == srcSpanEndCol x
diff --git a/src/Overloaded/Plugin/Names.hs b/src/Overloaded/Plugin/Names.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/Names.hs
@@ -0,0 +1,203 @@
+{-# LANGUAGE RecordWildCards #-}
+module Overloaded.Plugin.Names (
+    -- * Names
+    Names (..),
+    getNames,
+    -- * CatNames
+    CatNames (..),
+    getCatNames,
+    -- * VarName
+    VarName (..),
+    lookupVarName,
+    lookupTypeName,
+    -- * Selected modules
+    ghcRecordsCompatMN,
+    ) where
+
+import Control.Monad.IO.Class (MonadIO (..))
+
+import Overloaded.Plugin.Diagnostics
+
+import qualified GHC.Compat.All  as GHC
+import           GHC.Compat.Expr
+
+data Names = Names
+    { fromStringName     :: GHC.Name
+    , fromSymbolName     :: GHC.Name
+    , fromNumeralName    :: GHC.Name
+    , fromNaturalName    :: GHC.Name
+    , fromCharName       :: GHC.Name
+    , nilName            :: GHC.Name
+    , consName           :: GHC.Name
+    , ifteName           :: GHC.Name
+    , unitName           :: GHC.Name
+    , fromLabelName      :: GHC.Name
+    , fromTypeNatName    :: GHC.Name
+    , fromTypeSymbolName :: GHC.Name
+    , fmapName           :: GHC.Name
+    , pureName           :: GHC.Name
+    , apName             :: GHC.Name
+    , birdName           :: GHC.Name
+    , voidName           :: GHC.Name
+    , composeName        :: GHC.Name
+    , doPureName         :: GHC.Name
+    , doThenName         :: GHC.Name
+    , doBindName         :: GHC.Name
+    , conLeftName        :: GHC.Name
+    , conRightName       :: GHC.Name
+    , catNames           :: CatNames
+    }
+
+data CatNames = CatNames
+    { catIdentityName    :: GHC.Name
+    , catComposeName     :: GHC.Name
+    , catTerminalName    :: GHC.Name
+    , catProj1Name       :: GHC.Name
+    , catProj2Name       :: GHC.Name
+    , catFanoutName      :: GHC.Name
+    , catInlName         :: GHC.Name
+    , catInrName         :: GHC.Name
+    , catFaninName       :: GHC.Name
+    , catDistrName       :: GHC.Name
+    , catEvalName        :: GHC.Name
+    }
+
+getNames :: GHC.DynFlags -> GHC.HscEnv -> GHC.TcM Names
+getNames dflags env = do
+    fromStringName  <- lookupName dflags env dataStringMN "fromString"
+    fromSymbolName  <- lookupName dflags env overloadedSymbolsMN "fromSymbol"
+    fromNumeralName <- lookupName dflags env overloadedNumeralsMN "fromNumeral"
+    fromNaturalName <- lookupName dflags env overloadedNaturalsMN "fromNatural"
+    fromCharName    <- lookupName dflags env overloadedCharsMN "fromChar"
+    nilName         <- lookupName dflags env overloadedListsMN "nil"
+    unitName        <- lookupName dflags env overloadedListsMN "nil"
+    consName        <- lookupName dflags env overloadedListsMN "cons"
+    ifteName        <- lookupName dflags env overloadedIfMN "ifte"
+    fromLabelName   <- lookupName dflags env ghcOverloadedLabelsMN "fromLabel"
+
+    fromTypeNatName    <- lookupName' dflags env overloadedTypeNatsMN "FromNat"
+    fromTypeSymbolName <- lookupName' dflags env overloadedTypeSymbolsMN "FromTypeSymbol"
+
+    fmapName <- lookupName dflags env ghcBaseMN "fmap"
+    pureName <- lookupName dflags env ghcBaseMN "pure"
+    apName   <- lookupName dflags env ghcBaseMN "<*>"
+    birdName <- lookupName dflags env ghcBaseMN "<*"
+    voidName <- lookupName dflags env dataFunctorMN "void"
+
+    composeName <- lookupName dflags env ghcBaseMN "."
+
+    doPureName <- lookupName' dflags env overloadedDoMN "Pure"
+    doBindName <- lookupName' dflags env overloadedDoMN "Bind"
+    doThenName <- lookupName' dflags env overloadedDoMN "Then"
+
+    conLeftName  <- lookupNameDataCon dflags env dataEitherMN "Left"
+    conRightName <- lookupNameDataCon dflags env dataEitherMN "Right"
+
+    catNames <- getCatNames dflags env overloadedCategoriesMN
+
+    return Names {..}
+
+getCatNames :: GHC.DynFlags -> GHC.HscEnv -> GHC.ModuleName -> GHC.TcM CatNames
+getCatNames dflags env module_ = do
+    catIdentityName <- lookupName dflags env module_ "identity"
+    catComposeName  <- lookupName dflags env module_ "%%"
+    catProj1Name    <- lookupName dflags env module_ "proj1"
+    catProj2Name    <- lookupName dflags env module_ "proj2"
+    catFanoutName   <- lookupName dflags env module_ "fanout"
+    catInlName      <- lookupName dflags env module_ "inl"
+    catInrName      <- lookupName dflags env module_ "inr"
+    catFaninName    <- lookupName dflags env module_ "fanin"
+    catDistrName    <- lookupName dflags env module_ "distr"
+    catEvalName     <- lookupName dflags env module_ "eval"
+    catTerminalName <- lookupName dflags env module_ "terminal"
+
+    return CatNames {..}
+
+lookupName :: GHC.DynFlags -> GHC.HscEnv -> GHC.ModuleName -> String -> GHC.TcM GHC.Name
+lookupName dflags env mn vn = do
+    res <-  liftIO $ GHC.findImportedModule env mn Nothing
+    case res of
+        GHC.Found _ md -> GHC.lookupOrig md (GHC.mkVarOcc vn)
+        _              -> do
+            putError dflags noSrcSpan $ GHC.text "Cannot find module" GHC.<+> GHC.ppr mn
+            fail "panic!"
+
+lookupNameDataCon :: GHC.DynFlags -> GHC.HscEnv -> GHC.ModuleName -> String -> GHC.TcM GHC.Name
+lookupNameDataCon dflags env mn vn = do
+    res <-  liftIO $ GHC.findImportedModule env mn Nothing
+    case res of
+        GHC.Found _ md -> GHC.lookupOrig md (GHC.mkDataOcc vn)
+        _              -> do
+            putError dflags noSrcSpan $ GHC.text "Cannot find module" GHC.<+> GHC.ppr mn
+            fail "panic!"
+
+lookupName' :: GHC.DynFlags -> GHC.HscEnv -> GHC.ModuleName -> String -> GHC.TcM GHC.Name
+lookupName' dflags env mn vn = do
+    res <-  liftIO $ GHC.findImportedModule env mn Nothing
+    case res of
+        GHC.Found _ md -> GHC.lookupOrig md (GHC.mkTcOcc vn)
+        _              -> do
+            putError dflags noSrcSpan $ GHC.text "Cannot find module" GHC.<+> GHC.ppr mn
+            fail "panic!"
+
+-- | Module name and variable name
+data VarName = VN String String
+  deriving (Eq, Show)
+
+lookupVarName :: GHC.DynFlags -> GHC.HscEnv -> VarName -> GHC.TcM GHC.Name
+lookupVarName dflags env (VN vn mn) = lookupName dflags env (GHC.mkModuleName vn) mn
+
+lookupTypeName :: GHC.DynFlags -> GHC.HscEnv -> VarName -> GHC.TcM GHC.Name
+lookupTypeName dflags env (VN vn mn) = lookupName' dflags env (GHC.mkModuleName vn) mn
+
+-------------------------------------------------------------------------------
+-- ModuleNames
+-------------------------------------------------------------------------------
+
+dataStringMN :: GHC.ModuleName
+dataStringMN =  GHC.mkModuleName "Data.String"
+
+overloadedCharsMN :: GHC.ModuleName
+overloadedCharsMN =  GHC.mkModuleName "Overloaded.Chars"
+
+overloadedSymbolsMN :: GHC.ModuleName
+overloadedSymbolsMN =  GHC.mkModuleName "Overloaded.Symbols"
+
+overloadedNaturalsMN :: GHC.ModuleName
+overloadedNaturalsMN =  GHC.mkModuleName "Overloaded.Naturals"
+
+overloadedNumeralsMN :: GHC.ModuleName
+overloadedNumeralsMN =  GHC.mkModuleName "Overloaded.Numerals"
+
+overloadedListsMN :: GHC.ModuleName
+overloadedListsMN =  GHC.mkModuleName "Overloaded.Lists"
+
+overloadedIfMN :: GHC.ModuleName
+overloadedIfMN =  GHC.mkModuleName "Overloaded.If"
+
+overloadedDoMN :: GHC.ModuleName
+overloadedDoMN =  GHC.mkModuleName "Overloaded.Do"
+
+overloadedCategoriesMN :: GHC.ModuleName
+overloadedCategoriesMN =  GHC.mkModuleName "Overloaded.Categories"
+
+ghcOverloadedLabelsMN :: GHC.ModuleName
+ghcOverloadedLabelsMN =  GHC.mkModuleName "GHC.OverloadedLabels"
+
+overloadedTypeNatsMN :: GHC.ModuleName
+overloadedTypeNatsMN =  GHC.mkModuleName "Overloaded.TypeNats"
+
+overloadedTypeSymbolsMN :: GHC.ModuleName
+overloadedTypeSymbolsMN =  GHC.mkModuleName "Overloaded.TypeSymbols"
+
+ghcRecordsCompatMN :: GHC.ModuleName
+ghcRecordsCompatMN =  GHC.mkModuleName "GHC.Records.Compat"
+
+ghcBaseMN :: GHC.ModuleName
+ghcBaseMN = GHC.mkModuleName "GHC.Base"
+
+dataFunctorMN :: GHC.ModuleName
+dataFunctorMN = GHC.mkModuleName "Data.Functor"
+
+dataEitherMN :: GHC.ModuleName
+dataEitherMN = GHC.mkModuleName "Data.Either"
diff --git a/src/Overloaded/Plugin/Rewrite.hs b/src/Overloaded/Plugin/Rewrite.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/Rewrite.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE DeriveFunctor #-}
+module Overloaded.Plugin.Rewrite where
+
+import Control.Monad (ap)
+
+import qualified GHC.Compat.All  as GHC
+
+-------------------------------------------------------------------------------
+-- Rewrite
+-------------------------------------------------------------------------------
+
+data Rewrite a
+    = NoRewrite
+    | Rewrite a -- TODO: add warnings
+    | Error (GHC.DynFlags -> IO ())
+  deriving (Functor)
+
+instance Semigroup (Rewrite a) where
+    NoRewrite <> x = x
+    x         <> _ = x
+
+instance Applicative Rewrite where
+    pure = Rewrite
+    (<*>) = ap
+
+instance Monad Rewrite where
+    return = Rewrite
+    NoRewrite >>= _ = NoRewrite
+    Rewrite a >>= k = k a
+    Error err >>= _ = Error err
diff --git a/src/Overloaded/Plugin/V.hs b/src/Overloaded/Plugin/V.hs
new file mode 100644
--- /dev/null
+++ b/src/Overloaded/Plugin/V.hs
@@ -0,0 +1,7 @@
+module Overloaded.Plugin.V where
+
+data V2 a = V2 a a
+  deriving (Eq, Show)
+
+data V4 a = V4 a a a a
+  deriving (Eq, Show)
diff --git a/test/AD.hs b/test/AD.hs
new file mode 100644
--- /dev/null
+++ b/test/AD.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE TypeFamilies #-}
+module AD where
+
+import Overloaded.Categories
+
+import qualified Control.Category
+
+-- | A Function which computes value and derivative at the point.
+newtype AD a b = AD (a -> (b, a -> b))
+
+instance Category AD where
+    id = AD (\x -> (x, id))
+
+    AD g . AD f = AD $ \a ->
+        let (b, f') = f a
+            (c, g') = g b
+        in (c, g' . f')
+
+linearD :: (a -> b) -> AD a b
+linearD f = AD $ \x -> (f x, f)
+
+instance CategoryWith1 AD where
+    type Terminal AD = ()
+
+    terminal = AD $ \_ -> ((), \_ -> ())
+
+instance CartesianCategory AD where
+    type Product AD = (,) 
+
+    proj1 = linearD fst
+    proj2 = linearD snd
+
+    fanout (AD f) (AD g) = AD $ \a ->
+        let (b, f') = f a
+            (c, g') = g a
+        in ((b, c), fanout f' g')
+
+-- With this AD we cannot have GeneralizedElement
+
+plus :: Num a => AD (a, a) a
+plus = linearD (uncurry (+))
+
+mult :: Num a => AD (a, a) a
+mult = AD $ \(x,y) -> (x * y, \(dx, dy) -> dx * y + dy * x)
+
+ex1 :: AD Double Double
+ex1 = plus %% fanout identity identity 
+
+ex2 :: AD Double Double
+ex2 = mult %% fanout identity identity
+
+evaluateAD :: Functor f => AD a b -> a -> f a -> (b, f b)
+evaluateAD (AD f) x xs = let (y, f') = f x in (y, fmap f' xs)
diff --git a/test/IxMonad.hs b/test/IxMonad.hs
new file mode 100644
--- /dev/null
+++ b/test/IxMonad.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances  #-}
+module IxMonad where
+
+import Data.Functor.Identity (Identity (..))
+import Data.Kind             (Type)
+import Overloaded.Do
+
+-------------------------------------------------------------------------------
+-- Class
+-------------------------------------------------------------------------------
+
+class IxMonad m where
+    ipure :: a -> m i i a
+    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b
+
+infixl 4 >>>=
+
+-------------------------------------------------------------------------------
+-- Indexed State
+-------------------------------------------------------------------------------
+
+newtype IxStateT m i j a = IxStateT { runIxStateT :: i -> m (a, j) }
+
+instance Monad m => IxMonad (IxStateT m) where
+    ipure x = IxStateT $ \i -> pure (x, i)
+
+    m >>>= k = IxStateT $ \s0 -> do
+        (x, s1) <- runIxStateT m s0
+        runIxStateT (k x) s1
+
+ixmodify :: Applicative m => (i -> j) -> IxStateT m i j ()
+ixmodify f = IxStateT $ \i -> pure ((), f i)
+
+execIxState :: IxStateT Identity i j a -> i -> j
+execIxState m i = snd (runIdentity (runIxStateT m i))
+
+-------------------------------------------------------------------------------
+-- Overloading
+-------------------------------------------------------------------------------
+
+class IxMonad' (method :: DoMethod) (ty :: Type) where
+    ixmonad :: ty
+
+instance (ty ~ (a -> m i i a),                         IxMonad m) => IxMonad' 'Pure ty where ixmonad = ipure
+instance (ty ~ (m i j a -> m j k b -> m i k b),        IxMonad m) => IxMonad' 'Then ty where ixmonad = \x y -> x >>>= \_ -> y
+instance (ty ~ (m i j a -> (a -> m j k b) -> m i k b), IxMonad m) => IxMonad' 'Bind ty where ixmonad = (>>>=)
diff --git a/test/Overloaded/Test/Categories.hs b/test/Overloaded/Test/Categories.hs
new file mode 100644
--- /dev/null
+++ b/test/Overloaded/Test/Categories.hs
@@ -0,0 +1,147 @@
+{-# LANGUAGE Arrows #-}
+{-# LANGUAGE PolyKinds #-}
+{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Categories=Overloaded.Categories.identity #-}
+module Overloaded.Test.Categories where
+
+import Data.Bifunctor.Assoc  (assoc)
+import Test.QuickCheck       ((===))
+import Test.QuickCheck.Poly  (A, B, C)
+import Test.Tasty            (TestTree, testGroup)
+import Test.Tasty.HUnit      (testCase, (@?=))
+import Test.Tasty.QuickCheck (testProperty)
+
+import Overloaded.Categories
+import AD
+import STLC
+
+tests :: TestTree
+tests = testGroup "Categories"
+    [ testGroup "Basic tests"
+        [ testCase "Category" $ do
+            let lhs = proc x -> do
+                    y <- identity -< x
+                    identity -< y
+                rhs = id
+            lhs 'x' @?= rhs 'x'
+
+        , testCase "Product expession" $ do
+            let lhs = proc x -> do
+                    y <- identity -< (x, x)
+                    identity -< (y, x)
+                rhs = \x -> ((x,x),x)
+            lhs 'x' @?= rhs 'x'
+
+        , testCase "Wild pattern" $ do
+            let lhs = proc x -> do
+                  _ <- identity -< x
+                  identity -< x
+                rhs = id
+            lhs 'x' @?= rhs 'x'
+
+        , testCase "Product pattern" $ do
+            let lhs = proc x -> do
+                    (y, _) <- identity -< x
+                    (z, _) <- identity -< y
+                    identity -< z
+                rhs = fst . fst
+                test = (('x', 'y'), 'z')
+            lhs test @?= rhs test
+
+        , testCase "Coproduct expression" $ do
+            let lhs = proc x -> identity -< Left x
+                rhs :: a -> Either a ()
+                rhs = Left
+                test = 'x'
+            lhs test @?= rhs test
+
+        ]
+    , testProperty "assoc (->)" $ \abc ->
+        assoc abc === catAssoc (abc :: ((A, B), C))
+
+    , testCase "assoc Mapping" $ do
+        let M rhs = catAssoc
+            lhs = "Lam (Pair (Fst (Fst (Var Here))) (Pair (Snd (Fst (Var Here))) (Snd (Var Here))))"
+        -- writing Eq instance for Term is not nice :)
+        show rhs @?= lhs
+
+    , testProperty "assocCo (->)" $ \abc ->
+        assoc abc === catAssocCo (abc :: Either (Either A B) C)
+
+    , testCase "assocCo Mapping" $ do
+        let M rhs = catAssocCo
+            lhs = "Lam (Case (Case (InL (Var Here)) (InR (InL (Var Here))) (Var Here)) (InR (InR (Var Here))) (Var Here))"
+        show rhs @?= lhs
+
+    , testCase "uncurry Mapping" $ do
+        let M rhs = catUncurry
+            lhs = "Lam (Lam (App (App (Var (There Here)) (Fst (Var Here))) (Snd (Var Here))))"
+        show rhs @?= lhs
+
+    , testCase "konst Mapping" $ do
+        let M rhs = catKonst (Nat 3) (Nat 7)
+            lhs = "Lam (Pair (Nat 3) (Nat 7))"
+        show rhs @?= lhs
+
+    , testCase "AD" $ do
+        evaluateAD quad (0, 0) [(1,0), (0,1), (1, 1)] @?= (0 :: Int, [0,0,0])
+        evaluateAD quad (1, 2) [(1,0), (0,1), (1, 1)] @?= (5 :: Int, [2,4,6])
+    ]
+
+catAssoc
+    :: CartesianCategory cat
+    => cat (Product cat (Product cat a b) c) (Product cat a (Product cat b c))
+catAssoc = proc ((x, y), z) -> identity -< (x, (y, z))
+
+catSwapCo
+    :: BicartesianCategory cat
+    => cat (Coproduct cat a b) (Coproduct cat b a)
+-- catSwapCo =
+--     fanin (inr %% proj1) (inl %% proj1) %% (distr %% fanout identity identity)
+catSwapCo = proc xy -> case xy of
+    Left x  -> identity -< Right x
+    Right y -> identity -< Left y
+
+catAssocCo
+     :: BicartesianCategory cat
+     => cat (Coproduct cat (Coproduct cat a b) c) (Coproduct cat a (Coproduct cat b c))
+catAssocCo = proc xyz -> case xyz of
+    Left xy     -> case xy of
+        Left x  -> identity -< Left x
+        Right y -> identity -< Right (Left y)
+    Right z     -> identity -< Right (Right z)
+
+catUncurry
+    :: CCC cat
+    => cat (Exponential cat a (Exponential cat b c))
+           (Exponential cat (Product cat a b) c)
+catUncurry = transpose $ proc (f, (a, b)) -> do
+    bc <- f -<< a
+    bc -<< b
+
+catKonst
+    :: (CartesianCategory cat, GeneralizedElement cat)
+    => Object cat a
+    -> Object cat b
+    -> cat c (Product cat a b)
+catKonst a b = proc _ -> do
+    a' <- konst a -< ()
+    b' <- konst b -< ()
+    identity -< (a', b')
+    
+quad :: Num a => AD (a, a) a
+quad = proc (x, y) -> do
+    x2 <- mult -< (x, x)
+    y2 <- mult -< (y, y)
+    plus -< (x2, y2)
+
+-------------------------------------------------------------------------------
+-- Errors
+-------------------------------------------------------------------------------
+
+-- err01 = proc x -> case x of
+--     Left z -> identity -< z
+
+err01 :: BicartesianCategory cat => cat (Coproduct cat a a) a
+err01 = proc z -> case z of
+    Right x -> identity -< x
+    Left y -> identity -< y
diff --git a/test/Overloaded/Test/Do.hs b/test/Overloaded/Test/Do.hs
new file mode 100644
--- /dev/null
+++ b/test/Overloaded/Test/Do.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Do #-}
+module Overloaded.Test.Do where
+
+import Test.Tasty       (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase, (@?=))
+import Data.Functor.Identity (Identity (..))
+
+import Overloaded.Do
+import IxMonad
+
+tests :: TestTree
+tests = testGroup "Do"
+    [ testCase "Maybe" $ do
+        ex1a @?= Just "xy"
+        ex1b @?= Just "xy"
+        ex1c @?= Just "xy"
+        ex1d @?= Just "xy"
+    , testCase "IxState" $ do
+        execIxState ex2a 123 @?= "321"
+        execIxState ex2b 123 @?= "321"
+        execIxState ex2c 123 @?= "321"
+        execIxState ex2d 123 @?= "321"
+    ]
+
+-------------------------------------------------------------------------------
+-- Example 1
+-------------------------------------------------------------------------------
+
+ex1a :: Maybe String
+ex1a = do
+    x <- Just 'x'
+    y <- Just 'y'
+    pure [x, y]
+
+ex1b :: Maybe String
+ex1b =
+    Just 'x' >>= \x ->
+    Just 'y' >>= \y ->
+    pure [x, y]
+
+ex1c :: Maybe String
+ex1c =
+    monad @Bind (Just 'x') $ \x ->
+    monad @Bind (Just 'y') $ \y ->
+    monad @Pure [x, y]
+
+ex1d :: Maybe String
+ex1d = monad.do
+    x <- Just 'x'
+    y <- Just 'y'
+    monad @Pure [x, y]
+
+-------------------------------------------------------------------------------
+-- Example 2
+-------------------------------------------------------------------------------
+
+ex2a :: IxStateT Identity Int String ()
+ex2a =
+    ixmodify show >>>= \_ ->
+    ixmodify reverse
+
+ex2b :: IxStateT Identity Int String ()
+ex2b =
+    ixmonad @Then (ixmodify show) $
+    ixmodify reverse
+    
+ex2c :: IxStateT Identity Int String ()
+ex2c = ixmonad.do
+    ixmodify show
+    ixmodify reverse
+    
+ex2d :: IxStateT Identity Int String ()
+ex2d = ixmonad.do
+    _unused <- ixmodify show
+    ixmodify reverse
diff --git a/test/Overloaded/Test/Labels/GenericLens.hs b/test/Overloaded/Test/Labels/GenericLens.hs
--- a/test/Overloaded/Test/Labels/GenericLens.hs
+++ b/test/Overloaded/Test/Labels/GenericLens.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE DeriveGeneric    #-}
 {-# LANGUAGE OverloadedLabels #-}
-{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Labels=Data.Generics.Product.Fields.field #-}
+{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Labels=Data.Generics.Lens.Lite.field #-}
 module Overloaded.Test.Labels.GenericLens where
 
 import Control.Lens     (over, view)
diff --git a/test/Overloaded/Test/Lists.hs b/test/Overloaded/Test/Lists.hs
--- a/test/Overloaded/Test/Lists.hs
+++ b/test/Overloaded/Test/Lists.hs
@@ -6,6 +6,7 @@
 {-# OPTIONS_GHC -Wno-missing-signatures #-}
 {-# OPTIONS -fplugin=Overloaded
             -fplugin-opt=Overloaded:Lists
+            -Wno-type-defaults
   #-}
 module Overloaded.Test.Lists where
 
diff --git a/test/Overloaded/Test/Lists/Bidi.hs b/test/Overloaded/Test/Lists/Bidi.hs
--- a/test/Overloaded/Test/Lists/Bidi.hs
+++ b/test/Overloaded/Test/Lists/Bidi.hs
@@ -7,14 +7,12 @@
   #-}
 module Overloaded.Test.Lists.Bidi where
 
-import Data.List.NonEmpty     (NonEmpty (..))
 import Data.SOP.BasicFunctors (I (..))
 import Data.SOP.NP            (NP (..), POP (..))
 import Data.Vec.Lazy          (Vec (..))
 import Test.Tasty             (TestTree, testGroup)
 import Test.Tasty.HUnit       (testCase, (@?=))
 
-import qualified Data.Map      as Map
 import qualified Data.Set      as Set
 import qualified Data.Type.Nat as N
 
diff --git a/test/Overloaded/Test/Numerals.hs b/test/Overloaded/Test/Numerals.hs
--- a/test/Overloaded/Test/Numerals.hs
+++ b/test/Overloaded/Test/Numerals.hs
@@ -9,7 +9,6 @@
 
 import qualified Data.Bin      as B
 import qualified Data.BinP     as BP
-import qualified Data.Type.Bin as B
 import qualified Data.Type.Nat as N
 
 tests :: TestTree
diff --git a/test/Overloaded/Test/Strings.hs b/test/Overloaded/Test/Strings.hs
--- a/test/Overloaded/Test/Strings.hs
+++ b/test/Overloaded/Test/Strings.hs
@@ -4,7 +4,7 @@
 import Test.Tasty       (TestTree, testGroup)
 import Test.Tasty.HUnit (testCase, (@?=))
 
-import Data.Text (Text, pack)
+import Data.Text (pack)
 
 tests :: TestTree
 tests = testGroup "Strings"
diff --git a/test/STLC.hs b/test/STLC.hs
new file mode 100644
--- /dev/null
+++ b/test/STLC.hs
@@ -0,0 +1,288 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeOperators       #-}
+module STLC where
+
+import Data.Kind             (Type)
+import Data.Proxy            (Proxy (..))
+import Overloaded.Categories
+import Numeric.Natural (Natural)
+
+import qualified Control.Category
+
+data Ty
+    = TyUnit
+    | TyPair Ty Ty
+    | TyFun Ty Ty
+    | TyCoproduct Ty Ty
+    | TyNat
+  deriving (Show)
+
+data Elem :: [Ty] -> Ty -> Type where
+    Here  :: Elem (x ': xs) x
+    There :: Elem xs x -> Elem (y ': xs) x
+
+deriving instance Show (Elem xs x)
+
+data Term :: [Ty] -> Ty -> Type where
+    Var :: Elem ctx ty -> Term ctx ty
+
+    Lam :: Term (a ': ctx) b -> Term ctx ('TyFun a b)
+    App :: Term ctx ('TyFun a b) -> Term ctx a -> Term ctx b
+
+    Unit :: Term ctx 'TyUnit
+
+    Fst :: Term ctx ('TyPair a b) -> Term ctx a
+    Snd :: Term ctx ('TyPair a b) -> Term ctx b
+    Pair :: Term ctx a -> Term ctx b -> Term ctx ('TyPair a b)
+
+    InL :: Term ctx a -> Term ctx ('TyCoproduct a b)
+    InR :: Term ctx b -> Term ctx ('TyCoproduct a b)
+    Case :: Term (a ': ctx) c -> Term (b ':  ctx) c -> Term ctx ('TyCoproduct a b) -> Term ctx c
+
+    Nat :: Natural -> Term ctx 'TyNat
+
+deriving instance Show (Term xs x)
+
+-------------------------------------------------------------------------------
+-- Variables
+-------------------------------------------------------------------------------
+
+var0 :: Term (a ': ctx) a
+var0 = Var Here
+
+var1 :: Term (b ': a ': ctx) a
+var1 = Var (There Here)
+
+-------------------------------------------------------------------------------
+-- Weakening
+-------------------------------------------------------------------------------
+
+weakenTerm :: Term ctx b -> Term (a ': ctx) b
+weakenTerm = weakenTerm' SNil Proxy Proxy
+
+weakenTerm1 :: Term (b ': ctx) c -> Term (b ': a ': ctx) c
+weakenTerm1 = weakenTerm' (SCons SNil) Proxy Proxy
+
+weakenTerm2 :: Term ctx b -> Term (a ': a' ': ctx) b
+weakenTerm2 = weakenTerm . weakenTerm
+
+weakenTerm' :: SList pfx -> Proxy sfx -> Proxy a
+            -> Term (Append pfx sfx) b -> Term (Append pfx (a ': sfx)) b
+weakenTerm' pfx sfx a (Var el)     = Var (weakenElem pfx sfx a el)
+weakenTerm' pfx sfx a (Lam t)      = Lam (weakenTerm' (SCons pfx) sfx a t)
+weakenTerm' pfx sfx a (App u v)    = App (weakenTerm' pfx sfx a u) (weakenTerm' pfx sfx a v)
+weakenTerm' pfx sfx a (Fst t)      = Fst (weakenTerm' pfx sfx a t)
+weakenTerm' pfx sfx a (Snd t)      = Snd (weakenTerm' pfx sfx a t)
+weakenTerm' pfx sfx a (Pair u v)   = Pair (weakenTerm' pfx sfx a u) (weakenTerm' pfx sfx a v)
+weakenTerm' pfx sfx a (InL t)      = InL (weakenTerm' pfx sfx a t)
+weakenTerm' pfx sfx a (InR t)      = InR (weakenTerm' pfx sfx a t)
+weakenTerm' pfx sfx a (Case u v w) = Case
+    (weakenTerm' (SCons pfx) sfx a u)
+    (weakenTerm' (SCons pfx) sfx a v)
+    (weakenTerm' pfx         sfx a w)
+weakenTerm' _   _   _ Unit         = Unit
+weakenTerm' _   _   _ (Nat n)      = Nat n
+
+weakenElem
+    :: SList pfx
+    -> Proxy sfx
+    -> Proxy a
+    -> Elem (Append pfx sfx) b
+    -> Elem (Append pfx (a : sfx)) b
+weakenElem SNil         _sfx _a el         = There el
+weakenElem (SCons  pfx)  sfx  a (There el) = There (weakenElem pfx sfx a el)
+weakenElem (SCons _pfx) _sfx _a Here       = Here
+
+-------------------------------------------------------------------------------
+-- Append...
+-------------------------------------------------------------------------------
+
+type family Append (xs :: [k]) (ys :: [k]) :: [k] where
+    Append '[]       ys = ys
+    Append (x ': xs) ys = x ': Append xs ys
+
+data SList (xs :: [k]) where
+    SNil  :: SList '[]
+    SCons :: SList xs -> SList (x ': xs)
+
+-------------------------------------------------------------------------------
+-- Smart constructors
+-------------------------------------------------------------------------------
+
+app :: Term ctx ('TyFun a b) -> Term ctx a -> Term ctx b
+app (Lam b) x = subst SNil Proxy b x
+app f       x = App f x
+
+tfst :: Term ctx ('TyPair a b) -> Term ctx a
+tfst (Pair x _) = x
+tfst p          = Fst p
+
+tsnd :: Term ctx ('TyPair a b) -> Term ctx b
+tsnd (Pair _ y) = y
+tsnd p          = Snd p
+
+tcase :: Term (a ': ctx) c -> Term (b ':  ctx) c -> Term ctx ('TyCoproduct a b) -> Term ctx c
+tcase l _ (InL x) = subst SNil Proxy l x
+tcase _ r (InR x) = subst SNil Proxy r x
+
+-- case-of-case
+tcase l r (Case l' r' p) = tcase
+    (tcase (weakenTerm1 l) (weakenTerm1 r) l')
+    (tcase (weakenTerm1 l) (weakenTerm1 r) r')
+    p
+
+tcase l r p       = Case l r p
+
+-------------------------------------------------------------------------------
+-- Substitution
+-------------------------------------------------------------------------------
+
+subst
+    :: SList pfx -> Proxy sfx
+    -> Term (Append pfx (a ': sfx)) b -> Term sfx a -> Term (Append pfx sfx) b
+subst pfx sfx (Var el)     t = substElem pfx sfx el t
+subst pfx sfx (Lam x)      t = Lam (subst (SCons pfx) sfx x t)
+subst pfx sfx (Fst x)      t = tfst (subst pfx sfx x t)
+subst pfx sfx (Snd x)      t = tsnd (subst pfx sfx x t)
+subst pfx sfx (InL x)      t = InL (subst pfx sfx x t)
+subst pfx sfx (InR x)      t = InR (subst pfx sfx x t)
+subst pfx sfx (App u v)    t = app (subst pfx sfx u t) (subst pfx sfx v t)
+subst pfx sfx (Pair u v)   t = Pair (subst pfx sfx u t) (subst pfx sfx v t)
+subst pfx sfx (Case u v w) t = tcase
+    (subst (SCons pfx) sfx u t)
+    (subst (SCons pfx) sfx v t)
+    (subst pfx         sfx w t)
+subst _   _   (Nat n)      _ = Nat n
+subst _   _   Unit         _ = Unit
+
+substElem
+    :: SList pfx -> Proxy sfx
+    -> Elem (Append pfx (a : sfx)) b
+    -> Term sfx a
+    -> Term (Append pfx sfx) b
+substElem SNil         _sfx Here       t = t
+substElem SNil         _sfx (There el) _ = Var el
+substElem (SCons _pfx) _sfx Here       _ = Var Here
+substElem (SCons  pfx)  sfx (There el) t = weakenTerm (substElem pfx sfx el t)
+
+
+-------------------------------------------------------------------------------
+-- Mapping closed terms of type (a -> b)
+-------------------------------------------------------------------------------
+
+newtype Mapping (ctx :: [Ty]) (a :: Ty) (b :: Ty) = M (Term ctx ('TyFun a b))
+  deriving (Show)
+
+unMapping :: Mapping ctx a b -> Term ctx ('TyFun a b)
+unMapping (M t) = t
+
+-------------------------------------------------------------------------------
+-- Category: Mapping
+-------------------------------------------------------------------------------
+
+instance Category (Mapping ctx) where
+    id        = M $ Lam var0
+    M f . M g = M $ Lam $ app (weakenTerm f) (app (weakenTerm g) (Var Here))
+
+-------------------------------------------------------------------------------
+-- Product: Mapping
+-------------------------------------------------------------------------------
+
+instance CategoryWith1 (Mapping ctx) where
+    type Terminal (Mapping ctx) = 'TyUnit
+
+    terminal = M $ Lam $ Unit
+
+instance CartesianCategory (Mapping ctx) where
+    type Product (Mapping ctx) = 'TyPair
+
+    proj1 = M $ Lam $ Fst var0
+    proj2 = M $ Lam $ Snd var0
+    fanout (M f) (M g) = M $ Lam $ Pair
+        (app (weakenTerm f) (Var Here))
+        (app (weakenTerm g) (Var Here))
+
+-- | Thanks to 'app' this simplifies!
+--
+-- >>> ex01mapping
+-- M (Lam (Fst (Fst (Var Here))))
+ex01 :: CartesianCategory cat => cat (Product cat (Product cat a b) c) a
+ex01 = proj1 %% proj1
+
+ex01mapping :: Mapping ctx ('TyPair ('TyPair a b) c) a
+ex01mapping = ex01
+
+-- |
+--
+-- >>> ex0mapping
+-- M (Lam (Var Here))
+ex02 :: CartesianCategory cat => cat a a
+ex02 = proj1 %% fanout identity identity
+
+ex02mapping :: Mapping ctx a a
+ex02mapping = ex02
+
+-------------------------------------------------------------------------------
+-- Coproduct: Mapping
+-------------------------------------------------------------------------------
+
+instance CocartesianCategory (Mapping ctx) where
+    type Coproduct (Mapping ctx) = 'TyCoproduct
+
+    inl = M $ Lam $ InL var0
+    inr = M $ Lam $ InR var0
+    fanin (M f) (M g) = M $ Lam $ tcase
+        (app (weakenTerm2 f) var0)
+        (app (weakenTerm2 g) var0)
+        var0
+
+instance BicartesianCategory (Mapping ctx) where
+    distr = M $ Lam $ tcase
+        (InL (Pair var0 (Snd var1)))
+        (InR (Pair var0 (Snd var1)))
+        (Fst var0)
+
+-- |
+--
+-- >>> ex03mapping
+-- M (Lam (Var Here))
+ex03 :: CocartesianCategory cat => cat a a
+ex03 = fanin identity identity %% inl
+
+ex03mapping :: Mapping ctx a a
+ex03mapping = ex03
+
+-------------------------------------------------------------------------------
+-- Exponent: Mapping
+-------------------------------------------------------------------------------
+
+instance CCC (Mapping ctx) where
+    type Exponential (Mapping ctx) = 'TyFun
+
+    eval = M $ Lam $ app (Fst var0) (Snd var0)
+
+    transpose (M f) = M $ Lam $ Lam $ app (weakenTerm2 f) (Pair var1 var0)
+
+-- |
+--
+-- >>> ex04mapping
+-- M (Lam (Pair (Var Here) (Var Here)))
+ex04 :: CCC cat => cat a (Product cat a a)
+ex04 = eval %% fanout (transpose identity) identity
+
+ex04mapping :: Mapping ctx a ('TyPair a a)
+ex04mapping = ex04
+
+-------------------------------------------------------------------------------
+-- Generalized Element: Mapping
+-------------------------------------------------------------------------------
+
+instance GeneralizedElement (Mapping ctx) where
+    type Object (Mapping ctx) ty = Term ctx ty
+
+    konst t = M $ Lam $ weakenTerm t
diff --git a/test/Tests.hs b/test/Tests.hs
--- a/test/Tests.hs
+++ b/test/Tests.hs
@@ -2,7 +2,9 @@
 
 import Test.Tasty (defaultMain, testGroup)
 
+import qualified Overloaded.Test.Categories as Cat
 import qualified Overloaded.Test.Chars      as Chr
+import qualified Overloaded.Test.Do         as Doo
 import qualified Overloaded.Test.If         as Iff
 import qualified Overloaded.Test.Labels     as Lbl
 import qualified Overloaded.Test.Lists      as Lst
@@ -18,6 +20,7 @@
 main = defaultMain $ testGroup "Tests"
     [ Chr.tests
     , Iff.tests
+    , Doo.tests
     , Lbl.tests
     , Lst.tests
     , Lst.Bidi.tests
@@ -26,4 +29,5 @@
     , Str.tests
     , Sym.tests
     , GL.tests
+    , Cat.tests
     ]