diff --git a/quantification.cabal b/quantification.cabal
--- a/quantification.cabal
+++ b/quantification.cabal
@@ -1,5 +1,5 @@
 name: quantification
-version: 0.3
+version: 0.4
 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
@@ -23,7 +23,7 @@
       base >= 4.9 && < 5
     , ghc-prim >= 0.5 && < 0.6
     , hashable >= 1.2 && < 1.3
-    , aeson >= 0.11 && < 1.3
+    , aeson >= 1.0 && < 1.5
     , text >= 1.0 && < 2.0
     , path-pieces >= 0.2 && < 0.3
     , vector >= 0.11 && < 0.13
diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs
--- a/src/Data/Exists.hs
+++ b/src/Data/Exists.hs
@@ -1,18 +1,18 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE MagicHash #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeInType #-}
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeOperators #-}
 
 {-# OPTIONS_GHC -Wall #-}
 
@@ -29,12 +29,18 @@
   , Exists2(..)
   , Exists3(..)
   , Some(..)
+  , DependentPair(..)
+  , WitnessedEquality(..)
+  , WitnessedOrdering(..)
     -- * Type Classes
   , EqForall(..)
   , EqForallPoly(..)
+  , EqForeach(..)
   , OrdForall(..)
   , OrdForallPoly(..)
+  , OrdForeach(..)
   , ShowForall(..)
+  , ShowForeach(..)
   , ReadForall(..)
   , EnumForall(..)
   , BoundedForall(..)
@@ -45,13 +51,11 @@
   , FromJSONForall(..)
   , FromJSONExists(..)
   , ToJSONForall(..)
-#if MIN_VERSION_aeson(1,0,0) 
   , ToJSONKeyFunctionForall(..)
   , FromJSONKeyFunctionForall(..)
   , ToJSONKeyForall(..)
   , FromJSONKeyExists(..)
   , FromJSONKeyForall(..)
-#endif
   , StorableForall(..)
     -- * Higher Rank Classes
   , EqForall2(..)
@@ -77,9 +81,10 @@
     -- ** Defaulting
   , defaultEqForallPoly
   , defaultCompareForallPoly
-#if MIN_VERSION_aeson(1,0,0) 
   , parseJSONMapForallKey
-#endif
+    -- ** Weakening
+  , weakenEquality
+  , weakenOrdering
     -- ** Other
   , unreifyList
   ) where
@@ -108,52 +113,69 @@
 import qualified Text.Read as R
 import qualified Web.PathPieces as PP
 
-#if MIN_VERSION_aeson(1,0,0) 
 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 -> Type) = forall a. Exists !(f a)
 
+-- | Hide two type parameters.
 data Exists2 (f :: k -> j -> Type) = forall a b. Exists2 !(f a b)
 
+-- | Hide three type parameters.
 data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c)
 
-#if MIN_VERSION_aeson(1,0,0) 
+data DependentPair (f :: k -> Type) (g :: k -> Type) =
+  forall a. DependentPair (f a) (g a)
+
+data WitnessedEquality (a :: k) (b :: k) where
+  WitnessedEqualityEqual :: WitnessedEquality a a
+  WitnessedEqualityUnequal :: WitnessedEquality a b
+
+data WitnessedOrdering (a :: k) (b :: k) where
+  WitnessedOrderingLT :: WitnessedOrdering a b
+  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 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
   eqForall :: f a -> f a -> Bool
 
+-- | Variant of 'EqForall' that requires a pi-quantified type.
+class EqForeach f where
+  eqForeach :: Sing a -> f a -> f a -> Bool
+
 class EqForall f => OrdForall f where
   compareForall :: f a -> f a -> Ordering
 
 class EqForall f => EqForallPoly f where
-  eqForallPoly :: f a -> f b -> Bool
-  default eqForallPoly :: TestEquality f => f a -> f b -> Bool
+  eqForallPoly :: f a -> f b -> WitnessedEquality a b
+  default eqForallPoly :: TestEquality f => f a -> f b -> WitnessedEquality a b
   eqForallPoly = defaultEqForallPoly
 
 -- the default method does not work if your data type is a newtype wrapper
 -- over a function, but that should not really ever happen.
 class (OrdForall f, EqForallPoly f) => OrdForallPoly f where
