diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+0.1.0.0
+---
+First version. Not released yet
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2022 Lev Dvorkin
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,49 @@
+bidirectional-instances
+===
+
+This is a haskell package to provide wrapper class and useful template haskell
+instance-generator functions for bidirectional instances, i. e. for instance
+```hs
+instance (A a, B b) => C (Foo a b)
+```
+deduce not only `forall a b. (A a, B b) => C (Foo a b)`, but also
+`forall a b. C (Foo a b) => A a` and `forall a b. C (Foo a b) => B b`.
+This behavior doesn't implemented in modern GHC version, but its very intuitive
+(and, of course, sound) if there are no overlapping instances for `C (Foo a b)`.
+
+There was a [paper](https://arxiv.org/pdf/1906.12242.pdf), related to this 
+feature and an attempt to 
+[implement it as GHC extension](https://github.com/KoenP/ghc-proposals/blob/patch-1/proposals/0000-bidirectional-instances.md).
+In the discussion about alternatives for that extension this solution 
+[was mentioned](https://github.com/KoenP/ghc-proposals/blob/patch-1/proposals/0000-bidirectional-instances.md#using-constraint-kinds),
+but was discarded as "decidedly nontrivial, and some boilerplate is still 
+required, which needs to be written for every instance".
+To reduce these downsides, instances from this package are made more general
+and template haskell function for generating boilerplate code are provided.
+I suppose that implementation this as an compiler extension probably would be 
+better for performance, but I don't have enough qualification to implement it.
+
+Documentation
+---
+Detailed documentation with examples can be found in the main module 
+*(Control.Bidirectional)*.
+
+Usage
+---
+All function and classes you need to work with are exported from 
+`Control.Bidirectional`.
+
+To be implemented somewhere in the future
+---
+I'll try to make a GHC plugin to improve this solution in two directions:
+- no need for template haskell
+- more intuitive syntax
+
+More precisely, I'd like to have the following syntax for declaring 
+bidirectional instances:
+```hs
+instance {-# BIDIRECTIONAL #-} (A a, B b) => C (Foo a b)
+```
+and `-XBidirectionalInstances` to make all instances without 
+`OVERLAPS`/`OVERLAPPING`/`OVERLAPPABLE` bidirectional by default.
+
diff --git a/bidirectional-instances.cabal b/bidirectional-instances.cabal
new file mode 100644
--- /dev/null
+++ b/bidirectional-instances.cabal
@@ -0,0 +1,54 @@
+cabal-version:      3.0
+name:               bidirectional-instances
+version:            0.1.0.0
+synopsis:           Make instance constraints bidirectional
+description:        This package contains class for bidirectional instances 
+                    and TH methods for generating instances for it.
+                    See /README.md/ for more information
+homepage:           https://github.com/Lev135/bidirectional-instances
+bug-reports:        https://github.com/Lev135/bidirectional-instances/issues
+
+license:            MIT
+license-file:       LICENSE
+author:             Lev135
+maintainer:         lev_135@mail.ru
+copyright:          Lev Dvorkin (c) 2022
+category:           language
+
+extra-source-files: CHANGELOG.md
+extra-doc-files:    README.md
+
+source-repository head
+    type:           git
+    location:       https://github.com/Lev135/bidirectional-instances.git
+
+
+library
+    exposed-modules:  Control.Bidirectional
+                      Control.Bidirectional.Class
+                      Control.Bidirectional.TH
+
+    build-depends:    base ^>=4.14.3.0
+                    , template-haskell
+    hs-source-dirs:   src
+    default-language: Haskell2010
+
+test-suite examples
+    type:             exitcode-stdio-1.0
+    main-is:          Main.hs
+
+    other-modules:    Example1
+                      Example2
+                      Example1Alternative
+                      Example2Alternative
+                      Example1TH
+                      Example2TH
+                      Example1PreludeTH
+                      Overlap
+
+    build-depends:    base ^>=4.14.3.0
+                    , mtl
+                    , transformers
+                    , bidirectional-instances
+    hs-source-dirs:   examples
+    default-language: Haskell2010
diff --git a/examples/Example1.hs b/examples/Example1.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example1.hs
@@ -0,0 +1,44 @@
+{-
+  This module contains solution for example from "Bidirectional type instances"
+  by Koen Pauwels, Georgios Karachalias, Michiel Derhaeg and Tom Schrijvers
+  (https://arxiv.org/pdf/1906.12242.pdf)
+-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Example1 where
+
+import Data.Kind (Constraint, Type)
+
+data Term :: Type -> Type where
+  Con :: a -> Term a
+  Tup :: Term b -> Term c -> Term (b, c)
+
+{-
+-- Fails to type check:
+instance Show a => Show (Term a) where
+  show (Con x) = show x
+  show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+-}
+
+{-
+  Some kind of solution using modern haskell without new extensions
+-}
+
+-- somewhere in Prelude'
+class ShowC a => Show' a where
+  type ShowC a :: Constraint
+  show' :: a -> String
+
+-- also in Prelude'
+instance (Show' b, Show' c) => Show' (b, c) where
+  type ShowC (b, c) = (Show' b, Show' c)
+  show' (x, y) = unwords ["(", show' x, ",", show' y, ")"]
+
+-- then the following typechecks
+instance Show' a => Show' (Term a) where
+  type ShowC (Term a) = Show' a
+  show' (Con x) = show' x
+  show' (Tup x y) = unwords ["(", show' x, ",", show' y, ")"]
diff --git a/examples/Example1Alternative.hs b/examples/Example1Alternative.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example1Alternative.hs
@@ -0,0 +1,49 @@
+{-
+  This module contains solution for example from "Bidirectional type instances"
+  by Koen Pauwels, Georgios Karachalias, Michiel Derhaeg and Tom Schrijvers
+  (https://arxiv.org/pdf/1906.12242.pdf), alternative to provided in
+  [Example1](./Example1.hs). It's useful if in we have no access to the class
+  definition, but want to use bidirectional constraint
+-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Example1Alternative where
+
+import Data.Kind (Constraint, Type)
+
+data Term :: Type -> Type where
+  Con :: a -> Term a
+  Tup :: Term b -> Term c -> Term (b, c)
+
+{-
+-- Fails to type check:
+instance Show a => Show (Term a) where
+  show (Con x) = show x
+  show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+-}
+
+{-
+  Some kind of solution using modern haskell without new extensions
+-}
+
+-- somewhere in 'bidirectional' package
+class (c a, Constr c a) => Bidirectional (c :: k -> Constraint) (a :: k) where
+  type Constr c a :: Constraint
+
+-- provide instances for which we want bidirectional constraints
+instance Constr Show (b, c) => Bidirectional Show (b, c) where
+  type Constr Show (b, c) = (Bidirectional Show b, Bidirectional Show c)
+
+-- then the following typechecks
+instance Bidirectional Show a => Show (Term a) where
+  show (Con x) = show x
+  show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+
+-- of course we can also provide Bidirectional Show instance for Term, but it 
+-- isn't  necessary, unless we want to have bidirectional constraint for it
diff --git a/examples/Example1PreludeTH.hs b/examples/Example1PreludeTH.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example1PreludeTH.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Example1PreludeTH where
+
+import Control.Bidirectional (decBidirectionalInstances, BidirectionalRec)
+import Data.Kind (Type)
+
+data Term :: Type -> Type where
+  Con :: a -> Term a
+  Tup :: Term b -> Term c -> Term (b, c)
+
+class Show' a where
+  show' :: a -> String
+
+decBidirectionalInstances [d|
+    instance (Show' a, Show' b) => Show' (a, b) where
+      show' (x, y) = unwords ["(", show' x, ",", show' y, ")"]
+  |]
+
+instance BidirectionalRec Show' a => Show' (Term a) where
+  show' (Con x) = show' x
+  show' (Tup x y) = unwords ["(", show' x, ",", show' y, ")"]
diff --git a/examples/Example1TH.hs b/examples/Example1TH.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example1TH.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-
+  This module contains solution for example from "Bidirectional type instances"
+  by Koen Pauwels, Georgios Karachalias, Michiel Derhaeg and Tom Schrijvers
+  (https://arxiv.org/pdf/1906.12242.pdf), using this package
+-}
+
+module Example1TH where
+
+import Data.Kind (Constraint, Type)
+import Control.Bidirectional ( Bidirectional, makeBidirectionalInstances, BidirectionalRec ) 
+
+data Term :: Type -> Type where
+  Con :: a -> Term a
+  Tup :: Term b -> Term c -> Term (b, c)
+
+{-
+-- Fails to type check:
+instance Show a => Show (Term a) where
+  show (Con x) = show x
+  show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+-}
+
+{-
+  Some kind of solution using modern haskell without new extensions
+-}
+
+-- provide instances for which we want bidirectional constraints
+makeBidirectionalInstances [d|
+    instance (Show b, Show c)  => Show (b, c)
+  |]
+
+-- then the following typechecks
+instance BidirectionalRec Show a => Show (Term a) where
+  show (Con x) = show x
+  show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+
+-- of course we can also provide Bidirectional Show instance for Term, but it 
+-- isn't  necessary, unless we want to have bidirectional constraint for it
diff --git a/examples/Example2.hs b/examples/Example2.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example2.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module Example2 where
+import Control.Monad.State (MonadState, StateT)
+import Control.Monad.Except (ExceptT)
+import Data.Kind (Constraint)
+
+
+class (forall s e m e'. MonadState s (ExceptT e m) => 
+  MonadState s (ExceptT e' m)) => W
+
+{-
+-- this instance isn't typechecked
+instance W
+-}
+
+class (MonadState s m, MonadStateC s m) => MonadState' s m where
+  type MonadStateC s m :: Constraint
+
+instance Monad m => MonadState' s (StateT s m) where
+  type MonadStateC s (StateT s m) = Monad m
+
+instance MonadState' s m => MonadState' s (ExceptT e m) where
+  type MonadStateC s (ExceptT e m) = MonadState' s m
+
+class (forall s e m e'. MonadState' s (ExceptT e m) => 
+  MonadState' s (ExceptT e' m)) => W'
+
+-- but this instance is correct
+instance W'
diff --git a/examples/Example2Alternative.hs b/examples/Example2Alternative.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example2Alternative.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+
+module Example2Alternative where
+import Control.Monad.State (MonadState, StateT)
+import Control.Monad.Except (ExceptT)
+import Data.Kind (Constraint)
+
+
+class (forall s e m e'. MonadState s (ExceptT e m) => 
+  MonadState s (ExceptT e' m)) => W
+
+{-
+-- this instance isn't typechecked
+instance W
+-}
+
+-- somewhere in 'bidirectional' package
+class (c a, Constr c a) => Bidirectional (c :: k -> Constraint) (a :: k) where
+  type Constr c a :: Constraint
+
+instance Constr (MonadState s) (StateT s m) => Bidirectional (MonadState s) (StateT s m) where
+  type Constr (MonadState s) (StateT s m) = Monad m
+
+instance Constr (MonadState s) (ExceptT s m) => Bidirectional (MonadState s) (ExceptT e m) where
+  type Constr (MonadState s) (ExceptT e m) = Bidirectional (MonadState s) m
+
+class (forall s e m e'. Bidirectional (MonadState s) (ExceptT e m) => 
+  Bidirectional (MonadState s) (ExceptT e' m)) => W'
+
+-- but this instance is correct
+instance W'
diff --git a/examples/Example2TH.hs b/examples/Example2TH.hs
new file mode 100644
--- /dev/null
+++ b/examples/Example2TH.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Example2TH where
+
+import Control.Monad.State (MonadState, StateT)
+import Control.Monad.Except (ExceptT)
+import Data.Kind (Constraint)
+import Control.Bidirectional (makeBidirectionalInstances, Bidirectional)
+
+
+class (forall s e m e'. MonadState s (ExceptT e m) => 
+  MonadState s (ExceptT e' m)) => W
+
+{-
+-- this instance isn't typechecked
+instance W
+-}
+
+makeBidirectionalInstances [d|
+    instance Monad m => MonadState s (StateT s m)
+    instance MonadState s m => MonadState s (ExceptT e m)
+  |]
+
+class (forall s e m e'. Bidirectional (MonadState s) (ExceptT e m) => 
+  Bidirectional (MonadState s) (ExceptT e' m)) => W'
+
+-- but this instance is correct
+instance W'
+
diff --git a/examples/Main.hs b/examples/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/Main.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+module Main where
+
+import Control.Bidirectional
+
+-- makeBidirectionalInstance ''Show [t| (a, b) |] [t| (Show a, Show b) |]
+
+makeBidirectionalInstances [d| 
+    instance (Show a, Show b) => Show (a, b)
+  |]
+
+main :: IO ()
+main = putStrLn "Hello, Haskell!"
diff --git a/examples/Overlap.hs b/examples/Overlap.hs
new file mode 100644
--- /dev/null
+++ b/examples/Overlap.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module Overlap where
+
+import Control.Bidirectional (decBidirectionalInstances)
+
+data A a = A a
+
+decBidirectionalInstances [d| 
+    instance Show a => Show (A a) where
+      show (A a) = "A " ++ show a
+  |]
+
+instance {-# OVERLAPS #-} Show (A Int) where
+  show (A a) = "Integral A: " ++ show (toInteger a)
diff --git a/src/Control/Bidirectional.hs b/src/Control/Bidirectional.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Bidirectional.hs
@@ -0,0 +1,111 @@
+{- | 
+  Module:        Control.Bidirectional
+  Description:   All you need to use bidirectional instances
+  Copyright:     Lev Dvorkin (c) 2022
+  License:       MIT
+  Maintainer:    lev_135@mail.ru
+  Stability:     experimental
+
+  This module provides class wrapper for instances that should be bidirectional,
+  i. e. lets GHC know that from instance
+
+  > instance (A a, B b) => C (Foo a b)
+
+  not only @forall a b. (A a, B b) => C (Foo a b)@, but also
+  @forall a b. C (Foo a b) => A a@ and @forall a b. C (Foo a b) => B b@
+  can be deduced. This is correct, provided that there are no overlapping 
+  instances for @C (Foo a b)@.
+
+  === __Example 1: showing @GADT@__
+  Suppose we want to write @Show@ instance for the following GADT type:
+
+  > data Term :: Type -> Type where
+  >   Con :: a -> Term a
+  >   Tup :: Term b -> Term c -> Term (b, c)
+
+  It's a bit tricky, because an obvious declaration
+
+  > instance Show a => Show (Term a) where
+  >   show (Con x) = show x
+  >   show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+
+  fails to typecheck, because in the second equation we apply @show@ function
+  to @x@, so we need @Show@ instance for @b@ (from GADT constructor).
+  But we only have @Show a@ where @a ~ (b, c)@. So we need to deduce
+  @Show (b, c) => Show b@ and GHC fails to do this. This package provides 
+  a solution for this problem:
+
+  First of all, we need to make instance @Show (b, c)@ bidirectional.
+  Maybe sometime in the future it will be declared in @Prelude@, but now we
+  need to make it manually. TH functions from this module can help to reduce
+  boilerplate:
+
+  > makeBidirectionalInstances [d|
+  >     instance (Show b, Show c)  => Show (b, c)
+  >   |]
+
+  After bidirectional instance has been declared, we can use our previous
+  @Show (Term a)@ declaration with a small change: changing constraint
+  from @Show a@ to @BidirectionalRec Show a@.
+
+  > instance BidirectionalRec Show a => Show (Term a) where
+  >   show (Con x) = show x
+  >   show (Tup x y) = unwords ["(", show x, ",", show y, ")"]
+
+  Why we need 'BidirectionalRec' constraint, but not simple 'Bidirectional'?
+  It's so because we may have nested tuples: @(Tup (Tup x y) z)@ and for showing
+  @(Tup x y)@ we also need bidirectional @Show@ instance. So GHC must infer
+  @BidirectionalRec Show (b, c) => BidirectionalRec Show b@ and
+  @Bidirectional Show (b, c) => Show b@ is not enough.
+
+  === __Example 2: mapping error type for @ErrorT@ preserving MonadState constraint__
+  Suppose we want to change @e@ type for @ExceptT@ transformer preserving 
+  knowledge of @MonadState s@ instance for composed monad. So we want to infer
+  @MonadState s (ExceptT e m) => MonadState s (ExceptT e' m)@.
+  Using bidirectional instances it can be done this way:
+  
+  > Bidirectional (MonadState s) (ExceptT e m) 
+  >   => MonadState s ExceptT e m 
+  >   => Bidirectional (MonadSTate s) EXceptT e m
+
+  Thus, the following is well-typed:
+
+  > makeBidirectionalInstances [d|
+  >   instance Monad m => MonadState s (StateT s m)
+  >   instance MonadState s m => MonadState s (ExceptT e m)
+  > |]
+  > 
+  > class (forall s e m e'. Bidirectional (MonadState s) (ExceptT e m) => 
+  >   Bidirectional (MonadState s) (ExceptT e' m)) => W'
+  > instance W'
+
+  == Interaction with overlapping instances
+  
+  As was mentioned above backward implication is sound only when we have 
+  no overlapping instances for.
+  However, solution from this package /can/ work with overlapping instances,
+  provided that only one of them is selected to use in backward direction.
+  Selected instance should be passed to 
+  `makeBidirectionalInstances`/`decBidirectionalInstances`.
+
+  For example this code is correct:
+
+  > data A a = A a
+  > 
+  > decBidirectionalInstances [d| 
+  >     instance Show a => Show (A a) where
+  >       show (A a) = "A " ++ show a
+  >   |]
+  > 
+  > instance {-# OVERLAPS #-} Show (A Int) where
+  >   show (A a) = "Integral A: " ++ show (toInteger a)
+-}
+module Control.Bidirectional (
+  Bidirectional (..),
+  BidirectionalRec (..),
+  decBidirectionalInstances,
+  makeBidirectionalInstances
+) where
+
+import Control.Bidirectional.Class (Bidirectional(..), BidirectionalRec(..))
+import Control.Bidirectional.TH (makeBidirectionalInstances, decBidirectionalInstances)
diff --git a/src/Control/Bidirectional/Class.hs b/src/Control/Bidirectional/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Bidirectional/Class.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+{- | 
+  Module:        Control.Bidirectional.Class
+  Description:   Base types for bidirectional instances
+  Copyright:     Lev Dvorkin (c) 2022
+  License:       MIT
+  Maintainer:    lev_135@mail.ru
+  Stability:     experimental
+-}
+module Control.Bidirectional.Class (
+    Bidirectional (..), 
+    BidirectionalRec (..)
+  ) where
+
+import Data.Kind (Constraint)
+
+{-| 
+  Class for non-recursive bidirectional instances, i. e. for instances,
+  such that their components constraints ('Constr') is ordinary instance.
+ 
+  Arguments:
+    
+  - @c@ class for which we declare bidirectional instance
+  - @a@ data type for which instance is provided
+
+  For example:
+
+  > instance Show a => Bidirectional Show [a] where
+  >   type ConstrRec Show [a] = Show a
+ 
+  is correct 'Bidirectional' instance. If you want to have bidirectional
+  'Show' instance in backward constraint, use 'BidirectionalRec'
+  
+  Instances for this class are supposed to be generated by 
+  'Control.Bidirectional.makeBidirectionalInstances` or by
+  'Control.Bidirectional.decBidirectionalInstances`.
+-}
+class (c a, Constr c a) => Bidirectional (c :: k -> Constraint) (a :: k) where
+  -- | Constraint for backwards inference. 
+  -- Should not be recursively bidirectional (it means that all constraints 
+  -- should not be wrapped in 'Bidirectional', e. g. @Show a@ but not
+  -- @Bidirectional Show a@)
+  type Constr c a :: Constraint
+
+{-| 
+  Class for recursive bidirectional instances, i. e. for instances, such
+  that components also have bidirectional instance. Use 'Bidirectional'
+  non-recursive variant, if you need only one step in backward direction.
+
+  Arguments:
+    
+  - @c@ class for which we declare bidirectional instance
+  - @a@ data type for which instance is provided
+
+  For example, this is a nice recursive instance:
+  
+  > instance BidirectionalRec Show a => BidirectionalRec Show [a] where
+  >   type ConstrRec Show [a] = BidirectionalRec Show a
+  
+  but this one isn't (actually it should be a 'Bidirectional' instance):
+  
+  > instance Show a => BidirectionalRec Show [a] where
+  >   type ConstrRec Show [a] = Show a
+
+  Instances for this class are supposed to be generated by 
+  'Control.Bidirectional.makeBidirectionalInstances` or by
+  'Control.Bidirectional.decBidirectionalInstances`.
+-}
+class (c a, ConstrRec c a, Bidirectional c a) 
+  => BidirectionalRec (c :: k -> Constraint) (a :: k) where
+  -- | Constraint for backwards inference. 
+  -- Should be recursively bidirectional (it means that all constraints should
+  -- be wrapped in 'BidirectionalRec', e. g. @BidirectionalRec Show a@ but not
+  -- simply @Show a@)
+  type ConstrRec c a :: Constraint
diff --git a/src/Control/Bidirectional/TH.hs b/src/Control/Bidirectional/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Bidirectional/TH.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+{- | 
+  Module:        Control.Bidirectional.TH
+  Description:   Template haskell for generating bidirectional instances
+  Copyright:     Lev Dvorkin (c) 2022
+  License:       MIT
+  Maintainer:    lev_135@mail.ru
+  Stability:     experimental
+-}
+module Control.Bidirectional.TH (
+    decBidirectionalInstances, 
+    makeBidirectionalInstances
+  ) where
+import Language.Haskell.TH (Exp, Q, Dec (InstanceD, ClassD), TypeQ, DecsQ, reify, Info (ClassI), Type (ConT, AppT, TupleT), conT)
+import Control.Bidirectional.Class (Bidirectional, BidirectionalRec, Constr, ConstrRec)
+import Control.Monad (join)
+
+{-| 
+  Declare instance and make it bidirectional at the same time.
+  Provides instances for 'Bidirectional' and 'BidirectionalRec'.
+
+  It's suitable for declaring your own instances. To make existing instances
+  (for example, from libs) bidirectional, use 'makeBidirectionalInstances'.
+
+  You can use it for declaring multiple instances:
+
+  > data A a = A a
+  > data B a b = B a b
+  > data C a b = CA a | CB b
+  > 
+  > decBidirectionalInstances [d| 
+  >     instance Show a => Show (A a) where
+  >       show (A a) = "A " ++ show a
+  >     instance (Show a, Show b) => Show (B a b) where
+  >       show (B a b) = "B " ++ show a ++ " " show b
+  >     instance (Show a, Show b) => Show (C a b) where
+  >       show (CA a) = "CA " ++ show a
+  >       show (CB b) = "CB " ++ show b
+  >   |] 
+-} 
+decBidirectionalInstances :: Q [Dec] -> Q [Dec]
+decBidirectionalInstances instances = do
+  inst <- instances
+  (inst <>) <$> makeBidirectionalInstances instances
+
+{- |
+  Make existing instance bidirectional.
+  Provides instances for 'Bidirectional' and 'BidirectionalRec'.
+
+  It's suitable for making bidirectional existing instances, that you can't 
+  change (for example, from libs). If you want to declare your one instance
+  and make it bidirectional, use 'decBidirectionalInstances'.
+
+  You can use it for declaring multiple instances:
+
+  > makeBidirectionalInstances [d| 
+  >     instance Show a => Show [a]
+  >     instance (Show a, Show b) => Show (a, b)
+  >     instance (Show a, Show b) => Show (Either a b)
+  >   |] 
+  
+  Note that you need not provide the body of instance, only its head. 
+-}
+makeBidirectionalInstances :: Q [Dec] -> Q [Dec]
+makeBidirectionalInstances instances = do
+  insts <- instances
+  join <$> mapM makeBidirectionalInstance insts
+
+makeBidirectionalInstance :: Dec -> Q [Dec]
+makeBidirectionalInstance inst = do
+  let InstanceD Nothing constr (AppT c a) _ = inst
+      c' = pure c
+      a' = pure a
+      constr' = pure $ mkTup constr
+      constrRec' = mkTup <$> mapM mkRec constr
+  [d| 
+    instance (Constr $c' $a') => Bidirectional $c' $a' where
+      type Constr $c' $a' = $constr'
+    instance (ConstrRec $c' $a') => BidirectionalRec $c' $a' where
+      type ConstrRec $c' $a' = $constrRec'
+    |]
+  where 
+    mkTup :: [Type] -> Type
+    mkTup [] = TupleT 0
+    mkTup [t] = AppT (TupleT 1) t
+    mkTup (t : ts) = case mkTup ts of
+      AppT (TupleT n) u -> AppT (AppT (TupleT (n + 1)) t) u
+      _ -> error "tmp" 
+    
+    mkRec :: Type -> Q Type
+    mkRec (AppT a b) = [t| BidirectionalRec $(pure a) $(pure b) |]
+    mkRec t = pure t