diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,11 @@
 # Revision history for constraints-extras
 
+## 0.4.0.0 - 2022-11-18
+
+* Make `Has` from a type synonym into the class upon which everything else is based. Instances may define either `has` or `argDict` which are now both methods of `Has`. This should hopefully improve the readability of type errors involving the library a fair bit, as everything wanted to use `Has`, but it was defined in terms of the less commonly appearing `ArgDict` and `ConstraintsFor`.
+* The `ConstraintsFor` type family has been removed as it is now unnecessary, as instances of `Has` can simply be constrained directly. This has the added benefit of allowing `QuantifiedConstraints` in those instance heads that formerly would not have been allowed as part of the result of a type family.
+* The `ArgDict` class has also been removed, as it was also basically never used on its own.
+
 ## 0.3.2.1 - 2021-12-17
 
 * Support GHC 9.2
diff --git a/README.lhs b/README.lhs
--- a/README.lhs
+++ b/README.lhs
@@ -14,10 +14,12 @@
 > {-# LANGUAGE TypeApplications  #-}
 > {-# LANGUAGE TypeFamilies #-}
 > {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE ConstraintKinds #-}
 > {-# LANGUAGE FlexibleInstances #-}
 > {-# LANGUAGE MultiParamTypeClasses #-}
 > {-# LANGUAGE UndecidableInstances #-}
 > {-# LANGUAGE ExistentialQuantification #-}
+> {-# LANGUAGE TypeFamilies #-}
 >
 > import Data.Aeson
 > import Data.Constraint.Forall
@@ -41,6 +43,14 @@
 >
 > deriveArgDict ''V
 >
+> data family Fam a :: * -> *
+> data instance Fam () :: * -> * where
+>   FI :: Fam () Int
+>   FB :: Fam () Bool
+>
+> deriveArgDict 'FI
+> -- this derives an instance Has c (Fam ()) by looking up the associated data instance.
+>
 > data DSum k f = forall a. DSum (k a) (f a)
 >
 > -- Derive a ToJSON instance for our 'DSum'
@@ -65,4 +75,5 @@
 >
 > main :: IO ()
 > main = return ()
+
 ```
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -14,10 +14,12 @@
 > {-# LANGUAGE TypeApplications  #-}
 > {-# LANGUAGE TypeFamilies #-}
 > {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE ConstraintKinds #-}
 > {-# LANGUAGE FlexibleInstances #-}
 > {-# LANGUAGE MultiParamTypeClasses #-}
 > {-# LANGUAGE UndecidableInstances #-}
 > {-# LANGUAGE ExistentialQuantification #-}
+> {-# LANGUAGE TypeFamilies #-}
 >
 > import Data.Aeson
 > import Data.Constraint.Forall
@@ -41,6 +43,14 @@
 >
 > deriveArgDict ''V
 >
+> data family Fam a :: * -> *
+> data instance Fam () :: * -> * where
+>   FI :: Fam () Int
+>   FB :: Fam () Bool
+>
+> deriveArgDict 'FI
+> -- this derives an instance Has c (Fam ()) by looking up the associated data instance.
+>
 > data DSum k f = forall a. DSum (k a) (f a)
 >
 > -- Derive a ToJSON instance for our 'DSum'
@@ -65,4 +75,5 @@
 >
 > main :: IO ()
 > main = return ()
+
 ```
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.3.2.1
+version: 0.4.0.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
@@ -32,9 +32,9 @@
                   , TypeOperators
                   , ConstraintKinds
                   , TemplateHaskell
-  build-depends: base >=4.9 && <4.17
+  build-depends: base >=4.9 && <4.18
                , constraints >= 0.9 && < 0.14
-               , template-haskell >=2.11 && <2.19
+               , template-haskell >=2.11 && <2.20
   hs-source-dirs:  src
   default-language: Haskell2010
 
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
@@ -7,6 +7,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -28,15 +29,11 @@
 -- must come from the set { @Int@, @Bool@ }. We call this the "set of
 -- types @a@ that could be applied to @Tag@".
 module Data.Constraint.Extras
-  ( -- * The ArgDict typeclass
-    ArgDict(..)
-  , ConstraintsFor'
+  ( -- * The Has typeclass
+    Has(..)
   , argDict'
-  , ConstraintsForV
   , argDictV
     -- * Bringing instances into scope
-  , Has
-  , has
   , Has'
   , has'
   , HasV
@@ -44,8 +41,6 @@
   , whichever
     -- * Misc
   , Implies1(..)
-    -- * Deprecated
-  , ArgDictV
   ) where
 
 import Data.Constraint
@@ -56,93 +51,69 @@
 import Data.Kind
 import GHC.Generics ((:+:)(..))
 
--- | Morally, this class is for GADTs whose indices can be finitely
--- enumerated. An @'ArgDict' c f@ instance allows us to do two things:
---
--- 1. 'ConstraintsFor' requests the set of constraints @c a@ for all
---    possible types @a@ that could be applied to @f@.
---
--- 2. 'argDict' selects a specific @c a@ given a value of type @f a@.
---
--- Use 'Data.Constraint.Extras.TH.deriveArgDict' to derive instances
--- of this class.
-class ArgDict (c :: k -> Constraint) (f :: k -> Type) where
-  -- | Apply @c@ to each possible type @a@ that could appear in a @f a@.
+-- | The constraint @Has c f@ means that given any value of type @f a@, we can determine
+-- that there is an instance of @c a@. For example, @Has Show Tag@ means that given any
+-- @x :: Tag a@, we can conclude @Show a@. Most commonly, the type @f@ will be a GADT,
+-- where we can enumerate all the possible index types through pattern matching, and
+-- discover that there is an appropriate instance in each case. In this sort of
+-- situation, the @c@ can be left entirely polymorphic in the instance for @Has@, and
+-- this is the sort of instance that the provided Template Haskell code writes.
+
+-- It is also sometimes possible to hand-write instances of @Has c f@ for specific
+-- classes @c@ in cases where @f@ is a data type that packs an appropriate dictionary
+-- into its constructors.
+class Has c f where
+  -- | Use the @f a@ to show that there is an instance of @c a@, and
+  -- bring it into scope.
   --
-  -- > ConstraintsFor Show Tag = (Show Int, Show Bool)
-  type ConstraintsFor f c :: Constraint
+  -- The order of type variables is chosen to work
+  -- with @-XTypeApplications@.
+  --
+  -- > -- Hold a value of type a, along with a tag identifying the a.
+  -- > data SomeTagged tag where
+  -- >   SomeTagged :: a -> tag a -> SomeTagged tag
+  -- >
+  -- > -- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we
+  -- > -- have no knowledge of the tag type.
+  -- > showSomeTagged :: Has Show tag => SomeTagged tag -> String
+  -- > showSomeTagged (SomeTagged a tag) = has @Show tag $ show a
+  has :: forall a r. f a -> (c a => r) -> r
+  has x r | Dict <- argDict @c x = r
 
-  -- | Use an @f a@ to select a specific dictionary from @ConstraintsFor f c@.
+  -- | Use an @f a@ to obtain a dictionary for @c a@
   --
-  -- > argDict I :: Dict (Show Int)
-  argDict :: ConstraintsFor f c => f a -> Dict (c a)
+  -- > argDict @Show I :: Dict (Show Int)
+  argDict :: forall a. f a -> Dict (c a)
+  argDict x = has @c x Dict
+  {-# MINIMAL has | argDict #-}
 
 -- | @since 0.3.2.0
-instance (ArgDict c f, ArgDict c g) => ArgDict c (f :+: g) where
-  type ConstraintsFor (f :+: g) c = (ConstraintsFor f c, ConstraintsFor g c)
+instance (Has c f, Has c g) => Has c (f :+: g) where
   argDict = \case
     L1 f -> argDict f
     R1 g -> argDict g
 
 -- | @since 0.3.2.0
-instance (ArgDict c f, ArgDict c g) => ArgDict c (Sum f g) where
-  type ConstraintsFor (Sum f g) c = (ConstraintsFor f c, ConstraintsFor g c)
+instance (Has c f, Has c g) => Has c (Sum f g) where
   argDict = \case
     InL f -> argDict f
     InR g -> argDict g
 
--- | \"Primed\" variants (@ConstraintsFor'@, 'argDict'', 'Has'',
--- 'has'', &c.) use the 'ArgDict' instance on @f@ to apply constraints
--- on @g a@ instead of just @a@. This is often useful when you have
--- data structures parameterised by something of kind @(x -> Type) ->
--- Type@, like in the @dependent-sum@ and @dependent-map@ libraries.
---
--- > ConstraintsFor' Tag Show Identity = (Show (Identity Int), Show (Identity Bool))
-type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)
-
--- | Get a dictionary for a specific @g a@, using a value of type @f a@.
---
--- > argDict' B :: Dict (Show (Identity Bool))
-argDict' :: forall f c g a. (Has' c f g) => f a -> Dict (c (g a))
-argDict' tag = case argDict tag of
-  (Dict :: Dict (ComposeC c g a)) -> Dict
-
-type ConstraintsForV (f :: (k -> k') -> Type) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)
-
-argDictV :: forall f c g v. (HasV c f g) => f v -> Dict (c (v g))
-argDictV tag = case argDict tag of
-  (Dict :: Dict (FlipC (ComposeC c) g a)) -> Dict
-
-{-# DEPRECATED ArgDictV "Just use 'ArgDict'" #-}
-type ArgDictV f c = ArgDict f c
+-- | The constraint @Has' c f g@ means that given a value of type @f a@, we can satisfy the constraint @c (g a)@.
+type Has' (c :: k -> Constraint) f (g :: k' -> k) = Has (ComposeC c g) f
 
--- | @Has c f@ is a constraint which means that for every type @a@
--- that could be applied to @f@, we have @c a@.
---
--- > Has Show Tag = (ArgDict Show Tag, Show Int, Show Bool)
-type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)
+-- | The constraint @HasV c f g@ means that given a value of type @f v@, we can satisfy the constraint @c (v g)@.
+type HasV c f g = Has (FlipC (ComposeC c) g) f
 
--- | @Has' c f g@ is a constraint which means that for every type @a@
--- that could be applied to @f@, we have @c (g a)@.
+-- | Get a dictionary for @c (g a)@, using a value of type @f a@.
 --
--- > Has' Show Tag Identity = (ArgDict (Show . Identity) Tag, Show (Identity Int), Show (Identity Bool))
-type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)
-type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g)
+-- > argDict' @Show @Identity B :: Dict (Show (Identity Bool))
+argDict' :: forall c g f a. (Has' c f g) => f a -> Dict (c (g a))
+argDict' x = has @(ComposeC c g) x Dict
 
--- | Use the @a@ from @f a@ to select a specific @c a@ constraint, and
--- bring it into scope. The order of type variables is chosen to work
--- with @-XTypeApplications@.
---
--- > -- Hold an a, along with a tag identifying the a.
--- > data SomeTagged tag where
--- >   SomeTagged :: a -> tag a -> SomeTagged tag
--- >
--- > -- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we
--- > -- have no knowledge of the tag type.
--- > showSomeTagged :: Has Show tag => SomeTagged tag -> String
--- > showSomeTagged (SomeTagged a tag) = has @Show tag $ show a
-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
+-- | Get a dictionary for @c (v g)@, using a value of type @f v@.
+argDictV :: forall f c g v. (HasV c f g) => f v -> Dict (c (v g))
+argDictV x = has @(FlipC (ComposeC c) g) x Dict
 
 -- | Like 'has', but we get a @c (g a)@ instance brought into scope
 -- instead. Use @-XTypeApplications@ to specify @c@ and @g@.
@@ -153,11 +124,12 @@
 -- > -- Show the value from a dependent sum. (We'll need 'whichever', discussed later, to show the key.)
 -- > showDSumVal :: forall tag f . Has' Show tag f => DSum tag f -> String
 -- > showDSumVal (tag :=> fa) = has' @Show @f tag $ show fa
-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
+has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r
+has' k r = has @(ComposeC c g) 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
+-- | Similar to 'has', but given a value of type @f v@, we get a @c (v g)@ instance brought into scope instead.
+hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> r
+hasV k r = has @(FlipC (ComposeC c) g) k r
 
 -- | Given "forall a. @c (t a)@" (the @ForallF c t@ constraint), select a
 -- specific @a@, and bring @c (t a)@ into scope. Use @-XTypeApplications@ to
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
@@ -16,15 +16,14 @@
   (typeHead, constrs) <- getDeclInfo n
   c <- newName "c"
   ts <- gadtIndices c constrs
-  let xs = flip map ts $ \case
-        Left t -> AppT (AppT (ConT ''ConstraintsFor) t) (VarT c)
+  let constraints = flip map ts $ \case
+        Left t -> AppT (AppT (ConT ''Has) (VarT c)) t
         Right t -> (AppT (VarT c) t)
-      l = length xs
-      constraints = foldl AppT (TupleT l) xs
-  [d| instance ArgDict $(varT c) $(pure typeHead) where
-        type ConstraintsFor  $(pure typeHead) $(varT c) = $(pure constraints)
-        argDict = $(LamCaseE <$> matches c constrs 'argDict)
-    |]
+  ms <- matches c constrs 'argDict
+  return
+    [ InstanceD Nothing constraints (AppT (AppT (ConT ''Has) (VarT c)) typeHead)
+      [ ValD (VarP 'argDict) (NormalB (LamCaseE ms)) [] ]
+    ]
 
 {-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-}
 deriveArgDictV :: Name -> Q [Dec]
@@ -33,13 +32,13 @@
 matches :: Name -> [Con] -> Name -> Q [Match]
 matches c constrs argDictName = do
   x <- newName "x"
-  fmap concat $ forM constrs $ \case
+  fmap concat . forM constrs $ \case
     GadtC [name] _ _ -> return $
       [Match (RecP name []) (NormalB $ ConE 'Dict) []]
     ForallC _ _ (GadtC [name] bts (AppT _ (VarT b))) -> do
       ps <- forM bts $ \case
         (_, AppT t (VarT b')) | b == b' -> do
-          hasArgDictInstance <- not . null <$> reifyInstances ''ArgDict [VarT c, t]
+          hasArgDictInstance <- not . null <$> reifyInstances ''Has [VarT c, t]
           return $ if hasArgDictInstance
             then Just x
             else Nothing
@@ -81,8 +80,11 @@
     tyVars <- replicateM (arity - 1) (newName "a")
     let typeHead = foldr (\v x -> AppT x (VarT v)) (ConT n) tyVars
     return (typeHead, constrs)
-  DataConI _ (ForallT _ _ (AppT typeHead _)) parent -> do
-    reify parent >>= \case
+  DataConI _ (AppT typeHead _) parent -> handleParent typeHead parent
+  DataConI _ (ForallT _ _ (AppT typeHead _)) parent -> handleParent typeHead parent
+  a -> error $ "getDeclInfo: Unmatched 'Info': " ++ show a
+  where
+    handleParent typeHead parent = reify parent >>= \case
       FamilyI _ instances -> do
         let instCons :: InstanceDec -> [Con]
             instCons = \case
@@ -103,14 +105,13 @@
           l@(_:_:_) -> error $ "getDeclInfo: Expected one data family instance for constructor " ++ show n ++ " but found multiple: " ++ show l
           [i] -> return (typeHead, instCons i)
       a -> error $ "getDeclInfo: Unmatched parent of data family instance: " ++ show a
-  a -> error $ "getDeclInfo: Unmatched 'Info': " ++ show a
 
 gadtIndices :: Name -> [Con] -> Q [Either Type Type]
 gadtIndices c constrs = fmap concat $ forM constrs $ \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 [VarT c, t]
+      hasArgDictInstance <- fmap (not . null) $ reifyInstances ''Has [VarT c, t]
       return $ if hasArgDictInstance then [Left t] else []
     _ -> return []
   ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]