A collection of type-inference refactorings.
[ghc.git] / compiler / typecheck / TcSMonad.hs
index 29837a9..0174b4a 100644 (file)
@@ -41,8 +41,8 @@ module TcSMonad (
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getLclEnv,
-    getTcEvBinds, getTcEvBindsFromVar, getTcLevel,
-    getTcEvBindsMap,
+    getTcEvBindsVar, getTcLevel,
+    getTcEvBindsAndTCVs, getTcEvBindsMap,
     tcLookupClass,
 
     -- Inerts
@@ -66,7 +66,7 @@ module TcSMonad (
 
     -- Inert CDictCans
     lookupInertDict, findDictsByClass, addDict, addDictsByClass,
-    delDict, partitionDicts, foldDicts, filterDicts,
+    delDict, foldDicts, filterDicts,
 
     -- Inert CTyEqCans
     EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
@@ -81,8 +81,8 @@ module TcSMonad (
     lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
 
     -- Inert CFunEqCans
-    updInertFunEqs, findFunEq, sizeFunEqMap, filterFunEqs,
-    findFunEqsByTyCon, partitionFunEqs, foldFunEqs,
+    updInertFunEqs, findFunEq, sizeFunEqMap,
+    findFunEqsByTyCon,
 
     instDFunType,                              -- Instantiation
 
@@ -394,7 +394,7 @@ dictionary to the inert_solved_dicts.  In general, we use it to avoid
 creating a new EvVar when we have a new goal that we have solved in
 the past.
 
-But in particular, we can use it to create *recursive* dicationaries.
+But in particular, we can use it to create *recursive* dictionaries.
 The simplest, degnerate case is
     instance C [a] => C [a] where ...
 If we have
@@ -665,11 +665,12 @@ Note [inert_model: the inert model]
        decomposing injective arguments of type functions, and
        suchlike.
 
-     - A Derived "shadow copy" for every Given or Wanted (a ~N ty) in
-       inert_eqs.
+     - A Derived "shadow copy" for every Wanted (a ~N ty) in
+       inert_eqs.  (Originally included every Given too; but
+       see Note [Add derived shadows only for Wanteds])
 
    * The model is not subject to "kicking-out". Reason: we make a Derived
-     shadow copy of any Given/Wanted (a ~ ty), and that Derived copy will
+     shadow copy of any Wanted (a ~ ty), and that Derived copy will
      be fully rewritten by the model before it is added
 
    * The principal reason for maintaining the model is to generate
@@ -1123,26 +1124,22 @@ Note [Adding an inert canonical constraint the InertCans]
              NB: 'a' cannot be in fv(ty), because the constraint is canonical.
 
           2. (DShadow) Do emitDerivedShadows
-               For every inert G/W constraint c, st
+               For every inert [W] constraint c, st
                 (a) (a~ty) can rewrite c (see Note [Emitting shadow constraints]),
                     and
                 (b) the model cannot rewrite c
                kick out a Derived *copy*, leaving the original unchanged.
                Reason for (b) if the model can rewrite c, then we have already
                generated a shadow copy
+               See Note [Add derived shadows only for Wanteds]
 
        [Given/Wanted Nominal]  [G/W] a ~N ty:
           1. Add it to inert_eqs
-          2. Emit [D] a~ty
-          Step (2) is needed to allow the current model to fully
-          rewrite [D] a~ty before adding it using the [Derived Nominal]
-          steps above.
-
-          We must do this even for Givens, because
-             work-item [G] a ~ [b], model has [D] b ~ a.
-          We need a shadow [D] a ~ [b] in the work-list
-          When we process it, we'll rewrite to a ~ [a] and get an occurs check
-
+          2. For [W], Emit [D] a~ty
+             Step (2) is needed to allow the current model to fully
+             rewrite [D] a~ty before adding it using the [Derived Nominal]
+             steps above.
+             See Note [Add derived shadows only for Wanteds]
 
 * Unifying a:=ty, is like adding [G] a~ty, but we can't make a [D]
   a~ty, as in step (1) of the [G/W] case above.  So instead, do
@@ -1262,7 +1259,7 @@ emitDerivedShadows IC { inert_eqs      = tv_eqs
                   | otherwise      = cts
 
     want_shadow ct
-      =  not (isDerivedCt ct)              -- No need for a shadow of a Derived!
+      =  isWantedCt ct                     -- See Note [Add shadows only for Wanteds]
       && (new_tv `elemVarSet` rw_tvs)      -- New tv can rewrite ct, yielding a
                                            -- different ct
       && not (modelCanRewrite model rw_tvs)-- We have not already created a
@@ -1284,7 +1281,31 @@ mkShadowCt ct
     derived_ev = CtDerived { ctev_pred = ctEvPred ev
                            , ctev_loc  = ctEvLoc ev }
 
-{- Note [Keep CDictCan shadows as CDictCan]
+{- Note [Add derived shadows only for Wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We now only add shadows for Wanted constraints.  Why add derived
+shadows for Givens?  After all, Givens can rewrite Deriveds.  But
+Deriveds can't rewrite Givens.  So in principle, if we created a
+Derived shadow of a Given, it could be rewritten by other Deriveds,
+and that could, conceivably, lead to a useful unification.
+
+But (a) I have been unable to come up with an example of this
+happening and (b) see Trac #12660 for how adding the derived shadows
+of a Given led to an infinite loop.  For (b) there may be other
+ways to solve the loop, but simply reraining from adding
+derived shadows of Givens is particularly simple.  And it's more
+efficient too!
+
+Still, here's one possible reason for adding derived shadows
+for Givens.  Consider
+           work-item [G] a ~ [b], model has [D] b ~ a.
+If we added the derived shadow (into the work list)
+         [D] a ~ [b]
+When we process it, we'll rewrite to a ~ [a] and get an
+occurs check.  Without it we'll miss the occurs check (reporting
+inaccessible code); but that's probably OK.
+
+Note [Keep CDictCan shadows as CDictCan]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have
   class C a => D a b
@@ -1334,7 +1355,8 @@ addInertCan ct
        -- Emit shadow derived if necessary
        -- See Note [Emitting shadow constraints]
        ; let rw_tvs = rewritableTyCoVars ct
-       ; when (not (isDerivedCt ct) && modelCanRewrite (inert_model ics) rw_tvs)
+       ; when (isWantedCt ct && modelCanRewrite (inert_model ics) rw_tvs)
+              -- See Note [Add shadows only for Wanteds]
               (emitWork [mkShadowCt ct])
 
        ; traceTcS "addInertCan }" $ empty }
@@ -1631,7 +1653,7 @@ After solving the Givens we take two things out of the inert set
            We get [D] 1 <= n, and we must remove it!
          Otherwise we unflatten it more then once, and assign
          to its fmv more than once...disaster.
-     It's ok to remove them because they turned not not to
+     It's ok to remove them because they turned out not to
      yield an insoluble, and hence have now done their work.
 -}
 
@@ -1774,19 +1796,23 @@ isInInertEqs eqs tv rhs
       , rhs `eqType` rhs2 = True
       | otherwise         = False
 
-getNoGivenEqs :: TcLevel     -- TcLevel of this implication
+getNoGivenEqs :: TcLevel          -- TcLevel of this implication
                -> [TcTyVar]       -- Skolems of this implication
+               -> Cts             -- Given insolubles from solveGivens
                -> TcS Bool        -- True <=> definitely no residual given equalities
 -- See Note [When does an implication have given equalities?]
-getNoGivenEqs tclvl skol_tvs
-  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
+getNoGivenEqs tclvl skol_tvs given_insols
+  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
+                    , inert_funeqs = funeqs })
              <- getInertCans
        ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
 
-             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence)  False iirreds
+             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
+                                      (iirreds `unionBags` given_insols)
                           || anyDVarEnv (eqs_given_here local_fsks) ieqs
 
-       ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
+       ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
+                                        , ppr given_insols])
        ; return (not has_given_eqs) }
   where
     eqs_given_here :: VarSet -> EqualCtList -> Bool