-  compareForallPoly :: f a -> f b -> Ordering
-  default compareForallPoly :: TestEquality f => f a -> f b -> Ordering
-  compareForallPoly = defaultCompareForallPoly
+  compareForallPoly :: f a -> f b -> WitnessedOrdering a b
 
+-- | Variant of 'OrdForall' that requires a pi-quantified type.
+class EqForeach f => OrdForeach f where
+  compareForeach :: Sing a -> f a -> f a -> Ordering
+
 class ShowForall f where
   showsPrecForall :: Int -> f a -> ShowS
 
+class ShowForeach f where
+  showsPrecForeach :: Sing a -> Int -> f a -> ShowS
+
 class ShowForall2 f where
   showsPrecForall2 :: Int -> f a b -> ShowS
 
@@ -181,7 +203,6 @@
 class HashableForall f where
   hashWithSaltForall :: Int -> f a -> Int
 
-#if MIN_VERSION_aeson(1,0,0) 
 class ToJSONKeyForall f where
   toJSONKeyForall :: ToJSONKeyFunctionForall f
 
@@ -190,7 +211,6 @@
 
 class FromJSONKeyForall f where
   fromJSONKeyForall :: FromJSONKeyFunctionForall f
-#endif
 
 class ToJSONForall f where
   toJSONForall :: f a -> Aeson.Value
@@ -252,20 +272,13 @@
 instance Eq a => EqForall (Const a) where
   eqForall (Const x) (Const y) = x == y
 
-instance Eq a => EqForallPoly (Const a) where
-  eqForallPoly (Const x) (Const y) = x == y
-
 instance Ord a => OrdForall (Const a) where
   compareForall (Const x) (Const y) = compare x y
 
-instance Ord a => OrdForallPoly (Const a) where
-  compareForallPoly (Const x) (Const y) = compare x y
-
 instance Hashable a => HashableForall (Const a) where
   hashWithSaltForall s (Const a) = hashWithSalt s a
 
 
-#if MIN_VERSION_aeson(1,0,0) 
 -- I need to get rid of the ToJSONForall and FromJSONForall constraints
 -- on these two instances.
 instance (ToJSONKeyForall f, ToJSONForall f) => ToJSONKey (Exists f) where
@@ -275,16 +288,15 @@
 
 instance (FromJSONKeyExists f, FromJSONExists f) => FromJSONKey (Exists f) where
   fromJSONKey = fromJSONKeyExists
-#endif
 
 instance EqForallPoly f => Eq (Exists f) where
-  Exists a == Exists b = eqForallPoly a b
+  Exists a == Exists b = weakenEquality (eqForallPoly a b)
 
 instance EqForallPoly2 f => Eq (Exists2 f) where
   Exists2 a == Exists2 b = eqForallPoly2 a b
 
 instance OrdForallPoly f => Ord (Exists f) where
-  compare (Exists a) (Exists b) = compareForallPoly a b
+  compare (Exists a) (Exists b) = weakenOrdering (compareForallPoly a b)
 
 instance HashableForall f => Hashable (Exists f) where
   hashWithSalt s (Exists a) = hashWithSaltForall s a
@@ -326,13 +338,18 @@
   eqForall (Pair f1 g1) (Pair f2 g2) = eqForall f1 f2 && eqForall g1 g2
 
 instance (EqForallPoly f, EqForallPoly g) => EqForallPoly (Product f g) where
-  eqForallPoly (Pair f1 g1) (Pair f2 g2) = eqForallPoly f1 f2 && eqForallPoly g1 g2
+  eqForallPoly (Pair f1 g1) (Pair f2 g2) = case eqForallPoly f1 f2 of
+    WitnessedEqualityEqual -> eqForallPoly g1 g2
+    WitnessedEqualityUnequal -> WitnessedEqualityUnequal
 
 instance (OrdForall f, OrdForall g) => OrdForall (Product f g) where
   compareForall (Pair f1 g1) (Pair f2 g2) = mappend (compareForall f1 f2) (compareForall g1 g2)
 
 instance (OrdForallPoly f, OrdForallPoly g) => OrdForallPoly (Product f g) where
