diff --git a/quantification.cabal b/quantification.cabal
--- a/quantification.cabal
+++ b/quantification.cabal
@@ -1,5 +1,6 @@
+cabal-version: 2.0
 name: quantification
-version: 0.4
+version: 0.5.0
 synopsis: Rage against the quantification
 description: Data types and typeclasses to deal with universally and existentially quantified types
 homepage: https://github.com/andrewthad/quantification#readme
@@ -7,20 +8,21 @@
 license-file: LICENSE
 author: Andrew Martin
 maintainer: andrew.thaddeus@gmail.com
-copyright: 2016 Andrew Martin
+copyright: 2018 Andrew Martin
 category: Web
 build-type: Simple
-cabal-version: >=1.10
 
 library
   hs-source-dirs: src
   exposed-modules:
+    Data.Binary.Lifted
     Data.Exists
     Data.Monoid.Lifted
     Topaz.Rec
     Topaz.Types
   build-depends: 
       base >= 4.9 && < 5
+    , binary >= 0.8 && < 0.10
     , ghc-prim >= 0.5 && < 0.6
     , hashable >= 1.2 && < 1.3
     , aeson >= 1.0 && < 1.5
@@ -30,6 +32,7 @@
     , containers >= 0.5 && < 0.6
     , unordered-containers >= 0.2 && < 0.3
   default-language: Haskell2010
+  ghc-options: -O2 -Wall
 
 source-repository head
   type:     git
diff --git a/src/Data/Binary/Lifted.hs b/src/Data/Binary/Lifted.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Binary/Lifted.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Data.Binary.Lifted
+  ( Binary1(..)
+  , put1
+  , get1
+  ) where
+
+import Data.Binary (Get,Put,Binary,get,put)
+import Data.Functor.Compose (Compose(..))
+import Data.Word (Word8)
+import Data.Semigroup ((<>))
+
+class Binary1 f where
+  liftPut :: (a -> Put) -> f a -> Put
+  liftGet :: Get a -> Get (f a)
+
+instance Binary1 [] where
+  liftPut = liftPutList
+  liftGet = liftGetList
+
+instance Binary1 Maybe where
+  liftPut _ Nothing  = put (0 :: Word8)
+  liftPut f (Just x) = put (1 :: Word8) <> f x
+  liftGet f = do
+    (w :: Word8) <- get
+    case w of
+      0 -> return Nothing
+      _ -> fmap Just f
+
+instance (Binary1 f, Binary1 g) => Binary1 (Compose f g) where
+  liftPut f (Compose x) = liftPut (liftPut f) x
+  liftGet f = fmap Compose (liftGet (liftGet f))
+
+liftPutList :: (a -> Put) -> [a] -> Put
+liftPutList f xs = put (length xs) <> mapM_ f xs                                
+
+liftGetList :: Get a -> Get [a]                                                    
+liftGetList g = do
+  n <- get :: Get Int                                                           
+  internalGetMany g n                                                              
+
+internalGetMany :: Get a -> Int -> Get [a]                                         
+internalGetMany g n = go [] n                                                      
+  where 
+  go xs !0 = return $! reverse xs                                                  
+  go xs !i = do                                                                    
+    !x <- g
+    go (x:xs) (i-1)                                                                
+
+get1 :: (Binary1 f, Binary a) => Get (f a)
+get1 = liftGet get
+
+put1 :: (Binary1 f, Binary a) => f a -> Put
+put1 = liftPut put
+
+
diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs
--- a/src/Data/Exists.hs
+++ b/src/Data/Exists.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE ExistentialQuantification #-}
@@ -13,14 +14,16 @@
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnboxedTuples #-}
 
 {-# OPTIONS_GHC -Wall #-}
 
 {-| Data types and type classes for working with existentially quantified
-    values. In the event that Quantified Class Constraints ever land in GHC,
-    this package will be considered obsolete. The benefit that most of the
-    typeclasses in this module provide is that they help populate the instances
-    of 'Exists'.
+    values. When Quantified Class Constraints land in GHC 8.6,
+    the @BarForall@ classes will be considered obsolete. When Dependent
+    Haskell lands, the @BarForeach@ classes will also be obsolete.
+    The benefit that most of the typeclasses in this module provide is
+    that they help populate the instances of 'Exists' and @Rec@.
 -}
 
 module Data.Exists
@@ -32,6 +35,9 @@
   , DependentPair(..)
   , WitnessedEquality(..)
   , WitnessedOrdering(..)
+  , ApplyForall(..)
+  , ApplyForeach(..)
+  , ApplyLifted(..)
     -- * Type Classes
   , EqForall(..)
   , EqForallPoly(..)
@@ -41,26 +47,38 @@
   , OrdForeach(..)
   , ShowForall(..)
   , ShowForeach(..)
-  , ReadForall(..)
+  , ReadExists(..)
   , EnumForall(..)
-  , BoundedForall(..)
+  , EnumExists(..)
+  , BoundedExists(..)
   , SemigroupForall(..)
+  , SemigroupForeach(..)
   , MonoidForall(..)
+  , MonoidForeach(..)
   , HashableForall(..)
-  , PathPieceForall(..)
-  , FromJSONForall(..)
+  , HashableForeach(..)
+  , PathPieceExists(..)
+  , FromJSONForeach(..)
   , FromJSONExists(..)
   , ToJSONForall(..)
+  , ToJSONForeach(..)
   , ToJSONKeyFunctionForall(..)
-  , FromJSONKeyFunctionForall(..)
+  , FromJSONKeyFunctionForeach(..)
   , ToJSONKeyForall(..)
+  , ToJSONKeyForeach(..)
   , FromJSONKeyExists(..)
-  , FromJSONKeyForall(..)
+  , FromJSONKeyForeach(..)
+  , StorableForeach(..)
   , StorableForall(..)
+  , PrimForall(..)
+  , BinaryExists(..)
+  , BinaryForeach(..)
     -- * Higher Rank Classes
   , EqForall2(..)
   , EqForallPoly2(..)
   , ShowForall2(..)
+  , ShowForeach2(..)
+  , BinaryExists2(..)
     -- * More Type Classes
   , Sing
   , SingList(..)
@@ -69,55 +87,72 @@
   , Unreify(..)
     -- * Sing Type Classes
   , EqSing(..)
+  , OrdSing(..)
+  , ShowSing(..)
   , ToJSONSing(..)
   , FromJSONSing(..)
   , ToSing(..)
+  , SingKind(..)
     -- * Functions
     -- ** Show
   , showsForall
+  , showsForeach
   , showForall
+  , showListForall
+  , showListForeach
   , showsForall2
   , showForall2
     -- ** Defaulting
   , defaultEqForallPoly
   , defaultCompareForallPoly
-  , parseJSONMapForallKey
+  , parseJSONMapForeachKey
+  , toJSONMapForeachKey
     -- ** Weakening
   , weakenEquality
   , weakenOrdering
+  , strengthenEquality
+  , strengthenOrdering
+  , strengthenUnequalOrdering
     -- ** Other
   , unreifyList
   ) where
 
