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.

1 files changed, 16 insertions, 0 deletions

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