diff --git a/convert.cabal b/convert.cabal
--- a/convert.cabal
+++ b/convert.cabal
@@ -2,10 +2,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: bca179adb32f77b4678b362b4fb860f3129554c28e15f6a7a8591877f13e17de
+-- hash: 9ff99b3742ea434885ce185544b4b9b742020093530290716fbda798031db853
 
 name:           convert
-version:        1.4.2
+version:        1.5
 synopsis:       Safe and unsafe data conversion utilities with strong type-level operation. checking.
 category:       Data
 stability:      experimental
@@ -30,6 +30,7 @@
     , bytestring
     , containers
     , data-default
+    , impossible
     , lens
     , template-haskell
     , text
@@ -49,6 +50,9 @@
       Data.Convert.Instances.Text
       Data.Convert.Instances.TH
       Data.Convert.Instances.Tuple
+      Data.Convert2
+      Data.Convert2.Class
+      Data.Convert2.TH
       Text.PrettyPrint.ANSI.Leijen.Convert
   other-modules:
       Paths_convert
diff --git a/src/Data/Convert/Class.hs b/src/Data/Convert/Class.hs
--- a/src/Data/Convert/Class.hs
+++ b/src/Data/Convert/Class.hs
diff --git a/src/Data/Convert2.hs b/src/Data/Convert2.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Convert2.hs
@@ -0,0 +1,4 @@
+
+module Data.Convert2 (module X) where
+
+import Data.Convert2.Class     as X
diff --git a/src/Data/Convert2/Class.hs b/src/Data/Convert2/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Convert2/Class.hs
@@ -0,0 +1,381 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TemplateHaskell     #-}
+
+module Data.Convert2.Class where
+
+import Prelude
+
+import qualified Data.Convert2.TH as TH
+
+-- import Control.Lens
+import GHC.TypeLits
+import Data.Default
+import Data.Impossible (impossible)
+
+-- TODO[WD]: file GHC Bug:
+-- data A a = A a
+-- data B a = B a deriving (Functor)
+-- data C = C
+--
+-- instance Convertible1 A B
+-- instance Convertible (A a) (B a)
+--
+-- test :: A a -> B a' -- WRONG CONSTRAINT INFERRED HERE! FILE A BUG
+-- test = convert'
+
+
+type IdConversionErr (a :: k) 
+    = 'Text "Conversion of the same type (`" ':<>: 'ShowType a ':<>: 'Text "`)"
+ :<>: 'Text " is disabled by default. Please use convert' if you want to enable it."
+    
+
+------------------------
+-- === Convertibe === --
+------------------------
+
+-- === Definition === --
+
+-- > class To<N> tgt src where
+-- >     to<N> :: ∀ t1 t2 ... t<N>. src t1 t2 ... t<N> -> tgt
+-- > class From<N> tgt src where
+-- >     from<N> :: ∀ t1 t2 .. t<N>. tgt -> src t1 t2 ... t<N>
+TH.genConvertibleClasses False (TH.ixedName  "To")   (TH.ixedName  "to")
+TH.genConvertibleClasses False (TH.ixedName' "To")   (TH.ixedName' "to")
+TH.genConvertibleClasses True  (TH.ixedName  "From") (TH.ixedName  "from")
+TH.genConvertibleClasses True  (TH.ixedName' "From") (TH.ixedName' "from")
+
+-- > class UnsafeTo<N> tgt src where
+-- >     unsafeTo<N> :: ∀ t1 t2 ... t<N>. src t1 t2 ... t<N> -> tgt
+-- > class UnsafeFrom<N> tgt src where
+-- >     unsafeFrom<N> :: ∀ t1 t2 .. t<N>. tgt -> src t1 t2 ... t<N>
+TH.genConvertibleClasses False (TH.ixedName  "UnsafeTo")   (TH.ixedName  "unsafeTo")
+TH.genConvertibleClasses False (TH.ixedName' "UnsafeTo")   (TH.ixedName' "unsafeTo")
+TH.genConvertibleClasses True  (TH.ixedName  "UnsafeFrom") (TH.ixedName  "unsafeFrom")
+TH.genConvertibleClasses True  (TH.ixedName' "UnsafeFrom") (TH.ixedName' "unsafeFrom")
+
+
+-- === API Aliases === --
+
+convert :: ∀ tgt src. To tgt src => src -> tgt
+convert = to ; {-# INLINE convert #-}
+
+convert1 :: ∀ tgt src t1. To1 tgt src => src t1 -> tgt
+convert1 = to1 ; {-# INLINE convert1 #-}
+
+convert2 :: ∀ tgt src t1 t2. To2 tgt src => src t1 t2 -> tgt
+convert2 = to2 ; {-# INLINE convert2 #-}
+
+unsafeConvert :: ∀ tgt src. UnsafeTo tgt src => src -> tgt
+unsafeConvert = unsafeTo ; {-# INLINE unsafeConvert #-}
+
+unsafeConvert1 :: ∀ tgt src t1. UnsafeTo1 tgt src => src t1 -> tgt
+unsafeConvert1 = unsafeTo1 ; {-# INLINE unsafeConvert1 #-}
+
+unsafeConvert2 :: ∀ tgt src t1 t2. UnsafeTo2 tgt src => src t1 t2 -> tgt
+unsafeConvert2 = unsafeTo2 ; {-# INLINE unsafeConvert2 #-}
+
+
+convert' :: ∀ tgt src. To' tgt src => src -> tgt
+convert' = to' ; {-# INLINE convert' #-}
+
+convert1' :: ∀ tgt src t1. To1' tgt src => src t1 -> tgt
+convert1' = to1' ; {-# INLINE convert1' #-}
+
+convert2' :: ∀ tgt src t1 t2. To2' tgt src => src t1 t2 -> tgt
+convert2' = to2' ; {-# INLINE convert2' #-}
+
+unsafeConvert' :: ∀ tgt src. UnsafeTo' tgt src => src -> tgt
+unsafeConvert' = unsafeTo' ; {-# INLINE unsafeConvert' #-}
+
+unsafeConvert1' :: ∀ tgt src t1. UnsafeTo1' tgt src => src t1 -> tgt
+unsafeConvert1' = unsafeTo1' ; {-# INLINE unsafeConvert1' #-}
+
+unsafeConvert2' :: ∀ tgt src t1 t2. UnsafeTo2' tgt src => src t1 t2 -> tgt
+unsafeConvert2' = unsafeTo2' ; {-# INLINE unsafeConvert2' #-}
+
+
+-- === Preventing id-conversions === --
+
+-- > instance TypeError (IdConversionErr src) 
+-- >       => To<N> (src t1 t2 ... t<N>) src where
+-- >     to<N> = impossible
+-- >     {-# INLINE to<N> #-}
+--
+-- > instance TypeError (IdConversionErr src) 
+-- >       => From<N> (src t1 t2 ... t<N>) src where
+-- >     from<N> = impossible
+-- >     {-# INLINE from<N> #-}
+TH.genIdConversionErrorInstances (TH.ixedName "To")         (TH.ixedName "to")
+TH.genIdConversionErrorInstances (TH.ixedName "From")       (TH.ixedName "from")
+TH.genIdConversionErrorInstances (TH.ixedName "UnsafeTo")   (TH.ixedName "unsafeTo")
+TH.genIdConversionErrorInstances (TH.ixedName "UnsafeFrom") (TH.ixedName "unsafeFrom")
+
+
+-- === Higher kind defaulting === --
+
+-- > instance {-# OVERLAPPABLE #-} To<N+1> a a'
+-- >       => To<N> (a t) a' where
+-- >    to<N> = to<N+1>
+-- >    {-# INLINE to<N> #-}
+--
+-- > instance {-# OVERLAPPABLE #-} From<N+1> a a'
+-- >       => From<N> (a t) a' where
+-- >    from<N> = from<N+1>
+-- >    {-# INLINE from<N> #-}
+TH.genHigherKindDefInstances (TH.ixedName "To")         (TH.ixedName "to")
+TH.genHigherKindDefInstances (TH.ixedName "From")       (TH.ixedName "from")
+TH.genHigherKindDefInstances (TH.ixedName "UnsafeTo")   (TH.ixedName "unsafeTo")
+TH.genHigherKindDefInstances (TH.ixedName "UnsafeFrom") (TH.ixedName "unsafeFrom")
+
+
+
+-- === Bi-convertibles === --
+
+type Bi  tgt src = (To  tgt src, From  tgt src)
+type Bi1 tgt src = (To1 tgt src, From1 tgt src)
+type Bi2 tgt src = (To2 tgt src, From2 tgt src)
+type Bi3 tgt src = (To3 tgt src, From3 tgt src)
+type Bi4 tgt src = (To4 tgt src, From4 tgt src)
+type Bi5 tgt src = (To5 tgt src, From5 tgt src)
+
+type Bi'  tgt src = (To'  tgt src, From'  tgt src)
+type Bi1' tgt src = (To1' tgt src, From1' tgt src)
+type Bi2' tgt src = (To2' tgt src, From2' tgt src)
+type Bi3' tgt src = (To3' tgt src, From3' tgt src)
+type Bi4' tgt src = (To4' tgt src, From4' tgt src)
+type Bi5' tgt src = (To5' tgt src, From5' tgt src)
+
+
+instance {-# OVERLAPPABLE #-} To' a a where to' = id ; {-# INLINE to' #-} 
+instance To a b => To' a b where to' = to ; {-# INLINE to' #-} 
+
+instance {-# OVERLAPPABLE #-} From' a a where from' = id ; {-# INLINE from' #-} 
+instance From a b => From' a b where from' = from ; {-# INLINE from' #-} 
+
+
+-- -- === Utils === --
+
+-- convertTo  :: ∀ a' a. Convertible  a a' =>              a           -> a'
+-- convertTo1 :: ∀ a' a. Convertible1 a a' => ∀ b.         a b         -> a' 
+-- convertTo2 :: ∀ a' a. Convertible2 a a' => ∀ b c.       a b c       -> a' 
+-- convertTo3 :: ∀ a' a. Convertible3 a a' => ∀ b c d.     a b c d     -> a' 
+-- convertTo4 :: ∀ a' a. Convertible4 a a' => ∀ b c d e.   a b c d e   -> a' 
+-- convertTo5 :: ∀ a' a. Convertible5 a a' => ∀ b c d e f. a b c d e f -> a' 
+-- convertTo  = convert  ; {-# INLINE convertTo  #-}
+-- convertTo1 = convert1 ; {-# INLINE convertTo1 #-}
+-- convertTo2 = convert2 ; {-# INLINE convertTo2 #-}
+-- convertTo3 = convert3 ; {-# INLINE convertTo3 #-}
+-- convertTo4 = convert4 ; {-# INLINE convertTo4 #-}
+-- convertTo5 = convert5 ; {-# INLINE convertTo5 #-}
+
+
+
+-- -------------------------
+-- -- === Convertibe' === --
+-- -------------------------
+
+-- -- === Definition === --
+
+
+
+-- instance {-# OVERLAPPABLE #-} Convertible'  a a where convert'  = id ; {-# INLINE convert'  #-}
+-- -- instance {-# OVERLAPPABLE #-} Convertible1' a (a t1) where convert1' = id ; {-# INLINE convert1' #-}
+-- -- instance {-# OVERLAPPABLE #-} Convertible2' a (a t1 t2) where convert2' = id ; {-# INLINE convert2' #-}
+-- -- instance {-# OVERLAPPABLE #-} Convertible3' a (a t1 t2 t3) where convert3' = id ; {-# INLINE convert3' #-}
+-- -- instance {-# OVERLAPPABLE #-} Convertible4' a (a t1 t2 t3 t4) where convert4' = id ; {-# INLINE convert4' #-}
+-- -- instance {-# OVERLAPPABLE #-} Convertible5' a (a t1 t2 t3 t4 t5) where convert5' = id ; {-# INLINE convert5' #-}
+
+-- instance {-# OVERLAPPABLE #-} Convertible  a a' => Convertible'  a a' where convert'  = convert  ; {-# INLINE convert'  #-}
+-- instance {-# OVERLAPPABLE #-} Convertible1 a a' => Convertible1' a a' where convert1' = convert1 ; {-# INLINE convert1' #-}
+-- instance {-# OVERLAPPABLE #-} Convertible2 a a' => Convertible2' a a' where convert2' = convert2 ; {-# INLINE convert2' #-}
+-- instance {-# OVERLAPPABLE #-} Convertible3 a a' => Convertible3' a a' where convert3' = convert3 ; {-# INLINE convert3' #-}
+-- instance {-# OVERLAPPABLE #-} Convertible4 a a' => Convertible4' a a' where convert4' = convert4 ; {-# INLINE convert4' #-}
+-- instance {-# OVERLAPPABLE #-} Convertible5 a a' => Convertible5' a a' where convert5' = convert5 ; {-# INLINE convert5' #-}
+
+-- convertTo'  :: ∀ a' a. Convertible'  a a' =>              a           -> a'
+-- convertTo1' :: ∀ a' a. Convertible1' a a' => ∀ b.         a b         -> a'
+-- convertTo2' :: ∀ a' a. Convertible2' a a' => ∀ b c.       a b c       -> a' 
+-- convertTo3' :: ∀ a' a. Convertible3' a a' => ∀ b c d.     a b c d     -> a' 
+-- convertTo4' :: ∀ a' a. Convertible4' a a' => ∀ b c d e.   a b c d e   -> a' 
+-- convertTo5' :: ∀ a' a. Convertible5' a a' => ∀ b c d e f. a b c d e f -> a' 
+-- convertTo'  = convert'  ; {-# INLINE convertTo'  #-}
+-- convertTo1' = convert1' ; {-# INLINE convertTo1' #-}
+-- convertTo2' = convert2' ; {-# INLINE convertTo2' #-}
+-- convertTo3' = convert3' ; {-# INLINE convertTo3' #-}
+-- convertTo4' = convert4' ; {-# INLINE convertTo4' #-}
+-- convertTo5' = convert5' ; {-# INLINE convertTo5' #-}
+
+
+
+
+-- -------------------------------
+-- -- === UnsafeConvertible === --
+-- -------------------------------
+
+-- -- === Definition === --
+
+-- -- | UnsafeConvertible allows for conversion between two compatible types. When
+-- --   trying to convert between the same types, compile time error is reported in
+-- --   order to help tracking not needed usages. If you want to enable conversion
+-- --   between the same types, use `convert'` instead.
+-- class UnsafeConvertible  a a' where unsafeConvert  ::              a           -> a'
+-- class UnsafeConvertible1 a a' where unsafeConvert1 :: ∀ b.         a b         -> a'
+-- class UnsafeConvertible2 a a' where unsafeConvert2 :: ∀ b c.       a b c       -> a'
+-- class UnsafeConvertible3 a a' where unsafeConvert3 :: ∀ b c d.     a b c d     -> a'
+-- class UnsafeConvertible4 a a' where unsafeConvert4 :: ∀ b c d e.   a b c d e   -> a'
+-- class UnsafeConvertible5 a a' where unsafeConvert5 :: ∀ b c d e f. a b c d e f -> a'
+
+
+-- -- === Higher kind defaulting === --
+
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible1 a a' => UnsafeConvertible  (a t) a' where unsafeConvert  = unsafeConvert1 ; {-# INLINE unsafeConvert  #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible2 a a' => UnsafeConvertible1 (a t) a' where unsafeConvert1 = unsafeConvert2 ; {-# INLINE unsafeConvert1 #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible3 a a' => UnsafeConvertible2 (a t) a' where unsafeConvert2 = unsafeConvert3 ; {-# INLINE unsafeConvert2 #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible4 a a' => UnsafeConvertible3 (a t) a' where unsafeConvert3 = unsafeConvert4 ; {-# INLINE unsafeConvert3 #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible5 a a' => UnsafeConvertible4 (a t) a' where unsafeConvert4 = unsafeConvert5 ; {-# INLINE unsafeConvert4 #-}
+
+
+-- -- === Identity conversion errors === --
+
+-- instance TypeError (IdConversionErr a) => UnsafeConvertible  a a where unsafeConvert  = impossible ; {-# INLINE unsafeConvert  #-}
+-- instance TypeError (IdConversionErr a) => UnsafeConvertible1 a (a t1) where unsafeConvert1 = impossible ; {-# INLINE unsafeConvert1 #-}
+-- instance TypeError (IdConversionErr a) => UnsafeConvertible2 a (a t1 t2) where unsafeConvert2 = impossible ; {-# INLINE unsafeConvert2 #-}
+-- instance TypeError (IdConversionErr a) => UnsafeConvertible3 a (a t1 t2 t3) where unsafeConvert3 = impossible ; {-# INLINE unsafeConvert3 #-}
+-- instance TypeError (IdConversionErr a) => UnsafeConvertible4 a (a t1 t2 t3 t4) where unsafeConvert4 = impossible ; {-# INLINE unsafeConvert4 #-}
+-- instance TypeError (IdConversionErr a) => UnsafeConvertible5 a (a t1 t2 t3 t4 t5) where unsafeConvert5 = impossible ; {-# INLINE unsafeConvert5 #-}
+
+
+-- -- === Utils === --
+
+-- unsafeConvertTo  :: ∀ a' a. UnsafeConvertible  a a' =>              a           -> a'
+-- unsafeConvertTo1 :: ∀ a' a. UnsafeConvertible1 a a' => ∀ b.         a b         -> a' 
+-- unsafeConvertTo2 :: ∀ a' a. UnsafeConvertible2 a a' => ∀ b c.       a b c       -> a' 
+-- unsafeConvertTo3 :: ∀ a' a. UnsafeConvertible3 a a' => ∀ b c d.     a b c d     -> a' 
+-- unsafeConvertTo4 :: ∀ a' a. UnsafeConvertible4 a a' => ∀ b c d e.   a b c d e   -> a' 
+-- unsafeConvertTo5 :: ∀ a' a. UnsafeConvertible5 a a' => ∀ b c d e f. a b c d e f -> a' 
+-- unsafeConvertTo  = unsafeConvert  ; {-# INLINE unsafeConvertTo  #-}
+-- unsafeConvertTo1 = unsafeConvert1 ; {-# INLINE unsafeConvertTo1 #-}
+-- unsafeConvertTo2 = unsafeConvert2 ; {-# INLINE unsafeConvertTo2 #-}
+-- unsafeConvertTo3 = unsafeConvert3 ; {-# INLINE unsafeConvertTo3 #-}
+-- unsafeConvertTo4 = unsafeConvert4 ; {-# INLINE unsafeConvertTo4 #-}
+-- unsafeConvertTo5 = unsafeConvert5 ; {-# INLINE unsafeConvertTo5 #-}
+
+
+
+-- -------------------------------
+-- -- === UnsafeConvertibe' === --
+-- -------------------------------
+
+-- -- === Definition === --
+
+-- class UnsafeConvertible'  a a' where unsafeConvert'  ::              a           -> a'
+-- class UnsafeConvertible1' a a' where unsafeConvert1' :: ∀ b.         a b         -> a'
+-- class UnsafeConvertible2' a a' where unsafeConvert2' :: ∀ b c.       a b c       -> a' 
+-- class UnsafeConvertible3' a a' where unsafeConvert3' :: ∀ b c d.     a b c d     -> a' 
+-- class UnsafeConvertible4' a a' where unsafeConvert4' :: ∀ b c d e.   a b c d e   -> a' 
+-- class UnsafeConvertible5' a a' where unsafeConvert5' :: ∀ b c d e f. a b c d e f -> a'
+
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible'  a a where unsafeConvert'  = impossible ; {-# INLINE unsafeConvert'  #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible1' a (a t1) where unsafeConvert1' = impossible ; {-# INLINE unsafeConvert1' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible2' a (a t1 t2) where unsafeConvert2' = impossible ; {-# INLINE unsafeConvert2' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible3' a (a t1 t2 t3) where unsafeConvert3' = impossible ; {-# INLINE unsafeConvert3' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible4' a (a t1 t2 t3 t4) where unsafeConvert4' = impossible ; {-# INLINE unsafeConvert4' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible5' a (a t1 t2 t3 t4 t5) where unsafeConvert5' = impossible ; {-# INLINE unsafeConvert5' #-}
+
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible  a a' => UnsafeConvertible'  a a' where unsafeConvert'  = unsafeConvert  ; {-# INLINE unsafeConvert'  #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible1 a a' => UnsafeConvertible1' a a' where unsafeConvert1' = unsafeConvert1 ; {-# INLINE unsafeConvert1' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible2 a a' => UnsafeConvertible2' a a' where unsafeConvert2' = unsafeConvert2 ; {-# INLINE unsafeConvert2' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible3 a a' => UnsafeConvertible3' a a' where unsafeConvert3' = unsafeConvert3 ; {-# INLINE unsafeConvert3' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible4 a a' => UnsafeConvertible4' a a' where unsafeConvert4' = unsafeConvert4 ; {-# INLINE unsafeConvert4' #-}
+-- instance {-# OVERLAPPABLE #-} UnsafeConvertible5 a a' => UnsafeConvertible5' a a' where unsafeConvert5' = unsafeConvert5 ; {-# INLINE unsafeConvert5' #-}
+
+-- unsafeConvertTo'  :: ∀ a' a. UnsafeConvertible'  a a' =>              a           -> a'
+-- unsafeConvertTo1' :: ∀ a' a. UnsafeConvertible1' a a' => ∀ b.         a b         -> a'
+-- unsafeConvertTo2' :: ∀ a' a. UnsafeConvertible2' a a' => ∀ b c.       a b c       -> a' 
+-- unsafeConvertTo3' :: ∀ a' a. UnsafeConvertible3' a a' => ∀ b c d.     a b c d     -> a' 
+-- unsafeConvertTo4' :: ∀ a' a. UnsafeConvertible4' a a' => ∀ b c d e.   a b c d e   -> a' 
+-- unsafeConvertTo5' :: ∀ a' a. UnsafeConvertible5' a a' => ∀ b c d e f. a b c d e f -> a' 
+-- unsafeConvertTo'  = unsafeConvert'  ; {-# INLINE unsafeConvertTo'  #-}
+-- unsafeConvertTo1' = unsafeConvert1' ; {-# INLINE unsafeConvertTo1' #-}
+-- unsafeConvertTo2' = unsafeConvert2' ; {-# INLINE unsafeConvertTo2' #-}
+-- unsafeConvertTo3' = unsafeConvert3' ; {-# INLINE unsafeConvertTo3' #-}
+-- unsafeConvertTo4' = unsafeConvert4' ; {-# INLINE unsafeConvertTo4' #-}
+-- unsafeConvertTo5' = unsafeConvert5' ; {-# INLINE unsafeConvertTo5' #-}
+
+
+
+-- ----------------------------------
+-- -- === Partial convertibles === --
+-- ----------------------------------
+
+-- -- === Errors === --
+
+-- data SimpleConversionError = SimpleConversionError deriving (Show)
+-- instance Default SimpleConversionError where def = SimpleConversionError ; {-# INLINE def #-}
+
+
+-- -- === Classes === --
+
+-- -- | PartialConvertible allows conversions that could fail with `ConversionError`.
+-- class PartialConvertible t t' where
+--     type family ConversionError t t'
+--     convertAssert :: t -> Maybe (ConversionError t t')
+--     unsafeConvertOld :: t -> t'
+
+-- defConvertAssert :: Default e => (a -> Bool) -> a -> Maybe e
+-- defConvertAssert f = \s -> if f s then Just def else Nothing
+
+-- -- unsafeConvertTo :: ∀ t' t. PartialConvertible t t' => t -> t'
+-- -- unsafeConvertTo = unsafeConvert ; {-# INLINE unsafeConvertTo #-}
+
+-- convertAssertTo :: ∀ t' t. PartialConvertible t t' => t -> Maybe (ConversionError t t')
+-- convertAssertTo = convertAssert @t @t' ; {-# INLINE convertAssertTo #-}
+
+-- maybeConvert :: ∀ t t'. PartialConvertible t t' => t -> Maybe t'
+-- maybeConvert t = const (unsafeConvertOld t) <$> convertAssertTo @t' t ; {-# INLINE maybeConvert #-}
+
+-- tryConvert :: ∀ t t'. PartialConvertible t t' => t -> Either (ConversionError t t') t'
+-- tryConvert t = maybe (Right $ unsafeConvertOld t) Left $ convertAssertTo @t' t ; {-# INLINE tryConvert #-}
+
+
+
+-- -----------------------------
+-- -- === Bi-convertibles === --
+-- -----------------------------
+
+-- type BiConvertible  t t' = (Convertible  t t', Convertible  t' t)
+-- type BiConvertible'  t t' = (Convertible'  t t', Convertible'  t' t)
+
+
+-- converted   :: BiConvertible   t t' =>                        Iso' t                  t'
+-- converted'  :: BiConvertible'  t t' =>                        Iso' t                  t'
+-- converted   = iso convert   convert   ; {-# INLINE converted   #-}
+-- converted'  = iso convert'  convert'  ; {-# INLINE converted'  #-}
+
+-- convertedTo   :: BiConvertible   t' t =>                        Iso' t                  t'
+-- convertedTo'  :: BiConvertible'  t' t =>                        Iso' t                  t'
+-- convertedTo   = converted   ; {-# INLINE convertedTo   #-}
+-- convertedTo'  = converted'  ; {-# INLINE convertedTo'  #-}
+
+
+-- -- === ConvertibleVia === --
+
+-- type ConvertibleVia  t p t' = (Convertible  t p, Convertible  p t')
+
+-- convertVia  :: ∀ p t t'. ConvertibleVia  t p t' =>                        t                -> t'
+-- convertVia  = convert  . convertTo  @p ; {-# INLINE convertVia #-}
+
+-- type ConvertibleVia'  t p t' = (Convertible'  t p, Convertible'  p t')
+
+-- convertVia'  :: ∀ p t t'. ConvertibleVia'  t p t' =>                        t                -> t'
+-- convertVia'  = convert'  . convertTo'  @p ; {-# INLINE convertVia' #-}
+
+-- -- type PartialConvertibleVia  t p t' = (PartialConvertible  t p, PartialConvertible  p t')
+-- -- unsafeConvertVia :: ∀ p t t'. PartialConvertibleVia t p t' => t -> t'
+-- -- unsafeConvertVia = unsafeConvert . unsafeConvertTo @p ; {-# INLINE unsafeConvertVia #-}
diff --git a/src/Data/Convert2/TH.hs b/src/Data/Convert2/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Convert2/TH.hs
@@ -0,0 +1,88 @@
+module Data.Convert2.TH where
+
+import Prelude
+
+import Language.Haskell.TH 
+
+maxKind :: Int
+maxKind = 5
+
+appsT :: Foldable f => Type -> f Type -> Type
+appsT = foldl (AppT)
+
+showIfNot0 :: Int -> String
+showIfNot0 i = if i == 0 then "" else show i
+
+ixedName :: String -> Int -> String
+ixedName s i = s <> showIfNot0 i
+
+ixedName' :: String -> Int -> String
+ixedName' s i = ixedName s i <> "'"
+
+src, tgt :: Name
+src  = mkName "src"
+tgt = mkName "tgt"
+
+type IString = Int -> String
+
+swap :: (a,b) -> (b,a)
+swap (a,b) = (b,a)
+
+-- > class Convertible1 src tgt where convert1 :: ∀ b. src b -> tgt
+genConvertibleClass :: Bool -> IString -> IString -> Int -> Dec
+genConvertibleClass inv sname sfname i = cls where
+    name   = mkName $ sname  i
+    fname  = mkName $ sfname i
+    vnames = mkName . ("t" <>) . show <$> [1 .. i]
+    binds  = ForallT (PlainTV <$> vnames) []
+    (arg,result) = (if inv then swap else id)
+                 $ (appsT (VarT src) (VarT <$> vnames), VarT tgt)
+    body  = SigD fname (binds $ AppT (AppT ArrowT arg) result)
+    cls   = ClassD [] name [PlainTV tgt, PlainTV src] [] [body]
+
+-- > instance {-# OVERLAPPABLE #-} Convertible2 src tgt
+-- >       => Convertible1 (src t) tgt where
+-- >    convert1 = convert2
+-- >    {-# INLINE convert1 #-}
+genHigherKindDefInstance :: IString -> IString -> Int -> Dec
+genHigherKindDefInstance sname sfname i = inst where
+    name    = mkName $ sname  i
+    fname   = mkName $ sfname i
+    nameH   = mkName $ sname  (i + 1)
+    fnameH  = mkName $ sfname (i + 1)
+    overlap = Just Overlappable
+    ctx     = [AppT (AppT (ConT nameH) (VarT tgt)) (VarT src)]
+    body    = ValD (VarP fname) (NormalB (VarE fnameH)) []
+    inline  = PragmaD (InlineP fname Inline FunLike AllPhases)
+    arg     = appsT (VarT src) [VarT (mkName "t")]
+    inst    = InstanceD overlap ctx (AppT (AppT (ConT name) (VarT tgt)) arg) 
+              [body, inline]
+
+-- > instance TypeError (IdConversionErr src) 
+-- >       => Convertible1 src (src t1) where
+-- >     convert1 = impossible
+-- >     {-# INLINE convert1 #-}
+genIdConversionErrorInstance :: IString -> IString -> Int -> Dec
+genIdConversionErrorInstance sname sfname i = inst where
+    name    = mkName $ sname  i
+    fname   = mkName $ sfname i
+    vnames  = mkName . ("t" <>) . show <$> [1 .. i]
+    err     = AppT (ConT (mkName "TypeError")) 
+            $ AppT (ConT (mkName "IdConversionErr")) 
+            $ VarT src
+    overlap = Nothing
+    ctx     = [err]
+    body    = ValD (VarP fname) (NormalB (VarE $ mkName "impossible")) []
+    inline  = PragmaD (InlineP fname Inline FunLike AllPhases)
+    arg     = appsT (VarT src) (VarT <$> vnames)
+    inst    = InstanceD overlap ctx (AppT (AppT (ConT name) arg) (VarT src)) 
+              [body, inline]
+
+genConvertibleClasses :: Bool -> IString -> IString -> Q [Dec]
+genConvertibleClasses inv sname sfname = pure $ genConvertibleClass inv sname sfname <$> [0 .. maxKind]
+
+genHigherKindDefInstances :: IString -> IString -> Q [Dec]
+genHigherKindDefInstances sname sfname = pure $ genHigherKindDefInstance sname sfname <$> [0 .. maxKind - 1]
+
+genIdConversionErrorInstances :: IString -> IString -> Q [Dec]
+genIdConversionErrorInstances sname sfname = pure $ genIdConversionErrorInstance sname sfname <$> [0 .. maxKind]