diff --git a/quantification.cabal b/quantification.cabal
--- a/quantification.cabal
+++ b/quantification.cabal
@@ -1,5 +1,5 @@
 name: quantification
-version: 0.2
+version: 0.3
 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
@@ -18,14 +18,17 @@
     Data.Exists
     Data.Monoid.Lifted
     Topaz.Rec
+    Topaz.Types
   build-depends: 
       base >= 4.9 && < 5
     , ghc-prim >= 0.5 && < 0.6
     , hashable >= 1.2 && < 1.3
-    , aeson >= 0.11 && < 1.2
+    , aeson >= 0.11 && < 1.3
     , text >= 1.0 && < 2.0
     , path-pieces >= 0.2 && < 0.3
     , vector >= 0.11 && < 0.13
+    , containers >= 0.5 && < 0.6
+    , unordered-containers >= 0.2 && < 0.3
   default-language: Haskell2010
 
 source-repository head
diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs
--- a/src/Data/Exists.hs
+++ b/src/Data/Exists.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE CPP #-}
 
 {-# OPTIONS_GHC -Wall #-}
@@ -27,6 +28,7 @@
     Exists(..)
   , Exists2(..)
   , Exists3(..)
+  , Some(..)
     -- * Type Classes
   , EqForall(..)
   , EqForallPoly(..)
@@ -44,8 +46,11 @@
   , FromJSONExists(..)
   , ToJSONForall(..)
 #if MIN_VERSION_aeson(1,0,0) 
+  , ToJSONKeyFunctionForall(..)
+  , FromJSONKeyFunctionForall(..)
   , ToJSONKeyForall(..)
   , FromJSONKeyExists(..)
+  , FromJSONKeyForall(..)
 #endif
   , StorableForall(..)
     -- * Higher Rank Classes
@@ -55,8 +60,14 @@
     -- * More Type Classes
   , Sing
   , SingList(..)
+  , SingMaybe(..)
   , Reify(..)
   , Unreify(..)
+    -- * Sing Type Classes
+  , EqSing(..)
+  , ToJSONSing(..)
+  , FromJSONSing(..)
+  , ToSing(..)
     -- * Functions
     -- ** Show
   , showsForall
@@ -66,6 +77,9 @@
     -- ** Defaulting
   , defaultEqForallPoly
   , defaultCompareForallPoly
+#if MIN_VERSION_aeson(1,0,0) 
+  , parseJSONMapForallKey
+#endif
     -- ** Other
   , unreifyList
   ) where
@@ -83,6 +97,13 @@
 import GHC.Int (Int(..))
 import GHC.Prim (dataToTag#)
 import Foreign.Ptr (Ptr)
+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 qualified Data.HashMap.Strict as HM
+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
@@ -91,21 +112,25 @@
 import qualified Data.Aeson.Encoding as Aeson
 import Data.Aeson (ToJSONKey(..),FromJSONKey(..),
   ToJSONKeyFunction(..),FromJSONKeyFunction(..))
+import Data.Aeson.Internal ((<?>),JSONPathElement(Key,Index))
 #endif
 
 -- newtype Exists (f :: k -> *) = Exists { runExists :: forall r. (forall a. f a -> r) -> r }
 
 -- | Hide a type parameter.
-data Exists (f :: k -> *) = forall a. Exists !(f a)
+data Exists (f :: k -> Type) = forall a. Exists !(f a)
 
-data Exists2 (f :: k -> j -> *) = forall a b. Exists2 !(f a b)
+data Exists2 (f :: k -> j -> Type) = forall a b. Exists2 !(f a b)
 
-data Exists3 (f :: k -> j -> l -> *) = forall a b c. Exists3 !(f a b c)
+data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c)
 
 #if MIN_VERSION_aeson(1,0,0) 
 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))
 #endif
 
 class EqForall f where
@@ -162,6 +187,9 @@
 
 class FromJSONKeyExists f where
   fromJSONKeyExists :: FromJSONKeyFunction (Exists f)
+
+class FromJSONKeyForall f where
+  fromJSONKeyForall :: FromJSONKeyFunctionForall f
 #endif
 
 class ToJSONForall f where
@@ -188,7 +216,7 @@
 class SemigroupForall f where
   sappendForall :: f a -> f a -> f a
 
-class StorableForall (f :: k -> *) where
+class StorableForall (f :: k -> Type) where
   peekForall :: Sing a -> Ptr (f a) -> IO (f a)
   pokeForall :: Ptr (f a) -> f a -> IO ()
   sizeOfFunctorForall :: f a -> Int
