A bunch more simplification and refactoring to the constraint solver
authorSimon Peyton Jones <simonpj@microsoft.com>
Sat, 1 Sep 2012 10:25:47 +0000 (11:25 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Sat, 1 Sep 2012 10:25:47 +0000 (11:25 +0100)
* Instead of Untouchables being a [Unique], it is simply an Int
  indicating the depth of nesting.  This works fine now that
  floatEqualities is promoting the floated unification variables
  to the outer level

* Remove the inert_tv_eqs (InScopeSet) from InertCans.  It wasn't
  being used.  See Note [Shadowing in a constraint] in TcRnTypes

* Rename inert_frozen to inert_insols

* Some simple refactoring in
     TcErrors.reportFlatsAndInsols
     TcInteract.kickOutRewritable
     TsSimplify.floatEqualities

compiler/typecheck/TcCanonical.lhs
compiler/typecheck/TcErrors.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcType.lhs

index f52bc9a..e91e833 100644 (file)
@@ -641,7 +641,7 @@ flattenTyVar d f ctxt tv
   where
     flatten_from_inerts
       = do { ieqs <- getInertEqs
-           ; let mco = tv_eq_subst (fst ieqs) tv  -- co : v ~ ty
+           ; let mco = tv_eq_subst ieqs tv  -- co : v ~ ty
            ; case mco of -- Done, but make sure the kind is zonked
                Nothing -> 
                  do { let knd = tyVarKind tv
@@ -818,7 +818,7 @@ canEqAppTy d fl s1 t1 s2 t2
        ; canEvVarsCreated d ctevs }
 
 canEqFailure :: SubGoalDepth -> CtEvidence -> TcS StopOrContinue
-canEqFailure d fl = emitFrozenError fl d >> return Stop
+canEqFailure d fl = do { emitFrozenError fl d; return Stop }
 
 ------------------------
 emitKindConstraint :: Ct -> TcS StopOrContinue
index 869ccc2..f673f03 100644 (file)
@@ -139,27 +139,25 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
 
 reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
 reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics })
-  = reportTidyWanteds ctxt tidy_insols tidy_flats implics
+  = reportTidyWanteds ctxt tidy_all implics
   where
     env = cec_tidy ctxt
-    tidy_insols = mapBag (tidyCt env) insols
-    tidy_flats  = mapBag (tidyCt env) flats
+    tidy_all = mapBag (tidyCt env) (insols `unionBags` flats)
                   -- All the Derived ones have been filtered out alrady
                   -- by the constraint solver. This is ok; we don't want
                   -- to report unsolved Derived goals as error
                   -- See Note [Do not report derived but soluble errors]
 
-reportTidyWanteds :: ReportErrCtxt -> Bag Ct -> Bag Ct -> Bag Implication -> TcM ()
-reportTidyWanteds ctxt insols flats implics
+reportTidyWanteds :: ReportErrCtxt -> Cts -> Bag Implication -> TcM ()
+reportTidyWanteds ctxt flats implics
   | Just ev_binds_var <- cec_defer ctxt
   = do { -- Defer errors to runtime
          -- See Note [Deferring coercion errors to runtime] in TcSimplify
-         mapBagM_ (deferToRuntime ev_binds_var ctxt mkFlatErr) 
-                  (flats `unionBags` insols)
+         mapBagM_ (deferToRuntime ev_binds_var ctxt mkFlatErr) flats
        ; mapBagM_ (reportImplic ctxt) implics }
 
   | otherwise
