diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,14 @@
 # Revision history for constraints-extras
 
+## 0.3.1.0
+
+* Allow deriving instances with `deriveArgDict` for data and newtype family instances by supplying the name of one of its constructors
+* Support GHC 9.0.1
+
+## 0.3.0.3 - 2020-06-22
+
+* Update version bounds for GHC 8.10
+
 ## 0.3.0.2 - 2019-09-30
 
 * Update version bounds for GHC 8.8
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.0.2
+version: 0.3.1.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
@@ -13,7 +13,7 @@
 build-type: Simple
 cabal-version: 2.0
 tested-with:
-  GHC  ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1
+  GHC  ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1 || ==8.10.1 || ==9.0.1
 extra-source-files: README.md
                     ChangeLog.md
 
@@ -24,7 +24,7 @@
   exposed-modules: Data.Constraint.Extras
                  , Data.Constraint.Extras.TH
                  , Data.Constraint.Compose
-  other-modules: Data.Constraint.Flip
+                 , Data.Constraint.Flip
   other-extensions: LambdaCase
                   , MultiParamTypeClasses
                   , QuasiQuotes
@@ -32,18 +32,18 @@
                   , TypeOperators
                   , ConstraintKinds
                   , TemplateHaskell
-  build-depends: base >=4.9 && <4.14
-               , constraints >= 0.9 && < 0.12
-               , template-haskell >=2.11 && <2.16
+  build-depends: base >=4.9 && <4.16
+               , constraints >= 0.9 && < 0.13
+               , template-haskell >=2.11 && <2.18
   hs-source-dirs:  src
   default-language: Haskell2010
 
 executable readme
   if !flag(build-readme)
     buildable: False
-  build-depends: base >=4.9 && <4.14
+  build-depends: base
                , aeson
-               , constraints >= 0.9 && < 0.12
+               , constraints
                , constraints-extras
   main-is: README.lhs
   ghc-options: -Wall -optL -q
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
@@ -11,34 +11,86 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 
-module Data.Constraint.Extras where
+-- | Throughout this module, we use the following GADT and @ArgDict@ instance
+-- in our examples:
+--
+-- > {-# LANGUAGE StandaloneDeriving #-}
+-- >
+-- > data Tag a where
+-- >   I :: Tag Int
+-- >   B :: Tag Bool
+-- > deriving instance Show (Tag a)
+-- >
+-- > $(deriveArgDict ''Tag)
+--
+-- The constructors of @Tag@ mean that a type variable @a@ in @Tag a@
+-- 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'
+  , argDict'
+  , ConstraintsForV
+  , argDictV
+    -- * Bringing instances into scope
+  , Has
+  , has
+  , Has'
+  , has'
+  , HasV
+  , hasV
+  , whichever
+    -- * Misc
+  , Implies1(..)
+    -- * Deprecated
+  , ArgDictV
+  ) where
 
 import Data.Constraint
 import Data.Constraint.Compose
 import Data.Constraint.Flip
 import Data.Constraint.Forall
+import Data.Kind
 
--- | 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.
+-- | 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@.
+  --
+  -- > ConstraintsFor Show Tag = (Show Int, Show Bool)
+  type ConstraintsFor f c :: Constraint
 
-class ArgDict (c :: k -> Constraint) (f :: k -> *) where
-  type ConstraintsFor f (c :: k -> Constraint) :: Constraint
+  -- | Use an @f a@ to select a specific dictionary from @ConstraintsFor f c@.
+  --
+  -- > argDict I :: Dict (Show Int)
   argDict :: ConstraintsFor f c => f a -> Dict (c a)
 
+-- | \"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') -> *) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)
+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
@@ -47,23 +99,59 @@
 {-# DEPRECATED ArgDictV "Just use 'ArgDict'" #-}
 type ArgDictV f c = ArgDict f c
 
+-- | @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)
+
+-- | @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)@.
+--
+-- > 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)
 
-has :: forall c f a r. (Has c f) => f a -> (c a => r) -> r
+-- | 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
 
-has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r
+-- | Like 'has', but we get a @c (g a)@ instance brought into scope
+-- instead. Use @-XTypeApplications@ to specify @c@ and @g@.
+--
+-- > -- From dependent-sum:Data.Dependent.Sum
+-- > data DSum tag f = forall a. !(tag a) :=> f a
+-- >
+-- > -- 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
 
-hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> 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
+-- | 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
+-- specify @c@, @t@ and @a@.
+--
+-- > -- Show the tag of a dependent sum, even though we don't know the tag type.
+-- > showDSumKey :: forall tag f . ForallF Show tag => DSum tag f -> String
+-- > showDSumKey ((tag :: tag a) :=> fa) = whichever @Show @tag @a $ show tag
+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
+-- | 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
@@ -12,54 +12,50 @@
 
 deriveArgDict :: Name -> Q [Dec]
 deriveArgDict n = do
+  (typeHead, constrs) <- getDeclInfo n
   c <- newName "c"