@@ -2220,11 +2246,6 @@ filterFunEqs = filterTcAppMap
 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
 
--- insertFunEqCt :: FunEqMap Ct -> Ct -> FunEqMap Ct
--- insertFunEqCt m ct@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
---  = insertFunEq m tc tys ct
--- insertFunEqCt _ ct = pprPanic "insertFunEqCt" (ppr ct)
-
 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
 -- Optimise for the case where the predicate is false
 -- partitionFunEqs is called only from kick-out, and kick-out usually
@@ -2288,9 +2309,7 @@ should do two things differently:
 
 data TcSEnv
   = TcSEnv {
-      tcs_ev_binds    :: Maybe EvBindsVar,
-          -- this could be Nothing if we can't deal with non-equality
-          -- constraints, because, say, we're in a top-level type signature
+      tcs_ev_binds    :: EvBindsVar,
 
       tcs_unified     :: IORef Int,
          -- The number of unification variables we have filled
@@ -2304,10 +2323,6 @@ data TcSEnv
       -- See Note [Work list priorities] and
       tcs_worklist  :: IORef WorkList, -- Current worklist
 
-      tcs_used_tcvs :: IORef TyCoVarSet,
-        -- these variables were used when filling holes. Don't discard!
-        -- See also Note [Tracking redundant constraints] in TcSimplify
-
       tcs_need_deriveds :: Bool
         -- Keep solving, even if all the unsolved constraints are Derived
         -- See Note [Solving for Derived constraints]
@@ -2365,7 +2380,7 @@ traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 
 runTcPluginTcS :: TcPluginM a -> TcS a
-runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBinds
+runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
 
 instance HasDynFlags TcS where
     getDynFlags = wrapTcS getDynFlags
@@ -2378,11 +2393,6 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                     ; n <- TcM.readTcRef ref
                                     ; TcM.writeTcRef ref (n+1) }
 
