diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,13 @@
+# 0.10.0
+
+- Changed the types of `Data.Vinyl.CoRec.onCoRec` and `Data.Vinyl.CoRec.onField`. This was pushing through the changes to drop the use of `Proxy` arguments, relying instead on `TypeApplications`. Also added `onCoRec1` and `onField` to work with functions relying on a single type class.
+
+- Faster `asA` and `asA'`. These implementations utilize `unsafeCoerce` in their implementations after we have performed a runtime check that proves (to us) that the types match up. The old implementations are still available as `asASafe` and `asA'Safe`. While both implementations can run in constant time if the compiler optimizes everything successfully, the faster variants are a bit more than 3x faster in a trivial benchmark.
+
+- Add a `Generic` instance for `Rec` and common functors.
+
+- Add a variety of `ToJSON` implementations as a test case. One or all of these should probably exist as a separate package to avoid `vinyl` depending on `aeson`, but their content may be of interest.
+
 # 0.9.2
 
 - Add `runcurryX` for applying an uncurried function to a `Rec` passing through the `XRec` machinery to strip out syntactic noise.
diff --git a/Data/Vinyl/Class/Method.hs b/Data/Vinyl/Class/Method.hs
--- a/Data/Vinyl/Class/Method.hs
+++ b/Data/Vinyl/Class/Method.hs
@@ -29,6 +29,7 @@
     RecMapMethod(..)
   , rmapMethodF
   , mapFields
+  , RecMapMethod1(..)
   , RecPointed(..)
     -- * Support for 'RecMapMethod'
   , FieldTyper, ApplyFieldTyper, PayloadType
