diff --git a/examples/defaultsignature.hs b/examples/defaultsignature.hs
--- a/examples/defaultsignature.hs
+++ b/examples/defaultsignature.hs
@@ -1,4 +1,11 @@
-{-# LANGUAGE DeriveGeneric, DefaultSignatures, ConstraintKinds, TypeOperators, FlexibleContexts #-}
+{-# LANGUAGE
+  TypeOperators,
+  DeriveGeneric,
+  DeriveAnyClass,
+  ConstraintKinds,
+  FlexibleContexts,
+  DefaultSignatures 
+  #-}
 
 import GHC.Generics
 import Generics.OneLiner
@@ -29,10 +36,8 @@
 
 
 infixr 5 :^:
-data Tree a = Leaf { value :: a } | Tree a :^: Tree a deriving (Show, Generic)
-
-instance Size a => Size (Tree a)
-instance EnumAll a => EnumAll (Tree a)
+data Tree a = Leaf { value :: a } | Tree a :^: Tree a
+  deriving (Show, Generic, Size, EnumAll)
 
 trees :: [Tree (Maybe Bool)]
 trees = enumAll
diff --git a/examples/realworld.hs b/examples/realworld.hs
--- a/examples/realworld.hs
+++ b/examples/realworld.hs
@@ -5,11 +5,13 @@
 import Data.Monoid
 -- import Control.Lens (Traversal')
 -- import Data.Typeable
+import Control.Applicative
 import Control.DeepSeq
 import Test.SmallCheck.Series
 import Control.Monad.Logic.Class
 import Control.Monad
 import Data.Hashable
+import Data.Functor.Compose
 import Data.Functor.Contravariant
 import Data.Functor.Contravariant.Divisible
 import Data.Void
@@ -29,24 +31,22 @@
 instance MonadLogic m => Applicative (Fair m) where
   pure a = Fair $ pure a
   Fair fs <*> Fair as = Fair $ fs <~> as
+instance MonadLogic m => Alternative (Fair m) where
+  empty = Fair mzero
+  Fair l <|> Fair r = Fair $ l \/ r
 
 gseries :: forall t m. (ADT t, Constraints t (Serial m), MonadLogic m) => Series m t
-gseries = foldr ((\/) . decDepth . runFair) mzero $ createA (For :: For (Serial m)) [Fair series]
+gseries = decDepth $ runFair $ createA (For :: For (Serial m)) (Fair series)
 
 newtype CoSeries m a = CoSeries { runCoSeries :: forall r. Series m r -> Series m (a -> r) }
 instance Contravariant (CoSeries m) where
   contramap f (CoSeries g) = CoSeries $ fmap (. f) . g
 instance Divisible (CoSeries m) where
-  divide f (CoSeries g) (CoSeries h) = CoSeries $ \rs -> do
-    rs' <- fixDepth rs
-    f2 <- decDepthChecked (constM $ constM rs') (g $ h rs')
-    return $ uncurry f2 . f
+  divide f (CoSeries g) (CoSeries h) = CoSeries $ \rs -> (\bcr -> uncurry bcr . f) <$> g (h rs)
   conquer = CoSeries constM
 instance MonadLogic m => Decidable (CoSeries m) where
-  choose f (CoSeries g) (CoSeries h) = CoSeries $ \rs ->
-    (\br cr -> either br cr . f) <$> g rs <~> h rs
-  lose f = CoSeries $ \_ ->
-    return $ absurd . f
+  choose f (CoSeries g) (CoSeries h) = CoSeries $ \rs -> (\br cr -> either br cr . f) <$> g rs <~> h rs
+  lose f = CoSeries $ \_ -> return $ absurd . f
 
 gcoseries :: forall t m r. (ADT t, Constraints t (CoSerial m), MonadLogic m)
           => Series m r -> Series m (t -> r)
@@ -60,7 +60,7 @@
 
 -- http://hackage.haskell.org/package/binary-0.7.2.1/docs/Data-Binary.html
 gget :: (ADT t, Constraints t Binary) => Get t
-gget = getWord8 >>= \ix -> createA (For :: For Binary) [get] !! fromEnum ix
+gget = getWord8 >>= \ix -> getCompose (createA (For :: For Binary) (Compose [get])) !! fromEnum ix
 
 gput :: (ADT t, Constraints t Binary) => t -> Put
 gput t = putWord8 (toEnum (ctorIndex t)) <> gfoldMap (For :: For Binary) put t
diff --git a/one-liner.cabal b/one-liner.cabal
--- a/one-liner.cabal
+++ b/one-liner.cabal
@@ -1,14 +1,9 @@
 Name:                 one-liner
-Version:              0.6
+Version:              0.7
 Synopsis:             Constraint-based generics
 Description:          Write short and concise generic instances of type classes.
-                      .
-                      There are two separate parts: @Generics.OneLiner@ is for
-                      writing generic functions using @GHC.Generics@.
-                      The other modules show how to implement these same generic
-                      functions with a traversal-style generics type class,
-                      without the use of an intermediate generic representation
-                      type.
+                      one-liner is particularly useful for writing default
+                      implementations of type class methods.
 Homepage:             https://github.com/sjoerdvisscher/one-liner
 Bug-reports:          https://github.com/sjoerdvisscher/one-liner/issues
 License:              BSD3
@@ -34,7 +29,9 @@
     , transformers  >= 0.5 && < 0.6
     , contravariant >= 1.4 && < 1.5
     , ghc-prim      >= 0.5 && < 1.0
+    , bifunctors    >= 5.4 && < 6.0
     , profunctors   >= 5.2 && < 6.0
+    , tagged        >= 0.8 && < 0.9
 
 source-repository head
   type:     git
diff --git a/src/Generics/OneLiner.hs b/src/Generics/OneLiner.hs
--- a/src/Generics/OneLiner.hs
+++ b/src/Generics/OneLiner.hs
@@ -7,13 +7,13 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- This module is for writing generic functions on algebraic data types
--- of kind @*@. These data types must be an instance of the `Generic` type
--- class, which can be derived.
---
+-- 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.
 -----------------------------------------------------------------------------
 {-# LANGUAGE
     RankNTypes
+  , Trustworthy
   , TypeFamilies
   , ConstraintKinds
   , FlexibleContexts
@@ -21,71 +21,53 @@
 module Generics.OneLiner (
   -- * Producing values
   create, createA, ctorIndex,
+  create1, createA1, ctorIndex1,
   -- * Traversing values
   gmap, gfoldMap, gtraverse,
+  gmap1, gfoldMap1, gtraverse1,
   -- * Combining values
-  gzipWith, mzipWith, zipWithA,
+  mzipWith, zipWithA,
+  mzipWith1, zipWithA1,
   -- * Consuming values
-  consume,
-  -- * Single constructor functions
-  op0, op1, op2,
+  consume, consume1,
+  -- * Functions for records
+  -- | These functions only work for single constructor data types.
+  nullaryOp, unaryOp, binaryOp, algebra, dialgebra, gcotraverse1,
   -- * Generic programming with profunctors
-  GenericProfunctor(..), generic,
+  -- | All the above functions have been implemented using these functions,
+  -- using different `profunctor`s.
+  GenericRecordProfunctor(..), record, record1,
+  GenericNonEmptyProfunctor(..), nonEmpty, nonEmpty1,
+  GenericProfunctor(..), generic, generic1,
   -- * Types
-  ADT, ADTRecord, ADTNonEmpty, CtorCount, Constraints, For(..)
+  ADT, ADTNonEmpty, ADTRecord, Constraints,
+  ADT1, ADTNonEmpty1, ADTRecord1, Constraints1,
+  For(..), AnyType
 ) where
 
 import GHC.Generics
 import Control.Applicative
-import Data.Functor.Identity
-import Data.Functor.Contravariant
+import Data.Bifunctor.Biff
+import Data.Bifunctor.Clown
+import Data.Bifunctor.Joker
+import Data.Functor.Compose
 import Data.Functor.Contravariant.Divisible
 import Data.Profunctor
+import Data.Tagged
 import Generics.OneLiner.Internal
 
 
-newtype Zip f a b = Zip { runZip :: a -> a -> Maybe (f b) }
-instance Functor f => Profunctor (Zip f) where
-  dimap f g (Zip h) = Zip $ \a1 a2 -> fmap (fmap g) (h (f a1) (f a2))
-instance Applicative f => GenericProfunctor (Zip f) where
-  zero = Zip . const $ Just . pure
-  unit = Zip . const $ Just . pure
-  plus (Zip f) (Zip g) = Zip h where
-    h (L1 a) (L1 b) = fmap (fmap L1) (f a b)
-    h (R1 a) (R1 b) = fmap (fmap R1) (g a b)
-    h _ _ = Nothing
-  mult (Zip f) (Zip g) = Zip $ \(al :*: ar) (bl :*: br) -> liftA2 (:*:) <$> f al bl <*> g ar br
-
-newtype Create f a b = Create { unCreate :: [f b] }
-instance Functor f => Profunctor (Create f) where
-  dimap _ f = Create . map (fmap f) . unCreate
-instance Applicative f => GenericProfunctor (Create f) where
-  zero = Create []
-  unit = Create [pure U1]
-  plus (Create l) (Create r) = Create $ map (fmap L1) l ++ map (fmap R1) r
-  mult (Create l) (Create r) = Create $ liftA2 (:*:) <$> l <*> r
-
-newtype Consume f a b = Consume { unConsume :: f a }
-instance Contravariant f => Profunctor (Consume f) where
-  dimap f _ = Consume . contramap f . unConsume
-instance Decidable f => GenericProfunctor (Consume f) where
-  zero = Consume $ lose (\v -> v `seq` undefined)
-  unit = Consume conquer
-  plus (Consume f) (Consume g) = Consume $ choose h f g where
-    h (L1 l) = Left l
-    h (R1 r) = Right r
-  mult (Consume f) (Consume g) = Consume $ divide (\(l :*: r) -> (l, r)) f g
-
-
 -- | Create a value (one for each constructor), given how to construct the components.
 --
 -- @
 -- `minBound` = `head` `$` `create` (`For` :: `For` `Bounded`) [`minBound`]
 -- `maxBound` = `last` `$` `create` (`For` :: `For` `Bounded`) [`maxBound`]
 -- @
+--
+-- `create` is `createA` specialized to lists.
 create :: (ADT t, Constraints t c)
        => for c -> (forall s. c s => [s]) -> [t]
-create for f = map runIdentity (createA for (Identity <$> f))
+create = createA
 
 -- | Create a value (one for each constructor), given how to construct the components, under an applicative effect.
 --
@@ -94,21 +76,41 @@
 -- @
 -- get = getWord8 `>>=` \\ix -> `createA` (`For` :: `For` Binary) [get] `!!` `fromEnum` ix
 -- @
-createA :: (ADT t, Constraints t c, Applicative f)
-        => for c -> (forall s. c s => [f s]) -> [f t]
-createA for f = unCreate $ generic for (Create f)
+--
+-- `createA` is `generic` specialized to `Joker`.
+createA :: (ADT t, Constraints t c, Alternative f)
+        => for c -> (forall s. c s => f s) -> f t
+createA for f = runJoker $ generic for $ Joker f
 
 -- | Generate ways to consume values of type `t`. This is the contravariant version of `createA`.
+--
+-- `consume` is `generic` specialized to `Clown`.
 consume :: (ADT t, Constraints t c, Decidable f)
         => for c -> (forall s. c s => f s) -> f t
-consume for f = unConsume $ generic for (Consume f)
+consume for f = runClown $ generic for $ Clown f
 
+-- | `create1` is `createA1` specialized to lists.
+create1 :: (ADT1 t, Constraints1 t c)
+        => for c -> (forall b s. c s => [b] -> [s b]) -> [a] -> [t a]
+create1 = createA1
 
+-- | `createA1` is `generic1` specialized to `Joker`.
+createA1 :: (ADT1 t, Constraints1 t c, Alternative f)
+         => for c -> (forall b s. c s => f b -> f (s b)) -> f a -> f (t a)
+createA1 for f p = runJoker $ generic1 for (Joker . f . runJoker) (Joker p)
 
+-- | `consume1` is `generic1` specialized to `Clown`.
+consume1 :: (ADT1 t, Constraints1 t c, Decidable f)
+         => for c -> (forall b s. c s => f b -> f (s b)) -> f a -> f (t a)
+consume1 for f p = runClown $ generic1 for (Clown . f . runClown) (Clown p)
+
+
 -- | Map over a structure, updating each component.
+--
+-- `gmap` is `generic` specialized to @(->)@.
 gmap :: (ADT t, Constraints t c)
      => for c -> (forall s. c s => s -> s) -> t -> t
-gmap for f = runIdentity . gtraverse for (Identity . f)
+gmap = generic
 
 -- | Map each component of a structure to a monoid, and combine the results.
 --
@@ -117,65 +119,164 @@
 -- @
 -- size = `succ` `.` `getSum` `.` `gfoldMap` (`For` :: `For` Size) (`Sum` `.` size)
 -- @
+--
+-- `gfoldMap` is `gtraverse` specialized to `Const`.
 gfoldMap :: (ADT t, Constraints t c, Monoid m)
          => for c -> (forall s. c s => s -> m) -> t -> m
 gfoldMap for f = getConst . gtraverse for (Const . f)
 
 -- | 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 :: (ADT t, Constraints t c, Applicative f)
           => for c -> (forall s. c s => s -> f s) -> t -> f t
-gtraverse for f = runStar $ generic for (Star f)
+gtraverse for f = runStar $ generic for $ Star f
 
--- | Combine two values by combining each component of the structures with the given function.
--- Returns `Nothing` if the constructors don't match.
-gzipWith :: (ADT t, Constraints t c)
-         => for c -> (forall s. c s => s -> s -> Maybe s) -> t -> t -> Maybe t
-gzipWith for f l r = runIdentity <$> zipWithA for (\x y -> Identity <$> f x y) l r
+-- |
+-- @
+-- fmap = `gmap1` (`For` :: `For` `Functor`) `fmap`
+-- @
+--
+-- `gmap1` is `generic1` specialized to @(->)@.
+gmap1 :: (ADT1 t, Constraints1 t c)
+     => for c -> (forall d e s. c s => (d -> e) -> s d -> s e) -> (a -> b) -> t a -> t b
+gmap1 = generic1
 
+-- |
+-- @
+-- foldMap = `gfoldMap1` (`For` :: `For` `Foldable`) `foldMap`
+-- @
+--
+-- `gfoldMap1` is `gtraverse1` specialized to `Const`.
+gfoldMap1 :: (ADT1 t, Constraints1 t c, Monoid m)
+          => for c -> (forall s b. c s => (b -> m) -> s b -> m) -> (a -> m) -> t a -> m
+gfoldMap1 for f g = getConst . gtraverse1 for ((Const .) . f . (getConst .)) (Const . g)
+
+-- |
+-- @
+-- traverse = `gtraverse1` (`For` :: `For` `Traversable`) `traverse`
+-- @
+--
+-- `gtraverse1` is `generic1` specialized to `Star`.
+gtraverse1 :: (ADT1 t, Constraints1 t c, Applicative f)
+           => for c -> (forall d e s. c s => (d -> f e) -> s d -> f (s e)) -> (a -> f b) -> t a -> f (t b)
+gtraverse1 for f g = runStar $ generic1 for (Star . f . runStar) (Star g)
+
 -- | Combine two values by combining each component of the structures to a monoid, and combine the results.
 -- Returns `mempty` if the constructors don't match.
 --
 -- @
 -- `compare` s t = `compare` (`ctorIndex` s) (`ctorIndex` t) `<>` `mzipWith` (`For` :: `For` `Ord`) `compare` s t
 -- @
+--
+-- `mzipWith` is `zipWithA` specialized to @`Compose` `Maybe` (`Const` m)@
 mzipWith :: (ADT t, Constraints t c, Monoid m)
          => for c -> (forall s. c s => s -> s -> m) -> t -> t -> m
-mzipWith for f l r = maybe mempty getConst $ zipWithA for (\x y -> Just . Const $ f x y) l r
+mzipWith for f = outm2 $ zipWithA for (inm2 f)
 
 -- | Combine two values by combining each component of the structures with the given function, under an applicative effect.
--- Returns `Nothing` if the constructors don't match.
-zipWithA :: (ADT t, Constraints t c, Applicative f)
-         => for c -> (forall s. c s => s -> s -> Maybe (f s)) -> t -> t -> Maybe (f t)
-zipWithA for f = runZip $ generic for (Zip f)
+-- Returns `empty` if the constructors don't match.
+zipWithA :: (ADT t, Constraints t c, Alternative f)
+         => for c -> (forall s. c s => s -> s -> f s) -> t -> t -> f t
+zipWithA for f = runZip $ generic for $ Zip f
 
+-- |
+-- @
+-- liftCompare = mzipWith (For :: For Ord1) liftCompare
+-- @
+--
+-- `mzipWith1` is `zipWithA1` specialized to @`Compose` `Maybe` (`Const` m)@
+mzipWith1 :: (ADT1 t, Constraints1 t c, Monoid m)
+          => for c -> (forall s b. c s => (b -> b -> m) -> s b -> s b -> m)
+          -> (a -> a -> m) -> t a -> t a -> m
+mzipWith1 for f p = outm2 $ zipWithA1 for (inm2 . f . outm2) (inm2 p)
+
+zipWithA1 :: (ADT1 t, Constraints1 t c, Alternative f)
+          => for c -> (forall d e s. c s => (d -> d -> f e) -> s d -> s d -> f (s e))
+          -> (a -> a -> f b) -> t a -> t a -> f (t b)
+zipWithA1 for f p = runZip $ generic1 for (Zip . f . runZip) (Zip p)
+
+
+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))
+instance Applicative f => GenericRecordProfunctor (Zip f) where
+  unit = Zip $ \_ _ -> pure U1
+  mult (Zip f) (Zip g) = Zip $ \(al :*: ar) (bl :*: br) -> (:*:) <$> f al bl <*> g ar br
+instance Alternative f => GenericNonEmptyProfunctor (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
+instance Alternative f => GenericProfunctor (Zip f) where
+  zero = Zip absurd
+
+inm2 :: (t -> t -> m) -> t -> t -> Compose Maybe (Const m) a
+inm2 f x y = Compose $ Just $ Const $ f x y
+outm2 :: Monoid m => (t -> t -> Compose Maybe (Const m) a) -> t -> t -> m
+outm2 f x y = maybe mempty getConst $ getCompose (f x y)
+
 -- | Implement a nullary operator by calling the operator for each component.
 --
 -- @
--- `mempty` = `op0` (`For` :: `For` `Monoid`) `mempty`
--- `fromInteger` i = `op0` (`For` :: `For` `Num`) (`fromInteger` i)
+-- `mempty` = `nullaryOp` (`For` :: `For` `Monoid`) `mempty`
+-- `fromInteger` i = `nullaryOp` (`For` :: `For` `Num`) (`fromInteger` i)
 -- @
-op0 :: (ADTRecord t, Constraints t c)
-    => for c -> (forall s. c s => s) -> t
-op0 for f = head $ create for [f]
+--
+-- `nullaryOp` is `record` specialized to `Tagged`.
+nullaryOp :: (ADTRecord t, Constraints t c)
+          => for c -> (forall s. c s => s) -> t
+nullaryOp for f = unTagged $ record for $ Tagged f
 
 -- | Implement a unary operator by calling the operator on the components.
--- This is here for consistency, it is the same as `gmap`.
+-- This is here for consistency, it is the same as `record`.
 --
 -- @
--- `negate` = `op1` (`For` :: `For` `Num`) `negate`
+-- `negate` = `unaryOp` (`For` :: `For` `Num`) `negate`
 -- @
-op1 :: (ADTRecord t, Constraints t c)
-     => for c -> (forall s. c s => s -> s) -> t -> t
-op1 = gmap
+unaryOp :: (ADTRecord t, Constraints t c)
+        => for c -> (forall s. c s => s -> s) -> t -> t
+unaryOp = record
 
 -- | Implement a binary operator by calling the operator on the components.
 --
 -- @
--- `mappend` = `op2` (`For` :: `For` `Monoid`) `mappend`
--- (`+`) = `op2` (`For` :: `For` `Num`) (`+`)
+-- `mappend` = `binaryOp` (`For` :: `For` `Monoid`) `mappend`
+-- (`+`) = `binaryOp` (`For` :: `For` `Num`) (`+`)
 -- @
-op2 :: (ADTRecord t, Constraints t c)
-    => for c -> (forall s. c s => s -> s -> s) -> t -> t -> t
-op2 for f l r = case gzipWith for (\a b -> Just (f a b)) l r of
-  Just t -> t
-  Nothing -> error "op2: constructor mismatch should not be possible for ADTRecord"
+--
+-- `binaryOp` is `algebra` specialized to pairs.
+binaryOp :: (ADTRecord t, Constraints t c)
+         => for c -> (forall s. c s => s -> s -> s) -> t -> t -> t
+binaryOp for f l r = algebra for (\(Pair a b) -> f a b) (Pair l r)
+
+data Pair a = Pair a a
+instance Functor Pair where
+  fmap f (Pair a b) = Pair (f a) (f b)
+
+-- | Create an F-algebra, given an F-algebra for each of the components.
+--
+-- @
+-- `binaryOp` for f l r = `algebra` for (\\(Pair a b) -> f a b) (Pair l r)
+-- @
+--
+-- `algebra` is `record` specialized to `Costar`.
+algebra :: (ADTRecord t, Constraints t c, Functor f)
+        => for c -> (forall s. c s => f s -> s) -> f t -> t
+algebra for f = runCostar $ record for $ Costar f
+
+-- | `dialgebra` is `record` specialized to @`Biff` (->)@.
+dialgebra :: (ADTRecord t, Constraints t c, Functor f, Applicative g)
+        => for c -> (forall s. c s => f s -> g s) -> f t -> g t
+dialgebra for f = runBiff $ record for $ Biff f
+
+-- |
+--
+-- @
+-- cotraverse = `gcotraverse1` (`For` :: `For` `Distributive`) `cotraverse`
+-- @
+--
+-- `gcotraverse1` is `record1` specialized to `Costar`.
+gcotraverse1 :: (ADTRecord1 t, Constraints1 t c, Functor f)
+             => for c -> (forall d e s. c s => (f d -> e) -> f (s d) -> s e) -> (f a -> b) -> f (t a) -> t b
+gcotraverse1 for f p = runCostar $ record1 for (Costar . f . runCostar) (Costar p)
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,12 +11,15 @@
 {-# LANGUAGE
     GADTs
   , DataKinds
+  , EmptyCase
+  , PolyKinds
   , RankNTypes
   , LambdaCase
   , TypeFamilies
   , TypeOperators
   , ConstraintKinds
   , FlexibleContexts
+  , FlexibleInstances
   , ScopedTypeVariables
   , UndecidableInstances
   #-}
@@ -24,102 +27,259 @@
 
 import GHC.Generics
 import GHC.Types (Constraint)
-import GHC.TypeLits
-import Data.Proxy
+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.Profunctor
+import Data.Tagged
 
+
 type family Constraints' (t :: * -> *) (c :: * -> Constraint) :: Constraint
 type instance Constraints' V1 c = ()
 type instance Constraints' U1 c = ()
 type instance Constraints' (f :+: g) c = (Constraints' f c, Constraints' g c)
 type instance Constraints' (f :*: g) c = (Constraints' f c, Constraints' g c)
-type instance Constraints' (M1 i t f) c = Constraints' f c
 type instance Constraints' (K1 i a) c = c a
+type instance Constraints' (M1 i t f) c = Constraints' f c
 
 class ADT' (t :: * -> *) where
-  type CtorCount' t :: Nat
-  type CtorCount' t = 1
-  ctorIndex' :: t x -> Int
-  ctorIndex' _ = 0
-  ctorCount :: proxy t -> Int
-  ctorCount _ = 1
+  generic' :: (Constraints' t c, GenericProfunctor p)
+    => for c -> (forall s. c s => p s s) -> p (t x) (t x)
 
-  p :: (Constraints' t c, GenericProfunctor p)
+class ADTNonEmpty' (t :: * -> *) where
+  nonEmpty' :: (Constraints' t c, GenericNonEmptyProfunctor p)
     => for c -> (forall s. c s => p s s) -> p (t x) (t x)
 
-instance ADT' V1 where
-  type CtorCount' V1 = 0
-  ctorCount _ = 0
-  p _ _ = zero
+class ADTRecord' (t :: * -> *) where
+  record' :: (Constraints' t c, GenericRecordProfunctor p)
+    => for c -> (forall s. c s => p s s) -> p (t x) (t x)
 
-instance (ADT' f, ADT' g) => ADT' (f :+: g) where
-  type CtorCount' (f :+: g) = CtorCount' f + CtorCount' g
-  ctorIndex' (L1 l) = ctorIndex' l
-  ctorIndex' (R1 r) = ctorCount (Proxy :: Proxy f) + ctorIndex' r
-  ctorCount _ = ctorCount (Proxy :: Proxy f) + ctorCount (Proxy :: Proxy g)
-  p for f = plus (p for f) (p for f)
+instance ADT' V1 where generic' _ _ = zero
+instance ADT' U1 where generic' _ _ = unit
+instance (ADT' f, ADT' g) => ADT' (f :+: g) where generic' for f = plus (generic' for f) (generic' for f)
+instance (ADT' f, ADT' g) => ADT' (f :*: g) where generic' for f = mult (generic' for f) (generic' for f)
+instance ADT' (K1 i v) where generic' _ = dimap unK1 K1
+instance ADT' f => ADT' (M1 i t f) where generic' for f = dimap unM1 M1 (generic' for f)
 
-instance ADT' U1 where
-  p _ _ = unit
+instance ADTNonEmpty' U1 where nonEmpty' _ _ = unit
+instance (ADTNonEmpty' f, ADTNonEmpty' g) => ADTNonEmpty' (f :+: g) where nonEmpty' for f = plus (nonEmpty' for f) (nonEmpty' for f)
+instance (ADTNonEmpty' f, ADTNonEmpty' g) => ADTNonEmpty' (f :*: g) where nonEmpty' for f = mult (nonEmpty' for f) (nonEmpty' for f)
+instance ADTNonEmpty' (K1 i v) where nonEmpty' _ = dimap unK1 K1
+instance ADTNonEmpty' f => ADTNonEmpty' (M1 i t f) where nonEmpty' for f = dimap unM1 M1 (nonEmpty' for f)
 