-  = do { reportInsolsAndFlats ctxt insols flats
+  = do { reportFlats ctxt flats
        ; mapBagM_ (reportImplic ctxt) implics }
              
 
@@ -183,8 +181,8 @@ deferToRuntime ev_binds_var ctxt mk_err_msg ct
   | otherwise   -- Do not set any evidence for Given/Derived
   = return ()   
 
-reportInsolsAndFlats :: ReportErrCtxt -> Cts -> Cts -> TcM ()
-reportInsolsAndFlats ctxt insols flats
+reportFlats :: ReportErrCtxt -> Cts -> TcM ()
+reportFlats ctxt flats    -- Here 'flats' includes insolble goals
   = tryReporters 
       [ -- First deal with things that are utterly wrong
         -- Like Int ~ Bool (incl nullary TyCons)
@@ -198,7 +196,7 @@ reportInsolsAndFlats ctxt insols flats
 
       , ("Unambiguous",          unambiguous,     reportFlatErrs ctxt) ]
       (reportAmbigErrs ctxt)
-      (bagToList (insols `unionBags` flats))
+      (bagToList flats)
   where
     utterly_wrong, skolem_eq, unambiguous :: Ct -> PredTree -> Bool
 
index 35b8ce5..335f46e 100644 (file)
@@ -283,32 +283,25 @@ Case 2: Functional Dependencies
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem
-  = do { mSolve <- trySpontaneousSolve workItem
-       ; spont_solve mSolve } 
-  where spont_solve SPCantSolve
-          | CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
-          -- Unsolved equality
-          = do { wl <- modifyInertTcS (kickOutRewritable (ctEvFlavour fl) tv)
-               ; traceTcS "kickOutRewritableInerts" $
-                 vcat [ text "WorkItem (unsolved) =" <+> ppr workItem
-                      , text "Kicked out =" <+> ppr wl ]
-               ; updWorkListTcS (appendWorkList wl)
-               ; insertInertItemTcS workItem
-               ; return Stop }
-          | otherwise
-          = continueWith workItem
-        spont_solve (SPSolved new_tv)
-          -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
-          -- see Note [Spontaneously solved in TyBinds]
-          = do { bumpStepCountTcS
-               ; traceFireTcS (cc_depth workItem) $
-                 ptext (sLit "Spontaneously solved:") <+> ppr workItem
-               ; wl <- modifyInertTcS (kickOutRewritable Given new_tv)
-
-               ; traceTcS "kickOutRewritableInerts" $ ptext (sLit "Kicked out =") <+> ppr wl
-               ; updWorkListTcS (appendWorkList wl) 
-               ; return Stop }
-
+  = do { mb_solved <- trySpontaneousSolve workItem
+       ; case mb_solved of
+           SPCantSolve
+              | CTyEqCan { cc_tyvar = tv, cc_ev = fl } <- workItem
+              -- Unsolved equality
+              -> do { kickOutRewritable (ctEvFlavour fl) tv
+                    ; insertInertItemTcS workItem
+                    ; return Stop }
+              | otherwise
+              -> continueWith workItem
+
+           SPSolved new_tv
+              -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
+              -- see Note [Spontaneously solved in TyBinds]
+              -> do { bumpStepCountTcS
+                   ; traceFireTcS (cc_depth workItem) $
+                     ptext (sLit "Spontaneously solved:") <+> ppr workItem
+                   ; kickOutRewritable Given new_tv
+                   ; return Stop } }
 \end{code}
 Note [Spontaneously solved in TyBinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -326,45 +319,44 @@ and only record them in the TyBinds of the TcS monad. The flattener is now consu
 these binds /and/ the inerts for potentially unsolved or other given equalities.
 
 \begin{code}
-
 kickOutRewritable :: CtFlavour    -- Flavour of the equality that is 
                                   -- being added to the inert set
                   -> TcTyVar      -- The new equality is tv ~ ty
-                  -> InertSet -> (WorkList,InertSet)
+                  -> TcS ()
 kickOutRewritable new_flav new_tv
-       is@(IS { inert_cans = IC { inert_eqs    = tv_eqs
-                                , inert_eq_tvs = inscope
-                                , inert_dicts  = dictmap
-                                , inert_funeqs = funeqmap
-                                , inert_irreds = irreds }
-               , inert_frozen = frozen })
-  = (kicked_out, remaining)
+  = do { wl <- modifyInertTcS kick_out
+       ; traceTcS "kickOutRewritable" $ 
+            vcat [ text "tv = " <+> ppr new_tv  
+                 , ptext (sLit "Kicked out =") <+> ppr wl]
+       ; updWorkListTcS (appendWorkList wl) }
   where
-    rest_out = fro_out `andCts` dicts_out `andCts` irs_out
-    kicked_out = WorkList { wl_eqs    = varEnvElts tv_eqs_out
-                          , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
-                          , wl_rest   = bagToList rest_out }
-  
-    remaining = is { inert_cans = IC { inert_eqs = tv_eqs_in
-                                     , inert_eq_tvs = inscope 
-                                       -- keep the same, safe and cheap
-                                     , inert_dicts = dicts_in
-                                     , inert_funeqs = feqs_in
-                                     , inert_irreds = irs_in }
-                   , inert_frozen = fro_in } 
+    kick_out :: InertSet -> (WorkList, InertSet)
+    kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
+                     , inert_dicts  = dictmap
+                     , inert_funeqs = funeqmap
+                     , inert_irreds = irreds } }))
+       = (kicked_out, is { inert_cans = inert_cans_in })
                 -- NB: Notice that don't rewrite 
                 -- inert_solved_dicts, and inert_solved_funeqs
                 -- optimistically. But when we lookup we have to take the 
                 -- subsitution into account
