[commit: ghc] master: Prevent solveFlatWanteds from losing insolubles when using typechecker plugins (d6f9276)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/d6f92769a89c29a05127cdf5f19dee56fc65dc40/ghc

>---------------------------------------------------------------

commit d6f92769a89c29a05127cdf5f19dee56fc65dc40
Author: Adam Gundry <adam at well-typed.com>
Date:   Thu Dec 4 13:31:08 2014 +0000

    Prevent solveFlatWanteds from losing insolubles when using typechecker plugins
    
    Summary: I've added a Note explaining the problem.
    
    Test Plan:
    validate; we don't have a very good story for testing plugins yet,
    but I've verified that this does at least fix the bug in my plugin.
    
    Reviewers: simonpj, austin
    
    Reviewed By: austin
    
    Subscribers: carter, thomie, gridaphobe, yav
    
    Differential Revision: https://phabricator.haskell.org/D552


>---------------------------------------------------------------

d6f92769a89c29a05127cdf5f19dee56fc65dc40
 compiler/typecheck/TcInteract.hs | 47 +++++++++++++++++++++++++++-------------
 1 file changed, 32 insertions(+), 15 deletions(-)

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index ed686da..a9ed64a 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -110,6 +110,19 @@ to float. This means that
       [w] xxx[1] ~ s
       [W] forall[2] . (xxx[1] ~ Empty)
                    => Intersect (BuriedUnder sub k Empty) inv ~ Empty
+
+Note [Running plugins on unflattened wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+There is an annoying mismatch between solveFlatGivens and
+solveFlatWanteds, because the latter needs to fiddle with the inert
+set, unflatten and and zonk the wanteds.  It passes the zonked wanteds
+to runTcPluginsWanteds, which produces a replacement set of wanteds,
+some additional insolubles and a flag indicating whether to go round
+the loop again.  If so, prepareInertsForImplications is used to remove
+the previous wanteds (which will still be in the inert set).  Note
+that prepareInertsForImplications will discard the insolubles, so we
+must keep track of them separately.
 -}
 
 solveFlatGivens :: CtLoc -> [EvVar] -> TcS ()
@@ -128,21 +141,25 @@ solveFlatGivens loc givens
                    }
 
 solveFlatWanteds :: Cts -> TcS WantedConstraints
-solveFlatWanteds wanteds
-  = do { solveFlats wanteds
-       ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts
-       ; unflattened_eqs <- unflatten tv_eqs fun_eqs
-            -- See Note [Unflatten after solving the flat wanteds]
-
-       ; zonked <- zonkFlats (others `andCts` unflattened_eqs)
-            -- Postcondition is that the wl_flats are zonked
-
-       ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
-       ; if rerun then do { updInertTcS prepareInertsForImplications
-                          ; solveFlatWanteds wanteds' }
-                  else return (WC { wc_flat  = wanteds'
-                                  , wc_insol = insols' `unionBags` insols
-                                  , wc_impl  = implics }) }
+solveFlatWanteds = go emptyBag
+  where
+    go insols0 wanteds
+      = do { solveFlats wanteds
+           ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts
+           ; unflattened_eqs <- unflatten tv_eqs fun_eqs
+              -- See Note [Unflatten after solving the flat wanteds]
+
+           ; zonked <- zonkFlats (others `andCts` unflattened_eqs)
+             -- Postcondition is that the wl_flats are zonked
+
+           ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
+              -- See Note [Running plugins on unflattened wanteds]
+           ; let all_insols = insols0 `unionBags` insols `unionBags` insols'
+           ; if rerun then do { updInertTcS prepareInertsForImplications
+                              ; go all_insols wanteds' }
+                      else return (WC { wc_flat  = wanteds'
+                                      , wc_insol = all_insols
+                                      , wc_impl  = implics }) }
 
 
 -- The main solver loop implements Note [Basic Simplifier Plan]