Update docs for change to type-checking plugins

There was no mention of the changes to type-checking plugins
in the 9.4.1 notes, and the extending_ghc documentation contained
a reference to an outdated type.

docs/users_guide/9.4.1-notes.rst

@@ -72,6 +72,17 @@ Compiler
 - New :ghc-flag:`-fprof-late` that adds automatic CCS annotations to all
   top level functions *after* core optimisation have been run.
 
+- Typechecking plugins now support type-family rewriting. The ``TcPlugin``
+  datatype now contains an extra field, ``tcPluginRewrite``, which allows
+  typechecking plugin authors to specify which type families should be
+  rewritten by the plugin, returning for each type family application a
+  ``TcPluginRewriteResult``.
+  In addition, typechecking plugins now have the ability to emit new constraints
+  at the same time as contradictions. To account for these changes, the
+  ``TcPluginResult`` datatype has been renamed to ``TcPluginSolveResult``,
+  which bundles pattern synonyms ``TcPluginOk`` and ``TcPluginContradiction``
+  to recover the old interface.
+
 - A new type of plugin: defaulting plugins. These plugins can propose
   defaults for ambiguous variables that would otherwise cause errors
   just like the built-in defaulting mechanism.

docs/users_guide/extending_ghc.rst

@@ -582,7 +582,7 @@ is defined thus:
       , tcPluginStop    :: s -> TcPluginM ()
       }
 
-    type TcPluginSolver = [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+    type TcPluginSolver = [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
 
     type TcPluginRewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
 
@@ -615,7 +615,7 @@ The basic idea is as follows:
 
 -  During constraint solving, GHC repeatedly calls ``tcPluginSolve``.
    This function is provided with the current set of constraints, and
-   should return a ``TcPluginResult`` that indicates whether a
+   should return a ``TcPluginSolveResult`` that indicates whether a
    contradiction was found or progress was made. If the plugin solver
    makes progress, GHC will re-start the constraint solving pipeline,
    looping until a fixed point is reached.