diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index f8c5e04e3eeedf834cc32369251c7fde2338c6e8..1dc8713a1424c3f20ff84b7ada006988dd4dca04 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/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}
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 1d8a9208391e7bce7b9a3987f8e85655d89bd5a4..14d7af5f01afa6954cc854fbc5141de87700abad 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/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