+       where
+         inert_cans_in = IC { inert_eqs = tv_eqs_in
+                            , inert_dicts = dicts_in
+                            , inert_funeqs = feqs_in
+                            , inert_irreds = irs_in }
+
+         kicked_out = WorkList { wl_eqs    = varEnvElts tv_eqs_out
+                               , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
+                               , wl_rest   = bagToList (dicts_out `andCts` irs_out) }
+  
+         (tv_eqs_out, tv_eqs_in) = partitionVarEnv  kick_out_eq tv_eqs
+         (feqs_out,  feqs_in)    = partCtFamHeadMap kick_out_ct funeqmap
+         (dicts_out, dicts_in)   = partitionCCanMap kick_out_ct dictmap
+         (irs_out,   irs_in)     = partitionBag     kick_out_ct irreds
 
-    (tv_eqs_out, tv_eqs_in) = partitionVarEnv  kick_out_eq tv_eqs
-    (feqs_out,  feqs_in)    = partCtFamHeadMap kick_out funeqmap
-    (dicts_out, dicts_in)   = partitionCCanMap kick_out dictmap
-    (irs_out,   irs_in)     = partitionBag     kick_out irreds
-    (fro_out,   fro_in)     = partitionBag     kick_out frozen
-
-    kick_out inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
-                        (new_tv `elemVarSet` tyVarsOfCt inert_ct) 
+    kick_out_ct inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
+                          (new_tv `elemVarSet` tyVarsOfCt inert_ct) 
                     -- NB: tyVarsOfCt will return the type 
                     --     variables /and the kind variables/ that are 
                     --     directly visible in the type. Hence we will
@@ -374,7 +366,8 @@ kickOutRewritable new_flav new_tv
                     --     constraints that mention type variables whose
                     --     kinds could contain this variable!
 
-    kick_out_eq inert_ct = kick_out inert_ct && not (ctFlavour inert_ct `canRewrite` new_flav)
+    kick_out_eq inert_ct = kick_out_ct inert_ct && 
+                           not (ctFlavour inert_ct `canRewrite` new_flav)
                -- If also the inert can rewrite the subst then there is no danger of 
                -- occurs check errors sor keep it there. No need to rewrite the inert equality
                -- (as we did in the past) because of point (8) of 
index 5199f01..3038ce2 100644 (file)
@@ -859,10 +859,10 @@ data Ct
 
   | CIrredEvCan {  -- These stand for yet-unknown predicates
       cc_ev :: CtEvidence,   -- See Note [Ct/evidence invariant]
-      cc_ty     :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
-                       -- Since, if it were a type constructor application, that'd make the
-                       -- whole constraint a CDictCan, or CTyEqCan. And it can't be
-                       -- a type family application either because it's a Xi type.
+      cc_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
+                   -- Since, if it were a type constructor application, that'd make the
+                   -- whole constraint a CDictCan, or CTyEqCan. And it can't be
+                   -- a type family application either because it's a Xi type.
       cc_depth :: SubGoalDepth -- See Note [WorkList]
     }
 
