diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,13 +1,40 @@
+# Version 0.4
+
+* COMPILER ASSISTED BREAKING CHANGE: Fixed `TypeApplications` for `flay1` so
+  that @c@ comes first.
+
+* COMPILER ASSISTED BREAKING CHANGE: Not exporting `GFlay'`, `gflay'`,
+  `gterminal` anymore.
+
+* COMPILER ASSISTED BREAKING CHANGE: `GFlay` and `All` are now type synonyms
+  rather than classes.
+
+* COMPILER ASSISTED BREAKING CHANGE: `Flayable1` is not a typeclass anymore.
+  Now it is a type synonym for `Flayable` using “quantified constraints” as
+  implemented in `Data.Constraint.Forall`. Accordingly, `flay1` is not a
+  typeclass method anymore.
+
+* `Generic` types parametrized by a type constructor who have *all* of their
+  immediate children fields using said type constructor get a `Flayable`
+  instance for free.
+
+* Added `pump`, `dump`, `Pump` and `GPump`.
+
+* Added `GTerminal` instance for `GHC.Generics.U1`.
+
+* Added `Fields`, `GFields`, `FieldsF` and `GFieldsF`.
+
+
 # Version 0.3
 
-* `zip`, `zip1` and `unsafeZip` now take a monadic pairing function, and return
+* BREAKING CHANGE: `zip`, `zip1` and `unsafeZip` now take a monadic pairing function, and return
   `Maybe` where `Nothing` happens in the target indexes do not match.
 
+* BREAKING CHANGE: Remove `Record` and `GRecord`.
+
 * Added `trivialize`.
 
 * Generalized type of `trivial'`.
-
-* Remove `Record` and `GRecord`.
 
 
 # Version 0.2
diff --git a/LICENSE.txt b/LICENSE.txt
--- a/LICENSE.txt
+++ b/LICENSE.txt
@@ -1,4 +1,4 @@
-Copyright (c) 2017, Renzo Carbonara
+Copyright (c) 2017-2018, Renzo Carbonara
 
 All rights reserved.
 
diff --git a/default.nix b/default.nix
deleted file mode 100644
--- a/default.nix
+++ /dev/null
@@ -1,1 +0,0 @@
-(import ./release.nix {}).flay
diff --git a/flay.cabal b/flay.cabal
--- a/flay.cabal
+++ b/flay.cabal
@@ -1,11 +1,11 @@
 name: flay
-version: 0.3
+version: 0.4
 author: Renzo Carbonara
 maintainer: renλren!zone
-copyright: Renzo Carbonara 2017
+copyright: Renzo Carbonara 2017-2018
 license: BSD3
 license-file: LICENSE.txt
-extra-source-files: README.md CHANGELOG.md pkg.nix shell.nix default.nix release.nix
+extra-source-files: README.md CHANGELOG.md
 category: Data, Generics
 build-type: Simple
 cabal-version: >=1.18
@@ -39,6 +39,7 @@
     base,
     flay,
     tasty,
-    tasty-quickcheck
+    tasty-quickcheck,
+    transformers
 
 
diff --git a/pkg.nix b/pkg.nix
deleted file mode 100644
--- a/pkg.nix
+++ /dev/null
@@ -1,12 +0,0 @@
-{ mkDerivation, base, constraints, stdenv, tasty, tasty-quickcheck, transformers
-}:
-mkDerivation {
-  pname = "flay";
-  version = "0.3";
-  src = ./.;
-  libraryHaskellDepends = [ base constraints transformers ];
-  testHaskellDepends = [ base tasty tasty-quickcheck ];
-  homepage = "https://github.com/k0001/flay";
-  description = "Work on your datatype without knowing its shape nor its contents";
-  license = stdenv.lib.licenses.bsd3;
-}
diff --git a/release.nix b/release.nix
deleted file mode 100644
--- a/release.nix
+++ /dev/null
@@ -1,12 +0,0 @@
-{ nixpkgs ? builtins.fetchTarball channel:nixos-18.03
-}:
-
-let
-pkgs = import nixpkgs {};
-ghc841 = pkgs.haskell.packages.ghc841.override {
-  packageSetConfig = self: super: {
-    flay = super.callPackage ./pkg.nix {};
-  };
-};
-
-in { inherit (ghc841) flay; }
diff --git a/shell.nix b/shell.nix
deleted file mode 100644
--- a/shell.nix
+++ /dev/null
@@ -1,1 +0,0 @@
-(import ./default.nix).env
diff --git a/src/Flay.hs b/src/Flay.hs
--- a/src/Flay.hs
+++ b/src/Flay.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
@@ -28,14 +29,15 @@
 -- @
 module Flay
  ( Flay
- , inner
  -- * Flayable
  , Flayable(flay)
- , Flayable1(flay1)
+ , Flayable1
+ , flay1
  -- ** Generics
  , gflay
  , GFlay
- , GFlay'(gflay')
+ -- , gflay1
+ -- , GFlay1
  -- ** Utils
  , All
  , Trivial
@@ -51,8 +53,18 @@
  , unsafeZip
  , terminal
  , Terminal
