diff --git a/README.lhs b/README.lhs
new file mode 100644
--- /dev/null
+++ b/README.lhs
@@ -0,0 +1,62 @@
+# constraints-extras
+
+## Example usage:
+
+NB: This example can be built with `-pgmL markdown-unlit`.
+
+```haskell
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+import Data.Aeson
+import Data.Constraint.Forall
+import Data.Constraint.Extras
+import Data.Constraint.Extras.TH
+
+data A :: * -> * where
+  A_a :: A Int
+  A_b :: Int -> A ()
+
+data B :: * -> * where
+  B_a :: A a -> A a -> B a
+  B_x :: Int -> B Int
+
+data V :: (* -> *) -> * where
+  V_a :: A Int -> V A
+
+deriveArgDict ''A
+deriveArgDict ''B
+deriveArgDictV ''V
+
+data DSum k f = forall a. DSum (k a) (f a)
+
+-- Derive a ToJSON instance for our 'DSum'
+instance forall k f.
+  ( Has' ToJSON k f -- Given a value of type (k a), we can obtain an instance (ToJSON (f a))
+  , ForallF ToJSON k -- For any (a), we have an instance (ToJSON (k a))
+  ) => ToJSON (DSum k f) where
+  toJSON (DSum (k :: k a) f) = toJSON
+    ( whichever @ToJSON @k @a $ toJSON k -- Use the (ForallF ToJSON k) constraint to obtain the (ToJSON (k a)) instance
+    , has' @ToJSON @f k $ toJSON f -- Use the (Has' ToJSON k f) constraint to obtain the (ToJSON (f a)) instance
+    )
+
+data Some k = forall a. Some (k a)
+
+-- Derive a FromJSON instance for our 'DSum'
+instance (FromJSON (Some f), Has' FromJSON f g) => FromJSON (DSum f g) where
+  parseJSON x = do
+    (jf, jg) <- parseJSON x
+    Some (f :: f a) <- parseJSON jf
+    g <- has' @FromJSON @g f (parseJSON jg)
+    return $ DSum f g
+
+main :: IO ()
+main = return ()
+```
diff --git a/constraints-extras.cabal b/constraints-extras.cabal
--- a/constraints-extras.cabal
+++ b/constraints-extras.cabal
@@ -1,7 +1,8 @@
 name: constraints-extras
-version: 0.2.2.1
+version: 0.2.3.0
 synopsis: Utility package for constraints
 description: Convenience functions and TH for working with constraints. See <https://github.com/obsidiansystems/constraints-extras/blob/develop/README.md README.md> for example usage.
+category: Constraints
 license: BSD3
 license-file: LICENSE
 author: Cale Gibbard, Ali Abrar
@@ -23,7 +24,17 @@
                , constraints >= 0.9 && < 0.11
                , template-haskell >=2.11 && <2.14
   hs-source-dirs:  src
-  default-language:Haskell2010
+  default-language: Haskell2010
+
+executable readme
+  build-depends: base >=4.9 && <4.12
+               , aeson
+               , constraints >= 0.9 && < 0.11
+               , constraints-extras
+               , markdown-unlit
+  main-is: README.lhs
+  ghc-options: -pgmL markdown-unlit -Wall
+  default-language: Haskell2010
 
 source-repository head
   type:     git
diff --git a/src/Data/Constraint/Extras/TH.hs b/src/Data/Constraint/Extras/TH.hs
--- a/src/Data/Constraint/Extras/TH.hs
+++ b/src/Data/Constraint/Extras/TH.hs
@@ -25,13 +25,12 @@
       l = length xs
       constraints = foldl AppT (TupleT l) xs
       constraints' = foldl AppT (TupleT l) xs'
