Commit 6785820e authored by dimitris's avatar dimitris

Mostly commentary to follow up after discussions with SPJ on several open tickets.

parent d86e6c01
......@@ -736,6 +736,12 @@ flatten d ctxt ty@(ForAllTy {})
; (rho', co) <- flatten d ctxt rho
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
-- DV: Simon and I have a better plan here related to #T5934 and that plan is to
-- first normalize completely the rho type with respect to the top-level instances,
-- and then flatten out only the family equations that do not mention the quantified
-- variable. Keep the rest as they are. There is no worry that we don't normalize with
-- the givens because the givens can't possibly mention the quantified variable anyway!
where under_families tvs rho
= go (mkVarSet tvs) rho
where go _bound (TyVarTy _tv) = False
......
......@@ -335,8 +335,23 @@ rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs
= if fl `canRewrite` subst_fl then
-- If also the inert can rewrite the subst it's totally safe
-- to rewrite on the spot
do { ct' <- rewrite_on_the_spot ct
; return $ Just ct' }
do {
{- DV: I thought this might work but not because you don't have the full knowledge of the
implications (just the worklist). And it's a bit tedious. SPJ and I discussed about breaking
the 'idempotent substitution' invariant to be a little more lazy. -}
-- DV: Very experimental!
-- If it's a given equality and its LHS does not appear in the worklist
-- there is no point in rewriting him. In fact there is not point in keeping him,
-- at all, is there?
worklist_tvs <- getTcSWorkListTvs
; if isGiven (cc_flavor ct) && not (tyVarsOfCt ct `elemVarSet` worklist_tvs) then
return Nothing
else do {
ct' <- rewrite_on_the_spot ct
; return $ Just ct' }
}
else -- We have to throw inert back to worklist for occurs checks
do { updWorkListTcS (extendWorkListEq ct)
; return Nothing }
......@@ -388,10 +403,11 @@ kick_out_rewritable ct is@(IS { inert_cans =
, inert_frozen = frozen })
= ((kicked_out,eqmap), remaining)
where
rest_out = fro_out `andCts` dicts_out
`andCts` ips_out `andCts` irs_out
kicked_out = WorkList { wl_eqs = []
, wl_funeqs = bagToList feqs_out
, wl_rest = bagToList (fro_out `andCts` dicts_out
`andCts` ips_out `andCts` irs_out) }
, wl_rest = bagToList rest_out }
remaining = is { inert_cans = IC { inert_eqs = emptyVarEnv
, inert_eq_tvs = inscope
......
......@@ -17,6 +17,7 @@ module TcSMonad (
appendWorkListCt, appendWorkListEqs, unionWorkList, selectWorkItem,
getTcSWorkList, updWorkListTcS, updWorkListTcS_return, keepWanted,
getTcSWorkListTvs,
Ct(..), Xi, tyVarsOfCt, tyVarsOfCts, tyVarsOfCDicts,
emitFrozenError,
......@@ -196,7 +197,10 @@ better rewrite it as much as possible before reporting it as an error to the use
\begin{code}
-- See Note [WorkList]
data WorkList = WorkList { wl_eqs :: [Ct], wl_funeqs :: [Ct], wl_rest :: [Ct] }
data WorkList = WorkList { wl_eqs :: [Ct]
, wl_funeqs :: [Ct]
, wl_rest :: [Ct]
}
unionWorkList :: WorkList -> WorkList -> WorkList
......@@ -205,6 +209,7 @@ unionWorkList new_wl orig_wl =
, wl_funeqs = wl_funeqs new_wl ++ wl_funeqs orig_wl
, wl_rest = wl_rest new_wl ++ wl_rest orig_wl }
extendWorkListEq :: Ct -> WorkList -> WorkList
-- Extension by equality
extendWorkListEq ct wl
......@@ -215,7 +220,8 @@ extendWorkListEq ct wl
extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
extendWorkListNonEq ct wl
= wl { wl_rest = ct : wl_rest wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
......@@ -236,7 +242,7 @@ isEmptyWorkList wl
= null (wl_eqs wl) && null (wl_rest wl) && null (wl_funeqs wl)
emptyWorkList :: WorkList
emptyWorkList = WorkList { wl_eqs = [], wl_rest = [], wl_funeqs = []}
emptyWorkList = WorkList { wl_eqs = [], wl_rest = [], wl_funeqs = [] }
workListFromEq :: Ct -> WorkList
workListFromEq ct = extendWorkListEq ct emptyWorkList
......@@ -964,6 +970,16 @@ getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
getTcSWorkList :: TcS WorkList
getTcSWorkList = getTcSWorkListRef >>= wrapTcS . (TcM.readTcRef)
getTcSWorkListTvs :: TcS TyVarSet
-- Return the variables of the worklist
getTcSWorkListTvs
= do { wl <- getTcSWorkList
; return $
cts_tvs (wl_eqs wl) `unionVarSet` cts_tvs (wl_funeqs wl) `unionVarSet` cts_tvs (wl_rest wl) }
where cts_tvs = foldr (unionVarSet . tyVarsOfCt) emptyVarSet
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS f
= updWorkListTcS_return (\w -> ((),f w))
......
......@@ -597,6 +597,15 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
-- We allow ourselves to unify environment
-- variables; hence *no untouchables*
-- DV: SPJ and I discussed a new plan here:
-- Step 1: Simplify everything in the same bag
-- Step 2: zonk away the lhs constraints and get only the non-trivial ones
-- Step 3: do the implications with these constraints
-- This will have the advantage that (i) we no longer need simplEqsOnly flag
-- and (ii) will fix problems appearing from touchable unification variables
-- in the givens, manifested by #5853
-- TODO ...
; (lhs_results, lhs_binds)
<- runTcS (SimplRuleLhs name) untch emptyInert emptyWorkList $
solveWanteds zonked_lhs
......@@ -944,7 +953,10 @@ floatEqualities skols can_given wantders
| hasEqualities can_given = (emptyBag, wantders)
-- Note [Float Equalities out of Implications]
| otherwise = partitionBag is_floatable wantders
-- TODO: Maybe we should try out /not/ floating constraints that contain touchables only,
-- since they are inert and not going to interact with anything more in a more global scope.
where skol_set = mkVarSet skols
is_floatable :: Ct -> Bool
is_floatable ct
......@@ -1090,6 +1102,8 @@ Note [Float Equalities out of Implications]
We want to float equalities out of vanilla existentials, but *not* out
of GADT pattern matches.
---> TODO Expand in accordance to our discussion
\begin{code}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment