diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+# 0.3.0.0
+
+- Make surgeries first-class at the type level (`MajorSurgery`)
+
 # 0.2.1.0
 
 - Add `toORLazy` and `fromORLazy`, to clean up data types with strictness
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# Surgery for generic data types [![Hackage](https://img.shields.io/hackage/v/generic-data-surgery.svg)](https://hackage.haskell.org/package/generic-data-surgery) [![Build Status](https://travis-ci.org/Lysxia/generic-data-surgery.svg)](https://travis-ci.org/Lysxia/generic-data-surgery)
+# Surgery for generic data types [![Hackage](https://img.shields.io/hackage/v/generic-data-surgery.svg)](https://hackage.haskell.org/package/generic-data-surgery) [![GitHub CI](https://github.com/Lysxia/generic-data-surgery/workflows/CI/badge.svg)](https://github.com/Lysxia/generic-data-surgery/actions)
 
 Modify, add, or remove constructors and fields in generic types, to be used
 with generic implementations.
@@ -64,6 +64,10 @@
       (checksum f, f)
 ```
 
-See also the
-[`examples/`](https://github.com/Lysxia/generic-data-surgery/tree/master/examples)
-directory in the source repo.
+## See also
+
+- [*Surgery for data types*](https://blog.poisson.chat/posts/2018-11-26-type-surgery.html),
+  introductory blog post with another example.
+
+- The [`examples/`](https://github.com/Lysxia/generic-data-surgery/tree/master/examples)
+  directory in the source repo.
diff --git a/generic-data-surgery.cabal b/generic-data-surgery.cabal
--- a/generic-data-surgery.cabal
+++ b/generic-data-surgery.cabal
@@ -1,5 +1,5 @@
 name:                generic-data-surgery
-version:             0.2.1.0
+version:             0.3.0.0
 synopsis:            Surgery for generic data types
 description:
   Transform data types before passing them to generic functions.
@@ -14,7 +14,7 @@
 extra-source-files:  README.md, CHANGELOG.md
 cabal-version:       >=1.10
 tested-with:
-  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.1, GHC == 8.6.3
+  GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.1, GHC == 8.6.3, GHC == 8.8.3, GHC == 8.10.1
 
 library
   hs-source-dirs:      src
@@ -37,6 +37,24 @@
     generic-data,
     generic-data-surgery,
     base
+  ghc-options: -Wall
+  default-language: Haskell2010
+  type: exitcode-stdio-1.0
+
+test-suite synthetic-test
+  hs-source-dirs: test
+  main-is: synthetic.hs
+  build-depends:
+    tasty,
+    tasty-hunit,
+    generic-data,
+    generic-data-surgery,
+    show-combinators >= 0.2,
+    -- ^ avoid a bug
+    base
+  if !impl(ghc >= 8.6)
+    build-depends:
+      contravariant
   ghc-options: -Wall
   default-language: Haskell2010
   type: exitcode-stdio-1.0
diff --git a/src/Generic/Data/Surgery.hs b/src/Generic/Data/Surgery.hs
--- a/src/Generic/Data/Surgery.hs
+++ b/src/Generic/Data/Surgery.hs
@@ -69,6 +69,12 @@
     --
     -- Note that @()@ and 'Data.Functor.Identity.Identity' can be used as an
     -- empty and a singleton tuple type respectively.
+
+  , removeConstr
+  , insertConstr
+  , modifyConstr
+
+    -- *** Constructors as tuples
     --
     -- When the tuple type can't be inferred and doesn't really matter,
     -- an alternative to explicit type annotations is to use the @...ConstrT@
@@ -76,17 +82,51 @@
     -- (@()@, 'Data.Functor.Identity.Identity', @(,)@, @(,,)@, up to 7 ---
     -- because that's where 'GHC.Generics.Generic' instances currently stop).
 
-  , removeConstr
-  , insertConstr
-  , modifyConstr
   , removeConstrT
   , insertConstrT
   , modifyConstrT
 
+    -- * Surgeries as type-level operations
+
+    -- | Example usage: define a synthetic type which adds a @\"key\"@ field of type @Key@
+    -- to an existing record type.
+    --
+    -- @
+    -- -- Define the surgery to insert a field (key :: Key)
+    -- -- as the first field (index 0) of a record.
+    -- type InsertId = ('InsertField' 0 (''Just' \"key\") Key :: 'MajorSurgery' k)
+    --
+    -- -- Define a newtype for synthetic ('Data') types obtained from a real type @a@
+    -- -- using the @InsertId@ surgery we just defined.
+    -- newtype WithKey a = WithKey ('Data' ('Operate' ('GHC.Generics.Rep' a) InsertId) ())
+    -- @
+
+    -- ** Types and composition
+
+    -- |
+    -- === Implementation notes
+    --
+    -- The implementation of these type synonyms is hidden behind names
+    -- suffixed with an underscore. Although they appear in the haddocks,
+    -- these auxiliary names are internal and not exported by this module.
+
+  , MajorSurgery
+  , Perform
+  , Operate
+  , (:>>)
+  , IdSurgery
+
+    -- ** Surgeries
+  , InsertField
+  , RemoveField
+  , RemoveRField
+  , InsertConstrAt
+  , RemoveConstr
+  , Suture
+
     -- * Constraint synonyms
 
     -- | Hiding implementation details from the signatures above.
-    -- Useful to compose surgeries in a reusable way.
 
     -- ** Conversions
 
diff --git a/src/Generic/Data/Surgery/Internal.hs b/src/Generic/Data/Surgery/Internal.hs
--- a/src/Generic/Data/Surgery/Internal.hs
+++ b/src/Generic/Data/Surgery/Internal.hs
@@ -1,24 +1,28 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE
+    AllowAmbiguousTypes,
+    BangPatterns,
+    ConstraintKinds,
+    DataKinds,
+    DeriveGeneric,
+    FlexibleContexts,
+    FlexibleInstances,
+    LambdaCase,
+    MultiParamTypeClasses,
+    PolyKinds,
+    ScopedTypeVariables,
+    TypeApplications,
+    TypeFamilies,
+    TypeOperators,
+    TypeInType,
+    UndecidableInstances,
+    UndecidableSuperClasses #-}
 
 -- | Operate on data types: insert\/modify\/delete fields and constructors.
 
 module Generic.Data.Surgery.Internal where
 
 import Control.Monad ((<=<))
-import Data.Bifunctor (bimap, first)
+import Data.Bifunctor (first, second)
 import Data.Coerce
 import Data.Functor.Identity (Identity)
 import Data.Kind (Constraint, Type)
@@ -27,13 +31,14 @@
 import GHC.TypeLits
 
 import Fcf
-  ( Eval, If, _If, IsBool, Pure, Pure2, Bimap, Uncurry
-  , type (=<<), type (<=<), type (<$>)
+  ( Exp, Eval, If, Pure, Pure2, Bimap, Uncurry
+  , type (@@), type (=<<), type (<=<), type (<$>)
   )
 
+import Generic.Data (MetaOf, MetaConsName)
 import Generic.Data.Internal.Compat (Div)
 import Generic.Data.Internal.Data (Data(Data,unData))
-import Generic.Data.Internal.Meta (MetaOf, MetaConsName, UnM1)
+import Generic.Data.Internal.Meta (UnM1)
 import Generic.Data.Internal.Utils (coerce', absurd1)
 
 -- | /A sterile Operating Room, where generic data comes to be altered./
@@ -579,11 +584,10 @@
 --
 -- Note that there is no dependency to determine @t@.
 removeConstr
-  :: forall    c n t lc l l_t x
-  .  RmvConstr c n t lc l l_t
+  :: forall    c n t lc l x
+  .  RmvConstr c n t lc l
   => OR lc x -> Either t (OR l x)
-removeConstr (OR a) = bimap
-  (to . coerce' . gArborify @(Arborify l_t)) OR (gRemoveConstr @n a)
+removeConstr (OR a) = second OR (gRemoveConstr @n a)
 
 -- | A variant of 'removeConstr' that can infer the tuple type @t@ to hold
 -- the contents of the removed constructor.
@@ -598,8 +602,8 @@
 -- l_t -> t
 -- @
 removeConstrT
-  :: forall     c n t lc l l_t x
-  .  RmvConstrT c n t lc l l_t
+  :: forall     c n t lc l x
+  .  RmvConstrT c n t lc l
   => OR lc x -> Either t (OR l x)
 removeConstrT = removeConstr @c @n @t
 
@@ -640,12 +644,10 @@
 --
 -- Note that there is no dependency to determine @t@.
 insertConstr
-  :: forall    c n t lc l l_t x
-  .  InsConstr c n t lc l l_t
+  :: forall    c n t lc l x
+  .  InsConstr c n t lc l
   => Either t (OR l x) -> OR lc x
-insertConstr z =
-  OR (gInsertConstr @n
-    (bimap (gLinearize @(Arborify l_t) . coerce' . from) unOR z))
+insertConstr z = OR (gInsertConstr @n (second unOR z))
 
 -- | A variant of 'insertConstr' that can infer the tuple type @t@ to hold
 -- the contents of the inserted constructor.
@@ -660,8 +662,8 @@
 -- l_t -> t
 -- @
 insertConstrT
-  :: forall     c n t lc l l_t x
-  .  InsConstrT c n t lc l l_t
+  :: forall     c n t lc l x
+  .  InsConstrT c n t lc l
   => Either t (OR l x) -> OR lc x
 insertConstrT = insertConstr @c @n @t
 
@@ -708,8 +710,8 @@
 --
 -- Note that there is no dependency to determine @t@ and @t'@.
 modifyConstr
-  :: forall    c n t t' lc lc' l l_t l_t' x
-  .  ModConstr c n t t' lc lc' l l_t l_t'
+  :: forall    c n t t' lc lc' l x
+  .  ModConstr c n t t' lc lc' l
   => (t -> t') -> OR lc x -> OR lc' x
 modifyConstr f = insertConstr @c @n @t' . first f . removeConstr @c @n @t
 
@@ -727,8 +729,8 @@
 -- l_t' -> t'
 -- @
 modifyConstrT
-  :: forall     c n t t' lc lc' l l_t l_t' x
-  .  ModConstrT c n t t' lc lc' l l_t l_t'
+  :: forall     c n t t' lc lc' l x
+  .  ModConstrT c n t t' lc lc' l
   => (t -> t') -> OR lc x -> OR lc' x
 modifyConstrT = modifyConstr @c @n @t @t'
 
@@ -737,28 +739,28 @@
 -- | This constraint means that the (unnamed) field row @lt@ contains
 -- a field of type @t@ at position @n@, and removing it yields row @l@.
 type RmvCField n t lt l =
-  ( GRemoveField n lt
+  ( GRemoveField n t lt l
   , CFieldSurgery n t lt l
   )
 
 -- | This constraint means that the record field row @lt@ contains a field of
 -- type @t@ named @fd@ at position @n@, and removing it yields row @l@.
 type RmvRField fd n t lt l =
-  ( GRemoveField n lt
+  ( GRemoveField n t lt l
   , RFieldSurgery fd n t lt l
   )
 
 -- | This constraint means that inserting a field @t@ at position @n@ in the
 -- (unnamed) field row @l@ yields row @lt@.
 type InsCField n t lt l =
-  ( GInsertField n lt
+  ( GInsertField n t l lt
   , CFieldSurgery n t lt l
   )
 
 -- | This constraint means that inserting a field @t@ named @fd@ at position
 -- @n@ in the record field row @l@ yields row @lt@.
 type InsRField fd n t lt l =
-  ( GInsertField n lt
+  ( GInsertField n t l lt
   , RFieldSurgery fd n t lt l
   )
 
@@ -782,52 +784,50 @@
 -- named @c@ at position @n@, and removing it from @lc@ yields row @l@.
 -- Furthermore, constructor @c@ contains a field row @l_t@ compatible with the
 -- tuple type @t@.
-type RmvConstr c n t lc l l_t =
-  ( GRemoveConstr n lc
-  , GArborify (Arborify l_t)
-  , ConstrSurgery c n t lc l l_t
+type RmvConstr c n t lc l =
+  ( GRemoveConstr n t lc l
+  , ConstrSurgery c n t lc l (Eval (ConstrAt n lc))
   )
 
 -- | A variant of 'RmvConstr' allowing @t@ to be inferred.
-type RmvConstrT c n t lc l l_t =
-  ( RmvConstr c n t lc l l_t
-  , IsTuple (Arity l_t) t
+type RmvConstrT c n t lc l =
+  ( RmvConstr c n t lc l
+  , IsTuple (Arity (Eval (ConstrAt n lc))) t
   )
 
 -- | This constraint means that inserting a constructor @c@ at position @n@
 -- in the constructor row @l@ yields row @lc@.
 -- Furthermore, constructor @c@ contains a field row @l_t@ compatible with the
 -- tuple type @t@.
-type InsConstr c n t lc l l_t =
-  ( GInsertConstr n lc
-  , GLinearize (Arborify l_t)
-  , ConstrSurgery c n t lc l l_t
+type InsConstr c n (t :: Type) lc l =
+  ( GInsertConstr n t l lc
+  , ConstrSurgery c n t lc l (Eval (ConstrAt n lc))
   )
 
 -- | A variant of 'InsConstr' allowing @t@ to be inferred.
-type InsConstrT c n t lc l l_t =
-  ( InsConstr c n t lc l l_t
-  , IsTuple (Arity l_t) t
+type InsConstrT c n t lc l =
+  ( InsConstr c n t lc l
+  , IsTuple (Arity (Eval (ConstrAt n lc))) t
   )
 
 -- | This constraint means that the constructor row @lc@ contains a constructor
 -- named @c@ at position @n@ of type isomorphic to @t@, and modifying it to
 -- @t'@ yields row @lc'@.
-type ModConstr c n t t' lc lc' l l_t l_t' =
-  ( RmvConstr c n t  lc  l l_t
-  , InsConstr c n t' lc' l l_t'
+type ModConstr c n t t' lc lc' l =
+  ( RmvConstr c n t  lc  l
+  , InsConstr c n t' lc' l
   )
 
 -- | A variant of 'ModConstr' allowing @t@ and @t'@ to be inferred.
-type ModConstrT c n t t' lc lc' l l_t l_t' =
-  ( ModConstr c n t t' lc lc' l l_t l_t'
-  , IsTuple (Arity l_t) t
-  , IsTuple (Arity l_t') t'
+type ModConstrT c n t t' lc lc' l =
+  ( ModConstr c n t t' lc lc' l
+  , IsTuple (Arity (Eval (ConstrAt n lc ))) t
+  , IsTuple (Arity (Eval (ConstrAt n lc'))) t'
   )
 
 type FieldSurgery n t lt l =
   ( t ~ Eval (FieldTypeAt n lt)
-  , l ~ Eval (RemoveField n lt)
+  , l ~ Eval (RemoveField n t lt)
   )
 
 type CFieldSurgery n t lt l =
@@ -843,28 +843,25 @@
 
 type ConstrSurgery c n t lc l l_t =
   ( Generic t
-  , MatchFields (UnM1 (Rep t)) (Arborify l_t)
-  , Coercible (Arborify l_t) (Rep t)
+  , MatchFields (Linearize (UnM1 (Rep t))) l_t
   , n ~ Eval (ConstrIndex c lc)
   , c ~ MetaConsName (MetaOf l_t)
-  , l_t ~ Linearize (Arborify l_t)
-  , l_t ~ Eval (ConstrAt n lc)
-  , lc ~ Eval (InsertConstr n l_t l)
-  , l ~ Eval (RemoveConstr n lc)
+  , lc ~ Eval (InsertUConstrAtL n l_t l)
+  , l ~ Eval (RemoveUConstrAt_ n lc)
   )
 
 --
 
-type family   Linearize (f :: k -> *) :: k -> *
+type family   Linearize (f :: k -> Type) :: k -> Type
 type instance Linearize (M1 D m f) = M1 D m (LinearizeSum f V1)
 type instance Linearize (M1 C m f) = M1 C m (LinearizeProduct f U1)
 
-type family   LinearizeSum (f :: k -> *) (tl :: k -> *) :: k -> *
+type family   LinearizeSum (f :: k -> Type) (tl :: k -> Type) :: k -> Type
 type instance LinearizeSum V1 tl = tl
 type instance LinearizeSum (f :+: g) tl = LinearizeSum f (LinearizeSum g tl)
 type instance LinearizeSum (M1 c m f) tl = M1 c m (LinearizeProduct f U1) :+: tl
 
-type family   LinearizeProduct (f :: k -> *) (tl :: k -> *) :: k -> *
+type family   LinearizeProduct (f :: k -> Type) (tl :: k -> Type) :: k -> Type
 type instance LinearizeProduct U1 tl = tl
 type instance LinearizeProduct (f :*: g) tl = LinearizeProduct f (LinearizeProduct g tl)
 type instance LinearizeProduct (M1 s m f) tl = M1 s m f :*: tl
@@ -948,18 +945,18 @@
 instance GArborifyProduct (M1 s m f) tl where
   gArborifyProduct (a :*: c) = (a, c)
 
-type family   Arborify (f :: k -> *) :: k -> *
+type family   Arborify (f :: k -> Type) :: k -> Type
 type instance Arborify (M1 D m f) = M1 D m (Eval (ArborifySum (CoArity f) f))
 type instance Arborify (M1 C m f) = M1 C m (Eval (ArborifyProduct (Arity f) f))
 
-data ArborifySum (n :: Nat) (f :: k -> *) :: (k -> *) -> *
+data ArborifySum (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
 type instance Eval (ArborifySum n V1) = V1
 type instance Eval (ArborifySum n (f :+: g)) =
   Eval (If (n == 1)
     (ArborifyProduct (Arity f) f)
     (Arborify' ArborifySum (:+:) n (Div n 2) f g))
 
-data ArborifyProduct (n :: Nat) (f :: k -> *) :: (k -> *) -> *
+data ArborifyProduct (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
 type instance Eval (ArborifyProduct n (M1 C s f)) = M1 C s (Eval (ArborifyProduct n f))
 type instance Eval (ArborifyProduct n U1) = U1
 type instance Eval (ArborifyProduct n (f :*: g)) =
@@ -974,7 +971,7 @@
    <=< SplitAt nDiv2
    ) (op f g)
 
-type family Lazify (f :: k -> *) :: k -> *
+type family Lazify (f :: k -> Type) :: k -> Type
 type instance Lazify (M1 i m f) = M1 i (LazifyMeta m) (Lazify f)
 type instance Lazify (f :*: g) = Lazify f :*: Lazify g
 type instance Lazify (f :+: g) = Lazify f :+: Lazify g
@@ -988,7 +985,7 @@
 type instance LazifyMeta ('MetaSel mn su ss ds)
   = 'MetaSel mn 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
 
-data SplitAt :: Nat -> (k -> *) -> (k -> *, k -> *) -> *
+data SplitAt :: Nat -> (k -> Type) -> Exp (k -> Type, k -> Type)
 type instance Eval (SplitAt n (f :+: g)) =
   Eval (If (n == 0)
     (Pure '(V1, f :+: g))
@@ -998,25 +995,145 @@
     (Pure '(U1, f :*: g))
     (Bimap (Pure2 (:*:) f) Pure =<< SplitAt (n-1) g))
 
-data FieldTypeAt (n :: Nat) (f :: k -> *) :: * -> *
+-- * Surgeries
+
+-- | Kind of surgeries: operations on generic representations of types.
+--
+-- Treat this as an abstract kind (don't pay attention to its definition).
+--
+-- === __Implementation details__
+--
+-- The name @Surgery@ got taken first by generic-data.
+--
+-- @k@ is the kind of the extra parameter reserved for @Generic1@,
+-- which we just don't use.
+type MajorSurgery k = MajorSurgery_ k
+
+-- Whenever you see
+--   data ... :: MajorSurgery k
+-- mentally expand it to
+--   data ... (f :: k -> Type) :: Exp (k -> Type)
+
+-- | @Operate f s@. Apply a surgery @s@ to a generic representation @f@
+-- (e.g., @f = 'Rep' a@ for some 'Generic' type @a@).
+--
+-- The first argument is the generic representation;
+-- the second argument is the surgery, which typically has the more complex
+-- syntax, which is why this reverse application order was chosen.
+type Operate (f :: k -> Type) (s :: MajorSurgery k) = Operate_ f s
+
+-- | Internal definition of 'MajorSurgery'.
+type MajorSurgery_ k = (k -> Type) -> Exp (k -> Type)
+
+-- | Internal definition of 'Operate'.
+type Operate_ (f :: k -> Type) (s :: MajorSurgery k) = Arborify (OperateL (Linearize f) s)
+
+-- | Apply a surgery @s@ to a linearized generic representation @l@.
+type OperateL (l :: k -> Type) (s :: MajorSurgery k) = Eval (s l)
+
+-- | Composition of surgeries (left-to-right).
+--
+-- === Note
+--
+-- Surgeries work on normalized representations, so 'Operate', which applies
+-- a surgery to a generic representation, inserts normalization steps before
+-- and after the surgery. This means that @'Operate' r (s1 ':>>' s2)@ is not quite
+-- the same as @'Operate' ('Operate' r s1) s2@. Instead, the latter is
+-- equivalent to @'Operate' r (s1 ':>>' 'Suture' ':>>' s2)@, where 'Suture'
+-- inserts some intermediate normalization steps.
+data (:>>) :: MajorSurgery k -> MajorSurgery k -> MajorSurgery k
+type instance Eval ((s :>> t) l) = Eval (t (Eval (s l)))
+-- Note: This is a specialization of @(>=>)@ in Fcf.
+
+type instance PerformL l (s :>> t) = (PerformL l s, PerformL (Eval (s l)) t)
+
+infixl 1 :>>
+
+-- | The identity surgery: doesn't do anything.
+data IdSurgery :: MajorSurgery k
+type instance Eval (IdSurgery l) = l
+type instance PerformL l IdSurgery = ()
+
+-- | Use this if a patient ever needs to go out and back into the operating
+-- room, when it's not just to undo the surgery up to that point.
+data Suture :: MajorSurgery k
+type instance Eval (Suture l) = Linearize (Arborify l)
+
+-- Now we can compose surgeries into complex ones, we can relate the input and
+-- output of a whole surgery.
+--
+-- We still need to augment this with run-time information to 'Perform' the
+-- surgery at the term level.
+--
+-- We might also need to interpret surgeries backwards (this is not entirely
+-- symmetrical, a "removal" contains less information than an "insertion").
+
+type family PerformL (l :: k -> Type) (s :: MajorSurgery k) :: Constraint
+
+-- | A constraint @Perform r s@ means that the surgery @s@ can be applied to
+-- the generic representation @r@.
+class    Perform_ r s => Perform (r :: k -> Type) (s :: MajorSurgery k)
+instance Perform_ r s => Perform (r :: k -> Type) (s :: MajorSurgery k)
+
+type Perform_ (r :: k -> Type) (s :: MajorSurgery k) =
+  ( PerformL (Linearize r) s
+  , ToOR r (Linearize r)
+  , FromOR (Operate r s) (OperateL (Linearize r) s)
+  )
+
+data FieldTypeAt (n :: Nat) (f :: k -> Type) :: Exp Type
 type instance Eval (FieldTypeAt n (M1 i c f)) = Eval (FieldTypeAt n f)
 type instance Eval (FieldTypeAt n (f :+: V1)) = Eval (FieldTypeAt n f)
 type instance Eval (FieldTypeAt n (f :*: g)) =
   Eval (If (n == 0) (Pure (FieldTypeOf f)) (FieldTypeAt (n-1) g))
 
-type family   FieldTypeOf (f :: k -> *) :: *
+type family   FieldTypeOf (f :: k -> Type) :: Type
 type instance FieldTypeOf (M1 s m (K1 i a)) = a
 
-data RemoveField (n :: Nat) (f :: k -> *) :: (k -> *) -> *
-type instance Eval (RemoveField n (M1 i m f)) = M1 i m (Eval (RemoveField n f))
-type instance Eval (RemoveField n (f :+: V1)) = Eval (RemoveField n f) :+: V1
-type instance Eval (RemoveField n (f :*: g)) =
-  Eval (If (n == 0) (Pure g) ((:*:) f <$> RemoveField (n-1) g))
+data FieldNameAt (n :: Nat) (f :: k -> Type) :: Exp (Maybe Symbol)
+type instance Eval (FieldNameAt n (M1 i c f)) = Eval (FieldNameAt n f)
+type instance Eval (FieldNameAt n (f :+: V1)) = Eval (FieldNameAt n f)
+type instance Eval (FieldNameAt n (f :*: g)) =
+  Eval (If (n == 0) (FieldNameOf f) (FieldNameAt (n-1) g))
 
+data FieldNameOf (f :: k -> Type) :: Exp (Maybe Symbol)
+type instance Eval (FieldNameOf (M1 S ('MetaSel mn _ _ _) _)) = mn
+
+data RemoveField (n :: Nat) (a :: Type) :: MajorSurgery k
+type instance Eval (RemoveField n a f) = Eval (RemoveField_ n f)
+
+-- | Like 'RemoveField' but without the explicit field type.
+data RemoveField_ (n :: Nat) :: MajorSurgery k
+type instance Eval (RemoveField_ n (M1 i m f)) = M1 i m (Eval (RemoveField_ n f))
+type instance Eval (RemoveField_ n (f :+: V1)) = Eval (RemoveField_ n f) :+: V1
+type instance Eval (RemoveField_ n (f :*: g)) =
+  Eval (If (n == 0) (Pure g) ((:*:) f <$> RemoveField_ (n-1) g))
+
+type instance PerformL lt (RemoveField n a) = PerformL lt (RemoveFieldAt n (FieldNameAt n @@ lt) a)
+
+data RemoveFieldAt (n :: Nat) (fd :: Maybe Symbol) (a :: Type) :: MajorSurgery k
+type instance PerformL lt (RemoveFieldAt n fd a) =
+  PerformLRemoveFieldAt n fd a lt (Eval (RemoveField_ n lt))
+
+type PerformLRemoveFieldAt_ n fd t lt l =
+  ( GRemoveField n t lt l
+  , t ~ Eval (FieldTypeAt n lt)
+  , lt ~ Eval (InsertField n fd t l)
+  )
+
+class    PerformLRemoveFieldAt_ n fd t lt l => PerformLRemoveFieldAt n fd t lt l
+instance PerformLRemoveFieldAt_ n fd t lt l => PerformLRemoveFieldAt n fd t lt l
+
+data RemoveRField (fd :: Symbol) (a :: Type) :: MajorSurgery k
+type instance Eval (RemoveRField fd a f) = Eval (RemoveField_ (Eval (FieldIndex fd f)) f)
+
+type instance PerformL lt (RemoveRField fd a) =
+  PerformL lt (RemoveFieldAt (FieldIndex fd @@ lt) ('Just fd) a)
+
 type DefaultMetaSel field
   = 'MetaSel field 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
 
-data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: *) (f :: k -> *) :: (k -> *) -> *
+data InsertField (n :: Nat) (fd :: Maybe Symbol) (t :: Type) :: MajorSurgery k
 type instance Eval (InsertField n fd t (M1 D m f)) = M1 D m (Eval (InsertField n fd t f))
 type instance Eval (InsertField n fd t (M1 C m f)) = M1 C m (Eval (InsertField n fd t f))
 type instance Eval (InsertField n fd t (f :+: V1)) = Eval (InsertField n fd t f) :+: V1
@@ -1026,11 +1143,28 @@
     ((:*:) f <$> InsertField (n-1) fd t g))
 type instance Eval (InsertField 0 fd t U1) = M1 S (DefaultMetaSel fd) (K1 R t) :*: U1
 
-data Succ :: Nat -> Nat -> *
+type instance PerformL l (InsertField n fd t) = PerformLInsert n fd t l (Eval (InsertField n fd t l))
+
+type PerformLInsert_ n fd t l tl =
+  ( GInsertField n t l tl
+  , l ~ Eval (RemoveField_ n tl)
+  , tl ~ Eval (InsertField n fd t l)
+  , CheckField n fd tl
+  , t ~ Eval (FieldTypeAt n tl)
+  )
+
+class    PerformLInsert_ n fd t l tl => PerformLInsert n fd t l tl
+instance PerformLInsert_ n fd t l tl => PerformLInsert n fd t l tl
+
+type family CheckField (n :: Nat) (fd :: Maybe Symbol) (tl :: k -> Type) :: Constraint where
+  CheckField n 'Nothing tl = ()
+  CheckField n ('Just fd) tl = (n ~ Eval (FieldIndex fd tl))
+
+data Succ :: Nat -> Exp Nat
 type instance Eval (Succ n) = 1 + n
 
 -- | Position of a record field
-data FieldIndex (field :: Symbol) (f :: k -> *) :: Nat -> *
+data FieldIndex (field :: Symbol) (f :: k -> Type) :: Exp Nat
 type instance Eval (FieldIndex field (M1 D m f)) = Eval (FieldIndex field f)
 type instance Eval (FieldIndex field (M1 C m f)) = Eval (FieldIndex field f)
 type instance Eval (FieldIndex field (f :+: V1)) = Eval (FieldIndex field f)
@@ -1038,7 +1172,7 @@
   = Eval (If (field == field') (Pure 0) (Succ =<< FieldIndex field g))
 
 -- | Number of fields of a single constructor
-type family   Arity (f :: k -> *) :: Nat
+type family   Arity (f :: k -> Type) :: Nat
 type instance Arity (M1 d m f) = Arity f
 type instance Arity (f :+: V1) = Arity f
 type instance Arity (f :*: g) = Arity f + Arity g
@@ -1046,113 +1180,208 @@
 type instance Arity U1 = 0
 
 -- | Number of constructors of a data type
-type family   CoArity (f :: k -> *) :: Nat
+type family   CoArity (f :: k -> Type) :: Nat
 type instance CoArity (M1 D m f) = CoArity f
 type instance CoArity (M1 C m f) = 1
 type instance CoArity V1         = 0
 type instance CoArity (f :+: g)  = CoArity f + CoArity g
 
-class GRemoveField (n :: Nat) f where
-  gRemoveField :: f x -> (Eval (FieldTypeAt n f), Eval (RemoveField n f) x)
+class GRemoveField (n :: Nat) a f g where
+  gRemoveField :: f x -> (a, g x)
 
-instance GRemoveField n f => GRemoveField n (M1 i c f) where
+instance GRemoveField n a f g => GRemoveField n a (M1 i c f) (M1 i c g) where
   gRemoveField (M1 a) = M1 <$> gRemoveField @n a
 
-instance GRemoveField n f => GRemoveField n (f :+: V1) where
+-- Only single-constructor types are supported for the moment.
+instance GRemoveField n a f g => GRemoveField n a (f :+: V1) (g :+: V1) where
   gRemoveField (L1 a) = L1 <$> gRemoveField @n a
   gRemoveField (R1 v) = absurd1 v
 
-instance (If (n == 0) (() :: Constraint) (GRemoveField (n-1) g), IsBool (n == 0))
-  => GRemoveField n (M1 s m (K1 i t) :*: g) where
-  gRemoveField (a@(M1 (K1 t)) :*: b) = _If @(n == 0)
-    (t, b)
-    ((a :*:) <$> gRemoveField @(n-1) b)
+instance GRemoveField 0 a (M1 s m (K1 i a) :*: f) f where
+  gRemoveField (M1 (K1 t) :*: b) = (t, b)
 
-class GInsertField (n :: Nat) f where
-  gInsertField :: Eval (FieldTypeAt n f) -> Eval (RemoveField n f) x -> f x
+instance {-# OVERLAPPABLE #-}
+  ( (n == 0) ~ 'False
+  , f0g ~ (f0 :*: g)
+  , GRemoveField (n-1) a f g
+  ) => GRemoveField n a (f0 :*: f) f0g where
+  gRemoveField (a :*: b) = (a :*:) <$> gRemoveField @(n-1) b
 
-instance GInsertField n f => GInsertField n (M1 i c f) where
+class GInsertField (n :: Nat) a f g where
+  gInsertField :: a -> f x -> g x
+
+instance GInsertField n a f g => GInsertField n a (M1 i c f) (M1 i c g) where
   gInsertField t (M1 a) = M1 (gInsertField @n t a)
 
-instance GInsertField n f => GInsertField n (f :+: V1) where
+instance GInsertField n a f g => GInsertField n a (f :+: V1) (g :+: V1) where
   gInsertField t (L1 a) = L1 (gInsertField @n t a)
   gInsertField _ (R1 v) = absurd1 v
 
-instance (If (n == 0) (() :: Constraint) (GInsertField (n-1) g), IsBool (n == 0))
-  => GInsertField n (M1 s m (K1 i t) :*: g) where
-  gInsertField t ab = _If @(n == 0)
-    (M1 (K1 t) :*: ab)
-    (let a :*: b = ab in a :*: gInsertField @(n-1) t b)
+instance GInsertField 0 a f (M1 s m (K1 i a) :*: f) where
+  gInsertField t ab = M1 (K1 t) :*: ab
 
-data ConstrAt (n :: Nat) (f :: k -> *) :: (k -> *) -> *
+instance {-# OVERLAPPABLE #-}
+  ( (n == 0) ~ 'False
+  , f0f ~ (f0 :*: f)
+  , GInsertField (n-1) a f g
+  ) => GInsertField n a f0f (f0 :*: g) where
+  gInsertField t (a :*: b) = a :*: gInsertField @(n-1) t b
+
+data ConstrAt (n :: Nat) (f :: k -> Type) :: Exp (k -> Type)
 type instance Eval (ConstrAt n (M1 i m f)) = Eval (ConstrAt n f)
 type instance Eval (ConstrAt n (f :+: g)) =
   Eval (If (n == 0) (Pure f) (ConstrAt (n-1) g))
 
-data RemoveConstr (n :: Nat) (f :: k -> *) :: (k -> *) -> *
-type instance Eval (RemoveConstr n (M1 i m f)) = M1 i m (Eval (RemoveConstr n f))
-type instance Eval (RemoveConstr n (f :+: g)) =
-  Eval (If (n == 0) (Pure g) ((:+:) f <$> RemoveConstr (n-1) g))
+data RemoveConstr (c :: Symbol) (t :: Type) :: MajorSurgery k
+type instance Eval (RemoveConstr c t l) = Eval (RemoveConstrAt c (ConstrIndex c @@ l) t l)
 
-data InsertConstr (n :: Nat) (t :: k -> *) (f :: k -> *) :: (k -> *) -> *
-type instance Eval (InsertConstr n t (M1 i m f)) = M1 i m (Eval (InsertConstr n t f))
-type instance Eval (InsertConstr n t (f :+: g)) =
-  Eval (If (n == 0) (Pure (t :+: (f :+: g))) ((:+:) f <$> InsertConstr (n-1) t g))
-type instance Eval (InsertConstr 0 t V1) = t :+: V1
+type instance PerformL lc (RemoveConstr c t) = PerformLRemoveConstr lc c (ConstrIndex c @@ lc) t
 
-data ConstrIndex (con :: Symbol) (f :: k -> *) :: Nat -> *
+type PerformLRemoveConstr lc c n (t :: Type) =
+  PerformLRemoveConstrAt c n t (Eval (ConstrAt n lc)) lc (Eval (RemoveUConstrAt_ n lc))
+
+type PerformLRemoveConstrAt_ c n t l_t lc l =
+  ( GRemoveConstr n t lc l
+  -- , l_t ~ Linearize (Arborify l_t)
+  , c ~ MetaConsName (MetaOf l_t)
+  , lc ~ Eval (InsertUConstrAtL n l_t l)
+  , MatchFields (Linearize (UnM1 (Rep t))) l_t
+  , Arity l_t ~ Arity (Linearize (UnM1 (Rep t)))
+  )
+
+class    PerformLRemoveConstrAt_ c n t l_t lc l => PerformLRemoveConstrAt c n (t :: Type) l_t lc l
+instance PerformLRemoveConstrAt_ c n t l_t lc l => PerformLRemoveConstrAt c n (t :: Type) l_t lc l
+
+data RemoveConstrAt (c :: Symbol) (n :: Nat) (t :: Type) :: MajorSurgery k
+type instance Eval (RemoveConstrAt _ n t l) = Eval (RemoveUConstrAt n t l)
+
+data RemoveUConstrAt (n :: Nat) (t :: Type) :: MajorSurgery k
+type instance Eval (RemoveUConstrAt n _ l) = Eval (RemoveUConstrAt_ n l)
+
+-- | Like 'RemoveConstr', but without the explicit constructor type.
+data RemoveUConstrAt_ (n :: Nat) :: MajorSurgery k
+type instance Eval (RemoveUConstrAt_ n (M1 i m f)) = M1 i m (Eval (RemoveUConstrAt_ n f))
+type instance Eval (RemoveUConstrAt_ n (f :+: g)) =
+  Eval (If (n == 0) (Pure g) ((:+:) f <$> RemoveUConstrAt_ (n-1) g))
+
+-- | This is polymorphic to allow different ways of specifying the inserted constructor.
+--
+-- If @sym@ (the kind of the constructor name @c@) is:
+--
+-- - 'Symbol': treat it like a regular prefix constructor.
+-- - TODO Infix constructors and their fixities.
+--
+-- @t@ must be a single-constructor type, then we reuse its generic
+-- representation for the new constructor, only replacing its constructor name
+-- with @c@.
+data InsertConstrAt (c :: sym) (n :: Nat) (t :: ty) :: MajorSurgery k
+type instance Eval (InsertConstrAt c n t l) = Eval (InsertUConstrAtL n (ConGraft c t) l)
+
+type family ConGraft (c :: sym) (t :: ty) :: k -> Type
+type instance ConGraft c (t :: Type) = RenameCon c (Linearize (UnM1 (Rep t)))
+
+type family RenameCon (c :: sym) (t :: k -> Type) :: k -> Type
+type instance RenameCon c (M1 C m f) = M1 C (RenameMeta c m) f
+
+type family RenameMeta (c :: sym) (m :: Meta) :: Meta
+type instance RenameMeta (s :: Symbol) ('MetaCons _ _ r) = 'MetaCons s 'PrefixI r
+
+type instance PerformL l (InsertConstrAt c n t) = PerformLInsertConstrAt0 l c n t
+
+type PerformLInsertConstrAt0 l c n t =
+  PerformLInsertConstrAt c n t (ConGraft c t) l (Eval (InsertUConstrAtL n (ConGraft c t) l))
+
+type PerformLInsertConstrAt_ c n t l_t l lc =
+  ( GInsertConstr n t l lc
+  , c ~ MetaConsName (MetaOf l_t)
+  , n ~ (ConstrIndex c @@ lc)
+  , l_t ~ (ConstrAt n @@ lc)
+  , l ~ Eval (RemoveUConstrAt_ n lc)
+  , MatchFields (Linearize (UnM1 (Rep t))) l_t
+  )
+
+class    PerformLInsertConstrAt_ c n t l_t l lc => PerformLInsertConstrAt c n t l_t l lc
+instance PerformLInsertConstrAt_ c n t l_t l lc => PerformLInsertConstrAt c n t l_t l lc
+
+data InsertUConstrAt (n :: Nat) (t :: Type) :: MajorSurgery k
+type instance Eval (InsertUConstrAt n t l) = Eval (InsertUConstrAtL n (Linearize (UnM1 (Rep t))) l)
+
+data InsertUConstrAtL (n :: Nat) (t :: k -> Type) :: MajorSurgery k
+type instance Eval (InsertUConstrAtL n t (M1 i m f)) = M1 i m (Eval (InsertUConstrAtL n t f))
+type instance Eval (InsertUConstrAtL n t (f :+: g)) =
+  Eval (If (n == 0) (Pure (t :+: (f :+: g))) ((:+:) f <$> InsertUConstrAtL (n-1) t g))
+type instance Eval (InsertUConstrAtL 0 t V1) = t :+: V1
+
+data ConstrIndex (con :: Symbol) (f :: k -> Type) :: Exp Nat
 type instance Eval (ConstrIndex con (M1 D m f)) = Eval (ConstrIndex con f)
 type instance Eval (ConstrIndex con (M1 C ('MetaCons con' fx s) f :+: g)) =
   Eval (If (con == con') (Pure 0) (Succ =<< ConstrIndex con g))
 
-class GRemoveConstr (n :: Nat) f where
-  gRemoveConstr :: f x -> Either (Eval (ConstrAt n f) x) (Eval (RemoveConstr n f) x)
+class GRemoveConstr (n :: Nat) (t :: Type) f g where
+  gRemoveConstr :: f x -> Either t (g x)
 
-instance GRemoveConstr n f => GRemoveConstr n (M1 i c f) where
+instance GRemoveConstr n t f g => GRemoveConstr n t (M1 i c f) (M1 i c g) where
   gRemoveConstr (M1 a) = M1 <$> gRemoveConstr @n a
 
-instance (If (n == 0) (() :: Constraint) (GRemoveConstr (n-1) g), IsBool (n == 0))
-  => GRemoveConstr n (f :+: g) where
-  gRemoveConstr = _If @(n == 0)
-    (\case
-      L1 a -> Left a
-      R1 b -> Right b)
-    (\case
-      L1 a -> Right (L1 a)
-      R1 b -> R1 <$> gRemoveConstr @(n-1) b)
+type ConstrArborify t l =
+  ( Generic t
+  , Coercible (UnM1 (Rep t)) (Rep t)
+  , GArborify (UnM1 (Rep t))
+  , Coercible l (Linearize (UnM1 (Rep t)))
+  )
 
-class GInsertConstr (n :: Nat) f where
-  gInsertConstr :: Either (Eval (ConstrAt n f) x) (Eval (RemoveConstr n f) x) -> f x
+constrArborify' :: forall t l x. ConstrArborify t l => l x -> t
+constrArborify' = to @t @x . coerce (gArborify @(UnM1 (Rep t)) @x)
 
-instance GInsertConstr n f => GInsertConstr n (M1 i c f) where
+instance ConstrArborify t l => GRemoveConstr 0 t (l :+: f) f where
+  gRemoveConstr (L1 a) = Left (constrArborify' a)
+  gRemoveConstr (R1 b) = Right b
+
+instance {-# OVERLAPPABLE #-}
+  ( GRemoveConstr (n-1) t f g, (n == 0) ~ 'False
+  , f0g ~ (f0 :+: g)
+  ) => GRemoveConstr n t (f0 :+: f) f0g where
+  gRemoveConstr (L1 a) = Right (L1 a)
+  gRemoveConstr (R1 b) = R1 <$> gRemoveConstr @(n-1) b
+
+class GInsertConstr (n :: Nat) (t :: Type) f g where
+  gInsertConstr :: Either t (f x) -> g x
+
+instance GInsertConstr n t f g => GInsertConstr n t (M1 i c f) (M1 i c g) where
   gInsertConstr = M1 . gInsertConstr @n . fmap unM1
 
-instance (If (n == 0) (() :: Constraint) (GInsertConstr (n-1) g), IsBool (n == 0))
-  => GInsertConstr n (f :+: g) where
-  gInsertConstr = _If @(n == 0)
-    (\case
-      Left a -> L1 a
-      Right b -> R1 b)
-    (\case
-      Left a -> R1 (gInsertConstr @(n-1) (Left a))
-      Right (L1 a) -> L1 a
-      Right (R1 b) -> R1 (gInsertConstr @(n-1) (Right b)))
+type ConstrLinearize t l =
+  ( Generic t
+  , Coercible (Rep t) (UnM1 (Rep t))
+  , GLinearize (UnM1 (Rep t))
+  , Coercible (Linearize (UnM1 (Rep t))) l
+  )
 
--- | Generate equality constraints between fields of two matching generic
--- representations.
-class MatchFields (f :: k -> *) (g :: k -> *)
-instance (g' ~ M1 D d g, MatchFields f g) => MatchFields (M1 D c f) g'
--- Forcing the MetaCons field
-instance (g' ~ M1 C ('MetaCons _cn _s _t) g, MatchFields f g)
-  => MatchFields (M1 C c f) g'
-instance (g' ~ M1 S d g, MatchFields f g) => MatchFields (M1 S c f) g'
-instance (g' ~ (g1 :+: g2), MatchFields f1 g1, MatchFields f2 g2)
-  => MatchFields (f1 :+: f2) g'
-instance (g' ~ (g1 :*: g2), MatchFields f1 g1, MatchFields f2 g2)
-  => MatchFields (f1 :*: f2) g'
-instance (g' ~ K1 j a) => MatchFields (K1 i a) g'
-instance (g' ~ U1) => MatchFields U1 g'
-instance (g' ~ V1) => MatchFields V1 g'
+constrLinearize' :: forall t l x. ConstrLinearize t l => t -> l x
+constrLinearize' = coerce (gLinearize @(UnM1 (Rep t)) @x) . from @t @x
+
+instance ConstrLinearize t l => GInsertConstr 0 t f (l :+: f) where
+  gInsertConstr (Left a) = L1 (constrLinearize' a)
+  gInsertConstr (Right b) = R1 b
+
+instance {-# OVERLAPPABLE #-}
+  ( GInsertConstr (n-1) t f g, (n == 0) ~ 'False
+  , f0f ~ (f0 :+: f)
+  ) => GInsertConstr n t f0f (f0 :+: g) where
+  gInsertConstr (Left a) = R1 (gInsertConstr @(n-1) @t @f @g (Left a))
+  gInsertConstr (Right (L1 a)) = L1 a
+  gInsertConstr (Right (R1 b)) = R1 (gInsertConstr @(n-1) @t @f @g (Right b))
+
+-- | Equate two generic representations, but ignoring constructor and field metadata.
+class MatchFields (f :: k -> Type) (g :: k -> Type)
+instance (g ~ M1 D c g', MatchFields f' g') => MatchFields (M1 D c f') g
+instance (g ~ M1 C ('MetaCons _x _y _z) g', MatchFields f' g') => MatchFields (M1 C c f') g
+instance (g ~ M1 S ('MetaSel _w _x _y _z) g', MatchFields f' g') => MatchFields (M1 S c f') g
+instance (g ~ (g1 :+: g2), MatchFields f1 g1, MatchFields f2 g2) => MatchFields (f1 :+: f2) g
+instance (g ~ (g1 :*: g2), MatchFields f1 g1, MatchFields f2 g2) => MatchFields (f1 :*: f2) g
+instance (g ~ K1 i a) => MatchFields (K1 i a) g
+instance (g ~ U1) => MatchFields U1 g
+instance (g ~ V1) => MatchFields V1 g
 
 class IsTuple (n :: Nat) (t :: k)
 instance (t ~ ())                    => IsTuple 0 t
diff --git a/test/surgery.hs b/test/surgery.hs
--- a/test/surgery.hs
+++ b/test/surgery.hs
@@ -11,9 +11,11 @@
 -- Many of these tests are more about ensuring things typecheck than really
 -- comparing their runtime results.
 
+#if __GLASGOW_HASKELL__ >= 802
 import Data.Bifunctor (second)
-import Data.Functor.Identity
-import GHC.Generics
+#endif
+import Data.Functor.Identity (Identity(..))
+import GHC.Generics hiding (R)
 import Test.Tasty
 import Test.Tasty.HUnit
 
@@ -61,14 +63,14 @@
       rt (S 1 2 3) (fromORLazy . insertRField @"u'" . removeRField @"u'" . toORLazy)
   , testCase "SField-ins-rmv" $
       rt ((), S 1 2 3) (fmap fromORLazy . removeRField @"t" . insertRField @"t" @1 . fmap toORLazy)
--- Type error on 8.0
-#if __GLASGOW_HASKELL__ >= 802
+-- Type error on 8.2 and 8.4
+#if __GLASGOW_HASKELL__ <= 800 || __GLASGOW_HASKELL >= 806
   , testCase "Constr-rmv-ins" $
       rt A (fromOR . insertConstrT @"A" . removeConstrT @"A" . toOR)
-#endif
   , testCase "Constr-ins-rmv" $
       rt (Right A)
          (fmap fromOR . removeConstrT @"Z" . insertConstrT @"Z" @0 @() . fmap toOR)
+#endif
   ]
 
 testConsumer :: TestTree
@@ -104,10 +106,13 @@
       "[Right A,Left (Identity 0),Right (C 1 2 3 4 5)]" @?=
       (show . fmap (second (unit . fromOR') . removeConstrT @"B" . toOR))
         [A, B 0, C 1 2 3 4 5]
+#endif
 
   , testCase "insertConstr" $
       "B 0" @?= (show . fromOR @T . insertConstrT @"B" . Left) (Identity 0)
-#endif
+
+  , testCase "insertConstr (record)" $
+      "R {u = 0, v = 0, w = 0}" @?= (show . fromOR @R . insertConstr @"R" . Left) (0, 0, 0)
   ]
 
 testProducer :: TestTree
diff --git a/test/synthetic.hs b/test/synthetic.hs
new file mode 100644
--- /dev/null
+++ b/test/synthetic.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE
+    CPP,
+    DataKinds,
+    DeriveGeneric,
+    FlexibleContexts,
+    GeneralizedNewtypeDeriving,
+    KindSignatures,
+    PolyKinds,
+    ScopedTypeVariables,
+    StandaloneDeriving,
+    TypeApplications,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances
+  #-}
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE DerivingStrategies #-}
+#endif
+
+#if 806 > __GLASGOW_HASKELL__
+import Data.Coerce (Coercible, coerce)
+#endif
+import Data.Functor.Contravariant (Contravariant)
+import Data.Functor.Identity (Identity(..))
+import Data.Bifunctor (first, second, bimap)
+import GHC.Generics (Generic(..))
+import qualified GHC.Generics  -- Make constructors visible to Coercible
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Generic.Data (GShow1)
+import Generic.Data.Surgery
+
+data RowId = RowId
+  deriving Show
+
+type InsertId = (InsertField 0 ('Just "pk") RowId :: MajorSurgery k)
+
+newtype WithId a =
+  WithId (Data (Operate (Rep a) InsertId) ())
+
+deriving instance GShow1 (Operate (Rep a) InsertId) => Show (WithId a)
+
+#if __GLASGOW_HASKELL__ >= 806
+deriving newtype instance
+  ( Generic a
+  , Functor (Operate (Rep a) InsertId)
+  , Contravariant (Operate (Rep a) InsertId)
+  ) => Generic (WithId a)
+#else
+-- Without DerivingStrategies, we do newtype deriving of Generic by hand.
+instance
+  ( Generic a
+  , Functor (Operate (Rep a) InsertId)
+  , Contravariant (Operate (Rep a) InsertId)
+  ) => Generic (WithId a) where
+  type Rep (WithId a) = Operate (Rep a) InsertId
+  to = to'
+  from = from'
+
+to' :: forall a x.
+  (Coercible a (Data (Rep a) ()), Functor (Rep a), Contravariant (Rep a)) =>
+  Rep a x -> a
+to' = coerce (to @(Data (Rep a) ()) @x)
+
+from' :: forall a x.
+  (Coercible a (Data (Rep a) ()), Functor (Rep a), Contravariant (Rep a)) =>
+  a -> Rep a x
+from' = coerce (from @(Data (Rep a) ()) @x)
+#endif
+
+addKey ::
+  ( Generic a
+  , Perform (Rep a) InsertId
+  ) => RowId -> a -> WithId a
+addKey i = WithId . fromOR' . insertRField' @"pk" @0 @RowId i . toOR
+
+data Woof = Waf { fluff :: Int }
+  deriving Generic
+
+type SemiFluff = RemoveRField "fluff" Int
+
+type Fluffy = (SemiFluff :>> InsertField 0 ('Just "fluffy") Bool :: MajorSurgery k)
+
+unfluff :: (Generic a, Perform (Rep a) SemiFluff)
+  => a -> (Int, Data (Operate (Rep a) SemiFluff) ())
+unfluff = fmap fromOR' . removeRField @"fluff" . toOR
+
+fluffier :: (Generic a, Perform (Rep a) Fluffy) => a -> Data (Operate (Rep a) Fluffy) ()
+fluffier = fromOR' . insertRField @"fluffy" @0 . first (>= 0) . removeRField @"fluff" . toOR
+
+data Meow = Miaou Int
+  deriving Generic
+
+type UnMiaou = (RemoveConstr "Miaou" (Identity Int) :: MajorSurgery k)
+type Paw = InsertConstrAt "Paw" 1 (Bool, Bool)
+
+unMiaou :: (Generic a, Perform (Rep a) UnMiaou)
+  => a -> Either Int (Data (Operate (Rep a) UnMiaou) ())
+unMiaou = bimap runIdentity fromOR' . removeConstrT @"Miaou" . toOR
+
+purr :: (Generic a, Perform (Rep a) Paw) =>
+  Either (Bool, Bool) a -> Data (Operate (Rep a) Paw) ()
+purr = fromOR' . insertConstrT @"Paw" @1 . second toOR
+
+type Aww = (Paw :>> UnMiaou :: MajorSurgery k)
+
+{-
+pat :: forall a. (Generic a, Perform (Rep a) Aww) =>
+  Either (Bool, Bool) a -> Either (Identity Int) (Data (Operate (Rep a) Aww) ())
+pat = second fromOR' . removeConstrT @"Miaou" . insertConstrT @"Paw" @1 @(Bool, Bool) . second toOR
+-}
+
+main :: IO ()
+main = defaultMain test
+
+test :: TestTree
+test = testGroup "synthetic"
+  [ testCase "addKey" $ "WithId (Waf {pk = RowId, fluff = 77})" @?= show (addKey RowId (Waf 77))
+  , testCase "unfluff" $ "(33,Waf {})" @?= show (unfluff (Waf 33))
+  , testCase "fluffier" $ "Waf {fluffy = True}" @?= show (fluffier (Waf 33))
+  , testCase "unMiaou" $ "Left 3" @?= show (unMiaou (Miaou 3))
+  , testCase "purr" $ "Miaou 3" @?= show (purr (Right (Miaou 3)))
+  ]