diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,12 @@
-0.5.1
----------
+# 0.5.2
 
+Ported the tutorial to haddocks (andrewthad)
+
+# 0.5.1
+
 Added utilities for working with the `FieldRec` type.
 
-Vinyl 0.5
-=========
+# 0.5
 
 Vinyl 0.5 combines the generality of Vinyl 0.4 with the ease-of-use of previous
 versions by eschewing the defunctionalized type families and just using plain
@@ -14,8 +16,7 @@
 Also new in 0.5 is a unified lens-based approach to subtyping, coercion and
 projection.
 
-Vinyl 0.4
-=========
+# 0.4
 
 Vinyl 0.4 is a big departure from previous versions, in that it introduces a
 universe encoding as a means to generalize the space of keys from strings to
diff --git a/Data/Vinyl/Class/Method.hs b/Data/Vinyl/Class/Method.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Class/Method.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE BangPatterns          #-}
+{-# LANGUAGE ConstraintKinds       #-}
+
+{-| This module uses 'RecAll' to extend common typeclass methods to records.
+    Generally, it is preferable to use the original typeclass methods to these 
+    variants. For example, in most places where 'recCompare' could be used,
+    you could use 'compare' instead. They are useful in scenarios
+    that involve working on unknown subsets of a record's fields
+    because 'RecAll' constraints can easily be weakened. An example of this
+    is given at the bottom of this page.
+-}
+
+module Data.Vinyl.Class.Method 
+  ( -- * Eq Functions
+    recEq
+    -- * Ord Functions
+  , recCompare
+    -- * Monoid Functions
+  , recMempty
+  , recMappend
+  , recMconcat
+    -- * Num Functions
+  , recAdd
+  , recSubtract
+  , recMultiply
+  , recAbs
+  , recSignum
+  , recNegate
+    -- * Bounded Functions
+  , recMinBound
+  , recMaxBound
+    -- * Example
+    -- $example
+  ) where
+
+import Data.Vinyl.Core
+import Data.Vinyl.TypeLevel
+import Data.Monoid
+
+recEq :: RecAll f rs Eq => Rec f rs -> Rec f rs -> Bool
+recEq RNil RNil = True
+recEq (a :& as) (b :& bs) = a == b && recEq as bs
+
+recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering
+recCompare RNil RNil = EQ
+recCompare (a :& as) (b :& bs) = compare a b <> recCompare as bs
+
+-- | This function differs from the original 'mempty' in that 
+--   it takes an argument. In some cases, you will already
+--   have a record of the type you are interested in, and 
+--   that can be passed an the argument. In other situations
+--   where this is not the case, you may need the
+--   interpretation function of the argument record to be 
+--   @Const ()@ or @Proxy@ so the you can generate the
+--   argument with 'rpure'.
+recMempty :: RecAll f rs Monoid => Rec proxy rs -> Rec f rs
+recMempty RNil = RNil
+recMempty (_ :& rs) = mempty :& recMempty rs
+
+recMappend :: RecAll f rs Monoid => Rec f rs -> Rec f rs -> Rec f rs
+recMappend RNil RNil = RNil
+recMappend (a :& as) (b :& bs) = mappend a b :& recMappend as bs
+
+-- | This function differs from the original 'mconcat'.
+--   See 'recMempty'.
+recMconcat :: RecAll f rs Monoid => Rec proxy rs -> [Rec f rs] -> Rec f rs
+recMconcat p [] = recMempty p
+recMconcat p (rec : recs) = recMappend rec (recMconcat p recs)
+
+recAdd :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
+recAdd RNil RNil = RNil
+recAdd (a :& as) (b :& bs) = (a + b) :& recAdd as bs
+
+recSubtract :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
+recSubtract RNil RNil = RNil
+recSubtract (a :& as) (b :& bs) = (a - b) :& recSubtract as bs
+
+recMultiply :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
+recMultiply RNil RNil = RNil
+recMultiply (a :& as) (b :& bs) = (a * b) :& recSubtract as bs
+
+recAbs :: RecAll f rs Num => Rec f rs -> Rec f rs
+recAbs RNil = RNil
+recAbs (a :& as) = abs a :& recAbs as 
+
+recSignum :: RecAll f rs Num => Rec f rs -> Rec f rs
+recSignum RNil = RNil
+recSignum (a :& as) = signum a :& recAbs as 
+
+recNegate :: RecAll f rs Num => Rec f rs -> Rec f rs
+recNegate RNil = RNil
+recNegate (a :& as) = negate a :& recAbs as 
+
+-- | This function differs from the original 'minBound'.
+--   See 'recMempty'.
+recMinBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs
+recMinBound RNil = RNil
+recMinBound (_ :& rs) = minBound :& recMinBound rs
+
+-- | This function differs from the original 'maxBound'.
+--   See 'recMempty'.
+recMaxBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs
+recMaxBound RNil = RNil
+recMaxBound (_ :& rs) = maxBound :& recMaxBound rs
+
+{- $example
+    This module provides variants of typeclass methods that have 
+    a 'RecAll' constraint instead of the normal typeclass 
+    constraint. For example, a type-specialized 'compare' would
+    look like this:
+
+> compare :: Ord (Rec f rs) => Rec f rs -> Rec f rs -> Ordering
+
+    The 'recCompare' function looks like this:
+
+> recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering
+
+    The only difference is the constraint. Let's look at a potential 
+    use case for these functions.
+
+    Let's write a function that projects out a subrecord from two records and 
+    then compares those for equality. We can write this with 
+    the '<:' operator from @Data.Vinyl.Lens@ and the normal 'compare'
+    function. We don't need 'recCompare':
+
+> -- This needs ScopedTypeVariables
+> projectAndCompare :: forall super sub f. (super <: sub, Ord (Rec f sub)) 
+>                   => Proxy sub -> Rec f super -> Rec f super -> Ordering
+> projectAndCompare _ a b = compare (rcast a :: Rec f sub) (rcast b :: Rec f sub)
+
+    That works fine for the majority of use cases, and it is probably how you should 
+    write the function if it does everything you need. However, let's consider
+    a somewhat more complicated case. 
+
+    What if the exact subrecord we were projecting couldn't be 
+    known at compile time? Assume that the end user was allowd to
+    choose the fields on which he or she wanted to compare records.
+    The @projectAndCompare@ function cannot handle this because of the
+    @Ord (Rec f sub)@ constraint. Even if we amend the constraint to
+    read @Ord (Rec f super)@ instead, we cannot use this information
+    to recover the @Ord (Rec f sub)@ constraint that we need. Let's
+    try another approach.
+
+    We can use the following GADT to prove subsethood:
+
+> data Sublist (super :: [k]) (sub :: [k]) where
+>   SublistNil   :: Sublist '[]
+>   SublistSuper :: Proxy r -> Sublist super sub -> Sublist (r ': super) sub
+>   SublistBoth  :: Proxy r -> Sublist super sub -> Sublist (r ': super) (r ': sub)
+>
+> projectRec :: Sublist super sub -> Rec f super -> Rec f sub
+> projectRec s r = case s of
+>   SublistNil -> RNil
+>   SublistBoth n snext -> case r of
+>     rhead :& rtail -> rhead :& projectRec snext rtail
+>   SublistSuper n snext -> case r of
+>     rhead :& rtail -> projectRec snext rtail
+
+    It is also possible to write a typeclass to generate @Sublist@s
+    implicitly, but that is beyond the scope of this example. Let's
+    now write a function to use @Sublist@ to weaken a 'RecAll'
+    constraint:
+
+> import Data.Vinyl.Core hiding (Dict)
+> import Data.Constraint
+>
+> weakenRecAll :: Proxy f -> Proxy c -> Sublist super sub -> RecAll f super c :- RecAll f sub c
+> weakenRecAll f c s = case s of
+>   SublistNil -> Sub Dict
+>   SublistSuper _ snext -> Sub $ case weakenRecAll f c snext of
+>     Sub Dict -> Dict
+>   SublistBoth _ snext -> Sub $ case weakenRecAll f c snext of
+>     Sub Dict -> Dict
+
+    Now we can write a different version of our original function:
+
+> -- This needs ScopedTypeVariables
+> projectAndCompare2 :: forall super sub f. (RecAll f super Ord)
+>                    => Sublist super sub -> Rec f super -> Rec f super -> Ordering
+> projectAndCompare2 s a b = case weakenRecAll (Proxy :: Proxy f) (Proxy :: Proxy Ord) s of
+>   Sub Dict -> recCompare (projectRec s a) (projectRec s b)
+
+    Notice that in this case, the 'Ord' constraint applies to the full set of fields
+    and is then weakened to target a subset of them instead.
+-}
+
+
+
diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs
--- a/Data/Vinyl/Core.hs
+++ b/Data/Vinyl/Core.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE BangPatterns          #-}
 {-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -18,7 +19,9 @@
 import Foreign.Ptr (castPtr, plusPtr)
 import Foreign.Storable (Storable(..))
 import Data.Vinyl.Functor
+#if __GLASGOW_HASKELL__ < 710
 import Control.Applicative hiding (Const(..))
+#endif
 import Data.Typeable (Proxy(..))
 import Data.List (intercalate)
 import Data.Vinyl.TypeLevel
@@ -31,7 +34,7 @@
   RNil :: Rec f '[]
   (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
 
-infixr :&
+infixr 7 :&
 infixr 5  <+>
 infixl 8 <<$>>
 infixl 8 <<*>>
@@ -172,6 +175,11 @@
   _ == _ = True
 instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where
   (x :& xs) == (y :& ys) = (x == y) && (xs == ys)
+
+instance Ord (Rec f '[]) where
+  compare _ _ = EQ
+instance (Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) where
+  compare (x :& xs) (y :& ys) = mappend (compare x y) (compare xs ys)
 
 instance Storable (Rec f '[]) where
   sizeOf _    = 0
diff --git a/Data/Vinyl/Functor.hs b/Data/Vinyl/Functor.hs
--- a/Data/Vinyl/Functor.hs
+++ b/Data/Vinyl/Functor.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                        #-}
 {-# LANGUAGE DeriveFoldable             #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveTraversable          #-}
@@ -6,21 +7,53 @@
 {-# LANGUAGE PolyKinds                  #-}
 {-# LANGUAGE TypeOperators              #-}
 
-module Data.Vinyl.Functor where
+module Data.Vinyl.Functor 
+  ( -- * Introduction
+    -- $introduction
+    -- * Data Types
+    Identity(..)
+  , Thunk(..)
+  , Lift(..)
+  , Compose(..)
+  , (:.)
+  , Const(..)
+    -- * Discussion
+    
+    -- ** Example
+    -- $example
+    
+    -- ** Ecosystem
+    -- $ecosystem
+  ) where
 
-import Control.Applicative
+#if __GLASGOW_HASKELL__ < 710
+import Control.Applicative hiding (Const)
 import Data.Foldable
 import Data.Traversable
+#endif
 import Foreign.Storable
 
+{- $introduction
+    This module provides functors and functor compositions
+    that can be used as the interpretation function for a
+    'Rec'. For a more full discussion of this, scroll down
+    to the bottom.
+-}
+
+-- | This is identical to the "Identity" from "Data.Functor.Identity"
+-- in "base" except for its 'Show' instance.
 newtype Identity a
   = Identity { getIdentity :: a }
     deriving ( Functor
              , Foldable
              , Traversable
              , Storable
+             , Eq
+             , Ord
              )
 
+-- | Used this instead of 'Identity' to make a record
+--   lazy in its fields.
 data Thunk a
   = Thunk { getThunk :: a }
     deriving ( Functor
@@ -36,6 +69,7 @@
     deriving (Storable)
 
 type f :. g = Compose f g
+infixr 9 :.
 
 newtype Const (a :: *) (b :: k)
   = Const { getConst :: a }
@@ -91,3 +125,99 @@
   pure x = Lift (pure x, pure x)
   Lift (f, g) <*> Lift (x, y) = Lift (f <*> x, g <*> y)
 
+-- $setup
+-- >>> import Data.Vinyl.Core
+-- >>> :set -XDataKinds
+--
+
+{- $example
+    The data types in this module are used to build interpretation
+    fuctions for a 'Rec'. To build a 'Rec' that is simply a heterogeneous
+    list, use 'Identity':
+
+>>> :{
+let myRec1 :: Rec Identity '[Int,Bool,Char]
+    myRec1 = Identity 4 :& Identity True :& Identity 'c' :& RNil
+:}
+
+    For a record in which the fields are optional, you could alternatively
+    write:
+
+>>> :{
+let myRec2 :: Rec Maybe '[Int,Bool,Char]
+    myRec2 = Just 4 :& Nothing :& Nothing :& RNil
+:}
+
+    And we can gather all of the effects with 'rtraverse':
+
+>>> let r2 = rtraverse (fmap Identity) myRec2
+>>> :t r2
+r2 :: Maybe (Rec Identity '[Int, Bool, Char])
+>>> r2
+Nothing
+
+    If the fields only exist once an environment is provided, you can 
+    build the record as follows:
+
+>>> :{
+let myRec3 :: Rec ((->) Int) '[Int,Bool,Char]
+    myRec3 = (+5) :& (const True) :& (head . show) :& RNil
+:}
+
+    And again, we can collect these effects with "rtraverse":
+
+>>> (rtraverse (fmap Identity) myRec3) 8
+{13, True, '8'}
+
+    If you want the composition of these two effects, you can use "Compose":
+
+>>> import Data.Char (chr)
+>>> :{
+let safeDiv a b = if b == 0 then Nothing else Just (div a b)
+    safeChr i = if i >= 32 && i <= 126 then Just (chr i) else Nothing
+    myRec4 :: Rec (Compose ((->) Int) Maybe) '[Int,Char]
+    myRec4 = (Compose $ safeDiv 42) :& (Compose safeChr) :& RNil
+:}
+
+-}
+
+{- $ecosystem
+    Of the five data types provided by this modules, three can
+    be found in others places: "Identity", "Compose", and "Const".
+    They are included with "vinyl" to help keep the dependency
+    list small. The differences will be discussed here.
+
+    The "Data.Functor.Identity" module was originally provided
+    by "transformers". When GHC 7.10 was released, it was moved
+    into "base-4.8". The "Identity" data type provided by that
+    module is well recognized across the haskell ecosystem
+    and has typeclass instances for lots of common typeclasses. 
+    The significant difference between it and the copy of
+    it provided here is that this one has a different 'Show'
+    instance. This is illustrated below:
+
+>>> Identity "hello"
+"hello"
+
+    But, when using "Identity" from "base":
+
+>>> import qualified Data.Functor.Identity as Base
+>>> Base.Identity "hello"
+Identity "hello"
+
+    This 'Show' instance makes records look nicer in GHCi.
+    Feel free to use "Data.Functor.Identity" if you do not
+    need the prettier output or if you need the many additional
+    typeclass instances that are provided for the standard
+    "Identity".
+
+    The story with "Compose" and "Const" is much more simple.
+    These also exist in "transformers", although "Const" 
+    is named "Constant" there. Prior to the release of 
+    "transformers-0.5", they were not polykinded, making 
+    them unusable for certain universes. However, in 
+    "transformers-0.5" and forward, they have been made
+    polykinded. This means that they are just as usable with 'Rec'
+    as the vinyl equivalents but with many more typeclass
+    instances such as 'Ord' and 'Show'.
+-}
diff --git a/Data/Vinyl/Tutorial/Overview.hs b/Data/Vinyl/Tutorial/Overview.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vinyl/Tutorial/Overview.hs
@@ -0,0 +1,298 @@
+{-|
+
+    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.
+    
+    Let's work through a quick example. We'll need to enable some language
+    extensions first:
+
+>>> :set -XDataKinds
+>>> :set -XPolyKinds
+>>> :set -XTypeOperators
+>>> :set -XTypeFamilies
+>>> :set -XFlexibleContexts
+>>> :set -XFlexibleInstances
+>>> :set -XNoMonomorphismRestriction
+>>> :set -XGADTs
+>>> :set -XTypeSynonymInstances
+>>> :set -XTemplateHaskell
+>>> :set -XStandaloneDeriving
+
+>>> import Data.Vinyl
+>>> import Data.Vinyl.Functor
+>>> import Control.Applicative
+>>> import Control.Lens hiding (Identity)
+>>> import Control.Lens.TH
+>>> import Data.Char
+>>> import Test.DocTest
+>>> import Data.Singletons.TH
+>>> import Data.Maybe
+
+    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 autmatically 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. Unfortunately, type families aren't first class in Haskell.  That's
+    why we also need a data type, with which we will parametrise 'Rec'.
+    We also generate the necessary singletons for each field label using
+    Template Haskell.
+
+>>> :{
+type family ElF (f :: Fields) :: * where
+  ElF Name = String
+  ElF Age = Int
+  ElF Sleeping = Bool
+  ElF Master = Rec Attr LifeForm
+newtype Attr f = Attr { _unAttr :: ElF f }
+makeLenses ''Attr
+genSingletons [ ''Fields ]
+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".
+
+>>> :{
+let (=::) :: sing f -> ElF f -> Attr f
+    _ =:: x = Attr x
+:}
+
+    Now, let's try to make an entity that represents a human:
+
+>>> :{
+let jon = (SName =:: "jon")
+       :& (SAge =:: 23)
+       :& (SSleeping =:: False)
+       :& RNil
+:}
+
+    Automatically, we can show the record:
+
+>>> print 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:
+
+>>> :{ 
+let tucker = (SName =:: "tucker")
+          :& (SAge =:: 9)
+          :& (SSleeping =:: True)
+          :& (SMaster =:: jon)
+          :& RNil
+:}
+
+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:
+
+>>> :{
+let 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.
+
+>>> let tucker' = wakeUp tucker
+>>> let jon' = wakeUp jon
+
+>>> tucker' ^. rlens SSleeping
+sleeping: False
+
+>>> tucker ^. rlens SSleeping
+sleeping: True
+
+>>> jon' ^. rlens SSleeping
+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:
+
+>>> let masterSleeping = rlens SMaster . unAttr . rlens SSleeping
+>>> let tucker'' = masterSleeping .~ (SSleeping =:: True) $ tucker'
+
+>>> tucker'' ^. masterSleeping
+sleeping: True
+
+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:
+
+>>> :{
+let 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!
+
+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 (the module @Data.Either.Validation@
+from the @either@ package provides such a type, though we do not
+cover it here).
+
+>>> :{
+let goodPerson :: Rec Attr Person
+    goodPerson = (SName =:: "Jon")
+              :& (SAge =:: 20)
+              :& RNil
+:}
+
+>>> :{
+let badPerson = (SName =:: "J#@#$on")
+             :& (SAge =:: 20)
+             :& RNil
+:}
+
+We\'ll give validation a (rather poor) shot.
+
+>>> :{
+let 
+    validatePerson :: Rec Attr Person -> Maybe (Rec Attr Person)
+    validatePerson p = (\n a -> (SName =:: n) :& (SAge =:: a) :& RNil) <$> vName <*> vAge
+      where
+      vName = validateName $ p ^. rlens SName . unAttr
+      vAge  = validateAge $ p ^. rlens SAge . unAttr
+      validateName str | all isAlpha str = Just str
+      validateName _ = Nothing
+      validateAge i | i >= 0 = Just i
+      validateAge _ = Nothing
+:}
+
+Let\'s try it out:
+
+>>> 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@:
+
+>>> :{
+let 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
+    vperson :: Rec (Validator Attr) Person
+    vperson = lift validateName :& lift validateAge :& RNil
+:}
+
+And we can use the special application operator '<<*>>' (which is
+analogous to '<*>', but generalized a bit) to use this to validate a
+record:
+
+>>> let goodPersonResult = vperson <<*>> goodPerson
+>>> let badPersonResult  = vperson <<*>> badPerson
+
+>>> isJust . getCompose $ goodPersonResult ^. rlens SName
+True
+
+>>> isJust . getCompose $ goodPersonResult ^. rlens SAge
+True
+
+>>> isJust . getCompose $ badPersonResult ^. rlens SName
+False
+
+>>> isJust . getCompose $ badPersonResult ^. rlens SAge
+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`:
+
+>>> :{
+let mgoodPerson :: Maybe (Rec Attr Person)
+    mgoodPerson = rtraverse getCompose goodPersonResult
+:}
+
+>>> let mbadPerson  = rtraverse getCompose badPersonResult
+
+>>> isJust mgoodPerson
+True
+
+>>> isJust mbadPerson
+False
+
+-}
+
+module Data.Vinyl.Tutorial.Overview where
+
+import Data.Vinyl.Core
+import Data.Vinyl.Functor
+import Data.Vinyl.Lens
+
+
diff --git a/benchmarks/EqualityBench.hs b/benchmarks/EqualityBench.hs
new file mode 100644
--- /dev/null
+++ b/benchmarks/EqualityBench.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}
+import Control.Monad (join)
+import Criterion.Main
+import Data.Functor.Identity
+import Data.Vinyl
+import Data.Vinyl.TypeLevel
+
+class Eq2 a where
+  eq2 :: a -> a -> Bool
+
+instance RecAll f rs Eq => Eq2 (Rec f rs) where
+  eq2 RNil RNil = True
+  eq2 (a :& as) (b :& bs) = a == b && eq2 as bs
+
+main :: IO ()
+main = defaultMain [
+         bench "Eq" $ whnf (join (==)) r1
+       , bench "Eq2" $ whnf (join eq2) r1 ]
+  where r1 = pure 23 :& pure 'b' :& pure 3.14 :& RNil :: Rec Identity '[Int, Char, Double]
diff --git a/tests/Intro.lhs b/tests/Intro.lhs
--- a/tests/Intro.lhs
+++ b/tests/Intro.lhs
@@ -12,7 +12,7 @@
 First, install Vinyl from Hackage:
 
 < cabal update
-< cabal install vinyl
+< cabal install vinyl singletons
 
 Let’s work through a quick example. We’ll need to enable some language
 extensions first:
@@ -29,17 +29,30 @@
 > import Test.DocTest
 > import Data.Singletons.TH
 
-Let’s define a universe of fields which we want to use:
+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 autmatically 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
@@ -47,12 +60,22 @@
 > 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 man:
+Now, let’s try to make an entity that represents a human:
 
 > jon = (SName =:: "jon")
 >    :& (SAge =:: 23)
@@ -65,8 +88,9 @@
 > -- >>> 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 men, they have masters. So, let’s build my dog:
+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)
@@ -78,19 +102,19 @@
 ------------
 
 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 men (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:
+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.
+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
@@ -131,7 +155,7 @@
 > upcastedTucker = rcast tucker
 
 The subtyping relationship between record types is expressed with the
-`(<:)` constraint; so, cast is of the following type:
+`(<:)` constraint; so, rcast is of the following type:
 
 < rcast :: r1 <: r2 => Rec f r1 -> Rec f r2
 
@@ -257,4 +281,4 @@
 > -- False
 
 > main :: IO ()
-> main = doctest ["tests/Intro.lhs"]
+> main = doctest ["tests/Intro.lhs", "Data/Vinyl/Tutorial/Overview.hs"]
diff --git a/vinyl.cabal b/vinyl.cabal
--- a/vinyl.cabal
+++ b/vinyl.cabal
@@ -1,5 +1,5 @@
 name:                vinyl
-version:             0.5.1
+version:             0.5.2
 synopsis:            Extensible Records
 -- description:
 license:             MIT
@@ -21,12 +21,14 @@
 
 library
   exposed-modules:     Data.Vinyl
+                     , Data.Vinyl.Class.Method
                      , Data.Vinyl.Core
                      , Data.Vinyl.Lens
                      , Data.Vinyl.Derived
                      , Data.Vinyl.TypeLevel
                      , Data.Vinyl.Functor
                      , Data.Vinyl.Notation
+                     , Data.Vinyl.Tutorial.Overview
   build-depends:       base >=4.7 && <= 5, ghc-prim
   default-language:    Haskell2010
   ghc-options: -fwarn-dodgy-exports -fwarn-dodgy-imports -fwarn-unused-matches -fwarn-unused-imports -fwarn-unused-binds -fwarn-incomplete-record-updates -fwarn-missing-signatures -fwarn-name-shadowing -fwarn-orphans -fwarn-overlapping-patterns -fwarn-tabs -fwarn-type-defaults
@@ -35,13 +37,21 @@
   type:             exitcode-stdio-1.0
   hs-source-dirs:   benchmarks
   main-is:          StorableBench.hs
-  build-depends:    base >= 4.7 && <= 5, vector, criterion, vinyl == 0.5, mwc-random, lens, linear
+  build-depends:    base >= 4.7 && <= 5, vector, criterion, vinyl >= 0.5.1, mwc-random, lens, linear
   ghc-options:      -O2 -fllvm
   default-language: Haskell2010
 
+benchmark equality
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   benchmarks
+  main-is:          EqualityBench.hs
+  build-depends:    base >= 4.7 && <= 5, criterion, vinyl >= 0.5.1
+  ghc-options:      -O2 -fllvm
+  default-language: Haskell2010
+
 test-suite doctests
   type:             exitcode-stdio-1.0
   hs-source-dirs:   tests
   main-is:          Intro.lhs
-  build-depends:    base >= 4.7 && <= 5, lens, vinyl == 0.5, doctest >= 0.8, singletons >= 0.10
+  build-depends:    base >= 4.7 && <= 5, lens, vinyl >= 0.5, doctest >= 0.8, singletons >= 0.10
   default-language: Haskell2010