diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,22 @@
+# 0.9.0.0
+
+- Improved definition of `gfoldMap`, `gtraverse`, and `sequenceA`.
+  The optimized Core of `Traversable` instances eliminates all `GHC.Generic` instance
+  boilerplate. In many cases, it is identical to the result of GHC's `DeriveFoldable`
+  and `DeriveTraversable` extensions (note: this was already not a problem for
+  `gfmap`).
+
+  It's worth noting that there are currently issues with inlining which prevent
+  optimizations that *generic-data* would ideally rely on.
+
+    + The biggest issue is that GHC will not even inline the `to` and `from`
+      methods of the `Generic` instance it derives for large types (this shows
+      up at around 5 constructors and 10 fields, which is indeed not really
+      big). This will be fixed by a patch for GHC (WIP):
+      https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2965
+
+    + There appear to be some more inlining issues beyond that (issue #40).
+
 # 0.8.3.0
 
 - Add generic `Read`. Thanks to RyanGlScott.
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,2 @@
-import Distribution.Simple
-main = defaultMain
+import Distribution.Extra.Doctest (defaultMainWithDoctests)
+main = defaultMainWithDoctests "generic-data-doctest"
diff --git a/generic-data.cabal b/generic-data.cabal
--- a/generic-data.cabal
+++ b/generic-data.cabal
@@ -1,5 +1,5 @@
 name:                generic-data
-version:             0.8.3.0
+version:             0.9.0.0
 synopsis:            Deriving instances with GHC.Generics and related utilities
 description:
   Generic implementations of standard type classes.
@@ -12,12 +12,16 @@
 maintainer:          lysxia@gmail.com
 copyright:           2018-2020 Li-yao Xia
 category:            Generics
-build-type:          Simple
+build-type:          Custom
 extra-source-files:  README.md, CHANGELOG.md
 cabal-version:       >=1.10
 tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.1,
                      GHC == 8.6.3, GHC == 8.6.5, GHC == 8.8.2
 
+custom-setup
+  setup-depends:
+    base, Cabal, cabal-doctest >= 1.0.6 && < 1.1
+
 library
   hs-source-dirs:      src
   exposed-modules:
@@ -37,8 +41,10 @@
     Generic.Data.Internal.Read
     Generic.Data.Internal.Resolvers
     Generic.Data.Internal.Show
+    Generic.Data.Internal.Traversable
     Generic.Data.Internal.Utils
   build-depends:
+    ap-normalize >= 0.1 && < 0.2,
     base-orphans >= 0.8,
     contravariant,
     ghc-boot-th,
@@ -122,12 +128,28 @@
   default-language: Haskell2010
   type: exitcode-stdio-1.0
 
+test-suite generic-data-inspection-test
+  hs-source-dirs: test
+  main-is: inspection.hs
+  other-modules:
+    Inspection.Boilerplate
+  build-depends:
+    generic-data,
+    inspection-testing,
+    template-haskell,
+    unordered-containers,
+    base
+  ghc-options: -Wall -threaded
+  default-language: Haskell2010
+  type: exitcode-stdio-1.0
+  if impl(ghc < 8.2) || os(windows)
+    buildable: False
+
 test-suite generic-data-doctest
   hs-source-dirs: test
   main-is: doctest.hs
   build-depends:
     doctest,
-    Glob,
     QuickCheck,
     generic-data,
     base
diff --git a/src/Generic/Data.hs b/src/Generic/Data.hs
--- a/src/Generic/Data.hs
+++ b/src/Generic/Data.hs
@@ -1,5 +1,7 @@
 -- | Generic combinators to derive type class instances.
 --
+-- = Overview
+--
 -- /base/ classes that GHC can not derive instances for, as of version 8.2:
 --
 -- - 'Data.Semigroup.Semigroup', 'Monoid', 'Applicative',
@@ -11,6 +13,58 @@
 --
 -- GHC can derive instances for other classes here, although there may be
 -- types supported by one method but not the other or vice versa.
+--
+-- == __Minor discrepancies__
+--
+-- Here are documented some corner cases of deriving, both by GHC and
+-- generic-data. They are all minor and unlikely to cause problems in
+-- practice.
+--
+-- === Empty types
+--
+-- - Some of the derived methods are lazy, which might result in errors
+--   being silenced, though unlikely.
+-- - The only generic-data implementation which differs from GHC stock
+--   instances is 'gfoldMap'.
+--
+-- +------------------+-----------+--------------+-----------------------+
+-- | Class method     | GHC stock | generic-data | Comment               |
+-- +------------------+-----------+--------------+-----------------------+
+-- | @('==')@         | lazy      | lazy         | 'True'                |
+-- +------------------+-----------+--------------+-----------------------+
+-- | 'compare'        | lazy      | lazy         | 'EQ'                  |
+-- +------------------+-----------+--------------+-----------------------+
+-- | 'fmap'           | strict    | strict       | must be bottom anyway |
+-- +------------------+-----------+--------------+-----------------------+
+-- | 'foldMap'        | lazy      | strict       | 'mempty' if lazy      |
+-- +------------------+-----------+--------------+-----------------------+
+-- | 'foldr'          | lazy      | lazy         | returns accumulator   |
+-- +------------------+-----------+--------------+-----------------------+
+-- | 'traverse'       | strict    | strict       |                       |
+-- +------------------+-----------+--------------+-----------------------+
+-- | 'sequenceA'      | strict    | strict       |                       |
+-- +------------------+-----------+--------------+-----------------------+
+--
+-- === Single-constructor single-field types
+--
+-- @data@ types with one constructor and one field are extremely rare.
+-- @newtype@ is almost always more appropriate (for which there is no issue).
+--
+-- That said, for @data@ types both strict and lazy, all generic-data
+-- implementations are lazy (they don't even force the constructor),
+-- whereas GHC stock implementations, when they exist, are strict.
+--
+-- === Functor composition
+--
+-- Fields of functors involving the composition of two or more
+-- functors @f (g (h a))@ cannot be handled nicely using @GHC.Generics@.
+-- Some overhead cannot be safely avoided.
+--
+-- This is due to a particular encoding choice of @GHC.Generics@, where
+-- composition are nested to the right instead of to the left. @f (g (h _))@ is
+-- represented by the functor @f ':.:' (g ':.:' 'Rec1' h)@. A better choice is to
+-- encode it as @('Rec1' f ':.:' g) ':.:' h@, because that is coercible back to
+-- @f (g (h _))@.
 
 module Generic.Data
   ( -- * Regular classes
@@ -85,11 +139,13 @@
     -- | Can also be derived by GHC (@DeriveFoldable@ extension).
   , gfoldMap
   , gfoldr
+  , GFoldable
 
     -- ** 'Traversable'
     -- | Can also be derived by GHC (@DeriveTraversable@ extension).
   , gtraverse
   , gsequenceA
+  , GTraversable
 
     -- ** 'Applicative'
   , gpure
@@ -181,12 +237,13 @@
   , MetaSelStrictness
   ) where
 
-import Generic.Data.Internal.Prelude
+import Generic.Data.Internal.Prelude hiding (gfoldMap, gtraverse, gsequenceA)
 import Generic.Data.Internal.Enum
 import Generic.Data.Internal.Generically
 import Generic.Data.Internal.Meta
 import Generic.Data.Internal.Read
 import Generic.Data.Internal.Show
+import Generic.Data.Internal.Traversable
 import Generic.Data.Internal.Newtype
 import Generic.Data.Internal.Resolvers
 import Generic.Data.Internal.Utils
diff --git a/src/Generic/Data/Internal/Generically.hs b/src/Generic/Data/Internal/Generically.hs
--- a/src/Generic/Data/Internal/Generically.hs
+++ b/src/Generic/Data/Internal/Generically.hs
@@ -1,7 +1,9 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE
+  CPP,
+  FlexibleContexts,
+  TypeFamilies,
+  UndecidableInstances,
+  UndecidableSuperClasses #-}
 
 -- | Newtypes with instances implemented using generic combinators.
 --
@@ -22,11 +24,12 @@
 import GHC.Generics
 import Text.Read
 
-import Generic.Data.Internal.Prelude
+import Generic.Data.Internal.Prelude hiding (gfoldMap, gtraverse, gsequenceA)
 import Generic.Data.Internal.Enum
 import Generic.Data.Internal.Error
 import Generic.Data.Internal.Read
 import Generic.Data.Internal.Show
+import Generic.Data.Internal.Traversable (GFoldable, GTraversable, gfoldMap, gtraverse, gsequenceA)
 
 -- | Type with instances derived via 'Generic'.
 newtype Generically a = Generically { unGenerically :: a }
@@ -155,13 +158,15 @@
   empty = gempty
   (<|>) = galt
 
-instance (Generic1 f, Foldable (Rep1 f)) => Foldable (Generically1 f) where
+instance (Generic1 f, GFoldable (Rep1 f)) => Foldable (Generically1 f) where
   foldMap = gfoldMap
   foldr = gfoldr
 
-instance (Generic1 f, Traversable (Rep1 f)) => Traversable (Generically1 f) where
+instance (Generic1 f, Functor (Rep1 f), GFoldable (Rep1 f), GTraversable (Rep1 f))
+  => Traversable (Generically1 f) where
   traverse = gtraverse
   sequenceA = gsequenceA
+
 
 -- | Product type with generic instances of 'Semigroup' and 'Monoid'.
 --
diff --git a/src/Generic/Data/Internal/Prelude.hs b/src/Generic/Data/Internal/Prelude.hs
--- a/src/Generic/Data/Internal/Prelude.hs
+++ b/src/Generic/Data/Internal/Prelude.hs
@@ -141,6 +141,9 @@
 -- instance 'Foldable' MyTypeF where
 --   'foldMap' = 'gfoldMap'
 -- @
+--
+-- This is deprecated but kept around just for reference.
+{-# DEPRECATED gfoldMap "This definition has been replaced with 'Generic.Data.Internal.gfoldMap'." #-}
 gfoldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m) => (a -> m) -> f a -> m
 gfoldMap = \f -> foldMap f . from1
 
@@ -154,6 +157,7 @@
 -- See also 'gfoldMap'.
 gfoldr :: (Generic1 f, Foldable (Rep1 f)) => (a -> b -> b) -> b -> f a -> b
 gfoldr = \f b -> foldr f b . from1
+-- Note: this one is not deprecated because inlining Just Works.
 
 -- * 'Traversable'
 
@@ -163,6 +167,9 @@
 -- instance 'Traversable' MyTypeF where
 --   'traverse' = 'gtraverse'
 -- @
+--
+-- This is deprecated but kept around just for reference.
+{-# DEPRECATED gtraverse "This definition has been replaced with 'Generic.Data.Internal.gtraverse'." #-}
 gtraverse
   :: (Generic1 f, Traversable (Rep1 f), Applicative m)
   => (a -> m b) -> f a -> m (f b)
@@ -176,6 +183,9 @@
 -- @
 --
 -- See also 'gtraverse'.
+--
+-- This is deprecated but kept around just for reference.
+{-# DEPRECATED gsequenceA "This definition has been replaced with 'Generic.Data.Internal.gsequenceA'." #-}
 gsequenceA
   :: (Generic1 f, Traversable (Rep1 f), Applicative m)
   => f (m a) -> m (f a)
diff --git a/src/Generic/Data/Internal/Traversable.hs b/src/Generic/Data/Internal/Traversable.hs
new file mode 100644
--- /dev/null
+++ b/src/Generic/Data/Internal/Traversable.hs
@@ -0,0 +1,230 @@
+-- | Generic implementation of 'Foldable' and 'Traversable'.
+--
+-- There is already a naive implementation using the generic @'Rep'@'s
+-- own instances of 'Foldable' and 'Traversable'. However, deriving then
+-- generates a lot of code that may not be simplified away by GHC,
+-- that results in unnecessary run-time overhead.
+--
+-- In contrast, this implementation guarantees that the generated code is
+-- identical to stock-derived instances of 'Foldable' and 'Traversable',
+-- which have the following syntactic properties:
+--
+-- - constructors with zero fields use 'pure' once;
+-- - constructors with one field use 'fmap' once;
+-- - constructors with n >= 2 fields use 'liftA2' once and @('<*>')@ n-2 times.
+--
+-- The heavy lifting is actually done by the ap-normalize library.
+
+{-# LANGUAGE
+  DataKinds,
+  EmptyCase,
+  FlexibleContexts,
+  FlexibleInstances,
+  GADTs,
+  KindSignatures,
+  MultiParamTypeClasses,
+  ScopedTypeVariables,
+  TypeApplications,
+  TypeOperators,
+  UndecidableInstances,
+  UndecidableSuperClasses #-}
+
+module Generic.Data.Internal.Traversable where
+
+import Control.Applicative (liftA2)
+import Data.Kind (Type)
+import Data.Monoid
+import GHC.Generics
+
+import ApNormalize
+
+-- * Library
+
+-- | Generic 'foldMap'.
+--
+-- @
+-- instance 'Foldable' MyTypeF where
+--   'foldMap' = 'gfoldMap'
+-- @
+gfoldMap :: (Generic1 f, GFoldable (Rep1 f), Monoid m) => (a -> m) -> f a -> m
+gfoldMap = \f -> lowerEndoM . gfoldMap_ f . from1
+{-# INLINE gfoldMap #-}
+
+-- | Generic 'traverse'.
+--
+-- @
+-- instance 'Traversable' MyTypeF where
+--   'traverse' = 'gtraverse'
+-- @
+gtraverse
+  :: (Generic1 f, GTraversable (Rep1 f), Applicative m)
+  => (a -> m b) -> f a -> m (f b)
+gtraverse = \f -> lowerAps . fmap to1 . gtraverse_ (Kleisli f) . from1
+{-# INLINE gtraverse #-}
+
+-- | Generic 'sequenceA'.
+--
+-- @
+-- instance 'Traversable' MyTypeF where
+--   'sequenceA' = 'gsequenceA'
+-- @
+--
+-- See also 'gtraverse'.
+--
+gsequenceA
+  :: (Generic1 f, GTraversable (Rep1 f), Applicative m)
+  => f (m a) -> m (f a)
+gsequenceA = lowerAps . fmap to1 . gtraverse_ Refl . from1
+{-# INLINE gsequenceA #-}
+
+-- | Class of generic representations for which 'Foldable' can be derived.
+class    GFoldable_ t => GFoldable t
+instance GFoldable_ t => GFoldable t
+
+-- | Class of generic representations for which 'Traversable' can be derived.
+class    GTraversable_ t => GTraversable t
+instance GTraversable_ t => GTraversable t
+
+-- | Internal definition of 'GFoldable'.
+class    (GFoldMap t, Foldable t) => GFoldable_ t
+instance (GFoldMap t, Foldable t) => GFoldable_ t
+
+-- | Internal definition of 'GTraversable'.
+class    (GTraverse Kleisli t, GTraverse Equal t) => GTraversable_ t
+instance (GTraverse Kleisli t, GTraverse Equal t) => GTraversable_ t
+
+-- Implementation
+
+-- ** Foldable
+
+-- | Isomorphic to @Maybe m@, but we need to micromanage the
+-- use of Monoid vs Semigroup to match exactly the output
+-- of stock deriving, for inspection testing.
+data Maybe' m = Nothing' | Just' m
+
+type EndoM m = Endo (Maybe' m)
+
+liftEndoM :: Monoid m => m -> EndoM m
+liftEndoM x = Endo app where
+  app Nothing' = Just' x
+  app (Just' y) = Just' (x `mappend` y)
+{-# INLINE liftEndoM #-}
+
+lowerEndoM :: Monoid m => EndoM m -> m
+lowerEndoM (Endo app) = lowerMaybe (app Nothing')
+{-# INLINE lowerEndoM #-}
+
+lowerMaybe :: Monoid m => Maybe' m -> m
+lowerMaybe Nothing' = mempty
+lowerMaybe (Just' x) = x
+{-# INLINE lowerMaybe #-}
+
+class GFoldMap t where
+  gfoldMap_ :: Monoid m => (a -> m) -> t a -> EndoM m
+
+instance GFoldMap f => GFoldMap (M1 i c f) where
+  gfoldMap_ f (M1 x) = gfoldMap_ f x
+  {-# INLINE gfoldMap_ #-}
+
+instance (GFoldMap f, GFoldMap g) => GFoldMap (f :+: g) where
+  gfoldMap_ f (L1 x) = gfoldMap_ f x
+  gfoldMap_ f (R1 y) = gfoldMap_ f y
+  {-# INLINE gfoldMap_ #-}
+
+instance (GFoldMap f, GFoldMap g) => GFoldMap (f :*: g) where
+  gfoldMap_ f (x :*: y) = gfoldMap_ f x `mappend` gfoldMap_ f y
+  {-# INLINE gfoldMap_ #-}
+
+instance GFoldMap U1 where
+  gfoldMap_ _ _ = mempty
+  {-# INLINE gfoldMap_ #-}
+
+instance GFoldMap V1 where
+  gfoldMap_ _ v = case v of {}
+  {-# INLINE gfoldMap_ #-}
+
+instance GFoldMap (K1 i a) where
+  gfoldMap_ _ (K1 _) = mempty
+  {-# INLINE gfoldMap_ #-}
+
+instance GFoldMap Par1 where
+  gfoldMap_ f (Par1 x) = liftEndoM (f x)
+  {-# INLINE gfoldMap_ #-}
+
+instance Foldable t => GFoldMap (Rec1 t) where
+  gfoldMap_ f (Rec1 x) = liftEndoM (foldMap f x)
+  {-# INLINE gfoldMap_ #-}
+
+instance (Foldable t, Foldable f) => GFoldMap (t :.: f) where
+  gfoldMap_ f (Comp1 x) = liftEndoM (foldMap (foldMap f) x)
+  {-# INLINE gfoldMap_ #-}
+
+
+-- ** Traversable
+
+data Equal (f :: Type -> Type) a b where
+  Refl :: Equal f (f b) b
+
+newtype Kleisli f a b = Kleisli (a -> f b)
+
+class GTraverse arr t where
+  gtraverse_ :: Applicative f => arr f a b -> t a -> Aps f (t b)
+
+instance GTraverse arr f => GTraverse arr (M1 i c f) where
+  gtraverse_ f (M1 x) = M1 <$> gtraverse_ f x
+  {-# INLINE gtraverse_ #-}
+
+instance (GTraverse arr f, GTraverse arr g) => GTraverse arr (f :+: g) where
+  gtraverse_ f (L1 x) = L1 <$> gtraverse_ f x
+  gtraverse_ f (R1 y) = R1 <$> gtraverse_ f y
+  {-# INLINE gtraverse_ #-}
+
+instance (GTraverse arr f, GTraverse arr g) => GTraverse arr (f :*: g) where
+  gtraverse_ f (x :*: y) = liftA2 (:*:) (gtraverse_ f x) (gtraverse_ f y)
+  {-# INLINE gtraverse_ #-}
+
+instance GTraverse arr U1 where
+  gtraverse_ _ _ = pure U1
+  {-# INLINE gtraverse_ #-}
+
+instance GTraverse arr V1 where
+  gtraverse_ _ v = case v of {}
+  {-# INLINE gtraverse_ #-}
+
+instance GTraverse arr (K1 i a) where
+  gtraverse_ _ (K1 x) = pure (K1 x)
+  {-# INLINE gtraverse_ #-}
+
+-- traverse
+
+instance GTraverse Kleisli Par1 where
+  gtraverse_ (Kleisli f) (Par1 x) = Par1 <$> liftAps (f x)
+  {-# INLINE gtraverse_ #-}
+
+instance Traversable t => GTraverse Kleisli (Rec1 t) where
+  gtraverse_ (Kleisli f) (Rec1 x) = Rec1 <$> liftAps (traverse f x)
+  {-# INLINE gtraverse_ #-}
+
+-- Oh no, the encoding with @(':.:')@ is quite broken.
+--
+-- @t1 (... (tn (t a)) ...)@ is represented as:
+-- @(t1 :.: (... :.: (tn :.: Rec1 t) ...)) a@
+-- but it would be more efficient to associate to the left:
+-- @(((... (Rec1 t1 :.: t2) :.: ...) :.: tn) :.: t) a
+instance (Traversable t, Traversable f) => GTraverse Kleisli (t :.: f) where
+  gtraverse_ (Kleisli f) (Comp1 x) = Comp1 <$> liftAps (traverse (traverse f) x)
+  {-# INLINE gtraverse_ #-}
+
+-- sequenceA
+
+instance GTraverse Equal Par1 where
+  gtraverse_ Refl (Par1 x) = Par1 <$> liftAps x
+  {-# INLINE gtraverse_ #-}
+
+instance Traversable t => GTraverse Equal (Rec1 t) where
+  gtraverse_ Refl (Rec1 x) = Rec1 <$> liftAps (sequenceA x)
+  {-# INLINE gtraverse_ #-}
+
+instance (Traversable t, Traversable f) => GTraverse Equal (t :.: f) where
+  gtraverse_ Refl (Comp1 x) = Comp1 <$> liftAps (traverse sequenceA x)
+  {-# INLINE gtraverse_ #-}
diff --git a/test/Inspection/Boilerplate.hs b/test/Inspection/Boilerplate.hs
new file mode 100644
--- /dev/null
+++ b/test/Inspection/Boilerplate.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE
+  FlexibleInstances,
+  TemplateHaskell #-}
+
+module Inspection.Boilerplate where
+
+import Control.Applicative (liftA2)
+import Language.Haskell.TH
+
+import Generic.Data
+
+{- Example output this generates (modulo reordering):
+eqEmptyR, eqEmptyS, eqEmptyG :: Empty a -> Empty a -> Bool
+eqEmptyR = \_ _ -> True
+eqEmptyS = (==)
+eqEmptyG = geq
+-}
+
+class AppendQ q where
+  ($++) :: q -> DecsQ -> DecsQ
+
+  infixr 2 $++
+
+instance AppendQ (Q Dec) where
+  ($++) = liftA2 (:)
+
+instance AppendQ (Q [Dec]) where
+  ($++) = liftA2 (++)
+
+instance AppendQ q => AppendQ [q] where
+  ps $++ qs = foldr ($++) qs ps
+
+type Top = Name -> ExpQ -> DecsQ
+
+mk_ :: String -> Maybe Name -> Name -> (TypeQ -> TypeQ) -> Top
+mk_ bname fname_ gname ty_ tname ref = do
+  nameR <- newName (bname ++ nameBase tname ++ "R")  -- Reference
+  nameS <- newName (bname ++ nameBase tname ++ "S")  -- Stock
+  nameG <- newName (bname ++ nameBase tname ++ "G")  -- Generic
+  let ty = ty_ (conT tname)
+      stock = case fname_ of
+        Nothing -> pure []
+        Just fname ->
+              sigD nameS ty
+          $++ funD' nameS (varE fname)
+          $++ pure []
+  (     sigD nameR ty
+    $++ sigD nameG ty
+    $++ funD' nameR ref
+    $++ funD' nameG (varE gname)
+    $++ stock
+    $++ pure [] )
+
+funD' :: Name -> ExpQ -> DecQ
+funD' name body = funD name [clause [] (normalB body) []]
+
+--
+
+newVar :: String -> Q TypeQ
+newVar x = varT <$> newName x
+
+-- Eq and Ord
+
+-- Sometimes there isn't an Eq constraint on the parameter.
+mk_eq_ :: (TypeQ -> TypeQ) -> Top
+mk_eq_ = mk_ "eq" (Just '(==)) 'geq
+
+mk_eq :: Top
+mk_eq = mk_eq_ ty where
+  ty f = do
+    a <- newVar "a"
+    [t| Eq $a => $f $a -> $f $a -> Bool |]
+
+mk_eq' :: Top
+mk_eq' = mk_eq_ ty where
+  ty f = do
+    a <- newVar "a"
+    [t| $f $a -> $f $a -> Bool |]
+
+-- Sometimes there isn't an Ord constraint on the parameter.
+mk_compare_ :: (TypeQ -> TypeQ) -> Top
+mk_compare_ = mk_ "compare" (Just 'compare) 'gcompare
+
+mk_compare :: Top
+mk_compare = mk_compare_ ty where
+  ty f = do
+    a <- newVar "a"
+    [t| Ord $a => $f $a -> $f $a -> Ordering |]
+
+mk_compare' :: Top
+mk_compare' = mk_compare_ ty where
+  ty f = do
+    a <- newVar "a"
+    [t| $f $a -> $f $a -> Ordering |]
+
+-- Functor, Foldable, Traversable
+
+mk_fmap :: Top
+mk_fmap = mk_ "fmap" (Just 'fmap) 'gfmap ty where
+  ty f = do
+    a <- newVar "a"
+    b <- newVar "b"
+    [t| ($a -> $b) -> $f $a -> $f $b |]
+
+mk_foldMap :: Top
+mk_foldMap = mk_ "foldMap" (Just 'foldMap) 'gfoldMap ty where
+  ty f = do
+    a <- newVar "a"
+    m <- newVar "m"
+    [t| Monoid $m => ($a -> $m) -> $f $a -> $m |]
+
+mk_foldr :: Top
+mk_foldr = mk_ "foldr" (Just 'foldr) 'gfoldr ty where
+  ty f = do
+    a <- newVar "a"
+    b <- newVar "b"
+    [t| ($a -> $b -> $b) -> $b -> $f $a -> $b |]
+
+mk_traverse :: Top
+mk_traverse = mk_ "traverse" (Just 'traverse) 'gtraverse ty where
+  ty f = do
+    a <- newVar "a"
+    b <- newVar "b"
+    g <- newVar "g"
+    [t| Applicative $g => ($a -> $g $b) -> $f $a -> $g ($f $b) |]
+
+mk_sequenceA :: Top
+mk_sequenceA = mk_ "sequenceA" (Just 'sequenceA) 'gsequenceA ty where
+  ty f = do
+    a <- newVar "a"
+    g <- newVar "g"
+    [t| Applicative $g => $f ($g $a) -> $g ($f $a) |]
+
+-- Applicative (no stock deriving)
+
+mk_ap :: Top
+mk_ap = mk_ "ap" Nothing 'gap ty where
+  ty f = do
+    a <- newVar "a"
+    b <- newVar "b"
+    [t| $f ($a -> $b) -> $f $a -> $f $b |]
+
+mk_liftA2 :: Top
+mk_liftA2 = mk_ "liftA2" Nothing 'gliftA2 ty where
+  ty f = do
+    a <- newVar "a"
+    b <- newVar "b"
+    c <- newVar "c"
+    [t| ($a -> $b -> $c) -> $f $a -> $f $b -> $f $c |]
+
diff --git a/test/doctest.hs b/test/doctest.hs
--- a/test/doctest.hs
+++ b/test/doctest.hs
@@ -1,7 +1,7 @@
 module Main (main) where
 
-import System.FilePath.Glob (glob)
 import Test.DocTest (doctest)
+import Build_doctests (flags, pkgs, module_sources)
 
 main :: IO ()
-main = glob "src/**/*.hs" >>= doctest
+main = doctest (flags ++ pkgs ++ module_sources)
diff --git a/test/inspection.hs b/test/inspection.hs
new file mode 100644
--- /dev/null
+++ b/test/inspection.hs
@@ -0,0 +1,513 @@
+{-# OPTIONS_GHC -dsuppress-all #-}
+{-# LANGUAGE
+    BangPatterns,
+    CPP,
+    DeriveFunctor,
+    DeriveFoldable,
+    DeriveTraversable,
+    DeriveGeneric,
+    DerivingVia,
+    EmptyCase,
+    EmptyDataDeriving,
+    TemplateHaskell
+    #-}
+
+{-# LANGUAGE TypeOperators, TypeFamilies #-}
+
+import Control.Applicative (liftA2)
+import Data.Coerce (coerce)
+import GHC.Generics
+import Data.Semigroup (Sum(..), All(..))
+
+import Test.Inspection
+
+import Generic.Data
+import Generic.Data.Microsurgery
+  ( ProductSurgery
+  , CopyRep
+  , Surgery'(..)
+  )
+
+import Inspection.Boilerplate
+
+-- Test cases
+
+data T = T Int Bool
+  deriving Generic
+  deriving (Semigroup, Monoid)
+    via ProductSurgery (CopyRep (Sum Int, All)) T
+  deriving (Eq, Ord)
+    via Generically T
+
+mappendT, mappendTG :: T -> T -> T
+mappendT (T a1 b1) (T a2 b2) = T (a1 + a2) (b1 && b2)
+mappendTG x y = x <> y
+
+memptyT, memptyTG :: T
+memptyT = T 0 True
+memptyTG = mempty
+
+eqT, eqTG :: T -> T -> Bool
+eqT (T a1 b1) (T a2 b2) = a1 == a2 && b1 == b2
+eqTG = (==)
+
+compareT, compareTG :: T -> T -> Ordering
+compareT (T a1 b1) (T a2 b2) = compare a1 a2 <> compare b1 b2
+compareTG = compare
+
+inspect $ 'mappendT ==- 'mappendTG
+inspect $ 'memptyT ==- 'memptyTG
+inspect $ 'eqT ==- 'eqTG
+inspect $ 'compareT ==- 'compareTG
+
+data Empty a
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+-- Arity 0 (nullary)
+data Ary0 a = Ary0
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+-- Arity 1 (unary) (Lazy, Strict, Newtype)
+data Ary1 a = Ary1 a
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+data Ary1' a = Ary1' !a
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+newtype Ary1NT a = Ary1NT a
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+-- Arity 2 (binary)
+data Ary2 a = Ary2 a a
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+-- Arity 4 (quaternary)
+data Ary4 a = Ary4 a a [Int] [a]
+  deriving (Generic, Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+-- A big sum of stuff
+data Big a
+  = Big0
+  | Big1 a
+  | Big2 a a
+  | Big4 a a a a
+  | Big8 Int a [a] [Int] [a] a a a
+  deriving (Generic1, Eq, Ord, Functor, Foldable, Traversable)
+
+-- Handwritten to add INLINE pragmas. TODO: get GHC to do this
+instance Generic (Big a) where
+  type Rep (Big a) =
+        U1
+    :+: K1 () a
+    :+: (K1 () a :*: K1 () a)
+    :+: (K1 () a :*: K1 () a :*: K1 () a :*: K1 () a)
+    :+: (   K1 () Int :*: K1 () a :*: K1 () [a] :*: K1 () [Int]
+        :*: K1 () ([a]) :*: K1 () a :*: K1 () a :*: K1 () a)
+  from Big0 = L1 U1
+  from (Big1 x) = R1 (L1 (K1 x))
+  from (Big2 x1 x2) = R1 (R1 (L1 (K1 x1 :*: K1 x2)))
+  from (Big4 x1 x2 x3 x4) = R1 (R1 (R1 (L1 (K1 x1 :*: K1 x2 :*: K1 x3 :*: K1 x4))))
+  from (Big8 x1 x2 x3 x4 x5 x6 x7 x8) = R1 (R1 (R1 (R1 (K1 x1 :*: K1 x2 :*: K1 x3 :*: K1 x4 :*: K1 x5 :*: K1 x6 :*: K1 x7 :*: K1 x8))))
+  {-# INLINE from #-}
+
+  to (L1 _) = Big0
+  to (R1 (L1 (K1 x))) = Big1 x
+  to (R1 (R1 (L1 (K1 x1 :*: K1 x2)))) = Big2 x1 x2
+  to (R1 (R1 (R1 (L1 (K1 x1 :*: K1 x2 :*: K1 x3 :*: K1 x4))))) = Big4 x1 x2 x3 x4
+  to (R1 (R1 (R1 (R1 (K1 x1 :*: K1 x2 :*: K1 x3 :*: K1 x4 :*: K1 x5 :*: K1 x6 :*: K1 x7 :*: K1 x8))))) = Big8 x1 x2 x3 x4 x5 x6 x7 x8
+  {-# INLINE to #-}
+
+-- Empty
+
+-- Stock deriving of fmap does not use an EmptyCase.
+fmapEmptyRS :: (a -> b) -> Empty a -> Empty b
+fmapEmptyRS _ = coerce
+
+foldMapEmptyRS :: Monoid m => (a -> m) -> Empty a -> m
+foldMapEmptyRS _ _ = mempty
+
+--
+
+mk_eq' ''Empty [| \ _ _ -> True |]
+inspect $ 'eqEmptyR ==- 'eqEmptyS
+inspect $ 'eqEmptyR ==- 'eqEmptyG
+
+mk_compare' ''Empty [| \ _ _ -> EQ |]
+inspect $ 'compareEmptyR ==- 'compareEmptyS
+inspect $ 'compareEmptyR ==- 'compareEmptyG
+
+mk_fmap ''Empty [| \ _ v -> case v of {} |]
+inspect $ 'fmapEmptyRS ==- 'fmapEmptyS
+inspect $ 'fmapEmptyR ==- 'fmapEmptyG
+
+mk_foldMap ''Empty [| \ _ v -> case v of {} |]
+inspect $ 'foldMapEmptyRS ==- 'foldMapEmptyS
+inspect $ 'foldMapEmptyR ==- 'foldMapEmptyG
+
+-- No EmptyCase!
+mk_foldr ''Empty [| \_ b _ -> b |]
+inspect $ 'foldrEmptyR ==- 'foldrEmptyS
+inspect $ 'foldrEmptyR ==- 'foldrEmptyG
+
+mk_traverse ''Empty [| \ _ v -> case v of {} |]
+inspect $ 'traverseEmptyS ==- 'traverseEmptyS
+inspect $ 'traverseEmptyR ==- 'traverseEmptyG
+
+mk_sequenceA ''Empty [| \ v -> case v of {} |]
+inspect $ 'sequenceAEmptyS ==- 'sequenceAEmptyS
+inspect $ 'sequenceAEmptyR ==- 'sequenceAEmptyG
+
+-- Ary0
+
+eqAry0RS :: Ary0 a -> Ary0 a -> Bool
+eqAry0RS Ary0 Ary0 = True
+
+compareAry0RS :: Ary0 a -> Ary0 a -> Ordering
+compareAry0RS Ary0 Ary0 = EQ
+
+fmapAry0RS :: (a -> b) -> Ary0 a -> Ary0 b
+fmapAry0RS _ = coerce
+
+mk_eq' ''Ary0 [| \ _ _ -> True |]
+inspect $ 'eqAry0RS ==- 'eqAry0S
+inspect $ 'eqAry0R ==- 'eqAry0G
+
+mk_compare' ''Ary0 [| \ _ _ -> EQ |]
+inspect $ 'compareAry0RS ==- 'compareAry0S
+inspect $ 'compareAry0R ==- 'compareAry0G
+
+mk_fmap ''Ary0 [| \ _ _ -> Ary0 |]
+inspect $ 'fmapAry0RS ==- 'fmapAry0S
+inspect $ 'fmapAry0R ==- 'fmapAry0G
+
+mk_foldMap ''Ary0 [| \ _ _ -> mempty |]
+inspect $ 'foldMapAry0R ==- 'foldMapAry0S
+inspect $ 'foldMapAry0R ==- 'foldMapAry0G
+
+mk_foldr ''Ary0 [| \_ b _ -> b |]
+inspect $ 'foldrAry0R ==- 'foldrAry0S
+inspect $ 'foldrAry0R ==- 'foldrAry0G
+
+mk_traverse ''Ary0 [| \ _ _ -> pure Ary0 |]
+inspect $ 'traverseAry0S ==- 'traverseAry0S
+inspect $ 'traverseAry0R ==- 'traverseAry0G
+
+mk_sequenceA ''Ary0 [| \ _ -> pure Ary0 |]
+inspect $ 'sequenceAAry0S ==- 'sequenceAAry0S
+inspect $ 'sequenceAAry0R ==- 'sequenceAAry0G
+
+-- Ary1
+
+eqAry1RS :: Eq a => Ary1 a -> Ary1 a -> Bool
+eqAry1RS (Ary1 x1) (Ary1 y1) = x1 == y1
+
+compareAry1RS :: Ord a => Ary1 a -> Ary1 a -> Ordering
+compareAry1RS (Ary1 x1) (Ary1 y1) = compare x1 y1
+
+fmapAry1RS :: (a -> b) -> Ary1 a -> Ary1 b
+fmapAry1RS f (Ary1 x) = Ary1 (f x)
+
+foldMapAry1RS :: Monoid m => (a -> m) -> Ary1 a -> m
+foldMapAry1RS f (Ary1 x) = f x
+
+foldrAry1RS :: (a -> b -> b) -> b -> Ary1 a -> b
+foldrAry1RS f b (Ary1 x) = f x b
+
+traverseAry1RS :: Applicative f => (a -> f b) -> Ary1 a -> f (Ary1 b)
+traverseAry1RS f (Ary1 x) = Ary1 <$> f x
+
+sequenceAAry1RS :: Applicative f => Ary1 (f a) -> f (Ary1 a)
+sequenceAAry1RS (Ary1 x) = Ary1 <$> x
+
+mk_eq ''Ary1 [| \ ~(Ary1 x1) ~(Ary1 y1) -> x1 == y1 |]
+inspect $ 'eqAry1RS ==- 'eqAry1S
+inspect $ 'eqAry1R ==- 'eqAry1G
+
+mk_compare ''Ary1 [| \ ~(Ary1 x1) ~(Ary1 y1) -> compare x1 y1 |]
+inspect $ 'compareAry1RS ==- 'compareAry1S
+inspect $ 'compareAry1R ==- 'compareAry1G
+
+mk_fmap ''Ary1 [| \ f ~(Ary1 x) -> Ary1 (f x) |]
+inspect $ 'fmapAry1RS ==- 'fmapAry1S
+inspect $ 'fmapAry1R ==- 'fmapAry1G
+
+mk_foldMap ''Ary1 [| \ f ~(Ary1 x) -> f x |]
+inspect $ 'foldMapAry1RS ==- 'foldMapAry1S
+inspect $ 'foldMapAry1R ==- 'foldMapAry1G
+
+mk_foldr ''Ary1 [| \ f r ~(Ary1 x) -> f x r |]
+inspect $ 'foldrAry1RS ==- 'foldrAry1S
+inspect $ 'foldrAry1R ==- 'foldrAry1G
+
+mk_traverse ''Ary1 [| \ f ~(Ary1 x) -> Ary1 <$> f x |]
+inspect $ 'traverseAry1RS ==- 'traverseAry1S
+inspect $ 'traverseAry1R ==- 'traverseAry1G
+
+mk_sequenceA ''Ary1 [| \ ~(Ary1 x) -> Ary1 <$> x |]
+inspect $ 'sequenceAAry1RS ==- 'sequenceAAry1S
+inspect $ 'sequenceAAry1R ==- 'sequenceAAry1G
+
+-- Generic @to@ seems to be lazy here
+mk_ap ''Ary1 [| \ ~(Ary1 f1) ~(Ary1 x1) -> Ary1 (f1 x1) |]
+inspect $ 'apAry1R ==- 'apAry1G
+
+mk_liftA2 ''Ary1 [| \ f ~(Ary1 x1) ~(Ary1 x2) -> Ary1 (f x1 x2) |]
+inspect $ 'liftA2Ary1R ==- 'liftA2Ary1G
+
+-- Ary1' (strict, this is entirely the same as Ary1)
+
+eqAry1'RS :: Eq a => Ary1' a -> Ary1' a -> Bool
+eqAry1'RS (Ary1' x1) (Ary1' y1) = x1 == y1
+
+compareAry1'RS :: Ord a => Ary1' a -> Ary1' a -> Ordering
+compareAry1'RS (Ary1' x1) (Ary1' y1) = compare x1 y1
+
+fmapAry1'RS :: (a -> b) -> Ary1' a -> Ary1' b
+fmapAry1'RS f (Ary1' x) = Ary1' (f x)
+
+foldMapAry1'RS :: Monoid m => (a -> m) -> Ary1' a -> m
+foldMapAry1'RS f (Ary1' x) = f x
+
+foldrAry1'RS :: (a -> b -> b) -> b -> Ary1' a -> b
+foldrAry1'RS f b (Ary1' x) = f x b
+
+traverseAry1'RS :: Applicative f => (a -> f b) -> Ary1' a -> f (Ary1' b)
+traverseAry1'RS f (Ary1' x) = Ary1' <$> f x
+
+sequenceAAry1'RS :: Applicative f => Ary1' (f a) -> f (Ary1' a)
+sequenceAAry1'RS (Ary1' x) = Ary1' <$> x
+
+mk_eq ''Ary1' [| \ ~(Ary1' x1) ~(Ary1' y1) -> x1 == y1 |]
+inspect $ 'eqAry1'RS ==- 'eqAry1'S
+inspect $ 'eqAry1'R ==- 'eqAry1'G
+
+mk_compare ''Ary1' [| \ ~(Ary1' x1) ~(Ary1' y1) -> compare x1 y1 |]
+inspect $ 'compareAry1'RS ==- 'compareAry1'S
+inspect $ 'compareAry1'R ==- 'compareAry1'G
+
+mk_fmap ''Ary1' [| \ f ~(Ary1' x) -> Ary1' (f x) |]
+inspect $ 'fmapAry1'RS ==- 'fmapAry1'S
+inspect $ 'fmapAry1'R ==- 'fmapAry1'G
+
+mk_foldMap ''Ary1' [| \ f ~(Ary1' x) -> f x |]
+inspect $ 'foldMapAry1'RS ==- 'foldMapAry1'S
+inspect $ 'foldMapAry1'R ==- 'foldMapAry1'G
+
+mk_foldr ''Ary1' [| \ f r ~(Ary1' x) -> f x r |]
+inspect $ 'foldrAry1'RS ==- 'foldrAry1'S
+inspect $ 'foldrAry1'R ==- 'foldrAry1'G
+
+-- TODO: These tests fail because of a difference in how the Functor
+-- dictionary is accessed via the Applicative dictionary.
+-- The rest looks alright.
+#if __GLASGOW_HASKELL__ >= 810
+mk_traverse ''Ary1' [| \ f ~(Ary1' x) -> Ary1' <$> f x |]
+inspect $ 'traverseAry1'RS ==- 'traverseAry1'S
+inspect $ 'traverseAry1'R ==- 'traverseAry1'G
+
+mk_sequenceA ''Ary1' [| \ ~(Ary1' x) -> Ary1' <$> x |]
+inspect $ 'sequenceAAry1'RS ==- 'sequenceAAry1'S
+inspect $ 'sequenceAAry1'R ==- 'sequenceAAry1'G
+#endif
+
+-- Generic @to@ seems to be lazy here
+mk_ap ''Ary1' [| \ ~(Ary1' f1) ~(Ary1' x1) -> Ary1' (f1 x1) |]
+inspect $ 'apAry1'R ==- 'apAry1'G
+
+mk_liftA2 ''Ary1' [| \ f ~(Ary1' x1) ~(Ary1' x2) -> Ary1' (f x1 x2) |]
+inspect $ 'liftA2Ary1'R ==- 'liftA2Ary1'G
+
+-- Ary1NT
+
+eqAry1NTRS :: Eq a => Ary1NT a -> Ary1NT a -> Bool
+eqAry1NTRS = (coerce :: (a -> a -> Bool) -> Ary1NT a -> Ary1NT a -> Bool) (==)
+
+compareAry1NTRS :: Ord a => Ary1NT a -> Ary1NT a -> Ordering
+compareAry1NTRS = (coerce :: (a -> a -> Ordering) -> Ary1NT a -> Ary1NT a -> Ordering) compare
+
+mk_eq ''Ary1NT [| \ (Ary1NT x1) (Ary1NT y1) -> x1 == y1 |]
+inspect $ 'eqAry1NTRS ==- 'eqAry1NTS
+inspect $ 'eqAry1NTR ==- 'eqAry1NTG
+
+mk_compare ''Ary1NT [| \ (Ary1NT x1) (Ary1NT y1) -> compare x1 y1 |]
+inspect $ 'compareAry1NTRS ==- 'compareAry1NTS
+inspect $ 'compareAry1NTR ==- 'compareAry1NTG
+
+mk_fmap ''Ary1NT [| \ f (Ary1NT x) -> Ary1NT (f x) |]
+inspect $ 'fmapAry1NTR ==- 'fmapAry1NTS
+inspect $ 'fmapAry1NTR ==- 'fmapAry1NTG
+
+mk_foldMap ''Ary1NT [| \ f (Ary1NT x) -> f x |]
+inspect $ 'foldMapAry1NTR ==- 'foldMapAry1NTS
+inspect $ 'foldMapAry1NTR ==- 'foldMapAry1NTG
+
+mk_foldr ''Ary1NT [| \ f r (Ary1NT x) -> f x r |]
+inspect $ 'foldrAry1NTR ==- 'foldrAry1NTS
+inspect $ 'foldrAry1NTR ==- 'foldrAry1NTG
+
+mk_traverse ''Ary1NT [| \ f (Ary1NT x) -> fmap Ary1NT (f x) |]
+inspect $ 'traverseAry1NTR ==- 'traverseAry1NTS
+inspect $ 'traverseAry1NTR ==- 'traverseAry1NTG
+
+mk_ap ''Ary1NT [| \ (Ary1NT f1) (Ary1NT x1) -> Ary1NT (f1 x1) |]
+inspect $ 'apAry1NTR ==- 'apAry1NTG
+
+mk_liftA2 ''Ary1NT [| \ f (Ary1NT x1) (Ary1NT x2) -> Ary1NT (f x1 x2) |]
+inspect $ 'liftA2Ary1NTR ==- 'liftA2Ary1NTG
+
+-- Ary2
+
+mk_eq ''Ary2 [| \ (Ary2 x1 x2) (Ary2 y1 y2) -> x1 == y1 && x2 == y2 |]
+inspect $ 'eqAry2R ==- 'eqAry2S
+inspect $ 'eqAry2R ==- 'eqAry2G
+
+mk_compare ''Ary2 [| \ (Ary2 x1 x2) (Ary2 y1 y2) -> compare x1 y1 <> compare x2 y2 |]
+inspect $ 'compareAry2R ==- 'compareAry2S
+inspect $ 'compareAry2R ==- 'compareAry2G
+
+mk_fmap ''Ary2 [| \ f (Ary2 x y) -> Ary2 (f x) (f y) |]
+inspect $ 'fmapAry2R ==- 'fmapAry2S
+inspect $ 'fmapAry2R ==- 'fmapAry2G
+
+mk_foldMap ''Ary2 [| \ f (Ary2 x y) -> f x `mappend` f y |]
+inspect $ 'foldMapAry2R ==- 'foldMapAry2S
+inspect $ 'foldMapAry2R ==- 'foldMapAry2G
+
+mk_foldr ''Ary2 [| \ f r (Ary2 x y) -> f x (f y r) |]
+inspect $ 'foldrAry2R ==- 'foldrAry2S
+inspect $ 'foldrAry2R ==- 'foldrAry2G
+
+mk_traverse ''Ary2 [| \ f (Ary2 x y) -> liftA2 Ary2 (f x) (f y) |]
+inspect $ 'traverseAry2R ==- 'traverseAry2S
+inspect $ 'traverseAry2R ==- 'traverseAry2G
+
+mk_sequenceA ''Ary2 [| \ (Ary2 x y) -> liftA2 Ary2 x y |]
+inspect $ 'sequenceAAry2R ==- 'sequenceAAry2S
+inspect $ 'sequenceAAry2R ==- 'sequenceAAry2G
+
+mk_ap ''Ary2 [| \ (Ary2 f1 f2) (Ary2 x1 x2) -> Ary2 (f1 x1) (f2 x2) |]
+inspect $ 'apAry2R ==- 'apAry2G
+
+mk_liftA2 ''Ary2 [| \ f (Ary2 x1 y1) (Ary2 x2 y2) -> Ary2 (f x1 x2) (f y1 y2) |]
+inspect $ 'liftA2Ary2R ==- 'liftA2Ary2G
+
+-- Ary4
+
+sequenceAAry4RS :: Applicative f => Ary4 (f a) -> f (Ary4 a)
+sequenceAAry4RS = traverse id
+
+-- The simplifier is good enough to reassociate (&&)
+mk_eq ''Ary4
+  [| \ (Ary4 x1 x2 x3 x4) (Ary4 y1 y2 y3 y4) ->
+       x1 == y1 && x2 == y2 && x3 == y3 && x4 == y4 |]
+inspect $ 'eqAry4R ==- 'eqAry4S
+inspect $ 'eqAry4R ==- 'eqAry4G
+
+-- The simplifier is good enough to reassociate (<>)
+mk_compare ''Ary4
+  [| \ (Ary4 x1 x2 x3 x4) (Ary4 y1 y2 y3 y4) ->
+       compare x1 y1 <> compare x2 y2 <> compare x3 y3 <> compare x4 y4 |]
+inspect $ 'compareAry4R ==- 'compareAry4S
+inspect $ 'compareAry4R ==- 'compareAry4G
+
+mk_fmap ''Ary4
+  [| \ f (Ary4 x y z t) -> Ary4 (f x) (f y) z (fmap f t) |]
+inspect $ 'fmapAry4R ==- 'fmapAry4S
+inspect $ 'fmapAry4R ==- 'fmapAry4G
+
+mk_foldMap ''Ary4
+  [| \ f (Ary4 x y _ z) -> f x `mappend` (f y `mappend` foldMap f z) |]
+inspect $ 'foldMapAry4R ==- 'foldMapAry4S
+inspect $ 'foldMapAry4R ==- 'foldMapAry4G
+
+mk_foldr ''Ary4
+  [| \ f r (Ary4 x y _ t) -> f x (f y (foldr f r t)) |]
+inspect $ 'foldrAry4R ==- 'foldrAry4S
+inspect $ 'foldrAry4R ==- 'foldrAry4G
+
+mk_traverse ''Ary4
+  [| \ f (Ary4 x y z t) ->
+       liftA2 (\x' y' -> Ary4 x' y' z) (f x) (f y) <*> traverse f t |]
+inspect $ 'traverseAry4R ==- 'traverseAry4S
+inspect $ 'traverseAry4R ==- 'traverseAry4G
+
+mk_sequenceA ''Ary4 [| \ (Ary4 x y z t) -> liftA2 (\x' y' -> Ary4 x' y' z) x y <*> sequenceA t |]
+inspect $ 'sequenceAAry4RS ==- 'sequenceAAry4S
+inspect $ 'sequenceAAry4R ==- 'sequenceAAry4G
+
+mk_ap ''Ary4
+  [| \ (Ary4 f1 f2 fz f3) (Ary4 x1 x2 xz x3) ->
+       Ary4 (f1 x1) (f2 x2) (fz <> xz) (f3 <*> x3) |]
+inspect $ 'apAry4R ==- 'apAry4G
+
+mk_liftA2 ''Ary4
+  [| \ f (Ary4 x1 y1 fz z1) (Ary4 x2 y2 xz z2) ->
+       Ary4 (f x1 x2) (f y1 y2) (fz <> xz) (liftA2 f z1 z2) |]
+inspect $ 'liftA2Ary4R ==- 'liftA2Ary4G
+
+-- Big
+
+-- The simplifier is good enough to reassociate (&&)
+mk_eq ''Big
+  [| \ x y -> case (x, y) of
+       (Big0, Big0) -> True
+       (Big1 x1, Big1 y1) ->
+         x1 == y1
+       (Big2 x1 x2, Big2 y1 y2) ->
+         x1 == y1 && x2 == y2
+       (Big4 x1 x2 x3 x4, Big4 y1 y2 y3 y4) ->
+         x1 == y1 && x2 == y2 && x3 == y3 && x4 == y4
+       (Big8 x1 x2 x3 x4 x5 x6 x7 x8, Big8 y1 y2 y3 y4 y5 y6 y7 y8) ->
+         x1 == y1 && x2 == y2 && x3 == y3 && x4 == y4 &&
+         x5 == y5 && x6 == y6 && x7 == y7 && x8 == y8
+       (_, _) -> False |]
+inspect $ 'eqBigR === 'eqBigS
+inspect $ 'eqBigR =/= 'eqBigG -- TODO make this test pass
+
+{- TODO Update the rest, after figuring out the above test case
+-- The simplifier is good enough to reassociate (<>)
+mk_compare ''Big
+  [| \ (Big4 x1 x2 x3 x4) (Big4 y1 y2 y3 y4) ->
+       compare x1 y1 <> compare x2 y2 <> compare x3 y3 <> compare x4 y4 |]
+inspect $ 'compareBigR === 'compareBigS
+inspect $ 'compareBigR === 'compareBigG
+
+mk_fmap ''Big
+  [| \ f (Big4 x y z t) -> Big (f x) (f y) z (fmap f t) |]
+inspect $ 'fmapBigR ==- 'fmapBigS
+inspect $ 'fmapBigR ==- 'fmapBigG
+
+mk_foldMap ''Big
+  [| \ f (Big4 x y _ z) -> f x `mappend` (f y `mappend` foldMap f z) |]
+inspect $ 'foldMapBigR ==- 'foldMapBigS
+inspect $ 'foldMapBigR ==- 'foldMapBigG
+
+mk_foldr ''Big
+  [| \ f r (Big4 x y _ t) -> f x (f y (foldr f r t)) |]
+inspect $ 'foldrBigR ==- 'foldrBigS
+inspect $ 'foldrBigR ==- 'foldrBigG
+
+mk_traverse ''Big
+  [| \ f (Big4 x y z t) ->
+       liftA2 (\x' y' -> Big x' y' z) (f x) (f y) <*> (traverse f t) |]
+inspect $ 'traverseBigR ==- 'traverseBigS
+inspect $ 'traverseBigR ==- 'traverseBigG
+
+mk_sequenceA ''Big [| \ (Big4 x y z t) -> liftA2 (\x' y' -> Big x' y' z) x y <*> sequenceA t |]
+inspect $ 'sequenceABigRS ==- 'sequenceABigS
+inspect $ 'sequenceABigR ==- 'sequenceABigG
+
+mk_ap ''Big
+  [| \ (Big4 f1 f2 fz f3) (Big4 x1 x2 xz x3) ->
+       Big (f1 x1) (f2 x2) (fz <> xz) (f3 <*> x3) |]
+inspect $ 'apBigR ==- 'apBigG
+
+mk_liftA2 ''Big
+  [| \ f (Big4 x1 y1 fz z1) (Big4 x2 y2 xz z2) ->
+       Big (f x1 x2) (f y1 y2) (fz <> xz) (liftA2 f z1 z2) |]
+inspect $ 'liftA2BigR ==- 'liftA2BigG
+-}
+
+-- dummy
+main :: IO ()
+main = pure ()