@@ -882,7 +882,7 @@ data Ct
   | CFunEqCan {  -- F xis ~ xi  
                  -- Invariant: * isSynFamilyTyCon cc_fun 
                  --            * typeKind (F xis) `compatKind` typeKind xi
-      cc_ev :: CtEvidence,      -- See Note [Ct/evidence invariant]
+      cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,      -- A type function
       cc_tyargs :: [Xi],       -- Either under-saturated or exactly saturated
       cc_rhs    :: Xi,         --    *never* over-saturated (because if so
@@ -893,8 +893,8 @@ data Ct
     }
 
   | CNonCanonical { -- See Note [NonCanonical Semantics] 
-      cc_ev :: CtEvidence, 
-      cc_depth  :: SubGoalDepth
+      cc_ev    :: CtEvidence, 
+      cc_depth :: SubGoalDepth
     }
 \end{code}
 
@@ -1094,6 +1094,7 @@ data Implication
 
       ic_skols  :: [TcTyVar],    -- Introduced skolems 
                                 -- See Note [Skolems in an implication]
+                                 -- See Note [Shadowing in a constraint]
 
       ic_fsks  :: [TcTyVar],   -- Extra flatten-skolems introduced by the flattening
                                -- done by canonicalisation. 
@@ -1128,6 +1129,18 @@ instance Outputable Implication where
           , ppr (ctLocSpan loc) ])
 \end{code}
 
+Note [Shadowing in a constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We assume NO SHADOWING in a constraint.  Specifically
+ * The unification variables are all implicitly quantified at top
+   level, and are all unique
+ * The skolem varibles bound in ic_skols are all freah when the
+   implication is created.
+So we can safely substitute. For example, if we have
+   forall a.  a~Int => ...(forall b. ...a...)...
+we can push the (a~Int) constraint inwards in the "givens" without
+worrying that 'b' might clash.
+
 Note [Skolems in an implication]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The skolems in an implication are not there to perform a skolem escape
index 56a31e1..b77e0cb 100644 (file)
@@ -454,8 +454,6 @@ data InertCans
               --   a |-> ct,co
               -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } 
               -- And  co : a ~ xi
-       , inert_eq_tvs :: InScopeSet
-              -- Superset of the type variables of inert_eqs
        , inert_dicts :: CCanMap Class
               -- Dictionaries only, index is the class
               -- NB: index is /not/ the whole type because FD reactions 
@@ -535,7 +533,7 @@ data InertSet
               -- Canonical Given, Wanted, Derived (no Solved)
              -- Sometimes called "the inert set"
 
-       , inert_frozen :: Cts       
+       , inert_insols :: Cts       
               -- Frozen errors (as non-canonicals)
                                
        , inert_fsks :: [TcTyVar]  -- Flatten-skolems allocated in this local scope