-import Data.Proxy (Proxy(..))
-import Data.Type.Equality ((:~:)(Refl),TestEquality(..))
 import Control.Applicative (Const(..))
 import Data.Aeson (ToJSON(..),FromJSON(..))
-import Data.Hashable (Hashable(..))
-import Data.Text (Text)
-import Data.Functor.Classes (Eq1(..),Show1(..))
-import Data.Functor.Sum (Sum(..))
-import Data.Functor.Product (Product(..))
+import Data.Aeson (ToJSONKey(..),FromJSONKey(..))
+import Data.Aeson (ToJSONKeyFunction(..),FromJSONKeyFunction(..))
+import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index))
+import Data.Binary (Get,Put,Binary)
+import Data.Binary.Lifted (Binary1(..))
+import Data.Coerce (coerce)
+import Data.Functor.Classes (Eq1(..),Show1(..),Ord1(..),eq1,compare1)
 import Data.Functor.Compose (Compose(..))
-import GHC.Int (Int(..))
-import GHC.Prim (dataToTag#)
-import Foreign.Ptr (Ptr)
+import Data.Functor.Product (Product(..))
+import Data.Functor.Sum (Sum(..))
+import Data.Hashable (Hashable(..))
 import Data.Kind (Type)
 import Data.Map.Strict (Map)
-import Data.Coerce (coerce)
-import qualified Data.Traversable as TRV
-import qualified Data.Map.Strict as M
+import Data.Monoid.Lifted (Semigroup1(..),Monoid1(..),append1,empty1)
+import Data.Proxy (Proxy(..))
+import Data.Semigroup (Semigroup)
+import Data.Text (Text)
+import Data.Type.Equality ((:~:)(Refl),TestEquality(..))
+import Foreign.Ptr (Ptr)
+import GHC.Exts (dataToTag#,State#,Int#,Proxy#,Addr#,ByteArray#,MutableByteArray#)
+import GHC.Int (Int(..))
+
+import qualified Data.Aeson.Encoding as Aeson
+import qualified Data.Aeson.Encoding.Internal as AEI
+import qualified Data.Aeson.Types as Aeson
+import qualified Data.Binary as BN
 import qualified Data.HashMap.Strict as HM
+import qualified Data.Map.Strict as M
+import qualified Data.Semigroup as SG
+import qualified Data.Traversable as TRV
 import qualified Data.Vector as V
-import qualified Data.Aeson.Types as Aeson
 import qualified Text.Read as R
 import qualified Web.PathPieces as PP
 
-import qualified Data.Aeson.Encoding as Aeson
-import Data.Aeson (ToJSONKey(..),FromJSONKey(..),
-  ToJSONKeyFunction(..),FromJSONKeyFunction(..))
-import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index))
-
 -- | Hide a type parameter.
 data Exists (f :: k -> Type) = forall a. Exists !(f a)
 
@@ -127,9 +162,16 @@
 -- | Hide three type parameters.
 data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c)
 
+-- | A pair in which the type of the second element can only
+--   be discovered by looking at the first element. The type
+--   instance does not enforce this, but all of its typeclass
+--   instances make this assumption.
 data DependentPair (f :: k -> Type) (g :: k -> Type) =
   forall a. DependentPair (f a) (g a)
 
+-- | A dependent pair in which the first element is a singleton.
+data Some (f :: k -> Type) = forall a. Some !(Sing a) !(f a)
+
 data WitnessedEquality (a :: k) (b :: k) where
   WitnessedEqualityEqual :: WitnessedEquality a a
   WitnessedEqualityUnequal :: WitnessedEquality a b
@@ -142,10 +184,147 @@
 data ToJSONKeyFunctionForall f
   = ToJSONKeyTextForall !(forall a. f a -> Text) !(forall a. f a -> Aeson.Encoding' Text)
   | ToJSONKeyValueForall !(forall a. f a -> Aeson.Value) !(forall a. f a -> Aeson.Encoding)
-data FromJSONKeyFunctionForall f
-  = FromJSONKeyTextParserForall !(forall a. Sing a -> Text -> Aeson.Parser (f a))
-  | FromJSONKeyValueForall !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a))
+data FromJSONKeyFunctionForeach f
+  = FromJSONKeyTextParserForeach !(forall a. Sing a -> Text -> Aeson.Parser (f a))
+  | FromJSONKeyValueForeach !(forall a. Sing a -> Aeson.Value -> Aeson.Parser (f a))
 