@@ -311,6 +339,14 @@
     (p >= 11) 
     (showString "Pair " . showsPrecForall 11 f . showChar ' ' . showsPrecForall 11 g)
 
+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 (Eq1 f, EqForall g) => EqForall (Compose f g) where
   eqForall (Compose x) (Compose y) = liftEq eqForall x y
 
@@ -358,13 +394,17 @@
 getTagBox !x = I# (dataToTag# x)
 {-# INLINE getTagBox #-}
 
-type family Sing = (r :: k -> *) | r -> k
+type family Sing = (r :: k -> Type) | r -> k
 
 type instance Sing = SingList
+type instance Sing = SingMaybe
 
 class Unreify k where
   unreify :: forall (a :: k) b. Sing a -> (Reify a => b) -> b
 
+instance Unreify k => Unreify [k] where
+  unreify = unreifyList
+
 class Reify a where
   reify :: Sing a
 
@@ -374,18 +414,125 @@
 instance (Reify a, Reify as) => Reify (a ': as) where
   reify = SingListCons reify reify
 
+instance Reify 'Nothing where
+  reify = SingMaybeNothing
+
+instance Reify a => Reify ('Just a) where
+  reify = SingMaybeJust reify
+
+class EqSing k where
+  eqSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)
+
+instance EqSing a => EqSing [a] where
+  eqSing = eqSingList
+
+eqSingList :: forall (a :: [k]) (b :: [k]). EqSing k => SingList a -> SingList b -> Maybe (a :~: b)
+eqSingList SingListNil SingListNil = Just Refl
+eqSingList SingListNil (SingListCons _ _) = Nothing
+eqSingList (SingListCons _ _) SingListNil = Nothing
+eqSingList (SingListCons a as) (SingListCons b bs) = case eqSing a b of
+  Just Refl -> case eqSingList as bs of
+    Just Refl -> Just Refl
+    Nothing -> Nothing
+  Nothing -> Nothing
+
 class SemigroupForall f => MonoidForall f where
   memptyForall :: Sing a -> f a
 
-data SingList :: [k] -> * where
+data SingList :: [k] -> Type where
   SingListNil :: SingList '[]
   SingListCons :: Sing r -> SingList rs -> SingList (r ': rs)
 
+data SingMaybe :: Maybe k -> Type where
+  SingMaybeJust :: Sing a -> SingMaybe ('Just a)
+  SingMaybeNothing :: SingMaybe 'Nothing
+
 unreifyList :: forall (as :: [k]) b. Unreify k
   => SingList as
   -> (Reify as => b)
   -> b
 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 
+  Some s1 v1 == Some s2 v2 = case eqSing s1 s2 of
+    Just Refl -> eqForall v1 v2
+    Nothing -> False
+
+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]
+
+class FromJSONSing k where
+  parseJSONSing :: Aeson.Value -> Aeson.Parser (Exists (Sing :: k -> Type))
+
+instance (FromJSONForall 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
+      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
+
+#if MIN_VERSION_aeson(1,0,0) 
+-- | 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)
+  => (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
+      (\k v m -> M.insert
+        <$> (coerce (f s k :: Aeson.Parser (f a)) :: Aeson.Parser (Apply 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)])
+    . TRV.sequence
+    . zipWith (parseIndexedJSONPair (f s) valueParser) [0..]
+    . V.toList
+    ) obj
+
+-- copied from aeson
+parseIndexedJSONPair :: (Aeson.Value -> Aeson.Parser a) -> (Aeson.Value -> Aeson.Parser b) -> Int -> Aeson.Value -> Aeson.Parser (a, b)
+parseIndexedJSONPair keyParser valParser idx value = p value <?> Index idx
+  where
+    p = Aeson.withArray "(k,v)" $ \ab ->
+        let n = V.length ab
+        in if n == 2
+             then (,) <$> parseJSONElemAtIndex keyParser 0 ab
+                      <*> parseJSONElemAtIndex valParser 1 ab
+             else fail $ "cannot unpack array of length " ++
+                         show n ++ " into a pair"
+{-# INLINE parseIndexedJSONPair #-}
+
+-- copied from aeson
+parseJSONElemAtIndex :: (Aeson.Value -> Aeson.Parser a) -> Int -> V.Vector Aeson.Value -> Aeson.Parser a
+parseJSONElemAtIndex p idx ary = p (V.unsafeIndex ary idx) <?> Index idx
+#endif
 
 
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
@@ -1,18 +1,110 @@
 module Data.Monoid.Lifted
   ( Semigroup1(..)
+  , Monoid1(..)
+  , append1
+  , empty1
   ) where
 
+import Data.Functor.Identity
 import Data.Functor.Compose
+import qualified Data.Functor.Product as FP
+import Data.Map.Strict (Map)
+import Data.HashMap.Strict (HashMap)
+import Control.Applicative
+import Data.Semigroup (Semigroup)
+import Data.Hashable (Hashable)
+import Data.Monoid
+import Data.Proxy (Proxy(..))
+import qualified Data.Semigroup as SG
+import qualified Data.Map.Strict as M
+import qualified Data.HashMap.Strict as HM
 
+-- | Laws for this typeclass:
+--
+-- * @liftAppend f a (liftAppend f b c) = liftAppend f (liftAppend f a b) c@
 class Semigroup1 f where
-  sappend1 :: (a -> a -> a) -> f a -> f a -> f a
+  liftAppend :: (a -> a -> a) -> f a -> f a -> f a
 
+append1 :: (Semigroup1 f, Semigroup a) => f a -> f a -> f a
+append1 = liftAppend (SG.<>)
+
+-- | Laws for this typeclass:
+--
+-- * @liftAppend f a (liftEmpty mempty) = a@
+class Semigroup1 f => Monoid1 f where
+  liftEmpty :: a -> f a
+
+empty1 :: (Monoid1 f, Monoid a) => f a
+empty1 = liftEmpty mempty
+
 instance Semigroup1 Maybe where
-  sappend1 _ Nothing Nothing = Nothing
-  sappend1 _ a@(Just _) Nothing = a
-  sappend1 _ Nothing a@(Just _) = a
-  sappend1 f (Just a) (Just b) = Just (f a b)
+  liftAppend _ Nothing Nothing = Nothing
+  liftAppend _ a@(Just _) Nothing = a
+  liftAppend _ Nothing a@(Just _) = a
+  liftAppend f (Just a) (Just b) = Just (f a b)
 
 instance (Semigroup1 f, Semigroup1 g) => Semigroup1 (Compose f g) where
-  sappend1 f (Compose a) (Compose b) = Compose ((sappend1 (sappend1 f)) a b)
+  liftAppend f (Compose a) (Compose b) = Compose ((liftAppend (liftAppend f)) a b)
+
+instance (Monoid1 f, Monoid1 g) => Monoid1 (Compose f g) where
+  liftEmpty a = Compose (liftEmpty (liftEmpty a))
+
+instance Semigroup1 IO where
+  liftAppend = liftA2
+
+instance Monoid1 IO where
+  liftEmpty = pure
+
+-- | Disagrees with 'Semigroup' instance for 'Map'
+instance Ord k => Semigroup1 (Map k) where
+  liftAppend = M.unionWith
+
+-- | Disagrees with 'Semigroup' instance for 'HashMap'
+instance (Hashable k, Eq k) => Semigroup1 (HashMap k) where
+  liftAppend = HM.unionWith
+
+instance (Hashable k, Eq k) => Monoid1 (HashMap k) where
+  liftEmpty _ = HM.empty
+
+instance Semigroup1 [] where
+  liftAppend _ = (++)
+
+instance Monoid1 [] where
+  liftEmpty _ = []
+
+instance Semigroup1 Identity where
+  liftAppend f (Identity a) (Identity b) = Identity (f a b)
+
+instance Monoid1 Identity where
+  liftEmpty = Identity
+
+instance (Semigroup1 f, Semigroup1 g) => Semigroup1 (FP.Product f g) where
+  liftAppend f (FP.Pair a1 b1) (FP.Pair a2 b2) = FP.Pair (liftAppend f a1 a2) (liftAppend f b1 b2)
+
+instance (Monoid1 f, Monoid1 g) => Monoid1 (FP.Product f g) where
+  liftEmpty a = FP.Pair (liftEmpty a) (liftEmpty a)
+
+instance Semigroup1 Dual where
+  liftAppend f (Dual a) (Dual b) = Dual (f b a)
+
+instance Monoid1 Dual where
+  liftEmpty a = Dual a
+
+instance Semigroup a => Semigroup1 ((,) a) where
+  liftAppend f (a1,b1) (a2,b2) = (a1 SG.<> a2, f b1 b2)
+
+instance (Semigroup a, Monoid a) => Monoid1 ((,) a) where
+  liftEmpty b = (mempty,b)
+
+instance Semigroup1 Proxy where
+  liftAppend _ _ _ = Proxy
+
+instance Monoid1 Proxy where
+  liftEmpty _ = Proxy
+
+instance Semigroup1 ((->) a) where
+  liftAppend combine f g a = combine (f a) (g a)
+
+instance Monoid1 ((->) a) where
+  liftEmpty b _ = b
 
diff --git a/src/Topaz/Rec.hs b/src/Topaz/Rec.hs
--- a/src/Topaz/Rec.hs
+++ b/src/Topaz/Rec.hs
@@ -1,179 +1,46 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators #-}
 
 {-# OPTIONS_GHC -Wall #-}
 
 module Topaz.Rec
   ( Rec(..)
   , map
+  , append
   , traverse
   , traverse_
   , zipWith
   , foldMap
   , foldMap1
+    -- * Access
+  , get
+  , put
+  , gets
+  , puts
+    -- * Conversion
+  , fromSingList
   ) where
 
 import Prelude hiding (map,zipWith,foldMap,traverse)
+import Topaz.Types (Elem(..),type (++),Rec(..))
+import Topaz.Types (Elem(..),Rec(..))
 import Data.Exists
-import Data.Type.Equality
-import Data.Type.Coercion
-import Data.Foldable (foldrM)
 import Data.Proxy (Proxy(..))
-import Foreign.Ptr (castPtr,plusPtr)
-import Foreign.Storable (Storable(..))
 import Data.Semigroup (Semigroup)
-import Data.Hashable (Hashable(..))
 import qualified Data.Semigroup as SG
 import qualified Data.Vector as V
-import qualified Data.Aeson as AE
-import qualified Data.Aeson.Types as AET
 
-data Rec :: (k -> *) -> [k] -> * where
-  RecNil :: Rec f '[]
-  RecCons :: f r -> Rec f rs -> Rec f (r ': rs)
-
-instance TestEquality f => TestEquality (Rec f) where
-  testEquality RecNil RecNil = Just Refl
-  testEquality (RecCons x xs) (RecCons y ys) = do
-    Refl <- testEquality x y
-    Refl <- testEquality xs ys
-    Just Refl
-  testEquality _ _ = Nothing
-
-instance TestCoercion f => TestCoercion (Rec f) where
-  testCoercion RecNil RecNil = Just Coercion
-  testCoercion (RecCons x xs) (RecCons y ys) = do
-    Coercion <- testCoercion x y
-    Coercion <- testCoercion xs ys
-    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
-    go !s x = case x of
-      RecNil -> s
-      RecCons b bs -> go (hashWithSaltForall s b) bs
-
-instance HashableForall f => Hashable (Rec f as) where
-  hashWithSalt = hashWithSaltForall
-
-instance ShowForall f => ShowForall (Rec f) where
-  showsPrecForall p x = case x of
-    RecCons v vs -> showParen (p > 10)
-      $ showString "RecCons "
-      . showsPrecForall 11 v
-      . showString " "
-      . showsPrecForall 11 vs
-    RecNil -> showString "RecNil"
-
-instance ShowForall f => Show (Rec f as) where
-  showsPrec = showsPrecForall
-
-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 OrdForall f => Ord (Rec f as) where
-  compare = compareForall
-
-instance OrdForall f => OrdForall (Rec f) where
-  compareForall RecNil RecNil = EQ
-  compareForall (RecCons a as) (RecCons b bs) =
-    mappend (compareForall a b) (compareForall as bs)
-
-instance SemigroupForall f => Semigroup (Rec f as) where
-  (<>) = zipWith sappendForall
-
-instance (MonoidForall f, Reify as) => Monoid (Rec f as) where
-  mempty = map memptyForall (singListToRec reify)
-  mappend = zipWith sappendForall
-
-instance MonoidForall f => MonoidForall (Rec f) where
-  memptyForall SingListNil = RecNil
-  memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)
-
-instance SemigroupForall f => SemigroupForall (Rec f) where
-  sappendForall = zipWith sappendForall
-
-instance ToJSONForall f => AE.ToJSON (Rec f as) where
-  toJSON = toJSONForall
-
-instance ToJSONForall f => ToJSONForall (Rec f) where
-  toJSONForall = AE.toJSON . go
-    where
-    go :: forall g xs. ToJSONForall g => Rec g xs -> [AE.Value]
-    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 FromJSONForall f => FromJSONForall (Rec f) where
-  parseJSONForall 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)
-            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))
-    return (RecCons r rs)
-  pokeForall _ RecNil = return ()
-  pokeForall ptr (RecCons r rs) = do
-    pokeForall (castPtr ptr) r
-    pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs
-
-instance (StorableForall f, Reify as) => Storable (Rec f as) where
-  sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)
-  alignment _ = sizeOf (undefined :: Rec f as)
-  poke = pokeForall
-  peek = peekForall (reify :: SingList as)
-
-instance FromJSONExists f => FromJSONExists (Rec f) where
-  parseJSONExists = AE.withArray "Rec" $ \vs -> 
-    foldrM go (Exists RecNil) vs
-    where
-    go :: forall g. FromJSONExists g => AE.Value -> Exists (Rec g) -> AET.Parser (Exists (Rec g))
-    go v (Exists rs) = do
-      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)
-
 map :: (forall x. f x -> g x) -> Rec f as -> Rec g as
 map _ RecNil = RecNil
 map f (RecCons x xs) = RecCons (f x) (map f xs)
