diff --git a/Data/Vinyl/Classes.hs b/Data/Vinyl/Classes.hs
--- a/Data/Vinyl/Classes.hs
+++ b/Data/Vinyl/Classes.hs
@@ -8,11 +8,15 @@
 import           Control.Applicative
 import           Control.Monad.Identity
 
+-- | This class is a generalized, but non-pointed version of 'Applicative'. This
+-- is useful for types which range over functors rather than sets.
 class Apply (arr :: k -> k -> k) (f :: k -> *) where
   (<<*>>) :: f (arr a b) -> f a -> f b
 
+-- | To accumulate effects distributed over a data type, you 'run' it.
 class Run t where
   run :: Applicative f => t f -> f (t Identity)
 
+-- | '(~>)' is a morphism between functors.
 newtype (f ~> g) x = NT { runNT :: f x -> g x }
 
diff --git a/Data/Vinyl/Field.hs b/Data/Vinyl/Field.hs
--- a/Data/Vinyl/Field.hs
+++ b/Data/Vinyl/Field.hs
@@ -9,8 +9,10 @@
 
 import           GHC.TypeLits
 
--- A field is a symbol key and a type for its value.
+-- | A field contains a key and a type.
 data (:::) :: Symbol -> * -> * where
+  -- | A constructor is given to facilitate introducing fields from terms without
+  -- type annotations.
   Field :: sy ::: t
 
 instance SingI sy => Show (sy ::: t) where
diff --git a/Data/Vinyl/Rec.hs b/Data/Vinyl/Rec.hs
--- a/Data/Vinyl/Rec.hs
+++ b/Data/Vinyl/Rec.hs
@@ -28,76 +28,61 @@
 import           Data.Vinyl.Field
 import           GHC.TypeLits
 
--- A record is parameterized by a list of fields and a functor
+-- | A record is parameterized by a list of fields and a functor
 -- to be applied to each of those fields.
 data Rec :: [*] -> (* -> *) -> * where
+  -- | The empty record.
   RNil :: Rec '[] f