+newtype ApplyForall f a = ApplyForall { getApplyForall :: f a }
+
+instance ShowForall f => Show (ApplyForall f a) where
+  showsPrec p (ApplyForall x) = showParen (p > 10)
+    $ showString "ApplyForall "
+    . showsPrecForall 11 x
+
+instance SemigroupForall f => Semigroup (ApplyForall f a) where
+  (<>) = appendForall
+
+instance MonoidForall f => Monoid (ApplyForall f a) where
+  mempty = emptyForall
+  mappend = (SG.<>)
+
+instance SemigroupForall f => SemigroupForall (ApplyForall f) where
+  appendForall (ApplyForall a) (ApplyForall b) = ApplyForall (appendForall a b)
+
+instance MonoidForall f => MonoidForall (ApplyForall f) where
+  emptyForall = ApplyForall emptyForall
+
+newtype ApplyLifted f a = ApplyLifted { getApplyLifted :: f a }                         
+
+instance (Semigroup1 f, Semigroup a) => Semigroup (ApplyLifted f a) where  
+  (<>) = append1
+
+instance (Monoid1 f, Monoid a) => Monoid (ApplyLifted f a) where
+  mempty = empty1 
+  mappend = liftAppend mappend
+
+instance (Eq1 f, Eq a) => Eq (ApplyLifted f a) where
+  (==) = eq1 
+
+instance (Ord1 f, Ord a) => Ord (ApplyLifted f a) where
+  compare = compare1 
+
+instance Semigroup1 f => Semigroup1 (ApplyLifted f) where  
+  liftAppend g (ApplyLifted a) (ApplyLifted b) = ApplyLifted (liftAppend g a b)                        
+
+instance Monoid1 f => Monoid1 (ApplyLifted f) where        
+  liftEmpty f = ApplyLifted (liftEmpty f)                                        
+
+instance Eq1 f => Eq1 (ApplyLifted f) where
+  liftEq f (ApplyLifted a) (ApplyLifted b) = liftEq f a b
+
+instance Ord1 f => Ord1 (ApplyLifted f) where
+  liftCompare f (ApplyLifted a) (ApplyLifted b) = liftCompare f a b
+
+-- | This is useful for recovering an instance of a typeclass when
+-- we have the pi-quantified variant and a singleton in scope.
+newtype ApplyForeach f a = ApplyForeach { getApplyForeach :: f a }
+
+instance (EqForeach f, Reify a) => Eq (ApplyForeach f a) where
+  ApplyForeach a == ApplyForeach b = eqForeach reify a b
+
+instance (OrdForeach f, Reify a) => Ord (ApplyForeach f a) where
+  compare (ApplyForeach a) (ApplyForeach b) = compareForeach reify a b
+
+instance (ShowForeach f, Reify a) => Show (ApplyForeach f a) where
+  showsPrec p (ApplyForeach a) = showParen (p > 10)
+    $ showString "ApplyForeach "
+    . showsPrecForeach reify 11 a
+
+instance (SemigroupForeach f, Reify a) => Semigroup (ApplyForeach f a) where
+  (<>) = appendForeach reify
+
+instance (MonoidForeach f, Reify a) => Monoid (ApplyForeach f a) where
+  mempty = emptyForeach reify
+  mappend = (SG.<>)
+
+instance (ToJSONForeach f, Reify a) => ToJSON (ApplyForeach f a) where
+  toJSON = toJSONForeach reify
+
+instance (FromJSONForeach f, Reify a) => FromJSON (ApplyForeach f a) where
+  parseJSON = parseJSONForeach reify
+
+instance EqForeach f => EqForeach (ApplyForeach f) where
+  eqForeach s (ApplyForeach a) (ApplyForeach b) = eqForeach s a b
+
+instance OrdForeach f => OrdForeach (ApplyForeach f) where
+  compareForeach s (ApplyForeach a) (ApplyForeach b) = compareForeach s a b
+
+instance SemigroupForeach f => SemigroupForeach (ApplyForeach f) where
+  appendForeach s (ApplyForeach a) (ApplyForeach b) = ApplyForeach (appendForeach s a b)
+
+instance MonoidForeach f => MonoidForeach (ApplyForeach f) where
+  emptyForeach s = ApplyForeach (emptyForeach s)
+
+instance ToJSONForeach f => ToJSONForeach (ApplyForeach f) where
+  toJSONForeach s (ApplyForeach x) = toJSONForeach s x
+
+instance FromJSONForeach f => FromJSONForeach (ApplyForeach f) where
+  parseJSONForeach s = fmap ApplyForeach . parseJSONForeach s
+
+instance ToJSONKeyForeach f => ToJSONKeyForeach (ApplyForeach f) where
+  toJSONKeyForeach = case toJSONKeyForeach of
+    ToJSONKeyTextForall f g -> ToJSONKeyTextForall
+      (\(Pair s (ApplyForeach x)) -> f (Pair s x))
+      (\(Pair s (ApplyForeach x)) -> g (Pair s x))
+    ToJSONKeyValueForall f g -> ToJSONKeyValueForall
+      (\(Pair s (ApplyForeach x)) -> f (Pair s x))
+      (\(Pair s (ApplyForeach x)) -> g (Pair s x))
+
+instance FromJSONKeyForeach f => FromJSONKeyForeach (ApplyForeach f) where
+  fromJSONKeyForeach = case fromJSONKeyForeach of
+    FromJSONKeyTextParserForeach f -> FromJSONKeyTextParserForeach (\s t -> fmap ApplyForeach (f s t))
+    FromJSONKeyValueForeach f -> FromJSONKeyValueForeach (\s t -> fmap ApplyForeach (f s t))
+
+instance (ToJSONKeyForeach f, Reify a) => ToJSONKey (ApplyForeach f a) where
+  toJSONKey = case toJSONKeyForeach of
+    ToJSONKeyTextForall toText toEnc -> ToJSONKeyText
+      (\(ApplyForeach x) -> toText (Pair reify x))
+      (\(ApplyForeach x) -> toEnc (Pair reify x))
+    ToJSONKeyValueForall toValue toEnc -> ToJSONKeyValue
+      (\(ApplyForeach x) -> toValue (Pair reify x))
+      (\(ApplyForeach x) -> toEnc (Pair reify x))
+  toJSONKeyList = case toJSONKeyForeach of
+    ToJSONKeyTextForall toText toEnc -> ToJSONKeyValue
+      (\xs -> toJSON $ map (\(ApplyForeach x) -> toText (Pair reify x)) xs)
+      (\xs -> Aeson.list (textEncodingToValueEncoding . toEnc . Pair reify) (map getApplyForeach xs))
+    ToJSONKeyValueForall toValue toEnc -> ToJSONKeyValue
+      (\xs -> toJSON $ map (\(ApplyForeach x) -> toValue (Pair reify x)) xs)
+      (\xs -> Aeson.list (toEnc . Pair reify) (map getApplyForeach xs))
+
+-- this is always safe
+textEncodingToValueEncoding :: Aeson.Encoding' Text -> Aeson.Encoding' Aeson.Value
+textEncodingToValueEncoding = AEI.retagEncoding
+
+instance (FromJSONKeyForeach f, Reify a) => FromJSONKey (ApplyForeach f a) where
+  fromJSONKey = case fromJSONKeyForeach of
+    FromJSONKeyTextParserForeach f -> FromJSONKeyTextParser (fmap ApplyForeach . f reify)
+    FromJSONKeyValueForeach f -> FromJSONKeyValue (fmap ApplyForeach . f reify)
+  fromJSONKeyList = case fromJSONKeyForeach of
+    FromJSONKeyTextParserForeach f -> FromJSONKeyValue $ Aeson.withArray "ApplyForeach" $ \xs -> do
+      fmap V.toList (mapM (fmap ApplyForeach . Aeson.withText "ApplyForeach" (f reify)) xs)
+    FromJSONKeyValueForeach f -> FromJSONKeyValue $ Aeson.withArray "ApplyForeach" $ \xs -> do
+      fmap V.toList (mapM (fmap ApplyForeach . f reify) xs)
+
 class EqForall f where
   eqForall :: f a -> f a -> Bool
 
@@ -179,9 +358,15 @@
 class ShowForall2 f where
   showsPrecForall2 :: Int -> f a b -> ShowS
 
+class ShowForeach2 f where
+  showsPrecForeach2 :: Sing a -> Sing b -> Int -> f a b -> ShowS
+
 showsForall :: ShowForall f => f a -> ShowS
 showsForall = showsPrecForall 0
 
+showsForeach :: ShowForeach f => Sing a -> f a -> ShowS
+showsForeach s = showsPrecForeach s 0
+
 showForall :: ShowForall f => f a -> String
 showForall x = showsForall x ""
 
@@ -191,57 +376,106 @@
 showForall2 :: ShowForall2 f => f a b -> String
 showForall2 x = showsForall2 x ""
 
-class ReadForall f where
-  readPrecForall :: R.ReadPrec (Exists f)
+class ReadExists f where
+  readPrecExists :: R.ReadPrec (Exists f)
 
 class EqForall2 f where
   eqForall2 :: f a b -> f a b -> Bool
 
-class EqForallPoly2 f where
-  eqForallPoly2 :: f a b -> f c d -> Bool
+class EqForallPoly2 (f :: k -> j -> Type) where 
+  eqForallPoly2 :: forall (a :: k) (b :: j) (c :: k) (d :: j). f a b -> f c d -> WitnessedEquality '(a,b) '(c,d)
 
 class HashableForall f where
   hashWithSaltForall :: Int -> f a -> Int
 
+class HashableForeach f where
+  hashWithSaltForeach :: Sing a -> Int -> f a -> Int
+
 class ToJSONKeyForall f where
   toJSONKeyForall :: ToJSONKeyFunctionForall f
 