--- | Mark variables as used filling a coercion hole
-useVars :: TyCoVarSet -> TcS ()
-useVars vars = TcS $ \env -> do { let ref = tcs_used_tcvs env
-                                ; TcM.updTcRef ref (`unionVarSet` vars) }
-
 csTraceTcS :: SDoc -> TcS ()
 csTraceTcS doc
   = wrapTcS $ csTraceTcM 1 (return doc)
@@ -2411,7 +2421,7 @@ runTcS :: TcS a                -- What to run
        -> TcM (a, EvBindMap)
 runTcS tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; res <- runTcSWithEvBinds False (Just ev_binds_var) tcs
+       ; res <- runTcSWithEvBinds False ev_binds_var tcs
        ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
        ; return (res, ev_binds) }
 
@@ -2421,14 +2431,16 @@ runTcS tcs
 runTcSDeriveds :: TcS a -> TcM a
 runTcSDeriveds tcs
   = do { ev_binds_var <- TcM.newTcEvBinds
-       ; runTcSWithEvBinds True (Just ev_binds_var) tcs }
+       ; runTcSWithEvBinds True ev_binds_var tcs }
 
 -- | This can deal only with equality constraints.
 runTcSEqualities :: TcS a -> TcM a
-runTcSEqualities = runTcSWithEvBinds False Nothing
+runTcSEqualities thing_inside
+  = do { ev_binds_var <- TcM.newTcEvBinds
+       ; runTcSWithEvBinds False ev_binds_var thing_inside }
 
 runTcSWithEvBinds :: Bool  -- ^ keep running even if only Deriveds are left?
-                  -> Maybe EvBindsVar
+                  -> EvBindsVar
                   -> TcS a
                   -> TcM a
 runTcSWithEvBinds solve_deriveds ev_binds_var tcs
@@ -2436,15 +2448,11 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs
        ; step_count <- TcM.newTcRef 0
        ; inert_var <- TcM.newTcRef emptyInert
        ; wl_var <- TcM.newTcRef emptyWorkList
-       ; used_var <- TcM.newTcRef emptyVarSet -- never read from, but see
-                                              -- nestImplicTcS
-
        ; let env = TcSEnv { tcs_ev_binds      = ev_binds_var
                           , tcs_unified       = unified_var
                           , tcs_count         = step_count
                           , tcs_inerts        = inert_var
                           , tcs_worklist      = wl_var
-                          , tcs_used_tcvs     = used_var
                           , tcs_need_deriveds = solve_deriveds }
 
              -- Run the computation
@@ -2455,16 +2463,15 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs
          csTraceTcM 0 $ return (text "Constraint solver steps =" <+> int count)
 
 #ifdef DEBUG
-       ; whenIsJust ev_binds_var $ \ebv ->
-         do { ev_binds <- TcM.getTcEvBinds ebv
-            ; checkForCyclicBinds ev_binds }
+       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
+       ; checkForCyclicBinds ev_binds
 #endif
 
        ; return res }
 
 #ifdef DEBUG
-checkForCyclicBinds :: Bag EvBind -> TcM ()
-checkForCyclicBinds ev_binds
+checkForCyclicBinds :: EvBindMap -> TcM ()
+checkForCyclicBinds ev_binds_map
   | null cycles
   = return ()
   | null coercion_cycles
