diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,10 @@
 
+## 0.2.1.0 [2018-03-20]
+- Bug Fix: The type of 'update' for both Record and Variant now enforce the newly inserted type is correct.
+- New: Add 'restrict' and 'split' for Variants.  
+- - Removed 'restrict' from Data.Row export list.
+- New: Added support for universally quantified rows: 'mapForall' and 'uniqueMap'.
+- Added very simple test suite.
+
 ## 0.2.0.0 [2018-02-12]
 - Initial Release
diff --git a/Data/Row.hs b/Data/Row.hs
--- a/Data/Row.hs
+++ b/Data/Row.hs
@@ -34,7 +34,6 @@
   , type (.==), (.==), pattern (:==), unSingleton
   -- ** Restriction
   , type (.-), (.-)
-  , restrict
   -- ** Query
   , type (.!), (.!)
   -- ** Disjoint union
diff --git a/Data/Row/Internal.hs b/Data/Row/Internal.hs
--- a/Data/Row/Internal.hs
+++ b/Data/Row/Internal.hs
@@ -30,9 +30,15 @@
   , toKey
   , type (≈)
   , WellBehaved, AllUniqueLabels, Zip, Map, Subset, Disjoint
+
+  , mapForall
+  , uniqueMap
+  , IsA(..)
+  , As(..)
   )
 where
 
+import Data.Constraint
 import Data.Functor.Const
 import Data.Proxy
 import Data.String (IsString (fromString))
@@ -40,7 +46,8 @@
 import qualified Data.Text as Text
 import Data.Type.Equality (type (==))
 
-import GHC.Exts -- needed for constraints kinds
+import qualified Unsafe.Coerce as UNSAFE
+
 import GHC.OverloadedLabels
 import GHC.TypeLits
 import qualified GHC.TypeLits as TL
@@ -193,6 +200,39 @@
                -- ^ The fold
             -> f r  -- ^ The input structure
             -> g r
