diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,10 @@
+# 0.3.1
+* Rewrote `Data.Functor.Invariant.TH`'s type inferencer. This avoids a nasty
+  GHC 7.8-specific bug involving derived `Invariant(2)` instances for data
+  families.
+* Add `Invariant` instances for `Data.Complex.Complex`, `Data.Monoid.Product`,
+  and `Data.Monoid.Sum`
+
 # 0.3
 * Require `bifunctors-5.2` and `profunctors-5.2`. Add `Invariant(2)` instances
   for newly introduced datatypes from those packages.
diff --git a/invariant.cabal b/invariant.cabal
--- a/invariant.cabal
+++ b/invariant.cabal
@@ -1,5 +1,5 @@
 name:                invariant
-version:             0.3
+version:             0.3.1
 synopsis:            Haskell 98 invariant functors
 description:         Haskell 98 invariant functors
 category:            Control, Data
diff --git a/src/Data/Functor/Invariant.hs b/src/Data/Functor/Invariant.hs
--- a/src/Data/Functor/Invariant.hs
+++ b/src/Data/Functor/Invariant.hs
@@ -56,17 +56,26 @@
 import           Control.Monad (MonadPlus(..), liftM)
 import qualified Control.Monad.ST as Strict (ST)
 import qualified Control.Monad.ST.Lazy as Lazy (ST)
+#if MIN_VERSION_base(4,4,0)
+import           Data.Complex (Complex(..))
+#endif
 import qualified Data.Foldable as F (Foldable(..))
+import qualified Data.Functor.Compose as Functor (Compose(..))
 import           Data.Functor.Identity (Identity)
+import           Data.Functor.Product as Functor (Product(..))
+import           Data.Functor.Sum as Functor (Sum(..))
 #if __GLASGOW_HASKELL__ < 711
 import           Data.Ix (Ix)
 #endif
-import qualified Data.Monoid as Monoid (First(..), Last(..))
+import           Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.Monoid as Monoid (First(..), Last(..), Product(..), Sum(..))
 #if MIN_VERSION_base(4,8,0)
 import           Data.Monoid (Alt(..))
 #endif
 import           Data.Monoid (Dual(..), Endo(..))
 import           Data.Proxy (Proxy(..))
+import qualified Data.Semigroup as Semigroup (First(..), Last(..), Option(..))
+import           Data.Semigroup (Min(..), Max(..), Arg(..))
 import qualified Data.Traversable as T (Traversable(..))
 #if GHC_GENERICS_OK
 import           GHC.Generics
@@ -116,11 +125,6 @@
 import           Data.Profunctor.Traversing
 import           Data.Profunctor.Unsafe
 
--- semigroups
-import           Data.List.NonEmpty (NonEmpty(..))
-import qualified Data.Semigroup as Semigroup (First(..), Last(..), Option(..))
-import           Data.Semigroup (Min(..), Max(..), Arg(..))
-
 -- StateVar
 import           Data.StateVar (StateVar(..), SettableStateVar(..))
 
@@ -146,11 +150,8 @@
 import qualified Control.Monad.Trans.State.Strict as Strict (StateT(..))
 import qualified Control.Monad.Trans.Writer.Lazy as Lazy (WriterT, mapWriterT)
 import qualified Control.Monad.Trans.Writer.Strict as Strict (WriterT, mapWriterT)
-import qualified Data.Functor.Compose as Transformers (Compose(..))
 import           Data.Functor.Constant (Constant(..))
-import           Data.Functor.Product as Transformers (Product(..))
 import           Data.Functor.Reverse (Reverse(..))
-import           Data.Functor.Sum as Transformers (Sum(..))
 
 -- unordered-containers
 import           Data.HashMap.Lazy (HashMap)
@@ -201,17 +202,17 @@
 instance Invariant ((,,,,) a b c d) where
   invmap f _ ~(a, b, c, d, x) = (a, b, c, d, f x)
 
--- | from @Control.Applicative@
+-- | from "Control.Applicative"
 instance Invariant (Const a) where invmap = invmapFunctor
--- | from @Control.Applicative@
+-- | from "Control.Applicative"
 instance Invariant ZipList where invmap = invmapFunctor
--- | from @Control.Applicative@
+-- | from "Control.Applicative"
 instance Monad m => Invariant (WrappedMonad m) where invmap = invmapFunctor
--- | from @Control.Applicative@
+-- | from "Control.Applicative"
 instance Arrow arr => Invariant (App.WrappedArrow arr a) where
   invmap f _ (App.WrapArrow x) = App.WrapArrow $ ((arr f) Cat.. x)
 
--- | from @Control.Arrow@
+-- | from "Control.Arrow"
 instance
 #if MIN_VERSION_base(4,4,0)
   Arrow a
@@ -221,46 +222,96 @@
   => Invariant (ArrowMonad a) where
   invmap f _ (ArrowMonad m) = ArrowMonad (m >>> arr f)
 
--- | from @Control.Exception@
+-- | from "Control.Exception"
 instance Invariant Handler where
   invmap f _ (Handler h) = Handler (fmap f . h)
 
--- | from @Data.Functor.Identity@
+#if MIN_VERSION_base(4,4,0)
+-- | from "Data.Complex"
+instance Invariant Complex where
+  invmap f _ (r :+ i) = f r :+ f i
+#endif
+
+-- | from "Data.Functor.Compose"
+instance (Invariant f, Invariant g) => Invariant (Functor.Compose f g) where
+  invmap f g (Functor.Compose x) =
+    Functor.Compose (invmap (invmap f g) (invmap g f) x)
+
+-- | from "Data.Functor.Identity"
 instance Invariant Identity where
   invmap = invmapFunctor
 
--- | from @Data.Monoid@
-instance Invariant Dual where invmap f _ (Dual x) = Dual (f x)
--- | from @Data.Monoid@
+-- | from "Data.Functor.Product"
+instance (Invariant f, Invariant g) => Invariant (Functor.Product f g) where
+  invmap f g (Functor.Pair x y) = Functor.Pair (invmap f g x) (invmap f g y)
+
+-- | from "Data.Functor.Sum"
+instance (Invariant f, Invariant g) => Invariant (Functor.Sum f g) where
+  invmap f g (InL x) = InL (invmap f g x)
+  invmap f g (InR y) = InR (invmap f g y)
+
+-- | from "Data.List.NonEmpty"
+instance Invariant NonEmpty where
+  invmap = invmapFunctor
+
+-- | from "Data.Monoid"
+instance Invariant Dual where
+  invmap f _ (Dual x) = Dual (f x)
+-- | from "Data.Monoid"
 instance Invariant Endo where
   invmap f g (Endo x) = Endo (f . x . g)
--- | from @Data.Monoid@
+-- | from "Data.Monoid"
 instance Invariant Monoid.First where
   invmap f g (Monoid.First x) = Monoid.First (invmap f g x)
--- | from @Data.Monoid@
+-- | from "Data.Monoid"
 instance Invariant Monoid.Last where
   invmap f g (Monoid.Last x) = Monoid.Last (invmap f g x)
+-- | from "Data.Monoid"
+instance Invariant Monoid.Product where
+  invmap f _ (Monoid.Product x) = Monoid.Product (f x)
+-- | from "Data.Monoid"
+instance Invariant Monoid.Sum where
+  invmap f _ (Monoid.Sum x) = Monoid.Sum (f x)
 #if MIN_VERSION_base(4,8,0)
--- | from @Data.Monoid@
+-- | from "Data.Monoid"
 instance Invariant f => Invariant (Alt f) where
   invmap f g (Alt x) = Alt (invmap f g x)
 #endif
 
--- | from @Data.Proxy@
+-- | from "Data.Proxy"
 instance Invariant Proxy where
   invmap = invmapFunctor
 
--- | from @System.Console.GetOpt@
+-- | from "Data.Semigroup"
+instance Invariant Min where
+  invmap = invmapFunctor
+-- | from "Data.Semigroup"
+instance Invariant Max where
+  invmap = invmapFunctor
+-- | from "Data.Semigroup"
+instance Invariant Semigroup.First where
+  invmap = invmapFunctor
+-- | from "Data.Semigroup"
+instance Invariant Semigroup.Last where
+  invmap = invmapFunctor
+-- | from "Data.Semigroup"
+instance Invariant Semigroup.Option where
+  invmap = invmapFunctor
+-- | from "Data.Semigroup"
+instance Invariant (Arg a) where
+  invmap = invmapFunctor
+
+-- | from "System.Console.GetOpt"
 instance Invariant ArgDescr where
   invmap f _ (NoArg a)    = NoArg (f a)
   invmap f _ (ReqArg g s) = ReqArg (f . g) s
   invmap f _ (OptArg g s) = OptArg (f . g) s
--- | from @System.Console.GetOpt@
+-- | from "System.Console.GetOpt"
 instance Invariant ArgOrder where
   invmap _ _ RequireOrder      = RequireOrder
   invmap _ _ Permute           = Permute
   invmap f _ (ReturnInOrder g) = ReturnInOrder (f . g)
--- | from @System.Console.GetOpt@
+-- | from "System.Console.GetOpt"
 instance Invariant OptDescr where
   invmap f g (GetOpt.Option a b argDescr c) = GetOpt.Option a b (invmap f g argDescr) c
 
@@ -381,28 +432,6 @@
 instance Invariant2 p => Invariant (TambaraSum p a) where
   invmap = invmap2 id id
 