+class ToJSONKeyForeach f where
+  toJSONKeyForeach :: ToJSONKeyFunctionForall (Product Sing f)
+
 class FromJSONKeyExists f where
   fromJSONKeyExists :: FromJSONKeyFunction (Exists f)
 
-class FromJSONKeyForall f where
-  fromJSONKeyForall :: FromJSONKeyFunctionForall f
+class FromJSONKeyForeach f where
+  fromJSONKeyForeach :: FromJSONKeyFunctionForeach f
 
 class ToJSONForall f where
   toJSONForall :: f a -> Aeson.Value
 
-class FromJSONForall f where
-  parseJSONForall :: Sing a -> Aeson.Value -> Aeson.Parser (f a)
+class ToJSONForeach f where
+  toJSONForeach :: Sing a -> f a -> Aeson.Value
 
+class FromJSONForeach f where
+  parseJSONForeach :: Sing a -> Aeson.Value -> Aeson.Parser (f a)
+
 class FromJSONExists f where
   parseJSONExists :: Aeson.Value -> Aeson.Parser (Exists f)
 
 class EnumForall f where
-  toEnumForall :: Int -> Exists f
+  toEnumForall :: Int -> f a
   fromEnumForall :: f a -> Int
 
-class BoundedForall f where
-  minBoundForall :: Exists f
-  maxBoundForall :: Exists f
+class EnumExists f where
+  toEnumExists :: Int -> Exists f
+  fromEnumExists :: Exists f -> Int
 
-class PathPieceForall f where
+class BoundedExists f where
+  minBoundExists :: Exists f
+  maxBoundExists :: Exists f
+
+class PathPieceExists f where
   fromPathPieceForall :: Text -> Maybe (Exists f)
-  toPathPieceForall :: f a -> Text
+  toPathPieceForall :: Exists f -> Text
 
+class SemigroupForeach f where
+  appendForeach :: Sing a -> f a -> f a -> f a
+
 class SemigroupForall f where
-  sappendForall :: f a -> f a -> f a
+  appendForall :: f a -> f a -> f a
 
+class StorableForeach (f :: k -> Type) where
+  peekForeach :: Sing a -> Ptr (f a) -> IO (f a)
+  pokeForeach :: Sing a -> Ptr (f a) -> f a -> IO ()
+  sizeOfForeach :: forall (a :: k). Proxy f -> Sing a -> Int
+
+-- | This is like 'StorableForall' except that the type constructor
+-- must ignore its argument (for purposes of representation).
 class StorableForall (f :: k -> Type) where
-  peekForall :: Sing a -> Ptr (f a) -> IO (f a)
+  peekForall :: Ptr (f a) -> IO (f a)
   pokeForall :: Ptr (f a) -> f a -> IO ()
-  sizeOfFunctorForall :: f a -> Int
-  sizeOfForall :: forall (a :: k). Proxy f -> Sing a -> Int
+  sizeOfForall :: Proxy f -> Int
 
+-- | Be careful with this typeclass. It is more unsafe than 'Prim'.
+-- With 'writeByteArray#' and 'readByteArray#', one can implement
+-- @unsafeCoerce@.
+class PrimForall (f :: k -> Type) where
+  sizeOfForall# :: Proxy# f -> Int#
+  alignmentForall# :: Proxy# f -> Int#
+  indexByteArrayForall# :: ByteArray# -> Int# -> f a
+  readByteArrayForall# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, f a #)
+  writeByteArrayForall# :: MutableByteArray# s -> Int# -> f a -> State# s -> State# s
+  setByteArrayForall# :: MutableByteArray# s -> Int# -> Int# -> f a -> State# s -> State# s
+  indexOffAddrForall# :: Addr# -> Int# -> f a
+  readOffAddrForall# :: Addr# -> Int# -> State# s -> (# State# s, f a #)
+  writeOffAddrForall# :: Addr# -> Int# -> f a -> State# s -> State# s
+  setOffAddrForall# :: Addr# -> Int# -> Int# -> f a -> State# s -> State# s
+
+class BinaryForeach (f :: k -> Type) where
+  putForeach :: Sing a -> f a -> Put
+  getForeach :: Sing a -> Get (f a)
+
+class BinaryExists (f :: k -> Type) where
+  putExists :: Exists f -> Put
+  getExists :: Get (Exists f)
+
+class BinaryExists2 (f :: k -> j -> Type) where
+  putExists2 :: Exists2 f -> Put
+  getExists2 :: Get (Exists2 f)
+
 --------------------
 -- Instances Below
 --------------------
@@ -255,11 +489,11 @@
 instance ShowForall Proxy where
   showsPrecForall = showsPrec
 
-instance ReadForall Proxy where
-  readPrecForall = fmap Exists R.readPrec 
+instance ReadExists Proxy where
+  readPrecExists = fmap Exists R.readPrec 
 
 instance SemigroupForall Proxy where
-  sappendForall _ _ = Proxy 
+  appendForall _ _ = Proxy 
 
 instance EqForall ((:~:) a) where
   eqForall Refl Refl = True
@@ -267,7 +501,10 @@
 instance EqForall2 (:~:) where
   eqForall2 Refl Refl = True
 
-
+instance Show a => ShowForall (Const a) where
+  showsPrecForall p (Const a) = showParen (p > 10)
+    $ showString "Const "
+    . showsPrec p a
 
 instance Eq a => EqForall (Const a) where
   eqForall (Const x) (Const y) = x == y
@@ -278,8 +515,11 @@
 instance Hashable a => HashableForall (Const a) where
   hashWithSaltForall s (Const a) = hashWithSalt s a
 
+instance FromJSON a => FromJSONForeach (Const a) where
+  parseJSONForeach _ = fmap Const . parseJSON
 
--- I need to get rid of the ToJSONForall and FromJSONForall constraints
+
+-- I need to get rid of the ToJSONForall and FromJSONForeach constraints
 -- on these two instances.
 instance (ToJSONKeyForall f, ToJSONForall f) => ToJSONKey (Exists f) where
   toJSONKey = case toJSONKeyForall of
@@ -293,7 +533,7 @@
   Exists a == Exists b = weakenEquality (eqForallPoly a b)
 
 instance EqForallPoly2 f => Eq (Exists2 f) where
-  Exists2 a == Exists2 b = eqForallPoly2 a b
+  Exists2 a == Exists2 b = weakenEquality (eqForallPoly2 a b)
 
 instance OrdForallPoly f => Ord (Exists f) where
   compare (Exists a) (Exists b) = weakenOrdering (compareForallPoly a b)
@@ -317,21 +557,29 @@
     (p >= 11) 
     (showString "Exists " . showsPrecForall2 11 a)
 
-instance ReadForall f => Read (Exists f) where
+instance ReadExists f => Read (Exists f) where
   readPrec = R.parens $ R.prec 10 $ do
     R.Ident "Exists" <- R.lexP
-    R.step readPrecForall
+    R.step readPrecExists
     
-instance EnumForall f => Enum (Exists f) where
-  fromEnum (Exists x) = fromEnumForall x
-  toEnum = toEnumForall
+instance EnumExists f => Enum (Exists f) where
+  fromEnum = fromEnumExists
+  toEnum = toEnumExists
 
