diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,20 @@
+# Version 0.2
+
+* BREAKING CHANGE: The `m` parameter in in `Flay` and `Flayable` has been
+  existentialized, to be chosen by the caller.
+
+* BREAKING CHANGE: We don't use `DefaultSignatures` for `flay = gflay` anymore.
+  This is very sad, but unfortunately type inferrence for the `c` type variable
+  in new `Flayable` instances doesn't work.
+
+* Added `Flayable1`, `trivial1`, `collect1`, `Terminal`, `GTerminal`, `zip1`,
+  `zip`, `Record`, `GRecord`.
+
+* Removed `outer`.
+
+* Made compatible with GHC 8.2.2.
+
+
 # Version 0.1
 
 * Initial version.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,12 +1,10 @@
 # flay
 
-[![Build Status](https://travis-ci.org/k0001/flay.svg?branch=master)](https://travis-ci.org/k0001/flay)
-
 See the [BSD3 LICENSE](https://github.com/k0001/flay/blob/master/flay/LICENSE.txt)
 file to learn about the legal terms and conditions for this library.
 
 Find documentation for this library in the
-[`Flay`](https://github.com/k0001/flay/blob/master/flay/src/Flay.hs) module.
+[`Flay`](https://github.com/k0001/flay/blob/master/src/Flay.hs) module.
 
 You can build this library with [Nix](https://nixos.org/nix) by running
 `nix-build` on the top level of this module. `nix-shell` works as well.
diff --git a/default.nix b/default.nix
--- a/default.nix
+++ b/default.nix
@@ -1,1 +1,2 @@
-(import ./release.nix {}).flay
+{ compiler ? "ghc822" }:
+(import ./release.nix {}).${compiler}.flay
diff --git a/flay.cabal b/flay.cabal
--- a/flay.cabal
+++ b/flay.cabal
@@ -1,17 +1,17 @@
 name: flay
-version: 0.1
+version: 0.2
 author: Renzo Carbonara
 maintainer: renλren!zone
 copyright: Renzo Carbonara 2017
 license: BSD3
 license-file: LICENSE.txt
 extra-source-files: README.md CHANGELOG.md pkg.nix shell.nix default.nix release.nix
-category: Data
+category: Data, Generics
 build-type: Simple
 cabal-version: >=1.18
-synopsis: Work on your datatype without knowing its shape nor its contents.
+synopsis: Work generically on your datatype without knowing its shape nor its contents.
 description:
-  Work on your datatype without knowing its shape nor its contents using
+  Work generically on your datatype without knowing its shape nor its contents using
   a principlied approach.
 homepage: https://github.com/k0001/flay
 bug-reports: https://github.com/k0001/flay/issues
@@ -27,7 +27,8 @@
   exposed-modules: Flay
   build-depends:
     base >=4.9 && <5.0,
-    constraints
+    constraints,
+    ghc-prim
 
 test-suite tests
   default-language: Haskell2010
diff --git a/pkg.nix b/pkg.nix
--- a/pkg.nix
+++ b/pkg.nix
@@ -1,12 +1,12 @@
-{ mkDerivation, base, constraints, stdenv, tasty, tasty-quickcheck
+{ mkDerivation, base, constraints, ghc-prim, stdenv, tasty, tasty-quickcheck
 }:
 mkDerivation {
   pname = "flay";
-  version = "0.1";
+  version = "0.2";
   src = ./.;
-  libraryHaskellDepends = [ base constraints ];
+  libraryHaskellDepends = [ base constraints ghc-prim ];
   testHaskellDepends = [ base tasty tasty-quickcheck ];
   homepage = "https://github.com/k0001/flay";
-  description = "Work on your datatype without knowing much about it";
+  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
--- a/release.nix
+++ b/release.nix
@@ -1,21 +1,30 @@
 { nixpkgsBootstrap ? <nixpkgs>
 , nixpkgs ? (import nixpkgsBootstrap {}).fetchFromGitHub {
     owner = "NixOS";
-    repo = "nixpkgs";
-    rev = "100919ab5b69cbbb26886421aacc692467c7fec4"; # release-17.03
-    sha256 = "1nqiphqvxzszi0r4qq8w39x0g08wc7vaa9mfl7gi4a28bkv99781"; }
+    repo = "nixpkgs-channels";
+    rev = "3eccd0b11d176489d69c778f2fcb544438f3ab56"; # unstable, dec 4 2017
+    sha256 = "1i3p5m0pnn86lzni5y1win0sacckw3wlg9kqaw15nszhykgz22zq"; }
 }:
 
 let
-
 pkgs = import nixpkgs {};
 
 hsPackageSetConfig = self: super: {
   flay = self.callPackage (import ./pkg.nix) {};
 };
 
-ghc802 = pkgs.haskell.packages.ghc802.override {
-  packageSetConfig = hsPackageSetConfig;
+x = {
+  ghc802 = pkgs.haskell.packages.ghc802.override { packageSetConfig = hsPackageSetConfig; };
+  ghc822 = pkgs.haskell.packages.ghc822.override { packageSetConfig = hsPackageSetConfig; };
 };
 
-in { inherit (ghc802) flay; }
+in rec {
+  ghc802 = { inherit (x.ghc802) flay; };
+  ghc822 = { inherit (x.ghc822) flay; };
+
+  everything = pkgs.releaseTools.aggregate {
+    name = "everything";
+    meta.description = "Every job in release.nix";
+    constituents = [ ghc802.flay ghc822.flay ];
+  };
+}
diff --git a/shell.nix b/shell.nix
--- a/shell.nix
+++ b/shell.nix
@@ -1,1 +1,2 @@
-(import ./default.nix).env
+{ compiler ? "ghc822" }:
+(import ./release.nix {}).${compiler}.flay.env
diff --git a/src/Flay.hs b/src/Flay.hs
--- a/src/Flay.hs
+++ b/src/Flay.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -12,14 +14,11 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 
--- {-# LANGUAGE LambdaCase #-}
--- {-# LANGUAGE StandaloneDeriving #-}
-
 -- | The most commonly used names in this module are intended to be imported
 -- unqualified:
 --
 -- @
--- import Flay (Flay, Flayable(flay), Dict(Dict))
+-- import Flay (Flay, Flayable(flay), gflay, Dict(Dict))
 -- @
 --
 -- The rest of the names, qualified:
@@ -30,9 +29,9 @@
 module Flay
  ( Flay
  , inner
- , outer
  -- * Flayable
  , Flayable(flay)
+ , Flayable1(flay1)
  -- ** Generics
  , gflay
  , GFlay
@@ -41,38 +40,53 @@
  , All
  , Trivial
  , trivial
+ , trivial1
  , trivial'
  , collect
+ , collect1
  , collect'
+ , zip
+ , zip1
+ , unsafeZip
+ , Record
+ , GRecord
+ , terminal
+ , Terminal
+ , GTerminal(gterminal)
  -- ** Re-exports
  , Dict(Dict)
  ) where
 
-import Control.Monad (join)
-import Data.Functor.Identity (Identity, runIdentity)
+import Control.Monad.ST (ST, runST)
 import Data.Functor.Const (Const(Const, getConst))
+import Data.Functor.Identity (Identity(runIdentity))
 import Data.Constraint (Constraint, Dict(Dict))
+import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef)
 import qualified GHC.Generics as G
+import Prelude hiding (zip)
+import Unsafe.Coerce (unsafeCoerce)
 
+#if MIN_VERSION_ghc_prim(0,5,1)
+import GHC.Types (Any)
+#else
+import GHC.Prim (Any)
+#endif
+
+
 --------------------------------------------------------------------------------
 
--- | @'Flay' c m s t f g@ allows converting @s@ to @t@ by replacing
+-- | @'Flay' c s t f g@ allows converting @s@ to @t@ by replacing
 -- ocurrences of @f@ with @g@ by applicatively applying a function
 -- @(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 (and 'outer' identity law as
--- well, if the 'Flay' fits the type expected by 'outer').
---
--- When defining 'Flay' values, you should leave @c@, @m@, @f@, and @g@ fully
--- polymomrphic, as these are the most useful types of 'Flay's.
+-- A 'Flay' must obey the 'inner' identity law.
 --
--- When using a 'Flay', @m@ will be required to be a 'Functor' in case the 'Flay'
--- targets one element, or an 'Applicative' if it targets more than one. There
--- will be no constraints on the rest of the arguments to 'Flay'.
+-- When defining 'Flay' values, you should leave @c@, @f@, and @g@ fully
+-- polymorphic, as these are the most useful types of 'Flay's.
 --
 -- We use @'Dict' (c a) ->@ instead of @c a =>@ because the latter is often not
--- enough to satisfy the type checker. With this approach, one must explicitely
+-- enough to satisfy the type checker. With this approach, one must explicitly
 -- pattern match on the @'Dict' (c a)@ constructor in order to bring the @c a@
 -- instance to scope.  Also, it's necessary that @c@ is explicitly given a type
 -- at the 'Flay''s call site, as otherwise the type checker won't be able to
@@ -80,9 +94,9 @@
 --
 -- /to flay: tr. v., to strip off the skin or surface of./
 --
--- /Mnemonic for @c m s t f g@: CoMmon STandard FoG./
+-- /Mnemonic for @c s t f g@: Common STandard FoG./
 --
--- ==== Example 1: Removing uncertaininy
+-- ==== Example 1: Removing uncertainty
 --
 -- Consider the following types and values:
 --
@@ -93,7 +107,7 @@
 -- @
 --
 -- @
--- flayFoo :: ('Applicative' m, c 'Int', c 'Bool') => 'Flay' c m (Foo f) (Foo g) f g
+-- flayFoo :: ('Applicative' m, c 'Int', c 'Bool') => 'Flay' c (Foo f) (Foo g) f g
 -- flayFoo h (Foo a b) = Foo \<$> h 'Dict' a \<*> h 'Dict' b
 -- @
 --
@@ -155,10 +169,10 @@
 -- 'Just' (Foo ('Right' 2) ('Right' 'True'))
 -- @
 --
--- 'Flay', among other things, is intended to generalize this pattern so that
+-- 'Flay', among other things, is intended to generalize this pattern, so that
 -- whatever choice of 'Foo', 'Maybe' or 'Identity' you make, you can use
 -- 'Applicative' this way. The easiest way to use 'Flay' is through 'trivial'',
--- which is sufficient unless we need to enforce some constrain in the target
+-- which is sufficient unless we need to enforce some constraint in the target
 -- elements wrapped in @m@ inside foo (we don't need this now). With 'trivial'',
 -- we could have defined @fooMToG@ this way:
 --
@@ -182,7 +196,7 @@
 -- flayMToG fl = 'trivial'' fl ('fmap' 'pure')
 -- @
 --
--- This is the escence of 'Flay': We can work operate on the contents of a
+-- This is the esscence of 'Flay': We can work operating on the contents of a
 -- datatype @s@ targeted by a given 'Flay' /without/ knowing anything about @s@,
 -- nor about the @forall x. f x@ targets of the 'Flay'. And we do this using an
 -- principled approach relying on 'Applicative' and 'Functor'.
@@ -201,7 +215,7 @@
 --
 -- ==== Example 2: Standalone @m@
 --
--- In the previous example, @flayFoo@ took the type @Flay 'Trivial' m (Foo m) (Foo
+-- In the previous example, @flayFoo@ took the type @Flay 'Trivial' (Foo m) (Foo
 -- g) m g@ when it was used in @flayMToG@. That is, @m@ and @f@ were unified by
 -- our use of 'fmap'. However, keeping these different opens interesting
 -- possibilities. For example, let's try and convert a @Foo 'Maybe'@ to a @Foo
@@ -269,7 +283,7 @@
 -- Notice how we had to give an explicit type to our function @h@: This is
 -- because can't infer our @'Read' a@ constraint. You will always need to
 -- explicitly type the received @'Dict'@ unless the @c@ argument to 'Flay' has
--- been explicitely by other means (like in the definition of 'trivial'', where
+-- 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'').
 --
@@ -314,57 +328,69 @@
 -- about the targets themselves beyond the fact that they satisfy a particular
 -- constraint.
 --
-type Flay (c :: k -> Constraint) (m :: * -> *) s t (f :: k -> *) (g :: k -> *)
-  = (forall (a :: k). Dict (c a) -> f a -> m (g a)) -> s -> m t
+type Flay (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *)
+  = 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 Identity s s f f -> s -> s
+inner :: Flay Trivial s s f f -> s -> s
 inner fl = runIdentity . trivial' fl pure
 
--- | Outer identity law:
---
--- @
--- (\\fl -> 'join' . 'trivial'' fl 'pure') = 'id'
--- @
-outer :: Monad m => Flay Trivial m (m x) (m x) m m -> m x -> m x
-outer fl = join . trivial' fl pure
-
-
 --------------------------------------------------------------------------------
 
 -- | Default 'Flay' implementation for @s@ and @t@.
 --
--- When defining 'Flayable' instances, you should leave @c@, @m@, @f@, and @g@
+-- When defining 'Flayable' instances, you should leave @c@, @f@, and @g@
 -- fully polymomrphic, as these are the most useful types of 'Flayables's.
-
--- TODO: See if `c` can be made of kind `k -> Constraint`, probably in GHC 8.2.
-class Flayable (c :: * -> Constraint) m s t f g | s -> f, t -> g, s g -> t, t f -> s where
-  flay :: Flay c m s t f g
-  -- | If @s@ and @g@ are instances of 'G.Generic', then 'flay' 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 'flay':
+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 ('Applicative' m, c 'Int', c 'Bool') => 'Flayable' c m (Foo f) (Foo g) f g
+  -- instance (c 'Int', c 'Bool') => 'Flayable' c (Foo f) (Foo g) f g where
+  --   'flay' = 'gflay'
   -- @
   --
-  -- Notice that while this default definition works for an @s@ having "nested
-  -- 'Flayables'", GHC will prompt you for some additional constraints related
-  -- to 'GFlay'' in order for it to compile.
-  default flay :: (Functor m, GFlay c m s t f g) => Flay c m s t f g
-  flay = gflay
-  {-# INLINE flay #-}
+  -- 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.
+  flay :: Flay c s t f g
 
--- | Isomorphic to @c a => f a -> m (g a)@.
-instance {-# OVERLAPPABLE #-} c a => Flayable c m (f a) (g a) f g where
-  flay = \h fa -> h Dict fa
-  {-# 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'.
+--
+-- 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 #-}
+
 --------------------------------------------------------------------------------
 
 -- | 'Constraint' trivially satisfied by every type.
@@ -384,11 +410,12 @@
 -- @
 trivial'
   :: forall m s t f g
-  .  Flay Trivial m s t f g
+  .  Applicative m
+  => Flay Trivial s t f g
   -> (forall a. Trivial a => f a -> m (g a))
   -> s
   -> m t  -- ^
-trivial' fl = \h s -> fl (\Dict fa -> h fa) s
+trivial' fl = \h -> \s -> fl (\Dict fa -> h fa) s
 {-# INLINE trivial' #-}
 
 -- | Like 'trivial'', but works on a 'Flayable' instead of taking an explicit
@@ -398,58 +425,63 @@
 -- 'trivial' = 'trivial'' 'flay'
 -- @
 trivial
-  :: Flayable Trivial m s t f g
+  :: (Applicative m, Flayable Trivial s t f g)
   => (forall a. Trivial a => f a -> m (g a))
   -> s
   -> m t  -- ^
 trivial = trivial' flay
 {-# INLINE trivial #-}
 
+-- | Like 'trivial'', but works on a 'Flayable1' instead of taking an explicit
+-- 'Flay'.
+--
+-- @
+-- 'trivial' = 'trivial'' 'flay1'
+-- @
+trivial1
+  :: (Applicative m, Flayable1 Trivial r)
+  => (forall a. Trivial a => f a -> m (g a))
+  -> (r f)
+  -> m (r g)  -- ^
+trivial1 = trivial' flay1
+{-# INLINE trivial1 #-}
+
 --------------------------------------------------------------------------------
 
 -- | Convenience 'Constraint' for satisfying basic 'GFlay'' needs for @s@ and @t@.
-class (G.Generic s, G.Generic t, GFlay' c m (G.Rep s) (G.Rep t) f g)
-  => GFlay (c :: k -> Constraint) m s t f g
-instance (G.Generic s, G.Generic t, GFlay' c m (G.Rep s) (G.Rep t) f g)
-  => GFlay (c :: k -> Constraint) m s t f g
+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 -> *)
 
-gflay :: (Functor m, GFlay c m s t f g) => Flay c m s t f g
+
+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)
 {-# INLINE gflay #-}
 
-class GFlay' (c :: k -> Constraint) m s t f g where
-  gflay' :: Flay c m (s p) (t p) f g
+class GFlay' (c :: k -> Constraint) s t (f :: k -> *) (g :: k -> *) where
+  gflay' :: Flay c (s p) (t p) f g
 
-instance GFlay' c m G.V1 G.V1 f g where
+instance GFlay' c G.V1 G.V1 f g where
   gflay' _ _ = undefined -- unreachable
   {-# INLINE gflay' #-}
 
--- Is this necessary?
-instance (Functor m, GFlay' c m s t f g)
-  => GFlay' c m (G.Rec1 s) (G.Rec1 t) f g where
-  gflay' h (G.Rec1 sp) = G.Rec1 <$> gflay' h sp
-  {-# INLINE gflay' #-}
-
-instance (Functor m, Flayable c m (f a) (g a) f g) => GFlay' c m (G.K1 r (f a)) (G.K1 r (g a)) f g where
-  gflay' h (G.K1 fa) = G.K1 <$> flay h fa
-  {-# INLINE gflay' #-}
-
-instance Applicative m => GFlay' c m (G.K1 r x) (G.K1 r x) f g where
-  gflay' _ x = pure x
+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' #-}
 
-instance (Functor m, GFlay' c m s t f g)
-  => GFlay' c m (G.M1 i j s) (G.M1 i j t) f g where
+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
   {-# INLINE gflay' #-}
 
-instance (Applicative m, GFlay' c m sl tl f g, GFlay' c m sr tr f g)
-  => GFlay' c m (sl G.:*: sr) (tl G.:*: tr) f g where
+instance (GFlay' c sl tl f g, GFlay' c sr tr f g)
+  => GFlay' c (sl G.:*: sr) (tl G.:*: tr) f g where
   gflay' h (slp G.:*: srp) = (G.:*:) <$> gflay' h slp <*> gflay' h srp
   {-# INLINE gflay' #-}
 
-instance (Functor m, GFlay' c m sl tl f g, GFlay' c m sr tr f g)
-  => GFlay' c m (sl G.:+: sr) (tl G.:+: tr) f g where
+instance (GFlay' c sl tl f g, GFlay' c sr tr f g)
+  => GFlay' c (sl G.:+: sr) (tl G.:+: tr) f g where
   gflay' h x = case x of
     G.L1 slp -> G.L1 <$> gflay' h slp
     G.R1 srp -> G.R1 <$> gflay' h srp
@@ -470,21 +502,148 @@
 -- @
 collect'
   :: Monoid b
-  => Flay c (Const b) s t f (Const ())
+  => Flay c s t f (Const ())
   -> (forall a. Dict (c a) -> f a -> b)
   -> s
   -> b    -- ^
-collect' fl k = \s -> getConst (fl (\d fa -> Const (k d fa)) s)
+collect' fl = \k -> \s -> getConst (fl (\d fa -> Const (k d fa)) s)
 {-# INLINE collect' #-}
 
 -- | Like 'collect'', but works on a 'Flayable' instead of an explicit 'Flay'.
 collect
-  :: (Monoid b, Flayable c (Const b) s t f (Const ()))
+  :: (Monoid b, Flayable c s t f (Const ()))
   => (forall a. Dict (c a) -> f a -> b)
   -> s
   -> b    -- ^
-collect k = collect' flay k
+collect = collect' flay
 {-# INLINE collect #-}
+
+-- | Like 'collect'', but works on a 'Flayable1' instead of an explicit 'Flay'.
+collect1
+  :: (Monoid b, Flayable1 c r)
+  => (forall a. Dict (c a) -> f a -> b)
+  -> r f
+  -> b    -- ^
+collect1 = collect' flay1
+{-# INLINE collect1 #-}
+
+--------------------------------------------------------------------------------
+
+-- | Handwavy class of which only product or record types are supposed to be
+-- instances.
+class Record a
+instance {-# OVERLAPPABLE #-} (G.Generic a, GRecord (G.Rep a)) => Record a
+
+class GRecord (a :: * -> *) where
+instance GRecord G.U1
+instance GRecord (G.K1 r x)
+instance GRecord x => GRecord (G.M1 i j x)
+instance (GRecord l, GRecord r) => GRecord (l G.:*: r)
+
+--------------------------------------------------------------------------------
+
+
+-- | Witness that @a@ is a terminal object. That is, that @a@ can always be
+-- 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 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 #-}
+
+--------------------------------------------------------------------------------
+
+-- | Zip two 'Flayable1's together.
+--
+-- Example pairing two of the 'Foo' values seen elsewhere in this file.
+--
+-- @
+-- > let foo1 = 'Foo' ('Data.Functor.Identity.Identity' 0) ('Data.Functor.Identity.Identity' 'False')
+-- >   :: 'Foo' 'Data.Functor.Identity.Identity'
+--
+-- > let foo2 = 'Foo' ('Just' 1) 'Nothing'
+-- >   :: 'Foo' 'Maybe'
+--
+-- > 'zip1' (\('Dict' :: 'Dict' ('Trivial' x)) a b -> 'Data.Functor.Product.Pair' a b) foo1 foo2
+-- >   :: 'Foo' ('Data.Functor.Product.Product' 'Data.Functor.Identity.Identity' 'Maybe')
+-- 'Foo' ('Data.Functor.Product.Pair' ('Data.Functor.Identity.Identity' 0) ('Just' 1)) ('Data.Functor.Product.Pair' ('Data.Functor.Identity.Identity' 'False') 'Nothing')
+--
+-- > 'zip1' (\('Dict' :: 'Dict' ('Show' x)) ('Data.Functor.Identity.Identity' a) yb -> case yb of
+-- >           'Nothing' -> 'Const' ('show' a)
+-- >           'Just' b  -> 'Const' ('show' (a, b)) )
+-- >      foo1 foo2
+-- >   :: Foo ('Const' 'String')
+-- Foo ('Const' \"(0,1)\") ('Const' \"False\")
+-- @
+--
+-- Note: 'zip1' is safer but less general than 'unsafeZip'.
+zip1
+  :: (Record (s f), Flayable1 c s)
+  => (forall x. Dict (c x) -> f x -> g x -> h x)
+  -> s f
+  -> s g
+  -> s h  -- ^
+zip1 h = unsafeZip flay1 flay1 h
+{-# INLINABLE zip1 #-}
+
+-- | Zip two 'Flayable's together.
+--
+-- 'zip' is like 'zip1', but for 'Flayable's.
+--
+-- Note: 'zip' is safer but less general than 'unsafeZip'.
+zip
+  :: ( Record s0
+     , Flayable c s0 t0 f (Const ())
+     , Flayable c s1 t1 g h )
+  => (forall x. Dict (c x) -> f x -> g x -> h x)
+  -> s0
+  -> s1
+  -> t1   -- ^
+zip h = unsafeZip flay flay h
+{-# INLINABLE zip #-}
+
+-- | Unsafe version of 'zip' that doesn't guarantee that the given 'Flay's
+-- target the same values. 'zip' makes this function safe by simply using
+-- 'flay' twice.
+unsafeZip
+  :: forall c s0 s1 t0 t1 f g h
+  .  Record s0
+  => (Flay c s0 t0 f (Const ()))
+  -> (Flay c s1 t1 g h)
+  -> (forall x. Dict (c x) -> f x -> g x -> h x)
+  -> s0
+  -> s1
+  -> t1  -- ^
+unsafeZip fl0 fl1 pair = \s0 s1 -> runST $ do
+    r <- newSTRef (collect' fl0 f1 s0)
+    fl1 (f2 r) s1
+  where
+    f1 :: Dict (c a) -> f a -> [Any]
+    f1 = \Dict fa -> [unsafeCoerce fa :: Any]
+    f2 :: STRef z [Any] -> Dict (c a) -> g a -> ST z (h a)
+    f2 r = \Dict !ga -> do
+       (x:xs) <- readSTRef r
+       writeSTRef r xs
+       let !fa = unsafeCoerce (x :: Any) :: f a
+       pure $! pair Dict fa ga
 
 --------------------------------------------------------------------------------
 
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -12,6 +13,7 @@
 import Control.Monad (join)
 import Data.Functor.Const (Const(Const))
 import Data.Functor.Identity (Identity(Identity), runIdentity)
+import GHC.Exts (Constraint)
 import GHC.Generics (Generic)
 import qualified GHC.Generics as G
 import qualified Test.Tasty as Tasty
@@ -26,10 +28,11 @@
 data Foo f = Foo (f Int) (f Bool)
   deriving (Generic)
 
-flayFoo :: (Applicative m, c Int, c Bool) => Flay c m (Foo f) (Foo g) f g
+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 (Applicative m, c Int, c Bool) => Flayable c m (Foo f) (Foo g) f g
+instance (c Int, c Bool) => Flayable c (Foo f) (Foo g) f g where flay = gflay
+instance (c Int, c Bool) => Flayable1 c Foo
 
 deriving instance (Eq (f Int), Eq (f Bool)) => Eq (Foo f)
 deriving instance (Show (f Int), Show (f Bool)) => Show (Foo f)
@@ -37,15 +40,23 @@
 instance (QC.Arbitrary (f Int), QC.Arbitrary (f Bool)) => QC.Arbitrary (Foo f) where
   arbitrary = Foo <$> QC.arbitrary <*> QC.arbitrary
 
+-- example values
+foo1 :: Applicative m => Foo m
+foo1 = Foo (pure 0) (pure False)
+
+foo2 :: Applicative m => Foo m
+foo2 = Foo (pure 1) (pure True)
+
 --------------------------------------------------------------------------------
 
 data Bar f = Bar (f Int) Int
   deriving (Generic)
 
-flayBar :: (Applicative m, c Int) => Flay c m (Bar f) (Bar g) f g
+flayBar :: c Int => Flay c (Bar f) (Bar g) f g
 flayBar h (Bar a b) = Bar <$> h Dict a <*> pure b
 
-instance (Applicative m, c Int, c Bool) => Flayable c m (Bar f) (Bar g) f g
+instance (c Int) => Flayable c (Bar f) (Bar g) f g where flay = flay1
+instance (c Int) => Flayable1 c Bar where flay1 = flayBar
 
 deriving instance Eq (f Int) => Eq (Bar f)
 deriving instance Show (f Int) => Show (Bar f)
@@ -61,23 +72,20 @@
   | Qux3 (Foo f)
   deriving (Generic)
 
-flayQux :: (Applicative m, c Int, c Bool) => Flay c m (Qux f) (Qux g) f g
+flayQux :: (c Int, c Bool) => Flay c (Qux f) (Qux g) f g
 flayQux h (Qux1 a b) = Qux1 <$> h Dict a <*> pure b
 flayQux h (Qux2 a b) = Qux2 <$> h Dict a <*> h Dict b
 flayQux h (Qux3 a) = Qux3 <$> flayFoo h a
 
--- TODO: See if there is a way of removing all these constraints.
-instance
-  ( GFlay' c m (G.K1 G.R (Foo f)) (G.K1 G.R (Foo g)) f g
-  , Applicative m
-  , c Int
-  , c Bool
-  ) => Flayable c m (Qux f) (Qux g) f g
+instance (c Int , c Bool) => Flayable c (Qux f) (Qux g) f g where
+  flay h (Qux1 fa b) = Qux1 <$> h Dict fa <*> pure b
+  flay h (Qux2 fa fb) = Qux2 <$> h Dict fa <*> h Dict fb
+  flay h (Qux3 foo) = Qux3 <$> flay h foo
 
 deriving instance (Eq (f Int), Eq (Foo f)) => Eq (Qux f)
 deriving instance (Show (f Int), Show (Foo f)) => Show (Qux f)
 
-instance (QC.Arbitrary (f Int), QC.Arbitrary (Foo f)) => QC.Arbitrary (Qux f) where
+instance (QC.Arbitrary (f Int), QC.Arbitrary (f Bool)) => QC.Arbitrary (Qux f) where
   arbitrary = QC.oneof [ Qux1 <$> QC.arbitrary <*> QC.arbitrary
                        , Qux2 <$> QC.arbitrary <*> QC.arbitrary
                        , Qux3 <$> QC.arbitrary ]
@@ -101,24 +109,27 @@
   , QC.testProperty "Flayable: Qux: inner identity law" $
       QC.forAll QC.arbitrary $ \(qux :: Qux Maybe) ->
          qux === inner flay qux
-  , QC.testProperty "Flayable: outer identity law" $
-      QC.forAll QC.arbitrary $ \(ia :: Identity Int) ->
-         ia === outer flay ia
   , QC.testProperty "collectShow: Foo: flayFoo" $
       QC.forAll QC.arbitrary $ \foo@(Foo (Identity a) (Identity b)) ->
          [show a, show b] === collectShow' flayFoo foo
   , QC.testProperty "collectShow: Foo: flay" $
       QC.forAll QC.arbitrary $ \foo@(Foo (Identity a) (Identity b)) ->
          [show a, show b] === collectShow' flay foo
+  , QC.testProperty "collectShow: Foo: flay1" $
+      QC.forAll QC.arbitrary $ \foo@(Foo (Identity a) (Identity b)) ->
+         [show a, show b] === collectShow' flay1 foo
   , QC.testProperty "collectShow: Bar: flayBar" $
       QC.forAll QC.arbitrary $ \bar@(Bar (Identity a) _) ->
          [show a] === collectShow' flayBar bar
   , QC.testProperty "collectShow: Bar: flay" $
       QC.forAll QC.arbitrary $ \bar@(Bar (Identity a) _) ->
          [show a] === collectShow' flay bar
+  , QC.testProperty "collectShow: Bar: flay1" $
+      QC.forAll QC.arbitrary $ \bar@(Bar (Identity a) _) ->
+         [show a] === collectShow' flay bar
   ]
 
 
 collectShow'
-  :: Flay Show (Const [String]) s t Identity (Const ()) -> s -> [String]
+  :: Flay Show s t Identity (Const ()) -> s -> [String]
 collectShow' fl = collect' fl (\Dict (Identity a) -> [show a])