@@ -575,18 +573,17 @@ instance Outputable InertCans where
 instance Outputable InertSet where 
   ppr is = vcat [ ppr $ inert_cans is
                 , text "Frozen errors =" <+> -- Clearly print frozen errors
-                    braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
+                    braces (vcat (map ppr (Bag.bagToList $ inert_insols is)))
                 , text "Solved dicts"  <+> int (sizePredMap (inert_solved_dicts is))
                 , text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
 
 emptyInert :: InertSet
 emptyInert
   = IS { inert_cans = IC { inert_eqs    = emptyVarEnv
-                         , inert_eq_tvs = emptyInScopeSet
                          , inert_dicts  = emptyCCanMap
                          , inert_funeqs = FamHeadMap emptyTM 
                          , inert_irreds = emptyCts }
-       , inert_frozen        = emptyCts
+       , inert_insols        = emptyCts
        , inert_fsks          = []
        , inert_solved_dicts  = PredMap emptyTM 
        , inert_solved_funeqs = FamHeadMap emptyTM }
@@ -594,14 +591,10 @@ emptyInert
 insertInertItem :: Ct -> InertSet -> InertSet 
 -- Add a new inert element to the inert set. 
 insertInertItem item is
-  | isCNonCanonical item 
-    -- NB: this may happen if we decide to kick some frozen error 
-    -- out to rewrite him. Frozen errors are just NonCanonicals
-  = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
-    
-  | otherwise  
-    -- A canonical Given, Wanted, or Derived
-  = is { inert_cans = upd_inert_cans (inert_cans is) item }
+  = -- A canonical Given, Wanted, or Derived
+    ASSERT2( not (isCNonCanonical item), ppr item )
+        -- Can't be CNonCanonical, because they only land in inert_insols
+    is { inert_cans = upd_inert_cans (inert_cans is) item }
   
   where upd_inert_cans :: InertCans -> Ct -> InertCans
         -- Precondition: item /is/ canonical
@@ -614,10 +607,8 @@ insertInertItem item is
         
                 eqs'     = extendVarEnv_C upd_err (inert_eqs ics) 
                                                   (cc_tyvar item) item        
-                inscope' = extendInScopeSetSet (inert_eq_tvs ics)
-                                               (tyVarsOfCt item)
-                
-            in ics { inert_eqs = eqs', inert_eq_tvs = inscope' }
+
+            in ics { inert_eqs = eqs' }
 
           | isCIrredEvCan item                  -- Presently-irreducible evidence
           = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
@@ -689,17 +680,15 @@ updInertTcS upd
 prepareInertsForImplications :: InertSet -> InertSet
 -- See Note [Preparing inert set for implications]
 prepareInertsForImplications is
-  = is { inert_cans = getGivens (inert_cans is)
-       , inert_fsks = []
-       , inert_frozen = emptyCts }
+  = is { inert_cans   = getGivens (inert_cans is)
+       , inert_fsks   = []
+       , inert_insols = emptyCts }
   where
-    getGivens (IC { inert_eq_tvs = eq_tvs
-                  , inert_eqs    = eqs
+    getGivens (IC { inert_eqs    = eqs
                   , inert_irreds = irreds
                   , inert_funeqs = FamHeadMap funeqs
                   , inert_dicts  = dicts })
-      = IC { inert_eq_tvs = eq_tvs
-           , inert_eqs    = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs 
+      = IC { inert_eqs    = filterVarEnv_Directly (\_ ct -> isGivenCt ct) eqs 
            , inert_funeqs = FamHeadMap (mapTM given_from_wanted funeqs)
            , inert_irreds = Bag.filterBag isGivenCt irreds
            , inert_dicts  = keepGivenCMap dicts }
@@ -759,10 +748,9 @@ alpha.  (In general we can't float class constraints out just in case
 
 
 \begin{code}
-getInertEqs :: TcS (TyVarEnv Ct, InScopeSet)
+getInertEqs :: TcS (TyVarEnv Ct)
 getInertEqs = do { inert <- getTcSInerts
-                 ; let ics = inert_cans inert
-                 ; return (inert_eqs ics, inert_eq_tvs ics) }
+                 ; return (inert_eqs (inert_cans inert)) }
 
 getInertUnsolved :: TcS (Cts, Cts)
 -- Return (unsolved-wanteds, insolubles)
@@ -779,7 +767,7 @@ getInertUnsolved
             unsolved_flats = unsolved_eqs `unionBags` unsolved_irreds `unionBags` 
                              unsolved_dicts `unionBags` unsolved_funeqs
 
-      ; return (unsolved_flats, inert_frozen is) }
+      ; return (unsolved_flats, inert_insols is) }
   where
     add_if_unsolved ct cts
       | is_unsolved ct = cts `extendCts` ct
@@ -801,7 +789,7 @@ checkAllSolved
 
       ; return (not (unsolved_eqs || unsolved_irreds
                      || unsolved_dicts || unsolved_funeqs
-                     || not (isEmptyBag (inert_frozen is)))) }
+                     || not (isEmptyBag (inert_insols is)))) }
 
 extractRelevantInerts :: Ct -> TcS Cts
 -- Returns the constraints from the inert set that are 'relevant' to react with 
@@ -959,6 +947,9 @@ panicTcS doc = pprPanic "TcCanonical" doc
 traceTcS :: String -> SDoc -> TcS ()
 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
 
+instance HasDynFlags TcS where
+    getDynFlags = wrapTcS getDynFlags
+
 bumpStepCountTcS :: TcS ()
 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
                                     ; n <- TcM.readTcRef ref
@@ -1157,21 +1148,17 @@ emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts. 
 emitFrozenError fl depth 
   = do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
-       ; inert_ref <- getTcSInertsRef 
-       ; wrapTcS $ do
-       { inerts <- TcM.readTcRef inert_ref
-       ; let old_insols = inert_frozen inerts
-             ct = CNonCanonical { cc_ev = fl, cc_depth = depth } 
-             inerts_new = inerts { inert_frozen = extendCts old_insols ct } 
-             this_pred = ctEvPred fl
-             already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
+       ; updInertTcS add_insol }
+  where
+    add_insol inerts@(IS { inert_insols = old_insols })
+      | already_there = inerts
+      | otherwise     = inerts { inert_insols = extendCts old_insols insol_ct }
+      where
+        already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
             -- See Note [Do not add duplicate derived insolubles]
