validDerivPred: Reject exotic constraints in IrredPreds

This brings the `IrredPred` case in sync with the treatment of `ClassPred`s as
described in `Note [Valid 'deriving' predicate]` in `GHC.Tc.Validity`. Namely,
we should reject `IrredPred`s that are inferred from `deriving` clauses whose
arguments contain other type constructors, as described in `(VD2) Reject exotic
constraints` of that Note.  This has the nice property that `deriving` clauses
whose inferred instance context mention `TypeError` will now emit the type
error in the resulting error message, which better matches existing intuitions
about how `TypeError` should work.

While I was in town, I noticed that much of `Note [Valid 'deriving' predicate]`
was duplicated in a separate `Note [Exotic derived instance contexts]` in
`GHC.Tc.Deriv.Infer`. I decided to fold the latter Note into the former so that
there is a single authority on describing the conditions under which an
inferred `deriving` constraint can be considered valid.

This changes the behavior of `deriving` in a way that existing code might
break, so I have made a mention of this in the GHC User's Guide. It seems very,
very unlikely that much code is relying on this strange behavior, however, and
even if there is, there is a clear, backwards-compatible migration path using
`StandaloneDeriving`.

Fixes #22696.

9 files changed, 84 insertions, 12 deletions

diff --git a/testsuite/tests/deriving/should_compile/T22696a.hs b/testsuite/tests/deriving/should_compile/T22696a.hs
new file mode 100644
index 0000000000..c711fb1efc
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T22696a.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T22696a where
+
+import GHC.TypeLits
+
+newtype Foo = Foo Int
+
+class Bar a where
+  bar :: a
+
+instance (TypeError (Text "Boo")) => Bar Foo where
+  bar = undefined
+
+newtype Baz = Baz Foo
+
+deriving instance TypeError (Text "Boo") => Bar Baz
diff --git a/testsuite/tests/deriving/should_compile/T22696c.hs b/testsuite/tests/deriving/should_compile/T22696c.hs
new file mode 100644
index 0000000000..f0e0d14e04
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T22696c.hs
@@ -0,0 +1,24 @@
+module T22696c where
+
+class C a where
+  m :: a
+
+data S1 c a where
+  MkS1 :: c => S1 c a
+instance c => C (S1 c a) where
+  m = MkS1
+
+data S2 c a where
+  MkS2 :: c a => S2 c a
+instance c a => C (S2 c a) where
+  m = MkS2
+
+newtype T1 c a = MkT1 (S1 c a) deriving C
+newtype T2 c a = MkT2 (S2 c a) deriving C
+  -- The inferred instances would be:
+  --
+  --  instance c   => C (T1 c a)
+  --  instance c a => C (T2 c a)
+  --
+  -- These are valid instance context for the reasons described in
+  -- (VD2) in Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index 922b7126b7..dd1fe9cd3d 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -101,7 +101,6 @@ test('T13919', normal, compile, [''])
 test('T13998', normal, compile, [''])
 test('T14045b', normal, compile, [''])
 test('T14094', normal, compile, [''])
-test('T14339', normal, compile, [''])
 test('T14331', normal, compile, [''])
 test('T14332', normal, compile, [''])
 test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
@@ -140,3 +139,5 @@ test('T20501', normal, compile, [''])
 test('T20719', normal, compile, [''])
 test('T20994', normal, compile, [''])
 test('T22167', normal, compile, [''])
+test('T22696a', normal, compile, [''])
+test('T22696c', normal, compile, [''])
diff --git a/testsuite/tests/deriving/should_compile/drv015.hs b/testsuite/tests/deriving/should_compile/drv015.hs
index ea79179e68..0594d46ebb 100644
--- a/testsuite/tests/deriving/should_compile/drv015.hs
+++ b/testsuite/tests/deriving/should_compile/drv015.hs
@@ -1,12 +1,12 @@
 