-instance (ADT' f, ADT' g) => ADT' (f :*: g) where
-  p for f = mult (p for f) (p for f)
+instance ADTRecord' U1 where record' _ _ = unit
+instance (ADTRecord' f, ADTRecord' g) => ADTRecord' (f :*: g) where record' for f = mult (record' for f) (record' for f)
+instance ADTRecord' (K1 i v) where record' _ = dimap unK1 K1
+instance ADTRecord' f => ADTRecord' (M1 i t f) where record' for f = dimap unM1 M1 (record' for f)
 
-instance ADT' (K1 i v) where
-  p _ = dimap unK1 K1
 
-instance ADT' f => ADT' (M1 i t f) where
-  type CtorCount' (M1 i t f) = CtorCount' f
-  ctorIndex' = ctorIndex' . unM1
-  ctorCount _ = ctorCount (Proxy :: Proxy f)
-  p for f = dimap unM1 M1 (p for f)
+type family Constraints1' (t :: * -> *) (c :: (* -> *) -> Constraint) :: Constraint
+type instance Constraints1' V1 c = ()
+type instance Constraints1' U1 c = ()
+type instance Constraints1' (f :+: g) c = (Constraints1' f c, Constraints1' g c)
+type instance Constraints1' (f :*: g) c = (Constraints1' f c, Constraints1' g c)
+type instance Constraints1' (f :.: g) c = (c f, Constraints1' g c)
+type instance Constraints1' Par1 c = ()
+type instance Constraints1' (Rec1 f) c = c f
+type instance Constraints1' (M1 i t f) c = Constraints1' f c
 
