Commit 97420b05 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments only (on recursive dictionaries)

parent e5671302
......@@ -1009,23 +1009,28 @@ superclass is bottom when it should not be.
Consider the following (extreme) situation:
class C a => D a where ...
instance D [a] => D [a] where ...
instance D [a] => D [a] where ... (dfunD)
instance C [a] => C [a] where ... (dfunC)
Although this looks wrong (assume D [a] to prove D [a]), it is only a
more extreme case of what happens with recursive dictionaries, and it
can, just about, make sense because the methods do some work before
recursing.
To implement the dfun we must generate code for the superclass C [a],
To implement the dfunD we must generate code for the superclass C [a],
which we had better not get by superclass selection from the supplied
argument:
dfun :: forall a. D [a] -> D [a]
dfun = \d::D [a] -> MkD (scsel d) ..
dfunD :: forall a. D [a] -> D [a]
dfunD = \d::D [a] -> MkD (scsel d) ..
Otherwise if we later encounter a situation where
we have a [Wanted] dw::D [a] we might solve it thus:
dw := dfun dw
dw := dfunD dw
Which is all fine except that now ** the superclass C is bottom **!
The instance we want is:
dfunD :: forall a. D [a] -> D [a]
dfunD = \d::D [a] -> MkD (dfunC (scsel d)) ...
THE SOLUTION
Our solution to this problem "silent superclass arguments". We pass
......
......@@ -1087,56 +1087,69 @@ Consider generating the superclasses of the instance declaration
instance Foo a => Foo [a]
So our problem is this
d0 :_g Foo t
d1 :_w Data Maybe [t]
[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:
d0 :_g Foo t
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
WorkList
d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
d1 :_w Data Maybe [t]
Then d2 can readily enter the inert, and we also do solving of the wanted
[W] d1 : Data Maybe [t]
Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
Inert:
d0 :_g Foo t
d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
Solved:
d1 : Data Maybe [t]
WorkList
d2 :_w Sat (Maybe [t])
d3 :_w Data Maybe t
d01 :_g Data Maybe t
Now, we may simplify d2 more:
[W] d2 : Sat (Maybe [t])
[W] d3 : Data Maybe t
Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
Inert:
d0 :_g Foo t
d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
d1 :_g Data Maybe [t]
d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
Solved:
d1 : Data Maybe [t]
d2 : Sat (Maybe [t])
WorkList:
d3 :_w Data Maybe t
d4 :_w Foo [t]
d01 :_g Data Maybe t
[W] d3 : Data Maybe t
[W] d4 : Foo [t]
Now, we can just solve d3.
Now, we can just solve d3 from d01; d3 := d01
Inert
d0 :_g Foo t
d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
[G] d0 : Foo t
[G] d01 : Data Maybe t -- Superclass of d0
Solved:
d1 : Data Maybe [t]
d2 : Sat (Maybe [t])
WorkList
d4 :_w Foo [t]
d01 :_g Data Maybe t
And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
[W] d4 : Foo [t]
Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
Inert
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
[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:
d5 :_w Foo t
d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
d01 :_g Data Maybe t
Now, d5 can be solved! (and its superclass enter scope)
Inert
[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
......
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