-instance BoundedForall f => Bounded (Exists f) where
-  minBound = minBoundForall
-  maxBound = maxBoundForall
+instance BoundedExists f => Bounded (Exists f) where
+  minBound = minBoundExists
+  maxBound = maxBoundExists
 
-instance PathPieceForall f => PP.PathPiece (Exists f) where
-  toPathPiece (Exists f) = toPathPieceForall f
+instance BinaryExists f => Binary (Exists f) where
+  get = getExists
+  put = putExists
+
+instance BinaryExists2 f => Binary (Exists2 f) where
+  get = getExists2
+  put = putExists2
+
+instance PathPieceExists f => PP.PathPiece (Exists f) where
+  toPathPiece = toPathPieceForall
   fromPathPiece = fromPathPieceForall
 
 instance (EqForall f, EqForall g) => EqForall (Product f g) where
@@ -356,23 +604,45 @@
     (p >= 11) 
     (showString "Pair " . showsPrecForall 11 f . showChar ' ' . showsPrecForall 11 g)
 
+instance (Semigroup1 f, SemigroupForall g) => SemigroupForall (Compose f g) where
+  appendForall (Compose x) (Compose y) = Compose (liftAppend appendForall x y)
+
 instance (Aeson.ToJSON1 f, ToJSONForall g) => ToJSONForall (Compose f g) where
   toJSONForall (Compose x) = Aeson.liftToJSON toJSONForall (Aeson.toJSON . map toJSONForall) x
 
-instance (Aeson.FromJSON1 f, FromJSONForall g) => FromJSONForall (Compose f g) where
-  parseJSONForall s = fmap Compose . Aeson.liftParseJSON
-    (parseJSONForall s)
-    (Aeson.withArray "Compose" (fmap V.toList . V.mapM (parseJSONForall s)))
+instance (Aeson.ToJSON1 f, ToJSONForeach g) => ToJSONForeach (Compose f g) where
+  toJSONForeach s (Compose x) = Aeson.liftToJSON (toJSONForeach s) (Aeson.toJSON . map (toJSONForeach s)) x
 
+instance (Aeson.FromJSON1 f, FromJSONForeach g) => FromJSONForeach (Compose f g) where
+  parseJSONForeach s = fmap Compose . Aeson.liftParseJSON
+    (parseJSONForeach s)
+    (Aeson.withArray "Compose" (fmap V.toList . V.mapM (parseJSONForeach s)))
+
 instance (Eq1 f, EqForall g) => EqForall (Compose f g) where
   eqForall (Compose x) (Compose y) = liftEq eqForall x y
 
+instance (Eq1 f, EqForeach g) => EqForeach (Compose f g) where
+  eqForeach s (Compose x) (Compose y) = liftEq (eqForeach s) x y
+
 instance (Show1 f, ShowForall g) => ShowForall (Compose f g) where
-  showsPrecForall _ (Compose x) = showString "Compose " . liftShowsPrec showsPrecForall showListForall 11 x
+  showsPrecForall p (Compose x) = showParen (p > 10) $ showString "Compose " . liftShowsPrec showsPrecForall showListForall 11 x
 
+instance (Show1 f, ShowForeach g) => ShowForeach (Compose f g) where
+  showsPrecForeach s p (Compose x) = showParen (p > 10) $ showString "Compose " . liftShowsPrec (showsPrecForeach s) (showListForeach s) 11 x
+
+instance (Semigroup1 f, SemigroupForeach g) => SemigroupForeach (Compose f g) where
+  appendForeach s (Compose x) (Compose y) = Compose (liftAppend (appendForeach s) x y)
+
+instance (Binary1 f, BinaryForeach g) => BinaryForeach (Compose f g) where
+  putForeach s (Compose x) = liftPut (putForeach s) x
+  getForeach s = fmap Compose (liftGet (getForeach s))
+
 showListForall :: ShowForall f => [f a] -> ShowS
 showListForall = showList__ showsForall
 
+showListForeach :: ShowForeach f => Sing a -> [f a] -> ShowS
+showListForeach s = showList__ (showsForeach s)
+
 -- Copied from GHC.Show. I do not like to import internal modules
 -- if I can instead copy a small amount of code.
 showList__ :: (a -> ShowS) ->  [a] -> ShowS
@@ -410,6 +680,19 @@
 
 type family Sing = (r :: k -> Type) | r -> k
 
+-- | The two functions must form an isomorphism.
+class SingKind k where
+  demoteSing :: Sing (a :: k) -> k
+  promoteSing :: k -> Exists (Sing :: k -> Type)
+
+instance SingKind k => SingKind [k] where
+  demoteSing SingListNil = []
+  demoteSing (SingListCons s ss) = demoteSing s : demoteSing ss
+  promoteSing [] = Exists SingListNil
+  promoteSing (x : xs) = case promoteSing x of
+    Exists s -> case promoteSing xs of
+      Exists ss -> Exists (SingListCons s ss)
+
 type instance Sing = SingList
 type instance Sing = SingMaybe
 
@@ -437,6 +720,12 @@
 class EqSing k where
   eqSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)
 
+class EqSing k => OrdSing k where
+  compareSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> WitnessedOrdering a b
+
+class ShowSing k where
+  showsPrecSing :: forall (a :: k). Int -> Sing a -> ShowS
+
 instance EqSing a => EqSing [a] where
   eqSing = eqSingList
 
@@ -450,13 +739,46 @@
     Nothing -> Nothing
   Nothing -> Nothing
 
+class SemigroupForeach f => MonoidForeach f where
+  emptyForeach :: Sing a -> f a
+
 class SemigroupForall f => MonoidForall f where
-  memptyForall :: Sing a -> f a
+  emptyForall :: f a
 
