author Simon Peyton Jones Mon, 20 Jul 2015 22:37:42 +0000 (23:37 +0100) committer Simon Peyton Jones Tue, 21 Jul 2015 12:21:30 +0000 (13:21 +0100)

index e91304a..6f02325 100644 (file)
@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index b68dd34..6be3a2c 100644 (file)
@@ -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]
~~~~~~~~~~~~~~~~~~~~