diff --git a/src/Data/Type/Boolean.hs b/src/Data/Type/Boolean.hs
--- a/src/Data/Type/Boolean.hs
+++ b/src/Data/Type/Boolean.hs
@@ -1,9 +1,9 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -28,7 +28,7 @@
 
 module Data.Type.Boolean where
 
-import Data.Type.Quantifier (Some(..))
+-- import Data.Type.Quantifier (Some(..))
 import Type.Family.Bool
 import Type.Class.Known
 import Type.Class.Higher
diff --git a/src/Data/Type/Combinator.hs b/src/Data/Type/Combinator.hs
--- a/src/Data/Type/Combinator.hs
+++ b/src/Data/Type/Combinator.hs
@@ -35,8 +35,7 @@
 
 module Data.Type.Combinator where
 
-import Data.Type.Quantifier
-import Data.Type.Index.Trans
+-- import Data.Type.Quantifier
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
@@ -52,8 +51,10 @@
 instance (Functor1 f, Functor1 g) => Functor1 (Comp1 (f :: (l -> *) -> m -> *) (g :: (k -> *) -> l -> *)) where
   map1 f (Comp1 a) = Comp1 $ map1 (map1 f) a
 
+{-
 instance (IxFunctor1 i f, IxFunctor1 j g) => IxFunctor1 (IxComp i j) (Comp1 (f :: (l -> *) -> m -> *) (g :: (k -> *) -> l -> *)) where
   imap1 f = Comp1 . imap1 (\i -> imap1 $ \j -> f $ IxComp i j) . getComp1
+-}
 
 -- (:.:) {{{
 
@@ -322,4 +323,23 @@
 mapJoin f = Join . f . getJoin
 
 -- }}}
+
+data Conj (t :: (k -> *) -> l -> *) (f :: k -> m -> *) :: l -> m -> * where
+  Conj :: t (Flip f b) a
+       -> Conj t f a b
+
+{-
+data Conj2 (t :: (k -> l -> *) -> m -> n -> *) (f :: k -> l -> o -> *) :: m -> n -> o -> * where
+  Conj2 :: t 
+       -> Conj2 t f a b c
+-}
+
+data LL (c :: k -> *) :: l -> (l -> k) -> * where
+  LL :: { getLL :: c (f a)
+        }
+     -> LL c a f
+
+data RR (c :: k -> *) :: (l -> k) -> l -> * where
+  RR :: { getRR :: c (f a) }
+     -> RR c f a
 
diff --git a/src/Data/Type/Difference.hs b/src/Data/Type/Difference.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Difference.hs
@@ -0,0 +1,156 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Difference
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing the removal of a subset of a type level list.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Difference where
+
+-- import Data.Type.Quantifier
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.List
+import Data.Type.Length
+import Data.Type.Subset
+import Data.Type.Remove
+import Data.Type.Sum
+import Control.Arrow (first,left)
+
+data Difference :: [k] -> [k] -> [k] -> * where
+  ØD   :: Difference as Ø as
+  (:-) :: !(Remove bs a cs)
+       -> !(Difference cs as ds)
+       -> Difference bs (a :< as) ds
+infixr 5 :-
+
+diffLen :: Difference as bs cs -> Length bs
+diffLen = \case
+  ØD     -> LZ
+  _ :- d -> LS $ diffLen d
+
+{-
+deriving instance Eq   (Difference as bs cs)
+deriving instance Ord  (Difference as bs cs)
+deriving instance Show (Difference as bs cs)
+
+instance Eq1   (Difference as bs)
+instance Ord1  (Difference as bs)
+instance Show1 (Difference as bs)
+
+instance Eq2   (Difference as)
+instance Ord2  (Difference as)
+instance Show2 (Difference as)
+
+instance Eq3   Difference
+instance Ord3  Difference
+instance Show3 Difference
+-}
+
+{-
+instance Read3 Remove where
+  readsPrec3 d = readParen (d > 10) $ \s0 ->
+    [ (Some3 RZ,s1)
+    | ("RZ",s1) <- lex s0
+    ] ++
+    [ (i >>--- Some3 . RS,s2)
+    | ("RS",s1) <- lex s0
+    , (i,s2)    <- readsPrec3 11 s1
+    ]
+-}
+
+instance TestEquality (Difference as bs) where
+  testEquality = \case
+    ØD -> \case
+      ØD -> qed
+    r1 :- d1 -> \case
+      r2 :- d2 -> r1 =?= r2 //? d1 =?= d2 //? qed
+
+elimDifference :: (forall xs. p xs Ø xs)
+               -> (forall x ws xs ys zs. Remove xs x ys -> Difference ys ws zs -> p ys ws zs -> p xs (x :< ws) zs)
+               -> Difference as bs cs
+               -> p as bs cs
+elimDifference n c = \case
+  ØD     -> n
+  r :- d -> c r d $ elimDifference n c d
+
+{-
+diffSub :: Known Length as => Difference as bs cs -> Subset as bs
+diffSub = \case
+  ØD     -> Ø
+  (r :: Remove as a ds) :- (d :: Difference ds es cs) -> x :< s
+    where
+    x :: Index as a
+    x = remIx r
+    s :: Subset as es
+    s = subTrans s2 s1
+    s1 :: Subset ds es
+    s1 = diffSub d
+    s2 :: Subset as ds
+    s2 = remSub l r
+    l :: Length ds
+    l = _
+-}
+
+{-
+subDiff :: Subset as bs -> Some (Difference as bs)
+subDiff = \case
+  Ø      -> Some ØD
+  x :< s -> ixRem x >>- \r -> subDiff s >>- \d -> Some $ r :- _ d
+-}
+
+diffProd :: Difference as bs cs -> Prod f as -> (Prod f bs,Prod f cs)
+diffProd = \case
+  ØD     -> (,) Ø
+  r :- d -> \as -> let
+    (a,as') = remProd r as
+    in first (a :<) $ diffProd d as'
+
+diffSum :: Difference as bs cs -> Sum f as -> Either (Sum f bs) (Sum f cs)
+diffSum = \case
+  ØD     -> Right
+  r :- d -> \as -> case remSum r as of
+    Left  a  -> Left $ InL a
+    Right bs -> left InR $ diffSum d bs
+
+class WithoutAll (as :: [k]) (bs :: [k]) (cs :: [k]) | as bs -> cs where
+  withoutAll :: Difference as bs cs
+
+instance (cs ~ as) => WithoutAll as Ø cs where
+  withoutAll = ØD
+
+instance (Without as b cs, WithoutAll cs bs ds) => WithoutAll as (b :< bs) ds where
+  withoutAll = without :- withoutAll
+
+instance Witness ØC (WithoutAll as bs cs) (Difference as bs cs) where
+  (\\) r = \case
+    ØD     -> r
+    x :- d -> r \\ x \\ d
+
+instance WithoutAll as bs cs => Known (Difference as bs) cs where
+  type KnownC (Difference as bs) cs = WithoutAll as bs cs
+  known = withoutAll
+
diff --git a/src/Data/Type/Disjunction.hs b/src/Data/Type/Disjunction.hs
--- a/src/Data/Type/Disjunction.hs
+++ b/src/Data/Type/Disjunction.hs
@@ -32,7 +32,7 @@
 
 module Data.Type.Disjunction where
 
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
@@ -135,19 +135,15 @@
   eq1 = \case
     L' a -> \case
       L' b -> a =#= b
-      _    -> False
     R' a -> \case
       R' b -> a =#= b
-      _    -> False
 
 instance (Ord1 f, Ord1 g) => Ord1 (f :+: g) where
   compare1 = \case
     L' a -> \case
       L' b -> compare1 a b
-      _    -> LT
     R' a -> \case
       R' b -> compare1 a b
-      _    -> GT
 
 instance (Show1 f, Show1 g) => Show1 (f :+: g) where
   showsPrec1 d = showParen (d > 10) . \case
diff --git a/src/Data/Type/Fin.hs b/src/Data/Type/Fin.hs
--- a/src/Data/Type/Fin.hs
+++ b/src/Data/Type/Fin.hs
@@ -32,10 +32,11 @@
 
 import Data.Type.Nat
 import Type.Class.Higher
+import Type.Class.Known
 import Type.Class.Witness
 import Type.Family.Constraint
 import Type.Family.Nat
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 
 data Fin :: N -> * where
   FZ :: Fin (S n)
@@ -58,6 +59,20 @@
     | ("FS",s1) <- lex s0
     , (n,s2)    <- readsPrec1 11 s1
     ]