-  (:&) :: (r ~ (sy ::: t)) => f t -> Rec rs f -> Rec (r ': rs) f
+
+  -- | Cons for records.
+  (:&) :: f t -> Rec rs f -> Rec ((sy ::: t) ': rs) f
 infixr :&
 
--- Fixes a polymorphic record into the identity functor.
+-- | Fixes a polymorphic record into the 'Identity' functor.
 fixRecord :: (forall f. Applicative f => Rec rs f) -> PlainRec rs
 fixRecord xs = xs
 
--- Fields of plain records are in the Identity functor.
+-- | Fields of plain records are in the 'Identity' functor.
 type PlainRec rs = Rec rs Identity
 
--- Appends records
+-- | Append for records.
 (<+>) :: Rec as f -> Rec bs f -> Rec (as ++ bs) f
 RNil      <+> xs = xs
 (x :& xs) <+> ys =  x :& (xs <+> ys)
-infixl 8 <+>
+infixl 8  <+>
 
--- Shorthand for a record with a single field
+-- | Shorthand for a record with a single field. Lifts the field's
+-- value into the chosen functor automatically.
 (=:) :: Applicative f => sy ::: t -> t -> Rec '[sy ::: t] f
 a =: b = pure b :& RNil
 
--- Type level list append
+-- | Append for type-level lists.
 type family (as :: [*]) ++ (bs :: [*]) :: [*]
 type instance '[] ++ bs = bs
 type instance (a ': as) ++ bs  = a ': (as ++ bs)
 
--- Type Class Instances
+
 instance Show (Rec '[] f) where
   show RNil = "{}"
-
 instance (SingI sy, Show (g t), Show (Rec fs g)) => Show (Rec ((sy ::: t) ': fs) g) where
-  show (x :& xs) = show (Field :: sy ::: t) ++ " :=: " ++ show x ++ ", " ++ show xs where
+  show (x :& xs) = show (Field :: sy ::: t) ++ " :=: " ++ show x ++ ", " ++ show xs
 
+
 instance Eq (Rec '[] f) where
   _ == _ = True
 instance (Eq (g t), Eq (Rec fs g)) => Eq (Rec ((s ::: t) ': fs) g) where
   (x :& xs) == (y :& ys) = (x == y) && (xs == ys)
 
+-- | Records can be applied to each other.
 instance Apply (~>) (Rec rs) where
   RNil <<*>> RNil = RNil
   (f :& fs) <<*>> (x :& xs) = runNT f x :& (fs <<*>> xs)
 
+-- | Records may be 'run' to accumulate the effects of their fields.
 instance Run (Rec rs) where
   run RNil      = pure RNil
   run (x :& xs) = (:&) <$> (pure <$> x) <*> run xs
 
+-- | We provide a 'Show' instance for 'Identity'.
 instance Show a => Show (Identity a) where
   show (Identity x) = show x
-
-
-{-
-ex :: Rec Name Identity
-ex = Identity "jon"
-  :& Identity "sterling"
-  :& Identity 20
-  :& RNil
-
-verifyFirst = NT $ \str -> Failure ["asdfadS"]
-verifyLast = NT $ \str -> Failure ["uhoh"]
-verifyAge = NT $ \_ -> Failure ["uhoh"]
-
-ex2 :: Rec Name (Identity ~> Result [String])
-ex2 = verifyFirst
-    :& verifyLast
-    :& verifyAge
-    :& RNil
-
-ex3 = ex2 <<*>> ex
-ex4 = run ex3
--}
diff --git a/Data/Vinyl/Relation.hs b/Data/Vinyl/Relation.hs
--- a/Data/Vinyl/Relation.hs
+++ b/Data/Vinyl/Relation.hs
@@ -25,20 +25,20 @@
 
 import           GHC.Prim             (Constraint)
 
--- A subtyping relation
+-- | A subtyping relation.
 class (IsSubtype r1 r2) => r1 <: r2 where
   cast :: r1 -> r2
 
--- On record is a subtype of another if the fields of the latter are a
+-- | One record is a subtype of another if the fields of the latter are a
 -- subset of the fields of the former.
 type family IsSubtype r1 r2 :: Constraint
 type instance IsSubtype (Rec ss f) (Rec ts f) = ISubset ts ss
 
--- If two records types are subtypes of each other, that means that they
+-- | If two records types are subtypes of each other, that means that they
 -- differ only in order of fields.
 type r1 :~: r2 = (r1 <: r2, r2 <: r1)
 
--- Term-level record congruence
+-- | Term-level record congruence.
 (~=) :: (Eq a, a :~: b) => a -> b -> Bool
 x ~= y = x == (cast y)
 
@@ -50,7 +50,7 @@
     where field = lookupField (implicitly :: Elem y xs) r
 
 lookupField :: Elem x xs -> Rec xs f -> x
-lookupField Here (_ :& _)       = Field
+lookupField Here      (_ :& _)  = Field
 lookupField (There p) (_ :& xs) = lookupField p xs
 
 rIso :: (r1 :~: r2) => SimpleIso r1 r2
diff --git a/Data/Vinyl/Validation.hs b/Data/Vinyl/Validation.hs
--- a/Data/Vinyl/Validation.hs
+++ b/Data/Vinyl/Validation.hs
@@ -2,25 +2,30 @@
 
 module Data.Vinyl.Validation where
 
-import Data.Vinyl.Classes
-import Control.Applicative
-import Control.Monad.Identity
-import Data.Monoid
+import           Control.Applicative
+import           Control.Monad.Identity
+import           Data.Monoid
+import           Data.Vinyl.Classes
 
+-- | A type which is similar to 'Either', except that it has a
+-- slightly different Applicative instance.
 data Result e a
   = Failure e
   | Success a
   deriving (Show, Eq)
 
+-- | Validators transform identities into results.
 type Validator e = Identity ~> Result e
 
 instance Functor (Result e) where
-  fmap f (Success x) = Success (f x)
+  fmap f (Success x) = Success $ f x
   fmap f (Failure e) = Failure e
 
+-- | The 'Applicative' instance to 'Result' relies on its error type
+-- being a 'Monoid'. That way, it can accumulate errors.
 instance Monoid e => Applicative (Result e) where
   pure = Success
-  (Success f) <*> (Success x)  = Success (f x)
+  (Success f) <*> (Success x)  = Success $ f x
   (Failure e) <*> (Success x)  = Failure e
   (Success f) <*> (Failure e)  = Failure e
-  (Failure e) <*> (Failure e') = Failure (e <> e')
+  (Failure e) <*> (Failure e') = Failure $ e <> e'
diff --git a/Data/Vinyl/Witnesses.hs b/Data/Vinyl/Witnesses.hs
--- a/Data/Vinyl/Witnesses.hs
+++ b/Data/Vinyl/Witnesses.hs
@@ -13,18 +13,23 @@
 class Implicit p where
   implicitly :: p
 
-type IElem x xs = Implicit (Elem x xs)
+-- | An inductive list membership proposition.
 data Elem :: k -> [k] -> * where
   Here  :: Elem x (x ': xs)
   There :: Elem x xs -> Elem x (y ': xs)
 
-type ISubset xs ys = Implicit (Subset xs ys)
+-- | A constraint for implicit resolution of list membership proofs.
+type IElem x xs = Implicit (Elem x xs)
+
+-- | An inductive list subset relation.
 data Subset :: [k] -> [k] -> * where
   SubsetNil  :: Subset '[] xs
-  SubsetCons ::
-    Elem x ys ->
-    Subset xs ys ->
-    Subset (x ': xs) ys
+  SubsetCons :: Elem x ys
+             -> Subset xs ys
+             -> Subset (x ': xs) ys
+
+-- | A constraint for implicit resolution of list subset proofs.
+type ISubset xs ys = Implicit (Subset xs ys)
 
 instance Implicit (Elem x (x ': xs)) where
   implicitly = Here
diff --git a/vinyl.cabal b/vinyl.cabal
--- a/vinyl.cabal
+++ b/vinyl.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                vinyl
-version:             0.1.1.0
+version:             0.1.1.1
 synopsis:            Extensible Records
 -- description:
 license:             MIT