@@ -227,4 +94,27 @@
 traverse_ _ RecNil = pure ()
 traverse_ f (RecCons x xs) = f x *> traverse_ f xs
 {-# INLINABLE traverse_ #-}
+
+get :: Elem rs r -> Rec f rs -> f r
+get ElemHere (RecCons r _) = r
+get (ElemThere ix) (RecCons _ rs) = get ix rs
+
+put :: Elem rs r -> f r -> Rec f rs -> Rec f rs
+put ElemHere r' (RecCons _ rs) = RecCons r' rs
+put (ElemThere ix) r' (RecCons r rs) = RecCons r (put ix r' rs)
+
+gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss
+gets ixs rec = map (\e -> get e rec) ixs
+
+puts :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs
+puts RecNil rs _ = rs
+puts (RecCons ix ixs) rs (RecCons s ss) = put ix s (puts ixs rs ss)
+
+append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
+append RecNil ys = ys
+append (RecCons x xs) ys = RecCons x (append xs ys)
+
+fromSingList :: SingList as -> Rec Sing as
+fromSingList SingListNil = RecNil
+fromSingList (SingListCons r rs) = RecCons r (fromSingList rs)
 
diff --git a/src/Topaz/Types.hs b/src/Topaz/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Topaz/Types.hs
@@ -0,0 +1,228 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Topaz.Types
+  ( Elem(..)
+  , Rec(..)
+  -- , BiRec(..)
+  , NestRec(..)
+  , Fix(..)
+  , HFix(..)
+  , Nest(..)
+  , EqHetero(..)
+  , TestEqualityHetero(..)
+  , type (++)
+  ) where
+
+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.Kind (Type)
+import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)
+import qualified Data.Semigroup as SG
+import qualified Data.Aeson as AE
+import qualified Data.Aeson.Types as AET
+import qualified Data.Vector as V
+
+data Elem (rs :: [k]) (r :: k) where
+  ElemHere :: Elem (r ': rs) r
+  ElemThere :: Elem rs r -> Elem (s ': rs) r
+
+type family (as :: [k]) ++ (bs :: [k]) :: [k] where
+  '[] ++ bs = bs
+  (a ': as) ++ bs = a ': (as ++ bs)
+infixr 5 ++
+
+data Rec :: (k -> Type) -> [k] -> Type where
+  RecNil :: Rec f '[]
+  RecCons :: f r -> Rec f rs -> Rec f (r ': rs)
+
+-- data BiRec :: (k -> Type) -> (j -> Type) -> [k] -> [j] -> Type where
+--   BiRec :: Rec f ks -> Rec g js -> BiRec f g ks js
+
+data NestRec :: (k -> Type) -> Nest k -> Type where
+  NestRec :: Rec f rs -> Rec (NestRec f) ns -> NestRec f ('Nest ns rs)
+
+data Nest a = Nest [Nest a] [a]
+newtype Fix f = Fix (f (Fix f))
+newtype HFix h a = HFix (h (HFix h) a)
+
+instance Semigroup1 f => Semigroup (Fix f) where
+  Fix a <> Fix b = Fix (append1 a b)
+
+instance Monoid1 f => Monoid (Fix f) where
+  mempty = Fix (liftEmpty mempty)
+  mappend = (SG.<>)
+
+-- Think of a better name for this typeclass
+class EqHetero h where
+  eqHetero :: (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool
+
+instance EqHetero h => EqForall (HFix h) where
+  eqForall (HFix a) (HFix b) = eqHetero eqForall a b 
+
+instance EqHetero h => Eq (HFix h a) where
+  (==) = eqForall
+
+class TestEqualityHetero h where
+  testEqualityHetero :: (forall x y. f x -> f y -> Maybe (x :~: y)) -> h f a -> h f b -> Maybe (a :~: b)
+
+instance TestEqualityHetero h => TestEquality (HFix h) where
+  testEquality (HFix a) (HFix b) = testEqualityHetero testEquality a b
+
+instance TestEquality f => TestEquality (Rec f) where
+  testEquality RecNil RecNil = Just Refl
+  testEquality (RecCons x xs) (RecCons y ys) = do
+    Refl <- testEquality x y
+    Refl <- testEquality xs ys
+    Just Refl
+  testEquality _ _ = Nothing
+
+instance TestCoercion f => TestCoercion (Rec f) where
+  testCoercion RecNil RecNil = Just Coercion
+  testCoercion (RecCons x xs) (RecCons y ys) = do
+    Coercion <- testCoercion x y
+    Coercion <- testCoercion xs ys
+    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
+    go !s x = case x of
+      RecNil -> s
+      RecCons b bs -> go (hashWithSaltForall s b) bs
+
+instance HashableForall f => Hashable (Rec f as) where
+  hashWithSalt = hashWithSaltForall
+
+instance ShowForall f => ShowForall (Rec f) where
+  showsPrecForall p x = case x of
+    RecCons v vs -> showParen (p > 10)
+      $ showString "RecCons "
+      . showsPrecForall 11 v
+      . showString " "
+      . showsPrecForall 11 vs
+    RecNil -> showString "RecNil"
+
+instance ShowForall f => Show (Rec f as) where
+  showsPrec = showsPrecForall
+
+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 OrdForall f => Ord (Rec f as) where
+  compare = compareForall
+
+instance OrdForall f => OrdForall (Rec f) where
+  compareForall RecNil RecNil = EQ
+  compareForall (RecCons a as) (RecCons b bs) =
+    mappend (compareForall a b) (compareForall as bs)
+
+instance SemigroupForall f => Semigroup (Rec f as) where
+  (<>) = recZipWith sappendForall
+
+instance (MonoidForall f, Reify as) => Monoid (Rec f as) where
+  mempty = recMap memptyForall (singListToRec reify)
+  mappend = recZipWith sappendForall
+
+instance MonoidForall f => MonoidForall (Rec f) where
+  memptyForall SingListNil = RecNil
+  memptyForall (SingListCons s ss) = RecCons (memptyForall s) (memptyForall ss)
+
+instance SemigroupForall f => SemigroupForall (Rec f) where
+  sappendForall = recZipWith sappendForall
+
+instance ToJSONForall f => AE.ToJSON (Rec f as) where
+  toJSON = toJSONForall
+
+instance ToJSONForall f => ToJSONForall (Rec f) where
+  toJSONForall = AE.toJSON . go
+    where
+    go :: forall g xs. ToJSONForall g => Rec g xs -> [AE.Value]
+    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 FromJSONForall f => FromJSONForall (Rec f) where
+  parseJSONForall 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)
+            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))
+    return (RecCons r rs)
+  pokeForall _ RecNil = return ()
+  pokeForall ptr (RecCons r rs) = do
+    pokeForall (castPtr ptr) r
+    pokeForall (plusPtr ptr (sizeOfFunctorForall r)) rs
+
+instance (StorableForall f, Reify as) => Storable (Rec f as) where
+  sizeOf _ = sizeOfForall (Proxy :: Proxy (Rec f)) (reify :: SingList as)
+  alignment _ = sizeOf (undefined :: Rec f as)
+  poke = pokeForall
+  peek = peekForall (reify :: SingList as)
+
+instance FromJSONExists f => FromJSONExists (Rec f) where
+  parseJSONExists = AE.withArray "Rec" $ \vs -> 
+    foldrM go (Exists RecNil) vs
+    where
+    go :: forall g. FromJSONExists g => AE.Value -> Exists (Rec g) -> AET.Parser (Exists (Rec g))
+    go v (Exists rs) = do
+      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)
+