diff --git a/Data/Row.hs b/Data/Row.hs
--- a/Data/Row.hs
+++ b/Data/Row.hs
@@ -41,7 +41,7 @@
   -- * Variant construction
   , pattern IsJust
   -- ** Restriction
-  , diversify
+  , diversify, type (.\/)
   -- ** Destruction
   , impossible, trial, trial', multiTrial
   , type (.\\)
diff --git a/Data/Row/Internal.hs b/Data/Row/Internal.hs
--- a/Data/Row/Internal.hs
+++ b/Data/Row/Internal.hs
@@ -20,9 +20,10 @@
   -- * Row Operations
   , Extend, Modify, Rename
   , type (.\), type (.!), type (.-), type (.+), type (.\\), type (.==)
+  , type (.\/)
   , Lacks, HasType
   -- * Row Classes
-  , Labels, labels
+  , Labels, labels, labels'
   , Forall(..), Forall2(..)
   , Unconstrained1
   -- * Helper functions
@@ -32,9 +33,12 @@
   , WellBehaved, AllUniqueLabels, Zip, Map, Subset, Disjoint
 
   , mapForall
+  , freeForall
   , uniqueMap
   , IsA(..)
   , As(..)
+
+  , FoldStep
   )
 where
 
@@ -142,6 +146,11 @@
 type family (l :: Row *) .\\ (r :: Row *) :: Row * where
   R l .\\ R r = R (Diff l r)
 
+-- | The minimum join of the two rows.
+type family (l :: Row *) .\/ (r :: Row *) where
+  R l .\/ R r = R (MinJoinR l r)
+
+
 {--------------------------------------------------------------------
   Syntactic sugar for record operations
 --------------------------------------------------------------------}
@@ -168,9 +177,7 @@
 -- | Proof that the given label is a valid candidate for the next step
 -- in a metamorph fold, i.e. it's not in the list yet and, when sorted,
 -- will be placed at the head.
-type FoldStep ℓ τ ρ = ( Inject (ℓ :-> τ) ρ ≈ ℓ :-> τ ': ρ
-                      , R ρ .\ ℓ
-                      )
+type FoldStep ℓ τ ρ = Inject (ℓ :-> τ) ρ ≈ ℓ :-> τ ': ρ
 
 -- | Any structure over a row in which every element is similarly constrained can
 --   be metamorphized into another structure over the same row.
@@ -201,16 +208,21 @@
             -> f r  -- ^ The input structure
             -> g r
 
--- * Says that there exists a `t` such that `a ~ f t` and `c t`.
+-- | This data type is used to for its ability to existentially bind a type
+-- variable.  Particularly, it says that for the type 'a', there exists a 't'
+-- such that 'a ~ f t' and 'c t' holds.
 data As c f a where
   As :: forall c f a t. (a ~ f t, c t) => As c f a
 
+-- | A class to capture the idea of 'As' so that it can be partially applied in
+-- a context.
 class IsA c f a where
   as :: As c f a
 
 instance c a => IsA c f (f a) where
   as = As
 
+-- | An internal type used by the 'metamorph' in 'mapForall'.
 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 ..`.
@@ -234,6 +246,10 @@
 uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)
 uniqueMap = Sub $ UNSAFE.unsafeCoerce @(Dict Unconstrained) Dict
 
+-- | Allow any 'Forall` over a row-type, be usable for 'Unconstrained1'.
+freeForall :: forall r c. Forall r c :- Forall r Unconstrained1
+freeForall = Sub $ UNSAFE.unsafeCoerce @(Dict (Forall r c)) Dict
+
 instance Forall (R '[]) c where
   {-# INLINE metamorph #-}
   metamorph _ empty _ _ = empty
@@ -316,7 +332,11 @@
   where doUncons _ _ = (Const (), Const ())
         doCons l _ (Const c) = Const $ show' l : c
 
+-- | Return a list of the labels in a row type and is specialized to the 'Unconstrained1' constraint.
+labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]
+labels' = labels @ρ @Unconstrained1
 
+
 {--------------------------------------------------------------------
   Convenient type families and classes
 --------------------------------------------------------------------}
@@ -425,16 +445,14 @@
                           :<>: ShowType r)
 
 type family LacksR (l :: Symbol) (r :: [LT *]) (r_orig :: [LT *]) :: Constraint where
