Commit 65069806 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix solveOneFromTheOther for RecursiveSuperclasses

This patch fixes the redundant superclass expansion
in Trac #14774.

The main change is to fix TcInterac.solveOneFromTheOther, so
that it does not prefer a work-item with a binding if that binding
transitively depends on the inert item we are comparing it with.

Explained in Note [Replacement vs keeping] in TcInert, esp
item (c) of the "Constraints coming from the same level" part.

To make this work I refactored out a new function
TcEvidence.findNeededEvVars, which was previously buried
inside TcSimplify.neededEvVars.

I added quite a few more comments and signposts about superclass
expansion.
parent 41d29d5a
......@@ -241,19 +241,19 @@ So here's the plan:
1. Eagerly generate superclasses for given (but not wanted)
constraints; see Note [Eagerly expand given superclasses].
This is done in canClassNC, when we take a non-canonical constraint
and cannonicalise it.
This is done using mkStrictSuperClasses in canClassNC, when
we take a non-canonical Given constraint and cannonicalise it.
However stop if you encounter the same class twice. That is,
expand eagerly, but have a conservative termination condition: see
Note [Expanding superclasses] in TcType.
mkStrictSuperClasses expands eagerly, but has a conservative
termination condition: see Note [Expanding superclasses] in TcType.
2. Solve the wanteds as usual, but do no further expansion of
superclasses for canonical CDictCans in solveSimpleGivens or
solveSimpleWanteds; Note [Danger of adding superclasses during solving]
However, /do/ continue to eagerly expand superlasses for /given/
non-canonical constraints (canClassNC does this). As Trac #12175
However, /do/ continue to eagerly expand superlasses for new /given/
/non-canonical/ constraints (canClassNC does this). As Trac #12175
showed, a type-family application can expand to a class constraint,
and we want to see its superclasses for just the same reason as
Note [Eagerly expand given superclasses].
......@@ -261,9 +261,11 @@ So here's the plan:
3. If we have any remaining unsolved wanteds
(see Note [When superclasses help] in TcRnTypes)
try harder: take both the Givens and Wanteds, and expand
superclasses again. This may succeed in generating (a finite
number of) extra Givens, and extra Deriveds. Both may help the
proof. This is done in TcSimplify.expandSuperClasses.
superclasses again. See the calls to expandSuperClasses in
TcSimplify.simpl_loop and solveWanteds.
This may succeed in generating (a finite number of) extra Givens,
and extra Deriveds. Both may help the proof.
4. Go round to (2) again. This loop (2,3,4) is implemented
in TcSimplify.simpl_loop.
......@@ -285,10 +287,31 @@ Why do we do this? Two reasons:
When we take a CNonCanonical or CIrredCan, but end up classifying it
as a CDictCan, we set the cc_pend_sc flag to False.
Note [Superclass loops]
~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
class C a => D a
class D a => C a
Then, when we expand superclasses, we'll get back to the self-same
predicate, so we have reached a fixpoint in expansion and there is no
point in fruitlessly expanding further. This case just falls out from
our strategy. Consider
f :: C a => a -> Bool
f x = x==x
Then canClassNC gets the [G] d1: C a constraint, and eager emits superclasses
G] d2: D a, [G] d3: C a (psc). (The "psc" means it has its sc_pend flag set.)
When processing d3 we find a match with d1 in the inert set, and we always
keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
TcInteract. So d3 dies a quick, happy death.
Note [Eagerly expand given superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In step (1) of Note [The superclass story], why do we eagerly expand
Given superclasses by one layer? Mainly because of some very obscure
Given superclasses by one layer? (By "one layer" we mean expand transitively
until you meet the same class again -- the conservative criterion embodied
in expandSuperClasses. So a "layer" might be a whole stack of superclasses.)
We do this eagerly for Givens mainly because of some very obscure
cases like this:
instance Bad a => Eq (T a)
......
......@@ -21,7 +21,7 @@ module TcEvidence (
-- EvTerm (already a CoreExpr)
EvTerm(..), EvExpr,
evId, evCoercion, evCast, evDFunApp, evSelector,
mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable,
mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
evTermCoercion,
EvCallStack(..),
......@@ -765,6 +765,33 @@ evTermCoercion (EvExpr (Coercion co)) = co
evTermCoercion (EvExpr (Cast tm co)) = mkCoCast (evTermCoercion (EvExpr tm)) co
evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
{-
************************************************************************
* *
Free variables
* *
************************************************************************
-}
findNeededEvVars :: EvBindMap -> VarSet -> VarSet
findNeededEvVars ev_binds seeds
= transCloVarSet also_needs seeds
where
also_needs :: VarSet -> VarSet
also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
-- It's OK to use nonDetFoldUFM here because we immediately
-- forget about the ordering by creating a set
add :: Var -> VarSet -> VarSet
add v needs
| Just ev_bind <- lookupEvBind ev_binds v
, EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
, is_given
= evVarsOfTerm rhs `unionVarSet` needs
| otherwise
= needs
evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
......
......@@ -568,6 +568,8 @@ solveOneFromTheOther ev_i ev_w
loc_w = ctEvLoc ev_w
lvl_i = ctLocLevel loc_i
lvl_w = ctLocLevel loc_w
ev_id_i = ctEvEvId ev_i
ev_id_w = ctEvEvId ev_w
different_level_strategy
| isIPPred pred, lvl_w > lvl_i = KeepWork
......@@ -584,14 +586,15 @@ solveOneFromTheOther ev_i ev_w
| GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
= KeepInert
| has_binding binds ev_w
, not (has_binding binds ev_i)
| has_binding binds ev_id_w
, not (has_binding binds ev_id_i)
, not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
= KeepWork
| otherwise
= KeepInert
has_binding binds ev = isJust (lookupEvBind binds (ctEvEvId ev))
has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
{-
Note [Replacement vs keeping]
......@@ -616,22 +619,34 @@ we keep? More subtle than you might think!
* Constraints coming from the same level (i.e. same implication)
- Always get rid of InstSC ones if possible, since they are less
useful for solving. If both are InstSC, choose the one with
the smallest TypeSize
See Note [Solving superclass constraints] in TcInstDcls
(a) Always get rid of InstSC ones if possible, since they are less
useful for solving. If both are InstSC, choose the one with
the smallest TypeSize
See Note [Solving superclass constraints] in TcInstDcls
- Keep the one that has a non-trivial evidence binding.
Example: f :: (Eq a, Ord a) => blah
then we may find [G] d3 :: Eq a
[G] d2 :: Eq a
with bindings d3 = sc_sel (d1::Ord a)
(b) Keep the one that has a non-trivial evidence binding.
Example: f :: (Eq a, Ord a) => blah
then we may find [G] d3 :: Eq a
[G] d2 :: Eq a
with bindings d3 = sc_sel (d1::Ord a)
We want to discard d2 in favour of the superclass selection from
the Ord dictionary.
Why? See Note [Tracking redundant constraints] in TcSimplify again.
* Finally, when there is still a choice, use IRKeep rather than
IRReplace, to avoid unnecessary munging of the inert set.
Why? See Note [Tracking redundant constraints] in TcSimplify again.
(c) But don't do (b) if the evidence binding depends transitively on the
one without a binding. Example (with RecursiveSuperClasses)
class C a => D a
class D a => C a
Inert: d1 :: C a, d2 :: D a
Binds: d3 = sc_sel d2, d2 = sc_sel d1
Work item: d3 :: C a
Then it'd be ridiculous to replace d1 with d3 in the inert set!
Hence the findNeedEvVars test. See Trac #14774.
* Finally, when there is still a choice, use KeepInert rather than
KeepWork, for two reasons:
- to avoid unnecessary munging of the inert set.
- to cut off superclass loops; see Note [Superclass loops] in TcCanonical
Doing the depth-check for implicit parameters, rather than making the work item
always override, is important. Consider
......
......@@ -1463,7 +1463,7 @@ expandSuperClasses unsolved
| not (anyBag superClassesMightHelp unsolved)
= return (True, unsolved)
| otherwise
= do { traceTcS "expandSuperClasses {" empty
= do { traceTcS "expandSuperClasses {" (ppr unsolved)
; let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
get acc ct | Just ct' <- isPendingScDict ct
= (ct':acc, ct')
......@@ -1474,7 +1474,10 @@ expandSuperClasses unsolved
then do { traceTcS "End expandSuperClasses no-op }" empty
; return (True, unsolved) }
else
do { new_given <- makeSuperClasses pending_given
do { traceTcS "expandSuperClasses mid"
(vcat [ text "pending_given:" <+> ppr pending_given
, text "pending_wanted:" <+> ppr pending_wanted ])
; new_given <- makeSuperClasses pending_given
; solveSimpleGivens new_given
; new_wanted <- makeSuperClasses pending_wanted
; traceTcS "End expandSuperClasses }"
......@@ -1696,7 +1699,7 @@ neededEvVars implic@(Implic { ic_info = info
; let seeds1 = foldrBag add_implic_seeds old_needs implics
seeds2 = foldEvBindMap add_wanted seeds1 ev_binds
seeds3 = seeds2 `unionVarSet` tcvs
need_inner = transCloVarSet (also_needs ev_binds) seeds3
need_inner = findNeededEvVars ev_binds seeds3
live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
need_outer = foldEvBindMap del_ev_bndr need_inner live_ev_binds
`delVarSetList` givens
......@@ -1729,19 +1732,6 @@ neededEvVars implic@(Implic { ic_info = info
| is_given = needs -- Add the rhs vars of the Wanted bindings only
| otherwise = evVarsOfTerm rhs `unionVarSet` needs
also_needs :: EvBindMap -> VarSet -> VarSet
also_needs ev_binds needs
= nonDetFoldUniqSet add emptyVarSet needs
-- It's OK to use nonDetFoldUFM here because we immediately
-- forget about the ordering by creating a set
where
add v needs
| Just ev_bind <- lookupEvBind ev_binds v
, EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
, is_given
= evVarsOfTerm rhs `unionVarSet` needs
| otherwise
= needs
{- Note [Delete dead Given evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -6,6 +6,10 @@ T14434:
'$(TEST_HC)' $(TEST_HC_OPTS) -c T14434.hs -ddump-simpl | grep toStringX
# Expecting toStringX = toString, not discarding argument
T14774:
'$(TEST_HC)' $(TEST_HC_OPTS) -c T14774.hs -ddump-simpl | grep p1D
# Expecting no superclass selections to actually happen
tc170:
$(RM) Tc170_Aux.hi Tc170_Aux.o tc170.hi tc170.o
'$(TEST_HC)' $(TEST_HC_OPTS) -c Tc170_Aux.hs
......
{-# LANGUAGE UndecidableSuperClasses #-}
module T14774 where
class C a => D a where
cop :: a -> Bool
class D a => C a where
dop :: a -> a
f :: C a => Int -> a -> Bool
f 0 x = cop x
f n x = f (n-1) x
T14774.$p1D :: forall a. D a => C a
RULES: Built in rule for T14774.$p1D: "Class op $p1D"]
T14774.$p1D
......@@ -592,3 +592,4 @@ test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutio
test('T13032', normal, compile, [''])
test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
test('T14732', normal, compile, [''])
test('T14774', [], run_command, ['$MAKE -s --no-print-directory T14774'])
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