-data SingList :: [k] -> Type where
+data SingList :: forall (k :: Type). [k] -> Type where
   SingListNil :: SingList '[]
   SingListCons :: Sing r -> SingList rs -> SingList (r ': rs)
 
+-- singletons can only have one inhabitant per type, so if the
+-- types are equal, the values must be equal
+instance EqForall SingList where
+  eqForall _ _ = True
+
+instance EqSing k => EqForallPoly (SingList :: [k] -> Type) where
+  eqForallPoly SingListNil SingListNil = WitnessedEqualityEqual
+  eqForallPoly SingListNil (SingListCons _ _) = WitnessedEqualityUnequal
+  eqForallPoly (SingListCons _ _) SingListNil = WitnessedEqualityUnequal
+  eqForallPoly (SingListCons r rs) (SingListCons s ss) = case eqSing r s of
+    Nothing -> WitnessedEqualityUnequal
+    Just Refl -> case eqForallPoly rs ss of
+      WitnessedEqualityUnequal -> WitnessedEqualityUnequal
+      WitnessedEqualityEqual -> WitnessedEqualityEqual
+
+instance (SingKind k, Binary k) => BinaryExists (SingList :: [k] -> Type) where
+  putExists (Exists xs) = BN.put (demoteSing xs)
+  getExists = fmap promoteSing BN.get
+
+instance (ShowSing k) => Show (SingList (xs :: [k])) where
+  showsPrec _ SingListNil = showString "SingListNil"
+  showsPrec p (SingListCons s ss) = showParen (p > 10)
+    $ showString "SingListCons "
+    . showsPrecSing 11 s
+    . showChar ' '
+    . showsPrec 11 ss
+
+instance ShowSing k => ShowSing [k] where
+  showsPrecSing = showsPrec
+
 data SingMaybe :: Maybe k -> Type where
   SingMaybeJust :: Sing a -> SingMaybe ('Just a)
   SingMaybeNothing :: SingMaybe 'Nothing
@@ -468,63 +790,79 @@
 unreifyList SingListNil b = b
 unreifyList (SingListCons s ss) b = unreify s (unreifyList ss b)
 
-data Some (f :: k -> Type) = forall a. Some !(Sing a) !(f a)
-
-instance (EqForall f, EqSing k) => Eq (Some (f :: k -> Type)) where 
+instance (EqForeach f, EqSing k) => Eq (Some (f :: k -> Type)) where 
   Some s1 v1 == Some s2 v2 = case eqSing s1 s2 of
-    Just Refl -> eqForall v1 v2
+    Just Refl -> eqForeach s1 v1 v2
     Nothing -> False
 
+instance (OrdForeach f, OrdSing k) => Ord (Some (f :: k -> Type)) where 
+  compare (Some s1 v1) (Some s2 v2) = case compareSing s1 s2 of
+    WitnessedOrderingEQ -> compareForeach s1 v1 v2
+    WitnessedOrderingLT -> LT
+    WitnessedOrderingGT -> GT
+
+instance (ShowForeach f, ShowSing k) => Show (Some (f :: k -> Type)) where
+  showsPrec p (Some s a) = showParen (p >= 11)
+    $ showString "Sing "
+    . showsPrecSing 11 s
+    . showChar ' '
+    . showsPrecForeach s 11 a
+
 class ToSing (f :: k -> Type) where
   toSing :: f a -> Sing a
 
 class ToJSONSing k where
   toJSONSing :: forall (a :: k). Sing a -> Aeson.Value
 
-instance (ToJSONForall f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where
-  toJSON (Some s v) = toJSON [toJSONSing s, toJSONForall v]
+instance (ToJSONForeach f, ToJSONSing k) => ToJSON (Some (f :: k -> Type)) where
+  toJSON (Some s v) = toJSON [toJSONSing s, toJSONForeach s v]
 
 class FromJSONSing k where
   parseJSONSing :: Aeson.Value -> Aeson.Parser (Exists (Sing :: k -> Type))
 
-instance (FromJSONForall f, FromJSONSing k) => FromJSON (Some (f :: k -> Type)) where
+instance (FromJSONForeach f, FromJSONSing k) => FromJSON (Some (f :: k -> Type)) where
   parseJSON = Aeson.withArray "Some" $ \v -> if V.length v == 2
     then do
       let x = V.unsafeIndex v 0
           y = V.unsafeIndex v 1
       Exists s <- parseJSONSing x :: Aeson.Parser (Exists (Sing :: k -> Type))
-      val <- parseJSONForall s y
+      val <- parseJSONForeach s y
       return (Some s val)
     else fail "array of length 2 expected"
 
--- only used internally for its instances
-newtype Apply f a = Apply { getApply :: f a }
-
-instance EqForall f => Eq (Apply f a) where
-  Apply a == Apply b = eqForall a b
-
-instance OrdForall f => Ord (Apply f a) where
-  compare (Apply a) (Apply b) = compareForall a b
+-- This name is not great. I need to figure out a better naming
+-- scheme that allows this area to grow.
+toJSONMapForeachKey :: (ToJSONKeyForeach f, ToJSONForeach v)
+  => Sing a
+  -> Map (f a) (v a)
+  -> Aeson.Value
+toJSONMapForeachKey s m = case toJSONKeyForeach of
+  ToJSONKeyTextForall keyToText _ -> toJSON $ M.foldlWithKey'
+    ( \hm key val -> HM.insert (keyToText (Pair s key)) (toJSONForeach s val) hm
+    ) HM.empty m
+  ToJSONKeyValueForall keyToValue _ -> toJSON $ M.foldrWithKey' 
+    ( \key val xs -> (keyToValue (Pair s key), toJSONForeach s val) : xs
+    ) [] m
 
 -- | Parse a 'Map' whose key type is higher-kinded. This only creates a valid 'Map'
---   if the 'OrdForall' instance agrees with the 'Ord' instance.
-parseJSONMapForallKey :: forall f a v. (FromJSONKeyForall f, OrdForall f)
+--   if the 'OrdForeach' instance agrees with the 'Ord' instance.
+parseJSONMapForeachKey :: forall k (f :: k -> Type) (a :: k) v. (FromJSONKeyForeach f, OrdForeach f, Unreify k)
   => (Aeson.Value -> Aeson.Parser v) 
   -> Sing a
   -> Aeson.Value
   -> Aeson.Parser (Map (f a) v)
-parseJSONMapForallKey valueParser s obj = case fromJSONKeyForall of
-  FromJSONKeyTextParserForall f -> Aeson.withObject "Map k v"
-    ( fmap (M.mapKeysMonotonic getApply) . HM.foldrWithKey
+parseJSONMapForeachKey valueParser s obj = unreify s $ case fromJSONKeyForeach of
+  FromJSONKeyTextParserForeach f -> Aeson.withObject "Map k v"
+    ( fmap (M.mapKeysMonotonic getApplyForeach) . HM.foldrWithKey
       (\k v m -> M.insert
-        <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (Apply f a)) <?> Key k
+        <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (ApplyForeach f a)) <?> Key k
         <*> valueParser v <?> Key k
         <*> m
       ) (pure M.empty)
     ) obj
-  FromJSONKeyValueForall f -> Aeson.withArray "Map k v"
-    ( fmap (M.mapKeysMonotonic getApply . M.fromList)
-    . (coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(Apply f a, v)])
+  FromJSONKeyValueForeach f -> Aeson.withArray "Map k v"
+    ( fmap (M.mapKeysMonotonic getApplyForeach . M.fromList)
+    . (coerce :: Aeson.Parser [(f a, v)] -> Aeson.Parser [(ApplyForeach f a, v)])
     . TRV.sequence
     . zipWith (parseIndexedJSONPair (f s) valueParser) [0..]
     . V.toList
@@ -558,6 +896,26 @@
   WitnessedOrderingEQ -> EQ
   WitnessedOrderingLT -> LT
 
+strengthenEquality :: Bool -> WitnessedEquality a a
+strengthenEquality = \case
+  True -> WitnessedEqualityEqual
+  False -> WitnessedEqualityUnequal
+
+-- | Given that we already know two types are equal, promote an 'Ordering'.
+strengthenOrdering :: Ordering -> WitnessedOrdering a a                                
+strengthenOrdering = \case
+  LT -> WitnessedOrderingLT                                                    
+  EQ -> WitnessedOrderingEQ                                                              
+  GT -> WitnessedOrderingGT                                                                
+
+-- | Given that we already know two types to be unequal, promote an 'Ordering'.
+-- The argument should not be @EQ@.
+strengthenUnequalOrdering :: Ordering -> WitnessedOrdering a b                   
+strengthenUnequalOrdering = \case                                                  
+  LT -> WitnessedOrderingLT 
+  EQ -> WitnessedOrderingLT -- this case should not happen                                          
+  GT -> WitnessedOrderingGT               
+
 instance (EqForallPoly f, ToSing f, EqForeach g) => Eq (DependentPair f g) where
   DependentPair a1 b1 == DependentPair a2 b2 = case eqForallPoly a1 a2 of
     WitnessedEqualityUnequal -> False
@@ -575,4 +933,13 @@
     (showString "DependentPair " . showsPrecForall 11 a . showChar ' ' . showsPrecForeach (toSing a) 11 b)
     s
 
+instance Semigroup a => SemigroupForall (Const a) where
+  appendForall (Const x) (Const y) = Const (x SG.<> y)
+
+#if MIN_VERSION_base(4,11,0)
+instance Monoid a => MonoidForall (Const a) where
+#else
+instance (Semigroup a, Monoid a) => MonoidForall (Const a) where
+#endif
+  emptyForall = Const mempty
 
diff --git a/src/Data/Monoid/Lifted.hs b/src/Data/Monoid/Lifted.hs
--- a/src/Data/Monoid/Lifted.hs
+++ b/src/Data/Monoid/Lifted.hs
@@ -5,19 +5,20 @@
   , empty1
   ) where
 
-import Data.Functor.Identity
+import Control.Applicative
 import Data.Functor.Compose
-import qualified Data.Functor.Product as FP
-import Data.Map.Strict (Map)
+import Data.Functor.Identity
 import Data.HashMap.Strict (HashMap)
-import Control.Applicative
-import Data.Semigroup (Semigroup)
 import Data.Hashable (Hashable)
+import Data.Map.Strict (Map)
 import Data.Monoid
 import Data.Proxy (Proxy(..))
-import qualified Data.Semigroup as SG
-import qualified Data.Map.Strict as M
+import Data.Semigroup (Semigroup)
+import Data.Functor.Const (Const(..))
+import qualified Data.Functor.Product as FP
 import qualified Data.HashMap.Strict as HM
+import qualified Data.Map.Strict as M
+import qualified Data.Semigroup as SG
 
 -- | Laws for this typeclass:
 --
@@ -59,6 +60,9 @@
 instance Ord k => Semigroup1 (Map k) where
   liftAppend = M.unionWith
 
+instance Ord k => Monoid1 (Map k) where
+  liftEmpty _ = M.empty
+
 -- | Disagrees with 'Semigroup' instance for 'HashMap'
 instance (Hashable k, Eq k) => Semigroup1 (HashMap k) where
   liftAppend = HM.unionWith
@@ -107,4 +111,7 @@
 
 instance Monoid1 ((->) a) where
   liftEmpty b _ = b
+
+instance Semigroup a => Semigroup1 (Const a) where
+  liftAppend _ (Const x) (Const y) = Const (x SG.<> y)
 
diff --git a/src/Topaz/Rec.hs b/src/Topaz/Rec.hs
--- a/src/Topaz/Rec.hs
+++ b/src/Topaz/Rec.hs
@@ -30,16 +30,14 @@
   , puts
     -- * Conversion
   , fromSingList
+  , toSingList
   ) where
 
 import Prelude hiding (map,zipWith,foldMap,traverse)
 import Topaz.Types (Elem(..),type (++),Rec(..))
-import Topaz.Types (Elem(..),Rec(..))
 import Data.Exists
-import Data.Proxy (Proxy(..))
 import Data.Semigroup (Semigroup)
 import qualified Data.Semigroup as SG
-import qualified Data.Vector as V
 
 map :: (forall x. f x -> g x) -> Rec f as -> Rec g as
 map _ RecNil = RecNil
@@ -117,4 +115,8 @@
 fromSingList :: SingList as -> Rec Sing as
 fromSingList SingListNil = RecNil
 fromSingList (SingListCons r rs) = RecCons r (fromSingList rs)
+
+toSingList :: Rec Sing as -> SingList as
+toSingList RecNil = SingListNil
+toSingList (RecCons r rs) = SingListCons r (toSingList rs)
 
diff --git a/src/Topaz/Types.hs b/src/Topaz/Types.hs
--- a/src/Topaz/Types.hs
+++ b/src/Topaz/Types.hs
@@ -27,20 +27,22 @@
   , type (++)
   ) where
 