@@ -169,19 +170,36 @@
   rpointMethod f = f :& rpointMethod @c f
   {-# INLINE rpointMethod #-}
 
--- | Apply a typeclass method to each field of a 'Rec'.
+-- | Apply a typeclass method to each field of a 'Rec' where the class
+-- constrains the index of the field, but not its interpretation
+-- functor.
 class RecMapMethod c (f :: u -> *) (ts :: [u]) where
   rmapMethod :: (forall a. c (PayloadType f a) => f a -> g a)
              -> Rec f ts -> Rec g ts
 
+-- | Apply a typeclass method to each field of a 'Rec' where the class
+-- constrains the field when considered as a value interpreted by the
+-- record's interpretation functor.
+class RecMapMethod1 c (f :: u -> *) (ts :: [u])where
+  rmapMethod1 :: (forall a. c (f a) => f a -> g a)
+              -> Rec f ts -> Rec g ts
+
 instance RecMapMethod c f '[] where
   rmapMethod _ RNil = RNil
   {-# INLINE rmapMethod #-}
 
+instance RecMapMethod1 c f '[] where
+  rmapMethod1 _ RNil = RNil
+  {-# INLINE rmapMethod1 #-}
+
 instance (c (PayloadType f t), RecMapMethod c f ts)
   => RecMapMethod c f (t ': ts) where
   rmapMethod f (x :& xs) = f x :& rmapMethod @c f xs
   {-# INLINE rmapMethod #-}
+
+instance (c (f t), RecMapMethod1 c f ts) => RecMapMethod1 c f (t ': ts) where
+  rmapMethod1 f (x :& xs) = f x :& rmapMethod1 @c f xs
+  {-# INLINE rmapMethod1 #-}
 
 -- | Apply a typeclass method to each field of a @Rec f ts@ using the
 -- 'Functor' instance for @f@ to lift the function into the
diff --git a/Data/Vinyl/CoRec.hs b/Data/Vinyl/CoRec.hs
--- a/Data/Vinyl/CoRec.hs
+++ b/Data/Vinyl/CoRec.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE BangPatterns, CPP, ConstraintKinds, DataKinds, EmptyCase,
-             FlexibleContexts, FlexibleInstances, GADTs,
-             KindSignatures, MultiParamTypeClasses, PolyKinds,
-             RankNTypes, ScopedTypeVariables, TypeOperators,
+{-# LANGUAGE AllowAmbiguousTypes, BangPatterns, CPP, ConstraintKinds,
+             DataKinds, EmptyCase, FlexibleContexts,
+             FlexibleInstances, GADTs, KindSignatures,
+             MultiParamTypeClasses, PolyKinds, RankNTypes,
+             ScopedTypeVariables, TypeApplications, TypeOperators,
              UndecidableInstances #-}
 -- | Co-records: open sum types.
 --
@@ -13,15 +13,11 @@
 -- @C@. The type @CoRec '[A,B,C]@ corresponds to this sum type.
 module Data.Vinyl.CoRec where
 import Data.Maybe(fromJust)
-import Data.Proxy
-import Data.Vinyl
+import Data.Vinyl.Core
+import Data.Vinyl.Lens (RElem, rget, rput, type (∈))
 import Data.Vinyl.Functor (Compose(..), (:.), Identity(..), Const(..))
 import Data.Vinyl.TypeLevel
-#if __GLASGOW_HASKELL__ < 800
-import GHC.Prim (Constraint)
-#else
-import Data.Kind (Constraint)
-#endif
+import Unsafe.Coerce (unsafeCoerce)
 
 -- | Generalize algebraic sum types.
 data CoRec :: (k -> *) -> [k] -> * where
@@ -41,10 +37,7 @@
 
 instance forall ts. (RPureConstrained Show ts, RecApplicative ts)
   => Show (CoRec Identity ts) where
-  show (CoRec (Identity x)) = "(Col "++show' x++")"
-    where shower :: Rec (Op String) ts
-          shower = rpureConstrained @Show (Op show)
-          show' = runOp (rget shower)
+  show x = "(Col " ++ onField @Show show x++")"
 
 instance forall ts. (RecApplicative ts, RecordToList ts,
                      RZipWith ts, ReifyConstraint Eq Maybe ts, RMap ts)
@@ -84,6 +77,25 @@
 coRecMap :: (forall x. f x -> g x) -> CoRec f ts -> CoRec g ts
 coRecMap nt (CoRec x) = CoRec (nt x)
 
+-- | Capture a type class instance dictionary
+data DictOnly c a where
+  DictOnly :: c a => DictOnly c a
+
+-- | Get a 'DictOnly' from an 'RPureConstrained' instance.
+getDict :: forall c ts a proxy. (a ∈ ts, RPureConstrained c ts)
+        => proxy a -> DictOnly c a
+getDict _ = rget @a (rpureConstrained @c @ts DictOnly)
+
+-- | Like 'coRecMap', but the function mapped over the 'CoRec' can
+-- have a constraint.
+coRecMapC :: forall c ts f g.
+             (RPureConstrained c ts)
+          => (forall x. (x ∈ ts, c x) => f x -> g x)
+          -> CoRec f ts
+          -> CoRec g ts
+coRecMapC nt (CoRec x) = case getDict @c @ts x of
+                           DictOnly -> CoRec (nt x)
+
 -- | This can be used to pull effects out of a 'CoRec'.
 coRecTraverse :: Functor h
               => (forall x. f x -> h (g x)) -> CoRec f ts -> h (CoRec g ts)
@@ -120,50 +132,53 @@
         aux _ c@(CoRec (Compose (Just _))) = c
         aux c _ = c
 
--- | Apply a type class method on a 'CoRec'. The first argument is a
--- 'Proxy' value for a /list/ of 'Constraint' constructors. For
--- example, @onCoRec [pr|Num,Ord|] (> 20) r@. If only one constraint
--- is needed, use the @pr1@ quasiquoter.
-onCoRec :: forall (cs :: [* -> Constraint]) f ts b.
-           (AllAllSat cs ts, Functor f, RecApplicative ts)
-        => Proxy cs
-        -> (forall a. AllSatisfied cs a => a -> b)
-        -> CoRec f ts -> f b
-onCoRec p f (CoRec x) = fmap meth x
-  where meth = runOp $ rget (reifyDicts p (Op f) :: Rec (Op b) ts)
+-- | Apply methods from a type class to a 'CoRec'. Intended for use
+-- with @TypeApplications@, e.g. @onCoRec \@Show show r@
+onCoRec :: forall c f ts b g. (RPureConstrained c ts)
+        => (forall a. (a ∈ ts, c a) => f a -> g b)
+        -> CoRec f ts -> g b
+onCoRec f (CoRec x) = case getDict @c @ts x of
+                        DictOnly -> f x
+{-# INLINE onCoRec #-}
 
--- | Apply a type class method on a 'Field'. The first argument is a
--- 'Proxy' value for a /list/ of 'Constraint' constructors. For
--- example, @onCoRec [pr|Num,Ord|] (> 20) r@. If only one constraint
--- is needed, use the @pr1@ quasiquoter.
-onField :: forall cs ts b.
-           (AllAllSat cs ts, RecApplicative ts)
-        => Proxy cs
-        -> (forall a. AllSatisfied cs a => a -> b)
+-- | Apply a type class method to a 'Field'. Intended for use with
+-- @TypeApplications@, e.g. @onField \@Show show r@.
+onField :: forall c ts b. (RPureConstrained c ts)
+        => (forall a. (a ∈ ts, c a) => a -> b)
         -> Field ts -> b
-onField p f x = getIdentity (onCoRec p f x)
-
--- | Build a record whose elements are derived solely from a
--- list of constraint constructors satisfied by each.
-reifyDicts :: forall cs f proxy (ts :: [*]). (AllAllSat cs ts, RecApplicative ts)
-           => proxy cs -> (forall a. AllSatisfied cs a => f a) -> Rec f ts
-reifyDicts _ f = go (rpure Nothing)
-  where go :: AllAllSat cs ts' => Rec Maybe ts' -> Rec f ts'
-        go RNil = RNil
-        go (_ :& xs) = f :& go xs
+onField f x = getIdentity (onCoRec @c (fmap f) x)
+{-# INLINE onField #-}
 
 -- * Extracting values from a CoRec/Pattern matching on a CoRec
 
+-- | Compute a runtime 'Int' index identifying the position of the
+-- variant held by a @CoRec f ts@ in the type-level list @ts@.
+variantIndexOf :: forall f ts. CoRec f ts -> Int
+variantIndexOf (CoRec x) = aux x
+  where aux :: forall a. NatToInt (RIndex a ts) => f a -> Int
+        aux _ = natToInt @(RIndex a ts)
+{-# INLINE variantIndexOf #-}
+
+-- [NOTE: asA] We want to say that if @NatToInt (RIndex a ts) ~
+-- NatToInt (RIndex b ts)@ then @a ~ b@ by relying on an injectivity
+-- property of 'RIndex'. However, we are checking the variant index of
+-- the argument at runtime, so we do not statically know that
+-- extracting the variant at a particular type is safe at compile
+-- time.
+
 -- | If a 'CoRec' is a variant of the requested type, return 'Just'
 -- that value; otherwise return 'Nothing'.
-asA             :: (t ∈ ts, RecApplicative ts, RMap ts)
-                => CoRec Identity ts -> Maybe t
-asA c@(CoRec _) = rget $ coRecToRec' c
+asA :: NatToInt (RIndex t ts) => CoRec Identity ts -> Maybe t
+asA = fmap getIdentity . asA'
+{-# INLINE asA #-}
 
 -- | Like 'asA', but for any interpretation functor.
-asA' :: (t ∈ ts, RecApplicative ts, RMap ts)
-     => CoRec f ts -> (Maybe :. f) t
-asA' c@(CoRec _) = rget $ coRecToRec c
+asA' :: forall t ts f. (NatToInt (RIndex t ts))
+     => CoRec f ts -> Maybe (f t)
+asA' f@(CoRec x)
+  | variantIndexOf f == natToInt @(RIndex t ts) = Just (unsafeCoerce x)
+  | otherwise = Nothing
+{-# INLINE asA' #-}
 
 -- | Pattern match on a CoRec by specifying handlers for each case. Note that
 -- the order of the Handlers has to match the type level list (t:ts).
@@ -229,13 +244,33 @@
 -- type, or a 'CoRec' that must be one of the remaining types.
 restrictCoRec :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
               => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
-restrictCoRec = go . coRecToRec
-  where go :: Rec (Maybe :. f) (t ': ts) -> Either (f t) (CoRec f ts)
-        go (Compose Nothing :& xs) = Right (fromJust (firstField xs))
-        go (Compose (Just x) :& _) = Left x
+restrictCoRec r = maybe (Right (unsafeCoerce r)) Left (asA' @t r)
+{-# INLINE restrictCoRec #-}
 
 -- | A 'CoRec' whose possible types are @ts@ may be used at a type of
 -- 'CoRec' whose possible types are @t:ts@.
 weakenCoRec :: (RecApplicative ts, FoldRec (t ': ts) (t ': ts))
             => CoRec f ts -> CoRec f (t ': ts)
 weakenCoRec = fromJust . firstField . (Compose Nothing :&) . coRecToRec
+
+-- * Safe Variants
+
+-- | A 'CoRec' is either the first possible variant indicated by its
+-- type, or a 'CoRec' that must be one of the remaining types. The
+-- safety is related to that of 'asASafe'.
+restrictCoRecSafe :: forall t ts f. (RecApplicative ts, FoldRec ts ts)
+                  => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
+restrictCoRecSafe = go . coRecToRec
+  where go :: Rec (Maybe :. f) (t ': ts) -> Either (f t) (CoRec f ts)
+        go (Compose Nothing :& xs) = Right (fromJust (firstField xs))
+        go (Compose (Just x) :& _) = Left x
+
+-- | Like 'asA', but implemented more safely and typically slower.
+asASafe :: (t ∈ ts, RecApplicative ts, RMap ts)
+        => CoRec Identity ts -> Maybe t
+asASafe c@(CoRec _) = rget $ coRecToRec' c
+
+-- | Like 'asASafe', but for any interpretation functor.
+asA'Safe :: (t ∈ ts, RecApplicative ts, RMap ts)
+         => CoRec f ts -> (Maybe :. f) t
+asA'Safe c@(CoRec _) = rget $ coRecToRec c
diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs
--- a/Data/Vinyl/Core.hs
+++ b/Data/Vinyl/Core.hs
@@ -42,6 +42,7 @@
 import Data.Vinyl.TypeLevel
 import Data.Type.Equality (TestEquality (..), (:~:) (..))
 import Data.Type.Coercion (TestCoercion (..), Coercion (..))
+import GHC.Generics
 
 -- | A record is parameterized by a universe @u@, an interpretation @f@ and a
 -- list of rows @rs@.  The labels or indices of the record are given by
@@ -324,3 +325,30 @@
   {-# INLINE peek #-}
   poke ptr (!x :& xs) = poke (castPtr ptr) x >> poke (ptr `plusPtr` sizeOf (undefined :: f r)) xs
   {-# INLINE poke #-}
+
+instance Generic (Rec f '[]) where
+  type Rep (Rec f '[]) =
+    C1 ('MetaCons "RNil" 'PrefixI 'False)
+       (S1 ('MetaSel 'Nothing
+          'NoSourceUnpackedness
+          'NoSourceStrictness
+          'DecidedLazy) U1)
+  from RNil = M1 (M1 U1)
+  to (M1 (M1 U1)) = RNil
+
+instance (Generic (Rec f rs)) => Generic (Rec f (r ': rs)) where
+  type Rep (Rec f (r ': rs)) =
+    C1 ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False)
+    (S1 ('MetaSel 'Nothing
+         'NoSourceUnpackedness
+         'SourceStrict
+         'DecidedStrict)
+       (Rec0 (f r))
+      :*:
+      S1 ('MetaSel 'Nothing
+           'NoSourceUnpackedness
+           'NoSourceStrictness
+           'DecidedLazy)
+         (Rep (Rec f rs)))
+  from (x :& xs) = M1 (M1 (K1 x) :*: M1 (from xs))
+  to (M1 (M1 (K1 x) :*: M1 xs)) = x :& to xs
diff --git a/Data/Vinyl/Functor.hs b/Data/Vinyl/Functor.hs
--- a/Data/Vinyl/Functor.hs
+++ b/Data/Vinyl/Functor.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE DeriveFoldable             #-}
 {-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DeriveTraversable          #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GADTs                      #-}
@@ -9,6 +10,7 @@
 {-# LANGUAGE PolyKinds                  #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE TypeOperators              #-}
 
 module Data.Vinyl.Functor
@@ -37,6 +39,7 @@
 #endif
 import Foreign.Ptr (castPtr)
 import Foreign.Storable
+import GHC.Generics
 import GHC.TypeLits
 import GHC.Types (Type)
 
@@ -57,6 +60,7 @@
              , Storable
              , Eq
              , Ord
+             , Generic
              )
 
 -- | Used this instead of 'Identity' to make a record
@@ -73,7 +77,7 @@
 
 newtype Compose (f :: l -> *) (g :: k -> l) (x :: k)
   = Compose { getCompose :: f (g x) }
-    deriving (Storable)
+    deriving (Storable, Generic)
 
 type f :. g = Compose f g
 infixr 9 :.
@@ -84,6 +88,7 @@
              , Foldable
              , Traversable
              , Storable
+             , Generic
              )
 
 -- | A value with a phantom 'Symbol' label. It is not a
@@ -94,6 +99,11 @@
 
 deriving instance Eq t => Eq (ElField '(s,t))
 deriving instance Ord t => Ord (ElField '(s,t))
+
+instance KnownSymbol s => Generic (ElField '(s,a)) where
+  type Rep (ElField '(s,a)) = C1 ('MetaCons s 'PrefixI 'False) (Rec0 a)
+  from (Field x) = M1 (K1 x)
+  to (M1 (K1 x)) = Field x
 
 instance (Num t, KnownSymbol s) => Num (ElField '(s,t)) where
   Field x + Field y = Field (x+y)
diff --git a/Data/Vinyl/Lens.hs b/Data/Vinyl/Lens.hs
--- a/Data/Vinyl/Lens.hs
+++ b/Data/Vinyl/Lens.hs
@@ -36,9 +36,10 @@
 -- its value.  The fifth parameter to 'RecElem', @i@, is there to help
 -- the constraint solver realize that this is a decidable predicate
 -- with respect to the judgemental equality in @k@.
-class i ~ RIndex r rs => RecElem record (r :: k) (r' :: k)
-                                        (rs :: [k]) (rs' :: [k])
-                                        (i :: Nat) | r r' rs i -> rs' where
+class (i ~ RIndex r rs, NatToInt i)
+  => RecElem record (r :: k) (r' :: k)
+             (rs :: [k]) (rs' :: [k])
+             (i :: Nat) | r r' rs i -> rs' where
   -- | An opportunity for instances to generate constraints based on
   -- the functor parameter of records passed to class methods.
   type RecElemFCtx record (f :: k -> *) :: Constraint
diff --git a/Data/Vinyl/SRec.hs b/Data/Vinyl/SRec.hs
--- a/Data/Vinyl/SRec.hs
+++ b/Data/Vinyl/SRec.hs
@@ -63,7 +63,7 @@
 import Data.Vinyl.Core
 import Data.Vinyl.Functor (Lift(..), Compose(..), type (:.), ElField)
 import Data.Vinyl.Lens (RecElem(..), RecSubset(..), type (⊆), RecElemFCtx)
-import Data.Vinyl.TypeLevel (RImage, RIndex, Nat(..), RecAll, AllConstrained)
+import Data.Vinyl.TypeLevel (NatToInt, RImage, RIndex, Nat(..), RecAll, AllConstrained)
 import Foreign.Marshal.Utils (copyBytes)
 import Foreign.Ptr (Ptr)
 import Foreign.Storable (Storable(..))
@@ -261,6 +261,7 @@
 -- | Field accessors for 'SRec2' specialized to 'ElField' as the
 -- functor.
 instance ( i ~ RIndex t ts
+         , NatToInt i
          , FieldOffset ElField ts t
          , Storable (Rec ElField ts)
          , AllConstrained (FieldOffset ElField ts) ts)
@@ -281,6 +282,7 @@
 coerceSRec2to1 = coerce
 
 instance ( i ~ RIndex (t :: (Symbol,*)) (ts :: [(Symbol,*)])
+         , NatToInt i
          , FieldOffset ElField ts t
          , Storable (Rec ElField ts)
          , AllConstrained (FieldOffset ElField ts) ts)
diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs
--- a/Data/Vinyl/TypeLevel.hs
+++ b/Data/Vinyl/TypeLevel.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE AllowAmbiguousTypes   #-}
-
 {-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -88,9 +87,9 @@
 
 -- | Constraint that each Constraint in a type-level list is satisfied
 -- by a particular type.
-type family AllSatisfied cs t :: Constraint where
-  AllSatisfied '[] t = ()
-  AllSatisfied (c ': cs) t = (c t, AllSatisfied cs t)
+class AllSatisfied cs t where
+instance AllSatisfied '[] t where
+instance (c t, AllSatisfied cs t) => AllSatisfied (c ': cs) t where
 
 -- | Constraint that all types in a type-level list satisfy each
 -- constraint from a list of constraints.
diff --git a/Data/Vinyl/XRec.hs b/Data/Vinyl/XRec.hs
--- a/Data/Vinyl/XRec.hs
+++ b/Data/Vinyl/XRec.hs
@@ -168,6 +168,7 @@
 instance IsoHKD Maybe a where
 instance IsoHKD First a where
 instance IsoHKD Last a where
+instance IsoHKD ((,) a) b where
 
 -- | Work with values of type 'Sum' @a@ as if they were of type @a@.
 instance IsoHKD Sum a where
diff --git a/benchmarks/AsABench.hs b/benchmarks/AsABench.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/AsABench.hs
@@ -0,0 +1,14 @@
+{-# language DataKinds, TypeOperators, TypeApplications #-}
+import Data.Vinyl.CoRec
+import Data.Vinyl.Functor (Identity(..))
+import Criterion.Main
+
+main :: IO ()
+main = let x1 :: CoRec Identity '[Int,Bool,Char,Double,(),Float]
+           x1 = CoRec (Identity (23::Int))
+           x5 :: CoRec Identity '[Bool,Char,Double,(),Int,Float]
+           x5 = CoRec (Identity (23::Int))
+       in defaultMain [ bench "asASafe1" $ whnf (asASafe @Int) x1
+                      , bench "asA1" $ whnf (asA @Int) x1
+                      , bench "asASafe5" $ whnf (asASafe @Int) x5
+                      , bench "asA5" $ whnf (asA @Int) x5 ]
diff --git a/tests/Aeson.hs b/tests/Aeson.hs
new file mode 100644
--- /dev/null
+++ b/tests/Aeson.hs
@@ -0,0 +1,237 @@
+{-# LANGUAGE CPP, DataKinds, DeriveGeneric, FlexibleContexts,
+             FlexibleInstances, GADTs, OverloadedStrings, PolyKinds,
+             ScopedTypeVariables, TypeApplications, TypeOperators,
+             ViewPatterns #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Demonstrate encoding a 'Rec' to JSON. Three approaches are shown:
+-- the first utilizes 'ToJSON' instances for the record's
+-- interpretation type constructor applied to each of its fields. This
+-- has the advantage of being concise by virtue of re-using a lot of
+-- existing pieces. The downside to relying on existing 'ToJSON'
+-- instances is that they encode self-contained JSON values, when what
+-- we want to do is construct a single JSON object encompassing each
+-- record field as a named field of that JSON object. We can do this
+-- by inspecting the JSON serialization of each field, and extracting
+-- it as a key-value pair if it was serialized as a JSON object with a
+-- single named field. This works, but means that the types do not
+-- guarantee correctness (i.e. if a record field is serialized as a
+-- 'Number', we won't be able to include it in the serialization of
+-- the 'Rec').
+--
+-- The second approach uses a bit of @aeson@ internals to instead
+-- serialize each 'Rec' field as a key-value pair with no additional
+-- decoration. This should be faster as well as more tightly typed
+-- since we do not need to undo any 'Value' wrapping of the individual
+-- record fields.
+--
+-- The third approach uses aeson's built-in functions for working with
+-- 'Generic'. This requires some post-processing to address precisely
+-- the above problem: the function based on 'Generic' ends up
+-- producing a self-contained 'Value' for each field of the
+-- record. Specifically, each field becomes an 'Array' that is either
+-- empty or contains an 'Object' with a single field as well as
+-- another, nested, 'Array' for the rest of the record. We include
+-- here a function to flatten that recursive structure into the
+-- 'Object' shape we want.
+import Control.Lens (view, deep)
+import Control.Monad.State.Strict
+import qualified Data.HashMap.Strict as H
+#if __GLASGOW_HASKELL__ < 804
+import Data.Semigroup ((<>))
+#endif
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Vector as V
+import Data.Vinyl
+import Data.Vinyl.Class.Method (RecMapMethod1(..))
+import Data.Vinyl.Functor (Compose(..), (:.), Identity(..), Const(..))
+import Data.Aeson
+import Data.Aeson.Encoding.Internal (wrapObject, pair)
+import Data.Aeson.Lens (_Object)
+import GHC.Generics (Generic, Rep)
+import GHC.TypeLits (KnownSymbol)
+import Test.Hspec
+
+-- * Implementing 'ToJSON' for 'Rec'
+
+-- | An 'Identity' functor is not reflected in a value's JSON
+-- serialization.
+instance ToJSON a => ToJSON (Identity a) where
+  toJSON (Identity x) = toJSON x
+
+-- | A named field serializes to a JSON object with a single named
+-- field.
+instance ToJSON a => ToJSON (ElField '(s,a)) where
+  toJSON x = object [(T.pack (getLabel x), toJSON (getField x))]
+
+-- | A @((Text,) :. f) a@ value maps to a JSON field whose name is the
+-- 'Text' value, and whose value has type @f a@.
+instance ToJSON (f a) => ToJSON ((((,) Text) :. f) a) where
+  toJSON (Compose (name, x)) = object [(name, toJSON x)]
+
+-- | Replace each field of a record with the result of serializing it
+-- to a JSON 'Value', and then extracting that 'Value''s single named
+-- field. If the serialization is not in the form of an object with a
+-- single field, the conversion fails with a 'Nothing'.
+fieldsToJSON :: (RecMapMethod1 ToJSON f rs)
+             => Rec f rs -> Rec (Maybe :. Const (Text,Value)) rs
+fieldsToJSON = rmapMethod1 @ToJSON (Compose . aux)
+  where aux x = case toJSON x of
+                  Object (H.toList -> [field]) -> Just (Const field)
+                  _ -> Nothing
+
+-- | Convert a homogeneous record to a list factored through an outer
+-- functor. A useful specialization is when the outer functor is
+-- 'Maybe': if any field is 'Nothing', then the result of this
+-- function is 'Nothing'.
+recToListF :: (Applicative f, RFoldMap rs) => Rec (f :. Const a) rs -> f [a]
+recToListF = fmap (rfoldMap (pure . getConst)) . rtraverse getCompose
+
+instance (RFoldMap rs, RecMapMethod1 ToJSON f rs)
+  => ToJSON (Rec f rs) where
+  toJSON = maybe err object . recToListF . fieldsToJSON
+    where err = error (unlines [ "The interpretation functor of this "
+                               , "record did not produce a named field "
+                               , "for at least one of its fields." ])
+
+-- * Naming anonymous fields
+
+-- | Pair each record field with its position.
+recIndexed :: Rec f rs -> Rec ((,) Int :. f) rs
+recIndexed = flip evalState 1 . rtraverse aux
+  where aux x = do i <- get
+                   Compose (i,x) <$ put (i+1)
+
+-- | A helper to pair each field of a record with a name derived from
+-- its position in the record. This reflects the implicit ordering of
+-- the type-level list of the record's fields.
+nameFields :: RMap rs => Rec f rs -> Rec ((,) Text :. f) rs
+nameFields = rmap aux . recIndexed
+  where aux (Compose (i,x)) = Compose ("field"<>T.pack (show i), x)
+
+-- * Test Cases
+
+r1 :: Rec ElField '[("age" ::: Int), ("iscool" ::: Bool), ("yearbook" ::: Text)]
+r1 = xrec (23, True, "You spin me right round")
+
+r1JSON :: Value
+r1JSON = object [ "age" .= (23 :: Int)
+                , "iscool" .= True
+                , "yearbook" .= ("You spin me right round" :: Text) ]
+
+r2 :: Rec Identity '[Int,Bool,Text]
+r2 = xrec (23, True, "You spin me right round")
+
+r2JSON :: Value
+r2JSON = object [ "field1" .= (23 :: Int)
+                , "field2" .= True
+                , "field3" .= ("You spin me right round" :: Text) ]
+
+-- | A type with its own JSON Object encoding
+data MyType = MyType { bike :: Bool, skateboard :: Bool } deriving Generic
+instance ToJSON MyType
+
+r3 :: Rec ElField '[ "age" ::: Int
+                   , "iscool" ::: Bool
+                   , "yearbook" ::: Text
+                   , "hobbies" ::: MyType ]
+r3 = xrec (23, True, "You spin me right round", MyType True True)
+
+r3JSON :: Value
+r3JSON = object [ "age" .= (23 :: Int)
+                , "iscool" .= True
+                , "yearbook" .= ("You spin me right round" :: Text)
+                , "hobbies" .= object ["bike" .= True, "skateboard" .= True] ]
+
+main :: IO ()
+main = hspec $ do
+  describe "Simple Rec to JSON" $ do
+    it "Named fields" $
+      toJSON r1 `shouldBe` r1JSON
+    it "Anonymous fields" $
+      toJSON (nameFields r2) `shouldBe` r2JSON
+    it "Nested objects" $
+      toJSON r3 `shouldBe` r3JSON
+  describe "Type-safe Rec to JSON" $ do
+    it "Named fields" $
+      recToJSON r1 `shouldBe` r1JSON
+    it "Anonymous fields" $
+      recToJSON (nameFields r2) `shouldBe` r2JSON
+    it "Nested objects" $
+      recToJSON r3 `shouldBe` r3JSON
+  describe "Via Generics" $ do
+    it "Named fields" $
+      grecToJSON r1 `shouldBe` r1JSON
+    it "Anonymous fields" $
+      grecToJSON (nameFields r2) `shouldBe` r2JSON
+    it "Nested objects" $
+      grecToJSON r3 `shouldBe` r3JSON
+
+-- * More type safe and efficient
+
+-- | Produce a JSON key-value pair from a Haskell value. This is what
+-- we want from each field of our records. The simple encoding above
+-- that treats each record field as a self-contained JSON 'Value'
+-- loses precision in the type.
+class ToJSONField a where
+  encodeJSONField :: a -> Series
+  toJSONField :: a -> (Text,Value)
+
+-- | An @ElField '(s,a)@ value maps to a JSON field with name @s@ and
+-- value @a@.
+instance (ToJSON a, KnownSymbol s) => ToJSONField (ElField '(s,a)) where
+  encodeJSONField x = pair (T.pack (getLabel x)) (toEncoding (getField x))
+  toJSONField x = (T.pack (getLabel x), toJSON (getField x))
+
+-- | A @((Text,) :. f) a@ value maps to a JSON field whose name is the
+-- 'Text' value, and whose value has type @f a@.
+instance ToJSON (f a) => ToJSONField (((,) Text :. f) a) where
+  encodeJSONField (Compose (name,val)) = pair name (toEncoding val)
+  toJSONField (Compose (name,val)) = (name, toJSON val)
+
+encodeRec :: (RFoldMap rs, RecMapMethod1 ToJSONField f rs)
+          => Rec f rs -> Encoding
+encodeRec = wrapObject
+          . pairs
+          . rfoldMap getConst
+          . rmapMethod1 @ToJSONField (Const . encodeJSONField)
+
+recToJSON :: (RFoldMap rs, RecMapMethod1 ToJSONField f rs)
+          => Rec f rs -> Value
+recToJSON = object
+          . rfoldMap ((:[]) . getConst)
+          . rmapMethod1 @ToJSONField (Const . toJSONField)
+
+-- * Generically
+
+-- | If a 'Value' is a nested 'Array' of 'Object's, extract the
+-- collection of key-value pairs from the entire recursive structure.
+allAesonFields :: Value -> Maybe (H.HashMap Text Value)
+allAesonFields (Array arr) =
+  case V.toList arr of
+    [] -> Just mempty
+    [Object field, objTail] -> fmap (field <>) (allAesonFields objTail)
+    _ -> Nothing
+allAesonFields _ = Nothing
+
+-- | Try un-nesting a recursive 'Array' of fields. That is, if a
+-- 'Value' is laid out as @Array [Object [(key1,value1)], Array
+-- [Object [(key2, value2)], ...]]@ we extract all the key-value
+-- pairs, @[(key1,value1), (key2, value2), ...]@.
+unnestFields :: Value -> Value
+unnestFields v = maybe v Object (allAesonFields v)
+
+-- | A lens implementation of something a bit looser than
+-- 'unnestFields'.
+allFields :: Value -> H.HashMap Text Value
+allFields = view (deep _Object)
+
+-- | The generic 'ToJSON' instance is not quite right since we use the
+-- record's interpretation type constructor to define serialization,
+-- resulting in each record field being treated as a self-contained
+-- JSON object. What we want is for each record field to become a
+-- named field of a single JSON object, so we must post-process the
+-- result of the function defined on 'Generic'.
+grecToJSON :: (Generic (Rec f rs), GToJSON Zero (Rep (Rec f rs)))
+           => Rec f rs -> Value
+grecToJSON = Object . allFields . genericToJSON defaultOptions
diff --git a/vinyl.cabal b/vinyl.cabal
--- a/vinyl.cabal
+++ b/vinyl.cabal
@@ -1,5 +1,5 @@
 name:                vinyl
-version:             0.9.3
+version:             0.10.0
 synopsis:            Extensible Records
 -- description:
 license:             MIT
@@ -77,12 +77,28 @@
   ghc-options:      -O2
   default-language: Haskell2010
 
+benchmark asa
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   benchmarks
+  main-is:          AsABench.hs
+  build-depends:    base >= 4.7 && <= 5, criterion, vinyl
+  ghc-options:      -O2
+  default-language: Haskell2010
+
 test-suite doctests
   type:             exitcode-stdio-1.0
   hs-source-dirs:   tests
   other-modules:    Intro
   main-is:          doctests.hs
   build-depends:    base >= 4.7 && <= 5, lens, doctest >= 0.8, singletons >= 0.10, vinyl
+  default-language: Haskell2010
+
+test-suite aeson
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   tests
+  main-is:          Aeson.hs
+  build-depends:    base >= 4.7 && <= 5, hspec, aeson, text, mtl, vinyl,
+                    vector, unordered-containers, lens, lens-aeson
   default-language: Haskell2010
 
 test-suite spec