+class ADT1' (t :: * -> *) where
+  generic1' :: (Constraints1' t c, GenericProfunctor p)
+    => for c -> (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
 
-class Profunctor p => GenericProfunctor p where
-  zero :: p (V1 a) (V1 a)
-  unit :: p (U1 a) (U1 a)
-  plus :: p (f a) (f' a) -> p (g a) (g' a) -> p ((f :+: g) a) ((f' :+: g') a)
-  mult :: p (f a) (f' a) -> p (g a) (g' a) -> p ((f :*: g) a) ((f' :*: g') a)
+class ADTNonEmpty1' (t :: * -> *) where
+  nonEmpty1' :: (Constraints1' t c, GenericNonEmptyProfunctor p)
+    => for c -> (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
 
-instance Applicative f => GenericProfunctor (Star f) where
-  zero = Star pure
-  unit = Star pure
-  plus (Star f) (Star g) = Star $ \case
-    L1 l -> L1 <$> f l
-    R1 r -> R1 <$> g r
+class ADTRecord1' (t :: * -> *) where
+  record1' :: (Constraints1' t c, GenericRecordProfunctor p)
+    => for c -> (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+
+instance ADT1' V1 where generic1' _ _ _ = zero
+instance ADT1' U1 where generic1' _ _ _ = unit
+instance (ADT1' f, ADT1' g) => ADT1' (f :+: g) where generic1' for f p = plus (generic1' for f p) (generic1' for f p)
+instance (ADT1' f, ADT1' g) => ADT1' (f :*: g) where generic1' for f p = mult (generic1' for f p) (generic1' for f p)
+instance ADT1' g => ADT1' (f :.: g) where generic1' for f p = dimap unComp1 Comp1 $ f (generic1' for f p)
+instance ADT1' Par1 where generic1' _ _ = dimap unPar1 Par1
+instance ADT1' (Rec1 f) where generic1' _ f p = dimap unRec1 Rec1 (f p)
+instance ADT1' f => ADT1' (M1 i t f) where generic1' for f p = dimap unM1 M1 (generic1' for f p)
+
+instance ADTNonEmpty1' U1 where nonEmpty1' _ _ _ = unit
+instance (ADTNonEmpty1' f, ADTNonEmpty1' g) => ADTNonEmpty1' (f :+: g) where nonEmpty1' for f p = plus (nonEmpty1' for f p) (nonEmpty1' for f p)
+instance (ADTNonEmpty1' f, ADTNonEmpty1' g) => ADTNonEmpty1' (f :*: g) where nonEmpty1' for f p = mult (nonEmpty1' for f p) (nonEmpty1' for f p)
+instance ADTNonEmpty1' g => ADTNonEmpty1' (f :.: g) where nonEmpty1' for f p = dimap unComp1 Comp1 $ f (nonEmpty1' for f p)
+instance ADTNonEmpty1' Par1 where nonEmpty1' _ _ = dimap unPar1 Par1
+instance ADTNonEmpty1' (Rec1 f) where nonEmpty1' _ f p = dimap unRec1 Rec1 (f p)
+instance ADTNonEmpty1' f => ADTNonEmpty1' (M1 i t f) where nonEmpty1' for f p = dimap unM1 M1 (nonEmpty1' for f p)
+
+instance ADTRecord1' U1 where record1' _ _ _ = unit
+instance (ADTRecord1' f, ADTRecord1' g) => ADTRecord1' (f :*: g) where record1' for f p = mult (record1' for f p) (record1' for f p)
+instance ADTRecord1' g => ADTRecord1' (f :.: g) where record1' for f p = dimap unComp1 Comp1 $ f (record1' for f p)
+instance ADTRecord1' Par1 where record1' _ _ = dimap unPar1 Par1
+instance ADTRecord1' (Rec1 f) where record1' _ f p = dimap unRec1 Rec1 (f p)
+instance ADTRecord1' f => ADTRecord1' (M1 i t f) where record1' for f p = dimap unM1 M1 (record1' for f p)
+
+
+absurd :: V1 a -> b
+absurd = \case {}
+
+e1 :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b
+e1 f _ (L1 l) = f l
+e1 _ f (R1 r) = f r
+
+fst1 :: (f :*: g) a -> f a
+fst1 (l :*: _) = l
+snd1 :: (f :*: g) a -> g a
+snd1 (_ :*: r) = r
+
+-- | 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 => GenericRecordProfunctor p where
+  unit :: p (U1 a) (U1 a')
+  mult :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :*: g) a) ((f' :*: g') a')
+
+-- | A generic function using a `GenericNonEmptyProfunctor` works on any data
+-- type with at least one constructor.
+class GenericRecordProfunctor p => GenericNonEmptyProfunctor p where
+  plus :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :+: g) a) ((f' :+: g') a')
+
+-- | A generic function using a `GenericProfunctor` works on any
+-- algebraic data type, including those with no constructors.
+class GenericNonEmptyProfunctor p => GenericProfunctor p where
+  zero :: p (V1 a) (V1 a')
+
+instance GenericRecordProfunctor (->) where
+  unit _ = U1
+  mult f g (l :*: r) = f l :*: g r
+instance GenericNonEmptyProfunctor (->) where
+  plus f g = e1 (L1 . f) (R1 . g)
+instance GenericProfunctor (->) where
+  zero = absurd
+
+instance GenericRecordProfunctor Tagged where
+  unit = Tagged U1
+  mult (Tagged l) (Tagged r) = Tagged $ l :*: r
+
+instance Applicative f => GenericRecordProfunctor (Star f) where
+  unit = Star $ \_ -> pure U1
   mult (Star f) (Star g) = Star $ \(l :*: r) -> (:*:) <$> f l <*> g r
+instance Applicative f => GenericNonEmptyProfunctor (Star f) where
+  plus (Star f) (Star g) = Star $ e1 (fmap L1 . f) (fmap R1 . g)
+instance Applicative f => GenericProfunctor (Star f) where
+  zero = Star absurd
 
--- | All the above functions have been implemented using this single function,
--- using different `profunctor`s.
+instance Functor f => GenericRecordProfunctor (Costar f) where
+  unit = Costar $ const U1
+  mult (Costar f) (Costar g) = Costar $ \lr -> f (fst1 <$> lr) :*: g (snd1 <$> lr)
+
+instance (Functor f, Applicative g) => GenericRecordProfunctor (Biff (->) f g) where
+  unit = Biff $ const $ pure U1
+  mult (Biff f) (Biff g) = Biff $ \lr -> (:*:) <$> f (fst1 <$> lr) <*> g (snd1 <$> lr)
+
+instance Applicative f => GenericRecordProfunctor (Joker f) where
+  unit = Joker $ pure U1
+  mult (Joker l) (Joker r) = Joker $ (:*:) <$> l <*> r
+instance Alternative f => GenericNonEmptyProfunctor (Joker f) where
+  plus (Joker l) (Joker r) = Joker $ L1 <$> l <|> R1 <$> r
+instance Alternative f => GenericProfunctor (Joker f) where
+  zero = Joker empty
+
+instance Divisible f => GenericRecordProfunctor (Clown f) where
+  unit = Clown conquer
+  mult (Clown f) (Clown g) = Clown $ divide (\(l :*: r) -> (l, r)) f g
+instance Decidable f => GenericNonEmptyProfunctor (Clown f) where
+  plus (Clown f) (Clown g) = Clown $ choose (e1 Left Right) f g where
+instance Decidable f => GenericProfunctor (Clown f) where
+  zero = Clown $ lose (\v -> v `seq` undefined)
+
+instance (GenericRecordProfunctor p, GenericRecordProfunctor q) => GenericRecordProfunctor (Product p q) where
+  unit = Pair unit unit
+  mult (Pair l1 r1) (Pair l2 r2) = Pair (mult l1 l2) (mult r1 r2)
+instance (GenericNonEmptyProfunctor p, GenericNonEmptyProfunctor q) => GenericNonEmptyProfunctor (Product p q) where
+  plus (Pair l1 r1) (Pair l2 r2) = Pair (plus l1 l2) (plus r1 r2)
+instance (GenericProfunctor p, GenericProfunctor q) => GenericProfunctor (Product p q) where
+  zero = Pair zero zero
+
+instance (Applicative f, GenericRecordProfunctor p) => GenericRecordProfunctor (Tannen f p) where
+  unit = Tannen (pure unit)
+  mult (Tannen l) (Tannen r) = Tannen $ liftA2 mult l r
+instance (Applicative f, GenericNonEmptyProfunctor p) => GenericNonEmptyProfunctor (Tannen f p) where
+  plus (Tannen l) (Tannen r) = Tannen $ liftA2 plus l r
+instance (Applicative f, GenericProfunctor p) => GenericProfunctor (Tannen f p) where
+  zero = Tannen (pure zero)
+
+data Ctor a b = Ctor { index :: a -> Int, count :: Int }
+instance Profunctor Ctor where
+  dimap l _ (Ctor i c) = Ctor (i . l) c
+instance GenericRecordProfunctor Ctor where
+  unit = Ctor (const 0) 1
+  mult _ _ = Ctor (const 0) 1
+instance GenericNonEmptyProfunctor Ctor where
+  plus l r = Ctor (e1 (index l) ((count l + ) . index r)) (count l + count r)
+instance GenericProfunctor Ctor where
+  zero = Ctor (const 0) 0
+
+record :: (ADTRecord t, Constraints t c, GenericRecordProfunctor p)
+       => for c -> (forall s. c s => p s s) -> p t t
+record for f = dimap from to $ record' for f
+
+record1 :: (ADTRecord1 t, Constraints1 t c, GenericRecordProfunctor p)
+        => for c -> (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+record1 for f p = dimap from1 to1 $ record1' for f p
+
+nonEmpty :: (ADTNonEmpty t, Constraints t c, GenericNonEmptyProfunctor p)
+         => for c -> (forall s. c s => p s s) -> p t t
+nonEmpty for f = dimap from to $ nonEmpty' for f
+
+nonEmpty1 :: (ADTNonEmpty1 t, Constraints1 t c, GenericNonEmptyProfunctor p)
+          => for c -> (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+nonEmpty1 for f p = dimap from1 to1 $ nonEmpty1' for f p
+
 generic :: (ADT t, Constraints t c, GenericProfunctor p)
         => for c -> (forall s. c s => p s s) -> p t t
-generic for f = dimap from to $ p for f
+generic for f = dimap from to $ generic' for f
 
--- | `Constraints` is a constraint type synonym, containing the constraint requirements for an instance for `t` of class `c`.
+generic1 :: (ADT1 t, Constraints1 t c, GenericProfunctor p)
+         => for c -> (forall d e s. c s => p d e -> p (s d) (s e)) -> p a b -> p (t a) (t b)
+generic1 for f p = dimap from1 to1 $ generic1' for f p
+
+-- | `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
 
--- | `ADT` is a constraint type synonym. The `Generic` instance can be derived,
--- and any generic representation will be an instance of `ADT'`.
-type ADT t = (Generic t, ADT' (Rep t))
-
--- | `CtorCount` is the number of constructors of a type at the type level.
--- F.e. if you want to require that a type has at least two constructors,
--- you can add the constraint @(2 `GHC.TypeLits.<=` `CtorCount` t)@.
-type CtorCount t = CtorCount' (Rep t)
+type Constraints1 t c = Constraints1' (Rep1 t) c
 
 -- | `ADTRecord` is a constraint type synonym. An instance is an `ADT` with *exactly* one constructor.
-type ADTRecord t = (ADT t, 1 ~ CtorCount t)
+type ADTRecord t = (Generic t, ADTRecord' (Rep t), Constraints t AnyType)
 
+type ADTRecord1 t = (Generic1 t, ADTRecord1' (Rep1 t), Constraints1 t AnyType)
+
 -- | `ADTNonEmpty` is a constraint type synonym. An instance is an `ADT` with *at least* one constructor.
-type ADTNonEmpty t = (ADT t, 1 <= CtorCount t)
+type ADTNonEmpty t = (Generic t, ADTNonEmpty' (Rep t), Constraints t AnyType)
 
+type ADTNonEmpty1 t = (Generic1 t, ADTNonEmpty1' (Rep1 t), Constraints1 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)
+
 -- | Tell the compiler which class we want to use in the traversal. Should be used like this:
 --
 -- > (For :: For Show)
 --
 -- Where @Show@ can be any class.
-data For (c :: * -> Constraint) = For
+data For (c :: k -> Constraint) = For
 
 -- | Get the index in the lists returned by `create` and `createA` of the constructor of the given value.
 --
@@ -130,4 +290,12 @@
 -- `put` t = `putWord8` (`toEnum` (`ctorIndex` t)) `<>` `gfoldMap` (`For` :: `For` `Binary`) `put` t
 -- @
 ctorIndex :: ADT t => t -> Int
-ctorIndex = ctorIndex' . from
+ctorIndex = index $ generic (For :: For AnyType) (Ctor (const 0) 1)
+
+ctorIndex1 :: ADT1 t => t a -> Int
+ctorIndex1 = index $ generic1 (For :: For AnyType) (const $ Ctor (const 0) 1) (Ctor (const 0) 1)
+
+-- | Any type is instance of `AnyType`, you can use it with @For :: For AnyType@
+-- if you don't actually need a class constraint.
+class AnyType a
+instance AnyType a