TcPlugins: solve and report contras simultaneously

This changes the TcPlugin datatype to allow type-checking plugins
to report insoluble constraints while at the same time solve
some other constraints. This allows better error messages, as
the plugin can still simplify constraints, even when it wishes
to report a contradiction.

Pattern synonyms TcPluginContradiction and TcPluginOk are provided
for backwards compatibility: existing type-checking plugins should
continue to work without modification.

3 files changed, 68 insertions, 35 deletions

diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 98824022cd..72f4a509c4 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -287,15 +287,18 @@ runTcPluginSolvers solvers all_cts
         return $ progress p result
 
     progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
-    progress p (TcPluginContradiction bad_cts) =
-       p { pluginInputCts = discard bad_cts (pluginInputCts p)
-         , pluginBadCts   = bad_cts ++ pluginBadCts p
-         }
-    progress p (TcPluginOk solved_cts new_cts) =
-      p { pluginInputCts  = discard (map snd solved_cts) (pluginInputCts p)
-        , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
-        , pluginNewCts    = new_cts ++ pluginNewCts p
+    progress p
+      (TcPluginSolveResult
+        { tcPluginInsolubleCts = bad_cts
+        , tcPluginSolvedCts    = solved_cts
+        , tcPluginNewCts       = new_cts
         }
+      ) =
+        p { pluginInputCts  = discard (bad_cts ++ map snd solved_cts) (pluginInputCts p)
+          , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
+          , pluginNewCts    = new_cts ++ pluginNewCts p
+          , pluginBadCts    = bad_cts ++ pluginBadCts p
+          }
 
     initialProgress = TcPluginProgress all_cts ([], [], []) [] []
 
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index 2894321546..34d2c2e578 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE ExistentialQuantification  #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PatternSynonyms            #-}
 
 {-
 (c) The University of Glasgow 2006-2012
@@ -74,7 +75,9 @@ module GHC.Tc.Types(
         getPlatform,
 
         -- Constraint solver plugins
-        TcPlugin(..), TcPluginSolveResult(..), TcPluginRewriteResult(..),
+        TcPlugin(..),
+        TcPluginSolveResult(TcPluginContradiction, TcPluginOk, ..),
+        TcPluginRewriteResult(..),
         TcPluginSolver, TcPluginRewriter,
         TcPluginM(runTcPluginM), unsafeTcPluginTcM,
 
@@ -1774,23 +1777,48 @@ data TcPlugin = forall s. TcPlugin
    -- ^ Clean up after the plugin, when exiting the type-checker.
   }
 
+-- | The plugin found a contradiction.
+-- The returned constraints are removed from the inert set,
+-- and recorded as insoluble.
+--
+-- The returned list of constraints should never be empty.
+pattern TcPluginContradiction :: [Ct] -> TcPluginSolveResult
+pattern TcPluginContradiction insols
+  = TcPluginSolveResult
+  { tcPluginInsolubleCts = insols
+  , tcPluginSolvedCts    = []
+  , tcPluginNewCts       = [] }
+
+-- | The plugin has not found any contradictions,
+--
+-- The first field is for constraints that were solved.
+-- The second field contains new work, that should be processed by
+-- the constraint solver.
+pattern TcPluginOk :: [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
+pattern TcPluginOk solved new
+  = TcPluginSolveResult
+  { tcPluginInsolubleCts = []
+  , tcPluginSolvedCts    = solved
+  , tcPluginNewCts       = new }
+
+-- | Result of running a solver plugin.
 data TcPluginSolveResult
-  = TcPluginContradiction [Ct]
-    -- ^ The plugin found a contradiction.
-    -- The returned constraints are removed from the inert set,
-    -- and recorded as insoluble.
+  = TcPluginSolveResult
+  { -- | Insoluble constraints found by the plugin.
     --
-    -- The returned list of constraints should never be empty.
-
-  | TcPluginOk
-    { tcPluginSolvedCts :: [(EvTerm,Ct)]
-    , tcPluginNewCts :: [Ct] }
-    -- ^ The first field is for constraints that were solved.
-    -- These are removed from the inert set,
-    -- and the evidence for them is recorded.
-    -- The second field contains new work, that should be processed by
-    -- the constraint solver.
-
+    -- These constraints will be added to the inert set,
+    -- and reported as insoluble to the user.
+    tcPluginInsolubleCts :: [Ct]
+    -- | Solved constraints, together with their evidence.
+    --
+    -- These are removed from the inert set, and the
+    -- evidence for them is recorded.
+  , tcPluginSolvedCts :: [(EvTerm, Ct)]
+    -- | New constraints that the plugin wishes to emit.
+    --
+    -- These will be added to the work list.
+  , tcPluginNewCts :: [Ct]
+  }
 
 data TcPluginRewriteResult
   =
diff --git a/docs/users_guide/extending_ghc.rst b/docs/users_guide/extending_ghc.rst
index 0020c0213f..7b3f7f0a78 100644
--- a/docs/users_guide/extending_ghc.rst
+++ b/docs/users_guide/extending_ghc.rst
@@ -555,11 +555,12 @@ is defined thus:
 
     type TcPluginRewriter = RewriteEnv -> [Ct] -> [Type] -> TcPluginM TcPluginRewriteResult
 
-    data TcPluginResult
-      = TcPluginContradiction [Ct]
-      | TcPluginOk
-        { tcPluginSolvedCts :: [(EvTerm,Ct)]
-        , tcPluginNewCts :: [Ct] }
+  data TcPluginSolveResult
+    = TcPluginSolveResult
+        { tcPluginInsolubleCts :: [Ct]
+        , tcPluginSolvedCts    :: [(EvTerm, Ct)]
+        , tcPluginNewCts       :: [Ct]
+        }
 
     data TcPluginRewriteResult
       = TcPluginNoRewrite
@@ -634,19 +635,20 @@ The two ways can be distinguished by checking the Wanted constraints: in the
 first case (and the first case only), the plugin will be passed an empty list
 of Wanted constraints.
 
-The plugin is then expected to respond in either of the following ways:
+The plugin can then respond with:
 
-* return ``TcPluginOk`` with lists of solved and new constraints, or
+* solved constraints, which will be removed from the inert set,
 
-* return ``TcPluginContradiction`` with a list of impossible
-  constraints, so they can be turned into errors.
+* new constraints, which will be added to the work list,
 
-In both cases, the plugin must respond with constraints of the same flavour,
+* insoluble constraints, which will be reported as errors.
+
+The plugin must respond with constraints of the same flavour,
 i.e. in (1) it should return only Givens, and for (2) it should return only
 Wanteds (or Deriveds); all other constraints will be ignored.
 
 If the plugin cannot make any progress, it should return
-``TcPluginOk [] []``. Otherwise, if there were any new constraints, the
+``TcPluginSolveResult [] [] []``. Otherwise, if there were any new constraints, the
 main constraint solver will be re-invoked to simplify them, then the
 plugin will be invoked again. The plugin is responsible for making sure
 that this process eventually terminates.