diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,13 @@
 # Revision history for dependent-sum-template
 
+## 0.1.2.0 - 2023-07-11
+
+* Rework a lot of the logic using th-abstraction to get structural information about data types and to
+  normalize their representation. This should allow the deriving functions to work on a much wider range
+  of types.
+
+* Change dependency to just be on `some`, not `dependent-sum`, as we just need the reexported classes.
+
 ## 0.1.1.1 - 2021-12-30
 
 * Fix warning with GHC 9.2 about non-canonical `return`.
diff --git a/ReadMe.md b/ReadMe.md
new file mode 100644
--- /dev/null
+++ b/ReadMe.md
@@ -0,0 +1,12 @@
+dependent-sum-template [![Build Status](https://travis-ci.org/obsidiansystems/dependent-sum-template.svg)](https://travis-ci.org/obsidiansystems/dependent-sum-template) [![Hackage](https://img.shields.io/hackage/v/dependent-sum-template.svg)](http://hackage.haskell.org/package/dependent-sum-template)
+==============
+
+This library defines [Template Haskell](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/template_haskell.html) functions for deriving the `GEq`, `GCompare`, `GShow`, and `GRead` functions from the [`some`](https://hackage.haskell.org/package/some) library.
+
+ - `GEq tag` is similar to an `Eq` instance for `tag a` except that with `geq`, values of types `tag a` and `tag b` may be compared, and in the case of equality, evidence that the types `a` and `b` are equal is provided.
+
+ - `GCompare tag` is similar to the above for `Ord`, and provides `gcompare`, giving a `GOrdering` that gives similar evidence of type equality when values match.
+
+ - `GShow tag` means that `tag a` has (the equivalent of) a `Show` instance.
+
+ - `GRead tag` means that `tag a` has (the equivalent of) a `Read` instance.
diff --git a/dependent-sum-template.cabal b/dependent-sum-template.cabal
--- a/dependent-sum-template.cabal
+++ b/dependent-sum-template.cabal
@@ -1,5 +1,5 @@
 name:                   dependent-sum-template
-version:                0.1.1.1
+version:                0.1.2.0
 stability:              experimental
 
 cabal-version:          >= 1.10
@@ -8,11 +8,11 @@
 author:                 James Cook <mokus@deepbondi.net>
 maintainer:             Obsidian Systems, LLC <maintainer@obsidian.systems>
 license:                PublicDomain
-homepage:               https://github.com/obsidiansystems/dependent-sum
+homepage:               https://github.com/obsidiansystems/dependent-sum-template
 
 category:               Unclassified
-synopsis:               Template Haskell code to generate instances of classes in dependent-sum package
-description:            Template Haskell code to generate instances of classes in dependent-sum package, such as 'GEq' and 'GCompare'.
+synopsis:               Template Haskell code to generate instances of classes in some package
+description:            Template Haskell code to generate instances of classes in some package, such as 'GEq' and 'GCompare'.
 
 tested-with:            GHC == 8.0.2,
                         GHC == 8.2.2,
@@ -22,10 +22,11 @@
                         GHC == 9.0.1
 
 extra-source-files:     ChangeLog.md
+                      , ReadMe.md
 
 source-repository head
   type: git
-  location: https://github.com/obsidiansystems/dependent-sum
+  location: https://github.com/obsidiansystems/dependent-sum-template
 
 Library
   if impl(ghc < 7.10)
@@ -35,10 +36,12 @@
   exposed-modules:      Data.GADT.Compare.TH
                         Data.GADT.Show.TH
   other-modules:        Data.Dependent.Sum.TH.Internal
+                        Data.GADT.Compare.Monad
   build-depends:        base >= 3 && <5,
-                        dependent-sum >= 0.4.1 && < 0.8,
+                        some >= 1.0.1 && < 1.1,
+                        containers >= 0.5.9.2,
+                        mtl,
                         template-haskell,
-                        th-extras >= 0.0.0.2,
                         th-abstraction >= 0.4
 
 test-suite test
@@ -50,5 +53,7 @@
   main-is: test.hs
   build-depends: base
                , constraints-extras
-               , dependent-sum
                , dependent-sum-template
+               , template-haskell
+               , some
+               , th-abstraction
diff --git a/src/Data/Dependent/Sum/TH/Internal.hs b/src/Data/Dependent/Sum/TH/Internal.hs
--- a/src/Data/Dependent/Sum/TH/Internal.hs
+++ b/src/Data/Dependent/Sum/TH/Internal.hs
@@ -1,67 +1,128 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE PolyKinds #-}
+
 -- | Shared functions for dependent-sum-template
 module Data.Dependent.Sum.TH.Internal where
 
 import Control.Monad
+import Control.Monad.Writer
+import Data.List (foldl', drop)
+import Data.Maybe
+import Data.Map (Map)
+import qualified Data.Map as Map
+import qualified Data.Map.Merge.Lazy as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Language.Haskell.TH
-import Language.Haskell.TH.Extras
+import Language.Haskell.TH.Datatype
 import Language.Haskell.TH.Datatype.TyVarBndr
 
 classHeadToParams :: Type -> (Name, [Type])
 classHeadToParams t = (h, reverse reversedParams)
-  where (h, reversedParams) = go t
-        go :: Type -> (Name, [Type])
-        go t = case t of
-          AppT f x ->
-            let (h, reversedParams) = classHeadToParams f
-            in (h, x : reversedParams)
-          _ -> (headOfType t, [])
+  where
+    (h, reversedParams) = go t
+    go :: Type -> (Name, [Type])
+    go t = case t of
+      AppT f x ->
+        let (h, reversedParams) = classHeadToParams f
+        in (h, x : reversedParams)
+      _ -> (headOfType t, [])
 
+-- Do not export this type family, it must remain empty. It's used as a way to trick GHC into not unifying certain type variables.
+type family Skolem :: k -> k
+
+skolemize :: Set Name -> Type -> Type
+skolemize rigids t = case t of
+  ForallT bndrs cxt t' -> ForallT bndrs cxt (skolemize (Set.difference rigids (Set.fromList (map tvName bndrs))) t')
+  AppT t1 t2 -> AppT (skolemize rigids t1) (skolemize rigids t2)
+  SigT t k -> SigT (skolemize rigids t) k
+  VarT v -> if Set.member v rigids
+    then AppT (ConT ''Skolem) (VarT v)
+    else t
+  InfixT t1 n t2 -> InfixT (skolemize rigids t1) n (skolemize rigids t2)
+  UInfixT t1 n t2 -> UInfixT (skolemize rigids t1) n (skolemize rigids t2)
+  ParensT t -> ParensT (skolemize rigids t)
+  _ -> t
+
+reifyInstancesWithRigids :: Set Name -> Name -> [Type] -> Q [InstanceDec]
+reifyInstancesWithRigids rigids cls tys = reifyInstances cls (map (skolemize rigids) tys)
+
+-- | Determine the type variables which occur freely in a type.
+freeTypeVariables :: Type -> Set Name
+freeTypeVariables t = case t of
+  ForallT bndrs _ t' -> Set.difference (freeTypeVariables t') (Set.fromList (map tvName bndrs))
+  AppT t1 t2 -> Set.union (freeTypeVariables t1) (freeTypeVariables t2)
+  SigT t _ -> freeTypeVariables t
+  VarT n -> Set.singleton n
+  _ -> Set.empty
+
+subst :: Map Name Type -> Type -> Type
+subst s = f
+  where
+    f = \case
+      ForallT bndrs cxt t ->
+        let s' = Map.difference s (Map.fromList [(k,()) | k <- map tvName bndrs])
+        in ForallT bndrs cxt (subst s' t)
+      AppT t t' -> AppT (f t) (f t')
+      SigT t k -> SigT (f t) k
+      VarT n -> case Map.lookup n s of
+        Just t -> t
+        Nothing -> VarT n
+      InfixT t x t' -> InfixT (f t) x (f t')
+      UInfixT t x t' -> UInfixT (f t) x (f t')
+      x -> x
+
 -- Invoke the deriver for the given class instance.  We assume that the type
 -- we're deriving for is always the first typeclass parameter, if there are
 -- multiple.
