diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,39 @@
+# 0.14.3
+- Compatibility with `lens-aeson` > 1.2
+
+# 0.14.2
+- Export the `ToARec` class
+
+# 0.14.1
+- Compatibility with `aeson` > 2.0
+
+# 0.14.0
+- `ARec` efficiency improvements (@Philonous)
+- Make `ElField` a newtype (@Philonous)
+
+The `ElField` change brings more opportunities for the optimizer, but can result in longer compile times.
+
+# 0.13.3
+- Fixed CHANGELOG entry for 0.13.2: it referred to version 0.14.0
+- Relax bounds on `hspec`
+
+# 0.13.2
+- Removed aput and alens from Data.Vinyl.ARec. They were used internally, but their type is unsound.
+
+# 0.13.1
+- GHC 9.0.1 support
+
+# 0.13.0
+- GHC 8.10.1 support fix. A fix for the previous attempt at 8.10 support involves a backwards incompatible change.
+
+# 0.12.2
+
+- GHC 8.10.1 support
+
+# 0.12.0
+
+- GHC 8.8.1 support. Class type signatures were changed to remove explicit kind variables. This is to simplify the use of `TypeApplications` which changed with GHC 8.8.1 to require explicit application to those kind variables. Leaving them out of the class definitions preserves existing usage of `TypeApplications`. Thanks to Justin Le (@mstksg).
+
 # 0.11.0
 
 - Changed the `Show` instance of `CoRec`
diff --git a/Data/Vinyl/ARec.hs b/Data/Vinyl/ARec.hs
--- a/Data/Vinyl/ARec.hs
+++ b/Data/Vinyl/ARec.hs
@@ -1,133 +1,20 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE Trustworthy #-}
+
 -- | Constant-time field accessors for extensible records. The
 -- trade-off is the usual lists vs arrays one: it is fast to add an
 -- element to the head of a list, but element access is linear time;
 -- array access time is uniform, but extending the array is more
 -- slower.
