Be more careful when iterating the constraint-simpifier loop (fixes Trac #8474)

We were (uselessly) iterating the simplification loop an exponential
number of times.  Lovely simple test case showed this up.

See Note [Cutting off simpl_loop] in TcSimplify

compiler/typecheck/TcSMonad.lhs

@@ -54,11 +54,11 @@ module TcSMonad (
     newDerived,
     
        -- Creation of evidence variables
-    setWantedTyBind,
+    setWantedTyBind, reportUnifications,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
-    getTcEvBindsMap, getTcSTyBinds, getTcSTyBindsMap,
+    getTcEvBindsMap, getTcSTyBindsMap,
 
 
     lookupFlatEqn, newFlattenSkolem,            -- Flatten skolems 
@@ -552,6 +552,9 @@ data InertCans
               --   a |-> ct,co
               -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
               -- And  co : a ~ xi
+              -- Some Refl equalities are also in tcs_ty_binds
+              -- see Note [Spontaneously solved in TyBinds] in TcInteract
+
        , inert_dicts :: CCanMap Class
               -- Dictionaries only, index is the class
               -- NB: index is /not/ the whole type because FD reactions 
@@ -964,18 +967,20 @@ added.  This is initialised from the innermost implication constraint.
 
 \begin{code}
 data TcSEnv
-  = TcSEnv { 
+  = TcSEnv {
       tcs_ev_binds    :: EvBindsVar,
-      
-      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
-          -- Global type bindings
-                     
-      tcs_count      :: IORef Int, -- Global step count
+
+      tcs_ty_binds :: IORef (Bool, TyVarEnv (TcTyVar, TcType)),
+          -- Global type bindings for unification variables
+          -- See Note [Spontaneously solved in TyBinds] in TcInteract
+          -- The "dirty-flag" Bool is set True when we add a binding
+
+      tcs_count    :: IORef Int, -- Global step count
 
       tcs_inerts   :: IORef InertSet, -- Current inert set
       tcs_worklist :: IORef WorkList, -- Current worklist
-      
-      -- Residual implication constraints that are generated 
+
+      -- Residual implication constraints that are generated
       -- while solving or canonicalising the current worklist.
       -- Specifically, when canonicalising (forall a. t1 ~ forall a. t2)
       -- from which we get the implication (forall a. t1 ~ t2)
@@ -1053,7 +1058,7 @@ runTcSWithEvBinds :: EvBindsVar
                   -> TcS a 
                   -> TcM a
 runTcSWithEvBinds ev_binds_var tcs
-  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
+  = do { ty_binds_var <- TcM.newTcRef (False, emptyVarEnv)
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef is 
 
@@ -1068,7 +1073,7 @@ runTcSWithEvBinds ev_binds_var tcs
 	     -- Run the computation
        ; res <- unTcS tcs env
 	     -- Perform the type unifications required
-       ; ty_binds <- TcM.readTcRef ty_binds_var
+       ; (_, ty_binds) <- TcM.readTcRef ty_binds_var
        ; mapM_ do_unification (varEnvElts ty_binds)
 
 #ifdef DEBUG
@@ -1148,13 +1153,15 @@ nestTcS (TcS thing_inside)
        ; thing_inside nest_env }
 
 tryTcS :: TcS a -> TcS a
--- Like runTcS, but from within the TcS monad 
--- Completely afresh inerts and worklist, be careful! 
--- Moreover, we will simply throw away all the evidence generated. 
+-- Like runTcS, but from within the TcS monad
+-- Completely fresh inerts and worklist, be careful!
+-- Moreover, we will simply throw away all the evidence generated.
+-- We have a completely empty tcs_ty_binds too, so make sure the
+-- input stuff is fully rewritten wrt any outer inerts
 tryTcS (TcS thing_inside)
-  = TcS $ \env -> 
+  = TcS $ \env ->
     do { is_var <- TcM.newTcRef emptyInert
-       ; ty_binds_var <- TcM.newTcRef emptyVarEnv
+       ; ty_binds_var <- TcM.newTcRef (False, emptyVarEnv)
        ; ev_binds_var <- TcM.newTcEvBinds
 
        ; let nest_env = env { tcs_ev_binds = ev_binds_var
@@ -1243,11 +1250,13 @@ getUntouchables = wrapTcS TcM.getUntouchables
 getFlattenSkols :: TcS [TcTyVar]
 getFlattenSkols = do { is <- getTcSInerts; return (inert_fsks is) }
 
-getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
+getTcSTyBinds :: TcS (IORef (Bool, TyVarEnv (TcTyVar, TcType)))
 getTcSTyBinds = TcS (return . tcs_ty_binds)
 
 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
-getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
+getTcSTyBindsMap = do { ref <- getTcSTyBinds
+                      ; wrapTcS $ do { (_, binds) <- TcM.readTcRef ref
+                                     ; return binds } }
 
 getTcEvBindsMap :: TcS EvBindMap
 getTcEvBindsMap
@@ -1261,14 +1270,30 @@ setWantedTyBind tv ty
   = ASSERT2( isMetaTyVar tv, ppr tv )
     do { ref <- getTcSTyBinds
        ; wrapTcS $ 
-         do { ty_binds <- TcM.readTcRef ref
+         do { (_dirty, ty_binds) <- TcM.readTcRef ref
             ; when debugIsOn $
                   TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
                   vcat [ text "TERRIBLE ERROR: double set of meta type variable"
                        , ppr tv <+> text ":=" <+> ppr ty
                        , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
             ; TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
-            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
+            ; TcM.writeTcRef ref (True, extendVarEnv ty_binds tv (tv,ty)) } }
+
+reportUnifications :: TcS a -> TcS (Bool, a)
+reportUnifications thing_inside
+  = do { ty_binds_var <- getTcSTyBinds
+       ; outer_dirty <- wrapTcS $
+            do { (outer_dirty, binds1) <- TcM.readTcRef ty_binds_var
+               ; TcM.writeTcRef ty_binds_var (False, binds1)
+               ; return outer_dirty }
+      ; res <- thing_inside
+      ; wrapTcS $
+        do { (inner_dirty, binds2) <- TcM.readTcRef ty_binds_var
+           ; if inner_dirty then
+                 return (True, res)
+             else
+                do { TcM.writeTcRef ty_binds_var (outer_dirty, binds2)
+                   ; return (False, res) } } }
 \end{code}
 
 \begin{code}

compiler/typecheck/TcSimplify.lhs

@@ -671,18 +671,23 @@ simpl_loop :: Int
            -> Bag Implication
            -> TcS (Bag Implication)
 simpl_loop n implics
-  | n > 10 
+  | n > 10
   = traceTcS "solveWanteds: loop!" empty >> return implics
-  | otherwise 
+  | otherwise
   = do { traceTcS "simpl_loop, iteration" (int n)
        ; (floated_eqs, unsolved_implics) <- solveNestedImplications implics
-       ; if isEmptyBag floated_eqs 
-         then return unsolved_implics 
-         else 
+       ; if isEmptyBag floated_eqs
+         then return unsolved_implics
+         else
     do {   -- Put floated_eqs into the current inert set before looping
-         impls_from_eqs <- solveInteract floated_eqs
-       ; simpl_loop (n+1) (unsolved_implics `unionBags` impls_from_eqs)} }
-
+         (unifs_happened, impls_from_eqs) <- reportUnifications $
+                                             solveInteract floated_eqs
+       ; if   -- See Note [Cutting off simpl_loop]
+              isEmptyBag impls_from_eqs &&
+              not unifs_happened &&                 -- (a)
+              not (anyBag isCFunEqCan floated_eqs)  -- (b)
+         then return unsolved_implics
+         else simpl_loop (n+1) (unsolved_implics `unionBags` impls_from_eqs) } }
 
 solveNestedImplications :: Bag Implication
                         -> TcS (Cts, Bag Implication)
@@ -761,6 +766,43 @@ solveImplication inerts
        ; return (floated_eqs, res_implic) }
 \end{code}
 
+Note [Cutting off simpl_loop]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is very important not to iterate in simpl_loop unless there is a chance
+of progress.  Trac #8474 is a classic example:
+
+  * There's a deeply-nested chain of implication constraints.
+       ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
+
+  * From the innermost one we get a [D] alpha ~ Int,
+    but alpha is untouchable until we get out to the outermost one
+
+  * We float [D] alpha~Int out (it is in floated_eqs), but since alpha
+    is untouchable, the solveInteract in simpl_loop makes no progress
+
+  * So there is no point in attempting to re-solve
+       ?yn:betan => [W] ?x:Int
+    because we'll just get the same [D] again
+
+  * If we *do* re-solve, we'll get an ininite loop. It is cut off by
+    the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
+    exponentially many) iterations!
+
+Conclusion: we should iterate simpl_loop iff we will get more 'givens'
+in the inert set when solving the nested implications.  That is the
+result of prepareInertsForImplications is larger.  How can we tell
+this?
+
+Consider floated_eqs (all wanted or derived):
+
+(a) [W/D] CTyEqCan (a ~ ty).  This can give rise to a new given only by causing
+    a unification. So we count those unifications.
+
+(b) [W] CFunEqCan (F tys ~ xi).  Even though these are wanted, they
+    are pushed in as givens by prepareInertsForImplications.  See Note
+    [Preparing inert set for implications] in TcSMonad.  But because
+    of that very fact, we won't generate another copy if we iterate
+    simpl_loop.  So we iterate if there any of these
 
 \begin{code}
 floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints