diff --git a/quantification.cabal b/quantification.cabal
--- a/quantification.cabal
+++ b/quantification.cabal
@@ -1,10 +1,10 @@
-cabal-version: 2.0
+cabal-version: 2.4
 name: quantification
-version: 0.5.0
+version: 0.8
 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
-license: BSD3
+license: BSD-3-Clause
 license-file: LICENSE
 author: Andrew Martin
 maintainer: andrew.thaddeus@gmail.com
@@ -18,18 +18,13 @@
     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
-    , text >= 1.0 && < 2.0
+  build-depends:
+    , base >= 4.11.1 && < 5
+    , binary >= 0.8 && < 0.11
+    , hashable >= 1.4 && < 1.5
+    , text >= 1.0 && < 2.2
     , path-pieces >= 0.2 && < 0.3
-    , vector >= 0.11 && < 0.13
-    , containers >= 0.5 && < 0.6
+    , containers >= 0.5 && < 0.7
     , unordered-containers >= 0.2 && < 0.3
   default-language: Haskell2010
   ghc-options: -O2 -Wall
diff --git a/src/Data/Binary/Lifted.hs b/src/Data/Binary/Lifted.hs
--- a/src/Data/Binary/Lifted.hs
+++ b/src/Data/Binary/Lifted.hs
@@ -11,7 +11,6 @@
 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
diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs
--- a/src/Data/Exists.hs
+++ b/src/Data/Exists.hs
@@ -2,17 +2,13 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DefaultSignatures #-}
-{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
-{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UnboxedTuples #-}
 
@@ -58,16 +54,6 @@
   , HashableForall(..)
   , HashableForeach(..)
   , PathPieceExists(..)
-  , FromJSONForeach(..)
-  , FromJSONExists(..)
-  , ToJSONForall(..)
-  , ToJSONForeach(..)
-  , ToJSONKeyFunctionForall(..)
-  , FromJSONKeyFunctionForeach(..)
-  , ToJSONKeyForall(..)
-  , ToJSONKeyForeach(..)
-  , FromJSONKeyExists(..)
-  , FromJSONKeyForeach(..)
   , StorableForeach(..)
   , StorableForall(..)
   , PrimForall(..)
@@ -89,8 +75,6 @@
   , EqSing(..)
   , OrdSing(..)
   , ShowSing(..)
-  , ToJSONSing(..)
-  , FromJSONSing(..)
   , ToSing(..)
   , SingKind(..)
     -- * Functions
@@ -105,8 +89,6 @@
     -- ** Defaulting
   , defaultEqForallPoly
   , defaultCompareForallPoly
-  , parseJSONMapForeachKey
-  , toJSONMapForeachKey
     -- ** Weakening
   , weakenEquality
   , weakenOrdering
@@ -118,38 +100,24 @@
   ) where
 
 import Control.Applicative (Const(..))
-import Data.Aeson (ToJSON(..),FromJSON(..))
-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 Data.Functor.Product (Product(..))
 import Data.Functor.Sum (Sum(..))
 import Data.Hashable (Hashable(..))
 import Data.Kind (Type)
-import Data.Map.Strict (Map)
 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 Text.Read as R
 import qualified Web.PathPieces as PP
 
@@ -181,13 +149,6 @@
   WitnessedOrderingEQ :: WitnessedOrdering a a
   WitnessedOrderingGT :: WitnessedOrdering a b
 
-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 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
@@ -215,7 +176,7 @@
 
 instance (Monoid1 f, Monoid a) => Monoid (ApplyLifted f a) where
   mempty = empty1 
-  mappend = liftAppend mappend
+  mappend = (<>)
 
 instance (Eq1 f, Eq a) => Eq (ApplyLifted f a) where
   (==) = eq1 
@@ -257,12 +218,6 @@
   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
 
@@ -275,56 +230,6 @@
 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
 
@@ -391,30 +296,6 @@
 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 FromJSONKeyForeach f where
-  fromJSONKeyForeach :: FromJSONKeyFunctionForeach f
-
-class ToJSONForall f where
-  toJSONForall :: f a -> Aeson.Value
-
-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 -> f a
   fromEnumForall :: f a -> Int
@@ -515,20 +396,6 @@
 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 FromJSONForeach constraints
--- on these two instances.
-instance (ToJSONKeyForall f, ToJSONForall f) => ToJSONKey (Exists f) where
-  toJSONKey = case toJSONKeyForall of
-    ToJSONKeyTextForall t e -> ToJSONKeyText (\(Exists a) -> t a) (\(Exists a) -> e a)
-    ToJSONKeyValueForall v e -> ToJSONKeyValue (\x -> case x of Exists a -> v a) (\(Exists a) -> e a)
-
-instance (FromJSONKeyExists f, FromJSONExists f) => FromJSONKey (Exists f) where
-  fromJSONKey = fromJSONKeyExists
-
 instance EqForallPoly f => Eq (Exists f) where
   Exists a == Exists b = weakenEquality (eqForallPoly a b)
 
@@ -538,15 +405,9 @@
 instance OrdForallPoly f => Ord (Exists f) where
   compare (Exists a) (Exists b) = weakenOrdering (compareForallPoly a b)
 
-instance HashableForall f => Hashable (Exists f) where
+instance (EqForallPoly f, HashableForall f) => Hashable (Exists f) where
   hashWithSalt s (Exists a) = hashWithSaltForall s a
 
-instance ToJSONForall f => ToJSON (Exists f) where
-  toJSON (Exists a) = toJSONForall a
-
-instance FromJSONExists f => FromJSON (Exists f) where
-  parseJSON v = parseJSONExists v
-
 instance ShowForall f => Show (Exists f) where
   showsPrec p (Exists a) = showParen 
     (p >= 11) 
@@ -604,20 +465,12 @@
     (p >= 11) 
     (showString "Pair " . showsPrecForall 11 f . showChar ' ' . showsPrecForall 11 g)
 
+instance (Ord1 f, OrdForeach g) => OrdForeach (Compose f g) where
+  compareForeach s (Compose x) (Compose y) = liftCompare (compareForeach s) x y
+
 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.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
 
@@ -729,7 +582,7 @@
 instance EqSing a => EqSing [a] where
   eqSing = eqSingList
 
-eqSingList :: forall (a :: [k]) (b :: [k]). EqSing k => SingList a -> SingList b -> Maybe (a :~: b)
+eqSingList :: forall (k :: Type) (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
@@ -783,7 +636,7 @@
   SingMaybeJust :: Sing a -> SingMaybe ('Just a)
   SingMaybeNothing :: SingMaybe 'Nothing
 
-unreifyList :: forall (as :: [k]) b. Unreify k
+unreifyList :: forall (k :: Type) (as :: [k]) (b :: Type) . Unreify k
   => SingList as
   -> (Reify as => b)
   -> b
@@ -810,80 +663,6 @@
 
 class ToSing (f :: k -> Type) where
   toSing :: f a -> Sing a
-
-class ToJSONSing k where
-  toJSONSing :: forall (a :: k). Sing a -> Aeson.Value
-
-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 (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 <- parseJSONForeach s y
-      return (Some s val)
-    else fail "array of length 2 expected"
-
--- 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 '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)
-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 (ApplyForeach f a)) <?> Key k
-        <*> valueParser v <?> Key k
-        <*> m
-      ) (pure M.empty)
-    ) obj
-  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
-    ) 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
 
 weakenEquality :: WitnessedEquality a b -> Bool
 weakenEquality = \case
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
@@ -13,8 +13,7 @@
 import Data.Map.Strict (Map)
 import Data.Monoid
 import Data.Proxy (Proxy(..))
