diff options
-rw-r--r-- | compiler/typecheck/TcCanonical.hs | 128 | ||||
-rw-r--r-- | compiler/typecheck/TcInstDcls.hs | 5 | ||||
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 485 | ||||
-rw-r--r-- | compiler/typecheck/TcSMonad.hs | 167 |
4 files changed, 264 insertions, 521 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 493e742058..ee8b201bcc 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -242,67 +242,95 @@ emitSuperclasses _ = panic "emit_superclasses of non-class!" {- Note [Adding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~ -Since dictionaries are canonicalized only once in their lifetime, the -place to add their superclasses is canonicalisation (The alternative -would be to do it during constraint solving, but we'd have to be -extremely careful to not repeatedly introduced the same superclass in -our worklist). Here is what we do: - -For Givens: - We add all their superclasses as Givens. - -For Wanteds: - Generally speaking we want to be able to add superclasses of - wanteds for two reasons: - - (1) Oportunities for improvement. Example: - class (a ~ b) => C a b - Wanted constraint is: C alpha beta - We'd like to simply have C alpha alpha. Similar - situations arise in relation to functional dependencies. - - (2) To have minimal constraints to quantify over: - For instance, if our wanted constraint is (Eq a, Ord a) - we'd only like to quantify over Ord a. - - To deal with (1) above we only add the superclasses of wanteds - which may lead to improvement, that is: equality superclasses or - superclasses with functional dependencies. - - We deal with (2) completely independently in TcSimplify. See - Note [Minimize by SuperClasses] in TcSimplify. - - Moreover, in all cases the extra improvement constraints are - Derived. Derived constraints have an identity (for now), but - we don't do anything with their evidence. For instance they - are never used to rewrite other constraints. - - See also [New Wanted Superclass Work] in TcInteract. - - -For Deriveds: - We do nothing. +Since dictionaries are canonicalized only once in their lifetime, the +place to add their superclasses is canonicalisation. See Note [Add +superclasses only during canonicalisation]. Here is what we do: + + Deriveds: Do nothing. + + Givens: Add all their superclasses as Givens. + + Wanteds: Add all their superclasses as Derived. + Not as Wanted: we don't need a proof. + Nor as Given: that leads to superclass loops. + +We also want to ensure minimal constraints to quantify over. For +instance, if our wanted constraint is (Eq a, Ord a) we'd only like to +quantify over Ord a. But we deal with that completely independently +in TcSimplify. See Note [Minimize by SuperClasses] in TcSimplify. + +Examples of how adding superclasses as Derived is useful + + --- Example 1 + class C a b | a -> b + Suppose we want to solve + [G] C a b + [W] C a beta + Then adding [D] beta~b will let us solve it. + + -- Example 2 (similar but using a type-equality superclass) + class (F a ~ b) => C a b + And try to sllve: + [G] C a b + [W] C a beta + Follow the superclass rules to add + [G] F a ~ b + [D] F a ~ beta + Now we we get [D] beta ~ b, and can solve that. + +Example of why adding superclass of a Wanted as a Given would +be terrible, see Note [Do not add superclasses of solved dictionaries] +in TcSMonad, which has this example: + class Ord a => C a where + instance Ord [a] => C [a] where ... +Suppose we are trying to solve + [G] d1 : Ord a + [W] d2 : C [a] +If we (bogusly) added the superclass of d2 as Gievn we'd have + [G] d1 : Ord a + [W] d2 : C [a] + [G] d3 : Ord [a] -- Superclass of d2, bogus + +Then we'll use the instance decl to give + [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d4 + [G] d3 : Ord [a] -- Superclass of d2, bogus + [W] d4: Ord [a] + +ANd now we could bogusly solve d4 from d3. + + +Note [Add superclasses only during canonicalisation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We add superclasses only during canonicalisation, on the passage +from CNonCanonical to CDictCan. A class constraint can be repeatedly +rewritten, and there's no point in repeatedly adding its superclasses. -Here's an example that demonstrates why we chose to NOT add -superclasses during simplification: [Comes from ticket #4497] +Here's a serious, but now out-dated example, from Trac #4497: class Num (RealOf t) => Normed t type family RealOf x Assume the generated wanted constraint is: - RealOf e ~ e, Normed e + [W] RealOf e ~ e + [W] Normed e + If we were to be adding the superclasses during simplification we'd get: - Num uf, Normed e, RealOf e ~ e, RealOf e ~ uf + [W] RealOf e ~ e + [W] Normed e + [D] RealOf e ~ fuv + [D] Num fuv ==> - e ~ uf, Num uf, Normed e, RealOf e ~ e -==> [Spontaneous solve] - Num uf, Normed uf, RealOf uf ~ uf + e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv -While looks exactly like our original constraint. If we add the superclass again we'd loop. -By adding superclasses definitely only once, during canonicalisation, this situation can't +While looks exactly like our original constraint. If we add the +superclass of (Normed fuv) again we'd loop. By adding superclasses +definitely only once, during canonicalisation, this situation can't happen. --} + +Mind you, now that Wanteds cannot rewrite Derived, I think this particular +situation can't happen. + -} newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS () -- Returns superclasses, see Note [Adding superclasses] diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index 1955c1f218..c8746ff00e 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -1105,6 +1105,9 @@ See Trac #3731, #4809, #5751, #5913, #6117, #6161, which all describe somewhat more complicated situations, but ones encountered in practice. +See also tests tcrun020, tcrun021, tcrun033 + + ----- THE PROBLEM -------- The problem is that it is all too easy to create a class whose superclass is bottom when it should not be. @@ -1190,8 +1193,6 @@ that is *not* smaller than the target so we can't take *its* superclasses. As a result the program is rightly rejected, unless you add (Super (Fam a)) to the context of (i3). - - Note [Silent superclass arguments] (historical interest) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ NB1: this note describes our *old* solution to the diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 41f508daef..8b85a712e9 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -901,8 +901,6 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () -- Precondition: kind(xi) is a sub-kind of kind(tv) -- Precondition: CtEvidence is Wanted or Derived -- Precondition: CtEvidence is nominal --- See [New Wanted Superclass Work] to see why solveByUnification --- must work for Derived as well as Wanted -- Returns: workItem where -- workItem = the new Given constraint -- @@ -1100,342 +1098,6 @@ double unifications is the main reason we disallow touchable unification variables as RHS of type family equations: F xis ~ alpha. - -Note [Superclasses and recursive dictionaries] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - Overlaps with Note [SUPERCLASS-LOOP 1] - Note [SUPERCLASS-LOOP 2] - Note [Recursive instances and superclases] - ToDo: check overlap and delete redundant stuff - -Right before adding a given into the inert set, we must -produce some more work, that will bring the superclasses -of the given into scope. The superclass constraints go into -our worklist. - -When we simplify a wanted constraint, if we first see a matching -instance, we may produce new wanted work. To (1) avoid doing this work -twice in the future and (2) to handle recursive dictionaries we may ``cache'' -this item as given into our inert set WITHOUT adding its superclass constraints, -otherwise we'd be in danger of creating a loop [In fact this was the exact reason -for doing the isGoodRecEv check in an older version of the type checker]. - -But now we have added partially solved constraints to the worklist which may -interact with other wanteds. Consider the example: - -Example 1: - - class Eq b => Foo a b --- 0-th selector - instance Eq a => Foo [a] a --- fooDFun - -and wanted (Foo [t] t). We are first going to see that the instance matches -and create an inert set that includes the solved (Foo [t] t) but not its superclasses: - d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3 -Our work list is going to contain a new *wanted* goal - d3 :_w Eq t - -Ok, so how do we get recursive dictionaries, at all: - -Example 2: - - data D r = ZeroD | SuccD (r (D r)); - - instance (Eq (r (D r))) => Eq (D r) where - ZeroD == ZeroD = True - (SuccD a) == (SuccD b) = a == b - _ == _ = False; - - equalDC :: D [] -> D [] -> Bool; - equalDC = (==); - -We need to prove (Eq (D [])). Here's how we go: - - d1 :_w Eq (D []) - -by instance decl, holds if - d2 :_w Eq [D []] - where d1 = dfEqD d2 - -*BUT* we have an inert set which gives us (no superclasses): - d1 :_g Eq (D []) -By the instance declaration of Eq we can show the 'd2' goal if - d3 :_w Eq (D []) - where d2 = dfEqList d3 - d1 = dfEqD d2 -Now, however this wanted can interact with our inert d1 to set: - d3 := d1 -and solve the goal. Why was this interaction OK? Because, if we chase the -evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we -are really setting - d3 := dfEqD2 (dfEqList d3) -which is FINE because the use of d3 is protected by the instance function -applications. - -So, our strategy is to try to put solved wanted dictionaries into the -inert set along with their superclasses (when this is meaningful, -i.e. when new wanted goals are generated) but solve a wanted dictionary -from a given only in the case where the evidence variable of the -wanted is mentioned in the evidence of the given (recursively through -the evidence binds) in a protected way: more instance function applications -than superclass selectors. - -Here are some more examples from GHC's previous type checker - - -Example 3: -This code arises in the context of "Scrap Your Boilerplate with Class" - - class Sat a - class Data ctx a - instance Sat (ctx Char) => Data ctx Char -- dfunData1 - instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2 - - class Data Maybe a => Foo a - - instance Foo t => Sat (Maybe t) -- dfunSat - - instance Data Maybe a => Foo a -- dfunFoo1 - instance Foo a => Foo [a] -- dfunFoo2 - instance Foo [Char] -- dfunFoo3 - -Consider generating the superclasses of the instance declaration - instance Foo a => Foo [a] - -So our problem is this - [G] d0 : Foo t - [W] d1 : Data Maybe [t] -- Desired superclass - -We may add the given in the inert set, along with its superclasses -[assuming we don't fail because there is a matching instance, see - topReactionsStage, given case ] - Inert: - [G] d0 : Foo t - [G] d01 : Data Maybe t -- Superclass of d0 - WorkList - [W] d1 : Data Maybe [t] - -Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3 - Inert: - [G] d0 : Foo t - [G] d01 : Data Maybe t -- Superclass of d0 - Solved: - d1 : Data Maybe [t] - WorkList - [W] d2 : Sat (Maybe [t]) - [W] d3 : Data Maybe t - -Now, we may simplify d2 using dfunSat; d2 := dfunSat d4 - Inert: - [G] d0 : Foo t - [G] d01 : Data Maybe t -- Superclass of d0 - Solved: - d1 : Data Maybe [t] - d2 : Sat (Maybe [t]) - WorkList: - [W] d3 : Data Maybe t - [W] d4 : Foo [t] - -Now, we can just solve d3 from d01; d3 := d01 - Inert - [G] d0 : Foo t - [G] d01 : Data Maybe t -- Superclass of d0 - Solved: - d1 : Data Maybe [t] - d2 : Sat (Maybe [t]) - WorkList - [W] d4 : Foo [t] - -Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5 - Inert - [G] d0 : Foo t - [G] d01 : Data Maybe t -- Superclass of d0 - Solved: - d1 : Data Maybe [t] - d2 : Sat (Maybe [t]) - d4 : Foo [t] - WorkList: - [W] d5 : Foo t - -Now, d5 can be solved! d5 := d0 - -Result - d1 := dfunData2 d2 d3 - d2 := dfunSat d4 - d3 := d01 - d4 := dfunFoo2 d5 - d5 := d0 - - d0 :_g Foo t - d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3 - d2 :_g Sat (Maybe [t]) d2 := dfunSat d4 - d4 :_g Foo [t] d4 := dfunFoo2 d5 - d5 :_g Foo t d5 := dfunFoo1 d7 - WorkList: - d7 :_w Data Maybe t - d6 :_g Data Maybe [t] - d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0 - d01 :_g Data Maybe t - -Now, two problems: - [1] Suppose we pick d8 and we react him with d01. Which of the two givens should - we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence - that must not be used (look at case interactInert where both inert and workitem - are givens). So we have several options: - - Drop the workitem always (this will drop d8) - This feels very unsafe -- what if the work item was the "good" one - that should be used later to solve another wanted? - - Don't drop anyone: the inert set may contain multiple givens! - [This is currently implemented] - -The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2: - [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted - d7. Now the [isRecDictEv] function in the ineration solver - [case inert-given workitem-wanted] will prevent us from interacting d7 := d8 - precisely because chasing the evidence of d8 leads us to an unguarded use of d7. - - So, no interaction happens there. Then we meet d01 and there is no recursion - problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01! - -Note [SUPERCLASS-LOOP 1] -~~~~~~~~~~~~~~~~~~~~~~~~ -We have to be very, very careful when generating superclasses, lest we -accidentally build a loop. Here's an example: - - class S a - - class S a => C a where { opc :: a -> a } - class S b => D b where { opd :: b -> b } - - instance C Int where - opc = opd - - instance D Int where - opd = opc - -From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int} -Simplifying, we may well get: - $dfCInt = :C ds1 (opd dd) - dd = $dfDInt - ds1 = $p1 dd -Notice that we spot that we can extract ds1 from dd. - -Alas! Alack! We can do the same for (instance D Int): - - $dfDInt = :D ds2 (opc dc) - dc = $dfCInt - ds2 = $p1 dc - -And now we've defined the superclass in terms of itself. -Two more nasty cases are in - tcrun021 - tcrun033 - -Solution: - - Satisfy the superclass context *all by itself* - (tcSimplifySuperClasses) - - And do so completely; i.e. no left-over constraints - to mix with the constraints arising from method declarations - - -Note [SUPERCLASS-LOOP 2] -~~~~~~~~~~~~~~~~~~~~~~~~ -We need to be careful when adding "the constaint we are trying to prove". -Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where - - class Ord a => C a where - instance Ord [a] => C [a] where ... - -Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the -superclasses of C [a] to avails. But we must not overwrite the binding -for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just -build a loop! - -Here's another variant, immortalised in tcrun020 - class Monad m => C1 m - class C1 m => C2 m x - instance C2 Maybe Bool -For the instance decl we need to build (C1 Maybe), and it's no good if -we run around and add (C2 Maybe Bool) and its superclasses to the avails -before we search for C1 Maybe. - -Here's another example - class Eq b => Foo a b - instance Eq a => Foo [a] a -If we are reducing - (Foo [t] t) - -we'll first deduce that it holds (via the instance decl). We must not -then overwrite the Eq t constraint with a superclass selection! - -At first I had a gross hack, whereby I simply did not add superclass constraints -in addWanted, though I did for addGiven and addIrred. This was sub-optimal, -because it lost legitimate superclass sharing, and it still didn't do the job: -I found a very obscure program (now tcrun021) in which improvement meant the -simplifier got two bites a the cherry... so something seemed to be an Stop -first time, but reducible next time. - -Now we implement the Right Solution, which is to check for loops directly -when adding superclasses. It's a bit like the occurs check in unification. - -Note [Recursive instances and superclases] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this code, which arises in the context of "Scrap Your -Boilerplate with Class". - - class Sat a - class Data ctx a - instance Sat (ctx Char) => Data ctx Char - instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] - - class Data Maybe a => Foo a - - instance Foo t => Sat (Maybe t) - - instance Data Maybe a => Foo a - instance Foo a => Foo [a] - instance Foo [Char] - -In the instance for Foo [a], when generating evidence for the superclasses -(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]). -Using the instance for Data, we therefore need - (Sat (Maybe [a], Data Maybe a) -But we are given (Foo a), and hence its superclass (Data Maybe a). -So that leaves (Sat (Maybe [a])). Using the instance for Sat means -we need (Foo [a]). And that is the very dictionary we are bulding -an instance for! So we must put that in the "givens". So in this -case we have - Given: Foo a, Foo [a] - Wanted: Data Maybe [a] - -BUT we must *not not not* put the *superclasses* of (Foo [a]) in -the givens, which is what 'addGiven' would normally do. Why? Because -(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted -by selecting a superclass from Foo [a], which simply makes a loop. - -On the other hand we *must* put the superclasses of (Foo a) in -the givens, as you can see from the derivation described above. - -Conclusion: in the very special case of tcSimplifySuperClasses -we have one 'given' (namely the "this" dictionary) whose superclasses -must not be added to 'givens' by addGiven. - -There is a complication though. Suppose there are equalities - instance (Eq a, a~b) => Num (a,b) -Then we normalise the 'givens' wrt the equalities, so the original -given "this" dictionary is cast to one of a different type. So it's a -bit trickier than before to identify the "special" dictionary whose -superclasses must not be added. See test - indexed-types/should_run/EqInInstance - -We need a persistent property of the dictionary to record this -special-ness. Current I'm using the InstLocOrigin (a bit of a hack, -but cool), which is maintained by dictionary normalisation. -Specifically, the InstLocOrigin is - NoScOrigin -then the no-superclass thing kicks in. WATCH OUT if you fiddle -with InstLocOrigin! - - ************************************************************************ * * * Functional dependencies, instantiation of equations @@ -1498,9 +1160,6 @@ doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct) -- (a) The place to add superclasses in not here in doTopReact stage. -- Instead superclasses are added in the worklist as part of the -- canonicalization process. See Note [Adding superclasses]. --- --- (b) See Note [Given constraint that matches an instance declaration] --- for some design decisions for given dictionaries. doTopReact inerts work_item = do { traceTcS "doTopReact" (ppr work_item) @@ -1834,113 +1493,6 @@ This should probably be well typed, with So the inner binding for ?x::Bool *overrides* the outer one. Hence a work-item Given overrides an inert-item Given. - -Note [Given constraint that matches an instance declaration] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -What should we do when we discover that one (or more) top-level -instances match a given (or solved) class constraint? We have -two possibilities: - - 1. Reject the program. The reason is that there may not be a unique - best strategy for the solver. Example, from the OutsideIn(X) paper: - instance P x => Q [x] - instance (x ~ y) => R [x] y - - wob :: forall a b. (Q [b], R b a) => a -> Int - - g :: forall a. Q [a] => [a] -> Int - g x = wob x - - will generate the impliation constraint: - Q [a] => (Q [beta], R beta [a]) - If we react (Q [beta]) with its top-level axiom, we end up with a - (P beta), which we have no way of discharging. On the other hand, - if we react R beta [a] with the top-level we get (beta ~ a), which - is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is - now solvable by the given Q [a]. - - However, this option is restrictive, for instance [Example 3] from - Note [Recursive instances and superclases] will fail to work. - - 2. Ignore the problem, hoping that the situations where there exist indeed - such multiple strategies are rare: Indeed the cause of the previous - problem is that (R [x] y) yields the new work (x ~ y) which can be - *spontaneously* solved, not using the givens. - -We are choosing option 2 below but we might consider having a flag as well. - - -Note [New Wanted Superclass Work] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Even in the case of wanted constraints, we may add some superclasses -as new given work. The reason is: - - To allow FD-like improvement for type families. Assume that - we have a class - class C a b | a -> b - and we have to solve the implication constraint: - C a b => C a beta - Then, FD improvement can help us to produce a new wanted (beta ~ b) - - We want to have the same effect with the type family encoding of - functional dependencies. Namely, consider: - class (F a ~ b) => C a b - Now suppose that we have: - given: C a b - wanted: C a beta - By interacting the given we will get given (F a ~ b) which is not - enough by itself to make us discharge (C a beta). However, we - may create a new derived equality from the super-class of the - wanted constraint (C a beta), namely derived (F a ~ beta). - Now we may interact this with given (F a ~ b) to get: - derived : beta ~ b - But 'beta' is a touchable unification variable, and hence OK to - unify it with 'b', replacing the derived evidence with the identity. - - This requires trySpontaneousSolve to solve *derived* - equalities that have a touchable in their RHS, *in addition* - to solving wanted equalities. - -We also need to somehow use the superclasses to quantify over a minimal, -constraint see note [Minimize by Superclasses] in TcSimplify. - - -Finally, here is another example where this is useful. - -Example 1: ----------- - class (F a ~ b) => C a b -And we are given the wanteds: - w1 : C a b - w2 : C a c - w3 : b ~ c -We surely do *not* want to quantify over (b ~ c), since if someone provides -dictionaries for (C a b) and (C a c), these dictionaries can provide a proof -of (b ~ c), hence no extra evidence is necessary. Here is what will happen: - - Step 1: We will get new *given* superclass work, - provisionally to our solving of w1 and w2 - - g1: F a ~ b, g2 : F a ~ c, - w1 : C a b, w2 : C a c, w3 : b ~ c - - The evidence for g1 and g2 is a superclass evidence term: - - g1 := sc w1, g2 := sc w2 - - Step 2: The givens will solve the wanted w3, so that - w3 := sym (sc w1) ; sc w2 - - Step 3: Now, one may naively assume that then w2 can be solve from w1 - after rewriting with the (now solved equality) (b ~ c). - - But this rewriting is ruled out by the isGoodRectDict! - -Conclusion, we will (correctly) end up with the unsolved goals - (C a b, C a c) - -NB: The desugarer needs be more clever to deal with equalities - that participate in recursive dictionary bindings. -} data LookupInstResult @@ -2068,22 +1620,27 @@ matchClassInst inerts clas tys loc {- Note [Instance and Given overlap] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Assume that we have an inert set that looks as follows: - [Given] D [Int] -And an instance declaration: - instance C a => D [a] -A new wanted comes along of the form: - [Wanted] D [alpha] - -One possibility is to apply the instance declaration which will leave us -with an unsolvable goal (C alpha). However, later on a new constraint may -arise (for instance due to a functional dependency between two later dictionaries), -that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha]) -will be transformed to [Wanted] D [Int], which could have been discharged by the given. - -The solution is that in matchClassInst and eventually in topReact, we get back with -a matching instance, only when there is no Given in the inerts which is unifiable to -this particular dictionary. +Example, from the OutsideIn(X) paper: + instance P x => Q [x] + instance (x ~ y) => R y [x] + + wob :: forall a b. (Q [b], R b a) => a -> Int + + g :: forall a. Q [a] => [a] -> Int + g x = wob x + +This will generate the impliation constraint: + Q [a] => (Q [beta], R beta [a]) +If we react (Q [beta]) with its top-level axiom, we end up with a +(P beta), which we have no way of discharging. On the other hand, +if we react R beta [a] with the top-level we get (beta ~ a), which +is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is +now solvable by the given Q [a]. + +The solution is that: + In matchClassInst (and thus in topReact), we return a matching + instance only when there is no Given in the inerts which is + unifiable to this particular dictionary. The end effect is that, much as we do for overlapping instances, we delay choosing a class instance if there is a possibility of another instance OR a given to match our diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index a04bf9f43c..56c8a9ab2f 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -378,6 +378,165 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places using w3 itself! * The inert_funeqs are un-solved but fully processed and in the InertCans. + +Note [Solved dictionaries] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we apply a top-level instance declararation, we add the "solved" +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. +The simplest, degnerate case is + instance C [a] => C [a] where ... +If we have + [W] d1 :: C [x] +then we can apply the instance to get + d1 = $dfCList d + [W] d2 :: C [x] +Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1. + d1 = $dfCList d + d2 = d1 + +See Note [Example of recursive dictionaries] +Other notes about solved dictionaries + +* See also Note [Do not add superclasses of solved dictionaries] + +* The inert_solved_dicts field is not rewritten by equalities, so it may + get out of date. + +Note [Do not add superclasses of solved dictionaries] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Every member of inert_solved_dicts is the result of applying a dictionary +function, NOT of applying superclass selection to anything. +Consider + + class Ord a => C a where + instance Ord [a] => C [a] where ... + +Suppose we are trying to solve + [G] d1 : Ord a + [W] d2 : C [a] + +Then we'll use the instance decl to give + + [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d3 + [W] d3 : Ord [a] + +We must not add d4 : Ord [a] to the 'solved' set (by taking the +superclass of d2), otherwise we'll use it to solve d3, without ever +using d1, which would be a catastrophe. + +Solution: when extending the solved dictionaries, do not add superclasses. +That's why each element of the inert_solved_dicts is the result of applying +a dictionary function. + +Note [Example of recursive dictionaries] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +--- Example 1 + + data D r = ZeroD | SuccD (r (D r)); + + instance (Eq (r (D r))) => Eq (D r) where + ZeroD == ZeroD = True + (SuccD a) == (SuccD b) = a == b + _ == _ = False; + + equalDC :: D [] -> D [] -> Bool; + equalDC = (==); + +We need to prove (Eq (D [])). Here's how we go: + + [W] d1 : Eq (D []) +By instance decl of Eq (D r): + [W] d2 : Eq [D []] where d1 = dfEqD d2 +By instance decl of Eq [a]: + [W] d3 : Eq (D []) where d2 = dfEqList d3 + d1 = dfEqD d2 +Now this wanted can interact with our "solved" d1 to get: + d3 = d1 + +-- Example 2: +This code arises in the context of "Scrap Your Boilerplate with Class" + + class Sat a + class Data ctx a + instance Sat (ctx Char) => Data ctx Char -- dfunData1 + instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2 + + class Data Maybe a => Foo a + + instance Foo t => Sat (Maybe t) -- dfunSat + + instance Data Maybe a => Foo a -- dfunFoo1 + instance Foo a => Foo [a] -- dfunFoo2 + instance Foo [Char] -- dfunFoo3 + +Consider generating the superclasses of the instance declaration + instance Foo a => Foo [a] + +So our problem is this + [G] d0 : Foo t + [W] d1 : Data Maybe [t] -- Desired superclass + +We may add the given in the inert set, along with its superclasses + Inert: + [G] d0 : Foo t + [G] d01 : Data Maybe t -- Superclass of d0 + WorkList + [W] d1 : Data Maybe [t] + +Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3 + Inert: + [G] d0 : Foo t + [G] d01 : Data Maybe t -- Superclass of d0 + Solved: + d1 : Data Maybe [t] + WorkList: + [W] d2 : Sat (Maybe [t]) + [W] d3 : Data Maybe t + +Now, we may simplify d2 using dfunSat; d2 := dfunSat d4 + Inert: + [G] d0 : Foo t + [G] d01 : Data Maybe t -- Superclass of d0 + Solved: + d1 : Data Maybe [t] + d2 : Sat (Maybe [t]) + WorkList: + [W] d3 : Data Maybe t + [W] d4 : Foo [t] + +Now, we can just solve d3 from d01; d3 := d01 + Inert + [G] d0 : Foo t + [G] d01 : Data Maybe t -- Superclass of d0 + Solved: + d1 : Data Maybe [t] + d2 : Sat (Maybe [t]) + WorkList + [W] d4 : Foo [t] + +Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5 + Inert + [G] d0 : Foo t + [G] d01 : Data Maybe t -- Superclass of d0 + Solved: + d1 : Data Maybe [t] + d2 : Sat (Maybe [t]) + d4 : Foo [t] + WorkList: + [W] d5 : Foo t + +Now, d5 can be solved! d5 := d0 + +Result + d1 := dfunData2 d2 d3 + d2 := dfunSat d4 + d3 := d01 + d4 := dfunFoo2 d5 + d5 := d0 -} -- All Given (fully known) or Wanted or Derived @@ -435,11 +594,8 @@ data InertSet , inert_solved_dicts :: DictMap CtEvidence -- Of form ev :: C t1 .. tn - -- Always the result of using a top-level instance declaration - -- - Used to avoid creating a new EvVar when we have a new goal - -- that we have solved in the past - -- - Stored not necessarily as fully rewritten - -- (ToDo: rewrite lazily when we lookup) + -- See Note [Solved dictionaries] + -- and Note [Do not add superclasses of solved dictionaries] } instance Outputable InertCans where @@ -514,6 +670,7 @@ insertInertItemTcS item addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS () -- Add a new item in the solved set of the monad +-- See Note [Solved dictionaries] addSolvedDict item cls tys | isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!) = return () |