Do not add a 'solved dict' for quantified constraints

GHC has a wonderful-but-delicate mechanism for building recursive
dictionaries by adding a goal to the "solved dictionaries" before
solving the sub-goals.  See Note [Solved dictionaries] in TcSMonad

Ticket #17267 showed that if you use this mechanism for local
/quantified/ constraints you can get a loop -- or even unsafe
coerce.   This patch fixes the bug.

Specifically

* Make TcSMonad.addSolvedDict be conditional on using a
  /top level/ instance, not a quantified one.

* Moreover, we /also/ don't want to add a solved dict
  for equalities (a~b).

* Add lots more comments to Note [Solved dictionaries]
  to explain the above cryptic stuff.

* Extend InstanceWhat to identify those strange built-in
  equality instances.

A couple of other things along the way

* Delete the unused Type.isIPPred_maybe.

* Stop making addSolvedDict conditional on not being an
  impolicit parameter.  This comes from way back. But
  it's irrelevant now because IP dicts are never solved
  via an instance.

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, [''])