+import Control.Applicative (liftA2)
 import Data.Exists
-import Data.Hashable (Hashable(..))
-import Foreign.Storable (Storable(..))
-import Data.Type.Equality
-import Data.Type.Coercion
-import Data.Semigroup (Semigroup)
-import Data.Proxy (Proxy(..))
-import Foreign.Ptr (castPtr,plusPtr)
 import Data.Foldable (foldrM)
+import Data.Hashable (Hashable(..))
 import Data.Kind (Type)
 import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)
-import qualified Data.Semigroup as SG
+import Data.Proxy (Proxy(..))
+import Data.Semigroup (Semigroup)
+import Data.Type.Coercion
+import Data.Type.Equality
+import Foreign.Ptr (castPtr,plusPtr)
+import Foreign.Storable (Storable(..))
+
 import qualified Data.Aeson as AE
 import qualified Data.Aeson.Types as AET
+import qualified Data.Semigroup as SG
 import qualified Data.Vector as V
 
 data Nat = Succ Nat | Zero
@@ -121,9 +123,6 @@
     Just Coercion
   testCoercion _ _ = Nothing
 
-instance EqForall f => Eq (Rec f as) where
-  (==) = eqForall
-
 instance HashableForall f => HashableForall (Rec f) where
   hashWithSaltForall s0 = go s0 where
     go :: Int -> Rec f rs -> Int
@@ -146,11 +145,37 @@
 instance ShowForall f => Show (Rec f as) where
   showsPrec = showsPrecForall
 
+instance ShowForeach f => ShowForeach (Rec f) where
+  showsPrecForeach SingListNil _ RecNil = showString "RecNil"
+  showsPrecForeach (SingListCons s ss) p (RecCons v vs) = showParen (p > 10)
+    $ showString "RecCons "
+    . showsPrecForeach s 11 v
+    . showString " "
+    . showsPrecForeach ss 11 vs
+
+instance EqForall f => Eq (Rec f as) where
+  (==) = eqForall
+
 instance EqForall f => EqForall (Rec f) where
   eqForall RecNil RecNil = True
   eqForall (RecCons a as) (RecCons b bs) =
     eqForall a b && eqForall as bs
 
