Commit a9dc4277 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Comments only, mainly on superclasses

This tidies up all the comments about recursive superclasses
and when to add superclasses.  Lots of duplicate and contradictory
comments removed!
parent 44b65fd8
......@@ -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
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]
......@@ -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
......@@ -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 [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
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 ]
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
[W] d1 : Data Maybe [t]
Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
d1 : Data Maybe [t]
[W] d2 : Sat (Maybe [t])
[W] d3 : Data Maybe t
Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
d1 : Data Maybe [t]
d2 : Sat (Maybe [t])
[W] d3 : Data Maybe t
[W] d4 : Foo [t]
Now, we can just solve d3 from d01; d3 := d01
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
d1 : Data Maybe [t]
d2 : Sat (Maybe [t])
[W] d4 : Foo [t]
Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
d1 : Data Maybe [t]
d2 : Sat (Maybe [t])
d4 : Foo [t]
[W] d5 : Foo t
Now, d5 can be solved! d5 := d0
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
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!
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
- Satisfy the superclass context *all by itself*
- And do so completely; i.e. no left-over constraints
to mix with the constraints arising from method declarations
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
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
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)