@@ -2472,6 +2479,8 @@ checkForCyclicBinds ev_binds
   | otherwise
   = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
   where
+    ev_binds = evBindMapBinds ev_binds_map
+
     cycles :: [[EvBind]]
     cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
 
@@ -2487,57 +2496,39 @@ checkForCyclicBinds ev_binds
             -- Note [Deterministic SCC] in Digraph.
 #endif
 
-setEvBindsTcS :: Maybe EvBindsVar -> TcS a -> TcS a
-setEvBindsTcS m_ref (TcS thing_inside)
- = TcS $ \ env -> thing_inside (env { tcs_ev_binds = m_ref })
+setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
+setEvBindsTcS ref (TcS thing_inside)
+ = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
 
-nestImplicTcS :: Maybe EvBindsVar -> TyCoVarSet -- bound in this implication
+nestImplicTcS :: EvBindsVar
               -> TcLevel -> TcS a
-              -> TcS (a, TyCoVarSet)  -- also returns any vars used when filling
-                                      -- coercion holes (for redundant-constraint
-                                      -- tracking)
-nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside)
-  = do { (res, used_tcvs) <-
-         TcS $ \ TcSEnv { tcs_unified       = unified_var
-                        , tcs_inerts        = old_inert_var
-                        , tcs_count         = count
-                        , tcs_need_deriveds = solve_deriveds
-                        } ->
-      do { inerts <- TcM.readTcRef old_inert_var
-         ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
+              -> TcS a
+nestImplicTcS ref inner_tclvl (TcS thing_inside)
+  = TcS $ \ TcSEnv { tcs_unified       = unified_var
+                   , tcs_inerts        = old_inert_var
+                   , tcs_count         = count
+                   , tcs_need_deriveds = solve_deriveds
+                   } ->
+    do { inerts <- TcM.readTcRef old_inert_var
+       ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
                                      -- See Note [Do not inherit the flat cache]
-         ; new_inert_var <- TcM.newTcRef nest_inert
-         ; new_wl_var    <- TcM.newTcRef emptyWorkList
-         ; new_used_var  <- TcM.newTcRef emptyVarSet
-         ; let nest_env = TcSEnv { tcs_ev_binds      = m_ref
-                                 , tcs_unified       = unified_var
-                                 , tcs_count         = count
-                                 , tcs_inerts        = new_inert_var
-                                 , tcs_worklist      = new_wl_var
-                                 , tcs_used_tcvs     = new_used_var
-                                 , tcs_need_deriveds = solve_deriveds }
-         ; res <- TcM.setTcLevel inner_tclvl $
-                  thing_inside nest_env
+       ; new_inert_var <- TcM.newTcRef nest_inert
+       ; new_wl_var    <- TcM.newTcRef emptyWorkList
+       ; let nest_env = TcSEnv { tcs_ev_binds      = ref
+                               , tcs_unified       = unified_var
+                               , tcs_count         = count
+                               , tcs_inerts        = new_inert_var
+                               , tcs_worklist      = new_wl_var
+                               , tcs_need_deriveds = solve_deriveds }
+       ; res <- TcM.setTcLevel inner_tclvl $
+                thing_inside nest_env
 
 #ifdef DEBUG
-         -- Perform a check that the thing_inside did not cause cycles
-         ; whenIsJust m_ref $ \ ref ->
-           do { ev_binds <- TcM.getTcEvBinds ref
-              ; checkForCyclicBinds ev_binds }
+       -- Perform a check that the thing_inside did not cause cycles
+       ; ev_binds <- TcM.getTcEvBindsMap ref
+       ; checkForCyclicBinds ev_binds
 #endif
-         ; used_tcvs <- TcM.readTcRef new_used_var
-         ; return (res, used_tcvs) }
-
-       ; local_ev_vars <- case m_ref of
-           Nothing  -> return emptyVarSet
-           Just ref -> do { binds <- wrapTcS $ TcM.getTcEvBinds ref
-                          ; return $ mkVarSet $ map evBindVar $ bagToList binds }
-       ; let all_locals = bound_tcvs `unionVarSet` local_ev_vars
-             (inner_used_tcvs, outer_used_tcvs)
-               = partitionVarSet (`elemVarSet` all_locals) used_tcvs
-       ; useVars outer_used_tcvs
-
-       ; return (res, inner_used_tcvs) }
+       ; return res }
 
 {- Note [Do not inherit the flat cache]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2555,7 +2546,7 @@ nestTcS ::  TcS a -> TcS a
 -- Use the current untouchables, augmenting the current
 -- evidence bindings, and solved dictionaries
 -- But have no effect on the InertCans, or on the inert_flat_cache
---  (the latter because the thing inside a nestTcS does unflattening)
+-- (we want to inherit the latter from processing the Givens)
 nestTcS (TcS thing_inside)
   = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
     do { inerts <- TcM.readTcRef inerts_var
@@ -2661,21 +2652,22 @@ readTcRef ref = wrapTcS (TcM.readTcRef ref)
 updTcRef :: TcRef a -> (a->a) -> TcS ()
 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
 
-getTcEvBinds :: TcS (Maybe EvBindsVar)
-getTcEvBinds = TcS (return . tcs_ev_binds)
-
-getTcEvBindsFromVar :: EvBindsVar -> TcS (Bag EvBind)
-getTcEvBindsFromVar = wrapTcS . TcM.getTcEvBinds
+getTcEvBindsVar :: TcS EvBindsVar
+getTcEvBindsVar = TcS (return . tcs_ev_binds)
 
 getTcLevel :: TcS TcLevel
 getTcLevel = wrapTcS TcM.getTcLevel
 
+getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet)
+getTcEvBindsAndTCVs ev_binds_var
+  = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var
+                 ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
+                 ; return (bnds, tcvs) }
+
 getTcEvBindsMap :: TcS EvBindMap
 getTcEvBindsMap
