diff --git a/CHANGELOG b/CHANGELOG
new file mode 100644
--- /dev/null
+++ b/CHANGELOG
@@ -0,0 +1,8 @@
+CHANGELOG
+
+0.9 -> 1.0
+  - Added type changing traversals with Generics.OneLiner.Binary
+  - Changed Generics.OneLiner.Internal to work on binary type classes.
+  - Added Generics.OneLiner.Internal.Unary to convert the internals to unary
+  - Moved classes to Generics.OneLiner.Classes
+  - Started a change log
diff --git a/examples/tinplate.hs b/examples/tinplate.hs
--- a/examples/tinplate.hs
+++ b/examples/tinplate.hs
@@ -40,6 +40,7 @@
 
 tinplate :: forall a b f. (ADT b, Constraints b (TinplateAlias a), Applicative f) => (a -> f a) -> b -> f b
 tinplate f = gtraverse @(TinplateAlias a) (trav f)
+{-# INLINE tinplate #-}
 
 
 
diff --git a/one-liner.cabal b/one-liner.cabal
--- a/one-liner.cabal
+++ b/one-liner.cabal
@@ -1,5 +1,5 @@
 Name:                 one-liner
-Version:              0.9.2
+Version:              1.0
 Synopsis:             Constraint-based generics
 Description:          Write short and concise generic instances of type classes.
                       one-liner is particularly useful for writing default
@@ -8,7 +8,7 @@
 Bug-reports:          https://github.com/sjoerdvisscher/one-liner/issues
 License:              BSD3
 License-file:         LICENSE
-Author:               Sjoerd Visscher
+Author:               Sjoerd Visscher, Xia Li-yao
 Maintainer:           sjoerd@w3future.com
 Category:             Generics
 Build-type:           Simple
@@ -16,13 +16,17 @@
 
 Extra-Source-Files:
   examples/*.hs
+  CHANGELOG
 
 Library
   HS-Source-Dirs:  src
 
   Exposed-modules:
     Generics.OneLiner
+    Generics.OneLiner.Binary
+    Generics.OneLiner.Classes
     Generics.OneLiner.Internal
+    Generics.OneLiner.Internal.Unary
 
   Build-depends:
       base          >= 4.9 && < 5
diff --git a/src/Generics/OneLiner.hs b/src/Generics/OneLiner.hs
--- a/src/Generics/OneLiner.hs
+++ b/src/Generics/OneLiner.hs
@@ -36,7 +36,6 @@
   -- * Combining values
   mzipWith, mzipWith', zipWithA,
   mzipWith1, mzipWith1', zipWithA1,
-  Zip(..),
   -- * Consuming values
   consume, consume1,
   -- * Functions for records
@@ -62,9 +61,8 @@
   ADT1, ADTNonEmpty1, ADTRecord1, Constraints1, Constraints01,
   FunConstraints, FunResult,
   AnyType
-) where
+  ) where
 
-import GHC.Generics
 import Control.Applicative
 import Data.Bifunctor.Biff
 import Data.Bifunctor.Clown
@@ -73,8 +71,9 @@
 import Data.Functor.Contravariant.Divisible
 import Data.Profunctor
 import Data.Tagged
-import Generics.OneLiner.Internal
-
+import Generics.OneLiner.Classes
+import Generics.OneLiner.Internal (FunConstraints, FunResult, autoApply, Pair(..), (.:))
+import Generics.OneLiner.Internal.Unary
 
 -- | Create a value (one for each constructor), given how to construct the components.
 --
@@ -269,28 +268,6 @@
 zipWithA1 f = dimap Zip runZip $ generic1 @c $ dimap runZip Zip f
 {-# INLINE zipWithA1 #-}
 
-newtype Zip f a b = Zip { runZip :: a -> a -> f b }
-instance Functor f => Profunctor (Zip f) where
-  dimap f g (Zip h) = Zip $ \a1 a2 -> fmap g (h (f a1) (f a2))
-  {-# INLINE dimap #-}
-instance Applicative f => GenericUnitProfunctor (Zip f) where
-  unit = Zip $ \_ _ -> pure U1
-  {-# INLINE unit #-}
-instance Applicative f => GenericProductProfunctor (Zip f) where
-  mult (Zip f) (Zip g) = Zip $ \(al :*: ar) (bl :*: br) -> (:*:) <$> f al bl <*> g ar br
-  {-# INLINE mult #-}
-instance Alternative f => GenericSumProfunctor (Zip f) where
-  plus (Zip f) (Zip g) = Zip h where
-    h (L1 a) (L1 b) = fmap L1 (f a b)
-    h (R1 a) (R1 b) = fmap R1 (g a b)
-    h _ _ = empty
-  {-# INLINE plus #-}
-instance Alternative f => GenericEmptyProfunctor (Zip f) where
-  zero = Zip absurd
-  {-# INLINE zero #-}
-  identity = Zip $ \_ _ -> empty
-  {-# INLINE identity #-}
-
 inm2 :: (t -> t -> m) -> t -> t -> Compose Maybe (Const m) a
 inm2 f = Compose .: Just .: Const .: f
 {-# INLINE inm2 #-}
@@ -350,11 +327,6 @@
 createA' f = runJoker $ record @c $ Joker f
 {-# INLINE createA' #-}
 
-data Pair a = Pair a a
-instance Functor Pair where
-  fmap f (Pair a b) = Pair (f a) (f b)
-  {-# INLINE fmap #-}
-
 -- | Create an F-algebra, given an F-algebra for each of the components.
 --
 -- @
@@ -390,8 +362,3 @@
              => (forall d e s. c s => (f d -> e) -> f (s d) -> s e) -> (f a -> b) -> f (t a) -> t b
 gcotraverse1 f p = runCostar $ record1 @c (Costar . f . runCostar) (Costar p)
 {-# INLINE gcotraverse1 #-}
-
-infixr 9 .:
-(.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
-(.:) = (.) . (.)
-{-# INLINE (.:) #-}
diff --git a/src/Generics/OneLiner/Binary.hs b/src/Generics/OneLiner/Binary.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/OneLiner/Binary.hs
@@ -0,0 +1,157 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.OneLiner.Binary
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- These generic functions allow changing the types of the constant leaves. 
+-- They require type classes with 2 parameters, the first for the input type 
+-- and the second for the output type.
+--
+-- All functions without postfix are for instances of `Generic`, and functions
+-- with postfix @1@ are for instances of `Generic1` (with kind @* -> *@) which
+-- get an extra argument to specify how to deal with the parameter.
+-- Functions with postfix @01@ are also for `Generic1` but they get yet another
+-- argument that, like the `Generic` functions, allows handling of constant leaves.
+-----------------------------------------------------------------------------
+{-# LANGUAGE
+    RankNTypes
+  , Trustworthy
+  , TypeFamilies
+  , ConstraintKinds
+  , FlexibleContexts
+  , TypeApplications
+  , AllowAmbiguousTypes
+  , ScopedTypeVariables
+  #-}
+module Generics.OneLiner.Binary (
+  -- * Traversing values
+  gmap, gtraverse,
+  gmap1, gtraverse1,
+  -- * Combining values
+  zipWithA, zipWithA1,
+  -- * Functions for records
+  -- | These functions only work for single constructor data types.
+  unaryOp, binaryOp, algebra, dialgebra, gcotraverse1,
+  -- * Generic programming with profunctors
+  -- | All the above functions have been implemented using these functions,
+  -- using different `profunctor`s.
+  record, nonEmpty, generic,
+  record1, nonEmpty1, generic1,
+  record01, nonEmpty01, generic01,
+  -- ** Classes
+  GenericRecordProfunctor,
+  GenericNonEmptyProfunctor,
+  GenericProfunctor,
+  GenericUnitProfunctor(..),
+  GenericProductProfunctor(..),
+  GenericSumProfunctor(..),
+  GenericEmptyProfunctor(..),
+  -- * Types
+  ADT, ADTNonEmpty, ADTRecord, Constraints,
+  ADT1, ADTNonEmpty1, ADTRecord1, Constraints1, Constraints01,
+  FunConstraints, FunResult,
+  AnyType
+) where
+
+import GHC.Generics
+import Control.Applicative
+import Data.Bifunctor.Biff
+import Data.Profunctor
+import Generics.OneLiner.Classes
+import Generics.OneLiner.Internal
+
+-- | Map over a structure, updating each component.
+--
+-- `gmap` is `generic` specialized to @(->)@.
+gmap :: forall c t t'. (ADT t t', Constraints t t' c)
+     => (forall s s'. c s s' => s -> s') -> t -> t'
+gmap = generic @c
+{-# INLINE gmap #-}
+
+-- | Map each component of a structure to an action, evaluate these actions from left to right, and collect the results.
+--
+-- `gtraverse` is `generic` specialized to `Star`.
+gtraverse :: forall c t t' f. (ADT t t', Constraints t t' c, Applicative f)
+          => (forall s s'. c s s' => s -> f s') -> t -> f t'
+gtraverse f = runStar $ generic @c $ Star f
+{-# INLINE gtraverse #-}
+
+-- | `gmap1` is `generic1` specialized to @(->)@.
+gmap1 :: forall c t t' a b. (ADT1 t t', Constraints1 t t' c)
+     => (forall d e s s'. c s s' => (d -> e) -> s d -> s' e) -> (a -> b) -> t a -> t' b
+gmap1 = generic1 @c
+{-# INLINE gmap1 #-}
+
+-- | `gtraverse1` is `generic1` specialized to `Star`.
+gtraverse1 :: forall c t t' f a b. (ADT1 t t', Constraints1 t t' c, Applicative f)
+           => (forall d e s s'. c s s' => (d -> f e) -> s d -> f (s' e)) -> (a -> f b) -> t a -> f (t' b)
+gtraverse1 f = dimap Star runStar $ generic1 @c $ dimap runStar Star f
+{-# INLINE gtraverse1 #-}
+
+-- | Combine two values by combining each component of the structures with the given function, under an applicative effect.
+-- Returns `empty` if the constructors don't match.
+--
+-- `zipWithA` is `generic` specialized to `Zip`
+zipWithA :: forall c t t' f. (ADT t t', Constraints t t' c, Alternative f)
+         => (forall s s'. c s s' => s -> s -> f s') -> t -> t -> f t'
+zipWithA f = runZip $ generic @c $ Zip f
+{-# INLINE zipWithA #-}
+
+-- | `zipWithA1` is `generic1` specialized to `Zip`
+zipWithA1 :: forall c t t' f a b. (ADT1 t t', Constraints1 t t' c, Alternative f)
+          => (forall d e s s'. c s s' => (d -> d -> f e) -> s d -> s d -> f (s' e))
+          -> (a -> a -> f b) -> t a -> t a -> f (t' b)
+zipWithA1 f = dimap Zip runZip $ generic1 @c $ dimap runZip Zip f
+{-# INLINE zipWithA1 #-}
+
+-- | Implement a unary operator by calling the operator on the components.
+-- This is here for consistency, it is the same as `record`.
+--
+-- @
+-- `negate` = `unaryOp` \@`Num` `negate`
+-- @
+unaryOp :: forall c t t'. (ADTRecord t t', Constraints t t' c)
+        => (forall s s'. c s s' => s -> s') -> t -> t'
+unaryOp = record @c
+{-# INLINE unaryOp #-}
+
+-- | Implement a binary operator by calling the operator on the components.
+--
+-- @
+-- `mappend` = `binaryOp` \@`Monoid` `mappend`
+-- (`+`) = `binaryOp` \@`Num` (`+`)
+-- @
+--
+-- `binaryOp` is `algebra` specialized to pairs.
+binaryOp :: forall c t t'. (ADTRecord t t', Constraints t t' c)
+         => (forall s s'. c s s' => s -> s -> s') -> t -> t -> t'
+binaryOp f = algebra @c (\(Pair a b) -> f a b) .: Pair
+{-# INLINE binaryOp #-}
+
+-- | Create an F-algebra, given an F-algebra for each of the components.
+--
+-- @
+-- `binaryOp` f l r = `algebra` \@c (\\(Pair a b) -> f a b) (Pair l r)
+-- @
+--
+-- `algebra` is `record` specialized to `Costar`.
+algebra :: forall c t t' f. (ADTRecord t t', Constraints t t' c, Functor f)
+        => (forall s s'. c s s' => f s -> s') -> f t -> t'
+algebra f = runCostar $ record @c $ Costar f
+{-# INLINE algebra #-}
+
+-- | `dialgebra` is `record` specialized to @`Biff` (->)@.
+dialgebra :: forall c t t' f g. (ADTRecord t t', Constraints t t' c, Functor f, Applicative g)
+        => (forall s s'. c s s' => f s -> g s') -> f t -> g t'
+dialgebra f = runBiff $ record @c $ Biff f
+{-# INLINE dialgebra #-}
+
+-- | `gcotraverse1` is `record1` specialized to `Costar`.
+gcotraverse1 :: forall c t t' f a b. (ADTRecord1 t t', Constraints1 t t' c, Functor f)
+             => (forall d e s s'. c s s' => (f d -> e) -> f (s d) -> s' e) -> (f a -> b) -> f (t a) -> t' b
+gcotraverse1 f p = runCostar $ record1 @c (Costar . f . runCostar) (Costar p)
+{-# INLINE gcotraverse1 #-}
diff --git a/src/Generics/OneLiner/Classes.hs b/src/Generics/OneLiner/Classes.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/OneLiner/Classes.hs
@@ -0,0 +1,219 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.OneLiner.Classes
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+{-# LANGUAGE
+    EmptyCase
+  , LambdaCase
+  , TypeOperators
+  , MonoLocalBinds
+  , FlexibleInstances
+  , UndecidableInstances
+  #-}
+module Generics.OneLiner.Classes where
+
+import GHC.Generics
+import Control.Applicative
+import Data.Bifunctor.Biff
+import Data.Bifunctor.Clown
+import Data.Bifunctor.Joker
+import Data.Bifunctor.Product
+import Data.Bifunctor.Tannen
+import Data.Functor.Contravariant.Divisible
+import Data.Functor.Compose
+import Data.Profunctor
+import Data.Tagged
+
+-- | A generic function using a `GenericRecordProfunctor` works on any data type
+-- with exactly one constructor, a.k.a. records,
+-- with multiple fields (`mult`) or no fields (`unit`).
+--
+-- `GenericRecordProfunctor` is similar to `ProductProfuctor` from the
+-- product-profunctor package, but using types from GHC.Generics.
+class (Profunctor p, GenericUnitProfunctor p, GenericProductProfunctor p) => GenericRecordProfunctor p
+instance (Profunctor p, GenericUnitProfunctor p, GenericProductProfunctor p) => GenericRecordProfunctor p
+
+-- | A generic function using a `GenericNonEmptyProfunctor` works on any data
+-- type with at least one constructor.
+class (GenericRecordProfunctor p, GenericSumProfunctor p) => GenericNonEmptyProfunctor p where
+instance (GenericRecordProfunctor p, GenericSumProfunctor p) => GenericNonEmptyProfunctor p where
+
+-- | A generic function using a `GenericProfunctor` works on any
+-- algebraic data type, including those with no constructors and constants.
+class (GenericNonEmptyProfunctor p, GenericEmptyProfunctor p) => GenericProfunctor p where
+instance (GenericNonEmptyProfunctor p, GenericEmptyProfunctor p) => GenericProfunctor p where
+
+
+class Profunctor p => GenericUnitProfunctor p where
+  unit :: p (U1 a) (U1 a')
+
+class Profunctor p => GenericProductProfunctor p where
+  mult :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :*: g) a) ((f' :*: g') a')
+
+class Profunctor p => GenericSumProfunctor p where
+  plus :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :+: g) a) ((f' :+: g') a')
+
+class Profunctor p => GenericEmptyProfunctor p where
+  identity :: p a a
+  zero :: p (V1 a) (V1 a')
+
+
+instance GenericUnitProfunctor (->) where
+  unit _ = U1
+  {-# INLINE unit #-}
+instance GenericProductProfunctor (->) where
+  mult f g (l :*: r) = f l :*: g r
+  {-# INLINE mult #-}
+instance GenericSumProfunctor (->) where
+  plus f g = e1 (L1 . f) (R1 . g)
+  {-# INLINE plus #-}
+instance GenericEmptyProfunctor (->) where
+  zero = absurd
+  {-# INLINE zero #-}
+  identity = id
+  {-# INLINE identity #-}
+
+instance GenericUnitProfunctor Tagged where
+  unit = Tagged U1
+  {-# INLINE unit #-}
+instance GenericProductProfunctor Tagged where
+  mult (Tagged l) (Tagged r) = Tagged $ l :*: r
+  {-# INLINE mult #-}
+
+instance Applicative f => GenericUnitProfunctor (Star f) where
+  unit = Star $ \_ -> pure U1
+  {-# INLINE unit #-}
+instance Applicative f => GenericProductProfunctor (Star f) where
+  mult (Star f) (Star g) = Star $ \(l :*: r) -> (:*:) <$> f l <*> g r
+  {-# INLINE mult #-}
+instance Applicative f => GenericSumProfunctor (Star f) where
+  plus (Star f) (Star g) = Star $ e1 (fmap L1 . f) (fmap R1 . g)
+  {-# INLINE plus #-}
+instance Applicative f => GenericEmptyProfunctor (Star f) where
+  zero = Star absurd
+  {-# INLINE zero #-}
+  identity = Star pure
+  {-# INLINE identity #-}
+
+instance Functor f => GenericUnitProfunctor (Costar f) where
+  unit = Costar $ const U1
+  {-# INLINE unit #-}
+instance Functor f => GenericProductProfunctor (Costar f) where
+  mult (Costar f) (Costar g) = Costar $ \lr -> f (fst1 <$> lr) :*: g (snd1 <$> lr)
+  {-# INLINE mult #-}
+
+instance (Functor f, Applicative g, Profunctor p, GenericUnitProfunctor p) => GenericUnitProfunctor (Biff p f g) where
+  unit = Biff $ dimap (const U1) pure unit
+  {-# INLINE unit #-}
+instance (Functor f, Applicative g, Profunctor p, GenericProductProfunctor p) => GenericProductProfunctor (Biff p f g) where
+  mult (Biff f) (Biff g) = Biff $ dimap
+    (liftA2 (:*:) (Compose . fmap fst1) (Compose . fmap snd1))
+    (\(Compose l :*: Compose r) -> liftA2 (:*:) l r)
+    (mult (dimap getCompose Compose f) (dimap getCompose Compose g))
+  {-# INLINE mult #-}
+
+instance Applicative f => GenericUnitProfunctor (Joker f) where
+  unit = Joker $ pure U1
+  {-# INLINE unit #-}
+instance Applicative f => GenericProductProfunctor (Joker f) where
+  mult (Joker l) (Joker r) = Joker $ (:*:) <$> l <*> r
+  {-# INLINE mult #-}
+instance Alternative f => GenericSumProfunctor (Joker f) where
+  plus (Joker l) (Joker r) = Joker $ L1 <$> l <|> R1 <$> r
+  {-# INLINE plus #-}
+instance Alternative f => GenericEmptyProfunctor (Joker f) where
+  zero = Joker empty
+  {-# INLINE zero #-}
+  identity = Joker empty
+  {-# INLINE identity #-}
+
+instance Divisible f => GenericUnitProfunctor (Clown f) where
+  unit = Clown conquer
+  {-# INLINE unit #-}
+instance Divisible f => GenericProductProfunctor (Clown f) where
+  mult (Clown f) (Clown g) = Clown $ divide (\(l :*: r) -> (l, r)) f g
+  {-# INLINE mult #-}
+instance Decidable f => GenericSumProfunctor (Clown f) where
+  plus (Clown f) (Clown g) = Clown $ choose (e1 Left Right) f g
+  {-# INLINE plus #-}
+instance Decidable f => GenericEmptyProfunctor (Clown f) where
+  zero = Clown $ lose absurd
+  {-# INLINE zero #-}
+  identity = Clown conquer
+  {-# INLINE identity #-}
+
+instance (GenericUnitProfunctor p, GenericUnitProfunctor q) => GenericUnitProfunctor (Product p q) where
+  unit = Pair unit unit
+  {-# INLINE unit #-}
+instance (GenericProductProfunctor p, GenericProductProfunctor q) => GenericProductProfunctor (Product p q) where
+  mult (Pair l1 r1) (Pair l2 r2) = Pair (mult l1 l2) (mult r1 r2)
+  {-# INLINE mult #-}
+instance (GenericSumProfunctor p, GenericSumProfunctor q) => GenericSumProfunctor (Product p q) where
+  plus (Pair l1 r1) (Pair l2 r2) = Pair (plus l1 l2) (plus r1 r2)
+  {-# INLINE plus #-}
+instance (GenericEmptyProfunctor p, GenericEmptyProfunctor q) => GenericEmptyProfunctor (Product p q) where
+  zero = Pair zero zero
+  {-# INLINE zero #-}
+  identity = Pair identity identity
+  {-# INLINE identity #-}
+
+instance (Applicative f, GenericUnitProfunctor p) => GenericUnitProfunctor (Tannen f p) where
+  unit = Tannen (pure unit)
+  {-# INLINE unit #-}
+instance (Applicative f, GenericProductProfunctor p) => GenericProductProfunctor (Tannen f p) where
+  mult (Tannen l) (Tannen r) = Tannen $ liftA2 mult l r
+  {-# INLINE mult #-}
+instance (Applicative f, GenericSumProfunctor p) => GenericSumProfunctor (Tannen f p) where
+  plus (Tannen l) (Tannen r) = Tannen $ liftA2 plus l r
+  {-# INLINE plus #-}
+instance (Applicative f, GenericEmptyProfunctor p) => GenericEmptyProfunctor (Tannen f p) where
+  zero = Tannen (pure zero)
+  {-# INLINE zero #-}
+  identity = Tannen (pure identity)
+  {-# INLINE identity #-}
+
+
+newtype Zip f a b = Zip { runZip :: a -> a -> f b }
+instance Functor f => Profunctor (Zip f) where
+  dimap f g (Zip h) = Zip $ \a1 a2 -> fmap g (h (f a1) (f a2))
+  {-# INLINE dimap #-}
+instance Applicative f => GenericUnitProfunctor (Zip f) where
+  unit = Zip $ \_ _ -> pure U1
+  {-# INLINE unit #-}
+instance Applicative f => GenericProductProfunctor (Zip f) where
+  mult (Zip f) (Zip g) = Zip $ \(al :*: ar) (bl :*: br) -> (:*:) <$> f al bl <*> g ar br
+  {-# INLINE mult #-}
+instance Alternative f => GenericSumProfunctor (Zip f) where
+  plus (Zip f) (Zip g) = Zip h where
+    h (L1 a) (L1 b) = fmap L1 (f a b)
+    h (R1 a) (R1 b) = fmap R1 (g a b)
+    h _ _ = empty
+  {-# INLINE plus #-}
+instance Alternative f => GenericEmptyProfunctor (Zip f) where
+  zero = Zip absurd
+  {-# INLINE zero #-}
+  identity = Zip $ \_ _ -> empty
+  {-# INLINE identity #-}
+
+
+absurd :: V1 a -> b
+absurd = \case {}
+{-# INLINE absurd #-}
+
+e1 :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b
+e1 f _ (L1 l) = f l
+e1 _ f (R1 r) = f r
+{-# INLINE e1 #-}
+
+fst1 :: (f :*: g) a -> f a
+fst1 (l :*: _) = l
+{-# INLINE fst1 #-}
+snd1 :: (f :*: g) a -> g a
+snd1 (_ :*: r) = r
+{-# INLINE snd1 #-}
diff --git a/src/Generics/OneLiner/Internal.hs b/src/Generics/OneLiner/Internal.hs
--- a/src/Generics/OneLiner/Internal.hs
+++ b/src/Generics/OneLiner/Internal.hs
@@ -11,10 +11,8 @@
 {-# LANGUAGE
     GADTs
   , DataKinds
-  , EmptyCase
   , PolyKinds
   , RankNTypes
-  , LambdaCase
   , TypeFamilies
   , TypeOperators
   , ConstraintKinds
@@ -30,38 +28,30 @@
 
 import GHC.Generics
 import GHC.Types (Constraint)
-import Control.Applicative
-import Data.Bifunctor.Biff
-import Data.Bifunctor.Clown
-import Data.Bifunctor.Joker
-import Data.Bifunctor.Product
-import Data.Bifunctor.Tannen
-import Data.Functor.Contravariant.Divisible
-import Data.Functor.Compose
-import Data.Functor.Identity
 import Data.Profunctor
 import Data.Proxy
-import Data.Tagged
+import Data.Functor.Identity
 
+import Generics.OneLiner.Classes
 
-type family Constraints' (t :: * -> *) (c :: * -> Constraint) (c1 :: (* -> *) -> Constraint) :: Constraint
-type instance Constraints' V1 c c1 = ()
-type instance Constraints' U1 c c1 = ()
-type instance Constraints' (f :+: g) c c1 = (Constraints' f c c1, Constraints' g c c1)
-type instance Constraints' (f :*: g) c c1 = (Constraints' f c c1, Constraints' g c c1)
-type instance Constraints' (f :.: g) c c1 = (c1 f, Constraints' g c c1)
-type instance Constraints' Par1 c c1 = ()
-type instance Constraints' (Rec1 f) c c1 = c1 f
-type instance Constraints' (K1 i a) c c1 = c a
-type instance Constraints' (M1 i t f) c c1 = Constraints' f c c1
+type family Constraints' (t :: * -> *) (t' :: * -> *) (c :: * -> * -> Constraint) (c1 :: (* -> *) -> (* -> *) -> Constraint) :: Constraint
+type instance Constraints' V1 V1 c c1 = ()
+type instance Constraints' U1 U1 c c1 = ()
+type instance Constraints' (f :+: g) (f' :+: g') c c1 = (Constraints' f f' c c1, Constraints' g g' c c1)
+type instance Constraints' (f :*: g) (f' :*: g') c c1 = (Constraints' f f' c c1, Constraints' g g' c c1)
+type instance Constraints' (f :.: g) (f' :.: g') c c1 = (c1 f f', Constraints' g g' c c1)
+type instance Constraints' Par1 Par1 c c1 = ()
+type instance Constraints' (Rec1 f) (Rec1 g) c c1 = c1 f g
+type instance Constraints' (K1 i a) (K1 i' b) c c1 = c a b
+type instance Constraints' (M1 i t f) (M1 i' t' f') c c1 = Constraints' f f' c c1
 
 type ADT' = ADT_ Identity Proxy ADTProfunctor
 type ADTNonEmpty' = ADT_ Identity Proxy NonEmptyProfunctor
 type ADTRecord' = ADT_ Identity Proxy RecordProfunctor
 
-type ADT1' t = (ADT_ Identity Identity ADTProfunctor t, ADT_ Proxy Identity ADTProfunctor t)
-type ADTNonEmpty1' t = (ADT_ Identity Identity NonEmptyProfunctor t, ADT_ Proxy Identity NonEmptyProfunctor t)
-type ADTRecord1' t = (ADT_ Identity Identity RecordProfunctor t, ADT_ Proxy Identity RecordProfunctor t)
+type ADT1' t t' = (ADT_ Identity Identity ADTProfunctor t t', ADT_ Proxy Identity ADTProfunctor t t')
+type ADTNonEmpty1' t t' = (ADT_ Identity Identity NonEmptyProfunctor t t', ADT_ Proxy Identity NonEmptyProfunctor t t')
+type ADTRecord1' t t' = (ADT_ Identity Identity RecordProfunctor t t', ADT_ Proxy Identity RecordProfunctor t t')
 
 type ADTProfunctor = GenericEmptyProfunctor ': NonEmptyProfunctor
 type NonEmptyProfunctor = GenericSumProfunctor ': RecordProfunctor
@@ -82,253 +72,92 @@
   _ |- _ = id
   {-# INLINE (|-) #-}
 
-generic' :: forall t c p ks a b proxy0 for. (ADT_ Identity Proxy ks t, Constraints' t c AnyType, Satisfies p ks)
+generic' :: forall t t' c p ks a b proxy0 for. (ADT_ Identity Proxy ks t t', Constraints' t t' c AnyType, Satisfies p ks)
          => proxy0 ks
          -> for c
-         -> (forall s. c s => p s s)
-         -> p (t a) (t b)
+         -> (forall s s'. c s s' => p s s')
+         -> p (t a) (t' b)
 generic' proxy0 for f = generic_ proxy0 (Proxy :: Proxy Identity) for (Identity f) (Proxy :: Proxy AnyType) Proxy Proxy
 {-# INLINE generic' #-}
 
-generic1' :: forall t c1 p ks a b proxy0 for. (ADT_ Proxy Identity ks t, Constraints' t AnyType c1, Satisfies p ks)
+generic1' :: forall t t' c1 p ks a b proxy0 for. (ADT_ Proxy Identity ks t t', Constraints' t t' AnyType c1, Satisfies p ks)
            => proxy0 ks
            -> for c1
-           -> (forall s d e. c1 s => p d e -> p (s d) (s e))
+           -> (forall s s' d e. c1 s s' => p d e -> p (s d) (s' e))
            -> p a b
-           -> p (t a) (t b)
+           -> p (t a) (t' b)
 generic1' proxy0 for f p = generic_ proxy0 (Proxy :: Proxy Proxy) (Proxy :: Proxy AnyType) Proxy for (Identity f) (Identity p)
 {-# INLINE generic1' #-}
 
-generic01' :: forall t c0 c1 p ks a b proxy0 for for1. (ADT_ Identity Identity ks t, Constraints' t c0 c1, Satisfies p ks)
+generic01' :: forall t t' c0 c1 p ks a b proxy0 for for1. (ADT_ Identity Identity ks t t', Constraints' t t' c0 c1, Satisfies p ks)
           => proxy0 ks
           -> for c0
-          -> (forall s. c0 s => p s s)
+          -> (forall s s'. c0 s s' => p s s')
           -> for1 c1
-          -> (forall s d e. c1 s => p d e -> p (s d) (s e))
+          -> (forall s s' d e. c1 s s' => p d e -> p (s d) (s' e))
           -> p a b
-          -> p (t a) (t b)
+          -> p (t a) (t' b)
 generic01' proxy0 for0 k for1 f p = generic_ proxy0 (Proxy :: Proxy Identity) for0 (Identity k) for1 (Identity f) (Identity p)
 {-# INLINE generic01' #-}
 
-class ADT_ (nullary :: * -> *) (unary :: * -> *) (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) where
-  generic_ :: (Constraints' t c c1, Satisfies p ks)
+class ADT_ (nullary :: * -> *) (unary :: * -> *) (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) (t' :: * -> *) where
+  generic_ :: (Constraints' t t' c c1, Satisfies p ks)
            => proxy0 ks
            -> proxy1 nullary
            -> for c
-           -> (forall s. c s => nullary (p s s))
+           -> (forall s s'. c s s' => nullary (p s s'))
            -> for1 c1
-           -> (forall s1 d e. c1 s1 => unary (p d e -> p (s1 d) (s1 e)))
+           -> (forall r1 s1 d e. c1 r1 s1 => unary (p d e -> p (r1 d) (s1 e)))
            -> unary (p a b)
-           -> p (t a) (t b)
+           -> p (t a) (t' b)
 
-instance ks |- GenericEmptyProfunctor => ADT_ nullary unary ks V1 where
+instance ks |- GenericEmptyProfunctor => ADT_ nullary unary ks V1 V1 where
   generic_ proxy0 _ _ _ _ _ _ = (proxy0 |- (Proxy :: Proxy GenericEmptyProfunctor)) zero
   {-# INLINE generic_ #-}
 
-instance ks |- GenericUnitProfunctor => ADT_ nullary unary ks U1 where
+instance ks |- GenericUnitProfunctor => ADT_ nullary unary ks U1 U1 where
   generic_ proxy0 _ _ _ _ _ _ = (proxy0 |- (Proxy :: Proxy GenericUnitProfunctor)) unit
   {-# INLINE generic_ #-}
 
-instance (ks |- GenericSumProfunctor, ADT_ nullary unary ks f, ADT_ nullary unary ks g) => ADT_ nullary unary ks (f :+: g) where
+instance (ks |- GenericSumProfunctor, ADT_ nullary unary ks f f', ADT_ nullary unary ks g g') => ADT_ nullary unary ks (f :+: g) (f' :+: g') where
   generic_ proxy0 proxy1 for f for1 f1 p1 = (proxy0 |- (Proxy :: Proxy GenericSumProfunctor))
     (plus (generic_ proxy0 proxy1 for f for1 f1 p1) (generic_ proxy0 proxy1 for f for1 f1 p1))
   {-# INLINE generic_ #-}
 
-instance (ks |- GenericProductProfunctor, ADT_ nullary unary ks f, ADT_ nullary unary ks g) => ADT_ nullary unary ks (f :*: g) where
+instance (ks |- GenericProductProfunctor, ADT_ nullary unary ks f f', ADT_ nullary unary ks g g') => ADT_ nullary unary ks (f :*: g) (f' :*: g') where
   generic_ proxy0 proxy1 for f for1 f1 p1 = (proxy0 |- (Proxy :: Proxy GenericProductProfunctor))
     (mult (generic_ proxy0 proxy1 for f for1 f1 p1) (generic_ proxy0 proxy1 for f for1 f1 p1))
   {-# INLINE generic_ #-}
 
-instance ks |- Profunctor => ADT_ Identity unary ks (K1 i v) where
+instance ks |- Profunctor => ADT_ Identity unary ks (K1 i v) (K1 i' v') where
   generic_ proxy0 _ _ f _ _ _ = (proxy0 |- (Proxy :: Proxy Profunctor)) (dimap unK1 K1 (runIdentity f))
   {-# INLINE generic_ #-}
 
-instance ks |- GenericEmptyProfunctor => ADT_ Proxy unary ks (K1 i v) where
+instance ks |- GenericEmptyProfunctor => ADT_ Proxy unary ks (K1 i v) (K1 i' v) where
   generic_ proxy0 _ _ _ _ _ _ = (proxy0 |- (Proxy :: Proxy GenericEmptyProfunctor)) (dimap unK1 K1 identity)
   {-# INLINE generic_ #-}
 
-instance (ks |- Profunctor, ADT_ nullary unary ks f) => ADT_ nullary unary ks (M1 i c f) where
+instance (ks |- Profunctor, ADT_ nullary unary ks f f') => ADT_ nullary unary ks (M1 i c f) (M1 i' c' f') where
   generic_ proxy0 proxy1 for f for1 f1 p1 = (proxy0 |- (Proxy :: Proxy Profunctor))
     (dimap unM1 M1 (generic_ proxy0 proxy1 for f for1 f1 p1))
   {-# INLINE generic_ #-}
 
-instance (ks |- Profunctor, ADT_ nullary Identity ks g) => ADT_ nullary Identity ks (f :.: g) where
+instance (ks |- Profunctor, ADT_ nullary Identity ks g g') => ADT_ nullary Identity ks (f :.: g) (f' :.: g') where
   generic_ proxy0 proxy1 for f for1 f1 p1 = (proxy0 |- (Proxy :: Proxy Profunctor))
     (dimap unComp1 Comp1 $ runIdentity f1 (generic_ proxy0 proxy1 for f for1 f1 p1))
   {-# INLINE generic_ #-}
 
-instance ks |- Profunctor => ADT_ nullary Identity ks Par1 where
+instance ks |- Profunctor => ADT_ nullary Identity ks Par1 Par1 where
   generic_ proxy0 _ _ _ _ _ p = (proxy0 |- (Proxy :: Proxy Profunctor))
     (dimap unPar1 Par1 (runIdentity p))
   {-# INLINE generic_ #-}
 
-instance ks |- Profunctor => ADT_ nullary Identity ks (Rec1 f) where
+instance ks |- Profunctor => ADT_ nullary Identity ks (Rec1 f) (Rec1 f') where
   generic_ proxy0 _ _ _ _ f p = (proxy0 |- (Proxy :: Proxy Profunctor))
     (dimap unRec1 Rec1 (runIdentity (f <*> p)))
   {-# INLINE generic_ #-}
 
-absurd :: V1 a -> b
-absurd = \case {}
-{-# INLINE absurd #-}
 
-e1 :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b
-e1 f _ (L1 l) = f l
-e1 _ f (R1 r) = f r
-{-# INLINE e1 #-}
-
-fst1 :: (f :*: g) a -> f a
-fst1 (l :*: _) = l
-{-# INLINE fst1 #-}
-snd1 :: (f :*: g) a -> g a
-snd1 (_ :*: r) = r
-{-# INLINE snd1 #-}
-
-class Profunctor p => GenericUnitProfunctor p where
-  unit :: p (U1 a) (U1 a')
-
-class Profunctor p => GenericProductProfunctor p where
-  mult :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :*: g) a) ((f' :*: g') a')
-
-class Profunctor p => GenericSumProfunctor p where
-  plus :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :+: g) a) ((f' :+: g') a')
-
-class Profunctor p => GenericEmptyProfunctor p where
-  identity :: p a a
-  zero :: p (V1 a) (V1 a')
-
--- | A generic function using a `GenericRecordProfunctor` works on any data type
--- with exactly one constructor, a.k.a. records,
--- with multiple fields (`mult`) or no fields (`unit`).
---
--- `GenericRecordProfunctor` is similar to `ProductProfuctor` from the
--- product-profunctor package, but using types from GHC.Generics.
-class (Profunctor p, GenericUnitProfunctor p, GenericProductProfunctor p) => GenericRecordProfunctor p
-instance (Profunctor p, GenericUnitProfunctor p, GenericProductProfunctor p) => GenericRecordProfunctor p
-
--- | A generic function using a `GenericNonEmptyProfunctor` works on any data
--- type with at least one constructor.
-class (GenericRecordProfunctor p, GenericSumProfunctor p) => GenericNonEmptyProfunctor p where
-instance (GenericRecordProfunctor p, GenericSumProfunctor p) => GenericNonEmptyProfunctor p where
-
--- | A generic function using a `GenericProfunctor` works on any
--- algebraic data type, including those with no constructors and constants.
-class (GenericNonEmptyProfunctor p, GenericEmptyProfunctor p) => GenericProfunctor p where
-instance (GenericNonEmptyProfunctor p, GenericEmptyProfunctor p) => GenericProfunctor p where
-
-instance GenericUnitProfunctor (->) where
-  unit _ = U1
-  {-# INLINE unit #-}
-instance GenericProductProfunctor (->) where
-  mult f g (l :*: r) = f l :*: g r
-  {-# INLINE mult #-}
-instance GenericSumProfunctor (->) where
-  plus f g = e1 (L1 . f) (R1 . g)
-  {-# INLINE plus #-}
-instance GenericEmptyProfunctor (->) where
-  zero = absurd
-  {-# INLINE zero #-}
-  identity = id
-  {-# INLINE identity #-}
-
-instance GenericUnitProfunctor Tagged where
-  unit = Tagged U1
-  {-# INLINE unit #-}
-instance GenericProductProfunctor Tagged where
-  mult (Tagged l) (Tagged r) = Tagged $ l :*: r
-  {-# INLINE mult #-}
-
-instance Applicative f => GenericUnitProfunctor (Star f) where
-  unit = Star $ \_ -> pure U1
-  {-# INLINE unit #-}
-instance Applicative f => GenericProductProfunctor (Star f) where
-  mult (Star f) (Star g) = Star $ \(l :*: r) -> (:*:) <$> f l <*> g r
-  {-# INLINE mult #-}
-instance Applicative f => GenericSumProfunctor (Star f) where
-  plus (Star f) (Star g) = Star $ e1 (fmap L1 . f) (fmap R1 . g)
-  {-# INLINE plus #-}
-instance Applicative f => GenericEmptyProfunctor (Star f) where
-  zero = Star absurd
-  {-# INLINE zero #-}
-  identity = Star pure
-  {-# INLINE identity #-}
-
-instance Functor f => GenericUnitProfunctor (Costar f) where
-  unit = Costar $ const U1
-  {-# INLINE unit #-}
-instance Functor f => GenericProductProfunctor (Costar f) where
-  mult (Costar f) (Costar g) = Costar $ \lr -> f (fst1 <$> lr) :*: g (snd1 <$> lr)
-  {-# INLINE mult #-}
-
-instance (Functor f, Applicative g, Profunctor p, GenericUnitProfunctor p) => GenericUnitProfunctor (Biff p f g) where
-  unit = Biff $ dimap (const U1) pure unit
-  {-# INLINE unit #-}
-instance (Functor f, Applicative g, Profunctor p, GenericProductProfunctor p) => GenericProductProfunctor (Biff p f g) where
-  mult (Biff f) (Biff g) = Biff $ dimap
-    (liftA2 (:*:) (Compose . fmap fst1) (Compose . fmap snd1))
-    (\(Compose l :*: Compose r) -> liftA2 (:*:) l r)
-    (mult (dimap getCompose Compose f) (dimap getCompose Compose g))
-  {-# INLINE mult #-}
-
-instance Applicative f => GenericUnitProfunctor (Joker f) where
-  unit = Joker $ pure U1
-  {-# INLINE unit #-}
-instance Applicative f => GenericProductProfunctor (Joker f) where
-  mult (Joker l) (Joker r) = Joker $ (:*:) <$> l <*> r
-  {-# INLINE mult #-}
-instance Alternative f => GenericSumProfunctor (Joker f) where
-  plus (Joker l) (Joker r) = Joker $ L1 <$> l <|> R1 <$> r
-  {-# INLINE plus #-}
-instance Alternative f => GenericEmptyProfunctor (Joker f) where
-  zero = Joker empty
-  {-# INLINE zero #-}
-  identity = Joker empty
-  {-# INLINE identity #-}
-
-instance Divisible f => GenericUnitProfunctor (Clown f) where
-  unit = Clown conquer
-  {-# INLINE unit #-}
-instance Divisible f => GenericProductProfunctor (Clown f) where
-  mult (Clown f) (Clown g) = Clown $ divide (\(l :*: r) -> (l, r)) f g
-  {-# INLINE mult #-}
-instance Decidable f => GenericSumProfunctor (Clown f) where
-  plus (Clown f) (Clown g) = Clown $ choose (e1 Left Right) f g
-  {-# INLINE plus #-}
-instance Decidable f => GenericEmptyProfunctor (Clown f) where
-  zero = Clown $ lose absurd
-  {-# INLINE zero #-}
-  identity = Clown conquer
-  {-# INLINE identity #-}
-
-instance (GenericUnitProfunctor p, GenericUnitProfunctor q) => GenericUnitProfunctor (Product p q) where
-  unit = Pair unit unit
-  {-# INLINE unit #-}
-instance (GenericProductProfunctor p, GenericProductProfunctor q) => GenericProductProfunctor (Product p q) where
-  mult (Pair l1 r1) (Pair l2 r2) = Pair (mult l1 l2) (mult r1 r2)
-  {-# INLINE mult #-}
-instance (GenericSumProfunctor p, GenericSumProfunctor q) => GenericSumProfunctor (Product p q) where
-  plus (Pair l1 r1) (Pair l2 r2) = Pair (plus l1 l2) (plus r1 r2)
-  {-# INLINE plus #-}
-instance (GenericEmptyProfunctor p, GenericEmptyProfunctor q) => GenericEmptyProfunctor (Product p q) where
-  zero = Pair zero zero
-  {-# INLINE zero #-}
-  identity = Pair identity identity
-  {-# INLINE identity #-}
-
-instance (Applicative f, GenericUnitProfunctor p) => GenericUnitProfunctor (Tannen f p) where
-  unit = Tannen (pure unit)
-  {-# INLINE unit #-}
-instance (Applicative f, GenericProductProfunctor p) => GenericProductProfunctor (Tannen f p) where
-  mult (Tannen l) (Tannen r) = Tannen $ liftA2 mult l r
-  {-# INLINE mult #-}
-instance (Applicative f, GenericSumProfunctor p) => GenericSumProfunctor (Tannen f p) where
-  plus (Tannen l) (Tannen r) = Tannen $ liftA2 plus l r
-  {-# INLINE plus #-}
-instance (Applicative f, GenericEmptyProfunctor p) => GenericEmptyProfunctor (Tannen f p) where
-  zero = Tannen (pure zero)
-  {-# INLINE zero #-}
-  identity = Tannen (pure identity)
-  {-# INLINE identity #-}
-
 data Ctor a b = Ctor { index :: a -> Int, count :: Int }
 instance Profunctor Ctor where
   dimap l _ (Ctor i c) = Ctor (i . l) c
@@ -348,96 +177,78 @@
   identity = Ctor (const 0) 1
   {-# INLINE identity #-}
 
-record :: forall c p t. (ADTRecord t, Constraints t c, GenericRecordProfunctor p)
-       => (forall s. c s => p s s) -> p t t
+record :: forall c p t t'. (ADTRecord t t', Constraints t t' c, GenericRecordProfunctor p)
+       => (forall s s'. c s s' => p s s') -> p t t'
 record f = dimap from to $ generic' (Proxy :: Proxy RecordProfunctor) (Proxy :: Proxy c) f
 {-# INLINE record #-}
 
-record1 :: forall c p t a b. (ADTRecord1 t, Constraints1 t c, GenericRecordProfunctor p)
-        => (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+record1 :: forall c p t t' a b. (ADTRecord1 t t', Constraints1 t t' c, GenericRecordProfunctor p)
+        => (forall d e s s'. c s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
 record1 f p = dimap from1 to1 $ generic1' (Proxy :: Proxy RecordProfunctor) (Proxy :: Proxy c) f p
 {-# INLINE record1 #-}
 
-record01 :: forall c0 c1 p t a b. (ADTRecord1 t, Constraints01 t c0 c1, GenericRecordProfunctor p)
-         => (forall s. c0 s => p s s) -> (forall d e s. c1 s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+record01 :: forall c0 c1 p t t' a b. (ADTRecord1 t t', Constraints01 t t' c0 c1, GenericRecordProfunctor p)
+         => (forall s s'. c0 s s' => p s s') -> (forall d e s s'. c1 s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
 record01 k f p = dimap from1 to1 $ generic01' (Proxy :: Proxy RecordProfunctor) (Proxy :: Proxy c0) k (Proxy :: Proxy c1) f p
 {-# INLINE record01 #-}
 
-nonEmpty :: forall c p t. (ADTNonEmpty t, Constraints t c, GenericNonEmptyProfunctor p)
-         => (forall s. c s => p s s) -> p t t
+nonEmpty :: forall c p t t'. (ADTNonEmpty t t', Constraints t t' c, GenericNonEmptyProfunctor p)
+         => (forall s s'. c s s' => p s s') -> p t t'
 nonEmpty f = dimap from to $ generic' (Proxy :: Proxy NonEmptyProfunctor) (Proxy :: Proxy c) f
 {-# INLINE nonEmpty #-}
 
-nonEmpty1 :: forall c p t a b. (ADTNonEmpty1 t, Constraints1 t c, GenericNonEmptyProfunctor p)
-          => (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+nonEmpty1 :: forall c p t t' a b. (ADTNonEmpty1 t t', Constraints1 t t' c, GenericNonEmptyProfunctor p)
+          => (forall d e s s'. c s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
 nonEmpty1 f p = dimap from1 to1 $ generic1' (Proxy :: Proxy NonEmptyProfunctor) (Proxy :: Proxy c) f p
 {-# INLINE nonEmpty1 #-}
 
-nonEmpty01 :: forall c0 c1 p t a b. (ADTNonEmpty1 t, Constraints01 t c0 c1, GenericNonEmptyProfunctor p)
-           => (forall s. c0 s => p s s) -> (forall d e s. c1 s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+nonEmpty01 :: forall c0 c1 p t t' a b. (ADTNonEmpty1 t t', Constraints01 t t' c0 c1, GenericNonEmptyProfunctor p)
+           => (forall s s'. c0 s s' => p s s') -> (forall d e s s'. c1 s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
 nonEmpty01 k f p = dimap from1 to1 $ generic01' (Proxy :: Proxy NonEmptyProfunctor) (Proxy :: Proxy c0) k (Proxy :: Proxy c1) f p
 {-# INLINE nonEmpty01 #-}
 
-generic :: forall c p t. (ADT t, Constraints t c, GenericProfunctor p)
-        => (forall s. c s => p s s) -> p t t
+generic :: forall c p t t'. (ADT t t', Constraints t t' c, GenericProfunctor p)
+        => (forall s s'. c s s' => p s s') -> p t t'
 generic f = dimap from to $ generic' (Proxy :: Proxy ADTProfunctor) (Proxy :: Proxy c) f
 {-# INLINE generic #-}
 
-generic1 :: forall c p t a b. (ADT1 t, Constraints1 t c, GenericProfunctor p)
-         => (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+generic1 :: forall c p t t' a b. (ADT1 t t', Constraints1 t t' c, GenericProfunctor p)
+         => (forall d e s s'. c s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
 generic1 f p = dimap from1 to1 $ generic1' (Proxy :: Proxy ADTProfunctor) (Proxy :: Proxy c) f p
 {-# INLINE generic1 #-}
 
-generic01 :: forall c0 c1 p t a b. (ADT1 t, Constraints01 t c0 c1, GenericProfunctor p)
-          => (forall s. c0 s => p s s) -> (forall d e s. c1 s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+generic01 :: forall c0 c1 p t t' a b. (ADT1 t t', Constraints01 t t' c0 c1, GenericProfunctor p)
+          => (forall s s'. c0 s s' => p s s') -> (forall d e s s'. c1 s s' => p d e -> p (s d) (s' e)) -> p a b -> p (t a) (t' b)
 generic01 k f p = dimap from1 to1 $ generic01' (Proxy :: Proxy ADTProfunctor) (Proxy :: Proxy c0) k (Proxy :: Proxy c1) f p
 {-# INLINE generic01 #-}
 
 -- | `Constraints` is a constraint type synonym, containing the constraint
 -- requirements for an instance for `t` of class `c`.
 -- It requires an instance of class `c` for each component of `t`.
-type Constraints t c = Constraints' (Rep t) c AnyType
+type Constraints t t' c = Constraints' (Rep t) (Rep t') c AnyType
 
-type Constraints1 t c = Constraints' (Rep1 t) AnyType c
+type Constraints1 t t' c = Constraints' (Rep1 t) (Rep1 t') AnyType c
 
-type Constraints01 t c0 c1 = Constraints' (Rep1 t) c0 c1
+type Constraints01 t t' c0 c1 = Constraints' (Rep1 t) (Rep1 t') c0 c1
 
 -- | `ADTRecord` is a constraint type synonym. An instance is an `ADT` with *exactly* one constructor.
-type ADTRecord t = (Generic t, ADTRecord' (Rep t), Constraints t AnyType)
+type ADTRecord t t' = (Generic t, Generic t', ADTRecord' (Rep t) (Rep t'), Constraints t t' AnyType)
 
-type ADTRecord1 t = (Generic1 t, ADTRecord1' (Rep1 t), Constraints1 t AnyType)
+type ADTRecord1 t t' = (Generic1 t, Generic1 t', ADTRecord1' (Rep1 t) (Rep1 t'), Constraints1 t t' AnyType)
 
 -- | `ADTNonEmpty` is a constraint type synonym. An instance is an `ADT` with *at least* one constructor.
-type ADTNonEmpty t = (Generic t, ADTNonEmpty' (Rep t), Constraints t AnyType)
+type ADTNonEmpty t t' = (Generic t, Generic t', ADTNonEmpty' (Rep t) (Rep t'), Constraints t t' AnyType)
 
-type ADTNonEmpty1 t = (Generic1 t, ADTNonEmpty1' (Rep1 t), Constraints1 t AnyType)
+type ADTNonEmpty1 t t' = (Generic1 t, Generic1 t', ADTNonEmpty1' (Rep1 t) (Rep1 t'), Constraints1 t t' AnyType)
 
 -- | `ADT` is a constraint type synonym. The `Generic` instance can be derived,
 -- and any generic representation will be an instance of `ADT'` and `AnyType`.
-type ADT t = (Generic t, ADT' (Rep t), Constraints t AnyType)
-
-type ADT1 t = (Generic1 t, ADT1' (Rep1 t), Constraints1 t AnyType)
-
--- | Get the index in the lists returned by `create` and `createA` of the constructor of the given value.
---
--- For example, this is the implementation of `put` that generates the binary data that
--- the above implentation of `get` expects:
---
--- @
--- `put` t = `putWord8` (`toEnum` (`ctorIndex` t)) `<>` `gfoldMap` \@`Binary` `put` t
--- @
-ctorIndex :: ADT t => t -> Int
-ctorIndex = index $ generic @AnyType (Ctor (const 0) 1)
-{-# INLINE ctorIndex #-}
+type ADT t t' = (Generic t, Generic t', ADT' (Rep t) (Rep t'), Constraints t t' AnyType)
 
-ctorIndex1 :: ADT1 t => t a -> Int
-ctorIndex1 = index $ generic1 @AnyType (const $ Ctor (const 0) 1) (Ctor (const 0) 1)
-{-# INLINE ctorIndex1 #-}
+type ADT1 t t' = (Generic1 t, Generic1 t', ADT1' (Rep1 t) (Rep1 t'), Constraints1 t t' AnyType)
 
--- | Any type is instance of `AnyType`, you can use it with @\@`AnyType`@
--- if you don't actually need a class constraint.
-class AnyType (a :: k)
-instance AnyType (a :: k)
+class AnyType a b
+instance AnyType a b
 
 -- | The result type of a curried function.
 --
@@ -475,3 +286,15 @@
 instance FunResult r ~ r => FunConstraints c r where
   autoApply _run r = r
   {-# INLINE autoApply #-}
+
+
+data Pair a = Pair a a
+instance Functor Pair where
+  fmap f (Pair a b) = Pair (f a) (f b)
+  {-# INLINE fmap #-}
+  
+infixr 9 .:
+(.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
+(.:) = (.) . (.)
+{-# INLINE (.:) #-}
+
diff --git a/src/Generics/OneLiner/Internal/Unary.hs b/src/Generics/OneLiner/Internal/Unary.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/OneLiner/Internal/Unary.hs
@@ -0,0 +1,114 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.OneLiner.Internal.Unary
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  sjoerd@w3future.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-----------------------------------------------------------------------------
+{-# LANGUAGE
+    PolyKinds
+  , RankNTypes
+  , TypeFamilies
+  , ConstraintKinds
+  , FlexibleContexts
+  , TypeApplications
+  , FlexibleInstances
+  , AllowAmbiguousTypes
+  , ScopedTypeVariables
+  , MultiParamTypeClasses
+  , UndecidableSuperClasses
+  #-}
+module Generics.OneLiner.Internal.Unary where
+
+import Data.Kind (Constraint)
+import Generics.OneLiner.Classes
+import qualified Generics.OneLiner.Internal as I
+
+-- | Type-level 'join', of kind @(k -> k -> k') -> k -> k'@.
+type J f a = f a a
+
+-- | Constraint-level 'duplicate', of kind @(k -> Constraint) -> k -> k -> Constraint@.
+class (c a, a ~ b) => D (c :: k -> Constraint) a b
+instance (c a, a ~ b) => D c a b
+
+type Constraints t c = I.Constraints t t (D c)
+type Constraints1 t c = I.Constraints1 t t (D c)
+type Constraints01 t c0 c1 = I.Constraints01 t t (D c0) (D c1)
+type Constraints' t c c1 = I.Constraints' t t (D c) (D c1)
+
+type ADTRecord t = (I.ADTRecord t t, Constraints t AnyType)
+type ADTRecord1 t = (I.ADTRecord1 t t, Constraints1 t AnyType)
+type ADTNonEmpty t = (I.ADTNonEmpty t t, Constraints t AnyType)
+type ADTNonEmpty1 t = (I.ADTNonEmpty1 t t, Constraints1 t AnyType)
+type ADT t = (I.ADT t t, Constraints t AnyType)
+type ADT1 t = (I.ADT1 t t, Constraints1 t AnyType)
+
+record :: forall c p t. (ADTRecord t, Constraints t c, GenericRecordProfunctor p)
+       => (forall s. c s => p s s) -> p t t
+record = I.record @(D c)
+{-# INLINE record #-}
+
+record1 :: forall c p t a b. (ADTRecord1 t, Constraints1 t c, GenericRecordProfunctor p)
+        => (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+record1 = I.record1 @(D c)
+{-# INLINE record1 #-}
+
+record01 :: forall c0 c1 p t a b. (ADTRecord1 t, Constraints01 t c0 c1, GenericRecordProfunctor p)
+         => (forall s. c0 s => p s s) -> (forall d e s. c1 s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+record01 = I.record01 @(D c0) @(D c1)
+{-# INLINE record01 #-}
+
+nonEmpty :: forall c p t. (ADTNonEmpty t, Constraints t c, GenericNonEmptyProfunctor p)
+         => (forall s. c s => p s s) -> p t t
+nonEmpty = I.nonEmpty @(D c)
+{-# INLINE nonEmpty #-}
+
+nonEmpty1 :: forall c p t a b. (ADTNonEmpty1 t, Constraints1 t c, GenericNonEmptyProfunctor p)
+          => (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+nonEmpty1 = I.nonEmpty1 @(D c)
+{-# INLINE nonEmpty1 #-}
+
+nonEmpty01 :: forall c0 c1 p t a b. (ADTNonEmpty1 t, Constraints01 t c0 c1, GenericNonEmptyProfunctor p)
+           => (forall s. c0 s => p s s) -> (forall d e s. c1 s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+nonEmpty01 = I.nonEmpty01 @(D c0) @(D c1)
+{-# INLINE nonEmpty01 #-}
+
+generic :: forall c p t. (ADT t, Constraints t c, GenericProfunctor p)
+        => (forall s. c s => p s s) -> p t t
+generic = I.generic @(D c) @p @t @t
+{-# INLINE generic #-}
+
+generic1 :: forall c p t a b. (ADT1 t, Constraints1 t c, GenericProfunctor p)
+         => (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+generic1 = I.generic1 @(D c) @p @t @t
+{-# INLINE generic1 #-}
+
+generic01 :: forall c0 c1 p t a b. (ADT1 t, Constraints01 t c0 c1, GenericProfunctor p)
+          => (forall s. c0 s => p s s) -> (forall d e s. c1 s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+generic01 = I.generic01 @(D c0) @(D c1)
+{-# INLINE generic01 #-}
+
+-- | Get the index in the lists returned by `create` and `createA` of the constructor of the given value.
+--
+-- For example, this is the implementation of `put` that generates the binary data that
+-- the above implentation of `get` expects:
+--
+-- @
+-- `put` t = `putWord8` (`toEnum` (`ctorIndex` t)) `<>` `gfoldMap` \@`Binary` `put` t
+-- @
+ctorIndex :: forall t. ADT t => t -> Int
+ctorIndex = I.index $ I.generic @I.AnyType @_ @t @t (I.Ctor (const 0) 1)
+{-# INLINE ctorIndex #-}
+
+ctorIndex1 :: forall t a. ADT1 t => t a -> Int
+ctorIndex1 = I.index $ I.generic1 @I.AnyType @_ @t @t (const $ I.Ctor (const 0) 1) (I.Ctor (const 0) 1)
+{-# INLINE ctorIndex1 #-}
+
+-- | Any type is instance of `AnyType`, you can use it with @\@`AnyType`@
+-- if you don't actually need a class constraint.
+class AnyType (a :: k)
+instance AnyType (a :: k)
+