-  {-
-  runIO $ putStrLn "Constraints:"
-  runIO . putStrLn . pprint $ constraints'
-  -}
-  [d| instance ArgDict $(pure $ ConT n) where
-        type ConstraintsFor  $(conT n) $(varT c) = $(pure constraints)
-        type ConstraintsFor' $(conT n) $(varT c) $(varT g) = $(pure constraints')
+  arity <- tyConArity n
+  tyVars <- replicateM (arity - 1) (newName "a")
+  let n' = foldr (\v x -> AppT x (VarT v)) (ConT n) tyVars
+  [d| instance ArgDict $(pure n') where
+        type ConstraintsFor  $(pure n') $(varT c) = $(pure constraints)
+        type ConstraintsFor' $(pure n') $(varT c) $(varT g) = $(pure constraints')
         argDict = $(LamCaseE <$> matches n 'argDict)
         argDict' = $(LamCaseE <$> matches n 'argDict')
     |]
@@ -46,10 +45,6 @@
         Right v -> AppT (VarT c) $ AppT v (VarT g)
       l = length xs
       constraints = foldl AppT (TupleT l) xs
-  {-
-  runIO $ putStrLn "Constraints:"
-  runIO . putStrLn . pprint $ constraints'
-  -}
   ds <- deriveArgDict n
   d <- [d| instance ArgDictV $(pure $ ConT n) where
              type ConstraintsForV $(conT n) $(varT c) $(varT g) = $(pure constraints)
@@ -62,14 +57,12 @@
   x <- newName "x"
   reify n >>= \case
     TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \case
-      GadtC [name] _ (AppT (ConT _) (VarT _)) -> return $
-        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
       GadtC [name] _ _ -> return $
         [Match (RecP name []) (NormalB $ ConE 'Dict) []]
-      ForallC _ _ (GadtC [name] bts (AppT (ConT _) (VarT b))) -> do
+      ForallC _ _ (GadtC [name] bts (AppT _ (VarT b))) -> do
         ps <- forM bts $ \case
-          (_, AppT (ConT a) (VarT b')) | b == b' -> do
-            hasArgDictInstance <- not . null <$> reifyInstances ''ArgDict [(ConT a)]
+          (_, AppT t (VarT b')) | b == b' -> do
+            hasArgDictInstance <- not . null <$> reifyInstances ''ArgDict [t]
             return $ if hasArgDictInstance
               then Just x
               else Nothing
@@ -89,17 +82,28 @@
       a -> error $ "deriveArgDict matches: Unmatched 'Dec': " <> show a
     a -> error $ "deriveArgDict matches: Unmatched 'Info': " <> show a
 
+kindArity :: Kind -> Int
+kindArity = \case
+  ForallT _ _ t -> kindArity t
+  AppT (AppT ArrowT _) t -> 1 + kindArity t
+  SigT t _ -> kindArity t
+  ParensT t -> kindArity t
+  _ -> 0
+
+tyConArity :: Name -> Q Int
+tyConArity n = reify n >>= return . \case
+   TyConI (DataD _ _ ts mk _ _) -> fromMaybe 0 (fmap kindArity mk) + length ts
+   _ -> error $ "tyConArity: Supplied name reified to something other than a data declaration: " <> show n
+
 gadtIndices :: Name -> Q [Either Type Type]
-gadtIndices n = do
-  reify n >>= \case
-    TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \x -> case x of
-      GadtC _ _ (AppT (ConT _) (VarT _)) -> return []
-      GadtC _ _ (AppT _ typ) -> return [Right typ]
-      ForallC _ _ (GadtC _ bts (AppT (ConT _) (VarT _))) -> fmap concat $ forM bts $ \case
-        (_, AppT (ConT a) (VarT _)) -> do
-          hasArgDictInstance <- fmap (not . null) $ reifyInstances ''ArgDict [(ConT a)]
-          return $ if hasArgDictInstance then [Left (ConT a)] else []
-        _ -> return []
-      ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]
+gadtIndices n = reify n >>= \case
+  TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \case
+    GadtC _ _ (AppT _ typ) -> return [Right typ]
+    ForallC _ _ (GadtC _ bts (AppT _ (VarT _))) -> fmap concat $ forM bts $ \case
+      (_, AppT t (VarT _)) -> do
+        hasArgDictInstance <- fmap (not . null) $ reifyInstances ''ArgDict [t]
+        return $ if hasArgDictInstance then [Left t] else []
       _ -> return []
-    a -> error $ "gadtResults: Unmatched 'Info': " <> show a
+    ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]
+    _ -> return []
+  a -> error $ "gadtResults: Unmatched 'Info': " <> show a