-       ; unless already_there $
-         TcM.writeTcRef inert_ref inerts_new } }
-
-instance HasDynFlags TcS where
-    getDynFlags = wrapTcS getDynFlags
 
+    insol_ct = CNonCanonical { cc_ev = fl, cc_depth = depth } 
+    this_pred = ctEvPred fl
 
 getTcEvBinds :: TcS EvBindsVar
 getTcEvBinds = TcS (return . tcs_ev_binds) 
index 737d0e4..5c5bb09 100644 (file)
@@ -802,10 +802,6 @@ solveNestedImplications implics
        ; (floated_eqs, unsolved_implics)
            <- flatMapBagPairM (solveImplication thinner_inerts) implics
 
-       ; promoteFloatedUnificationVars floated_eqs
-           -- Performs some unifications, adding to monadically-carried ty_binds
-           -- These will be used when processing floated_eqs later
-
        -- ... and we are back in the original TcS inerts 
        -- Notice that the original includes the _insoluble_flats so it was safe to ignore
        -- them in the beginning of this function.
@@ -829,64 +825,57 @@ solveImplication inerts
                  , ic_given  = givens
                  , ic_wanted = wanteds
                  , ic_loc    = loc })
-  = nestImplicTcS ev_binds untch inerts $
+  = 
     do { traceTcS "solveImplication {" (ppr imp) 
 
          -- Solve the nested constraints
-       ; solveInteractGiven loc old_fsks givens 
-       ; residual_wanted <- solve_wanteds wanteds
-       ; new_fsks <- getFlattenSkols
-
-       ; let all_fsks = new_fsks ++ old_fsks
-             (floated_eqs, final_wanted)
-                 = floatEqualities (skols ++ all_fsks) givens residual_wanted
-
-             res_implic | isEmptyWC final_wanted 
+         -- NB: 'inerts' has empty inert_fsks
+       ; (new_fsks, residual_wanted) 
+            <- nestImplicTcS ev_binds untch inerts $
+               do { solveInteractGiven loc old_fsks givens 
+                  ; residual_wanted <- solve_wanteds wanteds
+                  ; more_fsks <- getFlattenSkols
+                  ; return (more_fsks ++ old_fsks, residual_wanted) }
+
+       ; (floated_eqs, final_wanted)
+             <- floatEqualities (skols ++ new_fsks) givens residual_wanted
+
+       ; let res_implic | isEmptyWC final_wanted 
                         = emptyBag
                         | otherwise
-                        = unitBag imp { ic_fsks   = all_fsks
-                                      , ic_wanted = dropDerivedWC final_wanted
-                                      , ic_insol  = insolubleWC final_wanted }
+                        = unitBag (imp { ic_fsks   = new_fsks
+                                       , ic_wanted = dropDerivedWC final_wanted
+                                       , ic_insol  = insolubleWC final_wanted })
 
        ; evbinds <- getTcEvBindsMap
        ; traceTcS "solveImplication end }" $ vcat
              [ text "floated_eqs =" <+> ppr floated_eqs
-             , text "new_fsks =" <+> ppr all_fsks
+             , text "new_fsks =" <+> ppr new_fsks
              , text "res_implic =" <+> ppr res_implic
              , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ]
 
        ; return (floated_eqs, res_implic) }
 \end{code}
 
-Note [Floating equalities]
 
 \begin{code}
-promoteFloatedUnificationVars :: Cts -> TcS ()
-promoteFloatedUnificationVars cts
-  = do { untch <- TcSMonad.getUntouchables
-       ; let tvs = filter (isFloatedTouchableMetaTyVar untch) $
-                   varSetElems (tyVarsOfCts cts)
-       ; mapM_ (promote_tv untch) tvs
-       ; ty_binds <- getTcSTyBindsMap
-       ; traceTcS "promoteFloated" (vcat [ text "Ctxt untoucables =" <+> ppr untch
-                                         , text "Floated eqs =" <+> ppr cts
-                                         , text "Promoted tvs =" <+> ppr tvs
-                                         , text "Ty binds =" <+> ppr ty_binds])
-       ; return () }
-  where
-    promote_tv untch tv 
-      = do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
-           ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
-           ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
-
-floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints -> (Cts, WantedConstraints)
+floatEqualities :: [TcTyVar] -> [EvVar] -> WantedConstraints 
+                -> TcS (Cts, WantedConstraints)
 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
 -- and come from the input wanted ev vars or deriveds 
