Commit ca0b7c66 authored by simonpj's avatar simonpj
Browse files

[project @ 2003-12-17 11:29:40 by simonpj]

-----------------------------------------------------
  Fix a subtle loop in the context-reduction machinery
  ----------------------------------------------------

This bug was provoked by a recent change: when trying to prove
a constraint C, TcSimplify.reduce now adds C to the database before
trying to prove C, thus building recursive dictionaries.

Two bugs
a) If we add C's superclasses (which we were) we can now build a
   bogusly-recursive dictionary (see Note [SUPERCLASS-LOOP]).
   Solution: in reduce, add C only (via addIrred NoSCs) and then
   later use addWanted to add its definition plus SCs.

b) Since we can have recursive definitions, the superclass-loop
   handling machinery (findAllDeps) must carry its visited-set
   with it (which it was not doing before)


The main file is TcSimplify; but I modified a bunch of others to
take advantage of new function extendVarSetList
parent 69e27f1d
......@@ -7,7 +7,7 @@
module VarSet (
VarSet, IdSet, TyVarSet,
emptyVarSet, unitVarSet, mkVarSet,
extendVarSet, extendVarSet_C,
extendVarSet, extendVarSetList, extendVarSet_C,
elemVarSet, varSetElems, subVarSet,
unionVarSet, unionVarSets,
intersectVarSet, intersectsVarSet,
......@@ -42,6 +42,7 @@ unionVarSets :: [VarSet] -> VarSet
varSetElems :: VarSet -> [Var]
unitVarSet :: Var -> VarSet
extendVarSet :: VarSet -> Var -> VarSet
extendVarSetList:: VarSet -> [Var] -> VarSet
elemVarSet :: Var -> VarSet -> Bool
delVarSet :: VarSet -> Var -> VarSet
delVarSetList :: VarSet -> [Var] -> VarSet
......@@ -62,6 +63,7 @@ delVarSetByKey :: VarSet -> Unique -> VarSet
emptyVarSet = emptyUniqSet
unitVarSet = unitUniqSet
extendVarSet = addOneToUniqSet
extendVarSetList= addListToUniqSet
intersectVarSet = intersectUniqSets
intersectsVarSet:: VarSet -> VarSet -> Bool -- True if non-empty intersection
......
......@@ -529,7 +529,7 @@ addLoc extra_loc m loc scope errs
addInScopeVars :: [Var] -> LintM a -> LintM a
addInScopeVars ids m loc scope errs
= m loc (scope `unionVarSet` mkVarSet ids) errs
= m loc (extendVarSetList scope ids) errs
\end{code}
\begin{code}
......
......@@ -261,7 +261,7 @@ dsRule in_scope (L loc (HsRule name act vars lhs rhs))
returnDs (fn, Rule name act tpl_vars args core_rhs)
where
tpl_vars = [var | RuleBndr (L _ var) <- vars]
all_vars = mkInScopeSet (in_scope `unionVarSet` mkVarSet tpl_vars)
all_vars = mkInScopeSet (extendVarSetList in_scope tpl_vars)
ds_lhs all_vars lhs
= let
......
......@@ -46,7 +46,7 @@ import Outputable
import HsPat ( collectPatBinders, collectPatsBinders )
import VarSet ( IdSet, mkVarSet, varSetElems,
intersectVarSet, minusVarSet,
intersectVarSet, minusVarSet, extendVarSetList,
unionVarSet, unionVarSets, elemVarSet )
import SrcLoc ( Located(..), unLoc, noLoc, getLoc )
\end{code}
......@@ -705,7 +705,7 @@ dsCmdStmt ids local_vars env_ids out_ids (ExprStmt cmd c_ty)
do_compose ids before_c_ty after_c_ty out_ty
(do_first ids in_ty1 c_ty out_ty core_cmd) $
do_arr ids after_c_ty out_ty snd_fn,
fv_cmd `unionVarSet` mkVarSet out_ids)
extendVarSetList fv_cmd out_ids)
where
-- A | xs1 |- c :: [] t
......
......@@ -837,7 +837,7 @@ isCandidate (OccEnv cands encl _) id = id `elemVarSet` cands
addNewCands :: OccEnv -> [Id] -> OccEnv
addNewCands (OccEnv cands encl ctxt) ids
= OccEnv (cands `unionVarSet` mkVarSet ids) encl ctxt
= OccEnv (extendVarSetList cands ids) encl ctxt
addNewCand :: OccEnv -> Id -> OccEnv
addNewCand (OccEnv cands encl ctxt) id
......
......@@ -1105,7 +1105,7 @@ splitUDs bndrs uds@(MkUD {dict_binds = orig_dbs,
dump_db (free_dbs, dump_dbs, dump_idset) db@(bind, fvs)
| dump_idset `intersectsVarSet` fvs -- Dump it
= (free_dbs, dump_dbs `snocBag` db,
dump_idset `unionVarSet` mkVarSet (bindersOf bind))
extendVarSetList dump_idset (bindersOf bind))
| otherwise -- Don't dump it
= (free_dbs `snocBag` db, dump_dbs, dump_idset)
......
......@@ -592,8 +592,8 @@ checkSigsTyVars qtvs sigs
-- f () = ()
-- Here, 'a' won't appear in qtvs, so we have to add it
sig_tvs = foldr (unionVarSet . mkVarSet) emptyVarSet sig_tvs_s
all_tvs = mkVarSet qtvs `unionVarSet` sig_tvs
sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
all_tvs = extendVarSetList sig_tvs qtvs
in
returnM (varSetElems all_tvs)
where
......
......@@ -44,7 +44,7 @@ import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
import TcType ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
mkClassPred, isOverloadedTy, mkTyConApp,
mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
tyVarsOfPred )
tyVarsOfPred, tcEqType )
import Id ( idType, mkUserLocal )
import Var ( TyVar )
import Name ( getOccName, getSrcLoc )
......@@ -907,7 +907,7 @@ tcSimplifyToDicts wanteds
doc = text "tcSimplifyToDicts"
-- Reduce methods and lits only; stop as soon as we get a dictionary
try_me inst | isDict inst = DontReduce NoSCs
try_me inst | isDict inst = DontReduce NoSCs -- See notes above for why NoSCs
| otherwise = ReduceMe
\end{code}
......@@ -1412,19 +1412,19 @@ reduceList (n,stack) try_me wanteds state
go ws state'
-- Base case: we're done!
reduce stack try_me wanted state
reduce stack try_me wanted avails
-- It's the same as an existing inst, or a superclass thereof
| Just avail <- isAvailable state wanted
| Just avail <- isAvailable avails wanted
= if isLinearInst wanted then
addLinearAvailable state avail wanted `thenM` \ (state', wanteds') ->
reduceList stack try_me wanteds' state'
addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
reduceList stack try_me wanteds' avails'
else
returnM state -- No op for non-linear things
returnM avails -- No op for non-linear things
| otherwise
= case try_me wanted of {
DontReduce want_scs -> addIrred want_scs state wanted
DontReduce want_scs -> addIrred want_scs avails wanted
; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
-- First, see if the inst can be reduced to a constant in one step
......@@ -1437,26 +1437,30 @@ reduce stack try_me wanted state
; ReduceMe -> -- It should be reduced
lookupInst wanted `thenM` \ lookup_result ->
case lookup_result of
GenInst wanteds' rhs -> addWanted state wanted rhs wanteds' `thenM` \ state' ->
reduceList stack try_me wanteds' state'
-- Experiment with doing addWanted *before* the reduceList,
GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
addWanted avails2 wanted rhs wanteds'
-- Experiment with temporarily doing addIrred *before* the reduceList,
-- which has the effect of adding the thing we are trying
-- to prove to the database before trying to prove the things it
-- needs. See note [RECURSIVE DICTIONARIES]
-- NB: we must not do an addWanted before, because that adds the
-- superclasses too, and thaat can lead to a spurious loop; see
-- the examples in [SUPERCLASS-LOOP]
-- So we do an addIrred before, and then overwrite it afterwards with addWanted
SimpleInst rhs -> addWanted state wanted rhs []
SimpleInst rhs -> addWanted avails wanted rhs []
NoInstance -> -- No such instance!
-- Add it and its superclasses
addIrred AddSCs state wanted
addIrred AddSCs avails wanted
}
where
try_simple do_this_otherwise
= lookupInst wanted `thenM` \ lookup_result ->
case lookup_result of
SimpleInst rhs -> addWanted state wanted rhs []
other -> do_this_otherwise state wanted
SimpleInst rhs -> addWanted avails wanted rhs []
other -> do_this_otherwise avails wanted
\end{code}
......@@ -1512,14 +1516,13 @@ addFree avails free = returnM (addToFM avails free IsFree)
addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
addWanted avails wanted rhs_expr wanteds
= ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
addAvailAndSCs avails wanted avail
= addAvailAndSCs avails wanted avail
where
avail | instBindingRequired wanted = Rhs rhs_expr wanteds
| otherwise = ASSERT( null wanteds ) NoRhs
addGiven :: Avails -> Inst -> TcM Avails
addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
-- No ASSERT( not (given `elemFM` avails) ) because in an instance
-- decl for Ord t we can add both Ord t and Eq t as 'givens',
-- so the assert isn't true
......@@ -1535,21 +1538,23 @@ addAvailAndSCs avails inst avail
| otherwise = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
addSCs is_loop avails1 inst
where
avails1 = addToFM avails inst avail
is_loop inst = inst `elem` deps -- Note: this compares by *type*, not by Unique
deps = findAllDeps avails avail
findAllDeps :: Avails -> Avail -> [Inst]
-- Find all the Insts that this one depends on
-- See Note [SUPERCLASS-LOOP]
findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
findAllDeps avails other = []
find_all_deps_help :: Avails -> Inst -> [Inst]
find_all_deps_help avails inst
= case lookupFM avails inst of
Just avail -> findAllDeps avails avail
Nothing -> []
avails1 = addToFM avails inst avail
is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
-- Note: this compares by *type*, not by Unique
deps = findAllDeps emptyVarSet avail
dep_tys = map idType (varSetElems deps)
findAllDeps :: IdSet -> Avail -> IdSet
-- Find all the Insts that this one depends on
-- See Note [SUPERCLASS-LOOP]
-- Watch out, though. Since the avails may contain loops
-- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
findAllDeps so_far (Rhs _ kids)
= foldl findAllDeps
(extendVarSetList so_far (map instToId kids)) -- Add the kids to so_far
[a | Just a <- map (lookupFM avails) kids] -- Find the kids' Avail
findAllDeps so_far other = so_far
addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
-- Add all the superclasses of the Inst to Avails
......@@ -1566,17 +1571,18 @@ addSCs is_loop avails dict
sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
| is_loop sc_dict
= returnM avails -- See Note [SUPERCLASS-LOOP]
| otherwise
= case lookupFM avails sc_dict of
Just (Given _ _) -> returnM avails -- Given is cheaper than superclass selection
Just other -> returnM avails' -- SCs already added
Nothing -> addSCs is_loop avails' sc_dict
| add_me sc_dict = addSCs is_loop avails' sc_dict
| otherwise = returnM avails
where
sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
avail = Rhs sc_sel_rhs [dict]
avails' = addToFM avails sc_dict avail
avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
add_me :: Inst -> Bool
add_me sc_dict
| is_loop sc_dict = False -- See Note [SUPERCLASS-LOOP]
| otherwise = case lookupFM avails sc_dict of
Just (Given _ _) -> False -- Given is cheaper than superclass selection
other -> True
\end{code}
Note [SUPERCLASS-LOOP]: Checking for loops
......@@ -1643,13 +1649,13 @@ by instance decl, holds if
by instance decl of Eq, holds if
d3 : D []
where d2 = dfEqList d2
where d2 = dfEqList d3
d1 = dfEqD d2
But now we can "tie the knot" to give
d3 = d1
d2 = dfEqList d2
d2 = dfEqList d3
d1 = dfEqD d2
and it'll even run! The trick is to put the thing we are trying to prove
......
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