Commit 3fbf4965 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments only (superclasses and improvement)

parent 8f48fdc8
......@@ -229,18 +229,13 @@ place to add their superclasses is canonicalisation. See Note [Add
superclasses only during canonicalisation]. Here is what we do:
Givens: Add all their superclasses as Givens.
They may be needed to prove Wanteds
They may be needed to prove Wanteds.
Wanteds: Do nothing.
Deriveds: Add all their superclasses as Derived.
Wanteds/Derived:
Add all their superclasses as Derived.
The sole reason is to expose functional dependencies
in superclasses or equality superclasses.
We only do this in the improvement phase, if solving has
not succeeded; see Note [The improvement story] in
TcInteract
Examples of how adding superclasses as Derived is useful
--- Example 1
......@@ -260,6 +255,24 @@ Examples of how adding superclasses as Derived is useful
[D] F a ~ beta
Now we we get [D] beta ~ b, and can solve that.
-- Example (tcfail138)
class L a b | a -> b
class (G a, L a b) => C a b
instance C a b' => G (Maybe a)
instance C a b => C (Maybe a) a
instance L (Maybe a) a
When solving the superclasses of the (C (Maybe a) a) instance, we get
[G] C a b, and hance by superclasses, [G] G a, [G] L a b
[W] G (Maybe a)
Use the instance decl to get
[W] C a beta
Generate its derived superclass
[D] L a beta. Now using fundeps, combine with [G] L a b to get
[D] beta ~ b
which is what we want.
---------- Historical note -----------
Example of why adding superclass of a Wanted as a Given would
be terrible, see Note [Do not add superclasses of solved dictionaries]
......@@ -280,7 +293,7 @@ Then we'll use the instance decl to give
[W] d4: Ord [a]
ANd now we could bogusly solve d4 from d3.
---------- End of historical note -----------
Note [Add superclasses only during canonicalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -1523,49 +1523,6 @@ Then it is solvable, but its very hard to detect this on the spot.
It's exactly the same with implicit parameters, except that the
"aggressive" approach would be much easier to implement.
Note [When improvement happens during solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During solving we maintain at "model" in the InertCans
Improvement for functional dependencies or type-function injectivity
means emitting a Derived equality constraint by interacting the work
item with an inert item, or with the top-level instances. e.g.
class C a b | a -> b
[W] C a b, [W] C a c ==> [D] b ~ c
We fire the fundep improvement if the "work item" is Given or Derived,
but not Wanted. Reason:
* Given: we want to spot Given/Given inconsistencies because that means
unreachable code. See typecheck/should_fail/FDsFromGivens
* Derived: during the improvement phase (i.e. when handling Derived
constraints) we also do improvement for functional dependencies. e.g.
And similarly wrt top-level instances.
* Wanted: spotting fundep improvements is somewhat inefficient, and
and if we can solve without improvement so much the better.
So we don't bother to do this when solving Wanteds, instead
leaving it for the try_improvement loop
Example (tcfail138)
class L a b | a -> b
class (G a, L a b) => C a b
instance C a b' => G (Maybe a)
instance C a b => C (Maybe a) a
instance L (Maybe a) a
When solving the superclasses of the (C (Maybe a) a) instance, we get
[G] C a b, and hance by superclasses, [G] G a, [G] L a b
[W] G (Maybe a)
Use the instance decl to get
[W] C a beta
During improvement (see Note [The improvement story]) we generate the superclasses
of (C a beta): [D] L a beta. Now using fundeps, combine with [G] L a b to get
[D] beta ~ b, which is what we want.
Note [Weird fundeps]
~~~~~~~~~~~~~~~~~~~~
......
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