11 files changed, 209 insertions, 0 deletions
diff --git a/testsuite/tests/quantified-constraints/T17267.hs b/testsuite/tests/quantified-constraints/T17267.hs
new file mode 100644
index 0000000000..eaad478003
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267 where
+
+class a ~ b => Thing a b
+instance a ~ b => Thing a b
+
+unsafeCoerce :: forall a b. a -> b
+unsafeCoerce a = oops a where
+  oops :: (a ~ b => Thing a b) => (Thing a b => r) -> r
+  oops r = r
+
+
+{-
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+uc :: a -> b
+uc = oops where
+  oops :: (C a b => C a b) => a -> b
+  oops x = op x
+-}
+
+{-
+-- Now rejected
+uc :: a -> b
+uc = oops where
+  oops :: (a ~ b => a ~ b) => a -> b
+  oops x = x
+-}
+
+
+{-
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+class C a b => Thing a b
+instance C a b => Thing a b
+
+unsafeCoerce :: forall a b. a -> b
+unsafeCoerce a = oops (op a :: Thing a b => b)
+  where
+    oops :: (C a b => Thing a b) => (Thing a b => x) -> x
+    oops r = r
+-}
+
diff --git a/testsuite/tests/quantified-constraints/T17267.stderr b/testsuite/tests/quantified-constraints/T17267.stderr
new file mode 100644
index 0000000000..79f09fdf98
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267.stderr
@@ -0,0 +1,16 @@
+
+T17267.hs:17:12: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: a ~ b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: r
+      In an equation for ‘oops’: oops r = r
+      In an equation for ‘unsafeCoerce’:
+          unsafeCoerce a
+            = oops a
+            where
+                oops :: (a ~ b => Thing a b) => (Thing a b => r) -> r
+                oops r = r
diff --git a/testsuite/tests/quantified-constraints/T17267a.hs b/testsuite/tests/quantified-constraints/T17267a.hs
new file mode 100644
index 0000000000..acf75b9355
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267a.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267a where
+
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+uc :: a -> b
+uc = oops where
+  oops :: (C a b => C a b) => a -> b
+  oops x = op x
diff --git a/testsuite/tests/quantified-constraints/T17267a.stderr b/testsuite/tests/quantified-constraints/T17267a.stderr
new file mode 100644
index 0000000000..c57eb1f75c
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267a.stderr
@@ -0,0 +1,16 @@
+
+T17267a.hs:18:12: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: C a b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: op x
+      In an equation for ‘oops’: oops x = op x
+      In an equation for ‘uc’:
+          uc
+            = oops
+            where
+                oops :: (C a b => C a b) => a -> b
+                oops x = op x
diff --git a/testsuite/tests/quantified-constraints/T17267b.hs b/testsuite/tests/quantified-constraints/T17267b.hs
new file mode 100644
index 0000000000..82285d0265
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267b.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267b where
+
+-- Now rejected
+uc :: a -> b
+uc = oops where
+  oops :: (a ~ b => a ~ b) => a -> b
+  oops x = x
+
diff --git a/testsuite/tests/quantified-constraints/T17267b.stderr b/testsuite/tests/quantified-constraints/T17267b.stderr
new file mode 100644
index 0000000000..8a5eeec908
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267b.stderr
@@ -0,0 +1,16 @@
+
+T17267b.hs:15:12: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: a ~ b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: x
+      In an equation for ‘oops’: oops x = x
+      In an equation for ‘uc’:
+          uc
+            = oops
+            where
+                oops :: (a ~ b => a ~ b) => a -> b
+                oops x = x
diff --git a/testsuite/tests/quantified-constraints/T17267c.hs b/testsuite/tests/quantified-constraints/T17267c.hs
new file mode 100644
index 0000000000..caa93e8234
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267c.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T17267c where
+
+-- Now rejected
+class C a b where
+  op :: a -> b
+
+class C a b => Thing a b
+instance C a b => Thing a b
+
+unsafeCoerce :: forall a b. a -> b
+unsafeCoerce a = oops (op a :: Thing a b => b)
+  where
+    oops :: (C a b => Thing a b) => (Thing a b => x) -> x
+    oops r = r
+
diff --git a/testsuite/tests/quantified-constraints/T17267c.stderr b/testsuite/tests/quantified-constraints/T17267c.stderr
new file mode 100644
index 0000000000..d616794abf
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267c.stderr
@@ -0,0 +1,16 @@
+
+T17267c.hs:22:14: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: C a b
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: r
+      In an equation for ‘oops’: oops r = r
+      In an equation for ‘unsafeCoerce’:
+          unsafeCoerce a
+            = oops (op a :: Thing a b => b)
+            where
+                oops :: (C a b => Thing a b) => (Thing a b => x) -> x
+                oops r = r
diff --git a/testsuite/tests/quantified-constraints/T17267d.hs b/testsuite/tests/quantified-constraints/T17267d.hs
new file mode 100644
index 0000000000..0a9666eb03
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267d.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+-- The instances below have large demands, though I think they're pretty sane.
+{-# LANGUAGE UndecidableInstances #-}
+
+-- This test uses recursive dictionaries
+-- where we do addSolvedDict before solving sub-goals
+
+module Main where
+
+data Foo f a = Foo (f (Maybe a))
+deriving instance Show (f (Maybe a)) => Show (Foo f a)
+deriving instance Functor f => Functor (Foo f)
+
+data Bar x a = Pure a | Bar (x (Bar x) a)
+-- This Show instance is knarly. Basically we ask @x f@ to preserve Show whenever @f@ preserves Show.
+deriving instance (forall f b. (Show b, forall c. Show c => Show (f c))
+                            => Show (x f b), Show a)
+               => Show (Bar x a)
+deriving instance (forall f. Functor f => Functor (x f))
+               => Functor (Bar x)
+
+-- I should now be able to get Show and Functor for @Bar Foo@.
+-- This will involve mutual recursion between the Show/Functor instances for Foo and Bar.
+main :: IO ()
+main = print $ fmap (<> " there") $ Bar $ Foo $ Pure $ Just "Hello"
diff --git a/testsuite/tests/quantified-constraints/T17267d.stdout b/testsuite/tests/quantified-constraints/T17267d.stdout
new file mode 100644
index 0000000000..09bb77d7e9
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T17267d.stdout
@@ -0,0 +1 @@
+Bar (Foo (Pure (Just "Hello there")))
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index da585823b2..7fb728654a 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -21,3 +21,8 @@ test('T15359a', normal, compile, [''])
 test('T15625', normal, compile, [''])
 test('T15625a', normal, compile, [''])
 test('T15918', normal, compile_fail, [''])
+test('T17267', normal, compile_fail, [''])
+test('T17267a', normal, compile_fail, [''])
+test('T17267b', normal, compile_fail, [''])
+test('T17267c', normal, compile_fail, [''])
+test('T17267d', normal, compile_and_run, [''])