--- | from the @semigroups@ package
-instance Invariant NonEmpty where
-  invmap = invmapFunctor
--- | from the @semigroups@ package
-instance Invariant Min where
-  invmap = invmapFunctor
--- | from the @semigroups@ package
-instance Invariant Max where
-  invmap = invmapFunctor
--- | from the @semigroups@ package
-instance Invariant Semigroup.First where
-  invmap = invmapFunctor
--- | from the @semigroups@ package
-instance Invariant Semigroup.Last where
-  invmap = invmapFunctor
--- | from the @semigroups@ package
-instance Invariant Semigroup.Option where
-  invmap = invmapFunctor
--- | from the @semigroups@ package
-instance Invariant (Arg a) where
-  invmap = invmapFunctor
-
 -- | from the @StateVar@ package
 instance Invariant StateVar where
   invmap f g (StateVar ga sa) = StateVar (fmap f ga) (lmap g sa)
@@ -481,22 +510,11 @@
     where mapFstPair :: (a -> b) -> (a, c) -> (b, c)
           mapFstPair h (a, w) = (h a, w)
 -- | from the @transformers@ package
-instance (Invariant f, Invariant g) => Invariant (Transformers.Compose f g) where
-  invmap f g (Transformers.Compose x) =
-    Transformers.Compose (invmap (invmap f g) (invmap g f) x)
--- | from the @transformers@ package
 instance Invariant (Constant a) where
   invmap = invmapFunctor
 -- | from the @transformers@ package
-instance (Invariant f, Invariant g) => Invariant (Transformers.Product f g) where
-  invmap f g (Transformers.Pair x y) = Transformers.Pair (invmap f g x) (invmap f g y)
--- | from the @transformers@ package
 instance Invariant f => Invariant (Reverse f) where
   invmap f g (Reverse a) = Reverse (invmap f g a)
--- | from the @transformers@ package
-instance (Invariant f, Invariant g) => Invariant (Transformers.Sum f g) where
-  invmap f g (InL x) = InL (invmap f g x)
-  invmap f g (InR y) = InR (invmap f g y)
 
 -- | from the @unordered-containers@ package
 instance Invariant (HashMap k) where
@@ -633,12 +651,16 @@
 instance Invariant2 ((,,,,) a b c) where
   invmap2 f _ g _ ~(a, b, c, x, y) = (a, b, c, f x, g y)
 
--- | from @Control.Applicative@
+-- | from "Control.Applicative"
 instance Invariant2 Const where invmap2 = invmap2Bifunctor
--- | from @Control.Applicative@
+-- | from "Control.Applicative"
 instance Arrow arr => Invariant2 (App.WrappedArrow arr) where
   invmap2 _ f' g _ (App.WrapArrow x) = App.WrapArrow $ arr g Cat.. x Cat.. arr f'
 
+-- | from "Data.Semigroup"
+instance Invariant2 Arg where
+  invmap2 = invmap2Bifunctor
+
 -- | from the @bifunctors@ package
 instance (Invariant2 p, Invariant f, Invariant g) => Invariant2 (Biff p f g) where
   invmap2 f f' g g' =
@@ -746,10 +768,6 @@
   invmap2 f f' g g' (TambaraSum p) =
     TambaraSum (invmap2 (first f) (first f') (first g) (first g') p)
 
--- | from the @semigroups@ package
-instance Invariant2 Arg where
-  invmap2 = invmap2Bifunctor
-
 -- | from the @tagged@ package
 instance Invariant2 Tagged where
   invmap2 = invmap2Bifunctor
@@ -821,31 +839,30 @@
 -- GHC Generics
 -------------------------------------------------------------------------------
 
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant V1 where
   -- NSF 25 July 2015: I'd prefer an -XEmptyCase, but Haskell98.
   invmap _ _ _ = error "Invariant V1"
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant U1 where invmap _ _ _ = U1
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance (Invariant l, Invariant r) => Invariant ((:+:) l r) where
   invmap f g (L1 l) = L1 $ invmap f g l
   invmap f g (R1 r) = R1 $ invmap f g r
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance (Invariant l, Invariant r) => Invariant ((:*:) l r) where
   invmap f g ~(l :*: r) = invmap f g l :*: invmap f g r
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant (K1 i c) where invmap _ _ (K1 c) = K1 c
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant2 (K1 i) where invmap2 f _ _ _ (K1 c) = K1 $ f c
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant f => Invariant (M1 i t f) where invmap f g (M1 fp) = M1 $ invmap f g fp
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant Par1 where invmap f _ (Par1 c) = Par1 $ f c
--- | from @GHC.Generics@
+-- | from "GHC.Generics"
 instance Invariant f => Invariant (Rec1 f) where invmap f g (Rec1 fp) = Rec1 $ invmap f g fp
--- | from @GHC.Generics@; genuinely relying on this instance
--- likely requires writing your 'Generic1' instance by hand
+-- | from "GHC.Generics"
 instance (Invariant f, Invariant g) => Invariant ((:.:) f g) where
   invmap f g (Comp1 fgp) = Comp1 $ invmap (invmap f g) (invmap g f) fgp
 
diff --git a/src/Data/Functor/Invariant/TH.hs b/src/Data/Functor/Invariant/TH.hs
--- a/src/Data/Functor/Invariant/TH.hs
+++ b/src/Data/Functor/Invariant/TH.hs
@@ -23,11 +23,15 @@
     , makeInvmap2
     ) where
 