-  compareForallPoly (Pair f1 g1) (Pair f2 g2) = mappend (compareForallPoly f1 f2) (compareForallPoly g1 g2)
+  compareForallPoly (Pair f1 g1) (Pair f2 g2) = case compareForallPoly f1 f2 of
+    WitnessedOrderingLT -> WitnessedOrderingLT
+    WitnessedOrderingGT -> WitnessedOrderingGT
+    WitnessedOrderingEQ -> compareForallPoly g1 g2
 
 instance (ShowForall f, ShowForall g) => ShowForall (Product f g) where
   showsPrecForall p (Pair f g) = showParen 
@@ -350,9 +367,6 @@
 instance (Eq1 f, EqForall g) => EqForall (Compose f g) where
   eqForall (Compose x) (Compose y) = liftEq eqForall x y
 
-instance (Eq1 f, EqForallPoly g) => EqForallPoly (Compose f g) where
-  eqForallPoly (Compose x) (Compose y) = liftEq eqForallPoly x y
-
 instance (Show1 f, ShowForall g) => ShowForall (Compose f g) where
   showsPrecForall _ (Compose x) = showString "Compose " . liftShowsPrec showsPrecForall showListForall 11 x
 
@@ -385,10 +399,10 @@
   Nothing -> compare (getTagBox a) (getTagBox b)
   Just Refl -> compareForall a b
 
-defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> Bool
+defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> WitnessedEquality a b
 defaultEqForallPoly x y = case testEquality x y of
-  Nothing -> False
-  Just Refl -> eqForall x y
+  Nothing -> WitnessedEqualityUnequal
+  Just Refl -> if eqForall x y then WitnessedEqualityEqual else WitnessedEqualityUnequal
 
 getTagBox :: a -> Int
 getTagBox !x = I# (dataToTag# x)
@@ -492,7 +506,6 @@
 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)
@@ -533,6 +546,33 @@
 -- 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
+
+weakenEquality :: WitnessedEquality a b -> Bool
+weakenEquality = \case
+  WitnessedEqualityEqual -> True
+  WitnessedEqualityUnequal -> False
+
+weakenOrdering :: WitnessedOrdering a b -> Ordering
+weakenOrdering = \case
+  WitnessedOrderingGT -> GT
+  WitnessedOrderingEQ -> EQ
+  WitnessedOrderingLT -> LT
+
+instance (EqForallPoly f, ToSing f, EqForeach g) => Eq (DependentPair f g) where
+  DependentPair a1 b1 == DependentPair a2 b2 = case eqForallPoly a1 a2 of
+    WitnessedEqualityUnequal -> False
+    WitnessedEqualityEqual -> eqForeach (toSing a1) b1 b2
+
+instance (OrdForallPoly f, ToSing f, OrdForeach g) => Ord (DependentPair f g) where
+  compare (DependentPair a1 b1) (DependentPair a2 b2) = case compareForallPoly a1 a2 of
+    WitnessedOrderingLT -> LT
+    WitnessedOrderingGT -> GT
+    WitnessedOrderingEQ -> compareForeach (toSing a1) b1 b2
+
+instance (ShowForall f, ToSing f, ShowForeach g) => Show (DependentPair f g) where
+  showsPrec p (DependentPair a b) s = showParen 
+    (p >= 11) 
+    (showString "DependentPair " . showsPrecForall 11 a . showChar ' ' . showsPrecForeach (toSing a) 11 b)
+    s
 
 
diff --git a/src/Topaz/Types.hs b/src/Topaz/Types.hs
--- a/src/Topaz/Types.hs
+++ b/src/Topaz/Types.hs
@@ -21,6 +21,9 @@
   , Nest(..)
   , EqHetero(..)
   , TestEqualityHetero(..)
+  , Nat(..)
+  , SingNat(..)
+  , Vector(..)
   , type (++)
   ) where
 
@@ -39,6 +42,22 @@
 import qualified Data.Aeson as AE
 import qualified Data.Aeson.Types as AET
 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