diff --git a/Data/Vinyl/CoRec.hs b/Data/Vinyl/CoRec.hs
index 6a47b15..ce85ad4 100644
--- a/Data/Vinyl/CoRec.hs
+++ b/Data/Vinyl/CoRec.hs
@@ -202,8 +202,12 @@ asA' f@(CoRec x)
 -- | Pattern match on a CoRec by specifying handlers for each case. Note that
 -- the order of the Handlers has to match the type level list (t:ts).
 --
+-- >>> :set -XDataKinds
+-- >>> import Data.Vinyl.Core ( Rec((:&), RNil))
+-- >>> import Data.Vinyl.Functor (Identity(Identity))
+-- >>> import Data.Vinyl.CoRec (CoRec(CoRec), match, Handler(H))
 -- >>> :{
--- let testCoRec = Col (Identity False) :: CoRec Identity [Int, String, Bool] in
+-- let testCoRec = CoRec (Identity False) :: CoRec Identity [Int, String, Bool] in
 -- match testCoRec $
 --       (H $ \i -> "my Int is the successor of " ++ show (i - 1))
 --    :& (H $ \s -> "my String is: " ++ s)
diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs
index 9ca3cdc..20057e5 100644
--- a/Data/Vinyl/Core.hs
+++ b/Data/Vinyl/Core.hs
@@ -57,10 +57,32 @@ import Control.DeepSeq (NFData, rnf)
 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
--- inhabitants of the kind @u@; the type of values at any label @r :: u@ is
--- given by its interpretation @f r :: *@.
+{- |
+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
+inhabitants of the kind @u@; the type of values at any label @r :: u@ is
+given by its interpretation @f r :: *@.
+
+>>> :set -XDataKinds
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> testRec = Identity 3 :& Identity "Hi" :& RNil
+>>> :t testRec
+testRec :: Num r => Rec Identity '[r, [Char]]
+>>> testRec :: Rec Identity '[Int, String]
+{3, "Hi"}
+
+>>> testRec = Just 3 :& Nothing :& Just "Hi" :& RNil
+>>> :t testRec
+testRec :: Num r1 => Rec Maybe '[r1, r2, [Char]]
+
+>>> :set -XTypeApplications
+>>> import Data.Vinyl.Functor (ElField(Field))
+>>> testRec = Field @'("name", String) "Alice" :& Field @'("age", Int) 20 :& RNil
+>>> :t testRec
+testRec :: Rec ElField '[ '("name", String), '("age", Int)]
+>>> testRec
+{name :-> "Alice", age :-> 20}
+-}
 data Rec :: (u -> *) -> [u] -> * where
   RNil :: Rec f '[]
   (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
@@ -86,7 +108,16 @@ instance TestCoercion f => TestCoercion (Rec f) where
     Just Coercion
   testCoercion _ _ = Nothing
 
--- | Two records may be pasted together.
+{- |
+Two records may be pasted together.
+
+>>> :set -XScopedTypeVariables
+>>> testRec1 :: Rec Maybe '[Int, String] = Just 3 :& Just "Hi" :& RNil
+>>> testRec2 :: Rec Maybe '[Double, [Double]] = Nothing :& Just [3.0, 2.2] :& RNil
+>>> appendedTestRec = rappend testRec1 testRec2
+>>> :t appendedTestRec
+appendedTestRec :: Rec Maybe '[Int, [Char], Double, [Double]]
+-}
 rappend
   :: Rec f as
   -> Rec f bs
@@ -94,18 +125,53 @@ rappend
 rappend RNil ys = ys
 rappend (x :& xs) ys = x :& (xs `rappend` ys)
 
--- | A shorthand for 'rappend'.
+{- |
+A shorthand for 'rappend'.
+
+>>> :set -XScopedTypeVariables
+>>> testRec1 :: Rec Maybe '[Int, String] = Just 3 :& Just "Hi" :& RNil
+>>> testRec2 :: Rec Maybe '[Double, [Double]] = Nothing :& Just [3.0, 2.2] :& RNil
+>>> appendedTestRecs = testRec1 <+> testRec2
+>>> :t appendedTestRecs
+appendedTestRecs :: Rec Maybe '[Int, [Char], Double, [Double]]
+-}
 (<+>)
   :: Rec f as
   -> Rec f bs
   -> Rec f (as ++ bs)
 (<+>) = rappend
 
--- | Combine two records by combining their fields using the given
--- function. The first argument is a binary operation for combining
--- two values (e.g. '(<>)'), the second argument takes a record field
--- into the type equipped with the desired operation, the third
--- argument takes the combined value back to a result type.
+{- | Combine two records by combining their fields using the given
+function. The first argument is a binary operation for combining
+two values (e.g. '(<>)'), the second argument takes a record field
+into the type equipped with the desired operation, the third
+argument takes the combined value back to a result type.
+
+This function makes no assumption on the types stored in the record and is thus
+limited to basic operations that can be executed on all types (as defined via
+the unconstrained forall a in arguments 1,2 and 3). The
+following snippet shows how to put each entry of a Rec Maybe in a list
+(second argument), concatenating them (first argument), and then outputting a
+Rec [] instead of a Rec Maybe—something which can be done for any type:
+
+>>> import Data.Maybe (maybeToList)
+>>> combineAsList = rcombine (<>) maybeToList id
+
+>>> testRec1 :: Rec Maybe '[String, String] = Just "Ho" :& Just "Hi" :& RNil
+>>> combineAsList testRec1 testRec1
+{["Ho","Ho"], ["Hi","Hi"]}
+
+We can't combine testRec1 with rcombine such that the Strings would be
+concatenated directly because that would make assumptions on the types and
+violate the unconstrained forall a. However, we can use combineAsList now on
+any other Rec Maybe as well.
+
+>>> testRec2 :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>> combineAsList testRec2 testRec2
+{["Ho","Ho"], [3.0,3.0], []}
+
+-}
+
 rcombine :: (RMap rs, RApply rs)
          => (forall a. m a -> m a -> m a)
          -> (forall a. f a -> m a)
@@ -118,9 +184,22 @@ rcombine smash toM fromM x y =
   where x' = rmap toM x
         y' = rmap toM y
 
--- | 'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u ->
--- Hask@; that is, a natural transformation between two interpretation functors
--- @f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@.
+{- |
+'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u ->
+Hask@; that is, a natural transformation between two interpretation functors
+@f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@.
+
+Here is an example:
+
+>>> import Data.Maybe (maybeToList)
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>> rmap maybeToList testRec
+{["Ho"], [3.0], []}
+
+Similar to other functions in this module, we can not use rmap to map type
+specific functions over a record. Only functions that work for any type can be
+used.
+-}
 class RMap rs where
   rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs
 
@@ -132,7 +211,12 @@ instance RMap xs => RMap (x ': xs) where
   rmap f (x :& xs) = f x :& rmap f xs
   {-# INLINE rmap #-}
 
--- | A shorthand for 'rmap'.
+{- | A shorthand for 'rmap'.
+>>> import Data.Maybe (maybeToList)
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>> maybeToList <<$>> testRec
+{["Ho"], [3.0], []}
+-}
 (<<$>>)
   :: RMap rs
   => (forall x. f x -> g x)
@@ -141,7 +225,12 @@ instance RMap xs => RMap (x ': xs) where
 (<<$>>) = rmap
 {-# INLINE (<<$>>) #-}
 
--- | An inverted shorthand for 'rmap'.
+{- | An inverted shorthand for 'rmap'.
+>>> import Data.Maybe (maybeToList)
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>> testRec <<&>> maybeToList 
+{["Ho"], [3.0], []}
+-}
 (<<&>>)
   :: RMap rs
   => Rec f rs
@@ -150,8 +239,22 @@ instance RMap xs => RMap (x ': xs) where
 xs <<&>> f = rmap f xs
 {-# INLINE (<<&>>) #-}
 
--- | A record of components @f r -> g r@ may be applied to a record of @f@ to
--- get a record of @g@.
+{- |
+A record of components @f r -> g r@ may be applied to a record of @f@ to
+get a record of @g@.
+
+>>> import Data.Vinyl.Functor (Const(Const), Lift(Lift))
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>> :{
+funcRec = Lift (\x -> Const "String")
+  :& Lift (\x -> Const "Double")
+  :& Lift (\x -> Const "Int")
+  :& RNil
+:}
+
+>>> recordToList $ rapply funcRec testRec
+["String","Double","Int"]
+-}
 class RApply rs where
   rapply :: Rec (Lift (->) f g) rs
          -> Rec f rs
@@ -165,7 +268,21 @@ instance RApply xs => RApply (x ': xs) where
   rapply (f :& fs) (x :& xs) = getLift f x :& (fs `rapply` xs)
   {-# INLINE rapply #-}
 
--- | A shorthand for 'rapply'.
+{- |
+A shorthand for 'rapply'.
+
+>>> import Data.Vinyl.Functor (Const(Const), Lift(Lift))
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>> :{
+funcRec = Lift (\x -> Const "String")
+  :& Lift (\x -> Const "Double")
+  :& Lift (\x -> Const "Int")
+  :& RNil
+:}
+
+>>> recordToList $ funcRec <<*>> testRec
+["String","Double","Int"]
+-}
 (<<*>>)
   :: RApply rs
   => Rec (Lift (->) f g) rs
@@ -174,8 +291,23 @@ instance RApply xs => RApply (x ': xs) where
 (<<*>>) = rapply
 {-# INLINE (<<*>>) #-}
 
--- | Given a section of some functor, records in that functor of any size are
--- inhabited.
+{- |
+Given a section of some functor, records in that functor of any size are
+inhabited. Note that you need a value that can inhabit any type in the record.
+It is not possible, with this function, to derive a default with a type class
+method. Here are a few examples:
+
+>>> testRec :: Rec Maybe '[Double, String] = rpure Nothing
+>>> testRec
+{Nothing, Nothing}
+>>> testRec :: Rec [] '[Double, String] = rpure []
+>>> testRec
+{[], []}
+>>> import Data.Proxy (Proxy(Proxy))
+>>> testRec :: Rec Proxy '[Double, String] = rpure Proxy
+>>> testRec
+{Proxy, Proxy}
+-}
 class RecApplicative rs where
   rpure
     :: (forall x. f x)
@@ -187,9 +319,57 @@ instance RecApplicative rs => RecApplicative (r ': rs) where
   rpure s = s :& rpure s
   {-# INLINE rpure #-}
 
--- | A record may be traversed with respect to its interpretation functor. This
--- can be used to yank (some or all) effects from the fields of the record to
--- the outside of the record.
+{- |
+A record may be traversed with respect to its interpretation functor. This
+can be used to yank (some or all) effects from the fields of the record to
+the outside of the record.
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>>
+:{
+ext :: Maybe x -> Maybe (Identity x)
+ext (Just x) = Just (Identity x)
+ext Nothing = Nothing
+:}
+>>> rtraverse ext testRec
+Nothing
+
+Here is another interesting example that allows reading a record
+interactively.
+
+>>> :set -XTypeOperators
+>>> import Text.Read (readMaybe)
+>>> import Data.Vinyl.Functor ((:.), Compose(Compose), getCompose)
+>>>
+:{
+readMaybeIO :: forall a. Read a => (IO :. Maybe) a
+readMaybeIO = Compose $ readMaybe <$> getLine
+testRec :: Rec (IO :. Maybe) [String, Double, Int]
+testRec = rpureConstrained @Read readMaybeIO
+:}
+>>> :t rtraverse getCompose testRec
+rtraverse getCompose testRec
+  :: IO (Rec Maybe '[String, Double, Int])
+
+And one more with State
+
+>>> :set -package mtl
+>>> import Control.Monad.State (StateT(StateT), runState, State, state)
+>>> import qualified Data.Vinyl.Functor as V
+>>> import qualified Data.Functor.Identity as I
+>>> testRec1 :: Rec (State Int) '[Int, Double] = state (\s -> (s, 2 * s)) :& state (\s -> (fromIntegral s, 3 * s)) :& RNil
+>>>
+:{
+ext :: State Int a -> State Int (V.Identity a)
+ext (StateT f) = StateT $ \s -> let (a, s') = I.runIdentity (f s) in I.Identity (V.Identity a, s')
+:}
+>>> stateRec = rtraverse ext testRec1
+>>> runState stateRec 1
+({1, 2.0},6)
+>>> runState (sequence $ replicate 5 stateRec) 1
+([{1, 2.0},{6, 12.0},{36, 72.0},{216, 432.0},{1296, 2592.0}],7776)
+-}
 rtraverse
   :: Applicative h
   => (forall x. f x -> h (g x))
@@ -199,13 +379,27 @@ rtraverse _ RNil      = pure RNil
 rtraverse f (x :& xs) = (:&) <$> f x <*> rtraverse f xs
 {-# INLINABLE rtraverse #-}
 
--- | While 'rtraverse' pulls the interpretation functor out of the
--- record, 'rtraverseIn' pushes the interpretation functor in to each
--- field type. This is particularly useful when you wish to discharge
--- that interpretation on a per-field basis. For instance, rather than
--- a @Rec IO '[a,b]@, you may wish to have a @Rec Identity '[IO a, IO
--- b]@ so that you can evaluate a single field to obtain a value of
--- type @Rec Identity '[a, IO b]@.
+{- |
+While 'rtraverse' pulls the interpretation functor out of the
+record, 'rtraverseIn' pushes the interpretation functor in to each
+field type. This is particularly useful when you wish to discharge
+that interpretation on a per-field basis. For instance, rather than
+a @Rec IO '[a,b]@, you may wish to have a @Rec Identity '[IO a, IO
+b]@ so that you can evaluate a single field to obtain a value of
+type @Rec Identity '[a, IO b]@.
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil
+>>>
+:{
+push :: forall x. Maybe x -> Identity (Maybe x)
+push (Just x) = Identity (Just x)
+push Nothing = Identity Nothing
+:}
+>>> :t rtraverseIn push testRec
+rtraverseIn push testRec
+  :: Rec Identity '[Maybe [Char], Maybe Double, Maybe Int]
+-}
 rtraverseIn :: forall h f g rs.
                (forall a. f a -> g (ApplyToField h a))
             -> Rec f rs
@@ -214,16 +408,45 @@ rtraverseIn _ RNil = RNil
 rtraverseIn f (x :& xs) = f x :& rtraverseIn f xs
 {-# INLINABLE rtraverseIn #-}
 
--- | Push an outer layer of interpretation functor into each field.
+{- |
+Push an outer layer of interpretation functor into each field.
+
+>>> :set -XTypeOperators
+>>> import Data.Vinyl.Functor ((:.), Identity(Identity), Compose(Compose))
+:{
+testRec :: Rec (Maybe :. Identity) '[ String, Double, Int] =
+    Compose (Just (Identity "Ho"))
+    :& Compose (Just (Identity 3.0))
+    :& Compose Nothing
+    :& RNil
+:}
+>>> :t rsequenceIn testRec
+rsequenceIn testRec
+  :: Rec Identity '[Maybe [Char], Maybe Double, Maybe Int]
+
+Note that this function can't be applied as easily to anything
+composed with interpretation functors as inner layer that take custom
+kinds as inputs. For example, when dealing with (Maybe :. ElField),
+Maybe the function can't be applied because that would require applying Maybe
+to a (Symbol, *) kind.
+-}
 rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g)
             => Rec (f :. g) rs -> Rec g (MapTyCon f rs)
 rsequenceIn = rtraverseIn @f (sequenceA . getCompose)
 {-# INLINABLE rsequenceIn #-}
 
--- | Given a natural transformation from the product of @f@ and @g@ to @h@, we
--- have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to
--- @'Rec' h@. You can also think about this operation as zipping two records
--- with the same element types but different interpretations.
+{- |
+Given a natural transformation from the product of @f@ and @g@ to @h@, we
+have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to
+@'Rec' h@. You can also think about this operation as zipping two records
+with the same element types but different interpretations.
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> testRec1 :: Rec Identity '[String, Double] = Identity "Joe" :& Identity 20.0 :& RNil
+>>> testRec2 :: Rec [] '[String, Double] = ["John"] :& [15.3] :& RNil
+>>> rzipWith (\(Identity a) xs -> a:xs) testRec1 testRec2
+{["Joe","John"], [20.0,15.3]}
+-}
 rzipWith :: (RMap xs, RApply xs)
          => (forall x. f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs
 rzipWith f = rapply . rmap (Lift . f)
@@ -244,6 +467,22 @@ instance RFoldMap xs => RFoldMap (x ': xs) where
   rfoldMapAux f m (r :& rs) = rfoldMapAux f (mappend m (f r)) rs
   {-# INLINE rfoldMapAux #-}
 
+{- |
+This function allows to collect all elements of a record in a monoid. The
+collector function can be specialized for a particular interpretation functor
+but has to be applicable for any type. It's therefore most useful to collect
+effects.
+
+>>> testRec1 :: Rec Maybe '[String, Double] = Just "Anna" :& Nothing :& RNil
+>>>
+:{
+func :: forall x. Maybe x -> String
+func (Just x) = "Just "
+func Nothing = "Nothing "
+:}
+>>> rfoldMap func testRec1
+"Just Nothing "
+-}
 rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs)
          => (forall x. f x -> m) -> Rec f rs -> m
 rfoldMap f = rfoldMapAux f mempty
@@ -261,18 +500,65 @@ instance RecordToList xs => RecordToList (x ': xs) where
   recordToList (x :& xs) = getConst x : recordToList xs
   {-# INLINE recordToList #-}
 
--- | Wrap up a value with a capability given by its type
+{- |
+Wrap up a value with a capability given by its type. In other words, the
+existance of a value x :: Dict c a proves the existence of an instance c a.
+This is useful to help the type checker realize that a value in a record does
+indeed have a certain instance.
+
+To understand better why this type is useful, consider the following function
+that doesn't typecheck:
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> import Data.Vinyl.TypeLevel (AllConstrained)
+>>>
+:{
+func :: forall rs. (RMap rs, AllConstrained Num rs) => Rec Identity rs -> Rec Identity rs
+func = rmap (\(Identity x) -> Identity (x+1))
+:}
+...
+    • Could not deduce (Num x) arising from a use of ‘+’
+      from the context: (RMap rs, AllConstrained Num rs)
+        bound by the type signature for:
+                   func :: forall (rs :: [*]).
+                           (RMap rs, AllConstrained Num rs) =>
+                           Rec Identity rs -> Rec Identity rs
+...
+
+Dict allows to encapsulate a constraint directly in the type such that anything
+wrapped in it automatically fullfils it. RMap understands that as well:
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>>
+:{
+func :: forall rs. RMap rs => Rec (Dict Num) rs -> Rec Identity rs
+func = rmap (\(Dict x) -> Identity (x + 1))
+:}
+>>> testRec :: Rec (Dict Num) '[Double, Int] = Dict 1.0 :& Dict 0 :& RNil
+>>> func testRec
+{2.0, 1}
+-}
 data Dict c a where
   Dict
     :: c a
     => a
     -> Dict c a
 
--- | Sometimes we may know something for /all/ fields of a record, but when
--- you expect to be able to /each/ of the fields, you are then out of luck.
--- Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly,
--- the constraint solver is not quite smart enough to realize this and we must
--- make it patently obvious by reifying the constraint pointwise with proof.
+{- |
+Sometimes we may know something for /all/ fields of a record, but when
+you expect to be able to /each/ of the fields, you are then out of luck.
+Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly,
+the constraint solver is not quite smart enough to realize this and we must
+make it patently obvious by reifying the constraint pointwise with proof.
+
+Here is an example how this can be used in practise:
+
+>>> import Data.Vinyl.Functor (ElField(Field), Compose(Compose))
+>>> testRec :: Rec ElField '[ '("age", Double), '("number", Int)] = Field 1.0 :& Field 0 :& RNil
+>>> testRecWithConstraints = reifyConstraint @Num testRec
+>>> rmap (\(Compose (Dict x)) -> x+1) testRecWithConstraints
+{age :-> 2.0, number :-> 1}
+-}
 class ReifyConstraint c f rs where
   reifyConstraint
     :: Rec f rs
@@ -287,8 +573,27 @@ instance (c (f x), ReifyConstraint c f xs)
   reifyConstraint (x :& xs) = Compose (Dict x) :& reifyConstraint xs
   {-# INLINE reifyConstraint #-}
 
--- | Build a record whose elements are derived solely from a
--- constraint satisfied by each.
+{- |
+Build a record whose elements are derived solely from a
+constraint satisfied by each.
+
+>>> :set -XFlexibleInstances
+>>> :set -XFlexibleContexts
+>>> :set -XUndecidableInstances
+>>> import Data.Vinyl.Derived (KnownField)
+>>> import Data.Vinyl.TypeLevel (Snd)
+>>> import Data.Vinyl.Functor (ElField(Field))
+>>> import Data.Proxy (Proxy(Proxy))
+>>> class (KnownField a, Monoid (Snd a)) => Helper a
+>>> instance (KnownField a, Monoid (Snd a)) => Helper a
+>>>
+:{
+testRec :: Rec ElField '[ '("list", [Double]), '("string", String) ]
+testRec = rpureConstrained @Helper (Field mempty)
+:}
+>>> testRec
+{list :-> [], string :-> ""}
+-}
 class RPureConstrained c ts where
   rpureConstrained :: (forall a. c a => f a) -> Rec f ts
 
@@ -300,20 +605,73 @@ instance (c x, RPureConstrained c xs) => RPureConstrained c (x ': xs) where
   rpureConstrained f = f :& rpureConstrained @c @xs f
   {-# INLINE rpureConstrained #-}
 
--- | Capture a type class instance dictionary. See
--- 'Data.Vinyl.Lens.getDict' for a way to obtain a 'DictOnly' value
--- from an 'RPureConstrained' constraint.
+{- |
+Capture a type class instance dictionary. This data type can
+be used together with rpureConstrained:
+
+>>> import Data.Vinyl.Lens (rget)
+>>>
+:{
+testRec :: Rec (DictOnly Num) '[Double, Int]
+testRec = rpureConstrained @Num @'[Double, Int] DictOnly
+:}
+>>>
+:{
+val :: DictOnly Num Double
+val = rget @Double testRec
+:}
+
+In itself not much can be done with a @DictOnly@. However,
+it becomes useful together with the @Product@ Functor that allows
+to pair it on the side with another value. That way we can keep
+track of a constraint and use the other value for computations:
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> import Data.Functor.Product (Product(Pair))
+>>>
+:{
+builder :: Num a => Product (DictOnly Num) Identity a
+builder = Pair DictOnly (Identity 0)
+:}
+>>>
+:{
+testRec :: Rec (Product (DictOnly Num) Identity) '[Double, Int]
+testRec = rpureConstrained @Num @'[Double, Int] builder
+:}
+>>> Pair DictOnly val = rget @Double testRec
+>>> val
+0.0
+-}
 data DictOnly (c :: k -> Constraint) a where
   DictOnly :: forall c a. c a => DictOnly c a
 
--- | A useful technique is to use 'rmap (Pair (DictOnly @MyClass))' on
--- a 'Rec' to pair each field with a type class dictionary for
--- @MyClass@. This helper can then be used to eliminate the original.
+{- |
+A useful technique is to use 'rmap (Pair (DictOnly @MyClass))' on a 'Rec' to
+pair each field with a type class dictionary for @MyClass@. This helper can
+then be used to apply a function to a DictOnly that is paired with another
+field:
+
+>>> import Data.Vinyl.Functor (Identity(Identity))
+>>> import Data.Functor.Product (Product(Pair))
+>>>
+:{
+testRec :: Rec (Product (DictOnly Num) Identity) '[Double, Int]
+testRec = rpureConstrained @Num @'[Double, Int] (Pair DictOnly (Identity 0))
+:}
+>>> rmap (withPairedDict (fmap (2 +))) testRec
+{2.0, 2}
+-}
 withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r
 withPairedDict f (Pair DictOnly x) = f x
 
--- | Build a record whose elements are derived solely from a
--- list of constraint constructors satisfied by each.
+{- |
+Build a record whose elements are derived solely from a
+list of constraint constructors satisfied by each.
+
+>>> import Data.Functor.Identity (Identity(Identity))
+>>> rpureConstraints @'[Num, Enum] (succ (Identity 0)) :: Rec Identity '[Int, Double] 
+{Identity 1, Identity 1.0}
+-}
 class RPureConstraints cs ts where
   rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts
 
@@ -326,8 +684,13 @@ instance (AllSatisfied cs t, RPureConstraints cs ts)
   rpureConstraints f = f :& rpureConstraints @cs @ts f
   {-# INLINE rpureConstraints #-}
 
--- | Records may be shown insofar as their points may be shown.
--- 'reifyConstraint' is used to great effect here.
+{- |
+Records may be shown insofar as their points may be shown.
+'reifyConstraint' is used to great effect here.
+
+>>> "record with Nothings: " ++ (show (rpure Nothing :: Rec Maybe '[Int, Double]))
+"record with Nothings: {Nothing, Nothing}"
+-}
 instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs)
   => Show (Rec f rs) where
   show xs =
@@ -337,6 +700,14 @@ instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs)
       . rmap (\(Compose (Dict x)) -> Const $ show x)
       $ reifyConstraint @Show xs
 
+{- |
+The Semigroup instance is mapped to each element of the record.
+
+>>> t1 = ["Alice", "Bob"] :& [20, 22] :& RNil
+>>> t2 = ["Charlie", "Dan"] :& [24, 23] :& RNil
+>>> t1 <> t2
+{["Alice","Bob","Charlie","Dan"], [20,22,24,23]}
+-}
 instance Semigroup (Rec f '[]) where
   RNil <> RNil = RNil
 
@@ -344,6 +715,12 @@ instance (Semigroup (f r), Semigroup (Rec f rs))
   => Semigroup (Rec f (r ': rs)) where
   (x :& xs) <> (y :& ys) = (x <> y) :& (xs <> ys)
 
+{- |
+The Monoid instance is also mapped to each element of the record.
+
+>>> mempty :: Rec [] '[Double, String, Int]
+{[], [], []}
+-}
 instance Monoid (Rec f '[]) where
   mempty = RNil
   RNil `mappend` RNil = RNil
@@ -352,11 +729,30 @@ instance (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where
   mempty = mempty :& mempty
   (x :& xs) `mappend` (y :& ys) = (mappend x y) :& (mappend xs ys)
 
+{- |
+The Eq instance is also just an element-wise comparison.
+
+>>> import Data.Vinyl.Functor (ElField(Field))
+>>> r1 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Alice":& Field 30 :& RNil
+>>> r2 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Bob":& Field 25 :& RNil
+>>> r1 == r2
+False
+-}
 instance Eq (Rec f '[]) where
   _ == _ = True
 instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where
   (x :& xs) == (y :& ys) = (x == y) && (xs == ys)
 
+{- |
+The Ord instance is element-wise, lexicographical ordering using the Monoid
+instance of the Ordering type.
+
+>>> import Data.Vinyl.Functor (ElField(Field))
+>>> r1 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Alice":& Field 30 :& RNil
+>>> r2 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Bob":& Field 25 :& RNil
+>>> r1 < r2
+True
+-}
 instance Ord (Rec f '[]) where
   compare _ _ = EQ
 instance (Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) where
@@ -415,19 +811,31 @@ instance ReifyConstraint NFData f xs => NFData (Rec f xs) where
       go RNil = ()
       go (Compose (Dict x) :& xs) = rnf x `seq` go xs
 
--- | Analogous to 'Data.List.head'. Unlike the version in @singletons@,
--- this family merely gets stuck instead of producing a type error if
--- the list is empty. This is often better, because the type error that
--- would be produced here would be much less informative than one that
--- would likely be available where it's used.
+{- |
+Analogous to 'Data.List.head'. Unlike the version in @singletons@,
+this family merely gets stuck instead of producing a type error if
+the list is empty. This is often better, because the type error that
+would be produced here would be much less informative than one that
+would likely be available where it's used.
+
+>>> :k! Head '[Int, Double, String]
+Head '[Int, Double, String] :: *
+= Int
+-}
 type family Head xs where
   Head (x ': _) = x
   
--- | Analogous to 'Data.List.tail'. Unlike the version in @singletons@,
--- this family merely gets stuck instead of producing a type error if
--- the list is empty. This is often better, because the type error that
--- would be produced here would be much less informative than one that
--- would likely be available where it's used.
+{- |
+Analogous to 'Data.List.tail'. Unlike the version in @singletons@,
+this family merely gets stuck instead of producing a type error if
+the list is empty. This is often better, because the type error that
+would be produced here would be much less informative than one that
+would likely be available where it's used.
+
+>>> :k! Tail '[Int, Double, String]
+Tail '[Int, Double, String] :: [*]
+= '[Double, String]
+-}
 type family Tail xs where
   Tail (_ ': xs) = xs
 
diff --git a/Data/Vinyl/Curry.hs b/Data/Vinyl/Curry.hs
index e61026b..f34f4df 100644
--- a/Data/Vinyl/Curry.hs
+++ b/Data/Vinyl/Curry.hs
@@ -123,9 +123,9 @@ runcurryX f = xruncurry f . toXRec
 {-|
 Lift an N-ary function to work over a record of 'Applicative' computations.
 
+>>> import Data.Vinyl.Core ( Rec((:&), RNil) )
 >>> runcurryA' (+) (Just 2 :& Just 3 :& RNil)
 Just 5
-
 >>> runcurryA' (+) (Nothing :& Just 3 :& RNil)
 Nothing
 -}
@@ -179,9 +179,17 @@ For the type-level list @ts@, @'CurriedX' f ts a@ is a curried function type
 from arguments of type @HKD f t@ for @t@ in @ts@, to a result of type @a@.
 
 >>> :set -XTypeOperators
+>>> import Data.Vinyl.Functor ((:.), Identity(Identity))
+>>> import Data.Vinyl.Curry (CurriedX)
 >>> :kind! CurriedX (Maybe :. Identity) '[Int, Bool, String] Int
 CurriedX (Maybe :. Identity) '[Int, Bool, String] Int :: *
-= Maybe Int -> Maybe Bool -> Maybe [Char] -> Int
+= Data.Vinyl.XRec.HKD
+    (Data.Vinyl.Functor.Compose Maybe Identity) Int
+  -> Data.Vinyl.XRec.HKD
+       (Data.Vinyl.Functor.Compose Maybe Identity) Bool
+  -> Data.Vinyl.XRec.HKD
+       (Data.Vinyl.Functor.Compose Maybe Identity) [Char]
+  -> Int
 -}
 type family CurriedX (f :: u -> Type) (ts :: [u]) a where
   CurriedX f '[] a = a
diff --git a/Data/Vinyl/Tutorial/Overview.hs b/Data/Vinyl/Tutorial/Overview.hs
index c17e7ef..203b355 100644
--- a/Data/Vinyl/Tutorial/Overview.hs
+++ b/Data/Vinyl/Tutorial/Overview.hs
@@ -7,6 +7,7 @@
 
     Let's work through a quick example. We'll need to enable some language
     extensions first:
+>>> :set -package lens
 
 >>> :set -XDataKinds
 >>> :set -XPolyKinds
@@ -15,6 +16,7 @@
 >>> :set -XTypeFamilies
 >>> :set -XFlexibleContexts
 >>> :set -XFlexibleInstances
+>>> :set -XStandaloneKindSignatures
 >>> :set -XNoMonomorphismRestriction
 >>> :set -XGADTs
 >>> :set -XTypeSynonymInstances
@@ -27,7 +29,6 @@
 >>> import Control.Lens hiding (Identity)
 >>> import Control.Lens.TH
 >>> import Data.Char
->>> import Test.DocTest
 >>> import Data.Singletons.TH (genSingletons)
 >>> import Data.Maybe
 
@@ -294,4 +295,3 @@ module Data.Vinyl.Tutorial.Overview where
 
 import Data.Vinyl.Core
 import Data.Vinyl.Functor
-import Data.Vinyl.Lens
diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs
index 70b00e9..9a44e3f 100644
--- a/Data/Vinyl/TypeLevel.hs
+++ b/Data/Vinyl/TypeLevel.hs
@@ -24,11 +24,36 @@ module Data.Vinyl.TypeLevel where
 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.
+{- |
+A mere approximation of the natural numbers. And their image as lifted by
+@-XDataKinds@ corresponds to the actual natural numbers.
+
+The following is an example for a term level number of type Nat:
+
+>>> number = S (S Z)
+>>> :t number
+number :: Nat
+
+But it is intended to be used at the type level:
+
+>>> import Data.Proxy (Proxy(Proxy))
+>>> Proxy :: Proxy (S (S Z))
+Proxy
+
+Often it is used with type applications:
+
+>>> Proxy @(S (S Z))
+Proxy
+-}
 data Nat = Z | S !Nat
 
--- | Produce a runtime 'Int' value corresponding to a 'Nat' type.
+{- |
+Produce a runtime 'Int' value corresponding to a 'Nat' type.
+This is intended to be used with TypeApplications:
+
+>>> natToInt @('S ('S 'Z))
+2
+-}
 class NatToInt (n :: Nat) where
   natToInt :: Int
 
@@ -40,8 +65,13 @@ instance NatToInt n => NatToInt ('S n) where
   natToInt = 1 + natToInt @n
   {-# INLINE natToInt #-}
 
--- | Reify a list of type-level natural number indices as runtime
--- 'Int's relying on instances of 'NatToInt'.
+{- |
+Reify a list of type-level natural number indices as runtime
+'Int's relying on instances of 'NatToInt'.
+
+>>> indexWitnesses @'[S (S Z), Z, S (S (S Z))]
+[2,0,3]
+-}
 class IndexWitnesses (is :: [Nat]) where
   indexWitnesses :: [Int]
 
@@ -53,61 +83,145 @@ instance (IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) where
   indexWitnesses = natToInt @i : indexWitnesses @is
   {-# INLINE indexWitnesses #-}
 
--- | Project the first component of a type-level tuple.
+{- |
+Project the first component of a type-level tuple.
+
+>>> :k! Fst '("age", Int)
+Fst '("age", Int) :: GHC.Types.Symbol
+= "age"
+-}
 type family Fst (a :: (k1,k2)) where Fst '(x,y) = x
 
--- | Project the second component of a type-level tuple.
+{- |
+Project the second component of a type-level tuple.
+
+>>> :k! Snd '("age", Int)
+Snd '("age", Int) :: *
+= Int
+-}
 type family Snd (a :: (k1,k2)) where Snd '(x,y) = y
 
+{- |
+Compute the length of a type level list.
+
+>>> :k! RLength '[ '("age", Int), '("name", String)]
+RLength '[ '("age", Int), '("name", String)] :: Nat
+= 'S ('S 'Z)
+-}
 type family RLength xs where
   RLength '[] = 'Z
   RLength (x ': xs) = 'S (RLength xs)
 
--- | A partial relation that gives the index of a value in a list.
+{- |
+Compute the index of a value in a list.
+
+>>> :k! RIndex '("age", Int) '[ '("age", Int), '("name", String)]
+RIndex '("age", Int) '[ '("age", Int), '("name", String)] :: Nat
+= 'Z
+-}
 type family RIndex (r :: k) (rs :: [k]) :: Nat where
   RIndex r (r ': rs) = 'Z
   RIndex r (s ': rs) = 'S (RIndex r rs)
 
--- | A partial relation that gives the indices of a sublist in a larger list.
+{- |
+Compute the indices of a sublist in a larger list.
+
+>>> :k! RImage '[Int, String] '[Int, Double, String]
+RImage '[Int, String] '[Int, Double, String] :: [Nat]
+= '[ 'Z, 'S ('S 'Z)]
+-}
 type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where
   RImage '[] ss = '[]
   RImage (r ': rs) ss = RIndex r ss ': RImage rs ss
 
--- | Remove the first occurrence of a type from a type-level list.
+{- |
+Remove the first occurrence of a type from a type-level list.
+
+>>> :k! RDelete Int '[Int, Double, String]
+RDelete Int '[Int, Double, String] :: [*]
+= '[Double, String]
+-}
 type family RDelete r rs where
   RDelete r (r ': rs) = rs
   RDelete r (s ': rs) = s ': RDelete r rs
 
--- | A constraint-former which applies to every field in a record.
+{- |
+Build a constraint tuple with one constraint for every field
+in a record.
+
+>>> import Data.Vinyl.Functor (ElField)
+>>> :k! RecAll ElField '[ '("age", Int), '("name", Double)] Num
+RecAll ElField '[ '("age", Int), '("name", Double)] Num :: Constraint
+= (Num (ElField '("age", Int)),
+   (Num (ElField '("name", Double)), () :: Constraint))
+-}
 type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where
   RecAll f '[] c = ()
   RecAll f (r ': rs) c = (c (f r), RecAll f rs c)
 
 infixr 5 ++
 
--- | Append for type-level lists.
+{- |
+Append for type-level lists.
+
+>>> :k! '[Int, Double] ++ '[String]
+'[Int, Double] ++ '[String] :: [*]
+= '[Int, Double, String]
+-}
 type family (as :: [k]) ++ (bs :: [k]) :: [k] where
   '[] ++ bs = bs
   (a ': as) ++ bs = a ': (as ++ bs)
 
--- | Constraint that all types in a type-level list satisfy a
--- constraint.
+{- |
+Constraint that all types in a type-level list satisfy a
+constraint.
+
+>>> :k! AllConstrained Num '[Int, Double]
+AllConstrained Num '[Int, Double] :: Constraint
+= (Num Int, (Num Double, () :: Constraint))
+
+>>>
+:{
+f :: AllConstrained Num '[a, b] => Either a b
+f = Right 0
+:}
+>>> f :: Either Double Int
+Right 0
+-}
 type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where
   AllConstrained c '[] = ()
   AllConstrained c (t ': ts) = (c t, AllConstrained c ts)
 
--- | Constraint that each Constraint in a type-level list is satisfied
--- by a particular type.
-class AllSatisfied cs t where
-instance AllSatisfied '[] t where
-instance (c t, AllSatisfied cs t) => AllSatisfied (c ': cs) t where
-
--- | Constraint that all types in a type-level list satisfy each
--- constraint from a list of constraints.
---
--- @AllAllSat cs ts@ should be equivalent to @AllConstrained
--- (AllSatisfied cs) ts@ if partial application of type families were
--- legal.
+{- |
+Alternative to get a constraint that each Constraint in a type-level list is
+satisfied by a particular type.
+
+>>>
+:{
+f :: AllSatisfied '[Num, Eq, Show] a => a -> String
+f a = if a == 0 then show a else "not equal to 0"
+:}
+-}
+type family AllSatisfied (cs :: [u -> Constraint]) (t :: u) :: Constraint where
+    AllSatisfied '[] t = ()
+    AllSatisfied (c ': cs) t = (c t, AllSatisfied cs t)
+
+{- |
+Constraint that all types in a type-level list satisfy each
+constraint from a list of constraints.
+
+@AllAllSat cs ts@ should be equivalent to @AllConstrained
+(AllSatisfied cs) ts@ if partial application of type families were
+legal.
+
+>>>
+:{
+f :: AllAllSat '[Num, Eq, Show] '[a, b] => a -> b -> (String, Bool)
+f a b = (if a == 0 then show a else "not equal to 0", b == 0)
+:}
+>>> f (0 :: Int) (1.0 :: Double)
+("0",False)
+-}
 type family AllAllSat cs ts :: Constraint where
   AllAllSat cs '[] = ()
   AllAllSat cs (t ': ts) = (AllSatisfied cs t, AllAllSat cs ts)
diff --git a/flake.lock b/flake.lock
index c566578..fbae18a 100644
--- a/flake.lock
+++ b/flake.lock
@@ -31,10 +31,26 @@
         "type": "github"
       }
     },
+    "nur": {
+      "locked": {
+        "lastModified": 1689328451,
+        "narHash": "sha256-WWJXUi3mT05cNBQ9YwLO/AqWyaTOxmHEp7EdJlkioM4=",
+        "owner": "nix-community",
+        "repo": "nur",
+        "rev": "1839d2b991671f63666cdb0716875a2dd8ba4a46",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-community",
+        "repo": "nur",
+        "type": "github"
+      }
+    },
     "root": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": "nixpkgs",
+        "nur": "nur"
       }
     }
   },
diff --git a/flake.nix b/flake.nix
index 8c47fc7..3213aea 100644
--- a/flake.nix
+++ b/flake.nix
@@ -3,12 +3,16 @@
 
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
+    nur.url = "github:nix-community/nur";
     flake-utils.url = "github:numtide/flake-utils";
   };
 
-  outputs = { self, nixpkgs, flake-utils }:
+  outputs = { self, nixpkgs, nur, flake-utils }:
     flake-utils.lib.eachDefaultSystem (system: let
-
+      nurpkgs = import nur {
+          nurpkgs = nixpkgs.legacyPackages.x86_64-linux;
+          pkgs = nixpkgs.legacyPackages.x86_64-linux;
+        };
       compiler = "8107";
       # compiler = "921";
       pkgs = import nixpkgs {
@@ -52,6 +56,9 @@
       buildInputs = [
         ghc
         hspkgs.cabal-install
+        hspkgs.haskell-language-server
+        hspkgs.cabal-plan
+        nurpkgs.repos.amesgen.cabal-docspec
       ];
     };
   });
diff --git a/stack.yaml b/stack.yaml
index 5c92dbd..6b2656e 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,4 +1,4 @@
-resolver: lts-17.8
+resolver: lts-18.28
 
 packages:
 - .
diff --git a/tests/Intro.lhs b/tests/Intro.lhs
deleted file mode 100644
index 7c5ef9d..0000000
--- a/tests/Intro.lhs
+++ /dev/null
@@ -1,291 +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 #-}
-> {-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 810
-> {-# LANGUAGE StandaloneKindSignatures #-}
-#endif
-
-> 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/doctests.hs b/tests/doctests.hs
index 872a4ce..a5b5b94 100644
--- a/tests/doctests.hs
+++ b/tests/doctests.hs
@@ -1,14 +1,8 @@
-{-# language CPP #-}
-import Test.DocTest
+module Main where
 
 main :: IO ()
-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" ]
+main = do
+    putStrLn "This test-suite exists only to add dependencies"
+    putStrLn "To run doctests: "
+    putStrLn "    cabal build all --enable-tests"
+    putStrLn "    cabal-docspec"
diff --git a/vinyl.cabal b/vinyl.cabal
index 1676ae9..65b7a2b 100644
--- a/vinyl.cabal
+++ b/vinyl.cabal
@@ -48,6 +48,10 @@ library
     build-depends: constraints >= 0.6.1
   default-language:    Haskell2010
   ghc-options:         -Wall
+  if impl (ghc < 9.0.1)
+      x-docspec-extra-packages: lens, singletons
+  else
+      x-docspec-extra-packages: lens, singletons-th
   other-extensions:    TypeApplications
 
 benchmark storable
@@ -93,17 +97,17 @@ benchmark asa
   ghc-options:      -O2
   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
+-- Dummy test for cabal-docspec dependencies that are used in
+-- Data.Vinyl.Tutorial.Overview
+test-suite doctests
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   tests
+  main-is:          doctests.hs
+  if impl (ghc < 9.0.1)
+    build-depends:    base, lens singletons >= 0.10 && < 3, vinyl
+  else
+    build-depends:    base, lens singletons-th >= 3 && < 3.1, vinyl
+  default-language: Haskell2010
 
 test-suite aeson
   type:             exitcode-stdio-1.0