-deriveForDec :: Name -> (Q Type -> Q Type) -> ([TyVarBndrSpec] -> [Con] -> Q Dec) -> Dec -> Q [Dec]
-deriveForDec className makeClassHead f dec = deriveForDec' className makeClassHead (f . changeTVFlags specifiedSpec) dec
+deriveForDec
+  :: Name
+  -> (DatatypeInfo -> WriterT [Type] Q Dec)
+  -> Dec
+  -> Q [Dec]
+deriveForDec className f (InstanceD overlaps cxt instanceHead decs) = do
+  let (givenClassName, firstParam : _) = classHeadToParams instanceHead
+  when (givenClassName /= className) $
+    fail $ "while deriving " ++ show className ++ ": wrong class name in prototype declaration: " ++ show givenClassName
+  let dataTypeName = headOfType firstParam
+  dataTypeInfo <- reifyDatatype dataTypeName
+  let instTypes = datatypeInstTypes dataTypeInfo
+      paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+      instTypes' = case reverse instTypes of
+        [] -> fail "deriveGEq: Not enough type parameters"
+        (_:xs) -> reverse xs
+      generatedInstanceHead = AppT (ConT className) (foldl AppT (ConT $ datatypeName dataTypeInfo) instTypes')
+  unifiedTypes <- unifyTypes [generatedInstanceHead, instanceHead]
+  let
+    newInstanceHead = applySubstitution unifiedTypes instanceHead
+    newContext = applySubstitution unifiedTypes cxt
+  -- We are not using the generated context that we collect from f, instead
+  -- relying on a correct instance head from the user
+  (dec, _) <- runWriterT $ f dataTypeInfo
+  return [InstanceD overlaps newContext newInstanceHead [dec]]
+deriveForDec className f dataDec = do
+  dataTypeInfo <- normalizeDec dataDec
+  let instTypes = datatypeInstTypes dataTypeInfo
+      paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+      instTypes' = case reverse instTypes of
+        [] -> fail "deriveGEq: Not enough type parameters"
+        (_:xs) -> reverse xs
+      instanceHead = AppT (ConT className) (foldl AppT (ConT $ datatypeName dataTypeInfo) instTypes')
+  (dec, cxt') <- runWriterT (f dataTypeInfo)
+  return [InstanceD Nothing (datatypeContext dataTypeInfo ++ cxt') instanceHead [dec]]
 
-deriveForDec' :: Name -> (Q Type -> Q Type) -> ([TyVarBndrUnit] -> [Con] -> Q Dec) -> Dec -> Q [Dec]
-deriveForDec' className _ f (InstanceD overlaps cxt classHead decs) = do
-    let (givenClassName, firstParam : _) = classHeadToParams classHead
-    when (givenClassName /= className) $
-      fail $ "while deriving " ++ show className ++ ": wrong class name in prototype declaration: " ++ show givenClassName
-    let dataTypeName = headOfType firstParam
-    dataTypeInfo <- reify dataTypeName
-    case dataTypeInfo of
-        TyConI (DataD dataCxt name bndrs _ cons _) -> do
-            dec <- f bndrs cons
-            return [InstanceD overlaps cxt classHead [dec]]
-        _ -> fail $ "while deriving " ++ show className ++ ": the name of an algebraic data type constructor is required"
-deriveForDec' className makeClassHead f (DataD dataCxt name bndrs _ cons _) = return <$> inst
-    where
-        inst = instanceD (cxt (map return dataCxt)) (makeClassHead $ conT name) [dec]
-        dec = f bndrs cons
-#if __GLASGOW_HASKELL__ >= 808
-deriveForDec' className makeClassHead f (DataInstD dataCxt tvBndrs ty _ cons _) = return <$> inst
-#else
-deriveForDec' className makeClassHead f (DataInstD dataCxt name tyArgs _ cons _) = return <$> inst
-#endif
-    where
-        inst = instanceD (cxt (map return dataCxt)) clhead [dec]
-#if __GLASGOW_HASKELL__ >= 808
-        clhead = makeClassHead $ return $ initTy ty
-#if __GLASGOW_HASKELL__ >= 900
-        bndrs = [PlainTV v x | PlainTV v x <- maybe [] id tvBndrs]
-#else
-        bndrs = [PlainTV v | PlainTV v <- maybe [] id tvBndrs]
-#endif
-        initTy (AppT ty _) = ty
-#else
-        clhead = makeClassHead $ foldl1 appT (map return $ (ConT name : init tyArgs))
-        -- TODO: figure out proper number of family parameters vs instance parameters
-        bndrs = [PlainTV v | VarT v <- tail tyArgs ]
-#endif
-        dec = f bndrs cons
+headOfType :: Type -> Name
+headOfType = \case
+  ForallT _ _ ty -> headOfType ty
+  VarT name -> name
+  ConT name -> name
+  TupleT n -> tupleTypeName n
+  ArrowT -> ''(->)
+  ListT -> ''[]
+  AppT t _ -> headOfType t
diff --git a/src/Data/GADT/Compare/Monad.hs b/src/Data/GADT/Compare/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/Compare/Monad.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE PolyKinds #-}
+module Data.GADT.Compare.Monad
+    ( GComparing
+    , runGComparing
+    , geq'
+    , compare'
+    ) where
+
+import Control.Applicative
+import Control.Monad
+import Data.GADT.Compare
+import Data.Type.Equality ((:~:) (..))
+
+-- A monad allowing gcompare to be defined in the same style as geq
+newtype GComparing a b t = GComparing (Either (GOrdering a b) t)
+
+instance Functor (GComparing a b) where fmap f (GComparing x) = GComparing (either Left (Right . f) x)
+instance Monad (GComparing a b) where
+    return = pure
+    GComparing (Left  x) >>= f = GComparing (Left x)
+    GComparing (Right x) >>= f = f x
+instance Applicative (GComparing a b) where
+    pure = GComparing . Right
+    (<*>) = ap
+
+geq' :: GCompare t => t a -> t b -> GComparing x y (a :~: b)
+geq' x y = GComparing (case gcompare x y of
+    GLT -> Left GLT
+    GEQ -> Right Refl
+    GGT -> Left GGT)
+
+compare' x y = GComparing $ case compare x y of
+    LT -> Left GLT
+    EQ -> Right ()
+    GT -> Left GGT
+
+runGComparing (GComparing x) = either id id x
diff --git a/src/Data/GADT/Compare/TH.hs b/src/Data/GADT/Compare/TH.hs
--- a/src/Data/GADT/Compare/TH.hs
+++ b/src/Data/GADT/Compare/TH.hs
@@ -1,113 +1,119 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PolyKinds #-}
 module Data.GADT.Compare.TH
     ( DeriveGEQ(..)
     , DeriveGCompare(..)
-    , GComparing, runGComparing, geq', compare'
+    , module Data.GADT.Compare.Monad
     ) where
 
-import Control.Applicative
 import Control.Monad
-import Data.Dependent.Sum
+import Control.Monad.Writer
 import Data.Dependent.Sum.TH.Internal
 import Data.Functor.Identity
 import Data.GADT.Compare
-import Data.Traversable (for)
+import Data.GADT.Compare.Monad
 import Data.Type.Equality ((:~:) (..))
+import qualified Data.Set as Set
+import Data.Set (Set)
+import qualified Data.Map as Map
+import qualified Data.Map.Merge.Lazy as Map
+import Data.Map (Map)
 import Language.Haskell.TH
-import Language.Haskell.TH.Extras
+import Language.Haskell.TH.Datatype
 
 -- A type class purely for overloading purposes
 class DeriveGEQ t where
     deriveGEq :: t -> Q [Dec]
 
 instance DeriveGEQ Name where
-    deriveGEq typeName = do
-        typeInfo <- reify typeName
-        case typeInfo of
-            TyConI dec -> deriveGEq dec
-            _ -> fail "deriveGEq: the name of a type constructor is required"
+  deriveGEq typeName = do
+    typeInfo <- reifyDatatype typeName
+    let instTypes = datatypeInstTypes typeInfo
+        paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+        instTypes' = case reverse instTypes of
+          [] -> fail "deriveGEq: Not enough type parameters"
+          (_:xs) -> reverse xs
+        instanceHead = AppT (ConT ''GEq) (foldl AppT (ConT typeName) instTypes')
+    (clauses, cxt) <- runWriterT (mapM (geqClause paramVars) (datatypeCons typeInfo))
 
+    return [InstanceD Nothing cxt instanceHead [geqFunction clauses]]
+
 instance DeriveGEQ Dec where
-    deriveGEq = deriveForDec ''GEq (\t -> [t| GEq $t |]) geqFunction
+    deriveGEq = deriveForDec ''GEq $ \typeInfo -> do
+      let
+        instTypes = datatypeInstTypes typeInfo
+        paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+      clauses <- mapM (geqClause paramVars) (datatypeCons typeInfo)
+      return $ geqFunction clauses
 
 instance DeriveGEQ t => DeriveGEQ [t] where
-    deriveGEq [it] = deriveGEq it
-    deriveGEq _ = fail "deriveGEq: [] instance only applies to single-element lists"
+  deriveGEq [it] = deriveGEq it
+  deriveGEq _ = fail "deriveGEq: [] instance only applies to single-element lists"
 
 instance DeriveGEQ t => DeriveGEQ (Q t) where
-    deriveGEq = (>>= deriveGEq)
-
-geqFunction bndrs cons = funD 'geq
-    (  map (geqClause bndrs) cons
-    ++  [ clause [wildP, wildP] (normalB [| Nothing |]) []
-        | length cons /= 1
-        ]
-    )
-
-geqClause bndrs con = do
-    let argTypes = argTypesOfCon con
-        needsGEq argType = any ((`occursInType` argType) . nameOfBinder) (bndrs ++ varsBoundInCon con)
-
-        nArgs = length argTypes
-    lArgNames <- replicateM nArgs (newName "x")
-    rArgNames <- replicateM nArgs (newName "y")
-
-    clause [ conP conName (map varP lArgNames)
-           , conP conName (map varP rArgNames)
-           ]
-        ( normalB $ doE
-            (  [ if needsGEq argType
-                    then bindS (conP 'Refl []) [| geq $(varE lArg) $(varE rArg) |]
-                    else noBindS [| guard ($(varE lArg) == $(varE rArg)) |]
-               | (lArg, rArg, argType) <- zip3 lArgNames rArgNames argTypes
-               ]
-            ++ [ noBindS [| return Refl |] ]
-            )
-        ) []
-    where conName = nameOfCon con
-
--- A monad allowing gcompare to be defined in the same style as geq
-newtype GComparing a b t = GComparing (Either (GOrdering a b) t)
+  deriveGEq = (>>= deriveGEq)
 
-instance Functor (GComparing a b) where fmap f (GComparing x) = GComparing (either Left (Right . f) x)
-instance Monad (GComparing a b) where
-    return = pure
-    GComparing (Left  x) >>= f = GComparing (Left x)
-    GComparing (Right x) >>= f = f x
-instance Applicative (GComparing a b) where
-    pure = GComparing . Right
-    (<*>) = ap
+geqFunction :: [Clause] -> Dec
+geqFunction clauses = FunD 'geq $ clauses ++ [ Clause [WildP, WildP] (NormalB (ConE 'Nothing)) [] ]
+ -- TODO: only include last clause if there's more than one constructor?
 
-geq' :: GCompare t => t a -> t b -> GComparing x y (a :~: b)
-geq' x y = GComparing (case gcompare x y of
-    GLT -> Left GLT
-    GEQ -> Right Refl
-    GGT -> Left GGT)
+geqClause :: Set Name -> ConstructorInfo -> WriterT Cxt Q Clause
+geqClause paramVars con = do
+  let conName = constructorName con
+      argTypes = constructorFields con
+      conTyVars = Set.fromList (map tvName (constructorVars con))
+      needsGEq argType = not . Set.null $
+        Set.intersection (freeTypeVariables argType) (Set.union paramVars conTyVars)
+  lArgNames <- forM argTypes $ \_ -> lift $ newName "x"
+  rArgNames <- forM argTypes $ \_ -> lift $ newName "y"
 
-compare' x y = GComparing $ case compare x y of
-    LT -> Left GLT
-    EQ -> Right ()
-    GT -> Left GGT
+  stmts <- forM (zip3 lArgNames rArgNames argTypes) $ \(l, r, t) -> do
+    case t of
+      AppT tyFun tyArg | needsGEq t -> do
+        u <- lift $ reifyInstancesWithRigids paramVars ''GEq [tyFun]
+        case u of
+          [] -> tell [AppT (ConT ''GEq) tyFun]
+          [(InstanceD _ cxt _ _)] -> tell cxt
+          _ -> fail $ "More than one instance found for GEq (" ++ show (ppr tyFun) ++ "), and unsure what to do. Please report this."
+        lift $ bindS (conP 'Refl []) [| geq $(varE l) $(varE r) |]
+      _ -> lift $ noBindS [| guard ($(varE l) == $(varE r)) |]
+  ret <- lift $ noBindS [| return Refl |]
 
-runGComparing (GComparing x) = either id id x
+  return $ Clause
+    [ ConP conName (map VarP lArgNames)
+    , ConP conName (map VarP rArgNames) ]
+    ( NormalB (doUnqualifiedE (stmts ++ [ret])))
+    []
 
 class DeriveGCompare t where
     deriveGCompare :: t -> Q [Dec]
 
 instance DeriveGCompare Name where
     deriveGCompare typeName = do
-        typeInfo <- reify typeName
-        case typeInfo of
-            TyConI dec -> deriveGCompare dec
-            _ -> fail "deriveGCompare: the name of a type constructor is required"
+      typeInfo <- reifyDatatype typeName
+      let instTypes = datatypeInstTypes typeInfo
+          paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+          instTypes' = case reverse instTypes of
+            [] -> fail "deriveGCompare: Not enough type parameters"
+            (_:xs) -> reverse xs
+          instanceHead = AppT (ConT ''GCompare) (foldl AppT (ConT typeName) instTypes')
+      (clauses, cxt) <- runWriterT (fmap concat $ mapM (gcompareClauses paramVars) (datatypeCons typeInfo))
+      dec <- gcompareFunction clauses
+      return [InstanceD Nothing cxt instanceHead [dec]]
 
 instance DeriveGCompare Dec where
-    deriveGCompare = deriveForDec ''GCompare (\t -> [t| GCompare $t |]) gcompareFunction
+    deriveGCompare = deriveForDec ''GCompare $ \typeInfo -> do
+      let
+        instTypes = datatypeInstTypes typeInfo
+        paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+      clauses <- mapM (gcompareClauses paramVars) (datatypeCons typeInfo)
+      lift $ gcompareFunction (concat clauses)
 
 instance DeriveGCompare t => DeriveGCompare [t] where
     deriveGCompare [it] = deriveGCompare it
@@ -116,47 +122,45 @@
 instance DeriveGCompare t => DeriveGCompare (Q t) where
     deriveGCompare = (>>= deriveGCompare)
 
-gcompareFunction boundVars cons
-    | null cons = funD 'gcompare [clause [] (normalB [| \x y -> seq x (seq y undefined) |]) []]
-    | otherwise = funD 'gcompare (concatMap gcompareClauses cons)
-    where
-        -- for every constructor, first check for equality (recursively comparing
-        -- arguments) then add catch-all cases; all not-yet-matched patterns are
-        -- "greater than" the constructor under consideration.
-        gcompareClauses con =
-            [ mainClause con
-            , clause [recP conName [], wildP] (normalB [| GLT |]) []
-            , clause [wildP, recP conName []] (normalB [| GGT |]) []
-            ] where conName = nameOfCon con
+gcompareFunction :: [Clause] -> Q Dec
+gcompareFunction [] = funD 'gcompare [clause [] (normalB [| \x y -> seq x (seq y undefined) |]) []]
+gcompareFunction clauses = return $ FunD 'gcompare clauses
 
-        needsGCompare argType con = any ((`occursInType` argType) . nameOfBinder) (boundVars ++ varsBoundInCon con)
+gcompareClauses :: Set Name -> ConstructorInfo -> WriterT Cxt Q [Clause]
+gcompareClauses paramVars con = do
+  let conName = constructorName con
+      argTypes = constructorFields con
+      conTyVars = Set.fromList (map tvName (constructorVars con))
+      needsGCompare argType = not . Set.null $
+        Set.intersection (freeTypeVariables argType) (Set.union paramVars conTyVars)
 
-        -- main clause; using the 'GComparing' monad, compare all arguments to the
-        -- constructor recursively, attempting to unify type variables by recursive
-        -- calls to gcompare whenever needed (that is, whenever a constructor argument's
-        -- type contains a variable bound in the data declaration or in the constructor's
-        -- type signature)
-        mainClause con = do
-            let conName = nameOfCon con
-                argTypes = argTypesOfCon con
-                nArgs = length argTypes
+  lArgNames <- forM argTypes $ \_ -> lift $ newName "x"
+  rArgNames <- forM argTypes $ \_ -> lift $ newName "y"
 
-            lArgNames <- replicateM nArgs (newName "x")
-            rArgNames <- replicateM nArgs (newName "y")
+  stmts <- forM (zip3 lArgNames rArgNames argTypes) $ \(lArg, rArg, argType) ->
+    case argType of
+      AppT tyFun tyArg | needsGCompare argType -> do
+        u <- lift $ reifyInstancesWithRigids paramVars ''GCompare [tyFun]
+        case u of
+          [] -> tell [AppT (ConT ''GCompare) tyFun]
+          [(InstanceD _ cxt _ _)] -> tell cxt -- this might not be enough, may want to do full instance resolution.
+          _ -> fail $ "More than one instance of GCompare (" ++ show (ppr tyFun) ++ ") found, and unsure what to do. Please report this."
+        lift $ bindS (conP 'Refl []) [| geq' $(varE lArg) $(varE rArg) |]
+      _ -> lift $ noBindS [| compare' $(varE lArg) $(varE rArg) |]
 
-            clause [ conP conName (map varP lArgNames)
-                   , conP conName (map varP rArgNames)
-                   ]
-                ( normalB
-                    [| runGComparing $
-                        $(doE
-                            (  [ if needsGCompare argType con
-                                    then bindS (conP 'Refl []) [| geq' $(varE lArg) $(varE rArg) |]
-                                    else noBindS [| compare' $(varE lArg) $(varE rArg) |]
-                               | (lArg, rArg, argType) <- zip3 lArgNames rArgNames argTypes
-                               ]
-                            ++ [ noBindS [| return GEQ |] ]
-                            )
-                        )
-                    |]
-                ) []
+  ret <- lift $ noBindS [| return GEQ |]
+
+  let main = Clause
+        [ ConP conName (map VarP lArgNames)
+        , ConP conName (map VarP rArgNames) ]
+        ( NormalB (AppE (VarE 'runGComparing) (doUnqualifiedE (stmts ++ [ret]))))
+        []
+      lt = Clause [RecP conName [], WildP] (NormalB (ConE 'GLT)) []
+      gt = Clause [WildP, RecP conName []] (NormalB (ConE 'GGT)) []
+  return [main, lt, gt]
+
+#if MIN_VERSION_template_haskell(2,17,0)
+doUnqualifiedE = DoE Nothing
+#else
+doUnqualifiedE = DoE
+#endif
diff --git a/src/Data/GADT/Show/TH.hs b/src/Data/GADT/Show/TH.hs
--- a/src/Data/GADT/Show/TH.hs
+++ b/src/Data/GADT/Show/TH.hs
@@ -5,27 +5,40 @@
 
 import Control.Applicative
 import Control.Monad
-import Data.Dependent.Sum
+import Control.Monad.Writer
 import Data.Dependent.Sum.TH.Internal
 import Data.Functor.Identity
 import Data.GADT.Show
 import Data.Traversable (for)
 import Data.List
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Language.Haskell.TH
-import Language.Haskell.TH.Extras
+import Language.Haskell.TH.Datatype
 
 class DeriveGShow t where
-    deriveGShow :: t -> Q [Dec]
+  deriveGShow :: t -> Q [Dec]
 
 instance DeriveGShow Name where
-    deriveGShow typeName = do
-        typeInfo <- reify typeName
-        case typeInfo of
-            TyConI dec -> deriveGShow dec
-            _ -> fail "deriveGShow: the name of a type constructor is required"
+ deriveGShow typeName = do
+  typeInfo <- reifyDatatype typeName
+  let instTypes = datatypeInstTypes typeInfo
+      paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+      instTypes' = case reverse instTypes of
+        [] -> fail "deriveGEq: Not enough type parameters"
+        (_:xs) -> reverse xs
+      instanceHead = AppT (ConT ''GShow) (foldl AppT (ConT typeName) instTypes')
+  (clauses, cxt) <- runWriterT (mapM (gshowClause typeName paramVars) (datatypeCons typeInfo))
 
+  return [InstanceD Nothing (datatypeContext typeInfo ++ cxt) instanceHead [gshowFunction clauses]]
+
 instance DeriveGShow Dec where
-    deriveGShow = deriveForDec ''GShow (\t -> [t| GShow $t |]) $ \_ -> gshowFunction
+    deriveGShow = deriveForDec ''GShow $ \typeInfo -> do
+      let
+        instTypes = datatypeInstTypes typeInfo
+        paramVars = Set.unions [freeTypeVariables t | t <- instTypes]
+      clauses <- mapM (gshowClause (datatypeName typeInfo) paramVars) (datatypeCons typeInfo)
+      return $ gshowFunction clauses
 
 instance DeriveGShow t => DeriveGShow [t] where
     deriveGShow [it] = deriveGShow it
@@ -34,32 +47,58 @@
 instance DeriveGShow t => DeriveGShow (Q t) where
     deriveGShow = (>>= deriveGShow)
 
-gshowFunction = funD 'gshowsPrec . map gshowClause
+gshowFunction :: [Clause] -> Dec
+gshowFunction clauses = FunD 'gshowsPrec clauses
 
-gshowClause con = do
-    let conName  = nameOfCon con
-        argTypes = argTypesOfCon con
-        nArgs    = length argTypes
+isApplicationOf :: Type -> Type -> Bool
+isApplicationOf t t' = t == t' || case t' of
+  AppT u _ -> isApplicationOf t u
+  _ -> False
 
-        precName = mkName "p"
+gshowClause :: Name -> Set Name -> ConstructorInfo -> WriterT [Type] Q Clause
+gshowClause typeName paramVars con = do
+  let conName  = constructorName con
+      argTypes = constructorFields con
+      conTyVars = Set.fromList (map tvName (constructorVars con))
 
-    argNames <- replicateM nArgs (newName "x")
+  precName <- lift $ newName "prec"
+  argNames <- forM argTypes $ \_ -> lift $ newName "x"
 
-    let precPat = if null argNames
-          then wildP
-          else varP precName
+  argShowExprs <- forM (zip argNames argTypes) $ \(n,t) -> do
+    let useShow = do
+          tell [AppT (ConT ''Show) t]
+          return [| showsPrec 11 $(varE n) |]
+    case t of
+      AppT tyFun tyArg -> do
+        let useGShow = do
+              tell [AppT (ConT ''GShow) tyFun]
+              return [| gshowsPrec 11 $(varE n) |]
+        if isApplicationOf (ConT typeName) tyFun
+          then return [| gshowsPrec 11 $(varE n) |]
+          else do
+            v <- lift $ reifyInstancesWithRigids paramVars ''GShow [tyFun]
+            case v of
+              (_:_) -> useGShow
+              _ -> do
+                u <- lift $ reifyInstancesWithRigids paramVars ''Show [t]
+                case u of
+                  (_:_) -> useShow
+                  [] -> useGShow
+      _ -> useShow
 
-    clause [precPat, conP conName (map varP argNames)]
-        (normalB (gshowBody (varE precName) conName argNames)) []
+  let precPat = if null argNames
+        then wildP
+        else varP precName
 
+  lift $ clause [precPat, conP conName (map varP argNames)]
+    (normalB (gshowBody (varE precName) conName argShowExprs)) []
+
 showsName name = [| showString $(litE . stringL $ nameBase name) |]
 
+gshowBody :: Q Exp -> Name -> [Q Exp] -> Q Exp
 gshowBody prec conName [] = showsName conName
-gshowBody prec conName argNames =
-    [| showParen ($prec > 10) $( composeExprs $ intersperse [| showChar ' ' |]
-        ( showsName conName
-        : [ [| showsPrec 11 $arg |]
-          | argName <- argNames, let arg = varE argName
-          ]
-        ))
-     |]
+gshowBody prec conName argShowExprs =
+  let body = foldr (\e es -> [| $e . $es |]) [| id |] .
+               intersperse [| showChar ' ' |] $
+                 showsName conName : argShowExprs
+  in [| showParen ($prec > 10) $body |]
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -11,8 +12,9 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -ddump-splices #-}
 import Control.Monad
-import Data.Dependent.Sum
 import Data.Functor.Identity
 import Data.Constraint.Extras.TH
 import Data.GADT.Compare
@@ -88,12 +90,12 @@
     F :: Foo a -> Bar a
     S :: Bar String
 
-data Baz a where
-    L :: Qux a -> Int -> Baz [a]
-
 data Qux a where
     FB :: Foo (a -> b) -> Bar b -> Qux (a -> (b, b))
 
+data Baz a where
+    L :: Qux a -> Int -> Baz [a]
+
 deriveGEq ''Foo
 deriveGEq ''Bar
 deriveGEq ''Qux
@@ -153,16 +155,32 @@
 -- ([t||] brackets won't work because they can only quote types of kind *).
 data Spleeb a b where
     P :: a Double -> Qux b -> Spleeb a b
+
+deriveGEq ''Spleeb
+deriveGCompare ''Spleeb
+
+-- NB: We could also write:
+-- deriving instance (Show (a Double), Show (Qux b)) => Show (Spleeb a b)
+-- instance (Show (a Double)) => GShow (Spleeb a)
+
+deriveGShow ''Spleeb
+
+
+data SpleebHard a b where
+    PH :: a Double -> Qux b -> SpleebHard a b
+    PI :: a Int -> Foo b -> SpleebHard a b
+
 -- need a cleaner 'one-shot' way of defining these - the empty instances need to appear
 -- in the same quotation because the GEq context of the GCompare class causes stage
 -- restriction errors... seems like GHC shouldn't actually check things like that till
 -- the final splice, but whatever.
+
 do
     [geqInst, gcompareInst, gshowInst] <-
         [d|
-            instance GEq a => GEq (Spleeb a)
-            instance GCompare a => GCompare (Spleeb a)
-            instance Show (a Double) => GShow (Spleeb a)
+            instance GEq a => GEq (SpleebHard a)
+            instance GCompare a => GCompare (SpleebHard a)
+            instance GShow a => GShow (SpleebHard a)
           |]
 
     concat <$> sequence
@@ -171,8 +189,16 @@
         , deriveGShow    gshowInst
         ]
 
-instance Show (a Double) => Show (Spleeb a b) where showsPrec = gshowsPrec
+instance GShow a => Show (SpleebHard a b) where showsPrec = gshowsPrec
 
+data SpleebHard2 a b where
+    PH2 :: a Double -> Qux b -> SpleebHard2 a b
+    PI2 :: a Int -> Foo b -> SpleebHard2 a b
+
+deriveGEq ''SpleebHard2
+deriveGCompare ''SpleebHard2
+deriveGShow ''SpleebHard2
+
 -- another option; start from the declaration and juggle that a bit
 do
     decs <- [d|
@@ -191,3 +217,17 @@
         ]
 
 instance Show (Fnord a) where showsPrec = gshowsPrec
+
+
+data MyTest a :: * -> * where
+  MyTest_1 :: MyTest a ()
+  MyTest_2 :: MyTest a Int
+
+deriving instance Eq (MyTest a b)
+deriving instance Ord (MyTest a b)
+deriving instance Show (MyTest a b)
+
+deriveGShow ''MyTest
+deriveGEq ''MyTest
+deriveGCompare ''MyTest
+deriveArgDict ''MyTest