Fix the free-var test in validDerivPred

The free-var test (now documented as (VD3)) was too narrow,
affecting only class predicates.  #21302 demonstrated that
this wasn't enough!

Fixes #21302.

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

4 files changed, 74 insertions, 57 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 598b07b8c7..6046c60dbc 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1621,30 +1621,30 @@ here because it uses sizeTypes, fvTypes.
 
 It checks for three things
 
-  * No repeated variables (hasNoDups fvs)
+(VD1) No repeated variables (hasNoDups fvs)
 
-  * No type constructors.  This is done by comparing
+(VD2) No type constructors.  This is done by comparing
         sizeTypes tys == length (fvTypes tys)
-    sizeTypes counts variables and constructors; fvTypes returns variables.
-    So if they are the same, there must be no constructors.  But there
-    might be applications thus (f (g x)).
-
-    Note that tys only includes the visible arguments of the class type
-    constructor. Including the non-visible arguments can cause the following,
-    perfectly valid instance to be rejected:
-       class Category (cat :: k -> k -> *) where ...
-       newtype T (c :: * -> * -> *) a b = MkT (c a b)
-       instance Category c => Category (T c) where ...
-    since the first argument to Category is a non-visible *, which sizeTypes
-    would count as a constructor! See #11833.
-
-  * Also check for a bizarre corner case, when the derived instance decl
-    would look like
-       instance C a b => D (T a) where ...
-    Note that 'b' isn't a parameter of T.  This gives rise to all sorts of
-    problems; in particular, it's hard to compare solutions for equality
-    when finding the fixpoint, and that means the inferContext loop does
-    not converge.  See #5287.
+      sizeTypes counts variables and constructors; fvTypes returns variables.
+      So if they are the same, there must be no constructors.  But there
+      might be applications thus (f (g x)).
+
+      Note that tys only includes the visible arguments of the class type
+      constructor. Including the non-visible arguments can cause the following,
+      perfectly valid instance to be rejected:
+         class Category (cat :: k -> k -> *) where ...
+         newtype T (c :: * -> * -> *) a b = MkT (c a b)
+         instance Category c => Category (T c) where ...
+      since the first argument to Category is a non-visible *, which sizeTypes
+      would count as a constructor! See #11833.
+
+(VD3) Also check for a bizarre corner case, when the derived instance decl
+      would look like
+         instance C a b => D (T a) where ...
+      Note that 'b' isn't a parameter of T.  This gives rise to all sorts of
+      problems; in particular, it's hard to compare solutions for equality
+      when finding the fixpoint, and that means the inferContext loop does
+      not converge.  See #5287, #21302
 
 Note [Equality class instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1657,21 +1657,27 @@ instances only in the defining module.
 validDerivPred :: TyVarSet -> PredType -> Bool
 -- See Note [Valid 'deriving' predicate]
 validDerivPred tv_set pred
+  | not (tyCoVarsOfType pred `subVarSet` tv_set)
+  = False  -- Check (VD3)
+
+  | otherwise
   = case classifyPredType pred of
-       ClassPred cls tys -> cls `hasKey` typeableClassKey
-                -- Typeable constraints are bigger than they appear due
-                -- to kind polymorphism, but that's OK
-                       || check_tys cls tys
-       EqPred {}       -> False  -- reject equality constraints
-       _               -> True   -- Non-class predicates are ok
-  where
-    check_tys cls tys
-              = hasNoDups fvs
-                   -- use sizePred to ignore implicit args
-                && lengthIs fvs (sizePred pred)
-                && all (`elemVarSet` tv_set) fvs
-      where tys' = filterOutInvisibleTypes (classTyCon cls) tys
-            fvs  = fvTypes tys'
+
+       ClassPred cls tys
+          | isTerminatingClass cls -> True
+            -- Typeable constraints are bigger than they appear due
+            -- to kind polymorphism, but that's OK
+
+          | otherwise -> hasNoDups visible_fvs                        -- Check (VD1)
+                      && lengthIs visible_fvs (sizeTypes visible_tys) -- Check (VD2)
+          where
+            visible_tys = filterOutInvisibleTypes (classTyCon cls) tys
+            visible_fvs = fvTypes visible_tys
+
+       IrredPred {}   -> True   -- Accept (f a)
+       EqPred {}      -> False  -- Reject equality constraints
+       ForAllPred {}  -> False  -- Rejects quantified predicates
+       SpecialPred {} -> False  -- Rejects special predicates
 
 {-
 ************************************************************************
@@ -2791,27 +2797,6 @@ sizeTyConAppArgs :: TyCon -> [Type] -> Int
 sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
                            -- See Note [Invisible arguments and termination]
 
--- Size of a predicate
---
--- We are considering whether class constraints terminate.
--- Equality constraints and constraints for the implicit
--- parameter class always terminate so it is safe to say "size 0".
--- See #4200.
-sizePred :: PredType -> Int
-sizePred ty = goClass ty
-  where
-    goClass p = go (classifyPredType p)
-
-    go (ClassPred cls tys')
-      | isTerminatingClass cls = 0
-      | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
-                    -- The filtering looks bogus
-                    -- See Note [Invisible arguments and termination]
-    go (EqPred {})           = 0
-    go (SpecialPred {})      = 0
-    go (IrredPred ty)        = sizeType ty
-    go (ForAllPred _ _ pred) = goClass pred
-
 -- | When this says "True", ignore this class constraint during
 -- a termination check
 isTerminatingClass :: Class -> Bool
diff --git a/testsuite/tests/deriving/should_fail/T21302.hs b/testsuite/tests/deriving/should_fail/T21302.hs
new file mode 100644
index 0000000000..16e7cf320d
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T21302.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UndecidableInstances, TypeFamilies #-}
+
+module T21302 where
+
+data BoxAssocDouble = BoxAssocDouble (BoxAssoc Int)
+  deriving (Eq)
+
+type family Assoc a
+
+data BoxAssoc a = BoxAssoc (Assoc a)
+
+deriving instance c Eq a => Eq (BoxAssoc a)
diff --git a/testsuite/tests/deriving/should_fail/T21302.stderr b/testsuite/tests/deriving/should_fail/T21302.stderr
new file mode 100644
index 0000000000..46910cbf4f
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T21302.stderr
@@ -0,0 +1,19 @@
+
+T21302.hs:6:13: error:
+    • Could not solve: (c0 Eq Int)
+        arising from the first field of ‘BoxAssocDouble’
+          (type ‘BoxAssoc Int’)
+    • When deriving the instance for (Eq BoxAssocDouble)
+
+T21302.hs:12:19: error:
+    • Could not deduce (c0 Eq a)
+      from the context: c Eq a
+        bound by a stand-alone deriving instance declaration:
+                   forall (c :: (* -> Constraint) -> * -> Constraint) a.
+                   c Eq a =>
+                   Eq (BoxAssoc a)
+        at T21302.hs:12:19-43
+    • In the ambiguity check for a stand-alone deriving instance declaration
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the stand-alone deriving instance for
+        ‘c Eq a => Eq (BoxAssoc a)’
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index 61d74b72b4..2b2f2af562 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -82,3 +82,4 @@ test('deriving-via-fail4', normal, compile_fail, [''])
 test('deriving-via-fail5', normal, compile_fail, [''])
 test('T21087', normal, compile_fail, [''])
 test('T21087b', [extra_files(['T21087b_aux.hs','T21087b_aux.hs-boot'])], multimod_compile_fail, ['T21087b', ''])
+test('T21302', normal, compile_fail, [''])