diff --git a/examples/defaultsignature.hs b/examples/defaultsignature.hs
--- a/examples/defaultsignature.hs
+++ b/examples/defaultsignature.hs
@@ -1,10 +1,11 @@
 {-# LANGUAGE
-  TypeOperators,
-  DeriveGeneric,
-  DeriveAnyClass,
-  ConstraintKinds,
-  FlexibleContexts,
-  DefaultSignatures 
+    TypeOperators
+  , DeriveGeneric
+  , DeriveAnyClass
+  , ConstraintKinds
+  , FlexibleContexts
+  , TypeApplications
+  , DefaultSignatures
   #-}
 
 import GHC.Generics
@@ -18,7 +19,7 @@
   size :: t -> Int
 
   default size :: (ADT t, Constraints t Size) => t -> Int
-  size = succ . getSum . gfoldMap (For :: For Size) (Sum . size)
+  size = succ . getSum . gfoldMap @Size (Sum . size)
 
 instance Size Bool
 instance Size a => Size (Maybe a)
@@ -29,7 +30,7 @@
   enumAll :: [t]
 
   default enumAll :: (ADT t, Constraints t EnumAll) => [t]
-  enumAll = concat $ createA (For :: For EnumAll) [enumAll]
+  enumAll = createA @EnumAll enumAll
 
 instance EnumAll Bool
 instance EnumAll a => EnumAll (Maybe a)
diff --git a/examples/freevars.hs b/examples/freevars.hs
--- a/examples/freevars.hs
+++ b/examples/freevars.hs
@@ -1,6 +1,6 @@
 -- Another go at this problem:
 -- https://github.com/sjoerdvisscher/blog/blob/master/2012/2012-03-03%20how%20to%20work%20generically%20with%20mutually%20recursive%20datatypes.md
-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts, DeriveGeneric #-}
+{-# LANGUAGE TypeSynonymInstances, TypeApplications, FlexibleInstances, FlexibleContexts, DeriveGeneric #-}
 
 import GHC.Generics
 import Generics.OneLiner
@@ -22,7 +22,7 @@
   vars :: t -> [Var] -> ([Var], [Var])
 
 varsDefault :: (ADT t, Constraints t Vars) => t -> [Var] -> ([Var], [Var])
-varsDefault = gfoldMap (For :: For Vars) vars
+varsDefault = gfoldMap @Vars vars
 
 instance Vars Var where
   vars v = const ([], [v])
diff --git a/examples/freevars1.hs b/examples/freevars1.hs
--- a/examples/freevars1.hs
+++ b/examples/freevars1.hs
@@ -1,6 +1,6 @@
 -- Another go at this problem:
 -- https://github.com/sjoerdvisscher/blog/blob/master/2012/2012-03-03%20how%20to%20work%20generically%20with%20mutually%20recursive%20datatypes.md
-{-# LANGUAGE FlexibleInstances, FlexibleContexts, DeriveGeneric, ScopedTypeVariables, MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, DeriveGeneric, TypeApplications, ScopedTypeVariables, MultiParamTypeClasses #-}
 
 import GHC.Generics
 import Generics.OneLiner
@@ -20,7 +20,7 @@
   vars1 :: (b -> [a] -> ([a], [a])) -> t b -> [a] -> ([a], [a])
 
 vars1Default :: forall a b t. (ADT1 t, Constraints1 t (Vars a)) => (b -> [a] -> ([a], [a])) -> t b -> [a] -> ([a], [a])
-vars1Default = gfoldMap1 (For :: For (Vars a)) vars1
+vars1Default = gfoldMap1 @(Vars a) vars1
 
 instance Vars a (Decl a) where
   vars1 f (v := e) = const ([], [v]) `mappend` vars1 f e
diff --git a/examples/lenses.hs b/examples/lenses.hs
--- a/examples/lenses.hs
+++ b/examples/lenses.hs
@@ -1,6 +1,6 @@
 -- This is a go at creating lenses with one-liner.
 -- It is not a perfect match, but with some unsafeCoerce here and there it works.
-{-# LANGUAGE RankNTypes, TypeOperators, DefaultSignatures, FlexibleContexts, DeriveGeneric, DeriveAnyClass #-}
+{-# LANGUAGE RankNTypes, TypeOperators, DefaultSignatures, FlexibleContexts, DeriveGeneric, DeriveAnyClass, TypeApplications #-}
 import Generics.OneLiner
 import Data.Profunctor
 import GHC.Generics
@@ -20,11 +20,12 @@
 newtype Lensed s t a b = Lensed { getLensed :: Lens s t a b -> b }
 instance Profunctor (Lensed s t) where
   dimap f g (Lensed ix) = Lensed $ \l -> g (ix (l . (fmap g .) . (. f)))
-instance GenericRecordProfunctor (Lensed s t) where
+instance GenericUnitProfunctor (Lensed s t) where
   unit = Lensed (constLens U1)
+instance GenericProductProfunctor (Lensed s t) where
   mult (Lensed a) (Lensed b) = Lensed (\l -> a (l . fstl) :*: b (l . sndl))
 
--- GenericRecordProfunctor is a bit too polymorphic,
+-- GenericProductProfunctor is a bit too polymorphic,
 -- but we can use unsafeCoerce because the types will end up being the same anyway.
 fstl :: Lens ((a :*: b) x) ((c :*: b') x') (a x) (c x')
 fstl f (a :*: b) = (\c -> c :*: unsafeCoerce b) <$> f a
@@ -36,7 +37,7 @@
 
   lensed :: (Lens s t a b -> b) -> Lens s t (f a) (f b) -> f b
   default lensed :: (ADTRecord1 f, Constraints1 f Repr) => (Lens s t a b -> b) -> Lens s t (f a) (f b) -> f b
-  lensed f = getLensed $ record1 (For :: For Repr) (\(Lensed g) -> Lensed $ lensed g) (Lensed f)
+  lensed f = getLensed $ record1 @Repr (\(Lensed g) -> Lensed $ lensed g) (Lensed f)
 
   tabulate :: (Key f -> a) -> f a
   tabulate f = lensed (\l -> f (runKey (unsafeCoerce (Lens l)))) id
diff --git a/examples/paradise.hs b/examples/paradise.hs
--- a/examples/paradise.hs
+++ b/examples/paradise.hs
@@ -3,8 +3,9 @@
   , DeriveGeneric
   , ConstraintKinds
   , FlexibleContexts
-  , FlexibleInstances
+  , TypeApplications
   , DefaultSignatures
+  , FlexibleInstances
   , OverlappingInstances
   #-}
 
@@ -37,7 +38,7 @@
 class IncreaseSalary t where
   increaseSalary :: Float -> t -> t
   default increaseSalary :: (ADT t, Constraints t IncreaseSalary) => Float -> t -> t
-  increaseSalary k = gmap (For :: For IncreaseSalary) (increaseSalary k)
+  increaseSalary k = gmap @IncreaseSalary (increaseSalary k)
 
 instance IncreaseSalary Company
 instance IncreaseSalary Dept
diff --git a/examples/realworld.hs b/examples/realworld.hs
--- a/examples/realworld.hs
+++ b/examples/realworld.hs
@@ -1,4 +1,15 @@
-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, ConstraintKinds, TypeOperators, FlexibleContexts, GeneralizedNewtypeDeriving, TypeSynonymInstances, FlexibleInstances #-}
+{-# LANGUAGE
+    GADTs
+  , RankNTypes
+  , TypeOperators
+  , ConstraintKinds
+  , FlexibleContexts
+  , TypeApplications
+  , FlexibleInstances
+  , ScopedTypeVariables
+  , TypeSynonymInstances
+  , GeneralizedNewtypeDeriving
+  #-}
 
 import Generics.OneLiner
 
@@ -24,7 +35,7 @@
 -- http://hackage.haskell.org/package/deepseq-generics-0.1.1.1/docs/src/Control-DeepSeq-Generics.html
 -- This would work if the monoid instance of () would have been strict, now it doesn't...
 grnf :: (ADT t, Constraints t NFData) => t -> ()
-grnf = gfoldMap (For :: For NFData) rnf
+grnf = gfoldMap @NFData rnf
 
 
 -- http://hackage.haskell.org/package/smallcheck-1.1.1/docs/src/Test-SmallCheck-Series.html
@@ -37,7 +48,7 @@
   Fair l <|> Fair r = Fair $ l \/ r
 
 gseries :: forall t m. (ADT t, Constraints t (Serial m), MonadLogic m) => Series m t
-gseries = decDepth $ runFair $ createA (For :: For (Serial m)) (Fair series)
+gseries = decDepth $ runFair $ createA @(Serial m) (Fair series)
 
 newtype CoSeries m a = CoSeries { runCoSeries :: forall r. Series m r -> Series m (a -> r) }
 instance Contravariant (CoSeries m) where
@@ -51,20 +62,20 @@
 
 gcoseries :: forall t m r. (ADT t, Constraints t (CoSerial m), MonadLogic m)
           => Series m r -> Series m (t -> r)
-gcoseries = runCoSeries $ consume (For :: For (CoSerial m)) (CoSeries coseries)
+gcoseries = runCoSeries $ consume @(CoSerial m) (CoSeries coseries)
 
 
 -- http://hackage.haskell.org/package/hashable-1.2.2.0/docs/src/Data-Hashable-Generic.html
 ghashWithSalt :: (ADT t, Constraints t Hashable) => Int -> t -> Int
 ghashWithSalt = flip $ \t -> flip hashWithSalt (ctorIndex t) .
-  appEndo (gfoldMap (For :: For Hashable) (Endo . flip hashWithSalt) t)
+  appEndo (gfoldMap @Hashable (Endo . flip hashWithSalt) t)
 
 -- 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 -> getCompose (createA (For :: For Binary) (Compose [get])) !! fromEnum ix
+gget = getWord8 >>= \ix -> getCompose (createA @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
+gput t = putWord8 (toEnum (ctorIndex t)) <> gfoldMap @Binary put t
 
 -- https://hackage.haskell.org/package/QuickCheck-2.8.1/docs/Test-QuickCheck-Arbitrary.html
 newtype CoArb a = CoArb { unCoArb :: forall b. a -> Gen b -> Gen b }
@@ -81,15 +92,15 @@
   lose f = CoArb $ absurd . f
 
 gcoarbitrary :: (ADT t, Constraints t CoArbitrary) => t -> Gen b -> Gen b
-gcoarbitrary = unCoArb $ consume (For :: For CoArbitrary) (CoArb coarbitrary)
+gcoarbitrary = unCoArb $ consume @CoArbitrary (CoArb coarbitrary)
 
 
 liftCompareDefault :: (ADT1 f, Constraints1 f Ord1) => (a -> a -> Ordering) -> f a -> f a -> Ordering
-liftCompareDefault = mzipWith1 (For :: For Ord1) liftCompare
+liftCompareDefault = mzipWith1 @Ord1 liftCompare
 
 infixr 9 .:
 (.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
 (.:) = (.) . (.)
 
 liftEqDefault :: (ADT1 f, Constraints1 f Eq1) => (a -> a -> Bool) -> f a -> f a -> Bool
-liftEqDefault = (getAll .:) . mzipWith1 (For :: For Eq1) ((All .:) . liftEq . (getAll .:)) . (All .:)
+liftEqDefault = (getAll .:) . mzipWith1 @Eq1 ((All .:) . liftEq . (getAll .:)) . (All .:)
diff --git a/examples/tinplate.hs b/examples/tinplate.hs
--- a/examples/tinplate.hs
+++ b/examples/tinplate.hs
@@ -4,41 +4,42 @@
   TypeFamilies,
   TypeOperators,
   FlexibleContexts,
+  TypeApplications,
   FlexibleInstances,
+  AllowAmbiguousTypes,
   ScopedTypeVariables,
   UndecidableInstances,
   MultiParamTypeClasses
   #-}
 
 import Generics.OneLiner
-import Data.Proxy
 import Data.Type.Equality
 
 import Data.Functor.Identity
 
 
 class TinplateHelper (p :: Bool) a b where
-  trav' :: Applicative f => proxy p -> (a -> f a) -> b -> f b
+  trav' :: Applicative f => (a -> f a) -> b -> f b
 
-instance TinplateHelper 'True a a where trav' _ f = f
+instance TinplateHelper 'True a a where trav' f = f
 
 instance {-# OVERLAPPABLE #-} (ADT b, Constraints b (TinplateAlias a)) => TinplateHelper 'False a b where
-  trav' _ = tinplate
+  trav' = tinplate
 
-instance TinplateHelper 'False a Char where trav' _ _ = pure
-instance TinplateHelper 'False a Double where trav' _ _ = pure
-instance TinplateHelper 'False a Float where trav' _ _ = pure
-instance TinplateHelper 'False a Int where trav' _ _ = pure
-instance TinplateHelper 'False a Word where trav' _ _ = pure
+instance TinplateHelper 'False a Char where trav' _ = pure
+instance TinplateHelper 'False a Double where trav' _ = pure
+instance TinplateHelper 'False a Float where trav' _ = pure
+instance TinplateHelper 'False a Int where trav' _ = pure
+instance TinplateHelper 'False a Word where trav' _ = pure
 
 class TinplateAlias a b where
   trav :: Applicative f => (a -> f a) -> b -> f b
 instance TinplateHelper (a == b) a b => TinplateAlias a b where
-  trav = trav' (Proxy :: Proxy (a == b))
+  trav = trav' @(a == b)
 
 
 tinplate :: forall a b f. (ADT b, Constraints b (TinplateAlias a), Applicative f) => (a -> f a) -> b -> f b
-tinplate f = gtraverse (For :: For (TinplateAlias a)) (trav f)
+tinplate f = gtraverse @(TinplateAlias a) (trav f)
 
 
 
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.8.1
+Version:              0.9
 Synopsis:             Constraint-based generics
 Description:          Write short and concise generic instances of type classes.
                       one-liner is particularly useful for writing default
@@ -12,7 +12,7 @@
 Maintainer:           sjoerd@w3future.com
 Category:             Generics
 Build-type:           Simple
-Cabal-version:        >= 1.6
+Cabal-version:        >= 1.8
 
 Extra-Source-Files:
   examples/*.hs
@@ -36,3 +36,15 @@
 source-repository head
   type:     git
   location: git://github.com/sjoerdvisscher/one-liner.git
+
+Test-suite unittests
+  Hs-source-dirs:  test
+  Main-is:         unittests.hs
+
+  Build-depends:
+      base
+    , contravariant
+    , HUnit
+    , one-liner
+
+  Type: exitcode-stdio-1.0
diff --git a/src/Generics/OneLiner.hs b/src/Generics/OneLiner.hs
--- a/src/Generics/OneLiner.hs
+++ b/src/Generics/OneLiner.hs
@@ -10,7 +10,7 @@
 -- 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.
--- The function `create_` does not require any such instance, but must be given
+-- The function `createA_` does not require any such instance, but must be given
 -- a constructor explicitly.
 -----------------------------------------------------------------------------
 {-# LANGUAGE
@@ -19,6 +19,9 @@
   , TypeFamilies
   , ConstraintKinds
   , FlexibleContexts
+  , TypeApplications
+  , AllowAmbiguousTypes
+  , ScopedTypeVariables
   #-}
 module Generics.OneLiner (
   -- * Producing values
@@ -40,13 +43,21 @@
   -- * Generic programming with profunctors
   -- | All the above functions have been implemented using these functions,
   -- using different `profunctor`s.
-  GenericRecordProfunctor(..), record, record1,
-  GenericNonEmptyProfunctor(..), nonEmpty, nonEmpty1,
-  GenericProfunctor(..), generic, generic1,
+  record, nonEmpty, generic,
+  record1, nonEmpty1, generic1,
+  -- ** Classes
+  GenericRecordProfunctor,
+  GenericNonEmptyProfunctor,
+  GenericProfunctor,
+  GenericUnitProfunctor(..),
+  GenericProductProfunctor(..),
+  GenericSumProfunctor(..),
+  GenericEmptyProfunctor(..),
   -- * Types
   ADT, ADTNonEmpty, ADTRecord, Constraints,
   ADT1, ADTNonEmpty1, ADTRecord1, Constraints1,
-  For(..), AnyType
+  FunConstraints, FunResult,
+  AnyType
 ) where
 
 import GHC.Generics
@@ -64,14 +75,15 @@
 -- | 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`]
+-- `minBound` = `head` `$` `create` \@`Bounded` [`minBound`]
+-- `maxBound` = `last` `$` `create` \@`Bounded` [`maxBound`]
 -- @
 --
 -- `create` is `createA` specialized to lists.
-create :: (ADT t, Constraints t c)
-       => for c -> (forall s. c s => [s]) -> [t]
-create = createA
+create :: forall c t. (ADT t, Constraints t c)
+       => (forall s. c s => [s]) -> [t]
+create = createA @c
+{-# INLINE create #-}
 
 -- | Create a value (one for each constructor), given how to construct the components, under an applicative effect.
 --
@@ -79,30 +91,34 @@
 -- constructor in a byte:
 --
 -- @
--- get = getWord8 `>>=` \\ix -> `getCompose` (`createA` (`For` :: `For` Binary) (`Compose` [get])) `!!` `fromEnum` ix
+-- get = getWord8 `>>=` \\ix -> `getCompose` (`createA` \@Binary (`Compose` [get])) `!!` `fromEnum` ix
 -- @
 --
 -- `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
+createA :: forall c t f. (ADT t, Constraints t c, Alternative f)
+        => (forall s. c s => f s) -> f t
+createA f = runJoker $ generic @c $ Joker f
+{-# INLINE createA #-}
 
 -- | 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 = runClown $ generic for $ Clown f
+consume :: forall c t f. (ADT t, Constraints t c, Decidable f)
+        => (forall s. c s => f s) -> f t
+consume f = runClown $ generic @c $ Clown f
+{-# INLINE consume #-}
 
 -- | `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
+create1 :: forall c t a. (ADT1 t, Constraints1 t c)
+        => (forall b s. c s => [b] -> [s b]) -> [a] -> [t a]
+create1 = createA1 @c
+{-# INLINE create1 #-}
 
 -- | `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 = dimap Joker runJoker $ generic1 for $ dimap runJoker Joker f
+createA1 :: forall c t f a. (ADT1 t, Constraints1 t c, Alternative f)
+         => (forall b s. c s => f b -> f (s b)) -> f a -> f (t a)
+createA1 f = dimap Joker runJoker $ generic1 @c $ dimap runJoker Joker f
+{-# INLINE createA1 #-}
 
 -- | Create a value, given a constructor (or a function) and
 -- how to construct its components, under an applicative effect.
@@ -111,163 +127,186 @@
 -- type with a single constructor (e.g., quadruples @(,,,)@).
 --
 -- @
--- arbitrary = `createA_` (`For` :: `For` Arbitrary) arbitrary (,,,)
+-- arbitrary = `createA_` \@`Arbitrary` arbitrary (,,,)
 -- @
-createA_ :: (FunConstraints t c, Applicative f)
-         => for c -> (forall s. c s => f s) -> t -> f (Result t)
-createA_ for run = autoApply for run . pure
+createA_ :: forall c t f. (FunConstraints c t, Applicative f)
+         => (forall s. c s => f s) -> t -> f (FunResult t)
+createA_ run = autoApply @c run . pure
+{-# INLINE createA_ #-}
 
 -- | `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 = dimap Clown runClown $ generic1 for $ dimap runClown Clown f
+consume1 :: forall c t f a. (ADT1 t, Constraints1 t c, Decidable f)
+         => (forall b s. c s => f b -> f (s b)) -> f a -> f (t a)
+consume1 f = dimap Clown runClown $ generic1 @c $ dimap runClown Clown f
+{-# INLINE consume1 #-}
 
 
 -- | 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 = generic
+gmap :: forall c t. (ADT t, Constraints t c)
+     => (forall s. c s => s -> s) -> t -> t
+gmap = generic @c
+{-# INLINE gmap #-}
 
 -- | Map each component of a structure to a monoid, and combine the results.
 --
 -- If you have a class `Size`, which measures the size of a structure, then this could be the default implementation:
 --
 -- @
--- size = `succ` `.` `getSum` `.` `gfoldMap` (`For` :: `For` Size) (`Sum` `.` size)
+-- size = `succ` `.` `getSum` `.` `gfoldMap` \@`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)
+gfoldMap :: forall c t m. (ADT t, Constraints t c, Monoid m)
+         => (forall s. c s => s -> m) -> t -> m
+gfoldMap f = getConst . gtraverse @c (Const . f)
+{-# INLINE gfoldMap #-}
 
 -- | 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 :: forall c t f. (ADT t, Constraints t c, Applicative f)
+          => (forall s. c s => s -> f s) -> t -> f t
+gtraverse f = runStar $ generic @c $ Star f
+{-# INLINE gtraverse #-}
 
 -- |
 -- @
--- fmap = `gmap1` (`For` :: `For` `Functor`) `fmap`
+-- fmap = `gmap1` \@`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
+gmap1 :: forall c t a b. (ADT1 t, Constraints1 t c)
+     => (forall d e s. c s => (d -> e) -> s d -> s e) -> (a -> b) -> t a -> t b
+gmap1 = generic1 @c
+{-# INLINE gmap1 #-}
 
 -- |
 -- @
--- foldMap = `gfoldMap1` (`For` :: `For` `Foldable`) `foldMap`
+-- foldMap = `gfoldMap1` \@`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 = dimap (Const .) (getConst .) $ gtraverse1 for $ dimap (getConst .) (Const .) f
+gfoldMap1 :: forall c t m a. (ADT1 t, Constraints1 t c, Monoid m)
+          => (forall s b. c s => (b -> m) -> s b -> m) -> (a -> m) -> t a -> m
+gfoldMap1 f = dimap (Const .) (getConst .) $ gtraverse1 @c $ dimap (getConst .) (Const .) f
+{-# INLINE gfoldMap1 #-}
 
 -- |
 -- @
--- traverse = `gtraverse1` (`For` :: `For` `Traversable`) `traverse`
+-- traverse = `gtraverse1` \@`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 = dimap Star runStar $ generic1 for $ dimap runStar Star f
+gtraverse1 :: forall c t f a b. (ADT1 t, Constraints1 t c, Applicative f)
+           => (forall d e s. c 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 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
+-- `compare` s t = `compare` (`ctorIndex` s) (`ctorIndex` t) `<>` `mzipWith` \@`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 = outm2 $ zipWithA for $ inm2 f
+mzipWith :: forall c t m. (ADT t, Constraints t c, Monoid m)
+         => (forall s. c s => s -> s -> m) -> t -> t -> m
+mzipWith f = outm2 $ zipWithA @c $ inm2 f
+{-# INLINE mzipWith #-}
 
 -- | 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 :: (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
+zipWithA :: forall c t f. (ADT t, Constraints t c, Alternative f)
+         => (forall s. c s => s -> s -> f s) -> t -> t -> f t
+zipWithA f = runZip $ generic @c $ Zip f
+{-# INLINE zipWithA #-}
 
 -- |
 -- @
--- liftCompare = mzipWith1 (For :: For Ord1) liftCompare
+-- `liftCompare` = `mzipWith1` \@`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)
+mzipWith1 :: forall c t m a. (ADT1 t, Constraints1 t c, Monoid m)
+          => (forall s b. c s => (b -> b -> m) -> s b -> s b -> m)
           -> (a -> a -> m) -> t a -> t a -> m
-mzipWith1 for f = dimap inm2 outm2 $ zipWithA1 for $ dimap outm2 inm2 f
+mzipWith1 f = dimap inm2 outm2 $ zipWithA1 @c $ dimap outm2 inm2 f
+{-# INLINE mzipWith1 #-}
 
-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))
+zipWithA1 :: forall c t f a b. (ADT1 t, Constraints1 t c, Alternative f)
+          => (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 = dimap Zip runZip $ generic1 for $ dimap runZip Zip f
-
+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))
-instance Applicative f => GenericRecordProfunctor (Zip f) where
+  {-# 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
-instance Alternative f => GenericNonEmptyProfunctor (Zip f) where
+  {-# 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
-instance Alternative f => GenericProfunctor (Zip f) where
+  {-# 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 #-}
 outm2 :: Monoid m => (t -> t -> Compose Maybe (Const m) a) -> t -> t -> m
 outm2 f = maybe mempty getConst .: getCompose .: f
+{-# INLINE outm2 #-}
 
 -- | Implement a nullary operator by calling the operator for each component.
 --
 -- @
--- `mempty` = `nullaryOp` (`For` :: `For` `Monoid`) `mempty`
--- `fromInteger` i = `nullaryOp` (`For` :: `For` `Num`) (`fromInteger` i)
+-- `mempty` = `nullaryOp` \@`Monoid` `mempty`
+-- `fromInteger` i = `nullaryOp` \@`Num` (`fromInteger` i)
 -- @
 --
 -- `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
+nullaryOp :: forall c t. (ADTRecord t, Constraints t c)
+          => (forall s. c s => s) -> t
+nullaryOp f = unTagged $ record @c $ Tagged f
+{-# INLINE nullaryOp #-}
 
 -- | Implement a unary operator by calling the operator on the components.
 -- This is here for consistency, it is the same as `record`.
 --
 -- @
--- `negate` = `unaryOp` (`For` :: `For` `Num`) `negate`
+-- `negate` = `unaryOp` \@`Num` `negate`
 -- @
-unaryOp :: (ADTRecord t, Constraints t c)
-        => for c -> (forall s. c s => s -> s) -> t -> t
-unaryOp = record
+unaryOp :: forall c t. (ADTRecord t, Constraints t c)
+        => (forall s. c s => s -> s) -> t -> t
+unaryOp = record @c
+{-# INLINE unaryOp #-}
 
 -- | Implement a binary operator by calling the operator on the components.
 --
 -- @
--- `mappend` = `binaryOp` (`For` :: `For` `Monoid`) `mappend`
--- (`+`) = `binaryOp` (`For` :: `For` `Num`) (`+`)
+-- `mappend` = `binaryOp` \@`Monoid` `mappend`
+-- (`+`) = `binaryOp` \@`Num` (`+`)
 -- @
 --
 -- `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 = algebra for (\(Pair a b) -> f a b) .: Pair
+binaryOp :: forall c t. (ADTRecord t, Constraints t c)
+         => (forall s. c s => s -> s -> s) -> t -> t -> t
+binaryOp f = algebra @c (\(Pair a b) -> f a b) .: Pair
+{-# INLINE binaryOp #-}
 
 -- | Create a value of a record type (with exactly one constructor), given
 -- how to construct the components, under an applicative effect.
@@ -279,46 +318,53 @@
 -- @
 --
 -- `createA'` is `record` specialized to `Joker`.
-createA' :: (ADTRecord t, Constraints t c, Applicative f)
-         => for c -> (forall s. c s => f s) -> f t
-createA' for f = runJoker $ record for $ Joker f
+createA' :: forall c t f. (ADTRecord t, Constraints t c, Applicative f)
+         => (forall s. c s => f s) -> f t
+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.
 --
 -- @
--- `binaryOp` for f l r = `algebra` for (\\(Pair a b) -> f a b) (Pair l r)
+-- `binaryOp` f l r = `algebra` \@c (\\(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
+algebra :: forall c t f. (ADTRecord t, Constraints t c, Functor f)
+        => (forall s. c s => f s -> s) -> f t -> t
+algebra f = runCostar $ record @c $ Costar f
+{-# INLINE algebra #-}
 
 -- | `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
+dialgebra :: forall c t f g. (ADTRecord t, Constraints t c, Functor f, Applicative g)
+        => (forall s. c s => f s -> g s) -> f t -> g t
+dialgebra f = runBiff $ record @c $ Biff f
+{-# INLINE dialgebra #-}
 
 -- | `createA1'` is `record1` specialized to `Joker`.
-createA1' :: (ADTRecord1 t, Constraints1 t c, Applicative f)
-         => for c -> (forall b s. c s => f b -> f (s b)) -> f a -> f (t a)
-createA1' for f = dimap Joker runJoker $ record1 for $ dimap runJoker Joker f
+createA1' :: forall c t f a. (ADTRecord1 t, Constraints1 t c, Applicative f)
+         => (forall b s. c s => f b -> f (s b)) -> f a -> f (t a)
+createA1' f = dimap Joker runJoker $ record1 @c $ dimap runJoker Joker f
+{-# INLINE createA1' #-}
 
 -- |
 --
 -- @
--- cotraverse = `gcotraverse1` (`For` :: `For` `Distributive`) `cotraverse`
+-- cotraverse = `gcotraverse1` \@`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)
+gcotraverse1 :: forall c t f a b. (ADTRecord1 t, Constraints1 t c, Functor f)
+             => (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/Internal.hs b/src/Generics/OneLiner/Internal.hs
--- a/src/Generics/OneLiner/Internal.hs
+++ b/src/Generics/OneLiner/Internal.hs
@@ -18,8 +18,10 @@
   , TypeFamilies
   , TypeOperators
   , ConstraintKinds
+  , TypeApplications
   , FlexibleContexts
   , FlexibleInstances
+  , AllowAmbiguousTypes
   , ScopedTypeVariables
   , UndecidableInstances
   , MultiParamTypeClasses
@@ -36,243 +38,347 @@
 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
 
 
-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' (K1 i a) c = c a
-type instance Constraints' (M1 i t f) c = Constraints' f c
+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
 
-class ADT' (t :: * -> *) where
-  generic' :: (Constraints' t c, GenericProfunctor p)
-    => for c -> (forall s. c s => p s s) -> p (t x) (t x)
+type ADT' = ADT_ Identity Proxy ADTProfunctor
+type ADTNonEmpty' = ADT_ Identity Proxy NonEmptyProfunctor
+type ADTRecord' = ADT_ Identity Proxy RecordProfunctor
 
-class ADTNonEmpty' (t :: * -> *) where
-  nonEmpty' :: (Constraints' t c, GenericNonEmptyProfunctor p)
-    => for c -> (forall s. c s => p s s) -> p (t x) (t x)
+type ADT1' = ADT_ Identity Identity ADTProfunctor
+type ADTNonEmpty1' = ADT_ Proxy Identity NonEmptyProfunctor
+type ADTRecord1' = ADT_ Proxy Identity RecordProfunctor
 
-class ADTRecord' (t :: * -> *) where
-  record' :: (Constraints' t c, GenericRecordProfunctor p)
-    => for c -> (forall s. c s => p s s) -> p (t x) (t x)
+type ADTProfunctor = GenericEmptyProfunctor ': NonEmptyProfunctor
+type NonEmptyProfunctor = GenericSumProfunctor ': RecordProfunctor
+type RecordProfunctor = '[GenericProductProfunctor, GenericUnitProfunctor, Profunctor]
 
-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)
+type family Satisfies (p :: * -> * -> *) (ks :: [(* -> * -> *) -> Constraint]) :: Constraint
+type instance Satisfies p (k ': ks) = (k p, Satisfies p ks)
+type instance Satisfies p '[] = ()
 
-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)
+class (ks :: [(* -> * -> *) -> Constraint]) |- (k :: (* -> * -> *) -> Constraint) where
+  (|-) :: Satisfies p ks => proxy0 ks -> proxy1 k -> (k p => p a b) -> p a b
 
-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 {-# OVERLAPPABLE #-} ks |- k => (_k ': ks) |- k where
+  (_ :: proxy0 (_k ': ks)) |- proxy1 = (Proxy :: Proxy ks) |- proxy1
+  {-# INLINE (|-) #-}
 
+instance (k ': _ks) |- k where
+  _ |- _ = id
+  {-# INLINE (|-) #-}
 
-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' (K1 i v) c = ()
-type instance Constraints1' (M1 i t f) c = Constraints1' f c
+generic' :: forall t c p ks a b proxy0 for. (ADT_ Identity Proxy ks t, Constraints' t c AnyType, Satisfies p ks)
+         => proxy0 ks
+         -> for c
+         -> (forall s. c 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' #-}
 
-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)
+nonEmpty1' :: forall t c1 p ks a b proxy0 for. (ADT_ Proxy Identity ks t, Constraints' t AnyType c1, Satisfies p ks)
+           => proxy0 ks
+           -> for c1
+           -> (forall s d e. c1 s => p d e -> p (s d) (s e))
+           -> p a b
+           -> p (t a) (t b)
+nonEmpty1' proxy0 for f p = generic_ proxy0 (Proxy :: Proxy Proxy) (Proxy :: Proxy AnyType) Proxy for (Identity f) (Identity p)
+{-# INLINE nonEmpty1' #-}
 
-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)
+generic1' :: forall t c1 p ks a b proxy0 for. (ADT_ Identity Identity ks t, Constraints' t AnyType c1, Satisfies p ks, ks |- GenericEmptyProfunctor)
+          => proxy0 ks
+          -> for c1
+          -> (forall s d e. c1 s => p d e -> p (s d) (s e))
+          -> p a b
+          -> p (t a) (t b)
+generic1' proxy0 for f p = (proxy0 |- (Proxy :: Proxy GenericEmptyProfunctor))
+  (generic_ proxy0 (Proxy :: Proxy Identity) (Proxy :: Proxy AnyType) (Identity identity) for (Identity f) (Identity p))
+{-# INLINE generic1' #-}
 
-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)
+class ADT_ (nullary :: * -> *) (unary :: * -> *) (ks :: [(* -> * -> *) -> Constraint]) (t :: * -> *) where
+  generic_ :: (Constraints' t c c1, Satisfies p ks)
+           => proxy0 ks
+           -> proxy1 nullary
+           -> for c
+           -> (forall s. c s => nullary (p s s))
+           -> for1 c1
+           -> (forall s1 d e. c1 s1 => unary (p d e -> p (s1 d) (s1 e)))
+           -> unary (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' (K1 i v) where generic1' _ _ _ = dimap unK1 K1 identity
-instance ADT1' f => ADT1' (M1 i t f) where generic1' for f p = dimap unM1 M1 (generic1' for f p)
+instance ks |- GenericEmptyProfunctor => ADT_ nullary unary ks V1 where
+  generic_ proxy0 _ _ _ _ _ _ = (proxy0 |- (Proxy :: Proxy GenericEmptyProfunctor)) zero
+  {-# INLINE generic_ #-}
 
-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 ks |- GenericUnitProfunctor => ADT_ nullary unary ks U1 where
+  generic_ proxy0 _ _ _ _ _ _ = (proxy0 |- (Proxy :: Proxy GenericUnitProfunctor)) unit
+  {-# INLINE generic_ #-}
 
-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)
+instance (ks |- GenericSumProfunctor, ADT_ nullary unary ks f, ADT_ nullary unary ks g) => ADT_ nullary unary ks (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
+  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
+  generic_ proxy0 _ _ f _ _ _ = (proxy0 |- (Proxy :: Proxy Profunctor)) (dimap unK1 K1 (runIdentity f))
+  {-# INLINE generic_ #-}
+
+instance (ks |- Profunctor, ADT_ nullary unary ks f) => ADT_ nullary unary ks (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
+  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
+  generic_ proxy0 _ _ _ _ _ p = (proxy0 |- (Proxy :: Proxy Profunctor))
+    (dimap unPar1 Par1 (runIdentity p))
+  {-# INLINE generic_ #-}
+
+instance ks |- Profunctor => ADT_ nullary Identity ks (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 GenericUnitProfunctor p where
+  unit :: p (U1 a) (U1 a')
+
+class GenericProductProfunctor p where
+  mult :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :*: g) a) ((f' :*: g') a')
+
+class GenericSumProfunctor p where
+  plus :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :+: g) a) ((f' :+: g') a')
+
+class 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 => 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')
+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 => GenericNonEmptyProfunctor p where
-  plus :: p (f a) (f' a') -> p (g a) (g' a') -> p ((f :+: g) a) ((f' :+: g') a')
+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 => GenericProfunctor p where
-  identity :: p a a
-  zero :: p (V1 a) (V1 a')
-  zero = lmap absurd identity
+class (GenericNonEmptyProfunctor p, GenericEmptyProfunctor p) => GenericProfunctor p where
+instance (GenericNonEmptyProfunctor p, GenericEmptyProfunctor p) => GenericProfunctor p where
 
-instance GenericRecordProfunctor (->) where
+instance GenericUnitProfunctor (->) where
   unit _ = U1
+  {-# INLINE unit #-}
+instance GenericProductProfunctor (->) where
   mult f g (l :*: r) = f l :*: g r
-instance GenericNonEmptyProfunctor (->) where
+  {-# INLINE mult #-}
+instance GenericSumProfunctor (->) where
   plus f g = e1 (L1 . f) (R1 . g)
-instance GenericProfunctor (->) where
+  {-# INLINE plus #-}
+instance GenericEmptyProfunctor (->) where
   zero = absurd
+  {-# INLINE zero #-}
   identity = id
+  {-# INLINE identity #-}
 
-instance GenericRecordProfunctor Tagged where
+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 => GenericRecordProfunctor (Star f) where
+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
-instance Applicative f => GenericNonEmptyProfunctor (Star f) where
+  {-# INLINE mult #-}
+instance Applicative f => GenericSumProfunctor (Star f) where
   plus (Star f) (Star g) = Star $ e1 (fmap L1 . f) (fmap R1 . g)
-instance Applicative f => GenericProfunctor (Star f) where
+  {-# INLINE plus #-}
+instance Applicative f => GenericEmptyProfunctor (Star f) where
   zero = Star absurd
+  {-# INLINE zero #-}
   identity = Star pure
+  {-# INLINE identity #-}
 
-instance Functor f => GenericRecordProfunctor (Costar f) where
+instance 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, GenericRecordProfunctor p) => GenericRecordProfunctor (Biff p f g) where
+instance (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 => GenericRecordProfunctor (Joker f) where
+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
-instance Alternative f => GenericNonEmptyProfunctor (Joker f) where
+  {-# INLINE mult #-}
+instance Alternative f => GenericSumProfunctor (Joker f) where
   plus (Joker l) (Joker r) = Joker $ L1 <$> l <|> R1 <$> r
-instance Alternative f => GenericProfunctor (Joker f) where
+  {-# INLINE plus #-}
+instance Alternative f => GenericEmptyProfunctor (Joker f) where
   zero = Joker empty
+  {-# INLINE zero #-}
   identity = Joker empty
+  {-# INLINE identity #-}
 
-instance Divisible f => GenericRecordProfunctor (Clown f) where
+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
-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
+  {-# 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 (GenericRecordProfunctor p, GenericRecordProfunctor q) => GenericRecordProfunctor (Product p q) where
+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)
-instance (GenericNonEmptyProfunctor p, GenericNonEmptyProfunctor q) => GenericNonEmptyProfunctor (Product p q) where
+  {-# 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)
-instance (GenericProfunctor p, GenericProfunctor q) => GenericProfunctor (Product p q) where
+  {-# 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, GenericRecordProfunctor p) => GenericRecordProfunctor (Tannen f p) where
+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
-instance (Applicative f, GenericNonEmptyProfunctor p) => GenericNonEmptyProfunctor (Tannen f p) where
+  {-# INLINE mult #-}
+instance (Applicative f, GenericSumProfunctor p) => GenericSumProfunctor (Tannen f p) where
   plus (Tannen l) (Tannen r) = Tannen $ liftA2 plus l r
-instance (Applicative f, GenericProfunctor p) => GenericProfunctor (Tannen f p) where
+  {-# 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
-instance GenericRecordProfunctor Ctor where
+  {-# INLINE dimap #-}
+instance GenericUnitProfunctor Ctor where
   unit = Ctor (const 0) 1
+  {-# INLINE unit #-}
+instance GenericProductProfunctor Ctor where
   mult _ _ = Ctor (const 0) 1
-instance GenericNonEmptyProfunctor Ctor where
+  {-# INLINE mult #-}
+instance GenericSumProfunctor Ctor where
   plus l r = Ctor (e1 (index l) ((count l + ) . index r)) (count l + count r)
-instance GenericProfunctor Ctor where
+  {-# INLINE plus #-}
+instance GenericEmptyProfunctor Ctor where
   zero = Ctor (const 0) 0
+  {-# INLINE zero #-}
   identity = Ctor (const 0) 1
+  {-# INLINE identity #-}
 
-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
+record :: forall c p t. (ADTRecord t, Constraints t c, GenericRecordProfunctor p)
+       => (forall s. c s => p s s) -> p t t
+record f = dimap from to $ generic' (Proxy :: Proxy RecordProfunctor) (Proxy :: Proxy c) f
+{-# INLINE record #-}
 
-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
+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 f p = dimap from1 to1 $ nonEmpty1' (Proxy :: Proxy RecordProfunctor) (Proxy :: Proxy c) f p
+{-# INLINE record1 #-}
 
-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
+nonEmpty :: forall c p t. (ADTNonEmpty t, Constraints t c, GenericNonEmptyProfunctor p)
+         => (forall s. c s => p s s) -> p t t
+nonEmpty f = dimap from to $ generic' (Proxy :: Proxy NonEmptyProfunctor) (Proxy :: Proxy c) f
+{-# INLINE nonEmpty #-}
 
-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
+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 f p = dimap from1 to1 $ nonEmpty1' (Proxy :: Proxy NonEmptyProfunctor) (Proxy :: Proxy c) f p
+{-# INLINE nonEmpty1 #-}
 
-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 $ generic' for f
+generic :: forall c p t. (ADT t, Constraints t c, GenericProfunctor p)
+        => (forall s. c s => p s s) -> p t t
+generic f = dimap from to $ generic' (Proxy :: Proxy ADTProfunctor) (Proxy :: Proxy c) f
+{-# INLINE generic #-}
 
-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
+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 f p = dimap from1 to1 $ generic1' (Proxy :: Proxy ADTProfunctor) (Proxy :: Proxy c) f p
+{-# INLINE generic1 #-}
 
 -- | `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
+type Constraints t c = Constraints' (Rep t) c AnyType
 
-type Constraints1 t c = Constraints1' (Rep1 t) c
+type Constraints1 t c = Constraints' (Rep1 t) AnyType c
 
 -- | `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)
@@ -290,63 +396,60 @@
 
 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 :: k -> Constraint) = For
-
 -- | 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` (`For` :: `For` `Binary`) `put` t
+-- `put` t = `putWord8` (`toEnum` (`ctorIndex` t)) `<>` `gfoldMap` \@`Binary` `put` t
 -- @
 ctorIndex :: ADT t => t -> Int
-ctorIndex = index $ generic (For :: For AnyType) (Ctor (const 0) 1)
+ctorIndex = index $ generic @AnyType (Ctor (const 0) 1)
+{-# INLINE ctorIndex #-}
 
 ctorIndex1 :: ADT1 t => t a -> Int
-ctorIndex1 = index $ generic1 (For :: For AnyType) (const $ Ctor (const 0) 1) (Ctor (const 0) 1)
+ctorIndex1 = index $ generic1 @AnyType (const $ Ctor (const 0) 1) (Ctor (const 0) 1)
+{-# INLINE ctorIndex1 #-}
 
--- | Any type is instance of `AnyType`, you can use it with @For :: For 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
-instance AnyType a
+class AnyType (a :: k)
+instance AnyType (a :: k)
 
 -- | The result type of a curried function.
 --
 -- If @r@ is not a function type (i.e., does not unify with `_ -> _`):
 --
 -- @
--- `Result` (a -> r) ~ r
--- `Result` (a -> b -> r) ~ r
--- `Result` (a -> b -> c -> r) ~ r
+-- `FunResult` (a -> r) ~ r
+-- `FunResult` (a -> b -> r) ~ r
+-- `FunResult` (a -> b -> c -> r) ~ r
 -- @
-type family Result t where
-  Result (a -> b) = Result b
-  Result r = r
+type family FunResult t where
+  FunResult (a -> b) = FunResult b
+  FunResult r = r
 
 -- | Automatically apply a lifted function to a polymorphic argument as
 -- many times as possible.
 --
--- A constraint `FunConstraint t c` is equivalent to the conjunction of
+-- A constraint `FunConstraint c t` is equivalent to the conjunction of
 -- constraints `c s` for every argument type of `t`.
 --
 -- If @r@ is not a function type:
 --
 -- @
--- c a :- FunConstraints (a -> r) c
--- (c a, c b) :- FunConstraints (a -> b -> r) c
--- (c a, c b, c d) :- FunConstraints (a -> b -> d -> r) c
+-- c a :- FunConstraints c (a -> r)
+-- (c a, c b) :- FunConstraints c (a -> b -> r)
+-- (c a, c b, c d) :- FunConstraints c (a -> b -> d -> r)
 -- @
-class FunConstraints t c where
-  autoApply :: Applicative f => for c -> (forall s. c s => f s) -> f t -> f (Result t)
+class FunConstraints c t where
+  autoApply :: Applicative f => (forall s. c s => f s) -> f t -> f (FunResult t)
 
-instance {-# OVERLAPPING #-} (c a, FunConstraints b c) => FunConstraints (a -> b) c where
-  autoApply for run f = autoApply for run (f <*> run)
+instance {-# OVERLAPPING #-} (c a, FunConstraints c b) => FunConstraints c (a -> b) where
+  autoApply run f = autoApply @c run (f <*> run)
+  {-# INLINE autoApply #-}
 
-instance Result r ~ r => FunConstraints r c where
-  autoApply _for _run r = r
+instance FunResult r ~ r => FunConstraints c r where
+  autoApply _run r = r
+  {-# INLINE autoApply #-}
diff --git a/test/unittests.hs b/test/unittests.hs
new file mode 100644
--- /dev/null
+++ b/test/unittests.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+
+import Data.Functor.Contravariant
+import Data.Functor.Identity
+import GHC.Generics
+import Test.HUnit
+import Generics.OneLiner
+
+data T a = T0 | T1 a | T2 a a deriving (Eq, Show, Generic, Generic1)
+data Pair a = Pair a a deriving (Eq, Show, Generic, Generic1)
+
+create0 :: (ADT t, Constraints t ((~) Int)) => [t]
+create0 = create @((~) Int) [0]
+
+testCreate = "create" ~:
+  [ "Identity" ~: create0 ~?= [Identity 0]
+  , "()"       ~: create0 ~?= [()]
+  , "(,)"      ~: create0 ~?= [(0, 0)]
+  , "Either"   ~: create0 ~?= [Left 0, Right 0]
+  , "Maybe"    ~: create0 ~?= [Nothing, Just 0]
+  , "T"        ~: create0 ~?= [T0, T1 0, T2 0 0]
+  ]
+
+createA10 :: ADT1 t => [t Int]
+createA10 = createA1 @AnyType (const []) [0]
+
+testCreateA1 = "createA1" ~:
+  [ "Identity" ~: createA10 ~?= [Identity 0]
+  , "(,)"      ~: createA10 ~?= ([] :: [(String, Int)])
+  , "Either"   ~: createA10 ~?= [Right 0 :: Either String Int]
+  , "Maybe"    ~: createA10 ~?= [Nothing, Just 0]
+  , "T"        ~: createA10 ~?= [T0, T1 0, T2 0 0]
+  ]
+
+nullaryOp0 :: (ADTRecord t, Constraints t ((~) Int)) => t
+nullaryOp0 = nullaryOp @((~) Int) 0
+
+testNullaryOp = "nullaryOp" ~:
+  [ "Identity" ~: nullaryOp0 ~?= Identity 0
+  , "()"       ~: nullaryOp0 ~?= ()
+  , "(,)"      ~: nullaryOp0 ~?= (0, 0)
+  ]
+
+createA1'0 :: ADTRecord1 t => [t Int]
+createA1'0 = createA1' @AnyType (const []) [0]
+
+testCreateA1' = "createA1'" ~:
+  [ "Identity" ~: createA1'0 ~?= [Identity 0]
+  , "Pair"     ~: createA1'0 ~?= [Pair 0 0]
+  ]
+
+main = runTestTT $ test
+  [ testCreate
+  , testCreateA1
+  , testNullaryOp
+  ]