-  = do { ev_binds <- getTcEvBinds
-       ; case ev_binds of
-           Just (EvBindsVar ev_ref _) -> wrapTcS $ TcM.readTcRef ev_ref
-           Nothing                    -> return emptyEvBindMap }
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
 
 unifyTyVar :: TcTyVar -> TcType -> TcS ()
 -- Unify a meta-tyvar with a type
@@ -2935,10 +2927,17 @@ getEvTerm (Cached evt) = evt
 
 setEvBind :: EvBind -> TcS ()
 setEvBind ev_bind
-  = do { tc_evbinds <- getTcEvBinds
-       ; case tc_evbinds of
-           Just evb -> wrapTcS $ TcM.addTcEvBind evb ev_bind
-           Nothing  -> pprPanic "setEvBind" (ppr ev_bind) }
+  = do { evb <- getTcEvBindsVar
+       ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
+
+-- | Mark variables as used filling a coercion hole
+useVars :: TyCoVarSet -> TcS ()
+useVars vars
+  = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar
+       ; wrapTcS $
+         do { tcvs <- TcM.readTcRef ref
+            ; let tcvs' = tcvs `unionVarSet` vars
+            ; TcM.writeTcRef ref tcvs' } }
 
 -- | Equalities only
 setWantedEq :: TcEvDest -> Coercion -> TcS ()
@@ -3085,7 +3084,17 @@ matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
 matchFamTcM tycon args
   = do { fam_envs <- FamInst.tcGetFamInstEnvs
-       ; return $ reduceTyFamApp_maybe fam_envs Nominal tycon args }
+       ; let match_fam_result
+              = reduceTyFamApp_maybe fam_envs Nominal tycon args
+       ; TcM.traceTc "matchFamTcM" $
+         vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
+              , ppr_res match_fam_result ]
+       ; return match_fam_result }
+  where
+    ppr_res Nothing        = text "Match failed"
+    ppr_res (Just (co,ty)) = hang (text "Match succeeded:")
+                                2 (vcat [ text "Rewrites to:" <+> ppr ty
+                                        , text "Coercion:" <+> ppr co ])
 
 {-
 Note [Residual implications]
@@ -3119,6 +3128,10 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
 
       ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
       ; env <- getLclEnv
+      ; ev_binds <- newTcEvBinds
+           -- We have nowhere to put these bindings
+           -- but TcSimplify.setImplicationStatus
+           -- checks that we don't actually use them
       ; let new_tclvl = pushTcLevel (tcl_tclvl env)
             wc        = WC { wc_simple = singleCt (mkNonCanonical ctev)
                            , wc_impl   = emptyBag
@@ -3129,7 +3142,7 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
                                , ic_given  = []
                                , ic_wanted = wc
                                , ic_status = IC_Unsolved
-                               , ic_binds  = Nothing -- no place to put binds
+                               , ic_binds  = ev_binds
                                , ic_env    = env
                                , ic_info   = skol_info }
       ; updWorkListTcS (extendWorkListImplic imp)