diff --git a/ChangeLog.md b/ChangeLog.md
deleted file mode 100644
--- a/ChangeLog.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# Revision history for argdict
-
-## 0.1.0.0  -- YYYY-mm-dd
-
-* First version. Released on an unsuspecting world.
diff --git a/constraints-extras.cabal b/constraints-extras.cabal
--- a/constraints-extras.cabal
+++ b/constraints-extras.cabal
@@ -1,5 +1,5 @@
 name: constraints-extras
-version: 0.2.0.0
+version: 0.2.1.0
 synopsis: Utility package for constraints
 license: BSD3
 license-file: LICENSE
@@ -7,7 +7,6 @@
 maintainer: maintainer@obsidian.systems
 copyright: Obsidian Systems LLC
 build-type: Simple
-extra-source-files: ChangeLog.md
 cabal-version: >=1.10
 
 library
diff --git a/src/Data/Constraint/Extras.hs b/src/Data/Constraint/Extras.hs
--- a/src/Data/Constraint/Extras.hs
+++ b/src/Data/Constraint/Extras.hs
@@ -13,15 +13,29 @@
 import Data.Constraint
 import Data.Constraint.Forall
 
--- | Provides proof of the existence of a constraint on a GADT
+-- | Morally, this class is for GADTs whose indices can be finitely enumerated. It provides operations which will
+-- select the appropriate type class dictionary from among a list of contenders based on a value of the type.
+-- There are a few different variations of this which we'd like to be able to support, and they're all implemented
+-- in the same fashion at the term level, by pattern matching on the constructors of the GADT, and producing Dict
+-- as the result.
+-- It would be nice to have some way to stop the proliferation of these variants and unify the existing ones, but
+-- at the moment, it appears to require honest type level functions. (Closed type families which must be fully
+-- applied didn't quite cut it when I tried). Some symbolic type-level application could do the trick, but I didn't
+-- want to go quite that far at the time of writing.
 class ArgDict f where
   type ConstraintsFor f (c :: k -> Constraint) :: Constraint
   type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) :: Constraint
   argDict :: ConstraintsFor f c => f a -> Dict (c a)
   argDict' :: ConstraintsFor' f c g => f a -> Dict (c (g a))
 
+-- | This places a tighter restriction on the kind of f, and so needs to be a separate class.
+class ArgDictV f where
+  type ConstraintsForV (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k) :: Constraint
+  argDictV :: ConstraintsForV f c g => f v -> Dict (c (v g))
+
 type Has (c :: k -> Constraint) f = (ArgDict f, ConstraintsFor f c)
 type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict f, ConstraintsFor' f c g)
+type HasV c f g = (ArgDictV f, ConstraintsForV f c g)
 
 has :: forall c f a r. (Has c f) => f a -> (c a => r) -> r
 has k r | (Dict :: Dict (c a)) <- argDict k = r
@@ -29,9 +43,13 @@
 has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r
 has' k r | (Dict :: Dict (c (g a))) <- argDict' k = r
 
+hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> r
+hasV k r | (Dict :: Dict (c (v g))) <- argDictV k = r
+
 whichever :: forall c t a r. (ForallF c t) => (c (t a) => r) -> r
 whichever r = r \\ (instF :: ForallF c t :- c (t a))
 
 -- | Allows explicit specification of constraint implication
 class Implies1 c d where
   implies1 :: c a :- d a
+
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
@@ -1,7 +1,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE TemplateHaskell #-}
-module Data.Constraint.Extras.TH where
+module Data.Constraint.Extras.TH (deriveArgDict, deriveArgDictV, gadtIndices) where
 
 import Data.Constraint.Extras
 import Control.Monad
@@ -11,7 +11,7 @@
 
 deriveArgDict :: Name -> Q [Dec]
 deriveArgDict n = do
-  ts <- gadtResults n
+  ts <- gadtIndices n
   c <- newName "c"
   g <- newName "g"
   let xs = map (AppT (VarT c)) ts
@@ -19,35 +19,56 @@
       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')
-        argDict = $(LamCaseE <$> matches 'argDict)
-        argDict' = $(LamCaseE <$> matches 'argDict')
+        argDict = $(LamCaseE <$> matches n 'argDict)
+        argDict' = $(LamCaseE <$> matches n 'argDict')
     |]
-  where
-    matches :: Name -> Q [Match]
-    matches argDictName = do
-      x <- newName "x"
-      reify n >>= \case
-        TyConI (DataD _ _ _ _ cons _) -> pure $ concat $ flip map cons $ \case
-          GadtC [name] _ (AppT (ConT _) (VarT _)) ->
-            [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
-          GadtC [name] _ _ ->
-            [Match (RecP name []) (NormalB $ ConE 'Dict) []]
-          ForallC _ _ (GadtC [name] _ (AppT (ConT _) (VarT _))) ->
-            [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
-          ForallC _ _ (GadtC [name] _ _) ->
-            [Match (RecP name []) (NormalB $ ConE 'Dict) []]
-          NormalC name [(_, AppT (ConT _) (VarT _))] ->
-            [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
-          a -> error $ "deriveArgDict matches: Unmatched 'Dec': " <> show a
-        a -> error $ "deriveArgDict matches: Unmatched 'Info': " <> show a
 
-gadtResults :: Name -> Q [Type]
-gadtResults n = do
+deriveArgDictV :: Name -> Q [Dec]
+deriveArgDictV n = do
+  vs <- gadtIndices n
+  c <- newName "c"
+  g <- newName "g"
+  let xs = map (\v -> AppT (VarT c) $ AppT v (VarT g)) vs
+      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)
+             argDictV = $(LamCaseE <$> matches n 'argDictV)
+       |]
+  return (d ++ ds)
+
+matches :: Name -> Name -> Q [Match]
+matches n argDictName = do
+  x <- newName "x"
+  reify n >>= \case
+    TyConI (DataD _ _ _ _ cons _) -> pure $ concat $ flip map cons $ \case
+      GadtC [name] _ (AppT (ConT _) (VarT _)) ->
+        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
+      GadtC [name] _ _ ->
+        [Match (RecP name []) (NormalB $ ConE 'Dict) []]
+      ForallC _ _ (GadtC [name] _ (AppT (ConT _) (VarT _))) ->
+        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
+      ForallC _ _ (GadtC [name] _ _) ->
+        [Match (RecP name []) (NormalB $ ConE 'Dict) []]
+      NormalC name [(_, AppT (ConT _) (VarT _))] ->
+        [Match (ConP name [VarP x]) (NormalB $ AppE (VarE argDictName) (VarE x)) []]
+      a -> error $ "deriveArgDict matches: Unmatched 'Dec': " <> show a
+    a -> error $ "deriveArgDict matches: Unmatched 'Info': " <> show a
+
+gadtIndices :: Name -> Q [Type]
+gadtIndices n = do
   reify n >>= \case
     TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \case
       GadtC _ _ (AppT (ConT _) (VarT _)) -> return []