Introduce warning for loopy superclass solve

Commit aed1974e completely re-engineered the treatment of loopy
superclass dictionaries in instance declarations. Unfortunately,
it has the potential to break (albeit in a rather minor way) user code.

To alleviate migration concerns, this commit re-introduces the old
behaviour. Any reliance on this old behaviour triggers a warning,
controlled by `-Wloopy-superclass-solve`. The warning text explains
that GHC might produce bottoming evidence, and provides a migration
strategy.

This allows us to provide a graceful migration period, alerting users
when they are relying on this unsound behaviour.

Fixes #22912 #22891 #20666 #22894 #22905

2 files changed, 43 insertions, 1 deletions

diff --git a/docs/users_guide/9.6.1-notes.rst b/docs/users_guide/9.6.1-notes.rst
index 34e7723092..36067df41c 100644
--- a/docs/users_guide/9.6.1-notes.rst
+++ b/docs/users_guide/9.6.1-notes.rst
@@ -3,10 +3,36 @@
 Version 9.6.1
 ==============
 
-
 Language
 ~~~~~~~~
 
+- GHC is now more conservative when solving constraints that arise from
+  superclass expansion in terms of other constraints that also arise from
+  superclass expansion.
+
+  For example: ::
+
+    class C a
+    class C a => D a b
+    instance D a a => D a b
+
+  When typechecking the instance, we need to also solve the constraints arising
+  from the superclasses of ``D``; in this case, we need ``C a``. We could obtain
+  evidence for this constraint by expanding the superclasses of the context,
+  as ``D a a`` also has a superclass context of ``C a``.
+  However, is it unsound to do so in general, as we might be assuming precisely
+  the predicate we want to prove! This can lead to programs that loop at runtime.
+
+  When such potentially-loopy situations arise, GHC now emits a warning.
+  In future releases, this behaviour will no longer be supported, and the
+  typechecker will outright refuse to solve these constraints, emitting a
+  ``Could not deduce`` error.
+
+  In practice, you should be able to fix these issues by adding the necessary
+  constraint to the context, e.g. for the above example: ::
+
+    instance (C a, D a a) => D a b
+
 - Record updates for GADTs and other existential datatypes are now
   fully supported.
 
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 2c70006a7c..3624a63384 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -2319,6 +2319,22 @@ of ``-W(no-)*``.
     triggered whenever this happens, and can be addressed by enabling the
     extension.
 
+.. ghc-flag:: -Wloopy-superclass-solve
+    :shortdesc: warn when creating potentially-loopy superclass constraint evidence
+    :type: dynamic
+    :reverse: -Wno-loopy-superclass-solve
+
+    :since: 9.6.1
+
+    As explained in :ref:`undecidable_instances`, when using
+    :extension:`UndecidableInstances` it is possible for GHC to construct
+    non-terminating evidence for certain superclass constraints.
+
+    This behaviour is scheduled to be removed in a future GHC version.
+    In the meantime, GHC emits this warning to inform users of potential
+    non-termination. Users can manually add the required constraint to the context
+    to avoid the problem (thus silencing the warning).
+
 .. ghc-flag:: -Wterm-variable-capture
     :shortdesc: warn when an implicitly quantified type variable captures a term's name
     :type: dynamic