-  LacksR l '[] r = Unconstrained
+  LacksR l '[] _ = Unconstrained
   LacksR l (l :-> t ': x) r = TypeError (TL.Text "The label " :<>: ShowType l
                                     :<>: TL.Text " already exists in " :<>: ShowType r)
-  LacksR l (p ': x) r = LacksR l x r
+  LacksR l (l' :-> _ ': x) r = Ifte (l <=.? l') Unconstrained (LacksR l x r)
 
 type family Merge (l :: [LT *]) (r :: [LT *]) where
   Merge '[] r = r
   Merge l '[] = l
-  Merge (h :-> a ': tl)   (h :-> a ': tr) =
-      (h :-> a ': Merge tl tr)
   Merge (h :-> a ': tl)   (h :-> b ': tr) =
     TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."
           :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")
@@ -442,6 +460,20 @@
       Ifte (hl <=.? hr)
       (hl :-> al ': Merge tl (hr :-> ar ': tr))
       (hr :-> ar ': Merge (hl :-> al ': tl) tr)
+
+type family MinJoinR (l :: [LT *]) (r :: [LT *]) where
+  MinJoinR '[] r = r
+  MinJoinR l '[] = l
+  MinJoinR (h :-> a ': tl)   (h :-> a ': tr) =
+      (h :-> a ': MinJoinR tl tr)
+  MinJoinR (h :-> a ': tl)   (h :-> b ': tr) =
+    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."
+          :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")
+  MinJoinR (hl :-> al ': tl) (hr :-> ar ': tr) =
+      Ifte (CmpSymbol hl hr == 'LT)
+      (hl :-> al ': MinJoinR tl (hr :-> ar ': tr))
+      (hr :-> ar ': MinJoinR (hl :-> al ': tl) tr)
+
 
 -- | Returns the left list with all of the elements from the right list removed.
 type family Diff (l :: [LT *]) (r :: [LT *]) where
diff --git a/Data/Row/Records.hs b/Data/Row/Records.hs
--- a/Data/Row/Records.hs
+++ b/Data/Row/Records.hs
@@ -47,12 +47,13 @@
   -- ** Zip
   , Zip, zip
   -- ** Sequence
-  , sequence
+  , sequence, sequence'
   -- ** Compose
   -- $compose
   , compose, uncompose
+  , compose', uncompose'
   -- ** Labels
-  , labels
+  , labels, labels'
   -- ** UNSAFE operations
   , unsafeRemove, unsafeInjectFront
   )
@@ -62,7 +63,7 @@
 
 import Control.DeepSeq (NFData(..), deepseq)
 
-import qualified Data.Constraint as Constraint
+import Data.Constraint ((\\))
 import Data.Functor.Compose
 import Data.Functor.Const
 import Data.Functor.Identity
@@ -70,7 +71,6 @@
 import Data.Hashable
 import Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as M
-import Data.List hiding (map, zip)
 import qualified Data.List as L
 import Data.Proxy
 import Data.String (IsString)
@@ -91,7 +91,7 @@
   OR :: HashMap Text HideType -> Rec r
 
 instance Forall r Show => Show (Rec r) where
-  show r = "{ " ++ intercalate ", " binds ++ " }"
+  show r = "{ " ++ L.intercalate ", " binds ++ " }"
     where binds = (\ (x, y) -> x ++ "=" ++ y) <$> eraseWithLabels @Show show r
 
 instance Forall r Eq => Eq (Rec r) where
@@ -292,14 +292,20 @@
 transform' :: forall r f g. Forall r Unconstrained1 => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
 transform' = transform @Unconstrained1 @r
 
--- | Applicative sequencing over a record
-sequence :: forall f r. (Forall r Unconstrained1, Applicative f) => Rec (Map f r) -> f (Rec r)
-sequence = getCompose . metamorph @r @Unconstrained1 @(RMap f) @(Compose f Rec) @f Proxy doNil doUncons doCons . RMap
+-- | A version of 'sequence' in which the constraint for 'Forall' can be chosen.
+sequence' :: forall f r c. (Forall r c, Applicative f)
+          => Rec (Map f r) -> f (Rec r)
+sequence' = getCompose . metamorph @r @c @(RMap f) @(Compose f Rec) @f Proxy doNil doUncons doCons . RMap
   where
     doNil _ = Compose (pure empty)
     doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)
     doCons l fv (Compose fr) = Compose $ unsafeInjectFront l <$> fv <*> fr
 