+
+-- * Says that there exists a `t` such that `a ~ f t` and `c t`.
+data As c f a where
+  As :: forall c f a t. (a ~ f t, c t) => As c f a
+
+class IsA c f a where
+  as :: As c f a
+
+instance c a => IsA c f (f a) where
+  as = As
+
+newtype MapForall c f (r :: Row *) = MapForall { unMapForall :: Dict (Forall (Map f r) (IsA c f)) }
+
+-- | This allows us to derive a `Forall (Map f r) ..` from a `Forall r ..`.
+mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f)
+mapForall = Sub $ unMapForall $ metamorph @ρ @c @(Const ()) @(MapForall c f) @(Const ()) Proxy empty uncons cons $ Const ()
+  where empty :: Const () Empty -> MapForall c f Empty
+        empty _ = MapForall Dict
+
+        uncons :: forall l t r. (KnownSymbol l, c t)
+               => Label l -> Const () ('R (l :-> t ': r)) -> (Const () t, Const () ('R r))
+        uncons _ _ = (Const (), Const ())
+
+        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FoldStep ℓ τ ρ)
+             => Label ℓ -> Const () τ -> MapForall c f ('R ρ)
+             -> MapForall c f ('R (ℓ :-> τ ': ρ))
+        cons _ _ (MapForall Dict) =
+           case UNSAFE.unsafeCoerce @(Dict Unconstrained) @(Dict (FoldStep ℓ (f τ) (MapR f ρ))) Dict of
+             Dict -> MapForall Dict
+
+-- | Map preserves uniqueness of labels.
+uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)
+uniqueMap = Sub $ UNSAFE.unsafeCoerce @(Dict Unconstrained) Dict
 
 instance Forall (R '[]) c where
   {-# INLINE metamorph #-}
diff --git a/Data/Row/Records.hs b/Data/Row/Records.hs
--- a/Data/Row/Records.hs
+++ b/Data/Row/Records.hs
@@ -25,7 +25,7 @@
   , empty
   , type (.==), (.==), pattern (:==), unSingleton
   , default', defaultA
-  , fromLabels, fromLabelsA
+  , fromLabels, fromLabelsA, fromLabelsMapA
   -- ** Extension
   , extend, Extend, Lacks, type (.\)
   -- ** Restriction
@@ -62,6 +62,7 @@
 
 import Control.DeepSeq (NFData(..), deepseq)
 
+import qualified Data.Constraint as Constraint
 import Data.Functor.Compose
 import Data.Functor.Const
 import Data.Functor.Identity
@@ -145,7 +146,7 @@
 extend (toKey -> l) a (OR m) = OR $ M.insert l (HideType a) m
 
 -- | Update the value associated with the label.
-update :: KnownSymbol l => Label l -> a -> Rec r -> Rec r
+update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Rec r -> Rec r
 update (toKey -> l) a (OR m) = OR $ M.adjust f l m where f = const (HideType a)
 
 -- | Focus on the value associated with the label.
@@ -376,3 +377,11 @@
                => Label ℓ -> Const () τ -> Compose f Rec ('R ρ) -> Compose f Rec ('R (ℓ :-> τ ': ρ))
         doCons l _ (Compose r) = Compose $ unsafeInjectFront l <$> mk l <*> r
 
+-- | Initialize a record that is produced by a `Map`.
+fromLabelsMapA :: forall c f g ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
+               => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Rec (Map g ρ))
+fromLabelsMapA f = fromLabelsA @(IsA c g) @f @(Map g ρ) inner
+                Constraint.\\ mapForall @g @c @ρ
+                Constraint.\\ uniqueMap @g @ρ
+   where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a
+         inner l = case as @c @g @a of As -> f l
diff --git a/Data/Row/Variants.hs b/Data/Row/Variants.hs
--- a/Data/Row/Variants.hs
+++ b/Data/Row/Variants.hs
@@ -22,6 +22,7 @@
   , update, focus, Modify, rename, Rename
   -- * Destruction
   , impossible, trial, trial', multiTrial, view
+  , restrict, split
   -- ** Types for destruction
   , type (.!), type (.-), type (.\\), type (.==)
   -- * Row operations
@@ -126,7 +127,7 @@
 
 -- | If the variant exists at the given label, update it to the given value.
 -- Otherwise, do nothing.
-update :: KnownSymbol l => Label l -> a -> Var r -> Var r
+update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Var r -> Var r
 update (toKey -> l') a (OneOf l x) = OneOf l $ if l == l' then HideType a else x
 
 -- | If the variant exists at the given label, focus on the value associated with it.
@@ -160,6 +161,15 @@
 -- myShow (view y -> Just s) = "String of "++s @
 view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)
 view = flip trial'
+
+-- | Split a variant into two sub-variants.
+split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var s) (Var (r .\\ s))
+split (OneOf l a) | l `elem` labels @s @Unconstrained1 = Left  $ OneOf l a
+                  | otherwise                          = Right $ OneOf l a
+
+-- | Arbitrary variant restriction.  Turn a variant into a subset of itself.
+restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r)
+restrict = either Just (pure Nothing) . split
 
 
 {--------------------------------------------------------------------
diff --git a/Examples.lhs b/Examples.lhs
deleted file mode 100644
--- a/Examples.lhs
+++ /dev/null
@@ -1,390 +0,0 @@
-> {-# LANGUAGE OverloadedLabels #-}
-> module Examples where
->
-> import Data.Row
-> import qualified Data.Row.Records as Rec
-> import qualified Data.Row.Variants as Var
-
-In this example file, we will explore how to create and use records and variants.
-
---------------------------------------------------------------------------------
-  LABELS
---------------------------------------------------------------------------------
-
-To begin, we will briefly discuss creating labels -- their use will follow.
-
-The most basic way to create a label is through construction with a type signature:
-
- x = Label :: Label "x"
-
-With the above definition, x is a label for the field x.  Using type applications,
-this can be shortened to:
-
- x = Label @"x"
-
-And with OverloadedLabels, one can just write:
-
- #x
-
-We will use the OverloadedLabels notation in these examples.
-
---------------------------------------------------------------------------------
-  LENS
---------------------------------------------------------------------------------
-
-Records and variants play nicely with the lens library if we additionally import
-Data.Row.Lens from the row-types-lens "orphan instance" library.  Each overloaded
-label is also a Lens for a record and a Traversal for variants.  Thus, .! can be
-replaced with ^. and trial can be made infix with ^?.  Additionally, update
-can be made infix:
-
-update #x v r === r & #x .~ v
-
-And because of the power of lens, it's easy to make modifications rather than
-just update:
-
-update #x (f $ r .! #x) r === r & #x %~ f
-
-Lens is not included with row-types by default, but using it can make row-types
-much friendlier.
-
---------------------------------------------------------------------------------
-  RECORDS
---------------------------------------------------------------------------------
-
-With some labels defined, let's begin with records.  To start, let's create a
-record representing the Cartesian coordinates of the origin.  To do this,
-we use the .== operator to initialize values in a record, and we separate each
-initialized value with the .+ operator.Notice that the value level code uses the
-same operators as the type level code.
-
-> origin :: Rec ("x" .== Double .+ "y" .== Double )
-> origin = #x .== 0 .+ #y .== 0
-
-Note that, although we wrote the type explicitly, GHC has no problem inferring
-it exactly.
-
-If we show this at the repl, we see:
-λ> origin
-{ x=0.0, y=0.0 }
-
-Of course, as an extensible record, the order that we build it shouldn't matter,
-and indeed, it doesn't.  Consider the following variation:
-
-> origin' :: Rec ("y" .== Double .+ "x" .== Double)
-> origin' = #y .== 0 .+ #x .== 0
-
-If we show this at the repl, we see:
-
-λ> origin2
-{ x=0.0, y=0.0 }
-
-Indeed, the two values are indistinguishable:
-
-λ> origin == origin'
-True
-
-Now, let's expand upon our record.  Why stop at two dimensions when we can make
-a record in three dimensions.
-
-> origin3D = #z .== 0.0 .+ origin
-
-Once again, the type is inferred for us, and the record is exactly as expected.
-
-In fact, we can do this generally.  The following function takes a name and a
-record and adds the "name" field to that record with the given name.
-
-> named :: r .\ "name" => a -> Rec r -> Rec ("name" .== a .+ r)
-> named s r = #name .== s .+ r
-
-Note that we require that the record we are naming must not have a "name" field
-already.  Overlapping labels within a single record/variant is strictly forbidden.
-
-Let's say we want to get the values out of the record.  Simple selection is achieved
-with the .! operator, like so:
-
-λ> origin .! #x
-0.0
-
-and we can use this to write whatever we want.  Here is a function for calculating
-Euclidean distance from the origin to a point:
-
-> distance :: (Floating t, r .! "y" ≈ t, r .! "x" ≈ t) => Rec r -> t
-> distance p = sqrt $ p .! #x * p .! #x + p .! #y * p .! #y
-
-Once again, the type of distance is entirely inferrable, but we write it here for
-convenience.  This works exactly as expected:
-
-λ> distance origin
-0.0
-λ> distance origin3D
-0.0
-λ> distance (named "2D" origin)
-0.0
-
-Of course, that wasn't very interesting when our only points are at the origin
-already.  We could make new records representing new points, but instead, let's
-write a function to move the points we have:
-
-> move :: (Num (r .! "x"), Num (r .! "y"))
->      => Rec r -> r .! "x" -> r .! "y" -> Rec r
-> move p dx dy = Rec.update #x (p .! #x + dx) $
->                Rec.update #y (p .! #y + dy) p
-
-Here, we're using the Rec.update operator to update the value at the label x by
-adding dx to it, and then we do the same for y.
-We can see it work in practice:
-
-λ> move origin 3 4
-{ x=3.0, y=4.0 }
-λ> distance (move origin 3 4)
-5.0
-λ> distance (move (named "2D" origin3D) 5 12)
-13.0
-
-Note that if we were using row-types-lens and the lens library, we could write
-move as:
-
-move p dx dy = p & #x +~ dx & #y +~ dy
-
-So far, we created an origin point in 2d and then one in 3d, but what if we are
-adventurous mathematicians who want to have points in a space with some arbitrary
-number of dimensions.  We could write out each of the 0s necessary, but there's
-an easier way to initialize a record:
-
-> origin4 :: Rec ("x" .== Double .+ "y" .== Double .+ "z" .== Double .+ "w" .== Double)
-> origin4 = Rec.default' @Num 0
-
-Finally, we have come to a case where GHC cannot infer the type signature, and how
-could it!  The type is providing crucial information about the shape of the record.
-Regardless, with the type provided, it works exactly as expected:
-
-λ> origin4
-{ w=0.0, x=0.0, y=0.0, z=0.0 }
-
-While we have added names or further fields, we can also choose to forget
-information in a record.  To remove a particular label, one can use the .-
-operator, like so:
-
-> unName :: HasType "name" a r => Rec r -> Rec (r .- "name")
-> unName r = r .- #name
-
-For larger changes, it is easier to use the restrict function.  The following
-function will take a record that contains both an x and y coordinate and remove
-the rest of the fields from it.
-
-> get2D :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)
->       => Rec (r .+ rest)
->       -> Rec r
-> get2D r = restrict r
-
-GHC is a little finicky about the type operators and constraints -- indeed, this
-type signature will fail to type check if the parentheses around
-  "x" .== Double .+ "y" .== Double
-in the argument are missing.  Of course, a type signature is not necessary when
-using type applications, and the function can instead be written as:
-
-> get2D' r = restrict @("x" .== Double .+ "y" .== Double) r
-
-with no trouble.  Yet another altnerative is to match directly on the values desired
-using the :== and :+ record patterns:
-
-> get2D'' :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)
->         => Rec (r .+ rest)
->         -> Rec r
-> get2D'' ((Label :: Label "x") :== n1 :+ (Label :: Label "y") :== n2 :+ _)
->           = #x .== n1 .+ #y .== n2
-
-(Note that overloaded labels cannot be used in the patterns, so the notation is
-unfortunately bloated by types.  Also, the type operators are left associated,
-so the "_" must go on the right, and the type signature is unforunately necessary.)
-
-All three of the get2D functions behave the same.
-
---------------------------------------------------------------------------------
-  VARIANTS
---------------------------------------------------------------------------------
-Let's move on from records to variants.  In many ways, variants are quite similar,
-as might be expected given that variants are dual to records.  The types look
-almost the same, and some of the operators are shared as well.  However,
-construction and destruction are obviously different.
-
-Creating a variant can be done with IsJust:
-
-> v,v' :: Var ("y" .== String .+ "x" .== Integer)
-> v  = IsJust #x 1
-> v' = IsJust #y "Foo"
-
-Here, the type is necessary to specify what concrete type the variant is (when
-using AllowAmbiguousTypes, the type is not always needed, but it would be needed
-to e.g. show the variant).  In the simple case of a variant of just one type,
-the simpler singleton function can be used:
-
-> v2 = Var.singleton #x 1
-
-Now, the type can be easily derived by GHC.  We can show variants as easily as
-records:
-
-λ> v
-{x=1}
-λ> v'
-{y="Foo"}
-λ> v2
-{x=1}
-
-Once created, a variant can be expanded by using type applications and the
-diversify function.
-
-> v3 = diversify @("y" .== String) v2
-> v4 = diversify @("y" .== String .+ "z" .== Double) v2
-
-λ> :t v4
-v4 :: Var ('R '["x" ':-> Integer, "y" ':-> String, "z" ':-> Double])
-λ> v == v3
-True
-
-Doing the above equality test does raise the question of how equality works on
-variants.  For instance, v2 and v3 both look the same when you show them, and they
-both have the same value inside, but can we test them for equality?  Indeed, we can't,
-precisely because their types are different: it is a type error to even try to
-check whether they're equal:
-
-λ> v2 == v3
-error:
-    • Couldn't match type ‘'["y" ':-> [Char]]’ with ‘'[]’
-      Expected type: Var ('R '["x" ':-> Integer])
-        Actual type: Var ('R '["x" ':-> Integer] .+ ("y" .== String))
-    • In the second argument of ‘(==)’, namely ‘v3’
-      In the expression: v2 == v3
-      In an equation for ‘it’: it = v2 == v3
-
-This may look a little scary, but it's actually a pretty useful message.  Essentially,
-it's expecting a variant that can only be an Integer at label "x", but it found one
-that could also be a String at label "y".  So, comparing v2 and v3 is not allowed,
-but since v3 now has the same labels as v1, that comparison is fine:
-
-λ> v == v3
-True
-λ> v == IsJust #x 3
-False
-λ> v == v'
-False
-λ> v == IsJust #y "fail"
-False
-
-(Also note here that using IsJust without a type signature is fine because the correct
-type can be easily inferred due to v's type.)
-
-What can you do with a variant?  The only way to really use one is to get the value
-out, and to do that, you must trial it:
-
-λ> trial v #x
-Left 1
-λ> trial v #y
-Right {x=1}
-λ> trial v' #x
-Right {y="Foo"}
-λ> trial v' #y
-Left "Foo"
-
-If trialing at a label l succeeds, then it provides a Left value of the value at l.
-If not, it provides a Right value of the variant with this label removed---since the
-trial failed, we now can be sure that the value is not from l.
-
-For ease of use in view patterns, Variants also exposes the view function.
-(If using lens, this can be replaced with preview.)  With it, we can write a
-function like this:
-
-> myShow :: (r .! "y" ≈ String, Show (r .! "x")) => Var r -> String
-> myShow (Var.view #x -> Just n) = "Int of "++show n
-> myShow (Var.view #y -> Just s) = "String of "++s
-> myShow _ = "Unknown"
-
-λ> myShow v
-"Int of 1"
-λ> myShow v'
-"String of Foo"
-λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))
-"Unknown"
-
-This can also be achieved with the IsJust pattern synonym in much the same way:
-
-> myShow' :: (WellBehaved r, r .! "y" ≈ String, Show (r .! "x")) => Var r -> String
-> myShow' (IsJust (Label :: Label "x") n) = "Int of "++show n
-> myShow' (IsJust (Label :: Label "y") s) = "String of "++s
-> myShow' _ = "Unknown"
-
-In either case, the type signature is once again totally derivable.
-
-There are two minor annoyances with this.  First, it's fairly common to want to define
-a function like myShow to be exhaustive in the variant's cases, but to do this,
-you must manually provide a type signature:
-
-> myShowRestricted :: Var ("y" .== String .+ "x" .== Integer) -> String
-> myShowRestricted (Var.view #x -> Just n) = "Int of "++show n
-> myShowRestricted (Var.view #y -> Just s) = "String of "++s
-> myShowRestricted _ = error "Unreachable"
-
-The second blemish can be seen in this restricted version of myShow.  Even though
-we know from the type that we've covered all the posibilities of the variant, GHC
-will generate a "non-exhaustive pattern match" warning without the final line.
-(This is true for the pattern synonym version too.)
-
-One way to avoid this problem is to use switch.  The switch operator takes a variant
-and a record such that for each label that the variant has, the record has a function
-at that label that consumes the value the variant has and produces a value in a
-common type.  Essentially, switch "applies" the variant to the record to produce
-an output value.
-
-> --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String
-> myShowRestricted' v = switch v $
->      #x .== (\n -> "Int of "++show n)
->   .+ #y .== (\s -> "String of "++s)
-
-This version of myShow needs neither a type signature (it is inferred exactly) nor
-a default "unreachable" case.  However, we no longer have the benefit of Haskell's
-standard pattern matching.
-
-
-
-A more powerful version of trial is multiTrial, which tests for multiple labels
-at once.  With this, you can wholesale change the type of the variant to any (valid)
-variant type you would like.  Of course, there needs to be a recourse if the variant
-you provide is not expressible in the type you want, so multiTrial returns an Either
-of the type you want or a Variant of the leftovers.  Consider the examples:
-
-λ> :t multiTrial @("x" .== Double .+ "y" .== String) v
-multiTrial @("x" .== Double .+ "y" .== String) v
-  :: Either
-       (Var ('R '["x" ':-> Double, "y" ':-> String]))
-       (Var ('R '["x" ':-> Integer]))
-λ> multiTrial @("x" .== Double .+ "y" .== String) v
-Right {x=1}
-
-λ> :t multiTrial @("x" .== Double .+ "y" .== String) v'
-multiTrial @("x" .== Double .+ "y" .== String) v'
-  :: Either
-       (Var ('R '["x" ':-> Double, "y" ':-> String]))
-       (Var ('R '["x" ':-> Integer]))
-λ> multiTrial @("x" .== Double .+ "y" .== String) v'
-Left {y="Foo"}
-
-Thus, multiTrial can be used not only to arbitrarily split apart a variant, but
-also to change unused label associations (in this case, we changed the variant
-from one where "x" is an Integer to one where it's a Double).
-
-
-Here are two functions you can define over variants.  The type constraints are a little
-ugly (the type equalities are necessary but annoying).
-
-> also :: Disjoint xs ys
->      => (Var xs -> a)
->      -> (Var ys -> a)
->      -> Var (xs .+ ys) -> a
-> also f1 f2 e = case multiTrial e of
->   Left  e' -> f1 e'
->   Right e' -> f2 e'
-
-> joinVarLists :: forall x y. (WellBehaved (x .+ y), x .+ y ≈ y .+ x)
->              => [Var x] -> [Var y] -> [Var (x .+ y)]
-> joinVarLists xs ys = map (diversify @y) xs ++ map (diversify @x) ys
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -3,7 +3,7 @@
 
 Row-types is a library of open records and variants for Haskell using closed
 type families and type literals (among other things...).
-See [Examples.lhs](https://raw.githubusercontent.com/target/row-types/master/Examples.lhs)
+See [examples/Examples.lhs](https://raw.githubusercontent.com/target/row-types/master/examples/Examples.lhs)
 for an overview of how this library can be used.
 
 This work is a branch from CTRex [1,2] with other inspiration from data-diverse [3].
diff --git a/examples/Examples.lhs b/examples/Examples.lhs
new file mode 100644
--- /dev/null
+++ b/examples/Examples.lhs
@@ -0,0 +1,390 @@
+> {-# LANGUAGE OverloadedLabels #-}
+> module Examples where
+>
+> import Data.Row
+> import qualified Data.Row.Records as Rec
+> import qualified Data.Row.Variants as Var
+
+In this example file, we will explore how to create and use records and variants.
+
+--------------------------------------------------------------------------------
+  LABELS
+--------------------------------------------------------------------------------
+
+To begin, we will briefly discuss creating labels -- their use will follow.
+
+The most basic way to create a label is through construction with a type signature:
+
+ x = Label :: Label "x"
+
+With the above definition, x is a label for the field x.  Using type applications,
+this can be shortened to:
+
+ x = Label @"x"
+
+And with OverloadedLabels, one can just write:
+
+ #x
+
+We will use the OverloadedLabels notation in these examples.
+
+--------------------------------------------------------------------------------
+  LENS
+--------------------------------------------------------------------------------
+
+Records and variants play nicely with the lens library if we additionally import
+Data.Row.Lens from the row-types-lens "orphan instance" library.  Each overloaded
+label is also a Lens for a record and a Traversal for variants.  Thus, .! can be
+replaced with ^. and trial can be made infix with ^?.  Additionally, update
+can be made infix:
+
+update #x v r === r & #x .~ v
+
+And because of the power of lens, it's easy to make modifications rather than
+just update:
+
+update #x (f $ r .! #x) r === r & #x %~ f
+
+Lens is not included with row-types by default, but using it can make row-types
+much friendlier.
+
+--------------------------------------------------------------------------------
+  RECORDS
+--------------------------------------------------------------------------------
+
+With some labels defined, let's begin with records.  To start, let's create a
+record representing the Cartesian coordinates of the origin.  To do this,
+we use the .== operator to initialize values in a record, and we separate each
+initialized value with the .+ operator.Notice that the value level code uses the
+same operators as the type level code.
+
+> origin :: Rec ("x" .== Double .+ "y" .== Double )
+> origin = #x .== 0 .+ #y .== 0
+
+Note that, although we wrote the type explicitly, GHC has no problem inferring
+it exactly.
+
+If we show this at the repl, we see:
+λ> origin
+{ x=0.0, y=0.0 }
+
+Of course, as an extensible record, the order that we build it shouldn't matter,
+and indeed, it doesn't.  Consider the following variation:
+
+> origin' :: Rec ("y" .== Double .+ "x" .== Double)
+> origin' = #y .== 0 .+ #x .== 0
+
+If we show this at the repl, we see:
+
+λ> origin2
+{ x=0.0, y=0.0 }
+
+Indeed, the two values are indistinguishable:
+
+λ> origin == origin'
+True
+
+Now, let's expand upon our record.  Why stop at two dimensions when we can make
+a record in three dimensions.
+
+> origin3D = #z .== 0.0 .+ origin
+
+Once again, the type is inferred for us, and the record is exactly as expected.
+
+In fact, we can do this generally.  The following function takes a name and a
+record and adds the "name" field to that record with the given name.
+
+> named :: r .\ "name" => a -> Rec r -> Rec ("name" .== a .+ r)
+> named s r = #name .== s .+ r
+
+Note that we require that the record we are naming must not have a "name" field
+already.  Overlapping labels within a single record/variant is strictly forbidden.
+
+Let's say we want to get the values out of the record.  Simple selection is achieved
+with the .! operator, like so:
+
+λ> origin .! #x
+0.0
+
+and we can use this to write whatever we want.  Here is a function for calculating
+Euclidean distance from the origin to a point:
+
+> distance :: (Floating t, r .! "y" ≈ t, r .! "x" ≈ t) => Rec r -> t
+> distance p = sqrt $ p .! #x * p .! #x + p .! #y * p .! #y
+
+Once again, the type of distance is entirely inferrable, but we write it here for
+convenience.  This works exactly as expected:
+
+λ> distance origin
+0.0
+λ> distance origin3D
+0.0
+λ> distance (named "2D" origin)
+0.0
+
+Of course, that wasn't very interesting when our only points are at the origin
+already.  We could make new records representing new points, but instead, let's
+write a function to move the points we have:
+
+> move :: (Num (r .! "x"), Num (r .! "y"))
+>      => Rec r -> r .! "x" -> r .! "y" -> Rec r
+> move p dx dy = Rec.update #x (p .! #x + dx) $
+>                Rec.update #y (p .! #y + dy) p
+
+Here, we're using the Rec.update operator to update the value at the label x by
+adding dx to it, and then we do the same for y.
+We can see it work in practice:
+
+λ> move origin 3 4
+{ x=3.0, y=4.0 }
+λ> distance (move origin 3 4)
+5.0
+λ> distance (move (named "2D" origin3D) 5 12)
+13.0
+
+Note that if we were using row-types-lens and the lens library, we could write
+move as:
+
+move p dx dy = p & #x +~ dx & #y +~ dy
+
+So far, we created an origin point in 2d and then one in 3d, but what if we are
+adventurous mathematicians who want to have points in a space with some arbitrary
+number of dimensions.  We could write out each of the 0s necessary, but there's
+an easier way to initialize a record:
+
+> origin4 :: Rec ("x" .== Double .+ "y" .== Double .+ "z" .== Double .+ "w" .== Double)
+> origin4 = Rec.default' @Num 0
+
+Finally, we have come to a case where GHC cannot infer the type signature, and how
+could it!  The type is providing crucial information about the shape of the record.
+Regardless, with the type provided, it works exactly as expected:
+
+λ> origin4
+{ w=0.0, x=0.0, y=0.0, z=0.0 }
+
+While we have added names or further fields, we can also choose to forget
+information in a record.  To remove a particular label, one can use the .-
+operator, like so:
+
+> unName :: HasType "name" a r => Rec r -> Rec (r .- "name")
+> unName r = r .- #name
+
+For larger changes, it is easier to use the restrict function.  The following
+function will take a record that contains both an x and y coordinate and remove
+the rest of the fields from it.
+
+> get2D :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)
+>       => Rec (r .+ rest)
+>       -> Rec r
+> get2D r = Rec.restrict r
+
+GHC is a little finicky about the type operators and constraints -- indeed, this
+type signature will fail to type check if the parentheses around
+  "x" .== Double .+ "y" .== Double
+in the argument are missing.  Of course, a type signature is not necessary when
+using type applications, and the function can instead be written as:
+
+> get2D' r = Rec.restrict @("x" .== Double .+ "y" .== Double) r
+
+with no trouble.  Yet another altnerative is to match directly on the values desired
+using the :== and :+ record patterns:
+
+> get2D'' :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)
+>         => Rec (r .+ rest)
+>         -> Rec r
+> get2D'' ((Label :: Label "x") :== n1 :+ (Label :: Label "y") :== n2 :+ _)
+>           = #x .== n1 .+ #y .== n2
+
+(Note that overloaded labels cannot be used in the patterns, so the notation is
+unfortunately bloated by types.  Also, the type operators are left associated,
+so the "_" must go on the right, and the type signature is unforunately necessary.)
+
+All three of the get2D functions behave the same.
+
+--------------------------------------------------------------------------------
+  VARIANTS
+--------------------------------------------------------------------------------
+Let's move on from records to variants.  In many ways, variants are quite similar,
+as might be expected given that variants are dual to records.  The types look
+almost the same, and some of the operators are shared as well.  However,
+construction and destruction are obviously different.
+
+Creating a variant can be done with IsJust:
+
+> v,v' :: Var ("y" .== String .+ "x" .== Integer)
+> v  = IsJust #x 1
+> v' = IsJust #y "Foo"
+
+Here, the type is necessary to specify what concrete type the variant is (when
+using AllowAmbiguousTypes, the type is not always needed, but it would be needed
+to e.g. show the variant).  In the simple case of a variant of just one type,
+the simpler singleton function can be used:
+
+> v2 = Var.singleton #x 1
+
+Now, the type can be easily derived by GHC.  We can show variants as easily as
+records:
+
+λ> v
+{x=1}
+λ> v'
+{y="Foo"}
+λ> v2
+{x=1}
+
+Once created, a variant can be expanded by using type applications and the
+diversify function.
+
+> v3 = diversify @("y" .== String) v2
+> v4 = diversify @("y" .== String .+ "z" .== Double) v2
+
+λ> :t v4
+v4 :: Var ('R '["x" ':-> Integer, "y" ':-> String, "z" ':-> Double])
+λ> v == v3
+True
+
+Doing the above equality test does raise the question of how equality works on
+variants.  For instance, v2 and v3 both look the same when you show them, and they
+both have the same value inside, but can we test them for equality?  Indeed, we can't,
+precisely because their types are different: it is a type error to even try to
+check whether they're equal:
+
+λ> v2 == v3
+error:
+    • Couldn't match type ‘'["y" ':-> [Char]]’ with ‘'[]’
+      Expected type: Var ('R '["x" ':-> Integer])
+        Actual type: Var ('R '["x" ':-> Integer] .+ ("y" .== String))
+    • In the second argument of ‘(==)’, namely ‘v3’
+      In the expression: v2 == v3
+      In an equation for ‘it’: it = v2 == v3
+
+This may look a little scary, but it's actually a pretty useful message.  Essentially,
+it's expecting a variant that can only be an Integer at label "x", but it found one
+that could also be a String at label "y".  So, comparing v2 and v3 is not allowed,
+but since v3 now has the same labels as v1, that comparison is fine:
+
+λ> v == v3
+True
+λ> v == IsJust #x 3
+False
+λ> v == v'
+False
+λ> v == IsJust #y "fail"
+False
+
+(Also note here that using IsJust without a type signature is fine because the correct
+type can be easily inferred due to v's type.)
+
+What can you do with a variant?  The only way to really use one is to get the value
+out, and to do that, you must trial it:
+
+λ> trial v #x
+Left 1
+λ> trial v #y
+Right {x=1}
+λ> trial v' #x
+Right {y="Foo"}
+λ> trial v' #y
+Left "Foo"
+
+If trialing at a label l succeeds, then it provides a Left value of the value at l.
+If not, it provides a Right value of the variant with this label removed---since the
+trial failed, we now can be sure that the value is not from l.
+
+For ease of use in view patterns, Variants also exposes the view function.
+(If using lens, this can be replaced with preview.)  With it, we can write a
+function like this:
+
+> myShow :: (r .! "y" ≈ String, Show (r .! "x")) => Var r -> String
+> myShow (Var.view #x -> Just n) = "Int of "++show n
+> myShow (Var.view #y -> Just s) = "String of "++s
+> myShow _ = "Unknown"
+
+λ> myShow v
+"Int of 1"
+λ> myShow v'
+"String of Foo"
+λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))
+"Unknown"
+
+This can also be achieved with the IsJust pattern synonym in much the same way:
+
+> myShow' :: (WellBehaved r, r .! "y" ≈ String, Show (r .! "x")) => Var r -> String
+> myShow' (IsJust (Label :: Label "x") n) = "Int of "++show n
+> myShow' (IsJust (Label :: Label "y") s) = "String of "++s
+> myShow' _ = "Unknown"
+
+In either case, the type signature is once again totally derivable.
+
+There are two minor annoyances with this.  First, it's fairly common to want to define
+a function like myShow to be exhaustive in the variant's cases, but to do this,
+you must manually provide a type signature:
+
+> myShowRestricted :: Var ("y" .== String .+ "x" .== Integer) -> String
+> myShowRestricted (Var.view #x -> Just n) = "Int of "++show n
+> myShowRestricted (Var.view #y -> Just s) = "String of "++s
+> myShowRestricted _ = error "Unreachable"
+
+The second blemish can be seen in this restricted version of myShow.  Even though
+we know from the type that we've covered all the posibilities of the variant, GHC
+will generate a "non-exhaustive pattern match" warning without the final line.
+(This is true for the pattern synonym version too.)
+
+One way to avoid this problem is to use switch.  The switch operator takes a variant
+and a record such that for each label that the variant has, the record has a function
+at that label that consumes the value the variant has and produces a value in a
+common type.  Essentially, switch "applies" the variant to the record to produce
+an output value.
+
+> --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String
+> myShowRestricted' v = switch v $
+>      #x .== (\n -> "Int of "++show n)
+>   .+ #y .== (\s -> "String of "++s)
+
+This version of myShow needs neither a type signature (it is inferred exactly) nor
+a default "unreachable" case.  However, we no longer have the benefit of Haskell's
+standard pattern matching.
+
+
+
+A more powerful version of trial is multiTrial, which tests for multiple labels
+at once.  With this, you can wholesale change the type of the variant to any (valid)
+variant type you would like.  Of course, there needs to be a recourse if the variant
+you provide is not expressible in the type you want, so multiTrial returns an Either
+of the type you want or a Variant of the leftovers.  Consider the examples:
+
+λ> :t multiTrial @("x" .== Double .+ "y" .== String) v
+multiTrial @("x" .== Double .+ "y" .== String) v
+  :: Either
+       (Var ('R '["x" ':-> Double, "y" ':-> String]))
+       (Var ('R '["x" ':-> Integer]))
+λ> multiTrial @("x" .== Double .+ "y" .== String) v
+Right {x=1}
+
+λ> :t multiTrial @("x" .== Double .+ "y" .== String) v'
+multiTrial @("x" .== Double .+ "y" .== String) v'
+  :: Either
+       (Var ('R '["x" ':-> Double, "y" ':-> String]))
+       (Var ('R '["x" ':-> Integer]))
+λ> multiTrial @("x" .== Double .+ "y" .== String) v'
+Left {y="Foo"}
+
+Thus, multiTrial can be used not only to arbitrarily split apart a variant, but
+also to change unused label associations (in this case, we changed the variant
+from one where "x" is an Integer to one where it's a Double).
+
+
+Here are two functions you can define over variants.  The type constraints are a little
+ugly (the type equalities are necessary but annoying).
+
+> also :: Disjoint xs ys
+>      => (Var xs -> a)
+>      -> (Var ys -> a)
+>      -> Var (xs .+ ys) -> a
+> also f1 f2 e = case multiTrial e of
+>   Left  e' -> f1 e'
+>   Right e' -> f2 e'
+
+> joinVarLists :: forall x y. (WellBehaved (x .+ y), x .+ y ≈ y .+ x)
+>              => [Var x] -> [Var y] -> [Var (x .+ y)]
+> joinVarLists xs ys = map (diversify @y) xs ++ map (diversify @x) ys
diff --git a/row-types.cabal b/row-types.cabal
--- a/row-types.cabal
+++ b/row-types.cabal
@@ -1,5 +1,5 @@
 Name:                row-types
-Version:             0.2.0.0
+Version:             0.2.1.0
 License:             MIT
 License-file:        LICENSE
 Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck
@@ -18,7 +18,7 @@
   label.
 
 extra-source-files:
-  Examples.lhs
+  examples/Examples.lhs
   README.md
   CHANGELOG.md
   LICENSE
@@ -26,6 +26,7 @@
 
 Library
   Build-Depends: base >= 2 && < 5,
+                 constraints,
                  deepseq >= 1.4,
                  hashable >= 1.2,
                  unordered-containers >= 0.2,
@@ -36,7 +37,6 @@
                  , Data.Row.Variants
                  , Data.Row.Switch
   ghc-options: -W
-  other-modules:
   Extensions: AllowAmbiguousTypes,
               ConstraintKinds,
               DataKinds,
@@ -78,6 +78,27 @@
               TypeApplications,
               TypeFamilies,
               TypeOperators
+
+test-suite test
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs: tests, examples
+  ghc-options: -W
+  other-modules: Examples
+  build-depends: base >= 2 && < 6
+               , row-types
+  Extensions: AllowAmbiguousTypes,
+              DataKinds,
+              FlexibleContexts,
+              OverloadedLabels,
+              PatternSynonyms,
+              RankNTypes,
+              ScopedTypeVariables,
+              TypeApplications,
+              TypeFamilies,
+              TypeOperators,
+              ViewPatterns
+
 
 source-repository head
     type:     git
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,6 @@
+
+module Main where
+
+import Examples ()
+
+main = putStrLn "Test passes if Examples.lhs type-checks."