+
+instance (Known Nat n, Pos n) => Enum (Fin n) where
+  toEnum n
+    | n <= 0 = FZ
+    | otherwise = case (known :: Nat n) of
+      S_ Z_   -> FZ
+      S_ S_{} -> FS $ toEnum (n-1)
+  fromEnum = fin
+
+instance (Known Nat n, Pos n) => Bounded (Fin n) where
+  minBound = FZ
+  maxBound = case (known :: Nat n) of
+    S_ Z_   -> FZ
+    S_ S_{} -> FS maxBound
 
 elimFin :: (forall x. p (S x))
         -> (forall x. Fin x -> p x -> p (S x))
diff --git a/src/Data/Type/Fin/Indexed.hs b/src/Data/Type/Fin/Indexed.hs
--- a/src/Data/Type/Fin/Indexed.hs
+++ b/src/Data/Type/Fin/Indexed.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -37,7 +38,7 @@
 import Type.Class.Witness
 import Type.Family.Constraint
 import Type.Family.Nat
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 
 data IFin :: N -> N -> * where
   IFZ :: IFin (S x) Z
diff --git a/src/Data/Type/Index.hs b/src/Data/Type/Index.hs
--- a/src/Data/Type/Index.hs
+++ b/src/Data/Type/Index.hs
@@ -1,10 +1,11 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -29,10 +30,11 @@
 
 module Data.Type.Index where
 
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
+import Type.Family.Constraint
 import Type.Family.List
 
 data Index :: [k] -> k -> * where
@@ -74,16 +76,14 @@
   IZ   -> z
   IS x -> s x $ elimIndex z s x
 
-ixNil :: Index Ø a -> Void
-ixNil = impossible
+ixNil :: Index Ø a -> b
+ixNil = absurd . impossible
 
 onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a
 onIxPred f = \case
   IZ   -> IZ
   IS x -> IS $ f x
 