--- July 07: I'm changing this from "should_compile" to "should_fail".
--- It would generate an instance decl like
+-- This will generate an instance decl like:
+--
 --      instance (Show (f a), Show (g a)) => Show (Pair1 f g a)
--- and that is not Haskell 98.
 --
--- See Note [Exotic derived instance contexts] in GHC.Tc.Solver.
--- The rule is simple: the context of a derived instance decl must
--- contain constraints of form (C tyvar) only, just as H98.
+-- Although the Haskell Report would not permit this instance if written out
+-- explicitly, it does not say anything about whether it is acceptable for a
+-- *derived* instance to generate it. As such, we allow this in GHC.
+-- See Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
 
 module ShouldCompile where
 
diff --git a/testsuite/tests/deriving/should_compile/T14339.hs b/testsuite/tests/deriving/should_fail/T14339.hs
index 098b6e829a..b48f2e2501 100644
--- a/testsuite/tests/deriving/should_compile/T14339.hs
+++ b/testsuite/tests/deriving/should_fail/T14339.hs
@@ -16,10 +16,10 @@ instance (TypeError (Text "Boo")) => Bar Foo where
 newtype Baz = Baz Foo
   deriving Bar
 
--- Apparently we derive
+-- We derive:
+--
 --  instance TypeError (Text "Boo") => Bar Baz
 --
--- Is that really what we want?  It defers the type
--- error... surely we should use standalone deriving
--- if that is what we want?
--- See GHC.Tc.Validity.validDerivPred and #22696.
\ No newline at end of file
+-- And error out due to the TypeError. See also
+-- deriving/should_compile/T22696a, which uses StandaloneDeriving to write a
+-- valid instance with a TypeError constraint in its instance context.
diff --git a/testsuite/tests/deriving/should_fail/T14339.stderr b/testsuite/tests/deriving/should_fail/T14339.stderr
new file mode 100644
index 0000000000..dc2611a243
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14339.stderr
@@ -0,0 +1,4 @@
+
+T14339.hs:17:12: error: [GHC-64725]
+    • Boo
+    • When deriving the instance for (Bar Baz)
diff --git a/testsuite/tests/deriving/should_fail/T22696b.hs b/testsuite/tests/deriving/should_fail/T22696b.hs
new file mode 100644
index 0000000000..937208a479
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T22696b.hs
@@ -0,0 +1,19 @@
+module T22696b where
+
+class C a where
+  m :: a
+
+data S c where
+  MkS :: c Int => S c
+
+instance c Int => C (S c) where
+  m = MkS
+
+newtype T c = MkT (S c)
+  deriving C
+  -- The inferred instance would be:
+  --
+  --  instance c Int => C (T c)
+  --
+  -- And we want to reject this instance due to the reasons mentioned in
+  -- (VD2) in Note [Valid 'deriving' predicate] in GHC.Tc.Validity.
diff --git a/testsuite/tests/deriving/should_fail/T22696b.stderr b/testsuite/tests/deriving/should_fail/T22696b.stderr
new file mode 100644
index 0000000000..0771d0d44b
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T22696b.stderr
@@ -0,0 +1,5 @@
+
+T22696b.hs:13:12: error: [GHC-05617]
+    • Could not solve: ‘c Int’
+        arising from the 'deriving' clause of a data type declaration
+    • When deriving the instance for (C (T c))
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index 656e4dd5c2..294f8261e8 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -69,6 +69,7 @@ test('T12801', normal, compile_fail, [''])
 test('T13154c', normal, compile_fail, [''])
 test('T14365', [extra_files(['T14365B.hs','T14365B.hs-boot'])],
                multimod_compile_fail, ['T14365A',''])
+test('T14339', normal, compile_fail, [''])
 test('T14728a', normal, compile_fail, [''])
 test('T14728b', normal, compile_fail, [''])
 test('T14916', normal, compile_fail, [''])
@@ -84,3 +85,4 @@ 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, [''])
 test('T21871', normal, compile_fail, [''])
+test('T22696b', normal, compile_fail, [''])