-module Data.Vinyl.ARec where
-import Data.Vinyl.Core
-import Data.Vinyl.Lens (RecElem(..), RecSubset(..))
-import Data.Vinyl.TypeLevel
-
-import qualified Data.Array as Array
-import qualified Data.Array.Base as BArray
-import GHC.Exts (Any)
-import Unsafe.Coerce
-
--- | An array-backed extensible record with constant-time field
--- access.
-newtype ARec (f :: k -> *) (ts :: [k]) = ARec (Array.Array Int Any)
-
--- | Convert a 'Rec' into an 'ARec' for constant-time field access.
-toARec :: forall f ts. (NatToInt (RLength ts)) => Rec f ts -> ARec f ts
-toARec = go id
-  where go :: ([Any] -> [Any]) -> Rec f ts' -> ARec f ts
-        go acc RNil = ARec $! Array.listArray (0, n - 1) (acc [])
-        go acc (x :& xs) = go (acc . (unsafeCoerce x :)) xs
-        n = natToInt @(RLength ts)
-{-# INLINE toARec #-}
-
--- | Defines a constraint that lets us index into an 'ARec' in order
--- to produce a 'Rec' using 'fromARec'.
-class (NatToInt (RIndex t ts)) => IndexableField ts t where
-instance (NatToInt (RIndex t ts)) => IndexableField ts t where
-
--- | Convert an 'ARec' into a 'Rec'.
-fromARec :: forall f ts.
-            (RecApplicative ts, RPureConstrained (IndexableField ts) ts)
-         => ARec f ts -> Rec f ts
-fromARec (ARec arr) = rpureConstrained @(IndexableField ts) aux
-  where aux :: forall t. NatToInt (RIndex t ts) => f t
-        aux = unsafeCoerce (arr Array.! natToInt @(RIndex t ts))
-{-# INLINE fromARec #-}
-
--- | Get a field from an 'ARec'.
-aget :: forall t f ts. (NatToInt (RIndex t ts)) => ARec f ts -> f t
-aget (ARec arr) =
-  unsafeCoerce (BArray.unsafeAt arr (natToInt @(RIndex t ts)))
-{-# INLINE aget #-}
-
--- | Set a field in an 'ARec'.
-aput :: forall t t' f ts ts'. (NatToInt (RIndex t ts))
-      => f t' -> ARec f ts -> ARec f ts'
-aput x (ARec arr) = ARec (arr Array.// [(i, unsafeCoerce x)])
-  where i = natToInt @(RIndex t ts)
-{-# INLINE aput #-}
-
--- | Define a lens for a field of an 'ARec'.
-alens :: forall f g t t' ts ts'. (Functor g, NatToInt (RIndex t ts))
-      => (f t -> g (f t')) -> ARec f ts -> g (ARec f ts')
-alens f ar = fmap (flip (aput @t) ar) (f (aget ar))
-{-# INLINE alens #-}
-
--- instance (i ~ RIndex t ts, i ~ RIndex t' ts', NatToInt (RIndex t ts)) => RecElem ARec t t' ts ts' i where
---   rlens = alens
---   rget = aget
---   rput = aput
-
-instance RecElem ARec t t' (t ': ts) (t' ': ts) 'Z where
-  rlensC = alens
-  {-# INLINE rlensC #-}
-  rgetC = aget
-  {-# INLINE rgetC #-}
-  rputC = aput @t
-  {-# INLINE rputC #-}
-
-instance (RIndex t (s ': ts) ~ 'S i, NatToInt i,  RecElem ARec t t' ts ts' i)
-  => RecElem ARec t t' (s ': ts) (s ': ts') ('S i) where
-  rlensC = alens
-  {-# INLINE rlensC #-}
-  rgetC = aget
-  {-# INLINE rgetC #-}
-  rputC = aput @t
-  {-# INLINE rputC #-}
-
--- | Get a subset of a record's fields.
-arecGetSubset :: forall rs ss f.
-                 (IndexWitnesses (RImage rs ss), NatToInt (RLength rs))
-              => ARec f ss -> ARec f rs
-arecGetSubset (ARec arr) = ARec (Array.listArray (0, n-1) $
-                                 go (indexWitnesses @(RImage rs ss)))
-  where go :: [Int] -> [Any]
-        go = map (arr Array.!)
-        n = natToInt @(RLength rs)
-{-# INLINE arecGetSubset #-}
-
--- | Set a subset of a larger record's fields to all of the fields of
--- a smaller record.
-arecSetSubset :: forall rs ss f. (IndexWitnesses (RImage rs ss))
-              => ARec f ss -> ARec f rs -> ARec f ss
-arecSetSubset (ARec arrBig) (ARec arrSmall) = ARec (arrBig Array.// updates)
-  where updates = zip (indexWitnesses @(RImage rs ss)) (Array.elems arrSmall)
-{-# INLINE arecSetSubset #-}
-
-instance (is ~ RImage rs ss, IndexWitnesses is, NatToInt (RLength rs))
-         => RecSubset ARec rs ss is where
-  rsubsetC f big = fmap (arecSetSubset big) (f (arecGetSubset big))
-  {-# INLINE rsubsetC #-}
-
-instance (RPureConstrained (IndexableField rs) rs,
-          RecApplicative rs,
-          Show (Rec f rs)) => Show (ARec f rs) where
-  show = show . fromARec
-
-instance (RPureConstrained (IndexableField rs) rs,
-          RecApplicative rs,
-          Eq (Rec f rs)) => Eq (ARec f rs) where
-  x == y = fromARec x == fromARec y
-
-instance (RPureConstrained (IndexableField rs) rs,
-          RecApplicative rs,
-          Ord (Rec f rs)) => Ord (ARec f rs) where
-  compare x y = compare (fromARec x) (fromARec y)
+module Data.Vinyl.ARec
+  ( ARec -- Exported abstractly
+  , IndexableField
+  , ToARec
+  , toARec
+  , fromARec
+  , aget
+  , arecGetSubset
+  , arecSetSubset
+  , arecRepsMatchCoercion
+  , arecConsMatchCoercion
+  ) where
+import Data.Vinyl.ARec.Internal
diff --git a/Data/Vinyl/ARec/Internal.hs b/Data/Vinyl/ARec/Internal.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/ARec/Internal.hs
@@ -0,0 +1,303 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+#endif
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- | Constant-time field accessors for extensible records. The
+-- trade-off is the usual lists vs arrays one: it is fast to add an
+-- element to the head of a list, but element access is linear time;
+-- array access time is uniform, but extending the array is more
+-- slower.
+--
+-- Tradeoffs:
+--
+-- * No sharing of the spine (i.e. when you change elements in the front of the
+--   record the tail can't be re-used)
+-- * ARec requires (4 + n) words + size of the fields
+--   * 1 for the ARec constructor
+--   * 1 for the pointer to the SmallArray#
+--   * The SmallArray# has 2 words as header (1 for GC, 1 for number of elements)
+--   * 1 pointer per element to the actual data
+-- * Rec requires (2n) words + size of Fields
+--   * 1 word per (:&) constructor
+--   * 1 word for the pointer to the element
+module Data.Vinyl.ARec.Internal
+  ( ARec (..)
+  , ToARec
+  , IndexableField
+  , arec
+  , ARecBuilder (..)
+  , arcons
+  , arnil
+  , toARec
+  , fromARec
+  , aget
+  , unsafeAput
+  , unsafeAlens
+  , arecGetSubset
+  , arecSetSubset
+  , arecRepsMatchCoercion
+  , arecConsMatchCoercion
+  ) where
+import Data.Vinyl.Core
+import Data.Vinyl.Lens (RecElem(..), RecSubset(..))
+import Data.Vinyl.TypeLevel
+import Data.Vinyl.ARec.Internal.SmallArray
+import Control.Monad.ST
+
+import Unsafe.Coerce
+#if __GLASGOW_HASKELL__ < 806
+import Data.Constraint.Forall (Forall)
+#endif
+import Data.Type.Coercion     (Coercion (..))
+import GHC.Types
+
+-- | An array-backed extensible record with constant-time field
+-- access.
+newtype ARec (f :: k -> *) (ts :: [k]) = ARec SmallArray
+type role ARec representational nominal
+
+-- | Get the ith element from the ARec
+unsafeIxARec
+  :: forall a k (f :: k -> *) (ts :: [k]).
+     ARec f ts
+  -> Int
+  -> a
+unsafeIxARec (ARec ar) ix = indexSmallArray ar ix
+{-# INLINE unsafeIxARec #-}
+
+-- | Given that @xs@ and @ys@ have the same length, and mapping
+-- @f@ over @xs@ and @g@ over @ys@ produces lists whose elements
+-- are pairwise 'Coercible', @ARec f xs@ and @ARec g ys@ are
+-- 'Coercible'.
+arecRepsMatchCoercion :: AllRepsMatch f xs g ys => Coercion (ARec f xs) (ARec g ys)
+arecRepsMatchCoercion = unsafeCoerce (Coercion :: Coercion () ())
+
+-- | Given that @forall x. Coercible (f x) (g x)@, produce a coercion from
+-- @ARec f xs@ to @ARec g xs@. While the constraint looks a lot like
+-- @Coercible f g@, it is actually weaker.
+
+#if __GLASGOW_HASKELL__ >= 806
+arecConsMatchCoercion ::
+  (forall (x :: k). Coercible (f x) (g x)) => Coercion (ARec f xs) (ARec g xs)
+arecConsMatchCoercion = unsafeCoerce (Coercion :: Coercion () ())
+#else
+arecConsMatchCoercion :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
+  Forall (Similar f g) => Coercion (Rec f xs) (Rec g xs)
+-- Why do we need this? No idea, really. I guess some change in
+-- newtype handling for Coercible in 8.6?
+arecConsMatchCoercion = unsafeCoerce (Coercion :: Coercion (Rec f xs) (Rec f xs))
+#endif
+
+-- Using a class instead of a recursive function allows aRecValues to be
+-- completely inlined
+class ToARec (us :: [k]) where
+  aRecValues :: Rec f us -> ARecBuilder f us
+
+instance ToARec '[] where
+  aRecValues RNil = arnil
+  {-# INLINE aRecValues #-}
+
+instance ToARec us => ToARec (u ': us) where
+  aRecValues (x :& xs) = x `arcons` aRecValues xs
+  {-# INLINE aRecValues #-}
+
+-- | Convert a 'Rec' into an 'ARec' for constant-time field access.
+toARec
+  :: forall f ts.
+     (NatToInt (RLength ts), ToARec ts)
+  => Rec f ts
+  -> ARec f ts
+toARec rs = arec (aRecValues rs)
+{-# INLINE toARec #-}
+
+{-
+-- This is sensible, but the ergonomics are likely quite bad thanks to the
+-- interaction between Coercible resolution and resolution in the presence of
+-- quantified constraints. Is there a good way to do this?
+
+arecConsMatchCoercible :: forall k f g rep (r :: TYPE rep).
+     (forall (x :: k). Coercible (f x) (g x))
+  => ((forall (xs :: [k]). Coercible (ARec f xs) (ARec g xs)) => r) -> r
+arecConsMatchCoercible f = f
+-}
+
+-- | An efficient builder for ARec values
+--
+-- Use the pseudo-constructors 'arcons' and 'arnil' to construct an
+-- 'ARecBuilder' and then turn it into an 'ARec' with 'arec'
+--
+-- Example: (requires -XOverloadedLabels and )
+--
+-- > user :: ARec ElField '[ "name"   ::: String
+-- >                       , "age"    ::: Int
+-- >                       , "active" ::: Bool]
+-- > user = arec (  #name   =: "Peter"
+-- >             `arcons` #age    =: 4
+-- >             `arcons` #active =: True
+-- >             `arcons` arnil
+-- >             )
+newtype ARecBuilder f us =
+  -- A function that writes values to the correct position in the underlying array
+  -- Takes the current index
+  ARecBuilder ( forall s.
+                Int -- Index to write to
+              -> SmallMutableArray s -- Arrray to write to
+              -> ST s ()
+              )
+
+infixr 1 `arcons`
+-- | Pseudo-constructor for an ARecBuilder
+--
+-- "Cons" a field to an ARec under construction
+--
+-- See 'ARecBuilder'
+arcons :: f u -> ARecBuilder f us -> ARecBuilder f (u ': us)
+arcons !v (ARecBuilder fvs) = ARecBuilder $ \i mArr -> do
+    writeSmallArray mArr i v
+    fvs (i+1) mArr
+{-# INLINE arcons #-}
+
+-- | Pseudo-constructor for 'ARecBuilder'
+--
+-- Build an ARec without fields
+--
+-- See 'ARecBuilder'
+arnil :: ARecBuilder f '[]
+arnil = ARecBuilder $ \_i _arr -> return ()
+{-# INLINE arnil #-}
+
+-- | Turn an ARecBuilder into an ARec
+--
+-- See 'ARecBuilder'
+arec
+  :: forall k (us :: [k] ) f
+  . (NatToInt (RLength us)) =>
+      ARecBuilder f us
+  -> ARec f us
+arec (ARecBuilder fillArray) = ARec $
+  runST $ withNewSmallArray (natToInt @(RLength us))
+          $ fillArray 0
+{-# INLINE arec #-}
+
+-- | Defines a constraint that lets us index into an 'ARec' in order
+-- to produce a 'Rec' using 'fromARec'.
+class (NatToInt (RIndex t ts)) => IndexableField ts t where
+instance (NatToInt (RIndex t ts)) => IndexableField ts t where
+
+-- | Convert an 'ARec' into a 'Rec'.
+fromARec :: forall f ts.
+            (RecApplicative ts, RPureConstrained (IndexableField ts) ts)
+         => ARec f ts -> Rec f ts
+fromARec ar = rpureConstrained @(IndexableField ts) aux
+  where aux :: forall t. NatToInt (RIndex t ts) => f t
+        aux = unsafeIxARec ar (natToInt @(RIndex t ts))
+{-# INLINE fromARec #-}
+
+-- | Get a field from an 'ARec'.
+aget :: forall t f ts. (NatToInt (RIndex t ts)) => ARec f ts -> f t
+aget ar = unsafeIxARec ar (natToInt @(RIndex t ts))
+{-# INLINE aget #-}
+
+-- | Set a field in an 'ARec'.
+unsafeAput :: forall t t' f ts ts'. (NatToInt (RIndex t ts))
+      => f t' -> ARec f ts -> ARec f ts'
+unsafeAput x (ARec arr) = ARec $ runST $
+  withThawedSmallArray arr $ \mArr ->
+    writeSmallArray mArr (natToInt @(RIndex t ts)) x
+{-# INLINE unsafeAput #-}
+
+-- | Define a lens for a field of an 'ARec'.
+unsafeAlens :: forall f g t t' ts ts'. (Functor g, NatToInt (RIndex t ts))
+      => (f t -> g (f t')) -> ARec f ts -> g (ARec f ts')
+unsafeAlens f ar = fmap (flip (unsafeAput @t) ar) (f (aget ar))
+{-# INLINE unsafeAlens #-}
+
+-- instance (i ~ RIndex t ts, i ~ RIndex t' ts', NatToInt (RIndex t ts)) => RecElem ARec t t' ts ts' i where
+--   rlens = alens
+--   rget = aget
+--   rput = aput
+
+instance RecElem ARec t t' (t ': ts) (t' ': ts) 'Z where
+  rlensC = unsafeAlens
+  {-# INLINE rlensC #-}
+  rgetC = aget
+  {-# INLINE rgetC #-}
+  rputC = unsafeAput @t
+  {-# INLINE rputC #-}
+
+instance (RIndex t (s ': ts) ~ 'S i, NatToInt i,  RecElem ARec t t' ts ts' i)
+  => RecElem ARec t t' (s ': ts) (s ': ts') ('S i) where
+  rlensC = unsafeAlens
+  {-# INLINE rlensC #-}
+  rgetC = aget
+  {-# INLINE rgetC #-}
+  rputC = unsafeAput @t
+  {-# INLINE rputC #-}
+
+-- | Get a subset of a record's fields.
+arecGetSubset :: forall rs ss f.
+                 (IndexWitnesses (RImage rs ss), NatToInt (RLength rs))
+              => ARec f ss -> ARec f rs
+arecGetSubset (ARec arr) =
+  ARec $ runST $
+    withNewSmallArray (natToInt @(RLength rs)) $ \mArr ->
+      go mArr 0 (indexWitnesses @(RImage rs ss))
+  where
+    go :: SmallMutableArray s -> Int -> [Int] -> ST s ()
+    go _mArr _to [] = return ()
+    go mArr to (from : froms) = do
+      writeSmallArray mArr to (indexSmallArray arr from :: Any)
+      go mArr (to + 1) froms
+{-# INLINE arecGetSubset #-}
+
+-- | Set a subset of a larger record's fields to all of the fields of
+-- a smaller record.
+arecSetSubset :: forall rs ss f. (IndexWitnesses (RImage rs ss))
+              => ARec f ss -> ARec f rs -> ARec f ss
+arecSetSubset (ARec arrBig) (ARec arrSmall) = ARec $ runST $
+  withThawedSmallArray arrBig $ \mArr -> do
+    go mArr 0 (indexWitnesses @(RImage rs ss))
+  where
+    go :: SmallMutableArray s -> Int -> [Int] -> ST s ()
+    go _mArr _ [] = return ()
+    go mArr from (to : tos) = do
+      writeSmallArray mArr to (indexSmallArray arrSmall from)
+      go mArr (from + 1) tos
+{-# INLINE arecSetSubset #-}
+
+instance (is ~ RImage rs ss, IndexWitnesses is, NatToInt (RLength rs))
+         => RecSubset ARec rs ss is where
+  rsubsetC f big = fmap (arecSetSubset big) (f (arecGetSubset big))
+  {-# INLINE rsubsetC #-}
+
+instance (RPureConstrained (IndexableField rs) rs,
+          RecApplicative rs,
+          Show (Rec f rs)) => Show (ARec f rs) where
+  show = show . fromARec
+
+instance (RPureConstrained (IndexableField rs) rs,
+          RecApplicative rs,
+          Eq (Rec f rs)) => Eq (ARec f rs) where
+  x == y = fromARec x == fromARec y
+
+instance (RPureConstrained (IndexableField rs) rs,
+          RecApplicative rs,
+          Ord (Rec f rs)) => Ord (ARec f rs) where
+  compare x y = compare (fromARec x) (fromARec y)
diff --git a/Data/Vinyl/ARec/Internal/SmallArray.hs b/Data/Vinyl/ARec/Internal/SmallArray.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/ARec/Internal/SmallArray.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE BangPatterns #-}
+
+-- | Helper functions for SmallArray#
+--
+-- This module exposes _unsafe_ functions to work with SmallArrays.  That means
+-- that specifically neither index bounds nor element types are checked So this
+-- functionality should only be used in a context that enforces them by some
+-- other means, e.g. ARec's type index
+
+module Data.Vinyl.ARec.Internal.SmallArray where
+
+import GHC.Prim
+import GHC.Types
+import Unsafe.Coerce
+import GHC.ST
+
+data SmallArray = SmallArray !(SmallArray# Any)
+data SmallMutableArray s = SmallMutableArray !(SmallMutableArray# s Any)
+
+indexSmallArray :: SmallArray -> Int -> a
+indexSmallArray (SmallArray arr) (I# ix) =
+  case indexSmallArray# arr ix of
+    (# v #) -> unsafeCoerce v
+{-# INLINE indexSmallArray #-}
+
+withNewSmallArray :: Int -> (SmallMutableArray s -> ST s ()) -> ST s SmallArray
+withNewSmallArray (I# len#) f =
+  ST $ \s0 ->  case newSmallArray# len# (error "withNewSmallArray exploded") s0 of
+       (# s1, mArr #) ->
+         case f (SmallMutableArray mArr) of
+           ST st -> case st s1 of
+             (# s2, () #) -> case unsafeFreezeSmallArray# mArr s2 of
+               (# s3, ar #) -> (# s3, SmallArray ar #)
+{-# INLINE withNewSmallArray #-}
+
+writeSmallArray :: SmallMutableArray s -> Int -> a -> ST s ()
+writeSmallArray (SmallMutableArray mArr) (I# n#) x = ST $ \s ->
+  case writeSmallArray# mArr n# (unsafeCoerce x) s of
+    s' -> (# s', () #)
+{-# INLINE writeSmallArray #-}
+
+withThawedSmallArray :: SmallArray
+               -> (SmallMutableArray s -> ST s ())
+               -> ST s SmallArray
+withThawedSmallArray (SmallArray arr) f = ST $ \s0 ->
+  let !(I# z#) = 0
+  in case thawSmallArray# arr z# (sizeofSmallArray# arr) s0 of
+       (# s1, mArr #) ->
+         case f (SmallMutableArray mArr) of
+           ST st -> case st s1 of
+             (# s2, () #) -> case unsafeFreezeSmallArray# mArr s2 of
+               (# s3, ar #) -> (# s3, SmallArray ar #)
+{-# INLINE withThawedSmallArray #-}
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
@@ -142,7 +142,7 @@
 -- | The interpretation function of the 'FieldTyper' symbols.
 type family ApplyFieldTyper (f :: FieldTyper) (a :: k) :: * where
   ApplyFieldTyper 'FieldId a = a
-  ApplyFieldTyper 'FieldSnd '(s, b) = b
+  ApplyFieldTyper 'FieldSnd a = Snd a
 
 -- | A mapping of record contexts into the 'FieldTyper' function
 -- space. We explicitly match on 'ElField' to pick out the payload
@@ -160,8 +160,8 @@
 
 -- | Generate a record from fields derived from type class
 -- instances.
-class RecPointed c (f :: u -> *) (ts :: [u]) where
-  rpointMethod :: (forall (a :: u). c (f a) => f a) -> Rec f ts
+class RecPointed c f ts where
+  rpointMethod :: (forall a. c (f a) => f a) -> Rec f ts
 
 instance RecPointed c f '[] where
   rpointMethod _ = RNil
@@ -175,14 +175,14 @@
 -- | 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
+class RecMapMethod c f ts 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
+class RecMapMethod1 c f ts where
   rmapMethod1 :: (forall a. c (f a) => f a -> g a)
               -> Rec f ts -> Rec g ts
 
diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs
--- a/Data/Vinyl/Core.hs
+++ b/Data/Vinyl/Core.hs
@@ -10,8 +10,12 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE Trustworthy           #-}
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE TypeFamilies          #-}
+#if __GLASGOW_HASKELL__ >= 806
+{-# LANGUAGE QuantifiedConstraints #-}
+#endif
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE UndecidableInstances  #-}
 
@@ -30,8 +34,10 @@
 -- type. Instead, they treat the record as a list of fields, so will
 -- have performance linear in the size of the record.
 module Data.Vinyl.Core where
-
+import Data.Coerce (Coercible)
+#if __GLASGOW_HASKELL__ < 808
 import Data.Monoid (Monoid)
+#endif
 #if __GLASGOW_HASKELL__ < 804
 import Data.Semigroup (Semigroup(..))
 #endif
@@ -45,6 +51,11 @@
 import Data.Type.Coercion (TestCoercion (..), Coercion (..))
 import GHC.Generics
 import GHC.Types (Constraint, Type)
+import Unsafe.Coerce (unsafeCoerce)
+import Control.DeepSeq (NFData, rnf)
+#if __GLASGOW_HASKELL__ < 806
+import Data.Constraint.Forall (Forall)
+#endif
 
 -- | 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
@@ -396,3 +407,97 @@
          (Rep (Rec f rs)))
   from (x :& xs) = M1 (M1 (K1 x) :*: M1 (from xs))
   to (M1 (M1 (K1 x) :*: M1 xs)) = x :& to xs
+
+instance ReifyConstraint NFData f xs => NFData (Rec f xs) where
+  rnf = go . reifyConstraint @NFData
+    where
+      go :: forall elems. Rec (Dict NFData :. f) elems -> ()
+      go RNil = ()
+      go (Compose (Dict x) :& xs) = rnf x `seq` go xs
+
+type family Head xs where
+  Head (x ': _) = x
+type family Tail xs where
+  Tail (_ ': xs) = xs
+
+type family AllRepsMatch_ (f :: j -> *) (xs :: [j]) (g :: k -> *) (ys :: [k]) :: Constraint where
+  AllRepsMatch_ f (x ': xs) g ys =
+    ( ys ~ (Head ys ': Tail ys)
+    , Coercible (f x) (g (Head ys))
+    , AllRepsMatch_ f xs g (Tail ys) )
+  AllRepsMatch_ _ '[] _ ys = ys ~ '[]
+
+-- | @AllRepsMatch f xs g ys@ means that @xs@ and @ys@ have the
+-- same lengths, and that mapping @f@ over @xs@ and @g@ over @ys@
+-- produces lists whose corresponding elements are 'Coercible' with
+-- each other. For example, the following hold:
+--
+-- @AllRepsMatch Proxy '[1,2,3] Proxy '[4,5,6]@
+-- @AllRepsMatch Sum '[Int,Word] Identity '[Min Int, Max Word]@
+type AllRepsMatch f xs g ys = (AllRepsMatch_ f xs g ys, AllRepsMatch_ g ys f xs)
+
+-- This two-sided approach means that the *length* of each list
+-- can be inferred from the length of the other. I don't know how
+-- useful that is in practice, but we get it almost for free.
+
+-- | Given that for each element @x@ in the list @xs@,
+repsMatchCoercion :: AllRepsMatch f xs g ys => Coercion (Rec f xs) (Rec g ys)
+repsMatchCoercion = unsafeCoerce (Coercion :: Coercion () ())
+
+{-
+-- "Proof" that repsMatchCoercion is sensible.
+repsMatchConvert :: AllRepsMatch f xs g ys => Rec f xs -> Rec g ys
+repsMatchConvert RNil = RNil
+repsMatchConvert (x :& xs) = coerce x :& repsMatchConvert xs
+-}
+
+#if __GLASGOW_HASKELL__ >= 806
+consMatchCoercion ::
+  (forall (x :: k). Coercible (f x) (g x)) => Coercion (Rec f xs) (Rec g xs)
+#else
+consMatchCoercion :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
+  Forall (Similar f g) => Coercion (Rec f xs) (Rec g xs)
+#endif
+consMatchCoercion = unsafeCoerce (Coercion :: Coercion () ())
+{-
+-- "Proof" that consMatchCoercion is sensible.
+consMatchConvert ::
+  (forall (x :: k). Coercible (f x) (g x)) => Rec f xs -> Rec g xs
+consMatchConvert RNil = RNil
+consMatchConvert (x :& xs) = coerce x :& consMatchConvert xs
+
+-- And for old GHC.
+consMatchConvert' :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
+  Forall (Similar f g) => Rec f xs -> Rec g xs
+consMatchConvert' RNil = RNil
+consMatchConvert' ((x :: f x) :& xs) =
+  case inst :: Forall (Similar f g) DC.:- Similar f g x of
+    DC.Sub DC.Dict -> coerce x :& consMatchConvert' xs
+-}
+
+{-
+-- This is sensible, but I suspect the ergonomics will be awful
+-- thanks to the interaction between Coercible constraint resolution
+-- and constraint resolution with quantified constraints. Is there
+-- a good way to accomplish it?
+
+-- | Given
+--
+-- @
+-- forall x. Coercible (f x) (g x)
+-- @
+--
+-- provide the constraint
+--
+-- @
+-- forall xs. Coercible (Rec f xs) (Rec g xs)
+-- @
+consMatchCoercible :: forall k f g rep (r :: TYPE rep).
+     (forall (x :: k). Coercible (f x) (g x))
+  => ((forall (xs :: [k]). Coercible (Rec f xs) (Rec g xs)) => r) -> r
+consMatchCoercible f = case unsafeCoerce @(Zouch f f) @(Zouch f g) (Zouch $ \r -> r) of
+  Zouch q -> q f
+
+newtype Zouch (f :: k -> *) (g :: k -> *) =
+  Zouch (forall rep (r :: TYPE rep). ((forall (xs :: [k]). Coercible (Rec f xs) (Rec g xs)) => r) -> r)
+-}
diff --git a/Data/Vinyl/Curry.hs b/Data/Vinyl/Curry.hs
--- a/Data/Vinyl/Curry.hs
+++ b/Data/Vinyl/Curry.hs
@@ -11,7 +11,7 @@
 
 -}
 module Data.Vinyl.Curry where
-
+import           Data.Kind (Type)
 import           Data.Vinyl
 import           Data.Vinyl.Functor
 import           Data.Vinyl.XRec
@@ -33,6 +33,7 @@
   -}
   rcurry :: (Rec f ts -> a) -> CurriedF f ts a
 
+class RecordCurry' ts where
   {-|
   N-ary version of 'curry' over pure records.
 
@@ -51,12 +52,14 @@
 instance RecordCurry '[] where
   rcurry f = f RNil
   {-# INLINABLE rcurry #-}
+instance RecordCurry' '[] where
   rcurry' f = f RNil
   {-# INLINABLE rcurry' #-}
 
 instance RecordCurry ts => RecordCurry (t ': ts) where
   rcurry f x = rcurry (\xs -> f (x :& xs))
   {-# INLINABLE rcurry #-}
+instance RecordCurry' ts => RecordCurry' (t ': ts) where
   rcurry' f x = rcurry' (\xs -> f (Identity x :& xs))
   {-# INLINABLE rcurry' #-}
 
@@ -167,7 +170,7 @@
 CurriedF Maybe '[Int, Bool, String] Int :: *
 = Maybe Int -> Maybe Bool -> Maybe [Char] -> Int
 -}
-type family CurriedF (f :: u -> *) (ts :: [u]) a where
+type family CurriedF (f :: u -> Type) (ts :: [u]) a where
   CurriedF f '[] a = a
   CurriedF f (t ': ts) a = f t -> CurriedF f ts a
 
@@ -180,6 +183,6 @@
 CurriedX (Maybe :. Identity) '[Int, Bool, String] Int :: *
 = Maybe Int -> Maybe Bool -> Maybe [Char] -> Int
 -}
-type family CurriedX (f :: u -> *) (ts :: [u]) a where
+type family CurriedX (f :: u -> Type) (ts :: [u]) a where
   CurriedX f '[] a = a
   CurriedX f (t ': ts) a = HKD f t -> CurriedX f ts a
diff --git a/Data/Vinyl/Derived.hs b/Data/Vinyl/Derived.hs
--- a/Data/Vinyl/Derived.hs
+++ b/Data/Vinyl/Derived.hs
@@ -46,7 +46,7 @@
 getField (Field x) = x
 
 -- | Get the label name of an 'ElField'.
-getLabel :: forall s t. ElField '(s,t) -> String
+getLabel :: forall s t. KnownSymbol s => ElField '(s,t) -> String
 getLabel (Field _) = symbolVal (Proxy::Proxy s)
 
 -- | 'ElField' is isomorphic to a functor something like @Compose
@@ -92,14 +92,14 @@
 rputf' :: forall l v v' record us us'.
           (HasField record l us us' v v', KnownSymbol l, RecElemFCtx record ElField)
        => Label l -> v' -> record ElField us -> record ElField us'
-rputf' _ = rput' @(l:::v) . (Field :: v' -> ElField '(l,v'))
+rputf' _ = rput' @_ @(l:::v) . (Field :: v' -> ElField '(l,v'))
 
 -- | Set a named field without changing its type. @rputf #foo 23@ sets
 -- the field named @#foo@ to @23@.
 rputf :: forall l v record us.
           (HasField record l us us v v, KnownSymbol l, RecElemFCtx record ElField)
        => Label l -> v -> record ElField us -> record ElField us
-rputf _ = rput @(l:::v) . Field
+rputf _ = rput @_ @(l:::v) . Field
 
 -- | A lens into a 'Rec' identified by a 'Label'.
 rlensfL' :: forall l v v' record g f us us'.
diff --git a/Data/Vinyl/FromTuple.hs b/Data/Vinyl/FromTuple.hs
--- a/Data/Vinyl/FromTuple.hs
+++ b/Data/Vinyl/FromTuple.hs
@@ -14,6 +14,7 @@
 -- example record construction using 'ElField' for named fields:
 -- @fieldRec (#x =: True, #y =: 'b') :: FieldRec '[ '("x", Bool), '("y", Char) ]@
 module Data.Vinyl.FromTuple where
+import Data.Kind (Type)
 import Data.Monoid (First(..))
 #if __GLASGOW_HASKELL__ < 804
 import Data.Semigroup (Semigroup(..))
@@ -29,7 +30,7 @@
 -- type constructor to a tuple of the common type constructor and a
 -- list of the types to which it is applied in the original
 -- tuple. E.g. @TupleToRecArgs f (f a, f b) ~ (f, [a,b])@.
-type family TupleToRecArgs f t = (r :: (u -> *, [u])) | r -> t where
+type family TupleToRecArgs f t = (r :: (u -> Type, [u])) | r -> t where
   TupleToRecArgs f (f a, f b, f c, f d, f e, f z, f g, f h) =
     '(f, [a,b,c,d,e,z,g,h])
   TupleToRecArgs f (f a, f b, f c, f d, f e, f z, f g) = '(f, [a,b,c,d,e,z,g])
@@ -42,16 +43,16 @@
 
 -- | Apply the 'Rec' type constructor to a type-level tuple of its
 -- arguments.
-type family UncurriedRec (t :: (u -> *, [u])) = r | r -> t where
+type family UncurriedRec (t :: (u -> Type, [u])) = r | r -> t where
   UncurriedRec '(f, ts) = Rec f ts
 
 -- | Apply the 'XRec' type constructor to a type-level tuple of its
 -- arguments.
-type family UncurriedXRec (t :: (u -> *, [u])) = r | r -> t where
+type family UncurriedXRec (t :: (u -> Type, [u])) = r | r -> t where
   UncurriedXRec '(f, ts) = XRec f ts
 
 -- | Convert between an 'XRec' and an isomorphic tuple.
-class TupleXRec (f :: u -> *) (t :: [u]) where
+class TupleXRec f t where
   -- | Convert an 'XRec' to a tuple. Useful for pattern matching on an
   -- entire record.
   xrecTuple :: XRec f t -> ListToHKDTuple f t
@@ -90,7 +91,7 @@
     (a, b, c, d, e, z, g, h)
   xrecX (a, b, c, d, e, z, g, h) = a ::& b ::& c ::& d ::& e ::& z ::& g ::& h ::& XRNil
 
-type family ListToHKDTuple (f :: u -> *) (ts :: [u]) :: * where
+type family ListToHKDTuple (f :: u -> Type) (ts :: [u]) :: Type where
   ListToHKDTuple f '[] = HKD f ()
   ListToHKDTuple f '[a,b] = (HKD f a, HKD f b)
   ListToHKDTuple f '[a,b,c] = (HKD f  a, HKD f b, HKD f c)
diff --git a/Data/Vinyl/Functor.hs b/Data/Vinyl/Functor.hs
--- a/Data/Vinyl/Functor.hs
+++ b/Data/Vinyl/Functor.hs
@@ -42,6 +42,7 @@
 import GHC.Generics
 import GHC.TypeLits
 import GHC.Types (Type)
+import Data.Vinyl.TypeLevel (Snd)
 
 {- $introduction
     This module provides functors and functor compositions
@@ -107,8 +108,10 @@
 -- | A value with a phantom 'Symbol' label. It is not a
 -- Haskell 'Functor', but it is used in many of the same places a
 -- 'Functor' is used in vinyl.
-data ElField (field :: (Symbol, Type)) where
-  Field :: KnownSymbol s => !t -> ElField '(s,t)
+--
+-- Morally: newtype ElField (s, t) = Field t
+-- But GHC doesn't allow that
+newtype ElField (t :: (Symbol, Type)) = Field (Snd t)
 
 deriving instance Eq t => Eq (ElField '(s,t))
 deriving instance Ord t => Ord (ElField '(s,t))
diff --git a/Data/Vinyl/Lens.hs b/Data/Vinyl/Lens.hs
--- a/Data/Vinyl/Lens.hs
+++ b/Data/Vinyl/Lens.hs
@@ -11,6 +11,11 @@
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE CPP                   #-}
+#if __GLASGOW_HASKELL__ < 806
+{-# LANGUAGE TypeInType #-}
+#endif
+
 -- | Lenses into record fields.
 module Data.Vinyl.Lens
   ( RecElem(..)
@@ -32,15 +37,16 @@
 import Data.Vinyl.Core
 import Data.Vinyl.Functor
 import Data.Vinyl.TypeLevel
+#if __GLASGOW_HASKELL__ < 806
+import Data.Kind
+#endif
 
 -- | The presence of a field in a record is witnessed by a lens into
 -- 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, NatToInt i)
-  => RecElem record (r :: k) (r' :: k)
-             (rs :: [k]) (rs' :: [k])
-             (i :: Nat) | r r' rs i -> rs' where
+  => RecElem (record :: (k -> *) -> [k] -> *) (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
@@ -92,16 +98,16 @@
   {-# INLINE rlensC #-}
   rgetC = getConst . rlensC Const
   {-# INLINE rgetC #-}
-  rputC y = getIdentity . rlensC @_ @r (\_ -> Identity y)
+  rputC y = getIdentity . rlensC @_ @_ @r (\_ -> Identity y)
   {-# INLINE rputC #-}
 
 instance (RIndex r (s ': rs) ~ 'S i, RecElem Rec r r' rs rs' i)
   => RecElem Rec r r' (s ': rs) (s ': rs') ('S i) where
   rlensC f (x :& xs) = fmap (x :&) (rlensC f xs)
   {-# INLINE rlensC #-}
-  rgetC = getConst . rlensC @_ @r @r' Const
+  rgetC = getConst . rlensC @_ @_ @r @r' Const
   {-# INLINE rgetC #-}
-  rputC y = getIdentity . rlensC @_ @r (\_ -> Identity y)
+  rputC y = getIdentity . rlensC @_ @_ @r (\_ -> Identity y)
   {-# INLINE rputC #-}
 
 --  | The 'rgetC' field getter with the type arguments re-ordered for
@@ -113,15 +119,16 @@
 
 -- | The type-changing field setter 'rputC' with the type arguments
 -- re-ordered for more convenient usage with @TypeApplications@.
-rput' :: forall r r' rs rs' record f. (RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f)
+rput' :: forall k (r :: k) (r' :: k) (rs :: [k]) (rs' :: [k]) record f
+       . (RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f)
       => f r' -> record f rs -> record f rs'
-rput' = rputC @_ @r @r'
+rput' = rputC @k @record @r @r' @rs @rs'
 
 -- | Type-preserving field setter. This type is simpler to work with
 -- than that of 'rput''.
-rput :: forall r rs record f. (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f)
+rput :: forall k (r :: k) rs record f. (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f)
       => f r -> record f rs -> record f rs
-rput = rput' @r
+rput = rput' @_ @r @r @rs @rs @record
 
 -- | Type-changing field lens 'rlensC' with the type arguments
 -- re-ordered for more convenient usage with @TypeApplications@.
@@ -141,7 +148,7 @@
 -- record to the former's is evident. That is, we can either cast a larger
 -- record to a smaller one, or we may replace the values in a slice of a
 -- record.
-class is ~ RImage rs ss => RecSubset record (rs :: [k]) (ss :: [k]) is where
+class is ~ RImage rs ss => RecSubset record rs ss is where
   -- | An opportunity for instances to generate constraints based on
   -- the functor parameter of records passed to class methods.
   type RecSubsetFCtx record (f :: k -> *) :: Constraint
@@ -178,7 +185,7 @@
 -- | A lens into a slice of the larger record. This is 'rsubsetC' with
 -- the type arguments reordered for more convenient usage with
 -- @TypeApplications@.
-rsubset :: forall rs ss f g record is.
+rsubset :: forall k rs ss f g record is.
            (RecSubset record (rs :: [k]) (ss :: [k]) is,
            Functor g, RecSubsetFCtx record f)
         => (record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
diff --git a/Data/Vinyl/Recursive.hs b/Data/Vinyl/Recursive.hs
--- a/Data/Vinyl/Recursive.hs
+++ b/Data/Vinyl/Recursive.hs
@@ -6,11 +6,19 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ < 806
+{-# LANGUAGE TypeInType #-}
+#endif
+
 -- | Recursive definitions of various core vinyl functions. These are
 -- simple definitions that put less strain on the compiler. They are
 -- expected to have slower run times, but faster compile times than
 -- the definitions in "Data.Vinyl.Core".
 module Data.Vinyl.Recursive where
+#if __GLASGOW_HASKELL__ < 806
+import Data.Kind
+#endif
 import Data.Proxy (Proxy(..))
 import Data.Vinyl.Core (rpure, RecApplicative, Rec(..), Dict(..))
 import Data.Vinyl.Functor (Compose(..), (:.), Lift(..), Const(..))
@@ -139,7 +147,7 @@
 
 -- | Build a record whose elements are derived solely from a
 -- constraint satisfied by each.
-rpureConstrained :: forall c (f :: u -> *) proxy ts.
+rpureConstrained :: forall u c (f :: u -> *) proxy ts.
                     (AllConstrained c ts, RecApplicative ts)
                  => proxy c -> (forall a. c a => f a) -> Rec f ts
 rpureConstrained _ f = go (rpure Proxy)
diff --git a/Data/Vinyl/SRec.hs b/Data/Vinyl/SRec.hs
--- a/Data/Vinyl/SRec.hs
+++ b/Data/Vinyl/SRec.hs
@@ -28,6 +28,7 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -44,6 +45,9 @@
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
+#if __GLASGOW_HASKELL__ < 806
+{-# LANGUAGE TypeInType #-}
+#endif
 
 -- We get warnings about incomplete patterns on various class
 -- instances.
@@ -60,6 +64,9 @@
   , peekField, pokeField
 ) where
 import Data.Coerce (coerce)
+#if __GLASGOW_HASKELL__ < 806
+import Data.Kind
+#endif
 import Data.Vinyl.Core
 import Data.Vinyl.Functor (Lift(..), Compose(..), type (:.), ElField)
 import Data.Vinyl.Lens (RecElem(..), RecSubset(..), type (⊆), RecElemFCtx)
@@ -68,13 +75,17 @@
 import Foreign.Ptr (Ptr)
 import Foreign.Storable (Storable(..))
 import System.IO.Unsafe (unsafePerformIO, unsafeDupablePerformIO)
+#if __GLASGOW_HASKELL__ >= 900
+import Unsafe.Coerce (unsafeCoerce#)
+import GHC.Prim (touch#, RealWorld)
+#else
+import GHC.Prim (touch#, unsafeCoerce#, RealWorld)
+#endif
 
 import GHC.IO (IO(IO))
 import GHC.Base (realWorld#)
 import GHC.TypeLits (Symbol)
-
 import GHC.Prim (MutableByteArray#, newAlignedPinnedByteArray#, byteArrayContents#)
-import GHC.Prim (unsafeCoerce#, touch#, RealWorld)
 import GHC.Ptr (Ptr(..))
 import GHC.Types (Int(..))
 
@@ -219,7 +230,7 @@
       dst <$ copyBytes dst' src' n
 
 -- | Set a field.
-sput :: forall (f :: u -> *) (t :: u) (ts :: [u]).
+sput :: forall u (f :: u -> *) (t :: u) (ts :: [u]).
         ( FieldOffset f ts t
         , Storable (Rec f ts)
         , AllConstrained (FieldOffset f ts) ts)
@@ -296,7 +307,7 @@
   {-# INLINE rputC #-}
 
 -- | Get a subset of a record's fields.
-srecGetSubset :: forall (ss :: [u]) (rs :: [u]) (f :: u -> *).
+srecGetSubset :: forall u (ss :: [u]) (rs :: [u]) (f :: u -> *).
                  (RPureConstrained (FieldOffset f ss) rs,
                   RPureConstrained (FieldOffset f rs) rs,
                   RFoldMap rs, RMap rs, RApply rs,
@@ -334,7 +345,7 @@
 type Poker f = Lift (->) f TaggedIO
 
 -- | Set a subset of a record's fields.
-srecSetSubset :: forall (f :: u -> *) (ss :: [u]) (rs :: [u]).
+srecSetSubset :: forall u (f :: u -> *) (ss :: [u]) (rs :: [u]).
                  (rs ⊆ ss,
                   RPureConstrained (FieldOffset f ss) rs,
                   RPureConstrained (FieldOffset f rs) rs,
diff --git a/Data/Vinyl/Syntax.hs b/Data/Vinyl/Syntax.hs
--- a/Data/Vinyl/Syntax.hs
+++ b/Data/Vinyl/Syntax.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, FlexibleInstances, InstanceSigs,
+{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, InstanceSigs,
              MultiParamTypeClasses, ScopedTypeVariables,
              TypeApplications, TypeFamilies, TypeOperators,
              UndecidableInstances #-}
diff --git a/Data/Vinyl/Tutorial/Overview.hs b/Data/Vinyl/Tutorial/Overview.hs
--- a/Data/Vinyl/Tutorial/Overview.hs
+++ b/Data/Vinyl/Tutorial/Overview.hs
@@ -38,7 +38,7 @@
 >>> data Fields = Name | Age | Sleeping | Master deriving Show
 
     Any record can be now described by a type-level list of these labels.
-    The @DataKinds@ extension must be enabled to autmatically turn all the
+    The @DataKinds@ extension must be enabled to automatically turn all the
     constructors of the @Field@ type into types.
 
 >>> type LifeForm = [Name, Age, Sleeping]
@@ -157,7 +157,7 @@
 The subtyping relationship between record types is expressed with the
 '<:' constraint; so, 'rcast' is of the following type:
 
-> rcast :: r1 <: r2 => Rec f r1 -> Rec f r2
+> rcast :: r1 <: r2 => Rec f r2 -> Rec f r1
 
 Also provided is a "≅" constraint which indicates record congruence
 (that is, two record types differ only in the order of their fields).
diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs
--- a/Data/Vinyl/TypeLevel.hs
+++ b/Data/Vinyl/TypeLevel.hs
@@ -11,11 +11,18 @@
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE CPP                   #-}
+#if __GLASGOW_HASKELL__ < 806
+{-# LANGUAGE TypeInType #-}
+#endif
+#if __GLASGOW_HASKELL__ >= 810
+{-# LANGUAGE UndecidableInstances  #-}
+#endif
 
 module Data.Vinyl.TypeLevel where
 
-import GHC.Exts
-import GHC.Types (Type)
+import Data.Coerce
+import Data.Kind
 
 -- | A mere approximation of the natural numbers. And their image as lifted by
 -- @-XDataKinds@ corresponds to the actual natural numbers.
@@ -66,7 +73,7 @@
   RImage '[] ss = '[]
   RImage (r ': rs) ss = RIndex r ss ': RImage rs ss
 
--- | Remove the first occurence of a type from a type-level list.
+-- | Remove the first occurrence of a type from a type-level list.
 type family RDelete r rs where
   RDelete r (r ': rs) = rs
   RDelete r (s ': rs) = s ': RDelete r rs
@@ -115,3 +122,8 @@
 type family MapTyCon t xs = r | r -> xs where
   MapTyCon t '[] = '[]
   MapTyCon t (x ': xs) = ApplyToField t x ': MapTyCon t xs
+
+-- | This class is used for `consMatchCoercion` with older versions
+-- of GHC.
+class Coercible (f x) (g x) => Similar f g (x :: k)
+instance Coercible (f x) (g x) => Similar f g (x :: k)
diff --git a/Data/Vinyl/XRec.hs b/Data/Vinyl/XRec.hs
--- a/Data/Vinyl/XRec.hs
+++ b/Data/Vinyl/XRec.hs
@@ -81,8 +81,8 @@
 -- permit unrolling of the recursion across a record. The function
 -- mapped across the vector hides the 'HKD' type family under a newtype
 -- constructor to help the type checker.
-class XRMap (f :: u -> *) (g :: u -> *) (rs :: [u]) where
-  xrmapAux :: (forall (a :: u) . XData f a -> XData g a) -> XRec f rs -> XRec g rs
+class XRMap f g rs where
+  xrmapAux :: (forall a . XData f a -> XData g a) -> XRec f rs -> XRec g rs
 
 instance XRMap f g '[] where
   xrmapAux _ RNil = RNil
@@ -127,7 +127,7 @@
 -- This involves the so-called /higher-kinded data/ type family. See
 -- <http://reasonablypolymorphic.com/blog/higher-kinded-data> for more
 -- discussion.
-class IsoHKD (f :: u -> *) (a :: u) where
+class IsoHKD f a where
   type HKD f a
   type HKD f a = f a
   unHKD :: HKD f a -> f a
diff --git a/benchmarks/AccessorsBench.hs b/benchmarks/AccessorsBench.hs
--- a/benchmarks/AccessorsBench.hs
+++ b/benchmarks/AccessorsBench.hs
@@ -8,21 +8,12 @@
 import Data.Monoid (Endo(..))
 import           Data.Vinyl
 import           Data.Vinyl.Syntax ()
-import Lens.Micro ((%~), (&))
-import           System.Exit (exitFailure)
-
-type Fields = '[ '( "a0", Int ), '( "a1", Int ), '( "a2", Int ), '( "a3", Int )
-               , '( "a4", Int ), '( "a5", Int ), '( "a6", Int ), '( "a7", Int )
-               , '( "a8", Int ), '( "a9", Int ), '( "a10", Int ), '( "a11", Int )
-               , '( "a12", Int ), '( "a13", Int ), '( "a14", Int ), '( "a15", Int )
-               ]
+import           Lens.Micro        ((%~), (&))
+import           System.Exit       (exitFailure)
 
-newF :: FieldRec Fields
-newF = Field 0 :& Field 0 :& Field 0 :& Field 0 :&
-       Field 0 :& Field 0 :& Field 0 :& Field 0 :&
-       Field 0 :& Field 0 :& Field 0 :& Field 0 :&
-       Field 0 :& Field 0 :& Field 0 :& Field 99 :&
-       RNil
+import           Bench.ARec
+import           Bench.SRec
+import           Bench.Rec
 
 data HaskRec = HaskRec {
   a0 :: Int,
@@ -45,6 +36,10 @@
 haskRec :: HaskRec
 haskRec = HaskRec 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 99
 
+sumHaskRec r =
+    a0 r + a1 r + a2 r + a3 r + a4 r + a5 r + a6 r + a7 r + a8 r + a9 r
+  + a10 r + a11 r + a12 r + a13 r + a14 r + a15 r
+
 data StrictHaskRec = StrictHaskRec {
   sa0 :: !Int,
   sa1 :: !Int,
@@ -66,6 +61,10 @@
 shaskRec :: StrictHaskRec
 shaskRec = StrictHaskRec 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 99
 
+sumSHaskRec r =
+    sa0 r + sa1 r + sa2 r + sa3 r + sa4 r + sa5 r + sa6 r + sa7 r + sa8 r + sa9 r
+  + sa10 r + sa11 r + sa12 r + sa13 r + sa14 r + sa15 r
+
 data UStrictHaskRec = UStrictHaskRec {
   usa0 :: {-# UNPACK #-} !Int,
   usa1 :: {-# UNPACK #-} !Int,
@@ -87,6 +86,10 @@
 ushaskRec :: UStrictHaskRec
 ushaskRec = UStrictHaskRec 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 99
 
+sumUSHaskRec r =
+    usa0 r + usa1 r + usa2 r + usa3 r + usa4 r + usa5 r + usa6 r + usa7 r + usa8 r
+    + usa9 r + usa10 r + usa11 r + usa12 r + usa13 r + usa14 r + usa15 r
+
 type SubFields = '[ '("a0", Int), '("a8", Int), '("a15", Int)]
 
 -- updateSRec :: forall record. RecordSubset record ElField SubFields Fields
@@ -115,7 +118,8 @@
 
 main :: IO ()
 main =
-  do let arec = toARec newF
+  do let newF = mkRec 0
+         arec = toARec newF
          srec = toSRec newF
      unless (rvalf #a15 arec == rvalf #a15 newF)
             (do putStrLn "AFieldRec accessor disagrees with rvalf"
@@ -142,7 +146,22 @@
          , bench "ARec" $ nf (rvalf #a15 . updateARec) arec
          , bench "SRec" $ nf (rvalf #a15 . updateSRec) srec
          ]
-         , bgroup "FieldRec"
+         ,
+         bgroup "creating"
+         [ bench "vinyl record" $ whnf mkRec 0
+         , bench "toSRec" $ whnf mkToSRec 0
+         , bench "New style ARec with toARec " $ whnf mkToARec 0
+         , bench "New style ARec with arec " $ whnf mkARec 0
+         ]
+         ,bgroup "sums"
+         [ bench "haskell record" $ nf sumHaskRec haskRec
+         , bench "strict haskell record" $ whnf sumSHaskRec shaskRec
+         , bench "unboxed strict haskell record" $ whnf sumUSHaskRec ushaskRec
+         , bench "vinyl SRec" $ nf sumSRec srec
+         , bench "vinyl Rec" $ nf sumRec newF
+         , bench "vinyl ARec" $ nf sumARec arec
+         ]
+       , bgroup "FieldRec"
          [ bench "a0" $ nf (rvalf #a0) newF
          , bench "a4" $ nf (rvalf #a4) newF
          , bench "a8" $ nf (rvalf #a8) newF
diff --git a/benchmarks/Bench/ARec.hs b/benchmarks/Bench/ARec.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Bench/ARec.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE OverloadedLabels      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+
+module Bench.ARec where
+
+import Data.Vinyl
+import Data.Vinyl.ARec.Internal
+import Data.Vinyl.Syntax ()
+
+import Bench.Rec
+
+mkARec :: Int -> ARec ElField Fields
+mkARec i= arec (Field i `arcons` Field i `arcons` Field i `arcons` Field i `arcons`
+                  Field i `arcons` Field i `arcons` Field i `arcons` Field i `arcons`
+                  Field i `arcons` Field i `arcons` Field i `arcons` Field i `arcons`
+                  Field i `arcons` Field i `arcons` Field i `arcons` Field 99 `arcons`
+                  arnil)
+
+
+mkToARec :: Int -> ARec ElField Fields
+mkToARec i= toARec (Field i :& Field i :& Field i :& Field i :&
+                  Field i :& Field i :& Field i :& Field i :&
+                  Field i :& Field i :& Field i :& Field i :&
+                  Field i :& Field i :& Field i :& Field 99 :&
+                  RNil)
+
+sumARec :: ARec ElField Fields -> Int
+sumARec str =
+    get #a0 str + get #a1 str + get #a2 str + get #a3 str + get #a4 str
+  + get #a5 str + get #a6 str + get #a7 str + get #a8 str
+  + get #a9 str + get #a10 str + get #a11 str + get #a12 str
+  + get #a13 str + get #a14 str + get #a15 str
+  where
+    get label r = rvalf label r
+    {-# INLINE get #-}
diff --git a/benchmarks/Bench/Rec.hs b/benchmarks/Bench/Rec.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Bench/Rec.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE OverloadedLabels      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+
+module Bench.Rec where
+
+import           Data.Vinyl
+import           Data.Vinyl.Syntax ()
+
+
+type Fields = '[ '( "a0", Int ), '( "a1", Int ), '( "a2", Int ), '( "a3", Int )
+               , '( "a4", Int ), '( "a5", Int ), '( "a6", Int ), '( "a7", Int )
+               , '( "a8", Int ), '( "a9", Int ), '( "a10", Int ), '( "a11", Int )
+               , '( "a12", Int ), '( "a13", Int ), '( "a14", Int ), '( "a15", Int )
+               ]
+
+mkRec :: Int -> Rec ElField Fields
+mkRec i= Field i :& Field i :& Field i :& Field i :&
+         Field i :& Field i :& Field i :& Field i :&
+         Field i :& Field i :& Field i :& Field i :&
+         Field i :& Field i :& Field i :& Field 99 :&
+         RNil
+
+sumRec :: Rec ElField Fields -> Int
+sumRec str =
+    get #a0 str + get #a1 str + get #a2 str + get #a3 str + get #a4 str
+  + get #a5 str + get #a6 str + get #a7 str + get #a8 str
+  + get #a9 str + get #a10 str + get #a11 str + get #a12 str
+  + get #a13 str + get #a14 str + get #a15 str
+  where
+    get (_label :: Label s) r =
+      let (Field v) = rget @'(s, _) r
+      in v
+    {-# INLINE get #-}
diff --git a/benchmarks/Bench/SRec.hs b/benchmarks/Bench/SRec.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/Bench/SRec.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE OverloadedLabels      #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+
+module Bench.SRec where
+
+import Data.Vinyl.SRec
+import Data.Vinyl
+
+import Bench.Rec (Fields)
+
+
+mkToSRec :: Int -> SRec ElField Fields
+mkToSRec i= toSRec (Field i :& Field i :& Field i :& Field i :&
+                  Field i :& Field i :& Field i :& Field i :&
+                  Field i :& Field i :& Field i :& Field i :&
+                  Field i :& Field i :& Field i :& Field 99 :&
+                  RNil)
+
+
+sumSRec :: SRec ElField Fields -> Int
+sumSRec str =
+    get #a0 str + get #a1 str + get #a2 str + get #a3 str + get #a4 str
+  + get #a5 str + get #a6 str + get #a7 str + get #a8 str
+  + get #a9 str + get #a10 str + get #a11 str + get #a12 str
+  + get #a13 str + get #a14 str + get #a15 str
+  where
+    get (label :: Label s) r =
+      case rget @'(s, Int) r of
+        Field v -> v
+    {-# INLINE get #-}
diff --git a/tests/Aeson.hs b/tests/Aeson.hs
--- a/tests/Aeson.hs
+++ b/tests/Aeson.hs
@@ -33,6 +33,7 @@
 -- 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.
+module Main where
 import Control.Lens (view, deep)
 import Control.Monad.State.Strict
 import qualified Data.HashMap.Strict as H
@@ -47,11 +48,42 @@
 import Data.Vinyl.Functor (Compose(..), (:.), Identity(..), Const(..))
 import Data.Aeson
 import Data.Aeson.Encoding.Internal (wrapObject, pair)
+#if MIN_VERSION_aeson(2,0,0)
+import Control.Lens (_1, (%~))
+import qualified Data.Aeson.Key as Key
+import qualified Data.Aeson.KeyMap as KeyMap
+#endif
 import Data.Aeson.Lens (_Object)
 import GHC.Generics (Generic, Rep)
 import GHC.TypeLits (KnownSymbol)
 import Test.Hspec
 
+-- * Compatibility with aeson < 2
+#if MIN_VERSION_aeson(2,0,0)
+type KeyMap = KeyMap.KeyMap Value
+
+keyFromString :: String -> Key
+keyFromString = Key.fromString
+
+keyFromText :: Text -> Key
+keyFromText = Key.fromText
+
+keyMapToList :: KeyMap -> [(Key,Value)]
+keyMapToList = KeyMap.toList
+#else
+type Key = Text
+type KeyMap = H.HashMap Text Value
+
+keyFromString :: String -> Key
+keyFromString = T.pack
+
+keyFromText :: Text -> Key
+keyFromText = id
+
+keyMapToList :: KeyMap -> [(Key,Value)]
+keyMapToList = H.toList
+#endif
+
 -- * Implementing 'ToJSON' for 'Rec'
 
 -- | An 'Identity' functor is not reflected in a value's JSON
@@ -61,23 +93,23 @@
 
 -- | 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))]
+instance (KnownSymbol s, ToJSON a) => ToJSON (ElField '(s,a)) where
+  toJSON x = object [(keyFromString (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)]
+  toJSON (Compose (name, x)) = object [(keyFromText 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
+             => Rec f rs -> Rec (Maybe :. Const (Key,Value)) rs
 fieldsToJSON = rmapMethod1 @ToJSON (Compose . aux)
   where aux x = case toJSON x of
-                  Object (H.toList -> [field]) -> Just (Const field)
+                  Object (keyMapToList -> [field]) -> Just (Const field)
                   _ -> Nothing
 
 -- | Convert a homogeneous record to a list factored through an outer
@@ -175,19 +207,21 @@
 -- loses precision in the type.
 class ToJSONField a where
   encodeJSONField :: a -> Series
-  toJSONField :: a -> (Text,Value)
+  toJSONField :: a -> (Key,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))
+  encodeJSONField x = pair (keyFromString (getLabel x))
+                           (toEncoding (getField x))
+  toJSONField x = (keyFromString (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)
+  encodeJSONField (Compose (name,val)) =
+    pair (keyFromText name) (toEncoding val)
+  toJSONField (Compose (name,val)) = (keyFromText name, toJSON val)
 
 encodeRec :: (RFoldMap rs, RecMapMethod1 ToJSONField f rs)
           => Rec f rs -> Encoding
@@ -206,7 +240,7 @@
 
 -- | 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 :: Value -> Maybe Object
 allAesonFields (Array arr) =
   case V.toList arr of
     [] -> Just mempty
@@ -223,8 +257,19 @@
 
 -- | A lens implementation of something a bit looser than
 -- 'unnestFields'.
-allFields :: Value -> H.HashMap Text Value
+allFields :: Value -> Object
+#if MIN_VERSION_aeson(2,0,0)
+allFields = KeyMap.fromList
+#if MIN_VERSION_lens_aeson(1,2,0)
+          . keyMapToList
+#else
+          . map (_1 %~ Key.fromText)
+          . H.toList
+#endif
+          . view (deep _Object)
+#else
 allFields = view (deep _Object)
+#endif
 
 -- | The generic 'ToJSON' instance is not quite right since we use the
 -- record's interpretation type constructor to define serialization,
diff --git a/tests/Intro.lhs b/tests/Intro.lhs
deleted file mode 100644
--- a/tests/Intro.lhs
+++ /dev/null
@@ -1,286 +0,0 @@
-This introduction was originally published at
-<http://www.jonmsterling.com/posts/2013-04-06-vinyl-modern-records-for-haskell.html>
-
-Vinyl: Modern Records for Haskell
-=================================
-
-Vinyl is a general solution to the records problem in Haskell using
-type level strings and other modern GHC features, featuring static
-structural typing (with a subtyping relation), and automatic
-row-polymorphic lenses. All this is possible without Template Haskell.
-
-First, install Vinyl from Hackage:
-
-< cabal update
-< cabal install vinyl singletons
-
-Let’s work through a quick example. We’ll need to enable some language
-extensions first:
-
-> {-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
-> {-# LANGUAGE FlexibleContexts, FlexibleInstances, NoMonomorphismRestriction #-}
-> {-# LANGUAGE GADTs, TypeSynonymInstances, TemplateHaskell, StandaloneDeriving #-}
-> {-# LANGUAGE TypeApplications #-}
-> module Intro where
-> import Data.Vinyl
-> import Data.Vinyl.Functor
-> import Control.Lens hiding (Identity)
-> import Data.Char
-> import Test.DocTest
-> import Data.Singletons.TH (genSingletons)
-
-Let’s define a universe of fields which we want to use.
-
-First of all, we need a data type defining the field labels:
-
-> data Fields = Name | Age | Sleeping | Master deriving Show
-
-Any record can be now described by a type-level list of these labels.
-The `DataKinds` extension must be enabled to automatically turn all the
-constructors of the `Field` type into types.
-
-> type LifeForm = [Name, Age, Sleeping]
-
-Now, we need a way to map our labels to concrete types. We use a type
-family for this purpose:
-
-> type family ElF (f :: Fields) :: * where
->   ElF Name = String
->   ElF Age = Int
->   ElF Sleeping = Bool
->   ElF Master = Rec Attr LifeForm
-
-Unfortunately, type families aren't first class in Haskell.  That's
-why we also need a data type, with which we will parametrise `Rec`:
-
-> newtype Attr f = Attr { _unAttr :: ElF f }
-> makeLenses ''Attr
-> instance Show (Attr Name) where show (Attr x) = "name: " ++ show x
-> instance Show (Attr Age) where show (Attr x) = "age: " ++ show x
-> instance Show (Attr Sleeping) where show (Attr x) = "sleeping: " ++ show x
-> instance Show (Attr Master) where show (Attr x) = "master: " ++ show x
-
-To make field construction easier, we define an operator.  The first
-argument of this operator is a singleton - a constructor bringing the
-data-kinded field label type into the data level.  It's needed because
-there can be multiple labels with the same field type, so by just
-supplying a value of type `ElF f` there would be no way to deduce the
-correct `f`.
-
-> (=::) :: sing f -> ElF f -> Attr f
-> _ =:: x = Attr x
-
-We generate the necessary singletons for each field label using
-Template Haskell:
-
-> genSingletons [ ''Fields ]
-
-Now, let’s try to make an entity that represents a human:
-
-> jon = (SName =:: "jon")
->    :& (SAge =:: 23)
->    :& (SSleeping =:: False)
->    :& RNil
-
-Automatically, we can show the record:
-
-> -- |
-> -- >>> show jon
-> -- "{name: \"jon\", age: 23, sleeping: False}"
-
-And its types are all inferred with no problem. Now, make a dog! Dogs
-are life-forms, but unlike humans, they have masters. So, let’s build
-my dog:
-
-> tucker = (SName =:: "tucker")
->       :& (SAge =:: 9)
->       :& (SSleeping =:: True)
->       :& (SMaster =:: jon)
->       :& RNil
-
-Using Lenses
-------------
-
-Now, if we want to wake entities up, we don’t want to have to write a
-separate wake-up function for both dogs and humans (even though they
-are of different type). Luckily, we can use the built-in lenses to
-focus on a particular field in the record for access and update,
-without losing additional information:
-
-
-> wakeUp :: (Sleeping ∈ fields) => Rec Attr fields -> Rec Attr fields
-> wakeUp = rput $ SSleeping =:: False
-
-Now, the type annotation on `wakeUp` was not necessary; I just wanted
-to show how intuitive the type is. Basically, it takes as an input
-any record that has a `Bool` field labelled `sleeping`, and modifies
-that specific field in the record accordingly.
-
-> tucker' = wakeUp tucker
-> jon' = wakeUp jon
-
-> -- |
-> -- >>> :set -XTypeApplications -XDataKinds
-> -- >>> tucker' ^. rlens @Sleeping
-> -- sleeping: False
-> --
-> -- >>> tucker ^. rlens @Sleeping
-> -- sleeping: True
-> --
-> -- >>> jon' ^. rlens @Sleeping
-> -- sleeping: False
-
-We can also access the entire lens for a field using the rLens
-function; since lenses are composable, it’s super easy to do deep
-update on a record:
-
-> masterSleeping = rlens @Master . unAttr . rlens @Sleeping
-> tucker'' = masterSleeping .~ (SSleeping =:: True) $ tucker'
-
-> -- | >>> tucker'' ^. masterSleeping
-> -- sleeping: True
-
-Subtyping Relation and Coercion
--------------------------------
-
-A record `Rec f xs` is a subtype of a record `Rec f ys` if `ys ⊆ xs`;
-that is to say, if one record can do everything that another record
-can, the former is a subtype of the latter. As such, we should be able
-to provide an upcast operator which “forgets” whatever makes one
-record different from another (whether it be extra data, or different
-order).
-
-Therefore, the following works:
-
-> upcastedTucker :: Rec Attr LifeForm
-> upcastedTucker = rcast tucker
-
-The subtyping relationship between record types is expressed with the
-`(<:)` constraint; so, `rcast` is of the following type:
-
-< rcast :: r1 <: r2 => Rec f r1 -> Rec f r2
-
-Also provided is a `(≅)` constraint which indicates record congruence
-(that is, two record types differ only in the order of their fields).
-
-In fact, `rcast` is actually given as a special case of the lens `rsubset`,
-which lets you modify entire (possibly non-contiguous) slices of a record!
-
-Records are polymorphic over functors
--------------------------------------
-
-Consider the following declaration:
-
-< data Rec :: (u -> *) -> [u] -> * where
-<   RNil :: Rec f '[]
-<   (:&) :: f r -> Rec f rs -> Rec f (r ': rs)
-
-Records are implicitly parameterized over a kind `u`, which stands for the
-"universe" or key space. Keys (inhabitants of `u`) are then interpreted into
-the types of their values by the first parameter to `Rec`, `f`. An extremely
-powerful aspect of Vinyl records is that you can construct natural
-transformations between different interpretation functors `f,g`, or postcompose
-some other functor onto the stack. This can be used to immerse each field of a
-record in some particular effect modality, and then the library functions can
-be used to traverse and accumulate these effects.
-
-Let’s imagine that we want to do validation on a record that
-represents a name and an age:
-
-> type Person = [Name, Age]
-
-We’ve decided that names must be alphabetic, and ages must be positive. For
-validation, we’ll use `Maybe` for now, though you should use a
-left-accumulating `Validation` type.
-
-> goodPerson :: Rec Attr Person
-> goodPerson = (SName =:: "Jon")
->           :& (SAge =:: 20)
->           :& RNil
-
-> badPerson = (SName =:: "J#@#$on")
->           :& (SAge =:: 20)
->           :& RNil
-
-We'll give validation a (rather poor) shot.
-
-> validatePerson :: Rec Attr Person -> Maybe (Rec Attr Person)
-> validatePerson p = (\n a -> (SName =:: n) :& (SAge =:: a) :& RNil) <$> vName <*> vAge where
->   vName = validateName $ p ^. rlens @'Name . unAttr
->   vAge  = validateAge $ p ^. rlens @'Age . unAttr
->
->   validateName str | all isAlpha str = Just str
->   validateName _ = Nothing
->   validateAge i | i >= 0 = Just i
->   validateAge _ = Nothing
-
-> -- $setup
-> -- >>> let isJust (Just _) = True; isJust _ = False
-
-> -- |
-> -- >>> isJust $ validatePerson goodPerson
-> -- True
-> --
-> -- >>> isJust $ validatePerson badPerson
-> -- False
-
-The results are as expected (`Just` for `goodPerson`, and a `Nothing` for
-`badPerson`); but this was not very fun to build.
-
-Further, it would be nice to have some notion of a partial record;
-that is, if part of it can’t be validated, it would still be nice to
-be able to access the rest. What if we could make a version of this
-record where the elements themselves were validation functions, and
-then that record could be applied to a plain one, to get a record of
-validated fields? That’s what we’re going to do.
-
-> type Validator f = Lift (->) f (Maybe :. f)
-
-Let’s parameterize a record by it: when we do, then an element of type
-`a` should be a function `Identity a -> Result e a`:
-
-> vperson :: Rec (Validator Attr) Person
-> vperson = lift validateName :& lift validateAge :& RNil
->   where
->     lift f = Lift $ Compose . f
->     validateName (Attr str) | all isAlpha str = Just (Attr str)
->     validateName _ = Nothing
->     validateAge (Attr i) | i >= 0 = Just (Attr i)
->     validateAge _ = Nothing
-
-And we can use the special application operator `<<*>>` (which is
-analogous to `<*>`, but generalized a bit) to use this to validate a
-record:
-
-> goodPersonResult = vperson <<*>> goodPerson
-> badPersonResult  = vperson <<*>> badPerson
-
-> -- |
-> -- >>> :set -XTypeApplications -XDataKinds
-> -- >>> isJust . getCompose $ goodPersonResult ^. rlens @Name
-> -- True
-> -- >>> isJust . getCompose $ goodPersonResult ^. rlens @Age
-> -- True
-> -- >>> isJust . getCompose $ badPersonResult ^. rlens @Name
-> -- False
-> -- >>> isJust . getCompose $ badPersonResult ^. rlens @Age
-> -- True
-
-
-So now we have a partial record, and we can still do stuff with its contents.
-Next, we can even recover the original behavior of the validator (that is, to
-give us a value of type `Maybe (Rec Attr Person)`) using `rtraverse`:
-
-> mgoodPerson :: Maybe (Rec Attr Person)
-> mgoodPerson = rtraverse getCompose goodPersonResult
-
-> mbadPerson  = rtraverse getCompose badPersonResult
-
-> -- |
-> -- >>> isJust mgoodPerson
-> -- True
-> -- >>> isJust mbadPerson
-> -- False
-
-> main :: IO ()
-> main = doctest ["tests/Intro.lhs", "Data/Vinyl/Tutorial/Overview.hs"]
diff --git a/tests/Spec.hs b/tests/Spec.hs
--- a/tests/Spec.hs
+++ b/tests/Spec.hs
@@ -11,6 +11,8 @@
 import qualified CoRecSpec as C
 import qualified XRecSpec as X
 
+import qualified Test.ARec as ARec
+
 -- d1 :: FieldRec '[ '("X",String), '("Y", String) ]
 -- d1 = Field @"X" "5" :& Field @"Y" "Hi" :& RNil
 
@@ -71,3 +73,5 @@
       (#x .~ 2.1) d3 `shouldBe` fieldRec (#x =: 2.1, #y =: "Hi")
     it "Can change a field's type" $
       (d3 & #y %~ length) `shouldBe` fieldRec (#x =: 5, #y =: 2)
+
+  ARec.spec
diff --git a/tests/Test/ARec.hs b/tests/Test/ARec.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/ARec.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, GADTs,
+             NoMonomorphismRestriction, OverloadedLabels,
+             ScopedTypeVariables, TypeApplications, TypeOperators #-}
+{-# OPTIONS_GHC -Wall -Wno-type-defaults #-}
+
+module Test.ARec where
+
+import Data.Vinyl.ARec
+import Data.Vinyl
+import Test.Hspec
+
+import Data.Vinyl.Syntax ()
+
+type FullARec = ARec ElField '[ "f0" ::: Int , "f1" ::: Bool , "f2" ::: String
+                              , "f3" ::: Double, "f4" ::: Integer
+                              , "f2" ::: Int -- intentionally duplicate field name
+                              ]
+
+type SubARecPre = ARec ElField '[ "f0" ::: Int , "f1" ::: Bool , "f2" ::: String ]
+
+type SubARecDupes = ARec ElField '[ "f2" ::: String, "f2" ::: String
+                                  , "f2" ::: Int, "f2" ::: String
+                                  ]
+
+
+fullARec :: FullARec
+fullARec = toARec ( #f0 =: 1 :& #f1 =: False :& #f2 =: "field2"
+                  :& #f3 =: 3.1415 :& #f4 =: 4444
+                  :& #f2 =: 666
+                  :& RNil
+                  )
+
+-- For arecGetSubset -----------------------------------------------------------
+
+subARecPre :: SubARecPre
+subARecPre = toARec ( #f0 =: 1 :& #f1 =: False :& #f2 =: "field2" :&  RNil)
+
+subARecDupes :: SubARecDupes
+subARecDupes = toARec ( #f2 =: "field2" :& #f2 =: "field2"
+                        :& #f2 =: 666 :& #f2 =: "field2"
+                        :& RNil
+                      )
+
+arecWithDupes :: ARec ElField '[ "f" ::: Int, "f" ::: Int]
+arecWithDupes = toARec (#f =: 1 :& #f =: 2 :& RNil)
+
+-- For arecSetSubset -----------------------------------------------------------
+
+subARecPreSet :: SubARecPre
+subARecPreSet = toARec ( #f0 =: 11 :& #f1 =: True :& #f2 =: "field2-updated" :&  RNil)
+
+fullARecUpdated :: FullARec
+fullARecUpdated = toARec ( #f0 =: 11 :& #f1 =: True :& #f2 =: "field2-updated"
+                           :& #f3 =: 3.1415 :& #f4 =: 4444
+                           :& #f2 =: 666
+                           :& RNil
+                         )
+
+updateARecWithDupes :: ARec ElField '[ '("f0", Int), '("f0", Int), '("f0", Int)]
+updateARecWithDupes = toARec (#f0 =: 3 :& #f0 =: 66 :& #f0 =: 1 :&RNil)
+
+subARecDupesUpdated :: SubARecDupes
+subARecDupesUpdated = toARec ( #f2 =: "updated" :& #f2 =: "field2"
+                               :& #f2 =: 666 :& #f2 =: "field2"
+                               :& RNil
+                             )
+
+
+
+spec :: SpecWith ()
+spec = describe "ARec" $ do
+  describe "arecGetSubset" $ do
+    it "retrieves a prefix ARec" $
+      -- The part to be retrieved is type-directed
+      arecGetSubset fullARec `shouldBe` subARecPre
+    it "retrieves the full ARec" $ do
+      -- Should catch off-by-one errors that lead to overflow
+      arecGetSubset fullARec `shouldBe` fullARec
+    it "handles an empty subARec correctly" $
+      arecGetSubset fullARec `shouldBe` toARec RNil
+    it "handles duplicate field names correctly in the sub arec" $
+      arecGetSubset fullARec `shouldBe` subARecDupes
+    it "handles duplicate field names correctly in the source arec" $
+      -- When both the name and the type of the field match we retrieve from the
+      -- first field
+      arecGetSubset arecWithDupes `shouldBe` toARec (#f =: (1 :: Int) :& RNil)
+  describe "arecSetSubset" $ do
+    it "sets a subset of fields" $ do
+      arecSetSubset fullARec subARecPreSet `shouldBe` fullARecUpdated
+    it "handles updates to every field" $ do
+      -- Should catch off-by-one errors that lead to overflow
+      arecSetSubset fullARec fullARec `shouldBe` fullARec
+    it "handles an empty subset" $ do
+      arecSetSubset fullARec (toARec RNil) `shouldBe` fullARec
+    it "handles duplicates in the updating ARec" $ do
+      -- The behaviour here should be that the _last_ updating field prevails
+      arecSetSubset fullARec updateARecWithDupes `shouldBe` fullARec
+    it "handles updatees with duplicate fields" $ do
+      -- Here, only the _first_ field should be updated
+      arecSetSubset subARecDupes (toARec (#f2 =: "updated" :& RNil))
+        `shouldBe` subARecDupesUpdated
diff --git a/tests/doctests.hs b/tests/doctests.hs
deleted file mode 100644
--- a/tests/doctests.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-import Test.DocTest
-
-main :: IO ()
-main = doctest [ "tests/Intro.lhs"
-               , "Data/Vinyl/Functor.hs"
-               , "Data/Vinyl/Curry.hs" ]
diff --git a/vinyl.cabal b/vinyl.cabal
--- a/vinyl.cabal
+++ b/vinyl.cabal
@@ -1,5 +1,5 @@
 name:                vinyl
-version:             0.11.0
+version:             0.14.3
 synopsis:            Extensible Records
 -- description:
 license:             MIT
@@ -12,7 +12,7 @@
 build-type:          Simple
 cabal-version:       >=1.10
 extra-source-files:  CHANGELOG.md
-tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.2
+tested-with:         GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4, GHC == 8.10.4, GHC == 9.0.1, GHC == 9.2.1
 
 description: Extensible records for Haskell with lenses.
 
@@ -23,6 +23,8 @@
 library
   exposed-modules:     Data.Vinyl
                      , Data.Vinyl.ARec
+                     , Data.Vinyl.ARec.Internal
+                     , Data.Vinyl.ARec.Internal.SmallArray
                      , Data.Vinyl.Class.Method
                      , Data.Vinyl.Core
                      , Data.Vinyl.CoRec
@@ -38,9 +40,12 @@
                      , Data.Vinyl.Syntax
                      , Data.Vinyl.Tutorial.Overview
                      , Data.Vinyl.XRec
-  build-depends:       base >=4.7 && <= 5,
+  build-depends:       base >= 4.11 && <= 5,
                        ghc-prim,
+                       deepseq,
                        array
+  if impl (ghc < 8.6.0)
+    build-depends: constraints >= 0.6.1
   default-language:    Haskell2010
   ghc-options:         -Wall
   other-extensions:    TypeApplications
@@ -49,7 +54,7 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          StorableBench.hs
-  build-depends:    base >= 4.7 && <= 5,
+  build-depends:    base,
                     vector,
                     criterion,
                     vinyl,
@@ -65,7 +70,7 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          EqualityBench.hs
-  build-depends:    base >= 4.7 && <= 5, criterion, vinyl
+  build-depends:    base, criterion, vinyl
   ghc-options:      -O2
   default-language: Haskell2010
 
@@ -73,7 +78,10 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          AccessorsBench.hs
-  build-depends:    base >= 4.7 && <= 5, criterion, tagged, vinyl, microlens
+  build-depends:    base, criterion, tagged, vinyl, microlens
+  other-modules:    Bench.ARec
+                    Bench.SRec
+                    Bench.Rec
   ghc-options:      -O2
   default-language: Haskell2010
 
@@ -81,23 +89,27 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          AsABench.hs
-  build-depends:    base >= 4.7 && <= 5, criterion, vinyl
+  build-depends:    base, 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
+-- TODO: Use cabal-docspec
+-- test-suite doctests
+--   type:             exitcode-stdio-1.0
+--   hs-source-dirs:   tests
+--   other-modules:    Intro
+--   main-is:          doctests.hs
+--   if impl (ghc < 9.0.1)
+--     build-depends:    base, lens, doctest >= 0.8, singletons >= 0.10 && < 3, vinyl
+--   else
+--     build-depends:    base, lens, doctest >= 0.8, singletons-th >= 3 && < 3.1, 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,
+  build-depends:    base, hspec, aeson >= 1.4, text, mtl, vinyl,
                     vector, unordered-containers, lens, lens-aeson
   default-language: Haskell2010
 
@@ -105,11 +117,13 @@
   type:                exitcode-stdio-1.0
   hs-source-dirs:      tests
   main-is:             Spec.hs
-  other-modules:       CoRecSpec XRecSpec
+  other-modules:       CoRecSpec
+                       XRecSpec
+                       Test.ARec
   build-depends:       base
                      , vinyl
                      , microlens
-                     , hspec >= 2.2.4 && < 2.7
+                     , hspec
                      , should-not-typecheck >= 2.0 && < 2.2
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N
   default-language:    Haskell2010