-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
diff --git a/src/Topaz/Rec.hs b/src/Topaz/Rec.hs
deleted file mode 100644
--- a/src/Topaz/Rec.hs
+++ /dev/null
@@ -1,122 +0,0 @@
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DefaultSignatures #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# 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
-  , toSingList
-  ) where
-
-import Prelude hiding (map,zipWith,foldMap,traverse)
-import Topaz.Types (Elem(..),type (++),Rec(..))
-import Data.Exists
-import Data.Semigroup (Semigroup)
-import qualified Data.Semigroup as SG
-
-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)
-
-zipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs
-zipWith _ RecNil RecNil = RecNil
-zipWith f (RecCons a as) (RecCons b bs) =
-  RecCons (f a b) (zipWith f as bs)
-
--- | Map each element of a record to a monoid and combine the results.
-foldMap :: forall f m rs. Monoid m
-  => (forall x. f x -> m)
-  -> Rec f rs
-  -> m
-foldMap f = go mempty
-  where
-  go :: forall ss. m -> Rec f ss -> m
-  go !m record = case record of
-    RecNil -> m
-    RecCons r rs -> go (mappend m (f r)) rs
-  {-# INLINABLE go #-}
-{-# INLINE foldMap #-}
-
-foldMap1 :: forall f m r rs. Semigroup m
-  => (forall x. f x -> m)
-  -> Rec f (r ': rs)
-  -> m
-foldMap1 f (RecCons b bs) = go (f b) bs
-  where
-  go :: forall ss. m -> Rec f ss -> m
-  go !m record = case record of
-    RecNil -> m
-    RecCons r rs -> go (m SG.<> (f r)) rs
-  {-# INLINABLE go #-}
-{-# INLINE foldMap1 #-}
-
-traverse
-  :: Applicative h
-  => (forall x. f x -> h (g x))
-  -> Rec f rs
-  -> h (Rec g rs)
-traverse _ RecNil = pure RecNil
-traverse f (RecCons x xs) = RecCons <$> f x <*> traverse f xs
-{-# INLINABLE traverse #-}
-
-traverse_
-  :: Applicative h
-  => (forall x. f x -> h b)
-  -> Rec f rs
-  -> h ()
-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)
-
-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
deleted file mode 100644
--- a/src/Topaz/Types.hs
+++ /dev/null
@@ -1,277 +0,0 @@
-{-# 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(..)
-  , Nat(..)
-  , SingNat(..)
-  , Vector(..)
-  , type (++)
-  ) where
-
-import Control.Applicative (liftA2)
-import Data.Exists
-import Data.Foldable (foldrM)
-import Data.Hashable (Hashable(..))
-import Data.Kind (Type)
-import Data.Monoid.Lifted (Semigroup1(..), Monoid1(..), append1)
-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
-
-data SingNat :: Nat -> Type where
-  SingZero :: SingNat 'Zero
-  SingSucc :: SingNat n -> SingNat ('Succ n)
-
-type instance Sing = SingNat
-
-data Vector :: Nat -> Type -> Type where
-  VectorNil :: Vector 'Zero a
-  VectorCons :: a -> Vector n a -> Vector ('Succ n) a
-
-instance Eq a => Eq (Vector n a) where
-  VectorNil == VectorNil = True
-  VectorCons a as == VectorCons b bs = a == b && as == bs
-
-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 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 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
-
-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 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 appendForall
-
-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 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
-  appendForall = recZipWith appendForall
-
-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 (FromJSONForeach f, Reify as) => AE.FromJSON (Rec f as) where
-  parseJSON = parseJSONForeach reify
-
-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 <- 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 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)
-  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 (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 = 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
-    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))
-
-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)
-