-  ts <- gadtIndices c n
+  ts <- gadtIndices c constrs
   let xs = flip map ts $ \case
         Left t -> AppT (AppT (ConT ''ConstraintsFor) t) (VarT c)
         Right t -> (AppT (VarT c) t)
       l = length xs
       constraints = foldl AppT (TupleT l) xs
-  arity <- tyConArity n
-  tyVars <- replicateM (arity - 1) (newName "a")
-  let n' = foldr (\v x -> AppT x (VarT v)) (ConT n) tyVars
-  [d| instance ArgDict $(varT c) $(pure n') where
-        type ConstraintsFor  $(pure n') $(varT c) = $(pure constraints)
-        argDict = $(LamCaseE <$> matches c n 'argDict)
+  [d| instance ArgDict $(varT c) $(pure typeHead) where
+        type ConstraintsFor  $(pure typeHead) $(varT c) = $(pure constraints)
+        argDict = $(LamCaseE <$> matches c constrs 'argDict)
     |]
 
 {-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-}
 deriveArgDictV :: Name -> Q [Dec]
 deriveArgDictV = deriveArgDict
 
-matches :: Name -> Name -> Name -> Q [Match]
-matches c n argDictName = do
+matches :: Name -> [Con] -> Name -> Q [Match]
+matches c constrs argDictName = do
   x <- newName "x"
-  reify n >>= \case
-    TyConI (DataD _ _ _ _ constrs _) -> 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]
-            return $ if hasArgDictInstance
-              then Just x
-              else Nothing
-          _ -> return Nothing
-        return $ case catMaybes ps of
-          [] -> [Match (RecP name []) (NormalB $ ConE 'Dict) []]
-          (v:_) ->
-            let patf = \v' rest done -> if done
-                  then WildP : rest done
-                  else case v' of
-                    Nothing -> WildP : rest done
-                    Just _ -> VarP v : rest True
-                pat = foldr patf (const []) ps False
-            in [Match (ConP name pat) (NormalB $ AppE (VarE argDictName) (VarE v)) []]
-      ForallC _ _ (GadtC [name] _ _) -> return $
-        [Match (RecP name []) (NormalB $ ConE 'Dict) []]
-      a -> error $ "deriveArgDict matches: Unmatched 'Dec': " ++ show a
-    a -> error $ "deriveArgDict matches: Unmatched 'Info': " ++ show a
+  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]
+          return $ if hasArgDictInstance
+            then Just x
+            else Nothing
+        _ -> return Nothing
+      return $ case catMaybes ps of
+        [] -> [Match (RecP name []) (NormalB $ ConE 'Dict) []]
+        (v:_) ->
+          let patf = \v' rest done -> if done
+                then WildP : rest done
+                else case v' of
+                  Nothing -> WildP : rest done
+                  Just _ -> VarP v : rest True
+              pat = foldr patf (const []) ps False
+          in [Match (ConP name pat) (NormalB $ AppE (VarE argDictName) (VarE v)) []]
+    ForallC _ _ (GadtC [name] _ _) -> return $
+      [Match (RecP name []) (NormalB $ ConE 'Dict) []]
+    a -> error $ "deriveArgDict matches: Unmatched 'Dec': " ++ show a
 
 kindArity :: Kind -> Int
 kindArity = \case
@@ -69,20 +65,44 @@
   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
+getDeclInfo :: Name -> Q (Type, [Con])
+getDeclInfo n = reify n >>= \case
+  TyConI (DataD _ _ ts mk constrs _) -> do
+    let arity = fromMaybe 0 (fmap kindArity mk) + length ts
+    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
+      FamilyI _ instances -> do
+        let instCons :: InstanceDec -> [Con]
+            instCons = \case
+              DataInstD _ _ _ _ cons _ -> cons
+              NewtypeInstD _ _ _ _ con _ -> [con]
+              _ -> error $ "getDeclInfo: Expected a data or newtype family instance"
+            conNames :: Con -> [Name]
+            conNames = \case
+              NormalC other _ -> [other]
+              RecC other _ -> [other]
+              InfixC _ other _ -> [other]
+              ForallC _ _ con -> conNames con
+              GadtC others _ _ -> others
+              RecGadtC others _ _ -> others
+            instHasThisConstructor i = any (== n) $ conNames =<< instCons i
+        case filter instHasThisConstructor instances of
+          [] -> error $ "getDeclInfo: Couldn't find data family instance for constructor " ++ show n
+          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 -> Name -> Q [Either Type Type]
-gadtIndices c n = reify n >>= \case
-  TyConI (DataD _ _ _ _ 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]
-        return $ if hasArgDictInstance then [Left t] else []
-      _ -> return []
-    ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]
+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]
+      return $ if hasArgDictInstance then [Left t] else []
     _ -> return []
-  a -> error $ "gadtIndices: Unmatched 'Info': " ++ show a
+  ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]
+  _ -> return []