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.1.0.1
+version: 0.2.0.0
 synopsis: Utility package for constraints
 license: BSD3
 license-file: LICENSE
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
@@ -2,17 +2,35 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 module Data.Constraint.Extras where
 
 import Data.Constraint
+import Data.Constraint.Forall
 
 -- | Provides proof of the existence of a constraint on a GADT
 class ArgDict f where
-  type ConstraintsFor (c :: * -> Constraint) f :: Constraint
-  argDict :: ConstraintsFor c f => f a -> Dict (c a)
+  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))
 
-type Has c f = (ArgDict f, ConstraintsFor c f)
+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)
+
+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
+
+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
+
+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
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
@@ -13,40 +13,46 @@
 deriveArgDict n = do
   ts <- gadtResults n
   c <- newName "c"
+  g <- newName "g"
   let xs = map (AppT (VarT c)) ts
+      xs' = map (AppT (VarT c) . AppT (VarT g)) ts
       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 $(varT c) $(pure $ ConT n) = $(pure constraints)
-        argDict = $(LamCaseE <$> matches)
+        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')
     |]
   where
-    matches :: Q [Match]
-    matches = do
+    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 'argDict) (VarE x)) []]
+            [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 'argDict) (VarE x)) []]
+            [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 'argDict) (VarE x)) []]
+            [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 = reify n >>= \case
-  TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \case
-    GadtC _ _ (AppT (ConT _) (VarT _)) -> return []
-    GadtC _ _ (AppT _ (AppT (ConT _) (VarT _))) -> return []
-    GadtC _ _ (AppT _ typ) -> return [typ]
-    ForallC _ _ (GadtC _ _ (AppT (ConT _) (VarT _))) -> return []
-    ForallC _ _ (GadtC _ _ (AppT _ (AppT (ConT _) (VarT _)))) -> return []
-    ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [typ]
-    _ -> return []
-  a -> error $ "gadtResults: Unmatched 'Info': " <> show a
+gadtResults n = do
+  reify n >>= \case
+    TyConI (DataD _ _ _ _ cons _) -> fmap concat $ forM cons $ \case
+      GadtC _ _ (AppT (ConT _) (VarT _)) -> return []
+      GadtC _ _ (AppT _ typ) -> return [typ]
+      ForallC _ _ (GadtC _ _ (AppT (ConT _) (VarT _))) -> return []
+      ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [typ]
+      _ -> return []
+    a -> error $ "gadtResults: Unmatched 'Info': " <> show a