- , GTerminal(gterminal)
- -- ** Re-exports
+ , GTerminal
+ -- * Pump & Dump
+ , Pump
+ , GPump
+ , pump
+ , dump
+ -- * Miscellaneous
+ , Fields
+ , GFields
+ , FieldsF
+ , GFieldsF
+ -- * Re-exports
  , Dict(Dict)
  ) where
 
@@ -63,10 +75,10 @@
 import Data.Dynamic (Dynamic, toDyn, fromDynamic)
 import Data.Functor.Product (Product(Pair))
 import Data.Functor.Const (Const(Const, getConst))
-import Data.Functor.Identity (Identity(runIdentity))
 import Data.Typeable (Typeable)
 import qualified GHC.Generics as G
 import Prelude hiding (zip)
+import Unsafe.Coerce (unsafeCoerce)
 
 --------------------------------------------------------------------------------
 
@@ -75,8 +87,13 @@
 -- @(forall a. c a => f a -> m (g a))@ to targeted occurences of @f a@ inside
 -- @s@.
 --
--- A 'Flay' must obey the 'inner' identity law.
+-- A 'Flay' must obey the following identity law:
 --
+-- @
+-- forall (fl :: 'Flay' c s t f g).
+--    fl ('const' 'pure')  ==  'pure'
+-- @
+--
 -- When defining 'Flay' values, you should leave @c@, @f@, and @g@ fully
 -- polymorphic, as these are the most useful types of 'Flay's.
 --
@@ -89,7 +106,13 @@
 --
 -- /to flay: tr. v., to strip off the skin or surface of./
 --
--- /Mnemonic for @c s t f g@: Common STandard FoG./
+-- Mnemonic for @c s t f g@: Much like lenses have type indexes @s t a b@ where
+-- @s@ is the input state, @t@ is the output state, and @a@ and @b@ are the
+-- input and output /values/ respectively, in 'Flay', @s@ and @t@ represent the
+-- input and output states like in lenses, and @f@ and @g@ represent the
+-- /wrappers/ over the input and output values respectively. The @c@ comes at
+-- the very beginning because it is the type you are expected to apply with
+-- 'TypeApplications' if necessary.
 --
 -- ==== Example 1: Removing uncertainty
 --