--- Elem {{{
-
 type a ∈ as = Elem as a
 infix 6 ∈
 
@@ -91,17 +91,45 @@
   elemIndex :: Index as a
 
 instance {-# OVERLAPPING #-} Elem (a :< as) a where
-  elemIndex = IZ
+  elemIndex   = IZ
 
 instance {-# OVERLAPPABLE #-} Elem as a => Elem (b :< as) a where
   elemIndex = IS elemIndex
 
+instance Witness ØC (Elem as a) (Index as a) where
+  (\\) r = \case
+    IZ   -> r
+    IS x -> r \\ x
 
-instance {-# OVERLAPPING #-} Known (Index (a :< as)) a where
-  known = IZ
+instance (a ∈ as) => Known (Index as) a where
+  type KnownC (Index as) a = (a ∈ as)
+  known = elemIndex
 
-instance {-# OVERLAPPABLE #-} Known (Index as) a => Known (Index (b :< as)) a where
-  known = IS known
+class EveryC c as => Every (c :: k -> Constraint) (as :: [k]) where
+  type EveryC c as :: Constraint
+  every :: Index as a -> Wit (c a)
 
--- }}}
+instance Every c Ø where
+  type EveryC c Ø = ØC
+  every = ixNil
+
+instance (c a, Every c as) => Every c (a :< as) where
+  type EveryC c (a :< as) = (c a, Every c as)
+  every = \case
+    IZ   -> Wit
+    IS x -> every x
+
+class ListC ((c <$> xs) <&> y)
+  => Every2 (c :: k -> l -> Constraint) (xs :: [k]) (y :: l) where
+  every2 :: Index xs x -> Wit (c x y)
+
+instance Every2 c Ø y where
+  every2 = ixNil
+
+instance (c x y, Every2 c xs y) => Every2 c (x :< xs) y where
+  every2 = \case
+    IZ   -> Wit
+    IS x -> every2 x
+
+
 
diff --git a/src/Data/Type/Index/Trans.hs b/src/Data/Type/Index/Trans.hs
--- a/src/Data/Type/Index/Trans.hs
+++ b/src/Data/Type/Index/Trans.hs
@@ -6,7 +6,6 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -19,15 +18,18 @@
   , (:~:)(..)
   ) where
 
-import Data.Type.Index
 import Type.Class.Witness ((:~:)(..))
 import Type.Family.List
+import Type.Family.Tuple
 
-ixList :: Index a b -> i b c -> IxList i a c
-ixList = \case
-  IZ   -> IxHead
-  IS x -> IxTail . ixList x
+type IxList' = IxList (:~:)
+type IxEnv   = IxList (IxFirst (:~:))
 
+class IxLift (t :: (k -> m -> *) -> l -> m -> *) (x :: l) where
+  type LiftI t x :: k
+  ixLift :: i (LiftI t x) y
+         -> t i x y
+
 data IxList (i :: k -> l -> *) :: [k] -> l -> * where
   IxHead :: !(i a b)
          -> IxList i (a :< as) b
@@ -38,15 +40,27 @@
   IxFirst :: !(i a b)
           -> IxFirst i '(a,c) b
 
+instance (p ~ '(Fst p,Snd p)) => IxLift IxFirst p where
+  type LiftI IxFirst p = Fst p
+  ixLift = IxFirst
+
 data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where
   IxSecond :: !(i a b)
            -> IxSecond i '(c,a) b
 
+instance (p ~ '(Fst p,Snd p)) => IxLift IxSecond p where
+  type LiftI IxSecond p = Snd p
+  ixLift = IxSecond
+
 data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> * where
   IxOrL :: !(i a b)
         -> IxOr i j (Left a) b
   IxOrR :: !(j a b)
         -> IxOr i j (Right a) b
+
+instance IxLift (IxOr i) (Right a) where
+  type LiftI (IxOr i) (Right a) = a
+  ixLift = IxOrR
 
 data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where
   IxJust :: !(i a b)
diff --git a/src/Data/Type/Length.hs b/src/Data/Type/Length.hs
--- a/src/Data/Type/Length.hs
+++ b/src/Data/Type/Length.hs
@@ -1,9 +1,9 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -29,10 +29,14 @@
 
 module Data.Type.Length where
 
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
+import Type.Class.Witness
 import Type.Class.Higher
 import Type.Class.Known
+import Type.Family.Constraint
 import Type.Family.List
+import Type.Family.Nat
+import Data.Type.Nat
 
 data Length :: [k] -> * where
   LZ :: Length Ø
@@ -62,6 +66,19 @@
 instance Known Length as => Known Length (a :< as) where
   type KnownC Length (a :< as) = Known Length as
   known = LS known
+
+instance (n ~ Len as) => Witness ØC (Known Nat n, Known Length as) (Length as) where
+  type WitnessC ØC (Known Nat n, Known Length as) (Length as) = (n ~ Len as)
+  (\\) r = \case
+    LZ -> r
+    LS l -> r \\ l
+
+{-
+natLen :: Nat (Len as) -> Length as
+natLen = \case
+  Z_   -> LZ
+  S_ n -> _
+-}
 
 elimLength :: p Ø
            -> (forall x xs. Length xs -> p xs -> p (x :< xs))
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -30,7 +30,7 @@
 
 import Data.Type.Boolean
 import Data.Type.Equality
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
diff --git a/src/Data/Type/Nat/Inequality.hs b/src/Data/Type/Nat/Inequality.hs
--- a/src/Data/Type/Nat/Inequality.hs
+++ b/src/Data/Type/Nat/Inequality.hs
@@ -5,7 +5,6 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances #-}
diff --git a/src/Data/Type/Option.hs b/src/Data/Type/Option.hs
--- a/src/Data/Type/Option.hs
+++ b/src/Data/Type/Option.hs
@@ -79,5 +79,4 @@
   type WitnessC p q (Option f x) = Witness p q (f (FromJust x))
   (\\) r = \case
     Just_ a -> r \\ a
-    _       -> error "impossible type"
 
diff --git a/src/Data/Type/Product.hs b/src/Data/Type/Product.hs
--- a/src/Data/Type/Product.hs
+++ b/src/Data/Type/Product.hs
@@ -44,7 +44,7 @@
 import Data.Type.Conjunction
 import Data.Type.Index
 import Data.Type.Length
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
@@ -67,19 +67,15 @@
   eq1 = \case
     Ø -> \case
       Ø -> True
-      _ -> False
     a :< as -> \case
       b :< bs -> a =#= b && as =#= bs
-      _       -> False
 
 instance Ord1 f => Ord1 (Prod f) where
   compare1 = \case
     Ø -> \case
       Ø -> EQ
-      _ -> LT
     a :< as -> \case
       b :< bs -> compare1 a b `mappend` compare1 as bs
-      _       -> GT
 
 instance Show1 f => Show1 (Prod f) where
   showsPrec1 d = \case
@@ -276,12 +272,27 @@
     Ø       -> pure Ø
     a :< as -> (:<) <$> f IZ a <*> itraverse1 (f . IS) as
 
+instance (Known Length as, Every (Known f) as) => Known (Prod f) as where
+  type KnownC (Prod f) as = (Known Length as, Every (Known f) as)
+  known = go known
+    where
+    go :: Every (Known f) xs => Length xs -> Prod f xs
+    go = \case
+      LZ   -> Ø
+      LS l -> known :< go l
+
+{-
 instance Known (Prod f) Ø where
   known = Ø
 
 instance (Known f a, Known (Prod f) as) => Known (Prod f) (a :< as) where
   type KnownC (Prod f) (a :< as) = (Known f a, Known (Prod f) as)
   known = known :< known
+-}
+
+type family Witnesses (ps :: [Constraint]) (qs :: [Constraint]) (f :: k -> *) (as :: [k]) :: Constraint where
+  Witnesses Ø Ø f Ø = ØC
+  Witnesses (p :< ps) (q :< qs) f (a :< as) = (Witness p q (f a), Witnesses ps qs f as)
 
 instance Witness ØC ØC (Prod f Ø) where
   r \\ _ = r
diff --git a/src/Data/Type/Product/Env.hs b/src/Data/Type/Product/Env.hs
--- a/src/Data/Type/Product/Env.hs
+++ b/src/Data/Type/Product/Env.hs
@@ -5,7 +5,6 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -110,4 +109,9 @@
 
 instance IxFunctor1 (IxList (IxSecond (:~:))) (Env k) where
   imap1 f = Env . imap1 (\i -> imap1 $ \j -> f $ ixList i j) . getEnv
+
+ixList :: Index as a -> i a b -> IxList i as b
+ixList = \case
+  IZ   -> IxHead
+  IS x -> IxTail . ixList x
 
diff --git a/src/Data/Type/Quantifier.hs b/src/Data/Type/Quantifier.hs
deleted file mode 100644
--- a/src/Data/Type/Quantifier.hs
+++ /dev/null
@@ -1,188 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Type.Quantifier
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- Types for working with (and under) existentially and universally
--- quantified types.
---
--- The 'Some' type can be very useful when working with type-indexed GADTs,
--- where defining instances for classes like 'Read' can be tedious at best,
--- and frequently impossible, for the GADT itself.
---
------------------------------------------------------------------------------
-
-module Data.Type.Quantifier where
-
-import Type.Family.Constraint
-
--- Some {{{
-
-data Some (f :: k -> *) :: * where
-  Some :: f a -> Some f
-
--- | An eliminator for a 'Some' type.
---
--- Consider this function akin to a Monadic bind, except
--- instead of binding into a Monad with a sequent function,
--- we're binding into the existential quantification with
--- a universal eliminator function.
---
--- It serves as an explicit delimiter in a program of where
--- the type index may be used and depended on, and where it may
--- not.
---
--- NB: the result type of the eliminating function may
--- not refer to the universally quantified type index @a@.
---
-some :: Some f -> (forall a. f a -> r) -> r
-some (Some a) f = f a
-
-(>>-) :: Some f -> (forall a. f a -> r) -> r
-(>>-) = some
-infixl 1 >>-
-
-(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h
-(f >-> g) a = f a >>- g
-infixr 1 >->
-
-withSome :: (forall a. f a -> r) -> Some f -> r
-withSome f (Some a) = f a
-
-onSome :: (forall a. f a -> g x) -> Some f -> Some g
-onSome f (Some a) = Some (f a)
-
-msome :: Monad m => f a -> m (Some f)
-msome = return . Some
-
-(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r
-m >>=- f = do
-  s <- m
-  s >>- f
-infixl 1 >>=-
-
--- }}}
-
--- Some2 {{{
-
-data Some2 (f :: k -> l -> *) :: * where
-  Some2 :: f a b -> Some2 f
-
-some2 :: Some2 f -> (forall a b. f a b -> r) -> r
-some2 (Some2 a) f = f a
-
-(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r
-(>>--) = some2
-infixl 1 >>--
-
-(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h
-(f >--> g) a = f a >>-- g
-infixr 1 >-->
-
-withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
-withSome2 f (Some2 a) = f a
-
-onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
-onSome2 f (Some2 a) = Some2 (f a)
-
-msome2 :: Monad m => f a b -> m (Some2 f)
-msome2 = return . Some2
-
-(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r
-m >>=-- f = do
-  s <- m
-  s >>-- f
-infixl 1 >>=--
-
--- }}}
-
--- Some3 {{{
-
-data Some3 (f :: k -> l -> m -> *) :: * where
-  Some3 :: f a b c -> Some3 f
-
-some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r
-some3 (Some3 a) f = f a
-
-(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
-(>>---) = some3
-infixl 1 >>---
-
-(>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h
-(f >---> g) a = f a >>--- g
-infixr 1 >--->
-
-withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
-withSome3 f (Some3 a) = f a
-
-onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
-onSome3 f (Some3 a) = Some3 (f a)
-
-msome3 :: Monad m => f a b c -> m (Some3 f)
-msome3 = return . Some3
-
-(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r
-m >>=--- f = do
-  s <- m
-  s >>--- f
-infixl 1 >>=---
-
--- }}}
-
--- SomeC {{{
-
-data SomeC (c :: k -> Constraint) (f :: k -> *) where
-  SomeC :: c a => f a -> SomeC c f
-
-someC :: SomeC c f -> (forall a. c a => f a -> r) -> r
-someC (SomeC a) f = f a
-
-(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r
-(>>~) = someC
-infixl 1 >>~
-
-msomeC :: (Monad m, c a) => f a -> m (SomeC c f)
-msomeC = return . SomeC
-
-(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r
-m >>=~ f = do
-  s <- m
-  s >>~ f
-infixl 1 >>=~
-
--- }}}
-
--- EveryN {{{
-
-data Every (f :: k -> *) :: * where
-  Every :: { instEvery :: forall a. f a } -> Every f
-
-data Every2 (f :: k -> l -> *) :: * where
-  Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f
-
-data Every3 (f :: k -> l -> m -> *) :: * where
-  Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f
-
-data EveryC (c :: k -> Constraint) (f :: k -> *) :: * where
-  EveryC :: { instEveryC :: forall a. c a => f a }
-         -> EveryC c f
-
--- }}}
-
diff --git a/src/Data/Type/Remove.hs b/src/Data/Type/Remove.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Remove.hs
@@ -0,0 +1,148 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Remove
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing the removal of an element from a type level list.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Remove where
+
+-- import Data.Type.Quantifier
+import Type.Class.Higher
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.Constraint
+import Type.Family.List
+import Type.Family.Nat
+import Data.Type.Length
+import Data.Type.Index
+import Data.Type.Subset
+import Data.Type.Product
+import Data.Type.Sum
+import Control.Arrow (second,right)
+
+data Remove :: [k] -> k -> [k] -> * where
+  RZ :: Remove (a :< as) a as
+  RS :: !(Remove as a bs)
+     -> Remove (b :< as) a (b :< bs)
+
+deriving instance Eq   (Remove as a bs)
+deriving instance Ord  (Remove as a bs)
+deriving instance Show (Remove as a bs)
+
+instance Eq1   (Remove as a)
+instance Ord1  (Remove as a)
+instance Show1 (Remove as a)
+
+instance Eq2   (Remove as)
+instance Ord2  (Remove as)
+instance Show2 (Remove as)
+
+instance Eq3   Remove
+instance Ord3  Remove
+instance Show3 Remove
+
+instance Read3 Remove where
+  readsPrec3 d = readParen (d > 10) $ \s0 ->
+    [ (Some3 RZ,s1)
+    | ("RZ",s1) <- lex s0
+    ] ++
+    [ (i >>--- Some3 . RS,s2)
+    | ("RS",s1) <- lex s0
+    , (i,s2)    <- readsPrec3 11 s1
+    ]
+
+instance TestEquality (Remove as a) where
+  testEquality = \case
+    RZ -> \case
+      RZ -> qed
+      _  -> Nothing
+    RS x -> \case
+      RS y -> x =?= y //? qed
+      _    -> Nothing
+
+remLen :: Remove as a bs -> S (Len bs) :~: Len as
+remLen = \case
+  RZ   -> Refl
+  RS r -> remLen r // Refl
+
+elimRemove :: (forall xs. p (a :< xs) a xs)
+           -> (forall x xs ys. Remove xs a ys -> p xs a ys -> p (x :< xs) a (x :< ys))
+           -> Remove as a bs
+           -> p as a bs
+elimRemove z s = \case
+  RZ   -> z
+  RS r -> s r $ elimRemove z s r
+
+remIx :: Remove as a bs -> Index as a
+remIx = \case
+  RZ   -> IZ
+  RS r -> IS $ remIx r
+
+remSub :: Length bs -> Remove as a bs -> Subset as bs
+remSub = \case
+  LZ   -> \case
+    RZ -> Ø
+  LS l -> \case
+    RZ   -> IS IZ :< map1 (IS . IS) subRefl \\ l
+    RS r -> IZ :< map1 IS (remSub l r)
+
+ixRem :: Index as a -> Some (Remove as a)
+ixRem = \case
+  IZ   -> Some RZ
+  IS x -> ixRem x >>- Some . RS
+
+remProd :: Remove as a bs -> Prod f as -> (f a,Prod f bs)
+remProd = \case
+  RZ   -> (,) <$> head' <*> tail'
+  RS r -> \(a :< as) -> second (a :<) $ remProd r as
+
+remSum :: Remove as a bs -> Sum f as -> Either (f a) (Sum f bs)
+remSum = \case
+  RZ   -> \case
+    InL a -> Left a
+    InR b -> Right b
+  RS r -> \case
+    InL a -> Right $ InL a
+    InR b -> right InR $ remSum r b
+
+class Without (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs where
+  without :: Remove as a bs
+
+instance {-# OVERLAPPING #-} (as ~ bs) => Without (a :< as) a bs where
+  without = RZ
+
+instance {-# OVERLAPPABLE #-} (cs ~ (b :< bs), Without as a bs) => Without (b :< as) a cs where
+  without = RS without
+
+instance Witness ØC (Without as a bs) (Remove as a bs) where
+  (\\) r = \case
+    RZ   -> r
+    RS x -> r \\ x
+
+instance (Without as a bs) => Known (Remove as a) bs where
+  type KnownC (Remove as a) bs = Without as a bs
+  known = without
+
diff --git a/src/Data/Type/Subset.hs b/src/Data/Type/Subset.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Subset.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Type.Subset
+-- Copyright   :  Copyright (C) 2015 Kyle Carter
+-- License     :  BSD3
+--
+-- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
+-- Stability   :  experimental
+-- Portability :  RankNTypes
+--
+-- A @singleton@-esque type for representing subsets of a type level list.
+--
+-----------------------------------------------------------------------------
+
+module Data.Type.Subset
+  ( module Data.Type.Subset
+  , module Exports
+  ) where
+
+-- import Data.Type.Quantifier
+import Type.Class.Higher
+import Type.Class.Known
+import Type.Class.Witness
+import Type.Family.List
+import Data.Type.Index
+import Data.Type.Length
+import Data.Type.Product as Exports (Prod(..))
+import Data.Type.Product (index)
+import Data.Type.Sum (Sum(..),prj)
+import Control.Applicative ((<|>))
+
+type Subset as = Prod (Index as)
+
+subNil :: Subset Ø as -> (as :~: Ø)
+subNil = \case
+  Ø      -> Refl
+  x :< _ -> ixNil x
+
+type as ⊆ bs = Every (Elem bs) as
+infix 4 ⊆
+
+subRefl :: Known Length as
+  => Subset as as
+subRefl = go known
+  where
+  go :: Length xs -> Subset xs xs
+  go = \case
+    LZ   -> Ø
+    LS l -> IZ :< map1 IS (go l)
+
+subTrans :: Subset as bs -> Subset bs cs -> Subset as cs
+subTrans s = map1 $ subIx s
+
+subProd :: Subset as bs -> Prod f as -> Prod f bs
+subProd = \case
+  Ø      -> pure Ø
+  x :< s -> (:<) <$> index x <*> subProd s
+
+subSum :: Subset as bs -> Sum f as -> Maybe (Sum f bs)
+subSum = \case
+  Ø      -> pure Nothing
+  x :< s -> \t -> (InL <$> (prj t \\ x))
+              <|> (InR <$> subSum s t)
+
+subIx :: Subset as bs -> Index bs x -> Index as x
+subIx = \case
+  Ø      -> ixNil
+  x :< s -> \case
+    IZ   -> x
+    IS y -> subIx s y
+
+subExt :: Known Length as => (forall x. Index as x -> Index bs x) -> Subset bs as
+subExt f = subExtBy f known
+
+subExtBy :: (forall x. Index as x -> Index bs x) -> Length as -> Subset bs as
+subExtBy f = \case
+  LZ   -> Ø
+  LS l -> f IZ :< subExtBy (f . IS) l
+
diff --git a/src/Data/Type/Sum.hs b/src/Data/Type/Sum.hs
--- a/src/Data/Type/Sum.hs
+++ b/src/Data/Type/Sum.hs
@@ -32,7 +32,7 @@
 module Data.Type.Sum where
 
 import Data.Type.Index
-import Data.Type.Quantifier
+-- import Data.Type.Quantifier
 
 import Type.Class.Higher
 import Type.Class.Witness
diff --git a/src/Data/Type/Sym.hs b/src/Data/Type/Sym.hs
deleted file mode 100644
--- a/src/Data/Type/Sym.hs
+++ /dev/null
@@ -1,67 +0,0 @@
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE GADTs #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Type.Sym
--- Copyright   :  Copyright (C) 2015 Kyle Carter
--- License     :  BSD3
---
--- Maintainer  :  Kyle Carter <kylcarte@indiana.edu>
--- Stability   :  experimental
--- Portability :  RankNTypes
---
--- A @singleton@-esque type for representing type-level Symbols.
---
------------------------------------------------------------------------------
-
-module Data.Type.Sym where
-
-import Data.Type.Boolean
-import Type.Class.Higher
-import Type.Class.Known
-import Type.Class.Witness
-import Type.Family.Constraint
-import Type.Family.Symbol
-import Data.Proxy
-
-data Sym :: Symbol -> * where
-  Sym :: KnownSymbol x => Sym x
-
-deriving instance Eq   (Sym x)
-deriving instance Ord  (Sym x)
-
-instance Show (Sym x) where
-  showsPrec d x = showParen (d > 0)
-    $ showString "Sym "
-    . shows (symbol x)
-
-instance Eq1   Sym
-instance Ord1  Sym
-instance Show1 Sym
-
-instance TestEquality Sym where
-  testEquality Sym Sym = sameSymbol Proxy Proxy
-
-instance KnownSymbol x => Known Sym x where
-  type KnownC Sym x = KnownSymbol x
-  known = Sym
-
-instance Witness ØC (KnownSymbol x) (Sym x) where
-  r \\ Sym = r
-
-symbol :: Sym x -> String
-symbol x = symbolVal x \\ x
-
diff --git a/src/Data/Type/Vector.hs b/src/Data/Type/Vector.hs
--- a/src/Data/Type/Vector.hs
+++ b/src/Data/Type/Vector.hs
@@ -25,13 +25,13 @@
 -- Stability   :  experimental
 -- Portability :  RankNTypes
 --
--- 'V' and its combinator analog 'VT' represent lists
+-- 'Vec' and its combinator analog 'VecT' represent lists
 -- of known length, characterized by the index @(n :: N)@ in
--- @'V' n a@ or @'VT' n f a@.
+-- @'Vec' n a@ or @'VecT' n f a@.
 --
 -- The classic example used ad nauseum for type-level programming.
 --
--- The operations on 'V' and 'VT' correspond to the type level arithmetic
+-- The operations on 'Vec' and 'VecT' correspond to the type level arithmetic
 -- operations on the kind 'N'.
 --
 -----------------------------------------------------------------------------
@@ -44,6 +44,7 @@
 import Data.Type.Nat
 import Data.Type.Product (Prod(..),curry',pattern (:>))
 
+import Type.Class.Higher
 import Type.Class.Known
 import Type.Class.Witness
 
@@ -54,162 +55,179 @@
 import qualified Data.List as L
 import Data.Monoid
 
-data VT (n :: N) (f :: k -> *) :: k -> * where
-  ØV   :: VT Z f a
-  (:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a
+data VecT (n :: N) (f :: k -> *) :: k -> * where
+  ØV   :: VecT Z f a
+  (:*) :: !(f a) -> !(VecT n f a) -> VecT (S n) f a
 infixr 4 :*
 
-elimVT :: p Z
+elimVecT :: p Z
        -> (forall x. f a -> p x -> p (S x))
-       -> VT n f a
+       -> VecT n f a
        -> p n
-elimVT z s = \case
+elimVecT z s = \case
   ØV      -> z
-  a :* as -> s a $ elimVT z s as
+  a :* as -> s a $ elimVecT z s as
 
 elimV :: p Z
       -> (forall x. a -> p x -> p (S x))
-      -> V n a
+      -> Vec n a
       -> p n
-elimV z s = elimVT z $ s . getI
+elimV z s = elimVecT z $ s . getI
 
-type V n = VT n I
-pattern (:+) :: a -> V n a -> V (S n) a
+type Vec n = VecT n I
+pattern (:+) :: a -> Vec n a -> Vec (S n) a
 pattern a :+ as = I a :* as
 infixr 4 :+
 
-deriving instance Eq   (f a) => Eq   (VT n f a)
-deriving instance Ord  (f a) => Ord  (VT n f a)
-deriving instance Show (f a) => Show (VT n f a)
+deriving instance Eq   (f a) => Eq   (VecT n f a)
+deriving instance Ord  (f a) => Ord  (VecT n f a)
+deriving instance Show (f a) => Show (VecT n f a)
 
-(.++) :: VT x f a -> VT y f a -> VT (x + y) f a
+(.++) :: VecT x f a -> VecT y f a -> VecT (x + y) f a
 (.++) = \case
   ØV      -> id
   a :* as -> (a :*) . (as .++)
 infixr 5 .++
 
-vrep :: forall n f a. Known Nat n => f a -> VT n f a
+vrep :: forall n f a. Known Nat n => f a -> VecT n f a
 vrep a = go (known :: Nat n)
   where
-  go :: Nat x -> VT x f a
+  go :: Nat x -> VecT x f a
   go = \case
     Z_   -> ØV
     S_ x -> a :* go x
 
-head' :: VT (S n) f a -> f a
+head' :: VecT (S n) f a -> f a
 head' (a :* _) = a
 
-tail' :: VT (S n) f a -> VT n f a
+tail' :: VecT (S n) f a -> VecT n f a
 tail' (_ :* as) = as
 
-onTail :: (VT m f a -> VT n f a) -> VT (S m) f a -> VT (S n) f a
+onTail :: (VecT m f a -> VecT n f a) -> VecT (S m) f a -> VecT (S n) f a
 onTail f (a :* as) = a :* f as
 
-vDel :: Fin n -> VT n f a -> VT (Pred n) f a
+vDel :: Fin n -> VecT n f a -> VecT (Pred n) f a
 vDel = \case
   FZ   -> tail'
   FS x -> onTail (vDel x) \\ x
 
-imap :: (Fin n -> f a -> g b) -> VT n f a -> VT n g b
+imap :: (Fin n -> f a -> g b) -> VecT n f a -> VecT n g b
 imap f = \case
   ØV      -> ØV
   a :* as -> f FZ a :* imap (f . FS) as
 
-ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VT n f a -> m
+ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VecT n f a -> m
 ifoldMap f = \case
   ØV      -> mempty
   a :* as -> f FZ a <> ifoldMap (f . FS) as
 
-itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VT n f a -> h (VT n g b)
+itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VecT n f a -> h (VecT n g b)
 itraverse f = \case
   ØV      -> pure ØV
   a :* as -> (:*) <$> f FZ a <*> itraverse (f . FS) as
 
-index :: Fin n -> VT n f a -> f a
+index :: Fin n -> VecT n f a -> f a
 index = \case
   FZ   -> head'
   FS x -> index x . tail'
 
-vmap :: (f a -> g b) -> VT n f a -> VT n g b
+index' :: Fin n -> Vec n a -> a
+index' i = getI . index i
+
+vmap :: (f a -> g b) -> VecT n f a -> VecT n g b
 vmap f = \case
   ØV      -> ØV
   a :* as -> f a :* vmap f as
 
-vap :: (f a -> g b -> h c) -> VT n f a -> VT n g b -> VT n h c
+vap :: (f a -> g b -> h c) -> VecT n f a -> VecT n g b -> VecT n h c
 vap f = \case
-  ØV  -> \_ -> ØV
+  ØV      -> const ØV
   a :* as -> \case
     b :* bs -> f a b :* vap f as bs
-    _       -> error "impossible type"
 
-vfoldr :: (f a -> b -> b) -> b -> VT n f a -> b
+vfoldr :: (f a -> b -> b) -> b -> VecT n f a -> b
 vfoldr s z = \case
   ØV      -> z
   a :* as -> s a $ vfoldr s z as
 
-vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VT n f a -> b
+vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VecT n f a -> b
 vfoldMap' j z f = \case
   ØV       -> z
   a :* ØV  -> f a
   a :* as  -> j (f a) $ vfoldMap' j z f as
 
-vfoldMap :: Monoid m => (f a -> m) -> VT n f a -> m
+vfoldMap :: Monoid m => (f a -> m) -> VecT n f a -> m
 vfoldMap f = \case
   ØV      -> mempty
   a :* as -> f a <> vfoldMap f as
 
-withVT :: [f a] -> (forall n. VT n f a -> r) -> r
-withVT as k = case as of
+withVecT :: [f a] -> (forall n. VecT n f a -> r) -> r
+withVecT as k = case as of
   []      -> k ØV
-  a : as' -> withVT as' $ \v -> k $ a :* v
+  a : as' -> withVecT as' $ \v -> k $ a :* v
 
-withV :: [a] -> (forall n. V n a -> r) -> r
-withV as k = withVT (I <$> as) k
+withV :: [a] -> (forall n. Vec n a -> r) -> r
+withV as = withVecT (I <$> as)
 
-findV :: Eq a => a -> V n a -> Maybe (Fin n)
-findV = findVT . I
+findV :: Eq a => a -> Vec n a -> Maybe (Fin n)
+findV = findVecT . I
 
-findVT :: Eq (f a) => f a -> VT n f a -> Maybe (Fin n)
-findVT a = \case
+findVecT :: Eq (f a) => f a -> VecT n f a -> Maybe (Fin n)
+findVecT a = \case
   ØV      -> Nothing
   b :* as -> if a == b
     then Just FZ
-    else FS <$> findVT a as
+    else FS <$> findVecT a as
 
-instance Functor f => Functor (VT n f) where
+instance Functor1 (VecT n) where
+  map1 f = \case
+    ØV      -> ØV
+    a :* as -> f a :* map1 f as
+
+instance Foldable1 (VecT n) where
+  foldMap1 f = \case
+    ØV -> mempty
+    a :* as -> f a <> foldMap1 f as
+
+instance Traversable1 (VecT n) where
+  traverse1 f = \case
+    ØV      -> pure ØV
+    a :* as -> (:*) <$> f a <*> traverse1 f as
+
+instance Functor f => Functor (VecT n f) where
   fmap = vmap . fmap
 
-instance (Applicative f, Known Nat n) => Applicative (VT n f) where
+instance (Applicative f, Known Nat n) => Applicative (VecT n f) where
   pure  = vrep . pure
   (<*>) = vap (<*>)
 
-instance (Monad f, Known Nat n) => Monad (VT n f) where
+instance (Monad f, Known Nat n) => Monad (VecT n f) where
   v >>= f = imap (\x -> (>>= index x . f)) v
 
-instance Foldable f => Foldable (VT n f) where
+instance Foldable f => Foldable (VecT n f) where
   foldMap f = \case
     ØV      -> mempty
     a :* as -> foldMap f a <> foldMap f as
 
-instance Traversable f => Traversable (VT n f) where
+instance Traversable f => Traversable (VecT n f) where
   traverse f = \case
     ØV      -> pure ØV
     a :* as -> (:*) <$> traverse f a <*> traverse f as
 
 {-
-instance (Witness p q (f a), n ~ S x) => Witness p q (VT n f a) where
-  type WitnessC p q (VT n f a) = Witness p q (f a)
+instance (Witness p q (f a), n ~ S x) => Witness p q (VecT n f a) where
+  type WitnessC p q (VecT n f a) = Witness p q (f a)
   (\\) r = \case
     a :* _ -> r \\ a
     _      -> error "impossible type"
 -}
 
-instance Witness ØC (Known Nat n) (VT n f a) where
+instance Witness ØC (Known Nat n) (VecT n f a) where
   (\\) r = \case
     ØV      -> r
     _ :* as -> r \\ as
 
-instance (Num (f a), Known Nat n) => Num (VT n f a) where
+instance (Num (f a), Known Nat n) => Num (VecT n f a) where
   (*)         = vap (*)
   (+)         = vap (+)
   (-)         = vap (-)
@@ -234,12 +252,12 @@
 
 type family Matrix (ns :: [N]) :: * -> * where
   Matrix Ø         = I
-  Matrix (n :< ns) = VT n (Matrix ns)
+  Matrix (n :< ns) = VecT n (Matrix ns)
 
-vgen_ :: Known Nat n => (Fin n -> f a) -> VT n f a
+vgen_ :: Known Nat n => (Fin n -> f a) -> VecT n f a
 vgen_ = vgen known
 
-vgen :: Nat n -> (Fin n -> f a) -> VT n f a
+vgen :: Nat n -> (Fin n -> f a) -> VecT n f a
 vgen x f = case x of
   Z_   -> ØV
   S_ y -> f FZ :* vgen y (f . FS)
@@ -255,10 +273,10 @@
 onMatrix :: (Matrix ms a -> Matrix ns b) -> M ms a -> M ns b
 onMatrix f = M . f . getMatrix
 
-diagonal :: VT n (VT n f) a -> VT n f a
+diagonal :: VecT n (VecT n f) a -> VecT n f a
 diagonal = imap index
 
-vtranspose :: Known Nat n => VT m (VT n f) a -> VT n (VT m f) a
+vtranspose :: Known Nat n => VecT m (VecT n f) a -> VecT n (VecT m f) a
 vtranspose v = vgen_ $ \x -> vmap (index x) v
 
 transpose :: Known Nat n => M (m :< n :< ns) a -> M (n :< m :< ns) a
@@ -279,7 +297,7 @@
 m4 :: M '[N2,N3,N4,N5] (Int,Int,Int,Int)
 m4 = mgen_ $ \(w :< x :< y :> z) -> (fin w,fin x,fin y,fin z)
 
-ppVec :: (VT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VT n f a -> ShowS
+ppVec :: (VecT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VecT n f a -> ShowS
 ppVec pV pF = pV . vmap pF
 
 ppMatrix :: forall ns a. (Show a, Known Length ns) => M ns a -> IO ()
@@ -343,7 +361,7 @@
 infixl 6 ^+^, ^-^
 
 instance Additive I
-instance (Additive f, Known Nat n) => Additive (VT n f) where
+instance (Additive f, Known Nat n) => Additive (VecT n f) where
   zero   = vrep zero
   liftU2 = vap . liftU2
   liftI2 = vap . liftI2
@@ -363,8 +381,8 @@
 infixl 6 .-., .+^, .-^
 
 instance Affine I
-instance (Affine f, Known Nat n) => Affine (VT n f) where
-  type Diff (VT n f) = VT n (Diff f)
+instance (Affine f, Known Nat n) => Affine (VecT n f) where
+  type Diff (VecT n f) = VecT n (Diff f)
   (.-.) = vap (.-.)
   (.+^) = vap (.+^)
   (.-^) = vap (.-^)
@@ -388,7 +406,7 @@
 instance Metric I where
   dot (I a) (I b) = a * b
 
-instance (Metric f, Known Nat n) => Metric (VT n f) where
+instance (Metric f, Known Nat n) => Metric (VecT n f) where
   dot a b = getSum $ foldMap Sum $ vap ((I .) . dot) a b
 
 (*^) :: (Functor f, Num a) => a -> f a -> f a
diff --git a/src/Type/Class/Higher.hs b/src/Type/Class/Higher.hs
--- a/src/Type/Class/Higher.hs
+++ b/src/Type/Class/Higher.hs
@@ -22,12 +22,15 @@
 -- Stability   :  experimental
 -- Portability :  RankNTypes
 --
--- Higher order analogs of type classes from the Prelude.
+-- Higher order analogs of type classes from the Prelude,
+-- and quantifier data types.
 ----------------------------------------------------------------------------
 
 module Type.Class.Higher where
 
-import Data.Type.Quantifier
+import Type.Class.Witness
+import Type.Family.Constraint
+import Data.Maybe (fromMaybe)
 
 -- EqN {{{
 
@@ -124,7 +127,6 @@
 shows1 :: Show1 f => f a -> ShowS
 shows1 = showsPrec1 0
 
-
 class Show2 (f :: k -> l -> *) where
   showsPrec2 :: Int -> f a b -> ShowS
   default showsPrec2 :: Show (f a b) => Int -> f a b -> ShowS
@@ -135,7 +137,6 @@
 shows2 :: Show2 f => f a b -> ShowS
 shows2 = showsPrec2 0
 
-
 class Show3 (f :: k -> l -> m -> *) where
   showsPrec3 :: Int -> f a b c -> ShowS
   default showsPrec3 :: Show (f a b c) => Int -> f a b c -> ShowS
@@ -233,4 +234,164 @@
           -> t f' g' b
 
 -- }}}
+
+
+
+-- Some {{{
+
+data Some (f :: k -> *) :: * where
+  Some :: f a -> Some f
+
+instance (TestEquality f, Eq1 f) => Eq (Some f) where
+  Some a == Some b = fromMaybe False $ testEquality a b //? return (eq1 a b)
+
+-- | An eliminator for a 'Some' type.
+--
+-- Consider this function akin to a Monadic bind, except
+-- instead of binding into a Monad with a sequent function,
+-- we're binding into the existential quantification with
+-- a universal eliminator function.
+--
+-- It serves as an explicit delimiter in a program of where
+-- the type index may be used and depended on, and where it may
+-- not.
+--
+-- NB: the result type of the eliminating function may
+-- not refer to the universally quantified type index @a@.
+--
+some :: Some f -> (forall a. f a -> r) -> r
+some (Some a) f = f a
+
+(>>-) :: Some f -> (forall a. f a -> r) -> r
+(>>-) = some
+infixl 1 >>-
+
+(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h
+(f >-> g) a = f a >>- g
+infixr 1 >->
+
+withSome :: (forall a. f a -> r) -> Some f -> r
+withSome f (Some a) = f a
+
+onSome :: (forall a. f a -> g x) -> Some f -> Some g
+onSome f (Some a) = Some (f a)
+
+msome :: Monad m => f a -> m (Some f)
+msome = return . Some
+
+(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r
+m >>=- f = do
+  s <- m
+  s >>- f
+infixl 1 >>=-
+
+-- }}}
+
+-- Some2 {{{
+
+data Some2 (f :: k -> l -> *) :: * where
+  Some2 :: f a b -> Some2 f
+
+some2 :: Some2 f -> (forall a b. f a b -> r) -> r
+some2 (Some2 a) f = f a
+
+(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r
+(>>--) = some2
+infixl 1 >>--
+
+(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h
+(f >--> g) a = f a >>-- g
+infixr 1 >-->
+
+withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
+withSome2 f (Some2 a) = f a
+
+onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
+onSome2 f (Some2 a) = Some2 (f a)
+
+msome2 :: Monad m => f a b -> m (Some2 f)
+msome2 = return . Some2
+
+(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r
+m >>=-- f = do
+  s <- m
+  s >>-- f
+infixl 1 >>=--
+
+-- }}}
+
+-- Some3 {{{
+
+data Some3 (f :: k -> l -> m -> *) :: * where
+  Some3 :: f a b c -> Some3 f
+
+some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r
+some3 (Some3 a) f = f a
+
+(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
+(>>---) = some3
+infixl 1 >>---
+
+(>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h
+(f >---> g) a = f a >>--- g
+infixr 1 >--->
+
+withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
+withSome3 f (Some3 a) = f a
+
+onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
+onSome3 f (Some3 a) = Some3 (f a)
+
+msome3 :: Monad m => f a b c -> m (Some3 f)
+msome3 = return . Some3
+
+(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r
+m >>=--- f = do
+  s <- m
+  s >>--- f
+infixl 1 >>=---
+
+-- }}}
+
+-- SomeC {{{
+
+data SomeC (c :: k -> Constraint) (f :: k -> *) where
+  SomeC :: c a => f a -> SomeC c f
+
+someC :: SomeC c f -> (forall a. c a => f a -> r) -> r
+someC (SomeC a) f = f a
+
+(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r
+(>>~) = someC
+infixl 1 >>~
+
+msomeC :: (Monad m, c a) => f a -> m (SomeC c f)
+msomeC = return . SomeC
+
+(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r
+m >>=~ f = do
+  s <- m
+  s >>~ f
+infixl 1 >>=~
+
+-- }}}
+
+{-
+-- EveryN {{{
+
+data Every (f :: k -> *) :: * where
+  Every :: { instEvery :: forall a. f a } -> Every f
+
+data Every2 (f :: k -> l -> *) :: * where
+  Every2 :: { instEvery2 :: forall a b. f a b } -> Every2 f
+
+data Every3 (f :: k -> l -> m -> *) :: * where
+  Every3 :: { instEvery3 :: forall a b c. f a b c } -> Every3 f
+
+data EveryC (c :: k -> Constraint) (f :: k -> *) :: * where
+  EveryC :: { instEveryC :: forall a. c a => f a }
+         -> EveryC c f
+
+-- }}}
+-}
 
diff --git a/src/Type/Class/Known.hs b/src/Type/Class/Known.hs
--- a/src/Type/Class/Known.hs
+++ b/src/Type/Class/Known.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
diff --git a/src/Type/Class/Witness.hs b/src/Type/Class/Witness.hs
--- a/src/Type/Class/Witness.hs
+++ b/src/Type/Class/Witness.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
@@ -5,7 +6,6 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -156,7 +156,7 @@
 infixr 6 ∨
 
 eitherC :: forall f g a b. f a :- b -> g a :- b -> (f ∨ g) a :- b
-eitherC f g = Sub $ case ((disjC :: Either (Wit (f a)) (Wit (g a))),f,g) of
+eitherC f g = Sub $ case (disjC :: Either (Wit (f a)) (Wit (g a)),f,g) of
   (Left  a,Sub b,_    ) -> b \\ a
   (Right a,_    ,Sub b) -> b \\ a
 
@@ -180,7 +180,7 @@
 -- Initial/Terminal {{{
 
 toEquality :: (a ~ b) :- (c ~ d) -> a :~: b -> c :~: d
-toEquality p = \Refl -> Refl \\ p
+toEquality p Refl = Refl \\ p
 
 commute :: (a ~ b) :- (b ~ a)
 commute = Sub Wit
diff --git a/src/Type/Family/Bool.hs b/src/Type/Family/Bool.hs
--- a/src/Type/Family/Bool.hs
+++ b/src/Type/Family/Bool.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -34,7 +35,7 @@
 import Type.Class.Witness as Exports (type (==))
 import Data.Type.Bool as Exports (type If, type Not, type (||), type (&&))
 
-type family BoolC (b :: Bool) :: Constraint where
+type family BoolC (b :: Bool) = (c :: Constraint) | c -> b where
   BoolC True  = ØC
   BoolC False = Fail
 
diff --git a/src/Type/Family/Constraint.hs b/src/Type/Family/Constraint.hs
--- a/src/Type/Family/Constraint.hs
+++ b/src/Type/Family/Constraint.hs
@@ -1,9 +1,9 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
@@ -43,4 +43,7 @@
   type IffC True  t f = t
 instance f => Iff False t f where
   type IffC False t f = f
+
+class d (c a) => Comp (d :: l -> Constraint) (c :: k -> l) (a :: k)
+instance d (c a) => Comp d c a
 
diff --git a/src/Type/Family/Either.hs b/src/Type/Family/Either.hs
--- a/src/Type/Family/Either.hs
+++ b/src/Type/Family/Either.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
diff --git a/src/Type/Family/List.hs b/src/Type/Family/List.hs
--- a/src/Type/Family/List.hs
+++ b/src/Type/Family/List.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -74,7 +75,7 @@
 
 -- | Type-level list snoc.
 type family (as :: [k]) >: (a :: k) :: [k] where
-  Ø         >: a = Only a
+  Ø         >: a = a :< Ø
   (b :< as) >: a = b :< (as >: a)
 infixl 6 >:
 
@@ -139,7 +140,7 @@
 -- | Takes a type-level list of 'Constraint's to a single
 -- 'Constraint', where @ListC cs@ holds iff all elements
 -- of @cs@ hold.
-type family ListC (cs :: [Constraint]) :: Constraint where
+type family ListC (cs :: [Constraint]) = (c :: Constraint) | c -> cs where
   ListC  Ø        = ØC
   ListC (c :< cs) = (c, ListC cs)
 
@@ -179,7 +180,7 @@
   Snds  Ø        = Ø
   Snds (p :< ps) = Snd p :< Snds ps
 
-type family Zip (as :: [k]) (bs :: [l]) :: [(k,l)] where
+type family Zip (as :: [k]) (bs :: [l]) = (cs :: [(k,l)]) | cs -> as bs where
   Zip  Ø         Ø        = Ø
   Zip (a :< as) (b :< bs) = a#b :< Zip as bs
 
diff --git a/src/Type/Family/Maybe.hs b/src/Type/Family/Maybe.hs
--- a/src/Type/Family/Maybe.hs
+++ b/src/Type/Family/Maybe.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
diff --git a/src/Type/Family/Nat.hs b/src/Type/Family/Nat.hs
--- a/src/Type/Family/Nat.hs
+++ b/src/Type/Family/Nat.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -63,7 +64,7 @@
   NatEq (S x) (S y) = NatEq x y
 type instance x == y = NatEq x y
 
-type family Iota (x :: N) :: [N] where
+type family Iota (x :: N) = (xs :: [N]) | xs -> x where
   Iota Z     = Ø
   Iota (S x) = x :< Iota x
 
@@ -73,6 +74,8 @@
 type family Pred (x :: N) :: N where
   Pred (S n) = n
 
+type Pos n = (n ~ S (Pred n))
+
 predCong :: (x ~ y) :- (Pred x ~ Pred y)
 predCong = Sub Wit
 
@@ -81,6 +84,11 @@
   S x + y = S (x + y)
 infixr 6 +
 
+data AddW (f :: N -> *) :: N -> * where
+  AddW :: !(f x)
+       -> !(f y)
+       -> AddW f (x + y)
+
 addCong :: (w ~ y,x ~ z) :- ((w + x) ~ (y + z))
 addCong = Sub Wit
 
@@ -88,6 +96,11 @@
   Z   * y = Z
   S x * y = (x * y) + y
 infixr 7 *
+
+data MulW (f :: N -> *) :: N -> * where
+  MulW :: !(f x)
+       -> !(f y)
+       -> MulW f (x * y)
 
 mulCong :: (w ~ y,x ~ z) :- ((w * x) ~ (y * z))
 mulCong = Sub Wit
diff --git a/src/Type/Family/Symbol.hs b/src/Type/Family/Symbol.hs
deleted file mode 100644
--- a/src/Type/Family/Symbol.hs
+++ /dev/null
@@ -1,7 +0,0 @@
-
-module Type.Family.Symbol
-  ( module GHC.TypeLits
-  ) where
-
-import GHC.TypeLits (Symbol,KnownSymbol,sameSymbol,symbolVal)
-
diff --git a/type-combinators.cabal b/type-combinators.cabal
--- a/type-combinators.cabal
+++ b/type-combinators.cabal
@@ -1,5 +1,5 @@
 name: type-combinators
-version: 0.2.2.1
+version: 0.2.4.0
 category: Data
 synopsis: A collection of data types for type-level programming
 cabal-version: >=1.10
@@ -17,9 +17,11 @@
 
 library
     exposed-modules:
+        -- Data.Type.Polynomial
         Data.Type.Boolean
         Data.Type.Combinator
         Data.Type.Conjunction
+        Data.Type.Difference
         Data.Type.Disjunction
         Data.Type.Fin
         Data.Type.Fin.Indexed
@@ -32,10 +34,12 @@
         Data.Type.Product
         Data.Type.Product.Env
         Data.Type.Product.Lifted
+        Data.Type.Remove
+        Data.Type.Subset
         Data.Type.Sum
         Data.Type.Sum.Lifted
-        Data.Type.Sym
-        Data.Type.Quantifier
+        -- Data.Type.Sym
+        -- Data.Type.Quantifier
         Data.Type.Vector
         Type.Class.Higher
         Type.Class.Known
@@ -47,10 +51,10 @@
         Type.Family.Maybe
         Type.Family.Monoid
         Type.Family.Nat
-        Type.Family.Symbol
+        -- Type.Family.Symbol
         Type.Family.Tuple
     build-depends:
-        base >=4.8 && <4.9
+        base >=4.9 && <5.0
     default-language: Haskell2010
     hs-source-dirs: src
     ghc-options: -Wall -fno-warn-unticked-promoted-constructors