+import           Control.Monad (unless, when)
+
+#if MIN_VERSION_template_haskell(2,8,0) && !(MIN_VERSION_template_haskell(2,10,0))
+import           Data.Foldable (foldr')
+#endif
 import           Data.Functor.Invariant.TH.Internal
 import           Data.List
-#if __GLASGOW_HASKELL__ < 710 && MIN_VERSION_template_haskell(2,8,0)
-import qualified Data.Set as Set
-#endif
+import qualified Data.Map as Map (fromList, keys, lookup, size)
+import           Data.Maybe
 
 import           Language.Haskell.TH.Lib
 import           Language.Haskell.TH.Ppr
@@ -108,24 +112,6 @@
   1. @v@ must be a type variable.
   2. @v@ must not be mentioned in any of @e1@, ..., @e2@.
 
-* In GHC 7.8, a bug exists that can cause problems when a data family declaration and
-  one of its data instances use different type variables, e.g.,
-
-  @
-  data family Foo a b c
-  data instance Foo Int y z = Foo Int y z
-  $('deriveInvariant' 'Foo)
-  @
-
-  To avoid this issue, it is recommened that you use the same type variables in the
-  same positions in which they appeared in the data family declaration:
-
-  @
-  data family Foo a b c
-  data instance Foo Int b c = Foo Int b c
-  $('deriveInvariant' 'Foo)
-  @
-
 -}
 
 -- | Generates an 'Invariant' instance declaration for the given data type or data
@@ -235,27 +221,23 @@
 deriveInvariantClass iClass name = withType name fromCons
   where
     fromCons :: Name -> Cxt -> [TyVarBndr] -> [Con] -> Maybe [Type] -> Q [Dec]
-    fromCons name' ctxt tvbs cons mbTys = (:[]) `fmap`
+    fromCons name' ctxt tvbs cons mbTys = (:[]) `fmap` do
+        (instanceCxt, instanceType)
+            <- buildTypeInstance iClass name' ctxt tvbs mbTys
         instanceD (return instanceCxt)
                   (return instanceType)
-                  (invmapDecs droppedNbs cons)
-      where
-        (instanceCxt, instanceType, droppedNbs) =
-            buildTypeInstance iClass name' ctxt tvbs mbTys
+                  (invmapDecs iClass cons)
 
 -- | Generates a declaration defining the primary function corresponding to a
 -- particular class (invmap for Invariant and invmap2 for Invariant2).
-invmapDecs :: [NameBase] -> [Con] -> [Q Dec]
-invmapDecs nbs cons =
-    [ funD classFuncName
+invmapDecs :: InvariantClass -> [Con] -> [Q Dec]
+invmapDecs iClass cons =
+    [ funD (invmapName iClass)
            [ clause []
-                    (normalB $ makeInvmapForCons nbs cons)
+                    (normalB $ makeInvmapForCons iClass cons)
                     []
            ]
     ]
-  where
-    classFuncName :: Name
-    classFuncName = invmapName . toEnum $ length nbs
 
 -- | Generates a lambda expression which behaves like invmap (for Invariant),
 -- or invmap2 (for Invariant2).
@@ -264,21 +246,23 @@
   where
     fromCons :: Name -> Cxt -> [TyVarBndr] -> [Con] -> Maybe [Type] -> Q Exp
     fromCons name' ctxt tvbs cons mbTys =
-        let nbs = thd3 $ buildTypeInstance iClass name' ctxt tvbs mbTys
-         in nbs `seq` makeInvmapForCons nbs cons
+        -- We force buildTypeInstance here since it performs some checks for whether
+        -- or not the provided datatype can actually have invmap/invmap2
+        -- implemented for it, and produces errors if it can't.
+        buildTypeInstance iClass name' ctxt tvbs mbTys
+          `seq` makeInvmapForCons iClass cons
 
 -- | Generates a lambda expression for invmap(2) for the given constructors.
 -- All constructors must be from the same type.
-makeInvmapForCons :: [NameBase] -> [Con] -> Q Exp
-makeInvmapForCons nbs cons = do
-    let numNbs = length nbs
+makeInvmapForCons :: InvariantClass -> [Con] -> Q Exp
+makeInvmapForCons iClass cons = do
+    let numNbs = fromEnum iClass
 
     value      <- newName "value"
     covMaps    <- newNameList "covMap" numNbs
     contraMaps <- newNameList "contraMap" numNbs
 
-    let tvis     = zip3 nbs covMaps contraMaps
-        iClass   = toEnum numNbs
+    let mapFuns  = zip covMaps contraMaps
         argNames = concat (transpose [covMaps, contraMaps]) ++ [value]
     lamE (map varP argNames)
         . appsE
@@ -287,37 +271,26 @@
                then appE (varE errorValName)
                          (stringE $ "Void " ++ nameBase (invmapName iClass))
                else caseE (varE value)
-                          (map (makeInvmapForCon iClass tvis) cons)
+                          (map (makeInvmapForCon iClass mapFuns) cons)
           ] ++ map varE argNames
 
 -- | Generates a lambda expression for invmap(2) for a single constructor.
-makeInvmapForCon :: InvariantClass -> [TyVarInfo] -> Con -> Q Match
-makeInvmapForCon iClass tvis (NormalC conName tys) = do
-    args <- newNameList "arg" $ length tys
-    let argTys = map snd tys
-    makeInvmapForArgs iClass tvis conName argTys args
-makeInvmapForCon iClass tvis (RecC conName tys) = do
-    args <- newNameList "arg" $ length tys
-    let argTys = map thd3 tys
-    makeInvmapForArgs iClass tvis conName argTys args
-makeInvmapForCon iClass tvis (InfixC (_, argTyL) conName (_, argTyR)) = do
-    argL <- newName "argL"
-    argR <- newName "argR"
-    makeInvmapForArgs iClass tvis conName [argTyL, argTyR] [argL, argR]
-makeInvmapForCon iClass tvis (ForallC tvbs faCxt con) =
-    if any (`predMentionsNameBase` map fst3 tvis) faCxt
-       then existentialContextError $ constructorName con
-       else makeInvmapForCon iClass (removeForalled tvbs tvis) con
+makeInvmapForCon :: InvariantClass -> [(Name, Name)] -> Con -> Q Match
+makeInvmapForCon iClass mapFuns con = do
+    let conName = constructorName con
+    (ts, tvMap) <- reifyConTys iClass conName mapFuns
+    argNames    <- newNameList "arg" $ length ts
+    makeInvmapForArgs iClass tvMap conName ts argNames
 
 makeInvmapForArgs :: InvariantClass
-                  -> [TyVarInfo]
+                  -> TyVarMap
                   -> Name
                   -> [Type]
                   -> [Name]
                   ->  Q Match
-makeInvmapForArgs iClass tvis conName tys args =
+makeInvmapForArgs iClass tvMap conName tys args =
     let mappedArgs :: [Q Exp]
-        mappedArgs = zipWith (makeInvmapForArg iClass conName tvis) tys args
+        mappedArgs = zipWith (makeInvmapForArg iClass conName tvMap) tys args
      in match (conP conName $ map varP args)
               (normalB . appsE $ conE conName:mappedArgs)
               []
@@ -325,45 +298,33 @@
 -- | Generates a lambda expression for invmap(2) for an argument of a constructor.
 makeInvmapForArg :: InvariantClass
                  -> Name
-                 -> [TyVarInfo]
+                 -> TyVarMap
                  -> Type
                  -> Name
                  -> Q Exp
-makeInvmapForArg iClass conName tvis ty tyExpName = do
-    ty' <- expandSyn ty
-    makeInvmapForArg' iClass conName tvis ty' tyExpName
-
--- | Generates a lambda expression for invmap(2) for an argument of a
--- constructor, after expanding all type synonyms.
-makeInvmapForArg' :: InvariantClass
-                  -> Name
-                  -> [TyVarInfo]
-                  -> Type
-                  -> Name
-                  -> Q Exp
-makeInvmapForArg' iClass conName tvis ty tyExpName =
+makeInvmapForArg iClass conName tvis ty tyExpName =
     appE (makeInvmapForType iClass conName tvis True ty) (varE tyExpName)
 
 -- | Generates a lambda expression for invmap(2) for a specific type.
 -- The generated expression depends on the number of type variables.
 makeInvmapForType :: InvariantClass
                   -> Name
-                  -> [TyVarInfo]
+                  -> TyVarMap
                   -> Bool
                   -> Type
                   -> Q Exp
-makeInvmapForType _ _ tvis covariant (VarT tyName) =
-    case lookup2 (NameBase tyName) tvis of
+makeInvmapForType _ _ tvMap covariant (VarT tyName) =
+    case Map.lookup tyName tvMap of
          Just (covMap, contraMap) ->
              varE $ if covariant then covMap else contraMap
          Nothing -> do -- Produce a lambda expression rather than id, addressing Trac #7436
              x <- newName "x"
              lamE [varP x] $ varE x
-makeInvmapForType iClass conName tvis covariant (SigT ty _) =
-    makeInvmapForType iClass conName tvis covariant ty
-makeInvmapForType iClass conName tvis covariant (ForallT tvbs _ ty)
-    = makeInvmapForType iClass conName (removeForalled tvbs tvis) covariant ty
-makeInvmapForType iClass conName tvis covariant ty =
+makeInvmapForType iClass conName tvMap covariant (SigT ty _) =
+    makeInvmapForType iClass conName tvMap covariant ty
+makeInvmapForType iClass conName tvMap covariant (ForallT _ _ ty)
+    = makeInvmapForType iClass conName tvMap covariant ty
+makeInvmapForType iClass conName tvMap covariant ty =
     let tyCon  :: Type
         tyArgs :: [Type]
         tyCon:tyArgs = unapplyTy ty
@@ -374,19 +335,19 @@
         lhsArgs, rhsArgs :: [Type]
         (lhsArgs, rhsArgs) = splitAt (length tyArgs - numLastArgs) tyArgs
 
-        tyVarNameBases :: [NameBase]
-        tyVarNameBases = map fst3 tvis
+        tyVarNames :: [Name]
+        tyVarNames = Map.keys tvMap
 
         doubleMap :: (Bool -> Type -> Q Exp) -> [Type] -> [Q Exp]
         doubleMap _ []     = []
         doubleMap f (t:ts) = f covariant t : f (not covariant) t : doubleMap f ts
 
         mentionsTyArgs :: Bool
-        mentionsTyArgs = any (`mentionsNameBase` tyVarNameBases) tyArgs
+        mentionsTyArgs = any (`mentionsName` tyVarNames) tyArgs
 
         makeInvmapTuple :: Type -> Name -> Q Exp
         makeInvmapTuple fieldTy fieldName =
-            appE (makeInvmapForType iClass conName tvis covariant fieldTy) $ varE fieldName
+            appE (makeInvmapForType iClass conName tvMap covariant fieldTy) $ varE fieldName
 
      in case tyCon of
              ArrowT | mentionsTyArgs ->
@@ -394,8 +355,8 @@
                   in do x <- newName "x"
                         b <- newName "b"
                         lamE [varP x, varP b] $
-                          makeInvmapForType iClass conName tvis covariant resTy `appE` (varE x `appE`
-                            (makeInvmapForType iClass conName tvis (not covariant) argTy `appE` varE b))
+                          makeInvmapForType iClass conName tvMap covariant resTy `appE` (varE x `appE`
+                            (makeInvmapForType iClass conName tvMap (not covariant) argTy `appE` varE b))
              TupleT n | n > 0 && mentionsTyArgs -> do
                  x  <- newName "x"
                  xs <- newNameList "x" n
@@ -406,12 +367,12 @@
                      ]
              _ -> do
                  itf <- isTyFamily tyCon
-                 if any (`mentionsNameBase` tyVarNameBases) lhsArgs || (itf && mentionsTyArgs)
-                      then outOfPlaceTyVarError conName tyVarNameBases
-                      else if any (`mentionsNameBase` tyVarNameBases) rhsArgs
+                 if any (`mentionsName` tyVarNames) lhsArgs || (itf && mentionsTyArgs)
+                      then outOfPlaceTyVarError conName tyVarNames
+                      else if any (`mentionsName` tyVarNames) rhsArgs
                            then appsE $
                                 ( varE (invmapName (toEnum numLastArgs))
-                                : doubleMap (makeInvmapForType iClass conName tvis) rhsArgs
+                                : doubleMap (makeInvmapForType iClass conName tvMap) rhsArgs
                                 )
                            else do x <- newName "x"
                                    lamE [varP x] $ varE x
@@ -437,8 +398,16 @@
   case info of
     TyConI dec ->
       case dec of
-        DataD    ctxt _ tvbs cons _ -> f name ctxt tvbs cons Nothing
-        NewtypeD ctxt _ tvbs con  _ -> f name ctxt tvbs [con] Nothing
+        DataD ctxt _ tvbs
+#if MIN_VERSION_template_haskell(2,11,0)
+              _
+#endif
+              cons _ -> f name ctxt tvbs cons Nothing
+        NewtypeD ctxt _ tvbs
+#if MIN_VERSION_template_haskell(2,11,0)
+                 _
+#endif
+                 con _ -> f name ctxt tvbs [con] Nothing
         _ -> error $ ns ++ "Unsupported type: " ++ show dec
 #if MIN_VERSION_template_haskell(2,7,0)
 # if MIN_VERSION_template_haskell(2,11,0)
@@ -454,13 +423,29 @@
         FamilyI (FamilyD DataFam _ tvbs _) decs ->
 # endif
           let instDec = flip find decs $ \dec -> case dec of
-                DataInstD    _ _ _ cons _ -> any ((name ==) . constructorName) cons
-                NewtypeInstD _ _ _ con  _ -> name == constructorName con
+                DataInstD _ _ _
+# if MIN_VERSION_template_haskell(2,11,0)
+                          _
+# endif
+                          cons _ -> any ((name ==) . constructorName) cons
+                NewtypeInstD _ _ _
+# if MIN_VERSION_template_haskell(2,11,0)
+                             _
+# endif
+                             con _ -> name == constructorName con
                 _ -> error $ ns ++ "Must be a data or newtype instance."
            in case instDec of
-                Just (DataInstD    ctxt _ instTys cons _)
+                Just (DataInstD ctxt _ instTys
+# if MIN_VERSION_template_haskell(2,11,0)
+                                _
+# endif
+                                cons _)
                   -> f parentName ctxt tvbs cons $ Just instTys
-                Just (NewtypeInstD ctxt _ instTys con  _)
+                Just (NewtypeInstD ctxt _ instTys
+# if MIN_VERSION_template_haskell(2,11,0)
+                                   _
+# endif
+                                   con _)
                   -> f parentName ctxt tvbs [con] $ Just instTys
                 _ -> error $ ns ++
                   "Could not find data or newtype instance constructor."
@@ -483,8 +468,7 @@
     ns :: String
     ns = "Data.Functor.Invariant.TH.withType: "
 
--- | Deduces the instance context, instance head, and eta-reduced type variables
--- for an instance.
+-- | Deduces the instance context and head for an instance.
 buildTypeInstance :: InvariantClass
                   -- ^ Invariant or Invariant2
                   -> Name
@@ -496,160 +480,342 @@
                   -> Maybe [Type]
                   -- ^ 'Just' the types used to instantiate a data family instance,
                   -- or 'Nothing' if it's a plain data type
-                  -> (Cxt, Type, [NameBase])
+                  -> Q (Cxt, Type)
 -- Plain data type/newtype case
 buildTypeInstance iClass tyConName dataCxt tvbs Nothing =
-    if remainingLength < 0 || not (wellKinded droppedKinds) -- If we have enough well-kinded type variables
-       then derivingKindError iClass tyConName
-    else if any (`predMentionsNameBase` droppedNbs) dataCxt -- If the last type variable(s) are mentioned in a datatype context
-       then datatypeContextError tyConName instanceType
-    else (instanceCxt, instanceType, droppedNbs)
-  where
-    instanceCxt :: Cxt
-    instanceCxt = map (applyInvariantConstraint)
-                $ filter (needsConstraint iClass . tvbKind) remaining
+    let varTys :: [Type]
+        varTys = map tvbToType tvbs
+    in buildTypeInstanceFromTys iClass tyConName dataCxt varTys False
+-- Data family instance case
+--
+-- The CPP is present to work around a couple of annoying old GHC bugs.
+-- See Note [Polykinded data families in Template Haskell]
+buildTypeInstance iClass parentName dataCxt tvbs (Just instTysAndKinds) = do
+#if !(MIN_VERSION_template_haskell(2,8,0)) || MIN_VERSION_template_haskell(2,10,0)
+    let instTys :: [Type]
+        instTys = zipWith stealKindForType tvbs instTysAndKinds
+#else
+    let kindVarNames :: [Name]
+        kindVarNames = nub $ concatMap (tyVarNamesOfType . tvbKind) tvbs
 
-    instanceType :: Type
-    instanceType = AppT (ConT $ invariantClassName iClass)
-                 . applyTyCon tyConName
-                 $ map (VarT . tvbName) remaining
+        numKindVars :: Int
+        numKindVars = length kindVarNames
 
-    remainingLength :: Int
-    remainingLength = length tvbs - fromEnum iClass
+        givenKinds, givenKinds' :: [Kind]
+        givenTys                :: [Type]
+        (givenKinds, givenTys) = splitAt numKindVars instTysAndKinds
+        givenKinds' = map sanitizeStars givenKinds
 
-    remaining, dropped :: [TyVarBndr]
-    (remaining, dropped) = splitAt remainingLength tvbs
+        -- A GHC 7.6-specific bug requires us to replace all occurrences of
+        -- (ConT GHC.Prim.*) with StarT, or else Template Haskell will reject it.
+        -- Luckily, (ConT GHC.Prim.*) only seems to occur in this one spot.
+        sanitizeStars :: Kind -> Kind
+        sanitizeStars = go
+          where
+            go :: Kind -> Kind
+            go (AppT t1 t2)                 = AppT (go t1) (go t2)
+            go (SigT t k)                   = SigT (go t) (go k)
+            go (ConT n) | n == starKindName = StarT
+            go t                            = t
 
-    droppedKinds :: [Kind]
-    droppedKinds = map tvbKind dropped
+    -- If we run this code with GHC 7.8, we might have to generate extra type
+    -- variables to compensate for any type variables that Template Haskell
+    -- eta-reduced away.
+    -- See Note [Polykinded data families in Template Haskell]
+    xTypeNames <- newNameList "tExtra" (length tvbs - length givenTys)
 
-    droppedNbs :: [NameBase]
-    droppedNbs = map (NameBase . tvbName) dropped
--- Data family instance case
-buildTypeInstance iClass parentName dataCxt tvbs (Just instTysAndKinds) =
-    if remainingLength < 0 || not (wellKinded droppedKinds) -- If we have enough well-kinded type variables
-       then derivingKindError iClass parentName
-    else if any (`predMentionsNameBase` droppedNbs) dataCxt -- If the last type variable(s) are mentioned in a datatype context
-       then datatypeContextError parentName instanceType
-    else if canEtaReduce remaining dropped -- If it is safe to drop the type variables
-       then (instanceCxt, instanceType, droppedNbs)
-    else etaReductionError instanceType
-  where
-    instanceCxt :: Cxt
-    instanceCxt = map (applyInvariantConstraint)
-                $ filter (needsConstraint iClass . tvbKind) lhsTvbs
+    let xTys   :: [Type]
+        xTys = map VarT xTypeNames
+        -- ^ Because these type variables were eta-reduced away, we can only
+        --   determine their kind by using stealKindForType. Therefore, we mark
+        --   them as VarT to ensure they will be given an explicit kind annotation
+        --   (and so the kind inference machinery has the right information).
 
-    -- We need to make sure that type variables in the instance head which have
-    -- Invariant(2) constraints aren't poly-kinded, e.g.,
-    --
-    -- @
-    -- instance Invariant f => Invariant (Foo (f :: k)) where
-    -- @
-    --
-    -- To do this, we remove every kind ascription (i.e., strip off every 'SigT').
-    instanceType :: Type
-    instanceType = AppT (ConT $ invariantClassName iClass)
-                 . applyTyCon parentName
-                 $ map unSigT remaining
+        substNamesWithKinds :: [(Name, Kind)] -> Type -> Type
+        substNamesWithKinds nks t = foldr' (uncurry substNameWithKind) t nks
 
-    remainingLength :: Int
-    remainingLength = length tvbs - fromEnum iClass
+        -- The types from the data family instance might not have explicit kind
+        -- annotations, which the kind machinery needs to work correctly. To
+        -- compensate, we use stealKindForType to explicitly annotate any
+        -- types without kind annotations.
+        instTys :: [Type]
+        instTys = map (substNamesWithKinds (zip kindVarNames givenKinds'))
+                  -- ^ Note that due to a GHC 7.8-specific bug
+                  --   (see Note [Polykinded data families in Template Haskell]),
+                  --   there may be more kind variable names than there are kinds
+                  --   to substitute. But this is OK! If a kind is eta-reduced, it
+                  --   means that is was not instantiated to something more specific,
+                  --   so we need not substitute it. Using stealKindForType will
+                  --   grab the correct kind.
+                $ zipWith stealKindForType tvbs (givenTys ++ xTys)
+#endif
+    buildTypeInstanceFromTys iClass parentName dataCxt instTys True
 
-    remaining, dropped :: [Type]
-    (remaining, dropped) = splitAt remainingLength rhsTypes
+-- For the given Types, generate an instance context and head. Coming up with
+-- the instance type isn't as simple as dropping the last types, as you need to
+-- be wary of kinds being instantiated with *.
+-- See Note [Type inference in derived instances]
+buildTypeInstanceFromTys :: InvariantClass
+                         -- ^ Invariant or Invariant2
+                         -> Name
+                         -- ^ The type constructor or data family name
+                         -> Cxt
+                         -- ^ The datatype context
+                         -> [Type]
+                         -- ^ The types to instantiate the instance with
+                         -> Bool
+                         -- ^ True if it's a data family, False otherwise
+                         -> Q (Cxt, Type)
+buildTypeInstanceFromTys iClass tyConName dataCxt varTysOrig isDataFamily = do
+    -- Make sure to expand through type/kind synonyms! Otherwise, the
+    -- eta-reduction check might get tripped up over type variables in a
+    -- synonym that are actually dropped.
+    -- (See GHC Trac #11416 for a scenario where this actually happened.)
+    varTysExp <- mapM expandSyn varTysOrig
 
-    droppedKinds :: [Kind]
-    droppedKinds = map tvbKind . snd $ splitAt remainingLength tvbs
+    let remainingLength :: Int
+        remainingLength = length varTysOrig - fromEnum iClass
 
-    droppedNbs :: [NameBase]
-    droppedNbs = map varTToNameBase dropped
+        droppedTysExp :: [Type]
+        droppedTysExp = drop remainingLength varTysExp
 
-    -- We need to be mindful of an old GHC bug which causes kind variables to appear in
-    -- @instTysAndKinds@ (as the name suggests) if
-    --
-    --   (1) @PolyKinds@ is enabled
-    --   (2) either GHC 7.6 or 7.8 is being used (for more info, see
-    --       https://ghc.haskell.org/trac/ghc/ticket/9692).
-    --
-    -- Since Template Haskell doesn't seem to have a mechanism for detecting which
-    -- language extensions are enabled, we do the next-best thing by counting
-    -- the number of distinct kind variables in the data family declaration, and
-    -- then dropping that number of entries from @instTysAndKinds@.
-    instTypes :: [Type]
-    instTypes =
-#if __GLASGOW_HASKELL__ >= 710 || !(MIN_VERSION_template_haskell(2,8,0))
-        instTysAndKinds
-#else
-        drop (Set.size . Set.unions $ map (distinctKindVars . tvbKind) tvbs)
-             instTysAndKinds
-#endif
+        droppedStarKindStati :: [StarKindStatus]
+        droppedStarKindStati = map canRealizeKindStar droppedTysExp
 
-    lhsTvbs :: [TyVarBndr]
-    lhsTvbs = map (uncurry replaceTyVarName)
-            . filter (isTyVar . snd)
-            . take remainingLength
-            $ zip tvbs rhsTypes
+    -- Check there are enough types to drop and that all of them are either of
+    -- kind * or kind k (for some kind variable k). If not, throw an error.
+    when (remainingLength < 0 || any (== NotKindStar) droppedStarKindStati) $
+      derivingKindError iClass tyConName
 
-    -- In GHC 7.8, only the @Type@s up to the rightmost non-eta-reduced type variable
-    -- in @instTypes@ are provided (as a result of this extremely annoying bug:
-    -- https://ghc.haskell.org/trac/ghc/ticket/9692). This is pretty inconvenient,
-    -- as it makes it impossible to come up with the correct Invariant(2)
-    -- instances in some cases. For example, consider the following code:
-    --
-    -- @
-    -- data family Foo a b c
-    -- data instance Foo Int y z = Foo Int y z
-    -- $(deriveInvariant2 'Foo)
-    -- @
-    --
-    -- Due to the aformentioned bug, Template Haskell doesn't tell us the names of
-    -- either of type variables in the data instance (@y@ and @z@). As a result, we
-    -- won't know which fields of the 'Foo' constructor to apply the map functions,
-    -- which will result in an incorrect instance. Urgh.
-    --
-    -- A workaround is to ensure that you use the exact same type variables, in the
-    -- exact same order, in the data family declaration and any data or newtype
-    -- instances:
-    --
-    -- @
-    -- data family Foo a b c
-    -- data instance Foo Int b c = Foo Int b c
-    -- $(deriveInvariant2 'Foo)
-    -- @
-    --
-    -- Thankfully, other versions of GHC don't seem to have this bug.
-    rhsTypes :: [Type]
-    rhsTypes =
-#if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710
-            instTypes ++ map tvbToType
-                             (drop (length instTypes)
-                                   tvbs)
-#else
-            instTypes
-#endif
+    let droppedKindVarNames :: [Name]
+        droppedKindVarNames = catKindVarNames droppedStarKindStati
 
--- | Given a TyVarBndr, apply an Invariant(2) constraint to it, depending
--- on its kind.
-applyInvariantConstraint :: TyVarBndr -> Pred
-applyInvariantConstraint PlainTV{}            = error "Cannot constrain type of kind *"
-applyInvariantConstraint (KindedTV name kind) = applyClass className name
-  where
-    className :: Name
-    className = invariantClassName . toEnum $ numKindArrows kind
+        -- Substitute kind * for any dropped kind variables
+        varTysExpSubst :: [Type]
+        varTysExpSubst = map (substNamesWithKindStar droppedKindVarNames) varTysExp
 
--- | Can a kind signature inhabit an Invariant constraint?
+        remainingTysExpSubst, droppedTysExpSubst :: [Type]
+        (remainingTysExpSubst, droppedTysExpSubst) =
+          splitAt remainingLength varTysExpSubst
+
+        -- All of the type variables mentioned in the dropped types
+        -- (post-synonym expansion)
+        droppedTyVarNames :: [Name]
+        droppedTyVarNames = concatMap tyVarNamesOfType droppedTysExpSubst
+
+    -- If any of the dropped types were polykinded, ensure that there are of kind *
+    -- after substituting * for the dropped kind variables. If not, throw an error.
+    unless (all hasKindStar droppedTysExpSubst) $
+      derivingKindError iClass tyConName
+
+    let preds    :: [Maybe Pred]
+        kvNames  :: [[Name]]
+        kvNames' :: [Name]
+        -- Derive instance constraints (and any kind variables which are specialized
+        -- to * in those constraints)
+        (preds, kvNames) = unzip $ map (deriveConstraint iClass) remainingTysExpSubst
+        kvNames' = concat kvNames
+
+        -- Substitute the kind variables specialized in the constraints with *
+        remainingTysExpSubst' :: [Type]
+        remainingTysExpSubst' =
+          map (substNamesWithKindStar kvNames') remainingTysExpSubst
+
+        -- We now substitute all of the specialized-to-* kind variable names with
+        -- *, but in the original types, not the synonym-expanded types. The reason
+        -- we do this is a superficial one: we want the derived instance to resemble
+        -- the datatype written in source code as closely as possible. For example,
+        -- for the following data family instance:
+        --
+        --   data family Fam a
+        --   newtype instance Fam String = Fam String
+        --
+        -- We'd want to generate the instance:
+        --
+        --   instance C (Fam String)
+        --
+        -- Not:
+        --
+        --   instance C (Fam [Char])
+        remainingTysOrigSubst :: [Type]
+        remainingTysOrigSubst =
+          map (substNamesWithKindStar (union droppedKindVarNames kvNames'))
+            $ take remainingLength varTysOrig
+
+        remainingTysOrigSubst' :: [Type]
+        -- See Note [Kind signatures in derived instances] for an explanation
+        -- of the isDataFamily check.
+        remainingTysOrigSubst' =
+          if isDataFamily
+             then remainingTysOrigSubst
+             else map unSigT remainingTysOrigSubst
+
+        instanceCxt :: Cxt
+        instanceCxt = catMaybes preds
+
+        instanceType :: Type
+        instanceType = AppT (ConT $ invariantClassName iClass)
+                     $ applyTyCon tyConName remainingTysOrigSubst'
+
+    -- If the datatype context mentions any of the dropped type variables,
+    -- we can't derive an instance, so throw an error.
+    when (any (`predMentionsName` droppedTyVarNames) dataCxt) $
+      datatypeContextError tyConName instanceType
+    -- Also ensure the dropped types can be safely eta-reduced. Otherwise,
+    -- throw an error.
+    unless (canEtaReduce remainingTysExpSubst' droppedTysExpSubst) $
+      etaReductionError instanceType
+    return (instanceCxt, instanceType)
+
+-- | Attempt to derive a constraint on a Type. If successful, return
+-- Just the constraint and any kind variable names constrained to *.
+-- Otherwise, return Nothing and the empty list.
 --
--- Invariant:  Kind k1 -> k2
--- Invariant2: Kind k1 -> k2 -> k3
-needsConstraint :: InvariantClass -> Kind -> Bool
-needsConstraint iClass kind =
-       fromEnum iClass >= nka
-    && nka >= fromEnum Invariant
-    && canRealizeKindStarChain kind
+-- See Note [Type inference in derived instances] for the heuristics used to
+-- come up with constraints.
+deriveConstraint :: InvariantClass -> Type -> (Maybe Pred, [Name])
+deriveConstraint iClass t
+  | not (isTyVar t) = (Nothing, [])
+  | otherwise = case hasKindVarChain 1 t of
+      Just ns | iClass >= Invariant
+              -> (Just (applyClass invariantTypeName tName), ns)
+      _ -> case hasKindVarChain 2 t of
+                Just ns | iClass == Invariant2
+                        -> (Just (applyClass invariant2TypeName tName), ns)
+                _       -> (Nothing, [])
   where
-   nka :: Int
-   nka = numKindArrows kind
+    tName :: Name
+    tName = varTToName t
 
+{-
+Note [Polykinded data families in Template Haskell]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In order to come up with the correct instance context and head for an instance, e.g.,
+  instance C a => C (Data a) where ...
+We need to know the exact types and kinds used to instantiate the instance. For
+plain old datatypes, this is simple: every type must be a type variable, and
+Template Haskell reliably tells us the type variables and their kinds.
+Doing the same for data families proves to be much harder for three reasons:
+1. On any version of Template Haskell, it may not tell you what an instantiated
+   type's kind is. For instance, in the following data family instance:
+     data family Fam (f :: * -> *) (a :: *)
+     data instance Fam f a
+   Then if we use TH's reify function, it would tell us the TyVarBndrs of the
+   data family declaration are:
+     [KindedTV f (AppT (AppT ArrowT StarT) StarT),KindedTV a StarT]
+   and the instantiated types of the data family instance are:
+     [VarT f1,VarT a1]
+   We can't just pass [VarT f1,VarT a1] to buildTypeInstanceFromTys, since we
+   have no way of knowing their kinds. Luckily, the TyVarBndrs tell us what the
+   kind is in case an instantiated type isn't a SigT, so we use the stealKindForType
+   function to ensure all of the instantiated types are SigTs before passing them
+   to buildTypeInstanceFromTys.
+2. On GHC 7.6 and 7.8, a bug is present in which Template Haskell lists all of
+   the specified kinds of a data family instance efore any of the instantiated
+   types. Fortunately, this is easy to deal with: you simply count the number of
+   distinct kind variables in the data family declaration, take that many elements
+   from the front of the  Types list of the data family instance, substitute the
+   kind variables with their respective instantiated kinds (which you took earlier),
+   and proceed as normal.
+3. On GHC 7.8, an even uglier bug is present (GHC Trac #9692) in which Template
+   Haskell might not even list all of the Types of a data family instance, since
+   they are eta-reduced away! And yes, kinds can be eta-reduced too.
+   The simplest workaround is to count how many instantiated types are missing from
+   the list and generate extra type variables to use in their place. Luckily, we
+   needn't worry much if its kind was eta-reduced away, since using stealKindForType
+   will get it back.
+Note [Kind signatures in derived instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is possible to put explicit kind signatures into the derived instances, e.g.,
+  instance C a => C (Data (f :: * -> *)) where ...
+But it is preferable to avoid this if possible. If we come up with an incorrect
+kind signature (which is entirely possible, since our type inferencer is pretty
+unsophisticated - see Note [Type inference in derived instances]), then GHC will
+flat-out reject the instance, which is quite unfortunate.
+Plain old datatypes have the advantage that you can avoid using any kind signatures
+at all in their instances. This is because a datatype declaration uses all type
+variables, so the types that we use in a derived instance uniquely determine their
+kinds. As long as we plug in the right types, the kind inferencer can do the rest
+of the work. For this reason, we use unSigT to remove all kind signatures before
+splicing in the instance context and head.
+Data family instances are trickier, since a data family can have two instances that
+are distinguished by kind alone, e.g.,
+  data family Fam (a :: k)
+  data instance Fam (a :: * -> *)
+  data instance Fam (a :: *)
+If we dropped the kind signatures for C (Fam a), then GHC will have no way of
+knowing which instance we are talking about. To avoid this scenario, we always
+include explicit kind signatures in data family instances. There is a chance that
+the inferred kind signatures will be incorrect, but if so, we can always fall back
+on the make- functions.
+Note [Type inference in derived instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type inference is can be tricky to get right, and we want to avoid recreating the
+entirety of GHC's type inferencer in Template Haskell. For this reason, we will
+probably never come up with derived instance contexts that are as accurate as
+GHC's. But that doesn't mean we can't do anything! There are a couple of simple
+things we can do to make instance contexts that work for 80% of use cases:
+1. If one of the last type parameters is polykinded, then its kind will be
+   specialized to * in the derived instance. We note what kind variable the type
+   parameter had and substitute it with * in the other types as well. For example,
+   imagine you had
+     data Data (a :: k) (b :: k) (c :: k)
+   Then you'd want to derived instance to be:
+     instance C (Data (a :: *))
+   Not:
+     instance C (Data (a :: k))
+2. We naïvely come up with instance constraints using the following criteria:
+   (i)  If there's a type parameter n of kind k1 -> k2 (where k1/k2 are * or kind
+        variables), then generate an Invariant n constraint, and if k1/k2 are kind
+        variables, then substitute k1/k2 with * elsewhere in the types. We must
+        consider the case where they are kind variables because you might have a
+        scenario like this:
+          newtype Compose (f :: k3 -> *) (g :: k1 -> k2 -> k3) (a :: k1) (b :: k2)
+            = Compose (f (g a b))
+        Which would have a derived Invariant2 instance of:
+          instance (Invariant f, Invariant2 g) => Invariant2 (Compose f g) where ...
+   (ii) If there's a type parameter n of kind k1 -> k2 -> k3 (where k1/k2/k3 are
+        * or kind variables), then generate a Invariant2 n constraint and perform
+        kind substitution as in the other case.
+-}
+
+-- Determines the types of a constructor's arguments as well as the last type
+-- parameters (along with their map functions), expanding through any type synonyms.
+-- The type parameters are determined on a constructor-by-constructor basis since
+-- they may be refined to be particular types in a GADT.
+reifyConTys :: InvariantClass
+            -> Name
+            -> [(Name, Name)]
+            -> Q ([Type], TyVarMap)
+reifyConTys iClass conName maps = do
+    info          <- reify conName
+    (ctxt, uncTy) <- case info of
+        DataConI _ ty _
+#if !(MIN_VERSION_template_haskell(2,11,0))
+                 _
+#endif
+                 -> fmap uncurryTy (expandSyn ty)
+        _ -> error "Must be a data constructor"
+    let (argTys, [resTy]) = splitAt (length uncTy - 1) uncTy
+        unapResTy = unapplyTy resTy
+        numToDrop = fromEnum iClass
+        -- If one of the last type variables is refined to a particular type
+        -- (i.e., not truly polymorphic), we mark it with Nothing and filter
+        -- it out later, since we only apply map functions to arguments of
+        -- a type that is (1) one of the last type variables, and (2)
+        -- of a truly polymorphic type.
+        mbTvNames = map varTToName_maybe $
+                        drop (length unapResTy - numToDrop) unapResTy
+        tvMap = Map.fromList
+                    . catMaybes -- Drop refined types
+                    $ zipWith (\mbTvName mapFuns ->
+                                  fmap (\tvName -> (tvName, mapFuns)) mbTvName)
+                              mbTvNames maps
+    if any (`predMentionsName` Map.keys tvMap) ctxt
+         || Map.size tvMap < numToDrop
+       then existentialContextError conName
+       else return (argTys, tvMap)
+
 -------------------------------------------------------------------------------
 -- Error messages
 -------------------------------------------------------------------------------
@@ -696,14 +862,13 @@
 
 -- | The data type mentions one of the n eta-reduced type variables in a place other
 -- than the last nth positions of a data type in a constructor's field.
-outOfPlaceTyVarError :: Name -> [NameBase] -> a
-outOfPlaceTyVarError conName tyVarNames = error
-    . showString "Constructor ‘"
-    . showString (nameBase conName)
-    . showString "‘ must use the type variable(s) "
-    . showsPrec 0 tyVarNames
-    . showString " only in the last argument(s) of a data type"
-    $ ""
+outOfPlaceTyVarError :: Name -> a
+outOfPlaceTyVarError conName = error
+  . showString "Constructor ‘"
+  . showString (nameBase conName)
+  . showString "‘ must only use its last two type variable(s) within"
+  . showString " the last two argument(s) of a data type"
+  $ ""
 
 -- | One of the last type variables cannot be eta-reduced (see the canEtaReduce
 -- function for the criteria it would have to meet).
diff --git a/src/Data/Functor/Invariant/TH/Internal.hs b/src/Data/Functor/Invariant/TH/Internal.hs
--- a/src/Data/Functor/Invariant/TH/Internal.hs
+++ b/src/Data/Functor/Invariant/TH/Internal.hs
@@ -11,10 +11,13 @@
 -}
 module Data.Functor.Invariant.TH.Internal where
 
-import           Data.Function (on)
+import           Control.Monad (liftM)
+
+import           Data.Foldable (foldr')
 import           Data.List
-import qualified Data.Map as Map (fromList, findWithDefault)
+import qualified Data.Map as Map (fromList, findWithDefault, singleton)
 import           Data.Map (Map)
+import           Data.Maybe (fromMaybe, mapMaybe)
 import qualified Data.Set as Set
 import           Data.Set (Set)
 
@@ -36,9 +39,18 @@
 expandSyn (ForallT tvs ctx t) = fmap (ForallT tvs ctx) $ expandSyn t
 expandSyn t@AppT{}            = expandSynApp t []
 expandSyn t@ConT{}            = expandSynApp t []
-expandSyn (SigT t _)          = expandSyn t   -- Ignore kind synonyms
+expandSyn (SigT t k)          = do t' <- expandSyn t
+                                   k' <- expandSynKind k
+                                   return (SigT t' k')
 expandSyn t                   = return t
 
+expandSynKind :: Kind -> Q Kind
+#if MIN_VERSION_template_haskell(2,8,0)
+expandSynKind = expandSyn
+#else
+expandSynKind = return -- There are no kind synonyms to deal with
+#endif
+
 expandSynApp :: Type -> [Type] -> Q Type
 expandSynApp (AppT t1 t2) ts = do
     t2' <- expandSyn t2
@@ -50,29 +62,48 @@
         TyConI (TySynD _ tvs rhs) ->
             let (ts', ts'') = splitAt (length tvs) ts
                 subs = mkSubst tvs ts'
-                rhs' = subst subs rhs
+                rhs' = substType subs rhs
              in expandSynApp rhs' ts''
         _ -> return $ foldl' AppT t ts
 expandSynApp t ts = do
     t' <- expandSyn t
     return $ foldl' AppT t' ts
 
-type Subst = Map Name Type
+type TypeSubst = Map Name Type
+type KindSubst = Map Name Kind
 
-mkSubst :: [TyVarBndr] -> [Type] -> Subst
+mkSubst :: [TyVarBndr] -> [Type] -> TypeSubst
 mkSubst vs ts =
    let vs' = map un vs
        un (PlainTV v)    = v
        un (KindedTV v _) = v
    in Map.fromList $ zip vs' ts
 
-subst :: Subst -> Type -> Type
-subst subs (ForallT v c t) = ForallT v c $ subst subs t
-subst subs t@(VarT n)      = Map.findWithDefault t n subs
-subst subs (AppT t1 t2)    = AppT (subst subs t1) (subst subs t2)
-subst subs (SigT t k)      = SigT (subst subs t) k
-subst _ t                  = t
+substType :: TypeSubst -> Type -> Type
+substType subs (ForallT v c t) = ForallT v c $ substType subs t
+substType subs t@(VarT n)      = Map.findWithDefault t n subs
+substType subs (AppT t1 t2)    = AppT (substType subs t1) (substType subs t2)
+substType subs (SigT t k)      = SigT (substType subs t)
+#if MIN_VERSION_template_haskell(2,8,0)
+                                      (substType subs k)
+#else
+                                      k
+#endif
+substType _ t                  = t
 
+substKind :: KindSubst -> Type -> Type
+#if MIN_VERSION_template_haskell(2,8,0)
+substKind = substType
+#else
+substKind _ = id -- There are no kind variables!
+#endif
+
+substNameWithKind :: Name -> Kind -> Type -> Type
+substNameWithKind n k = substKind (Map.singleton n k)
+
+substNamesWithKindStar :: [Name] -> Type -> Type
+substNamesWithKindStar ns t = foldr' (flip substNameWithKind starK) t ns
+
 -------------------------------------------------------------------------------
 -- Class-specific constants
 -------------------------------------------------------------------------------
@@ -118,41 +149,115 @@
 {-# INLINE invmap2Const #-}
 
 -------------------------------------------------------------------------------
--- NameBase
+-- StarKindStatus
 -------------------------------------------------------------------------------
 
--- | A wrapper around Name which only uses the 'nameBase' (not the entire Name)
--- to compare for equality. For example, if you had two Names a_123 and a_456,
--- they are not equal as Names, but they are equal as NameBases.
---
--- This is useful when inspecting type variables, since a type variable in an
--- instance context may have a distinct Name from a type variable within an
--- actual constructor declaration, but we'd want to treat them as the same
--- if they have the same 'nameBase' (since that's what the programmer uses to
--- begin with).
-newtype NameBase = NameBase { getName :: Name }
-
-getNameBase :: NameBase -> String
-getNameBase = nameBase . getName
-
-instance Eq NameBase where
-    (==) = (==) `on` getNameBase
+-- | Whether a type is not of kind *, is of kind *, or is a kind variable.
+data StarKindStatus = NotKindStar
+                    | KindStar
+                    | IsKindVar Name
+  deriving Eq
 
-instance Ord NameBase where
-    compare = compare `on` getNameBase
+-- | Does a Type have kind * or k (for some kind variable k)?
+canRealizeKindStar :: Type -> StarKindStatus
+canRealizeKindStar t
+  | hasKindStar t = KindStar
+  | otherwise = case t of
+#if MIN_VERSION_template_haskell(2,8,0)
+                     SigT _ (VarT k) -> IsKindVar k
+#endif
+                     _               -> NotKindStar
 
-instance Show NameBase where
-    showsPrec p = showsPrec p . getNameBase
+-- | Returns 'Just' the kind variable 'Name' of a 'StarKindStatus' if it exists.
+-- Otherwise, returns 'Nothing'.
+starKindStatusToName :: StarKindStatus -> Maybe Name
+starKindStatusToName (IsKindVar n) = Just n
+starKindStatusToName _             = Nothing
 
--- | A NameBase paired with the name of its map functions. For example, when deriving
--- Invariant2, its list of TyVarInfos might look like [(a, 'covMap1, 'contraMap1),
--- (b, 'covMap2, 'contraMap2)].
-type TyVarInfo = (NameBase, Name, Name)
+-- | Concat together all of the StarKindStatuses that are IsKindVar and extract
+-- the kind variables' Names out.
+catKindVarNames :: [StarKindStatus] -> [Name]
+catKindVarNames = mapMaybe starKindStatusToName
 
 -------------------------------------------------------------------------------
 -- Assorted utilities
 -------------------------------------------------------------------------------
 
+-- | Returns True if a Type has kind *.
+hasKindStar :: Type -> Bool
+hasKindStar VarT{}         = True
+#if MIN_VERSION_template_haskell(2,8,0)
+hasKindStar (SigT _ StarT) = True
+#else
+hasKindStar (SigT _ StarK) = True
+#endif
+hasKindStar _              = False
+
+-- Returns True is a kind is equal to *, or if it is a kind variable.
+isStarOrVar :: Kind -> Bool
+#if MIN_VERSION_template_haskell(2,8,0)
+isStarOrVar StarT  = True
+isStarOrVar VarT{} = True
+#else
+isStarOrVar StarK  = True
+#endif
+isStarOrVar _      = False
+
+-- | Gets all of the type/kind variable names mentioned somewhere in a Type.
+tyVarNamesOfType :: Type -> [Name]
+tyVarNamesOfType = go
+  where
+    go :: Type -> [Name]
+    go (AppT t1 t2) = go t1 ++ go t2
+    go (SigT t _k)  = go t
+#if MIN_VERSION_template_haskell(2,8,0)
+                           ++ go _k
+#endif
+    go (VarT n)     = [n]
+    go _            = []
+
+-- | Gets all of the type/kind variable names mentioned somewhere in a Kind.
+tyVarNamesOfKind :: Kind -> [Name]
+#if MIN_VERSION_template_haskell(2,8,0)
+tyVarNamesOfKind = tyVarNamesOfType
+#else
+tyVarNamesOfKind _ = [] -- There are no kind variables
+#endif
+
+-- | @hasKindVarChain n kind@ Checks if @kind@ is of the form
+-- k_0 -> k_1 -> ... -> k_(n-1), where k0, k1, ..., and k_(n-1) can be * or
+-- kind variables.
+hasKindVarChain :: Int -> Type -> Maybe [Name]
+hasKindVarChain kindArrows t =
+  let uk = uncurryKind (tyKind t)
+  in if (length uk - 1 == kindArrows) && all isStarOrVar uk
+        then Just (concatMap tyVarNamesOfKind uk)
+        else Nothing
+
+-- | If a Type is a SigT, returns its kind signature. Otherwise, return *.
+tyKind :: Type -> Kind
+tyKind (SigT _ k) = k
+tyKind _          = starK
+
+-- | If a VarT is missing an explicit kind signature, steal it from a TyVarBndr.
+stealKindForType :: TyVarBndr -> Type -> Type
+stealKindForType tvb t@VarT{} = SigT t (tvbKind tvb)
+stealKindForType _   t        = t
+
+-- | Monadic version of concatMap
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM f xs = liftM concat (mapM f xs)
+
+-- | A mapping of type variable Names to their map function Names. For example, in a
+-- Invariant declaration, a TyVarMap might look like:
+--
+--   (a ~> (covA, contraA), b ~> (covB, contraB))
+--
+-- where a and b are the last two type variables of the datatype, and covA and covB
+-- are the two map functions for a and b in covariant positions, and contraA and
+-- contraB are the two map functions for a and b in contravariant positions.
+type TyVarMap = Map Name (Name, Name)
+
 fst3 :: (a, b, c) -> a
 fst3 (a, _, _) = a
 
@@ -172,35 +277,36 @@
 constructorName (RecC    name      _  ) = name
 constructorName (InfixC  _    name _  ) = name
 constructorName (ForallC _    _    con) = constructorName con
+#if MIN_VERSION_template_haskell(2,11,0)
+constructorName (GadtC    names _ _)    = head names
+constructorName (RecGadtC names _ _)    = head names
+#endif
 
 -- | Generate a list of fresh names with a common prefix, and numbered suffixes.
 newNameList :: String -> Int -> Q [Name]
 newNameList prefix n = mapM (newName . (prefix ++) . show) [1..n]
 
--- | Remove any occurrences of a forall-ed type variable from a list of @TyVarInfo@s.
-removeForalled :: [TyVarBndr] -> [TyVarInfo] -> [TyVarInfo]
-removeForalled tvbs = filter (not . foralled tvbs)
-  where
-    foralled :: [TyVarBndr] -> TyVarInfo -> Bool
-    foralled tvbs' tvi = fst3 tvi `elem` map (NameBase . tvbName) tvbs'
-
--- | Extracts the name from a TyVarBndr.
-tvbName :: TyVarBndr -> Name
-tvbName (PlainTV  name)   = name
-tvbName (KindedTV name _) = name
-
 -- | Extracts the kind from a TyVarBndr.
 tvbKind :: TyVarBndr -> Kind
 tvbKind (PlainTV  _)   = starK
 tvbKind (KindedTV _ k) = k
 
--- | Replace the Name of a TyVarBndr with one from a Type (if the Type has a Name).
-replaceTyVarName :: TyVarBndr -> Type -> TyVarBndr
-replaceTyVarName tvb            (SigT t _) = replaceTyVarName tvb t
-replaceTyVarName (PlainTV  _)   (VarT n)   = PlainTV  n
-replaceTyVarName (KindedTV _ k) (VarT n)   = KindedTV n k
-replaceTyVarName tvb            _          = tvb
+-- | Convert a TyVarBndr to a Type.
+tvbToType :: TyVarBndr -> Type
+tvbToType (PlainTV n)    = VarT n
+tvbToType (KindedTV n k) = SigT (VarT n) k
 
+createKindChain :: Int -> Kind
+createKindChain = go starK
+  where
+    go :: Kind -> Int -> Kind
+    go k 0  = k
+#if MIN_VERSION_template_haskell(2,8,0)
+    go k n = n `seq` go (AppT (AppT ArrowT StarT) k) (n - 1)
+#else
+    go k n = n `seq` go (ArrowK StarK k) (n - 1)
+#endif
+
 -- | Applies a typeclass constraint to a type.
 applyClass :: Name -> Name -> Pred
 #if MIN_VERSION_template_haskell(2,10,0)
@@ -218,22 +324,24 @@
 canEtaReduce :: [Type] -> [Type] -> Bool
 canEtaReduce remaining dropped =
        all isTyVar dropped
-    && allDistinct nbs -- Make sure not to pass something of type [Type], since Type
-                       -- didn't have an Ord instance until template-haskell-2.10.0.0
-    && not (any (`mentionsNameBase` nbs) remaining)
+    && allDistinct droppedNames -- Make sure not to pass something of type [Type], since Type
+                                -- didn't have an Ord instance until template-haskell-2.10.0.0
+    && not (any (`mentionsName` droppedNames) remaining)
   where
-    nbs :: [NameBase]
-    nbs = map varTToNameBase dropped
+    droppedNames :: [Name]
+    droppedNames = map varTToName dropped
 
--- | Extract the Name from a type variable.
-varTToName :: Type -> Name
-varTToName (VarT n)   = n
-varTToName (SigT t _) = varTToName t
-varTToName _          = error "Not a type variable!"
+-- | Extract Just the Name from a type variable. If the argument Type is not a
+-- type variable, return Nothing.
+varTToName_maybe :: Type -> Maybe Name
+varTToName_maybe (VarT n)   = Just n
+varTToName_maybe (SigT t _) = varTToName_maybe t
+varTToName_maybe _          = Nothing
 
--- | Extract the NameBase from a type variable.
-varTToNameBase :: Type -> NameBase
-varTToNameBase = NameBase . varTToName
+-- | Extract the Name from a type variable. If the argument Type is not a
+-- type variable, throw an error.
+varTToName :: Type -> Name
+varTToName = fromMaybe (error "Not a type variable!") . varTToName_maybe
 
 -- | Peel off a kind signature from a Type (if it has one).
 unSigT :: Type -> Type
@@ -276,34 +384,28 @@
         | otherwise            = allDistinct' (Set.insert x uniqs) xs
     allDistinct' _ _           = True
 
--- | Does the given type mention any of the NameBases in the list?
-mentionsNameBase :: Type -> [NameBase] -> Bool
-mentionsNameBase = go Set.empty
+-- | Does the given type mention any of the Names in the list?
+mentionsName :: Type -> [Name] -> Bool
+mentionsName = go
   where
-    go :: Set NameBase -> Type -> [NameBase] -> Bool
-    go foralls (ForallT tvbs _ t) nbs =
-        go (foralls `Set.union` Set.fromList (map (NameBase . tvbName) tvbs)) t nbs
-    go foralls (AppT t1 t2) nbs = go foralls t1 nbs || go foralls t2 nbs
-    go foralls (SigT t _)   nbs = go foralls t nbs
-    go foralls (VarT n)     nbs = varNb `elem` nbs && not (varNb `Set.member` foralls)
-      where
-        varNb = NameBase n
-    go _       _            _   = False
+    go :: Type -> [Name] -> Bool
+    go (AppT t1 t2) names = go t1 names || go t2 names
+    go (SigT t _k)  names = go t names
+#if MIN_VERSION_template_haskell(2,8,0)
+                              || go _k names
+#endif
+    go (VarT n)     names = n `elem` names
+    go _            _     = False
 
--- | Does an instance predicate mention any of the NameBases in the list?
-predMentionsNameBase :: Pred -> [NameBase] -> Bool
+-- | Does an instance predicate mention any of the Names in the list?
+predMentionsName :: Pred -> [Name] -> Bool
 #if MIN_VERSION_template_haskell(2,10,0)
-predMentionsNameBase = mentionsNameBase
+predMentionsName = mentionsName
 #else
-predMentionsNameBase (ClassP _ tys) nbs = any (`mentionsNameBase` nbs) tys
-predMentionsNameBase (EqualP t1 t2) nbs = mentionsNameBase t1 nbs || mentionsNameBase t2 nbs
+predMentionsName (ClassP n tys) names = n `elem` names || any (`mentionsName` names) tys
+predMentionsName (EqualP t1 t2) names = mentionsName t1 names || mentionsName t2 names
 #endif
 
--- | The number of arrows that compose the spine of a kind signature
--- (e.g., (* -> *) -> k -> * has two arrows on its spine).
-numKindArrows :: Kind -> Int
-numKindArrows k = length (uncurryKind k) - 1
-
 -- | Construct a type via curried application.
 applyTy :: Type -> [Type] -> Type
 applyTy = foldl' AppT
@@ -327,77 +429,41 @@
 unapplyTy = reverse . go
   where
     go :: Type -> [Type]
-    go (AppT t1 t2) = t2:go t1
-    go (SigT t _)   = go t
-    go t            = [t]
+    go (AppT t1 t2)    = t2:go t1
+    go (SigT t _)      = go t
+    go (ForallT _ _ t) = go t
+    go t               = [t]
 
 -- | Split a type signature by the arrows on its spine. For example, this:
 --
 -- @
--- (Int -> String) -> Char -> ()
+-- forall a b. (a ~ b) => (a -> b) -> Char -> ()
 -- @
 --
 -- would split to this:
 --
 -- @
--- [Int -> String, Char, ()]
+-- (a ~ b, [a -> b, Char, ()])
 -- @
-uncurryTy :: Type -> [Type]
-uncurryTy (AppT (AppT ArrowT t1) t2) = t1:uncurryTy t2
-uncurryTy (SigT t _)                 = uncurryTy t
-uncurryTy t                          = [t]
+uncurryTy :: Type -> (Cxt, [Type])
+uncurryTy (AppT (AppT ArrowT t1) t2) =
+  let (ctxt, tys) = uncurryTy t2
+  in (ctxt, t1:tys)
+uncurryTy (SigT t _) = uncurryTy t
+uncurryTy (ForallT _ ctxt t) =
+  let (ctxt', tys) = uncurryTy t
+  in (ctxt ++ ctxt', tys)
+uncurryTy t = ([], [t])
 
 -- | Like uncurryType, except on a kind level.
 uncurryKind :: Kind -> [Kind]
 #if MIN_VERSION_template_haskell(2,8,0)
-uncurryKind = uncurryTy
+uncurryKind = snd . uncurryTy
 #else
 uncurryKind (ArrowK k1 k2) = k1:uncurryKind k2
 uncurryKind k              = [k]
 #endif
 
-wellKinded :: [Kind] -> Bool
-wellKinded = all canRealizeKindStar
-
--- | Of form k1 -> k2 -> ... -> kn, where k is either a single kind variable or *.
-canRealizeKindStarChain :: Kind -> Bool
-canRealizeKindStarChain = all canRealizeKindStar . uncurryKind
-
-canRealizeKindStar :: Kind -> Bool
-canRealizeKindStar k = case uncurryKind k of
-    [k'] -> case k' of
-#if MIN_VERSION_template_haskell(2,8,0)
-                 StarT    -> True
-                 (VarT _) -> True -- Kind k can be instantiated with *
-#else
-                 StarK    -> True
-#endif
-                 _ -> False
-    _ -> False
-
-createKindChain :: Int -> Kind
-createKindChain = go starK
-  where
-    go :: Kind -> Int -> Kind
-    go k 0  = k
-#if MIN_VERSION_template_haskell(2,8,0)
-    go k n = n `seq` go (AppT (AppT ArrowT StarT) k) (n - 1)
-#else
-    go k n = n `seq` go (ArrowK StarK k) (n - 1)
-#endif
-
-distinctKindVars :: Kind -> Set Name
-#if MIN_VERSION_template_haskell(2,8,0)
-distinctKindVars (AppT k1 k2) = distinctKindVars k1 `Set.union` distinctKindVars k2
-distinctKindVars (SigT k _)   = distinctKindVars k
-distinctKindVars (VarT k)     = Set.singleton k
-#endif
-distinctKindVars _            = Set.empty
-
-tvbToType :: TyVarBndr -> Type
-tvbToType (PlainTV n)    = VarT n
-tvbToType (KindedTV n k) = SigT (VarT n) k
-
 -------------------------------------------------------------------------------
 -- Manually quoted names
 -------------------------------------------------------------------------------
@@ -439,3 +505,8 @@
 
 errorValName :: Name
 errorValName = mkNameG_v "base" "GHC.Err" "error"
+
+#if MIN_VERSION_base(4,6,0) && !(MIN_VERSION_base(4,9,0))
+starKindName :: Name
+starKindName = mkNameG_tc "ghc-prim" "GHC.Prim" "*"
+#endif
diff --git a/test/THSpec.hs b/test/THSpec.hs
--- a/test/THSpec.hs
+++ b/test/THSpec.hs
@@ -8,6 +8,9 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
 {-# OPTIONS_GHC -fno-warn-unused-matches #-}
+#if __GLASGOW_HASKELL__ >= 800
+{-# OPTIONS_GHC -fno-warn-unused-foralls #-}
+#endif
 module THSpec (main, spec) where
 
 import Data.Functor.Invariant