@@ -280,8 +303,16 @@
 -- explicitly type the received @'Dict'@ unless the @c@ argument to 'Flay' has
 -- been explicitly by other means (like in the definition of 'trivial'', where
 -- we don't have to explicitly type 'Dict' because @c ~ 'Trivial'@ according to
--- the top level signature of 'trivial'').
+-- the top level signature of 'trivial''). Using the @TypeApplications@ GHC
+-- extension might make things easier:
 --
+-- @
+-- fooMaybeToIdentityIO :: Foo 'Maybe' -> 'IO' (Foo 'Identity')
+-- fooMaybeToIdentityIO = flayFoo @Read (\\'Dict' -> \\case
+--     'Nothing' -> 'fmap' 'pure' prompt
+--     'Just' a -> 'pure' ('pure' a))
+-- @
+--
 -- Example using this in GHCi:
 --
 -- @
@@ -327,65 +358,118 @@
   = forall m. Applicative m
        => (forall (a :: k). Dict (c a) -> f a -> m (g a)) -> s -> m t
 
--- | Inner identity law:
---
--- @
--- (\\fl -> 'runIdentity' . 'trivial'' fl 'pure') = 'id'
--- @
-inner :: Flay Trivial s s f f -> s -> s
-inner fl = runIdentity . trivial' fl pure
-
 --------------------------------------------------------------------------------
 
 -- | Default 'Flay' implementation for @s@ and @t@.
 --
 -- When defining 'Flayable' instances, you should leave @c@, @f@, and @g@
 -- fully polymomrphic, as these are the most useful types of 'Flayables's.
-class Flayable (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *) | s -> f, t -> g, s g -> t, t f -> s where
-  -- | If @s@ and @t@ are instances of 'G.Generic', then 'gflay' can be used as
-  -- default implementation for 'flay'. For example, provided the @Foo@ datatype
-  -- shown in the documentation for 'Flay' had a 'G.Generic' instance, then the
-  -- following 'Flayable' instance would get a default implementation for
-  -- 'flay':
-  --
-  -- @
-  -- instance (c 'Int', c 'Bool') => 'Flayable' c (Foo f) (Foo g) f g where
-  --   'flay' = 'gflay'
-  -- @
-  --
-  -- Notice that 'flay' can be defined in terms of 'flay1' as well.
-  --
-  -- /Implementors note:/ Unfortunately, due to some strange bug in GHC, we
-  -- can't use @DefaultSignatures@ to say @'flay' = 'gflay'@, because when doing
-  -- that the kind of @c@ infers incorrectly.
+--
+-- If @s@ and @t@ are instances of 'G.Generic', then 'gflay' can be used as
+-- default implementation for 'flay'. For example, provided the following
+-- datatype and its 'G.Generic' instance:
+--
+-- @
+-- data Foo f = Foo (f 'Int') (f 'Bool')
+--   deriving ('G.Generic')
+-- @
+-- Then the following 'Flayable' instance would get a default implementation for
+-- 'flay':
+--
+-- @
+-- instance (c 'Int', c 'Bool') => 'Flayable' c (Foo f) (Foo g) f g
+-- @
+--
+-- But actually, this library exports an @OVERLAPPABLE@ instance that covers
+-- datatypes like 'Foo' above. That is, datatypes parametrized by some type
+-- constructor where that type constructor wraps each of the immediate children
+-- fields. So
+-- /most times you don't even need to write the 'Flayable' instance yourself/.
+-- That is, a @'Flayable' c (r f) (r g) f g@ for @r@ types parametrized by a
+-- type-constructor, such as 'Foo', having 'G.Generic' instances.
+--
+-- In cases where you do need to define the 'Flayable' instance yourself, you'll
+-- notice that constraints applying @c@ to every immediate child field type will
+-- bubble up, such as @(c 'Int', c 'Bool')@ in the example above. This module
+-- exports the 'FieldsF' constraint that can be used to reduce that boilerplate
+-- for datatypes that implement 'G.Generic', tackling all of the fields at once.
+-- That is, the 'Flayable' instance for 'Foo' above could have been written like
+-- this:
+--
+-- @
+-- instance 'FieldsF' c Foo => 'Flayable' c (Foo f) (Foo g) f g
+-- @
+--
+-- Notice that 'flay' can be defined in terms of 'flay1' as well.
+class Flayable (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+  | s -> f, t -> g, s g -> t, t f -> s where
   flay :: Flay c s t f g
+  default flay :: GFlay c s t f g => Flay c s t f g
+  flay = gflay
+  {-# INLINE flay #-}
 
+-- | All datatypes parametrized over some type constructor @f :: k -> *@ that
+-- have a 'G.Generic' instance get a 'Flayable' instance for free. For example:
+--
+-- @
+-- data Foo f = Foo (f 'Int') (f 'Bool')
+--   deriving ('G.Generic')
+-- @
+--
+-- This is an @OVERLAPPABLE@ instance, meaning that you can provide a different
+-- instance for your 'G.Generic' datatype, if necessary.
+instance {-# OVERLAPPABLE #-}
+  GFlay c (r f) (r g) f g
+  => Flayable c (r f) (r g) f g where
+  flay = gflay
+  {-# INLINE flay #-}
+
 --------------------------------------------------------------------------------
 
 -- | 'Flayable1' is 'Flayable' specialized for the common case of @s ~ r f@ and
--- @t ~ r g@. The rationale for introducing this seemingly redundant class is
--- that the 'Flayable1' constraint is less verbose than 'Flayable'.
+-- @t ~ r g@. The rationale for introducing this seemingly redundant constraint
+-- is that 'Flayable1' is less verbose than 'Flayable'.
 --
--- Unfortunately, we can't readily existentialize the arguments to 'Flayable',
--- which is why you'll need to specify both 'Flayable1' and 'Flayable'
--- instances. Notice, however, that 'flay1' can be defined in terms of
--- 'flay' and vice-versa, so this should be very mechanical.
-class Flayable1 (c :: k -> Constraint) (r :: (k -> *) -> *) where
-  -- | If @r f@ and @r g@ are instances of 'G.Generic', then 'flay1' gets a
-  -- default implementation. For example, provided the @Foo@ datatype shown in
-  -- the documentation for 'Flay' had a 'G.Generic' instance, then the following
-  -- 'Flayable' instance would get a default implementation for 'flay1':
-  --
-  -- @
-  -- instance (c 'Int', c 'Bool') => 'Flayable1' c Foo
-  -- @
-  --
-  -- Notice that 'flay1' can be defined in terms of 'flay' as well.
-  flay1 :: Flay c (r f) (r g) f g
-  default flay1 :: GFlay c (r f) (r g) f g => Flay c (r f) (r g) f g
-  flay1 = gflay
-  {-# INLINE flay1 #-}
+-- In other words, if we had @QuantifiedConstraints@, then 'Flayable1' would be
+-- something like:
+--
+-- @
+-- 'Flayable1' c r
+--    ==  forall (f :: k -> *) (g :: k -> *).
+--           'Flayable' c (r f) (r g) f g
+-- @
 
+-- Implementors note: Currently, 'Flayable1' is uses some of the skolem trickery
+-- described in detail in "Data.Constraint.Forall", specialized to 'Flayable'.
+type family Flayable1 (c :: k -> Constraint) (r :: (k -> *) -> *) :: Constraint where
+  Flayable1 c r = Flayable1_ c r
+
+-- | This inner 'Flayable1_' class prevents the skolem from leaking to the user.
+class Flayable1K c r (Skolem (Flayable1K c r))
+  => Flayable1_ (c :: k -> Constraint) (r :: (k -> *) -> *)
+instance Flayable1K c r (Skolem (Flayable1K c r))
+  => Flayable1_ c r
+
+-- | Like @Flayable c (r F) (r G) F G@, but with a superfluous trailing @x@
+-- to match the kind expected by 'Skolem'.
+class Flayable c (r F) (r G) F G
+  => Flayable1K (c :: k -> Constraint) (r :: (k -> *) -> *) (x :: *)
+instance Flayable c (r F) (r G) F G
+  => Flayable1K c r x
+
+-- The `Skolem` type family represents skolem variables; do not export!
+type family Skolem (p :: k -> Constraint) :: k where
+
+-- | Like 'flay', but specialized to work on 'Flayable1'.
+flay1 :: forall c r f g. Flayable1 c r => Flay c (r f) (r g) f g
+{-# INLINE flay1 #-}
+flay1 =
+  let flFG = flay :: Flay c (r F) (r G) F G
+  in \(h0 :: Dict (c a0) -> f a0 -> m (g a0)) (rf :: r f) ->
+         unsafeCoerce (flFG (unsafeCoerce h0 :: Dict (c a1) -> F a1 -> m (G a1))
+                            (unsafeCoerce rf :: r F)
+                         :: m (r G))
+
 --------------------------------------------------------------------------------
 
 -- | 'Constraint' trivially satisfied by every type.
@@ -407,8 +491,9 @@
 -- all you can do with such @a@ is pass it around.
 --
 -- @
--- 'trivial'' fl h
---    = fl (\\('Dict' :: 'Dict' ('Trivial' a)) (fa :: f a) -> h fa)
+-- forall (fl :: 'Flay' 'Trivial' s t f g)
+--        (h :: 'Applicative' m => 'Dict' 'Trivial' -> f a -> m (g a)).
+-- 'trivial'' fl h  == fl ('const' h)
 -- @
 trivial'
   :: forall m c s t f g
@@ -452,12 +537,9 @@
 
 --------------------------------------------------------------------------------
 
--- | Convenience 'Constraint' for satisfying basic 'GFlay'' needs for @s@ and @t@.
-class (G.Generic s, G.Generic t, GFlay' c (G.Rep s) (G.Rep t) f g)
-  => GFlay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
-instance (G.Generic s, G.Generic t, GFlay' c (G.Rep s) (G.Rep t) f g)
-  => GFlay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
-
+-- | Convenient 'Constraint' for satisfying the requirements of 'gflay'.
+type GFlay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+  = (GFlay' c (G.Rep s) (G.Rep t) f g, G.Generic s, G.Generic t)
 
 gflay :: GFlay c s t f g => Flay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
 gflay = \h s -> G.to <$> gflay' h (G.from s)
@@ -470,10 +552,34 @@
   gflay' _ _ = undefined -- unreachable
   {-# INLINE gflay' #-}
 
+instance GFlay' c G.U1 G.U1 f g where
+  gflay' _ _ = pure G.U1
+  {-# INLINE gflay' #-}
+
 instance c a => GFlay' c (G.K1 r (f a)) (G.K1 r (g a)) f g where
   gflay' h (G.K1 fa) = G.K1 <$> h Dict fa
   {-# INLINE gflay' #-}
 
+{- Enabling this breaks gflay, when used from flay1. This instance is the one that
+   allows us to use GFlay with a datatype where not all its fields are parametrized
+   by some type constructor (e.g., data Foo f = Foo (f Int) Bool).
+
+    • Overlapping instances for Flay.GFlay' c (G.K1 G.R (f Int)) (G.K1 G.R (g Int)) f g
+        arising from a use of ‘Flay.$dmflay1’
+      Matching instances:
+        instance [safe]
+          forall k1 k2 (c :: k2 -> Constraint) (a :: k2) r (f :: k2 -> *) (g :: k2 -> *).
+          c a =>
+          Flay.GFlay' c (G.K1 r (f a)) (G.K1 r (g a)) f g
+        instance [overlappable] [safe]
+          forall k1 k2 (c :: k2 -> Constraint) r a (f :: k2 -> *) (g :: k2 -> *).
+          Flay.GFlay' c (G.K1 r a) (G.K1 r a) f g
+
+instance {-# OVERLAPPABLE #-} GFlay' c (G.K1 r a) (G.K1 r a) f g where
+  gflay' _ (G.K1 a) = pure (G.K1 a)
+  {-# INLINE gflay' #-}
+-}
+
 instance (GFlay' c s t f g)
   => GFlay' c (G.M1 i j s) (G.M1 i j t) f g where
   gflay' h (G.M1 sp) = G.M1 <$> gflay' h sp
@@ -537,24 +643,35 @@
 -- constructed out of thin air.
 class Terminal a where
   terminal :: a
+
 instance Terminal () where
   terminal = ()
   {-# INLINE terminal #-}
+
 instance {-# OVERLAPPABLE #-} (G.Generic a, GTerminal (G.Rep a)) => Terminal a where
   terminal = G.to gterminal
   {-# INLINE terminal #-}
+
 instance Terminal (Const () a) where
   terminal = Const ()
   {-# INLINE terminal #-}
 
+---
 class GTerminal (f :: * -> *) where
   gterminal :: f p
+
+instance GTerminal G.U1 where
+  gterminal = G.U1
+  {-# INLINE gterminal #-}
+
 instance Terminal x => GTerminal (G.K1 i x) where
   gterminal = G.K1 terminal
   {-# INLINE gterminal #-}
+
 instance GTerminal f => GTerminal (G.M1 i c f) where
   gterminal = G.M1 gterminal
   {-# INLINE gterminal #-}
+
 instance (GTerminal l, GTerminal r) => GTerminal (l G.:*: r) where
   gterminal = gterminal G.:*: gterminal
   {-# INLINE gterminal #-}
@@ -651,14 +768,303 @@
 
 --------------------------------------------------------------------------------
 
+-- | Wrapper allowing a 'G.Generic' non 'Flayable' type to become 'Flayable'.
+--
+-- Most datatypes that can have useful 'Flayable' instances are often
+-- parametrized by a type constructor @f :: k -> *@, and have all or some of
+-- their fields wrapped in said @f@, like so:
+--
+-- @
+-- data Foo f = Foo (f 'Int') (f 'Bool')
+-- @
+--
+-- However, that kind of representation is not that common, and it can sometimes
+-- be unconfortable to use, particularly if @f ~ 'Identity'@ due to the
+-- necessary wrapping and unwrapping of values. In Haskell, it's more common to
+-- use a representation like the following for records (or sums):
+--
+-- @
+-- data Bar = Bar 'Int' 'Bool'
+--   deriving ('G.Generic')
+-- @
+--
+-- The problem with that representation, however, is that it prevents us to
+-- operate on the individual fields as enabled by 'Flay'.
+--
+-- 'Pump' is a wrapper that converts types like 'Bar' into types like 'Foo'. In
+-- our concrete case, @'Pump' 'Bar' f@ is isomorphic to @'Foo' f@. But more
+-- importantly, @'Pump' 'Bar' f@ automatically gets a 'Flayable' instance of its
+-- own, allowing you to use 'flay' to operate on @'Pump' 'Bar' f@ as you would
+-- operate on @'Foo' f@.
+--
+-- To construct a 'Pump' you use 'pump', and to remove the 'Pump' wrapper you
+-- use 'dump', which satisfy the following identity law:
+--
+-- @
+-- 'dump' 'id' . 'pump' 'pure'  ==  'pure'
+-- @
+--
+-- 'Pump' relies on Haskell's 'G.Generic's, which is why we derived
+-- 'G.Generic' for our @Bar@ above. If @Bar@ didn't have a 'G.Generic' instance,
+-- then you wouldn't be able to use 'Pump' and would be better served by a
+-- manually written functions converting @Bar@ to @Foo@ and back.
+--
+-- Keep in mind that @'Pump' s f@ will only add @f@ wrappers to the immediate
+-- children fields of @s@ (which could itself be a sum type or a product type),
+-- but it won't recurse into the fields and add @f@ wrappers to them.
+--
+-- Very contrived and verbose example using all of 'pump', 'dump' and 'flay':
+--
+-- @
+-- -- | Replaces all of the fields of the given Bar with values 'Read' from
+-- -- 'System.IO.stdin', if possible.
+-- qux :: Bar -> 'IO' ('Either' 'String' 'Bar')
+-- qux bar0 = do
+--    let pbar0 :: 'Pump' Bar 'Identity'
+--        pbar0 = 'pump' 'Identity' bar0
+--    let h :: 'Dict' ('Read' a) -> 'Identity' a -> 'IO' ('Maybe' a)
+--        h 'Dict' ('Identity' _) = 'fmap' 'Text.Read.readMaybe' 'getLine'
+--    pbar1 :: 'Pump' Bar 'Maybe' <- 'flay' h pbar0
+--    -- We convert the 'Maybe's to 'Either' just for demonstration purposes.
+--    -- Using 'dump' 'id' would have been enough to make this function
+--    -- return a 'Maybe' Bar.
+--    let ebar1 :: 'Either' 'String' 'Bar'
+--        ebar1 = 'dump' ('maybe' ('Left' \"Bad") 'Right') pbar1
+--    pure ebar1
+-- @
+--
+-- Or, written in a less verbose manner:
+--
+-- @
+-- qux :: Bar -> 'IO' ('Either' 'String' 'Bar')
+-- qux bar = 'fmap' ('dump' ('maybe' ('Left' \"Bad") 'Right'))
+--                ('flay' \@'Read'
+--                      (\('Dict' ('Identity' _) -> 'fmap' 'Text.readMaybe' 'getLine')
+--                      ('pump' 'Identity' bar)
+-- @
+--
+-- We can use @qux@ in GHCi as follows:
+--
+-- @
+-- > qux (Bar 0 False)
+-- /not a number/
+-- /not a bool/
+-- __Left \"Bad"__
+--
+-- > qux (Bar 0 False)
+-- /1/
+-- /True/
+-- __Right (Bar 1 True)__
+-- @
+data Pump s f = forall p. Pump !(GPumped (G.Rep s) f p)
+
+instance
+  (GFlay' c (GPumped (G.Rep s) f) (GPumped (G.Rep s) g) f g)
+  => Flayable c (Pump s f) (Pump s g) f g where
+  flay h (Pump rep) = Pump <$> gflay' h rep
+  {-# INLINE flay #-}
+
+-- Giving a Flayable1 instance to Pump is a bit more tricky, so we are not
+-- doing it for the time being.
+
+-- | Wrap @s@ in 'Pump' so that it can be 'flay'ed.
+--
+-- See the documentation for 'Pump' for more details.
+pump
+  :: GPump s f
+  => (forall x. x -> f x)
+  -- ^ How to wrap in @f@ each individual child field of @s@.
+  -> s
+  -> Pump s f  -- ^
+pump f = \s -> Pump (gpump f (G.from s))
+{-# INLINE pump #-}
+
+-- | Remove the 'Pump' wraper around @s@.
+--
+-- See the documentation for 'Pump' for more details.
+dump
+  :: (GPump s f, Applicative m)
+  => (forall a. f a -> m a)
+  -- ^ How to remove the @f@ wrapper from every child field of @'Pump' s f@.
+  -> Pump s f
+  -> m s  -- ^
+dump f = \(Pump rep) -> G.to <$> gdump f rep
+{-# INLINE dump #-}
+
+-- | Convenient 'Constraint' for satisfying the requirements of 'pump' and
+-- 'dump'.
+type GPump s f = (G.Generic s, GPump' (G.Rep s) f)
+
+class GPump' (s :: k -> *) (f :: * -> *) where
+  type GPumped s f :: k -> *
+  gpump :: (forall a. a -> f a) -> s p -> GPumped s f p
+  gdump :: Applicative m => (forall a. f a -> m a) -> GPumped s f p -> m (s p)
+
+instance GPump' G.V1 f where
+  type GPumped G.V1 f = G.V1
+  gpump _ _ = undefined -- unreachable
+  gdump _ _ = undefined -- unreachable
+
+instance GPump' G.U1 f where
+  type GPumped G.U1 f = G.U1
+  gpump _ G.U1 = G.U1
+  {-# INLINE gpump #-}
+  gdump _ G.U1 = pure G.U1
+  {-# INLINE gdump #-}
+
+instance GPump' (G.K1 i c) f where
+  type GPumped (G.K1 i c) f = G.K1 i (f c)
+  gpump f (G.K1 c) = G.K1 (f c)
+  {-# INLINE gpump #-}
+  gdump f (G.K1 c) = G.K1 <$> f c
+  {-# INLINE gdump #-}
+
+instance GPump' s f => GPump' (G.M1 i j s) f where
+  type GPumped (G.M1 i j s) f = G.M1 i j (GPumped s f)
+  gpump f (G.M1 sp) = G.M1 (gpump f sp)
+  {-# INLINE gpump #-}
+  gdump f (G.M1 sp) = G.M1 <$> gdump f sp
+  {-# INLINE gdump #-}
+
+instance (GPump' sl f, GPump' sr f) => GPump' (sl G.:*: sr) f where
+  type GPumped (sl G.:*: sr) f = GPumped sl f G.:*: GPumped sr f
+  gpump f (slp G.:*: srp) = gpump f slp G.:*: gpump f srp
+  {-# INLINE gpump #-}
+  gdump f (slp G.:*: srp) = (G.:*:) <$> gdump f slp <*> gdump f srp
+  {-# INLINE gdump #-}
+
+instance (GPump' sl f, GPump' sr f) => GPump' (sl G.:+: sr) f where
+  type GPumped (sl G.:+: sr) f = GPumped sl f G.:+: GPumped sr f
+  gpump f (G.L1 slp) = G.L1 (gpump f slp)
+  gpump f (G.R1 srp) = G.R1 (gpump f srp)
+  {-# INLINE gpump #-}
+  gdump f (G.L1 slp) = G.L1 <$> gdump f slp
+  gdump f (G.R1 srp) = G.R1 <$> gdump f srp
+  {-# INLINE gdump #-}
+
+--------------------------------------------------------------------------------
+
 -- | Ensure that @x@ satisfies all of the constraints listed in @cs@.
+type family All (cs :: [k -> Constraint]) (x :: k) :: Constraint where
+  All (c ': cs) x = (c x, All cs x)
+  All '[] _ = ()
 
--- Implementation notice. @All@ and @All'@ have the same semantics, the only
--- difference is that @All@ can be partially applied, whereas @All'@ can't.
--- Thus, we only export @All@
-class All' cs x => All (cs :: [k -> Constraint]) (x :: k)
-instance All' cs x => All cs x
-type family All' (cs :: [k -> Constraint]) (x :: k) :: Constraint where
-  All' (c ': cs) x = (c x, All' cs x)
-  All' '[] _ = ()
+-- | Ensure that all of the immeditate children fields of @s@ satisfy @c@.
+--
+-- For example, in a datatype like the following:
+--
+-- @
+-- data Bar = Bar 'Int' 'Bool'
+-- @
+--
+-- The 'Fields' constraint behaves like this:
+--
+-- @
+-- 'Fields' c Bar  ==  (c 'Int', c 'Bool')
+-- @
+--
+-- 'Fields' can be used to remove boilerplate from contexts, since @c@
+-- will need to be mentioned just once, rather than once per type of field. This
+-- is particularly useful in the case of datatypes as 'Foo' below, intended to
+-- be used with 'Flay':
+--
+-- @
+-- data Foo f = Foo (f 'Int') (f 'Bool')
+-- @
+--
+-- The problem with types shaped like 'Foo' is that deriving some useful
+-- instances for them, like 'Show', involves a lot of boilerplate.
+-- For one, the usual @deriving ('Show')@ statement doesn't work, and you
+-- need to rely on the @StandaloneDeriving@ GHC extension. But even that's not
+-- enough, since you need to ensure that 'Show' constrains the individual field
+-- types as well. That is:
+--
+-- @
+-- deriving instance ('Show' (f 'Int'), 'Show' (f 'Bool')) => 'Show' (Foo f)
+-- @
+--
+-- This works, but hopefully you can see how this can become very verbose when
+-- you have more than a two or three datatypes in your fields. Instead, provided
+-- we derive 'G.Generic' for 'Foo', we can use 'Fields' to remove that
+-- boilerplate. That is:
+--
+-- @
+-- data Foo f = Foo (f 'Int') (f 'Bool')
+--   deriving ('G.Generic')
+--
+-- deriving instance 'Fields' 'Show' (Foo f) => 'Show' (Foo f)
+-- @
+type Fields c s = GFields c (G.Rep s)
+
+-- | Like 'Fields', but @s@ is expected to be a 'G.Rep'.
+--
+-- This 'Constraint' ensures that @c@ is satsfieds by all of the 'G.K1' types
+-- appearing in @s@, which is expected to be one of the various 'G.Generic'
+-- representation types.
+type family GFields (c :: kc -> Constraint) (s :: ks -> *) :: Constraint where
+  GFields _ G.V1 = ()
+  GFields _ G.U1 = ()
+  GFields c (G.K1 _ a) = (c a)
+  GFields c (G.M1 _ _ s) = GFields c s
+  GFields c (sl G.:*: sr) = (GFields c sl, GFields c sr)
+  GFields c (sl G.:+: sr) = (GFields c sl, GFields c sr)
+
+--------------------------------------------------------------------------------
+
+-- | This is like 'Fields', but it targets only field types that are wrapped by
+-- some type-constructor @f@.
+--
+-- That is, for all @a@ in @s f@ such that @f a@ is an immediate children of @s
+-- f@, then @c a@ must be satisfied.
+--
+-- 'FieldsF' can be used to remove boilerplate from contexts, since @c@
+-- will need to be mentioned just once, rather than once per type of field. This
+-- is particularly useful in the case of datatypes as 'Foo' below, intended to
+-- be used with 'Flay':
+--
+-- @
+-- data Foo f = Foo (f 'Int') (f 'Bool')
+-- @
+--
+-- If, for example, you intend to implement a @'Flayable' c (Foo f) (Foo g) f g@
+-- instance, then constraints @c 'Int'@ and @c 'Bool'@ will propagate. However,
+-- instead of writing @(c 'Int', c 'Bool')@, you can write @'FieldsF' c 'Foo'@
+-- and achieve the same, which will reduce boilerplate significantly in cases
+-- where the number of types contained in @f@ is larger. That is:
+--
+-- @
+-- forall (c :: * -> 'Constraint').
+--    'FieldsF' c 'Foo'  ==  (c 'Int', c 'Bool')
+-- @
+--
+-- Notice that 'FieldsF' only works with types of kind @(k -> *) -> *@ such as
+-- 'Foo'. That is, types that are parametrized by a type constructor.
+
+-- This type-family vs. class dance is so that 'F' doesn't show up in the public
+-- API (that is, in 'FieldsF').
+type family FieldsF (c :: k -> Constraint) (r :: (k -> *) -> *) :: Constraint where
+  FieldsF c r = FieldsF_ c r
+class GFieldsF c (G.Rep (r F)) F => FieldsF_ c r
+instance GFieldsF c (G.Rep (r F)) F => FieldsF_ c r
+
+-- | Like 'FieldsF', but @s@ is expected to be a 'G.Rep', and the type-constructor
+-- @f@ expected to wrap all of the field targets we want to constraint with @c@
+-- should be given explicitly.
+--
+-- This 'Constraint' ensures that @c@ is satsfieds by all of the 'G.K1' types
+-- appearing in @s@ that are wrapped by @f@.
+type family GFieldsF (c :: k -> Constraint) (s :: ks -> *) (f :: k -> *) :: Constraint where
+  GFieldsF _ G.V1 _ = ()
+  GFieldsF _ G.U1 _ = ()
+  GFieldsF c (G.K1 _ (f a)) f = (c a)
+  GFieldsF c (G.K1 _ _) f = ()
+  GFieldsF c (G.M1 _ _ s) f = GFieldsF c s f
+  GFieldsF c (sl G.:*: sr) f = (GFieldsF c sl f, GFieldsF c sr f)
+  GFieldsF c (sl G.:+: sr) f = (GFieldsF c sl f, GFieldsF c sr f)
+
+-- | INTERNAL. DO NOT EXPORT. Used as a placeholder of kind @forall k. k -> *@.
+data F (a :: k)
+
+-- | INTERNAL. DO NOT EXPORT. Used as a placeholder of kind @forall k. k -> *@.
+data G (a :: k)
 
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -1,16 +1,19 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Main where
 
 import Control.Monad (join)
+import Control.Monad.Trans.State.Strict (State, state, evalState)
 import Data.Functor.Const (Const(Const))
 import Data.Functor.Identity (Identity(Identity), runIdentity)
 import GHC.Exts (Constraint)
@@ -20,22 +23,41 @@
 import qualified Test.Tasty.Runners as Tasty
 import Test.Tasty.QuickCheck ((===))
 import qualified Test.Tasty.QuickCheck as QC
+import qualified Text.Read
 
 import Flay
 
 --------------------------------------------------------------------------------
 
+-- | Just making sure TypeApplications works as expected.
+_test_flay_TypeApplications
+  :: Flayable Trivial s t f g
+  => Flay Trivial s t (f :: k -> *) (g :: k -> *)
+_test_flay_TypeApplications = flay @Trivial
+
+-- | Just making sure TypeApplications works as expected.
+--
+-- Note: This triggers a warning about '-Wsimplifiable-class-constraints'.
+-- I'm not sure how to prevent it.
+_test_flay1_TypeApplications
+  :: Flayable1 Trivial r
+  => Flay Trivial (r f) (r g) (f :: k -> *) (g :: k -> *)
+_test_flay1_TypeApplications = flay1 @Trivial
+
+--------------------------------------------------------------------------------
+
 data Foo f = Foo (f Int) (f Bool)
   deriving (Generic)
 
 flayFoo :: (c Int, c Bool) => Flay c (Foo f) (Foo g) f g
 flayFoo h (Foo a b) = Foo <$> h Dict a <*> h Dict b
 
-instance (c Int, c Bool) => Flayable c (Foo f) (Foo g) f g where flay = gflay
-instance (c Int, c Bool) => Flayable1 c Foo
+-- This one is actually free:
+--   instance FieldsF c Foo => Flayable c (Foo f) (Foo g) f g
 
 deriving instance (Eq (f Int), Eq (f Bool)) => Eq (Foo f)
-deriving instance (Show (f Int), Show (f Bool)) => Show (Foo f)
+-- Testing 'Fields' here as well.
+deriving instance Fields Show (Foo f) => Show (Foo f)
 
 instance (QC.Arbitrary (f Int), QC.Arbitrary (f Bool)) => QC.Arbitrary (Foo f) where
   arbitrary = Foo <$> QC.arbitrary <*> QC.arbitrary
@@ -55,8 +77,8 @@
 flayBar :: c Int => Flay c (Bar f) (Bar g) f g
 flayBar h (Bar a b) = Bar <$> h Dict a <*> pure b
 
-instance (c Int) => Flayable c (Bar f) (Bar g) f g where flay = flay1
-instance (c Int) => Flayable1 c Bar where flay1 = flayBar
+-- | Checking 'FieldsF' here as well.
+instance FieldsF c Bar => Flayable c (Bar f) (Bar g) f g where flay = flayBar
 
 deriving instance Eq (f Int) => Eq (Bar f)
 deriving instance Show (f Int) => Show (Bar f)
@@ -92,6 +114,19 @@
 
 --------------------------------------------------------------------------------
 
+data Zoo
+  = Zoo0
+  | Zoo1 Int
+  | Zoo2 Int Int
+  deriving (Generic, Eq, Show)
+
+instance QC.Arbitrary Zoo where
+  arbitrary = QC.oneof [ pure Zoo0
+                       , pure Zoo1 <*> QC.arbitrary
+                       , pure Zoo2 <*> QC.arbitrary <*> QC.arbitrary ]
+
+--------------------------------------------------------------------------------
+
 main :: IO ()
 main = Tasty.defaultMainWithIngredients
   [ Tasty.consoleTestReporter
@@ -100,15 +135,15 @@
 
 tt :: Tasty.TestTree
 tt = Tasty.testGroup "main"
-  [ QC.testProperty "Flayable: Foo: inner identity law" $
+  [ QC.testProperty "Flayable: Foo: identity law" $
       QC.forAll QC.arbitrary $ \(foo :: Foo Maybe) ->
-         foo === inner flay foo
-  , QC.testProperty "Flayable: Bar: inner identity law" $
+         Identity foo === flay @Trivial (const pure) foo
+  , QC.testProperty "Flayable: Bar: identity law" $
       QC.forAll QC.arbitrary $ \(bar :: Bar Maybe) ->
-         bar === inner flay bar
-  , QC.testProperty "Flayable: Qux: inner identity law" $
+         Identity bar === flay @Trivial (const pure) bar
+  , QC.testProperty "Flayable: Qux: identity law" $
       QC.forAll QC.arbitrary $ \(qux :: Qux Maybe) ->
-         qux === inner flay qux
+         Identity qux === flay @Trivial (const pure) qux
   , QC.testProperty "collectShow: Foo: flayFoo" $
       QC.forAll QC.arbitrary $ \foo@(Foo (Identity a) (Identity b)) ->
          [show a, show b] === collectShow' flayFoo foo
@@ -126,7 +161,22 @@
          [show a] === collectShow' flay bar
   , QC.testProperty "collectShow: Bar: flay1" $
       QC.forAll QC.arbitrary $ \bar@(Bar (Identity a) _) ->
-         [show a] === collectShow' flay bar
+         [show a] === collectShow' flay1 bar
+  , QC.testProperty "pump/flay/dump: Zoo" $
+      QC.forAll QC.arbitrary $ \(zoo0 :: Zoo, i0 :: Int) ->
+         let pzoo0 :: Pump Zoo Identity
+             pzoo0 = pump Identity zoo0
+             h :: Dict (Read a) -> Identity a -> State Int (Maybe a)
+             h Dict _ = state (\i -> (Text.Read.readMaybe (show i), i+1))
+             spzoo1 :: State Int (Pump Zoo Maybe)
+             spzoo1 = flay1 h pzoo0
+             pzoo1 :: Pump Zoo Maybe
+             pzoo1 = evalState spzoo1 i0
+             yzoo1 :: Maybe Zoo
+             yzoo1 = dump id pzoo1
+         in yzoo1 === Just (case zoo0 of Zoo0 -> Zoo0
+                                         Zoo1{} -> Zoo1 i0
+                                         Zoo2{} -> Zoo2 i0 (i0+1))
   ]