+-- Also performs some unifications, adding to monadically-carried ty_binds
+-- These will be used when processing floated_eqs later
 floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
   | hasEqualities can_given 
-  = (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
+  = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
   | otherwise 
-  = (float_eqs, wanteds { wc_flat = remaining_flats })
+  = do { untch <- TcSMonad.getUntouchables
+       ; mapM_ (promote_tv untch) (varSetElems (tyVarsOfCts float_eqs))
+       ; ty_binds <- getTcSTyBindsMap
+       ; traceTcS "floatEqualities" (vcat [ text "Ctxt untoucables =" <+> ppr untch
+                                          , text "Floated eqs =" <+> ppr float_eqs
+                                          , text "Ty binds =" <+> ppr ty_binds])
+       ; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
   where 
     (float_eqs, remaining_flats) = partitionBag is_floatable flats
     skol_set = growSkols wanteds (mkVarSet skols)
@@ -897,6 +886,14 @@ floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
        where
          pred = ctPred ct
 
+    promote_tv untch tv 
+      | isFloatedTouchableMetaTyVar untch tv
+      = do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
+           ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
+           ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
+      | otherwise
+      = return ()
+
 growSkols :: WantedConstraints -> VarSet -> VarSet
 -- Find all the type variables that might possibly be unified
 -- with a type that mentions a skolem.  This test is very conservative.
index 724d03a..f33e2bb 100644 (file)
@@ -319,6 +319,31 @@ vanillaSkolemTv = SkolemTv False  -- Might be instantiated
 superSkolemTv   = SkolemTv True   -- Treat this as a completely distinct type
 
 -------------------------
+newtype Untouchables = Untouchables Int
+
+noUntouchables :: Untouchables
+noUntouchables = Untouchables 0   -- 0 = outermost level
+
+pushUntouchables :: Unique -> Untouchables -> Untouchables 
+pushUntouchables _ (Untouchables us) = Untouchables (us+1)
+
+isFloatedTouchable :: Untouchables -> Untouchables -> Bool
+isFloatedTouchable (Untouchables ctxt_untch) (Untouchables tv_untch) 
+  = ctxt_untch < tv_untch
+
+isTouchable :: Untouchables -> Untouchables -> Bool
+isTouchable (Untouchables ctxt_untch) (Untouchables tv_untch) 
+  = ctxt_untch == tv_untch   -- NB: invariant ctxt_untch >= tv_untch
+                             --     So <= would be equivalent
+
+checkTouchableInvariant :: Untouchables -> Untouchables -> Bool
+checkTouchableInvariant (Untouchables ctxt_untch) (Untouchables tv_untch) 
+  = ctxt_untch >= tv_untch
+
+instance Outputable Untouchables where
+  ppr (Untouchables us) = ppr us
+
+{-   OLD
 newtype Untouchables = Untouchables [Unique]
 
 noUntouchables :: Untouchables
@@ -343,6 +368,8 @@ isTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
 
 instance Outputable Untouchables where
   ppr (Untouchables us) = pprWithCommas ppr us
+-}
+
 
 -----------------------------
 data MetaDetails
@@ -705,7 +732,10 @@ isTouchableMetaTyVar :: Untouchables -> TcTyVar -> Bool
 isTouchableMetaTyVar ctxt_untch tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of 
-      MetaTv { mtv_untch = tv_untch } -> isTouchable ctxt_untch tv_untch
+      MetaTv { mtv_untch = tv_untch } 
+        -> ASSERT2( checkTouchableInvariant ctxt_untch tv_untch, 
+                    ppr tv $$ ppr tv_untch $$ ppr ctxt_untch )
+           isTouchable ctxt_untch tv_untch
       _ -> False
 
 isFloatedTouchableMetaTyVar :: Untouchables -> TcTyVar -> Bool