DeriveFunctor: Check for last type variables using dataConUnivTyVars

Previously, derived instances of `Functor` (as well as the related classes
`Foldable`, `Traversable`, and `Generic1`) would determine which constraints to
infer by checking for fields that contain the last type variable. The problem
was that this last type variable was taken from `tyConTyVars`. For GADTs, the
type variables in each data constructor are _not_ the same type variables as
in `tyConTyVars`, leading to #22167.

This fixes the issue by instead checking for the last type variable using
`dataConUnivTyVars`. (This is very similar in spirit to the fix for #21185,
which also replaced an errant use of `tyConTyVars` with type variables from
each data constructor.)

Fixes #22167.

5 files changed, 107 insertions, 22 deletions

diff --git a/compiler/GHC/Tc/Deriv/Functor.hs b/compiler/GHC/Tc/Deriv/Functor.hs
index b3e9fb775c..4b111f7a41 100644
--- a/compiler/GHC/Tc/Deriv/Functor.hs
+++ b/compiler/GHC/Tc/Deriv/Functor.hs
@@ -538,8 +538,36 @@ functorLikeTraverse var (FT { ft_triv = caseTrivial,     ft_var = caseVar
 
     go _ _ = (caseTrivial,False)
 
--- Return all syntactic subterms of ty that contain var somewhere
--- These are the things that should appear in instance constraints
+-- | Return all syntactic subterms of a 'Type' that are applied to the 'TyVar'
+-- argument. This determines what constraints should be inferred for derived
+-- 'Functor', 'Foldable', and 'Traversable' instances in "GHC.Tc.Deriv.Infer".
+-- For instance, if we have:
+--
+-- @
+-- data Foo a = MkFoo Int a (Maybe a) (Either Int (Maybe a))
+-- @
+--
+-- Then the following would hold:
+--
+-- * @'deepSubtypesContaining' a Int@ would return @[]@, since @Int@ does not
+--   contain the type variable @a@ at all.
+--
+-- * @'deepSubtypesContaining' a a@ would return @[]@. Although the type @a@
+--   contains the type variable @a@, it is not /applied/ to @a@, which is the
+--   criterion that 'deepSubtypesContaining' checks for.
+--
+-- * @'deepSubtypesContaining' a (Maybe a)@ would return @[Maybe]@, as @Maybe@
+--   is applied to @a@.
+--
+-- * @'deepSubtypesContaining' a (Either Int (Maybe a))@ would return
+--   @[Either Int, Maybe]@. Both of these types are applied to @a@ through
+--   composition.
+--
+-- As used in "GHC.Tc.Deriv.Infer", the 'Type' argument will always come from
+-- 'derivDataConInstArgTys', so it is important that the 'TyVar' comes from
+-- 'dataConUnivTyVars' to match. Make sure /not/ to take the 'TyVar' from
+-- 'tyConTyVars', as these differ from the 'dataConUnivTyVars' when the data
+-- type is a GADT. (See #22167 for what goes wrong if 'tyConTyVars' is used.)
 deepSubtypesContaining :: TyVar -> Type -> [TcType]
 deepSubtypesContaining tv
   = functorLikeTraverse tv
diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs
index 2c7639c3a9..b47d6cd632 100644
--- a/compiler/GHC/Tc/Deriv/Generics.hs
+++ b/compiler/GHC/Tc/Deriv/Generics.hs
@@ -93,10 +93,25 @@ gen_Generic_binds gk loc dit = do
 ************************************************************************
 -}
 
+-- | Called by 'GHC.Tc.Deriv.Infer.inferConstraints'; generates a list of
+-- types, each of which must be a 'Functor' in order for the 'Generic1'
+-- instance to work. For instance, if we have:
+--
+-- @
+-- data Foo a = MkFoo Int a (Maybe a) (Either Int (Maybe a))
+-- @
+--
+-- Then @'get_gen1_constrained_tys' a (f (g a))@ would return @[Either Int]@,
+-- as a derived 'Generic1' instance would need to call 'fmap' at that type.
+-- Invoking @'get_gen1_constrained_tys' a@ on any of the other fields would
+-- return @[]@.
+--
+-- 'get_gen1_constrained_tys' is very similar in spirit to
+-- 'deepSubtypesContaining' in "GHC.Tc.Deriv.Functor". Just like with
+-- 'deepSubtypesContaining', it is important that the 'TyVar' argument come
+-- from 'dataConUnivTyVars'. (See #22167 for what goes wrong if 'tyConTyVars'
+-- is used.)
 get_gen1_constrained_tys :: TyVar -> Type -> [Type]
--- called by GHC.Tc.Deriv.Infer.inferConstraints; generates a list of
--- types, each of which must be a Functor in order for the Generic1 instance to
--- work.
 get_gen1_constrained_tys argVar
   = argTyFold argVar $ ArgTyAlg { ata_rec0 = const []
                                 , ata_par1 = [], ata_rec1 = const []
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs
index 4966a65b1f..5aa954ca4b 100644
--- a/compiler/GHC/Tc/Deriv/Infer.hs
+++ b/compiler/GHC/Tc/Deriv/Infer.hs
@@ -178,9 +178,10 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
 
               -- Constraints arising from the arguments of each constructor
            con_arg_constraints
-             :: (CtOrigin -> TypeOrKind
-                          -> Type
-                          -> [(ThetaSpec, Maybe Subst)])
+             :: ([TyVar] -> CtOrigin
+                         -> TypeOrKind
+                         -> Type
+                         -> [(ThetaSpec, Maybe Subst)])
              -> (ThetaSpec, [TyVar], [TcType], DerivInstTys)
            con_arg_constraints get_arg_constraints
              = let -- Constraints from the fields of each data constructor.
@@ -195,7 +196,8 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                      , not (isUnliftedType arg_ty)
                      , let orig = DerivOriginDC data_con arg_n wildcard
                      , preds_and_mbSubst
-                         <- get_arg_constraints orig arg_t_or_k arg_ty
+                         <- get_arg_constraints (dataConUnivTyVars data_con)
+                                                orig arg_t_or_k arg_ty
                      ]
                    -- Stupid constraints from DatatypeContexts. Note that we
                    -- must gather these constraints from the data constructors,
@@ -237,21 +239,39 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
            is_functor_like = tcTypeKind inst_ty `tcEqKind` typeToTypeKind
                           || is_generic1
 
-           get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
-                                -> [(ThetaSpec, Maybe Subst)]
-           get_gen1_constraints functor_cls orig t_or_k ty
+           get_gen1_constraints ::
+                Class
+             -> [TyVar] -- The universally quantified type variables for the
+                        -- data constructor
+             -> CtOrigin -> TypeOrKind -> Type
+             -> [(ThetaSpec, Maybe Subst)]
+           get_gen1_constraints functor_cls dc_univs orig t_or_k ty
               = mk_functor_like_constraints orig t_or_k functor_cls $
-                get_gen1_constrained_tys last_tv ty
-
-           get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
-                                   -> [(ThetaSpec, Maybe Subst)]
-           get_std_constrained_tys orig t_or_k ty
+                get_gen1_constrained_tys last_dc_univ ty
+             where
+               -- If we are deriving an instance of 'Generic1' and have made
+               -- it this far, then there should be at least one universal type
+               -- variable, making this use of 'last' safe.
+               last_dc_univ = assert (not (null dc_univs)) $
+                              last dc_univs
+
+           get_std_constrained_tys ::
+                [TyVar] -- The universally quantified type variables for the
+                        -- data constructor
+             -> CtOrigin -> TypeOrKind -> Type
+             -> [(ThetaSpec, Maybe Subst)]
+           get_std_constrained_tys dc_univs orig t_or_k ty
                | is_functor_like
                = mk_functor_like_constraints orig t_or_k main_cls $
-                 deepSubtypesContaining last_tv ty
+                 deepSubtypesContaining last_dc_univ ty
                | otherwise
                = [( [mk_cls_pred orig t_or_k main_cls ty]
                   , Nothing )]
+             where
+               -- If 'is_functor_like' holds, then there should be at least one
+               -- universal type variable, making this use of 'last' safe.
+               last_dc_univ = assert (not (null dc_univs)) $
+                              last dc_univs
 
            mk_functor_like_constraints :: CtOrigin -> TypeOrKind
                                        -> Class -> [Type]
@@ -279,9 +299,6 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                              , tcUnifyTy ki typeToTypeKind
                              )
 
-           rep_tc_tvs      = tyConTyVars rep_tc
-           last_tv         = last rep_tc_tvs
-
            -- Extra Data constraints
            -- The Data class (only) requires that for
            --    instance (...) => Data (T t1 t2)
@@ -320,7 +337,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
              -- Generic1 needs Functor
              -- See Note [Getting base classes]
           |  is_generic1
-           -> assert (rep_tc_tvs `lengthExceeds` 0) $
+           -> assert (tyConTyVars rep_tc `lengthExceeds` 0) $
               -- Generic1 has a single kind variable
               assert (cls_tys `lengthIs` 1) $
               do { functorClass <- lift $ tcLookupClass functorClassName
diff --git a/testsuite/tests/deriving/should_compile/T22167.hs b/testsuite/tests/deriving/should_compile/T22167.hs
new file mode 100644
index 0000000000..c7f23166f6
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T22167.hs
@@ -0,0 +1,24 @@
+module T22167 where
+
+import GHC.Generics (Generic1)
+
+data T1 f a = MkT1 (f a)
+  deriving (Functor, Foldable, Traversable)
+
+data T2 f a where
+  MkT2 :: f a -> T2 f a
+  deriving (Functor, Foldable, Traversable)
+
+-- A slightly more complicated example from the `syntactic` library
+data (sym1 :+: sym2) sig
+  where
+    InjL :: sym1 a -> (sym1 :+: sym2) a
+    InjR :: sym2 a -> (sym1 :+: sym2) a
+  deriving (Functor, Foldable, Traversable)
+
+-- Test Generic1 instances with inferred Functor constraints
+data G1 f g a = MkG1 (f (g a)) deriving Generic1
+
+data G2 f g a where
+  MkG2 :: f (g a) -> G2 f g a
+  deriving Generic1
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index c5edb5275f..5d23680d2b 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -139,3 +139,4 @@ test('T20387', normal, compile, [''])
 test('T20501', normal, compile, [''])
 test('T20719', normal, compile, [''])
 test('T20994', normal, compile, [''])
+test('T22167', normal, compile, [''])