diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,6 @@
+# 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.
 
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,21 @@
-{-# 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
+  , fromARec
+  , aget
+  , aput
+  , alens
+  , 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,193 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# 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.
+module Data.Vinyl.ARec.Internal
+  ( ARec (..)
+  , IndexableField
+  , toARec
+  , fromARec
+  , aget
+  , aput
+  , alens
+  , arecGetSubset
+  , arecSetSubset
+  , arecRepsMatchCoercion
+  , arecConsMatchCoercion
+  ) 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
+#if __GLASGOW_HASKELL__ < 806
+import Data.Constraint.Forall (Forall)
+#endif
+import Data.Coerce (Coercible)
+import Data.Type.Coercion (Coercion (..))
+
+-- | An array-backed extensible record with constant-time field
+-- access.
+newtype ARec (f :: k -> *) (ts :: [k]) = ARec (Array.Array Int Any)
+type role ARec representational nominal
+
+-- | 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 = 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 = 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
+
+{-
+-- 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
+-}
+
+-- | 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)
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,6 +34,7 @@
 -- 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
@@ -46,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
@@ -397,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/SRec.hs b/Data/Vinyl/SRec.hs
--- a/Data/Vinyl/SRec.hs
+++ b/Data/Vinyl/SRec.hs
@@ -75,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(..))
 
diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs
--- a/Data/Vinyl/TypeLevel.hs
+++ b/Data/Vinyl/TypeLevel.hs
@@ -21,12 +21,8 @@
 
 module Data.Vinyl.TypeLevel where
 
-#if __GLASGOW_HASKELL__ < 806
+import Data.Coerce
 import Data.Kind
-#else
-import GHC.Exts
-#endif
-import GHC.Types (Type)
 
 -- | A mere approximation of the natural numbers. And their image as lifted by
 -- @-XDataKinds@ corresponds to the actual natural numbers.
@@ -126,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/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
diff --git a/tests/doctests.hs b/tests/doctests.hs
--- a/tests/doctests.hs
+++ b/tests/doctests.hs
@@ -1,6 +1,14 @@
+{-# language CPP #-}
 import Test.DocTest
 
 main :: IO ()
-main = doctest [ "tests/Intro.lhs"
+main = doctest [ "-package lens"
+               , "-package doctest"
+#if __GLASGOW_HASKELL__ >= 900            
+               , "-package singletons-th"
+#else
+               , "-package singletons"
+#endif
+               , "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.13.0
+version:             0.13.1
 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.4.4, GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.1
+tested-with:         GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4, GHC == 8.10.4, GHC == 9.0.1
 
 description: Extensible records for Haskell with lenses.
 
@@ -23,6 +23,7 @@
 library
   exposed-modules:     Data.Vinyl
                      , Data.Vinyl.ARec
+                     , Data.Vinyl.ARec.Internal
                      , Data.Vinyl.Class.Method
                      , Data.Vinyl.Core
                      , Data.Vinyl.CoRec
@@ -40,7 +41,10 @@
                      , Data.Vinyl.XRec
   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
@@ -90,7 +94,10 @@
   hs-source-dirs:   tests
   other-modules:    Intro
   main-is:          doctests.hs
-  build-depends:    base, lens, doctest >= 0.8, singletons >= 0.10, vinyl
+  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