+instance EqForeach f => EqForeach (Rec f) where
+  eqForeach SingListNil RecNil RecNil = True
+  eqForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =
+    eqForeach s a b && eqForeach ss as bs
+
+instance EqForallPoly f => EqForallPoly (Rec f) where
+  eqForallPoly RecNil RecNil = WitnessedEqualityEqual
+  eqForallPoly RecNil (RecCons _ _) = WitnessedEqualityUnequal
+  eqForallPoly (RecCons _ _) RecNil = WitnessedEqualityUnequal
+  eqForallPoly (RecCons x xs) (RecCons y ys) = case eqForallPoly x y of
+    WitnessedEqualityUnequal -> WitnessedEqualityUnequal
+    WitnessedEqualityEqual -> case eqForallPoly xs ys of
+      WitnessedEqualityUnequal -> WitnessedEqualityUnequal
+      WitnessedEqualityEqual -> WitnessedEqualityEqual
+
 instance OrdForall f => Ord (Rec f as) where
   compare = compareForall
 
@@ -159,19 +184,26 @@
   compareForall (RecCons a as) (RecCons b bs) =
     mappend (compareForall a b) (compareForall as bs)
 
+instance OrdForeach f => OrdForeach (Rec f) where
+  compareForeach SingListNil RecNil RecNil = EQ
+  compareForeach (SingListCons s ss) (RecCons a as) (RecCons b bs) =
+    mappend (compareForeach s a b) (compareForeach ss as bs)
+
+
 instance SemigroupForall f => Semigroup (Rec f as) where
-  (<>) = recZipWith sappendForall
+  (<>) = recZipWith appendForall
 
-instance (MonoidForall f, Reify as) => Monoid (Rec f as) where
-  mempty = recMap memptyForall (singListToRec reify)
-  mappend = recZipWith sappendForall
+instance SemigroupForeach f => SemigroupForeach (Rec f) where
+  appendForeach SingListNil RecNil RecNil = RecNil
+  appendForeach (SingListCons s ss) (RecCons x xs) (RecCons y ys) =
+    RecCons (appendForeach s x y) (appendForeach ss xs ys)
 
-instance MonoidForall f => MonoidForall (Rec f) where
-  memptyForall SingListNil = RecNil
-  memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)
+instance MonoidForeach f => MonoidForeach (Rec f) where
+  emptyForeach SingListNil = RecNil
+  emptyForeach (SingListCons s ss) = RecCons (emptyForeach s) (emptyForeach ss)
 
 instance SemigroupForall f => SemigroupForall (Rec f) where
-  sappendForall = recZipWith sappendForall
+  appendForall = recZipWith appendForall
 
 instance ToJSONForall f => AE.ToJSON (Rec f as) where
   toJSON = toJSONForall
@@ -183,46 +215,52 @@
     go RecNil = []
     go (RecCons x xs) = toJSONForall x : go xs
 
-instance (FromJSONForall f, Reify as) => AE.FromJSON (Rec f as) where
-  parseJSON = parseJSONForall reify
+instance (FromJSONForeach f, Reify as) => AE.FromJSON (Rec f as) where
+  parseJSON = parseJSONForeach reify
 
-instance FromJSONForall f => FromJSONForall (Rec f) where
-  parseJSONForall s0 = AE.withArray "Rec" $ \vs -> do
+instance FromJSONForeach f => FromJSONForeach (Rec f) where
+  parseJSONForeach s0 = AE.withArray "Rec" $ \vs -> do
     let go :: SingList as -> Int -> AET.Parser (Rec f as)
         go SingListNil !ix = if V.length vs == ix
           then return RecNil
           else fail "too many elements in array"
         go (SingListCons s ss) !ix = if ix < V.length vs
           then do
-            r <- parseJSONForall s (vs V.! ix)
+            r <- parseJSONForeach s (vs V.! ix)
             rs <- go ss (ix + 1)
             return (RecCons r rs)
           else fail "not enough elements in array"
     go s0 0
 
-instance StorableForall f => StorableForall (Rec f) where
-  sizeOfFunctorForall RecNil = 0
-  sizeOfFunctorForall (RecCons r rs) =
-    sizeOfFunctorForall r + sizeOfFunctorForall rs
-  sizeOfForall _ SingListNil = 0
-  sizeOfForall _ (SingListCons s ss) =
-    sizeOfForall (Proxy :: Proxy f) s + sizeOfForall (Proxy :: Proxy (Rec f)) ss
-  peekForall SingListNil _ = return RecNil
-  peekForall (SingListCons s ss) ptr = do
-    r <- peekForall s (castPtr ptr)
-    rs <- peekForall ss (plusPtr ptr (sizeOfForall (Proxy :: Proxy f) s))
+instance StorableForeach f => StorableForeach (Rec f) where
+  sizeOfForeach _ SingListNil = 0
+  sizeOfForeach _ (SingListCons s ss) =
+    sizeOfForeach (Proxy :: Proxy f) s + sizeOfForeach (Proxy :: Proxy (Rec f)) ss
+  peekForeach SingListNil _ = return RecNil
+  peekForeach (SingListCons s ss) ptr = do
+    r <- peekForeach s (castPtr ptr)
+    rs <- peekForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s))
     return (RecCons r rs)
-  pokeForall _ RecNil = return ()
-  pokeForall ptr (RecCons r rs) = do
-    pokeForall (castPtr ptr) r
-    pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs
+  pokeForeach _ _ RecNil = return ()
+  pokeForeach (SingListCons s ss) ptr (RecCons r rs) = do
+    pokeForeach s (castPtr ptr) r
+    pokeForeach ss (plusPtr ptr (sizeOfForeach (Proxy :: Proxy f) s)) rs
 
-instance (StorableForall f, Reify as) => Storable (Rec f as) where
-  sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)
+instance (StorableForeach f, Reify as) => Storable (Rec f as) where
+  sizeOf _ = sizeOfForeach (Proxy :: Proxy (Rec f)) (reify :: SingList as)
   alignment _ = sizeOf (undefined :: Rec f as)
-  poke = pokeForall
-  peek = peekForall (reify :: SingList as)
+  poke = pokeForeach (reify :: SingList as)
+  peek = peekForeach (reify :: SingList as)
 
+instance BinaryForeach f => BinaryForeach (Rec f) where
+  putForeach SingListNil RecNil = return ()
+  putForeach (SingListCons s ss) (RecCons r rs) = do
+    putForeach s r
+    putForeach ss rs
+  getForeach SingListNil = return RecNil
+  getForeach (SingListCons s ss) =
+    liftA2 RecCons (getForeach s) (getForeach ss)
+
 instance FromJSONExists f => FromJSONExists (Rec f) where
   parseJSONExists = AE.withArray "Rec" $ \vs -> 
     foldrM go (Exists RecNil) vs
@@ -232,16 +270,8 @@
       Exists r <- parseJSONExists v :: AET.Parser (Exists g)
       return (Exists (RecCons r rs))
 
-singListToRec :: SingList as -> Rec Sing as
-singListToRec SingListNil = RecNil
-singListToRec (SingListCons r rs) = RecCons r (singListToRec rs)
-
 recZipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
 recZipWith _ RecNil RecNil = RecNil
 recZipWith f (RecCons a as) (RecCons b bs) =
   RecCons (f a b) (recZipWith f as bs)
-
-recMap :: (forall x. f x -> g x) -> Rec f as -> Rec g as
-recMap _ RecNil = RecNil
-recMap f (RecCons x xs) = RecCons (f x) (recMap f xs)