+-- | Applicative sequencing over a record.
+sequence :: forall f r. (Forall r Unconstrained1, Applicative f)
+         => Rec (Map f r) -> f (Rec r)
+sequence = sequence' @_ @_ @Unconstrained1
+
 -- $compose
 -- We can easily convert between mapping two functors over the types of a row
 -- and mapping the composition of the two functors.  The following two functions
@@ -309,25 +315,38 @@
 --
 -- >>> uncompose . compose = id
 
--- | Convert from a record where two functors have been mapped over the types to
--- one where the composition of the two functors is mapped over the types.
-compose :: forall (f :: * -> *) g r . Forall r Unconstrained1 => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
-compose = unRMap . metamorph @r @Unconstrained1 @(RMap2 f g) @(RMap (Compose f g)) Proxy doNil doUncons doCons . RMap2
+-- | A version of 'compose' in which the constraint for 'Forall' can be chosen.
+compose' :: forall c (f :: * -> *) g r . Forall r c
+        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
+compose' = unRMap . metamorph @r @c @(RMap2 f g) @(RMap (Compose f g)) @(Compose f g) Proxy doNil doUncons doCons . RMap2
   where
     doNil _ = RMap empty
     doUncons l (RMap2 r) = (Compose $ r .! l, RMap2 $ unsafeRemove l r)
     doCons l v (RMap r) = RMap $ unsafeInjectFront l v r
 
--- | Convert from a record where the composition of two functors have been mapped
--- over the types to one where the two functors are mapped individually one at a
--- time over the types.
-uncompose :: forall (f :: * -> *) g r . Forall r Unconstrained1 => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
-uncompose = unRMap2 . metamorph @r @Unconstrained1 @(RMap (Compose f g)) @(RMap2 f g) Proxy doNil doUncons doCons . RMap
+-- | Convert from a record where two functors have been mapped over the types to
+-- one where the composition of the two functors is mapped over the types.
+compose :: forall (f :: * -> *) g r . Forall r Unconstrained1
+        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
+compose = compose' @Unconstrained1 @f @g @r
+
+-- | A version of 'uncompose' in which the constraint for 'Forall' can be chosen.
+uncompose' :: forall c (f :: * -> *) g r . Forall r c
+           => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
+uncompose' = unRMap2 . metamorph @r @c @(RMap (Compose f g)) @(RMap2 f g) @(Compose f g) Proxy doNil doUncons doCons . RMap
   where
     doNil _ = RMap2 empty
     doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)
     doCons l (Compose v) (RMap2 r) = RMap2 $ unsafeInjectFront l v r
 
+-- | Convert from a record where the composition of two functors have been mapped
+-- over the types to one where the two functors are mapped individually one at a
+-- time over the types.
+uncompose :: forall (f :: * -> *) g r . Forall r Unconstrained1
+          => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
+uncompose = uncompose' @Unconstrained1 @f @g @r
+
+
 -- | RZipPair is used internally as a type level lambda for zipping records.
 newtype RZipPair (ρ1 :: Row *) (ρ2 :: Row *) = RZipPair { unRZipPair :: Rec (Zip ρ1 ρ2) }
 
@@ -381,7 +400,7 @@
 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 @ρ
+                \\ mapForall @g @c @ρ
+                \\ 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
@@ -17,7 +17,7 @@
   , HasType, pattern IsJust, singleton
   , fromLabels
   -- ** Extension
-  , type (.\), Lacks, diversify, type (.+)
+  , type (.\), Lacks, type (.\/), diversify, type (.+)
   -- ** Modification
   , update, focus, Modify, rename, Rename
   -- * Destruction
@@ -122,7 +122,7 @@
 unSingleton v = (l, view l v) where l = Label @l
 
 -- | Make the variant arbitrarily more diverse.
-diversify :: forall r' r. AllUniqueLabels (r .+ r') => Var r -> Var (r .+ r')
+diversify :: forall r' r. Var r -> Var (r .\/ r')
 diversify = unsafeCoerce -- (OneOf l x) = OneOf l x
 
 -- | If the variant exists at the given label, update it to the given value.
diff --git a/examples/Examples.lhs b/examples/Examples.lhs
--- a/examples/Examples.lhs
+++ b/examples/Examples.lhs
@@ -94,7 +94,7 @@
 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 :: 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
@@ -385,6 +385,6 @@
 >   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 :: 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.1.0
+Version:             0.2.2.0
 License:             MIT
 License-file:        LICENSE
 Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck