Do not create nested quantified constraints

Previously, we would accidentally make constraints like
forall a. C a => forall b. D b => E a b c as we traversed
superclasses. No longer!

This patch also expands Note [Eagerly expand given superclasses]
to work over quantified constraints; necessary for T16502b.

Close #17202 and #16502.

test cases: typecheck/should_compile/T{17202,16502{,b}}

5 files changed, 72 insertions, 2 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T16502b.hs b/testsuite/tests/typecheck/should_compile/T16502b.hs
new file mode 100644
index 0000000000..03855c4557
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16502b.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T16502b where
+
+import Data.Kind
+
+type family Sing :: k -> Type
+
+class    (forall (sing :: k -> Type). sing ~ Sing => Show (sing z))
+                       => ShowSing' (z :: k)
+instance Show (Sing z) => ShowSing' (z :: k)
+
+class    (forall (z :: k). ShowSing' z) => ShowSing k
+instance (forall (z :: k). ShowSing' z) => ShowSing k
+
+newtype Foo a = MkFoo a
+data SFoo :: forall a. Foo a -> Type where
+  SMkFoo :: Sing x -> SFoo (MkFoo x)
+type instance Sing = SFoo
+deriving instance ShowSing a => Show (SFoo (z :: Foo a))
+
+newtype Bar a = MkBar (Foo a)
+data SBar :: forall a. Bar a -> Type where
+  SMkBar :: forall a (x :: Foo a). Sing x -> SBar (MkBar x)
+type instance Sing = SBar
+deriving instance ShowSing (Foo a) => Show (SBar (z :: Bar a))
diff --git a/testsuite/tests/typecheck/should_compile/T17202.hs b/testsuite/tests/typecheck/should_compile/T17202.hs
index d9d6ec281f..9f28ccc753 100644
--- a/testsuite/tests/typecheck/should_compile/T17202.hs
+++ b/testsuite/tests/typecheck/should_compile/T17202.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ConstraintKinds #-}
 
 module T17202 where
 
@@ -15,6 +16,7 @@ data Dict c = c => Dict
 foo :: forall a. C3 a => Dict (C1 a)
 foo = Dict
 
+{- is rejected due to #17719
 bar :: forall a. C3 a => Dict (C1 a)
 bar = Dict :: C2 a => Dict (C1 a)
-
+-}
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 54a0c4f4c7..8eb6f17b57 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -688,9 +688,10 @@ test('T16832', normal, ghci_script, ['T16832.script'])
 test('T16995', normal, compile, [''])
 test('T17007', normal, compile, [''])
 test('T17067', normal, compile, [''])
-test('T17202', expect_broken(17202), compile, [''])
+test('T17202', normal, compile, [''])
 test('T15839a', normal, compile, [''])
 test('T15839b', normal, compile, [''])
+test('T16502b', normal, compile, [''])
 test('T17343', exit_code(1), compile_and_run, [''])
 test('T17566', [extra_files(['T17566a.hs'])], makefile_test, [])
 test('T12760', unless(compiler_debugged(), skip), compile, ['-O'])
diff --git a/testsuite/tests/typecheck/should_fail/T16502.hs b/testsuite/tests/typecheck/should_fail/T16502.hs
new file mode 100644
index 0000000000..5fac062d85
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16502.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE InstanceSigs #-}
+module T16502 where
+
+import Data.Kind
+
+class    (forall c. c ~ T a => Show (c b)) => ShowT a b
+instance Show (T a b) => ShowT a b
+
+class (forall b. Show b => ShowT a b) => C a where
+  type family T a :: Type -> Type
+
+data D a = MkD (T a Int)
+
+instance C a => Show (D a) where
+  showsPrec p (MkD x)
+    = (showParen (p > 10) $ showString "MkD " . showsPrec 11 x)
+
+-- This is rejected because we cannot derive (Show (D a)) from (C a)
+-- due to troublesome quantified constraints. And then the error
+-- message mentions the internal name of the default method for show.
+-- Simon thinks that we should accept the fact that this doesn't get
+-- accepted, given that a quantified constraint for (Show (c b)) is far
+-- too applicable to be useful. So we're left with the suboptimal
+-- error message.
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e2496562e1..31b1fb3333 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -551,6 +551,7 @@ test('T17355', normal, compile_fail, [''])
 test('T17360', normal, compile_fail, [''])
 test('T17563', normal, compile_fail, [''])
 test('T16946', normal, compile_fail, [''])
+test('T16502', expect_broken(12854), compile, [''])
 test('T17566b', normal, compile_fail, [''])
 test('T17566c', normal, compile_fail, [''])
 test('T17773', normal, compile_fail, [''])