author Simon Peyton Jones Wed, 10 Dec 2014 14:56:30 +0000 (14:56 +0000) committer Simon Peyton Jones Wed, 10 Dec 2014 16:01:19 +0000 (16:01 +0000)

index ffe39ab..2aa9243 100644 (file)
@@ -9,207 +9,6 @@ ToDo:
* RAE: I think it would be better to split off CNonCanonical into its own
type, and remove it completely from Ct. Then, we would keep CIrredCan

-===========================
-
-The inert equalities
-~~~~~~~~~~~~~~~~~~~~
-
-Definition: can-rewrite relation.
-A "can-rewrite" relation between flavours, written f1 >= f2, is a
-binary relation with the following properties
-
-  R1.  >= is transitive
-  R2.  If f1 >= f, and f2 >= f,
-       then either f1 >= f2 or f2 >= f1
-
-Lemma.  If f1 >= f then f1 >= f1
-Proof.  By property (R2), with f1=f2
-
-Definition: generalised substitution.
-A "generalised substitution" S is a set of triples (a -f-> t), where
-  a is a type variable
-  t is a type
-  f is a flavour
-such that
-  (WF1) if (a -f1-> t1) in S
-            (a -f2-> t2) in S
-        then neither (f1 >= f2) nor (f2 >= f1) hold
-  (WF2) if (a -f-> t) is in S, then t /= a
-
-Definition: applying a generalised substitution.
-If S is a generalised substitution
-   S(f,a) = t,  if (a -fs-> t) in S, and fs >= f
-          = a,  otherwise
-Application extends naturally to types S(f,t)
-
-Theorem: S(f,a) is well defined as a function.
-Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
-               and  f1 >= f and f2 >= f
-       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF)
-
-Notation: repeated application.
-  S^0(f,t)     = t
-  S^(n+1)(f,t) = S(f, S^n(t))
-
-Definition: inert generalised substitution
-A generalised substitution S is "inert" iff
-
-  (IG1) there is an n such that
-        for every f,t, S^n(f,t) = S^(n+1)(f,t)
-
-  (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
-        that is, each individual binding is "self-stable"
-
-----------------------------------------------------------------
-Our main invariant:
-   the inert CTyEqCans should be an inert generalised substitution
-----------------------------------------------------------------
-
-Note that inertness is not the same as idempotence.  To apply S to a
-type, you may have to apply it recursive.  But inertness does
-guarantee that this recursive use will terminate.
-
-The main theorem.
-   Suppose we have a "work item"
-       a -fw-> t
-   and an inert generalised substitution S,
-   such that
-      (T1) S(fw,a) = a     -- LHS of work-item is a fixpoint of S(fw,_)
-      (T2) S(fw,t) = t     -- RHS of work-item is a fixpoint of S(fw,_)
-      (T3) a not in t      -- No occurs check in the work item
-
-      (K1) if (a -fs-> s) is in S then not (fw >= fs)
-      (K2) if (b -fs-> s) is in S, where b /= a, then
-              (K2a) not (fs >= fs)
-           or (K2b) not (fw >= fs)
-           or (K2c) a not in s
-     or (K3) if (b -fs-> a) is in S then not (fw >= fs)
-             (a stronger version of (K2))
-
-   then the extended substition T = S+(a -fw-> t)
-   is an inert generalised substitution.
-
-The idea is that
-* (T1-2) are guaranteed by exhaustively rewriting the work-item
-  with S(fw,_).
-
-* T3 is guaranteed by a simple occurs-check on the work item.
-
-* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
-  "keep" criteria.) If the current inert S contains a triple that does
-  not satisfy (K1-3), then we remove it from S by "kicking it out",
-  and re-processing it.
-
-* Note that kicking out is a Bad Thing, because it means we have to
-  re-process a constraint.  The less we kick out, the better.
-
-* Assume we have  G>=G, G>=W, D>=D, and that's all.  Then, when performing
-  a unification we add a new given  a -G-> ty.  But doing so does NOT require
-  us to kick out an inert wanted that mentions a, because of (K2a).  This
-  is a common case, hence good not to kick out.
-
-* Lemma (L1): The conditions of the Main Theorem imply that there is no
-              (a fs-> t) in S, s.t.  (fs >= fw).
-  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
-  S(fw,a)=a.  But since fs>=fw, S(fw,a) = s, hence s=a.  But now we
-  have (a -fs-> a) in S, which contradicts (WF2).
-
-* The extended substitution satisfies (WF1) and (WF2)
-  - (K1) plus (L1) guarantee that the extended substiution satisfies (WF1).
-  - (T3) guarantees (WF2).
-
-* (K2) is about inertness.  Intuitively, any infinite chain T^0(f,t),
-  T^1(f,t), T^2(f,T).... must pass through the new work item infnitely
-  often, since the substution without the work item is inert; and must
-  pass through at least one of the triples in S infnitely often.
-
-  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
-    and hence this triple never plays a role in application S(f,a).
-    It is always safe to extend S with such a triple.
-
-    (NB: we could strengten K1) in this way too, but see K3.
-
-  - (K2b): If this holds, we can't pass through this triple infinitely
-    often, because if we did then fs>=f, fw>=f, hence fs>=fw,
-
-  - (K2c): if a not in s, we hae no further opportunity to apply the
-    work item.
-
-  NB: this reasoning isn't water tight.
-
-Key lemma to make it watertight.
-  Under the conditions of the Main Theorem,
-  forall f st fw >= f, a is not in S^k(f,t), for any k
-
-
-Completeness
-~~~~~~~~~~~~~
-K3: completeness.  (K3) is not ncessary for the extended substitution
-to be inert.  In fact K1 could be made stronger by saying
-   ... then (not (fw >= fs) or not (fs >= fs))
-But it's not enough for S to be inert; we also want completeness.
-That is, we want to be able to solve all soluble wanted equalities.
-Suppose we have
-
-   work-item   b -G-> a
-   inert-item  a -W-> b
-
-Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
-so we could extend the inerts, thus:
-
-   inert-items   b -G-> a
-                 a -W-> b
-
-But if we kicked-out the inert item, we'd get
-
-   work-item     a -W-> b
-   inert-item    b -G-> a
-
-Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
-So we add one more clause to the kick-out criteria
-
-Another way to understand (K3) is that we treat an inert item
-        a -f-> b
-in the same way as
-        b -f-> a
-So if we kick out one, we should kick out the other.  The orientation
-is somewhat accidental.
-
------------------------
-RAE: To prove that K3 is sufficient for completeness (as opposed to a rule that
-looked for `a` *anywhere* on the RHS, not just at the top), we need this property:
-All types in the inert set are "rigid". Here, rigid means that a type is one of
-two things: a type that can equal only itself, or a type variable. Because the
-inert set defines rewritings for type variables, a type variable can be considered
-rigid because it will be rewritten only to a rigid type.
-
-In the current world, this rigidity property is true: all type families are
-flattened away before adding equalities to the inert set. But, when we add
-representational equality, that is no longer true! Newtypes are not rigid
-w.r.t. representational equality. Accordingly, we would to change (K3) thus:
-
-(K3) If (b -fs-> s) is in S with (fw >= fs), then
-  (K3a) If the role of fs is nominal: s /= a
-  (K3b) If the role of fs is representational: EITHER
-          a not in s, OR
-          the path from the top of s to a includes at least one non-newtype
-
-SPJ/DV: this looks important... follow up
-
------------------------
-RAE: Do we have evidence to support our belief that kicking out is bad? I can
-imagine scenarios where kicking out *more* equalities is more efficient, in that
-kicking out a Given, say, might then discover that the Given is reflexive and
-thus can be dropped. Once this happens, then the Given is no longer used in
-rewriting, making later flattenings faster. I tend to thing that, probably,
-kicking out is something to avoid, but it would be nice to have data to support
-this conclusion. And, that data is not terribly hard to produce: we can just
-twiddle some settings and then time the testsuite in some sort of controlled
-environment.
-
-SPJ: yes it would be good to do that.
-
The coercion solver
~~~~~~~~~~~~~~~~~~~~
Our hope. In GHC currently drawn from {G,W,D}, but with the coercion
@@ -230,3 +29,4 @@ flattening algorithm. Flattening (T a) looks at the roles of
T's parameters, and chooses the role for flattening `a` appropriately.
This is why there must be the [Role] parameter to flattenMany.
Of course, this non-uniform rewriting may gum up the proof works.
+
index f8d2148..5cb12bd 100644 (file)
@@ -859,6 +859,207 @@ way to its *final* value, not just the single step reduction.
Flattening a type variable
*                                                                      *
************************************************************************
+
+
+Note [The inert equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Definition [Can-rewrite relation]
+A "can-rewrite" relation between flavours, written f1 >= f2, is a
+binary relation with the following properties
+
+  R1.  >= is transitive
+  R2.  If f1 >= f, and f2 >= f,
+       then either f1 >= f2 or f2 >= f1
+
+Lemma.  If f1 >= f then f1 >= f1
+Proof.  By property (R2), with f1=f2
+
+Definition [Generalised substitution]
+A "generalised substitution" S is a set of triples (a -f-> t), where
+  a is a type variable
+  t is a type
+  f is a flavour
+such that
+  (WF1) if (a -f1-> t1) in S
+            (a -f2-> t2) in S
+        then neither (f1 >= f2) nor (f2 >= f1) hold
+  (WF2) if (a -f-> t) is in S, then t /= a
+
+Definition [Applying a generalised substitution]
+If S is a generalised substitution
+   S(f,a) = t,  if (a -fs-> t) in S, and fs >= f
+          = a,  otherwise
+Application extends naturally to types S(f,t)
+
+Theorem: S(f,a) is well defined as a function.
+Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
+               and  f1 >= f and f2 >= f
+       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF)
+
+Notation: repeated application.
+  S^0(f,t)     = t
+  S^(n+1)(f,t) = S(f, S^n(t))
+
+Definition: inert generalised substitution
+A generalised substitution S is "inert" iff
+
+  (IG1) there is an n such that
+        for every f,t, S^n(f,t) = S^(n+1)(f,t)
+
+  (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
+        that is, each individual binding is "self-stable"
+
+----------------------------------------------------------------
+Our main invariant:
+   the inert CTyEqCans should be an inert generalised substitution
+----------------------------------------------------------------
+
+Note that inertness is not the same as idempotence.  To apply S to a
+type, you may have to apply it recursive.  But inertness does
+guarantee that this recursive use will terminate.
+
+---------- The main theorem --------------
+   Suppose we have a "work item"
+       a -fw-> t
+   and an inert generalised substitution S,
+   such that
+      (T1) S(fw,a) = a     -- LHS of work-item is a fixpoint of S(fw,_)
+      (T2) S(fw,t) = t     -- RHS of work-item is a fixpoint of S(fw,_)
+      (T3) a not in t      -- No occurs check in the work item
+
+      (K1) if (a -fs-> s) is in S then not (fw >= fs)
+      (K2) if (b -fs-> s) is in S, where b /= a, then
+              (K2a) not (fs >= fs)
+           or (K2b) not (fw >= fs)
+           or (K2c) a not in s
+     or (K3) if (b -fs-> a) is in S then not (fw >= fs)
+             (a stronger version of (K2))
+
+   then the extended substition T = S+(a -fw-> t)
+   is an inert generalised substitution.
+
+The idea is that
+* (T1-2) are guaranteed by exhaustively rewriting the work-item
+  with S(fw,_).
+
+* T3 is guaranteed by a simple occurs-check on the work item.
+
+* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
+  "keep" criteria.) If the current inert S contains a triple that does
+  not satisfy (K1-3), then we remove it from S by "kicking it out",
+  and re-processing it.
+
+* Note that kicking out is a Bad Thing, because it means we have to
+  re-process a constraint.  The less we kick out, the better.
+
+* Assume we have  G>=G, G>=W, D>=D, and that's all.  Then, when performing
+  a unification we add a new given  a -G-> ty.  But doing so does NOT require
+  us to kick out an inert wanted that mentions a, because of (K2a).  This
+  is a common case, hence good not to kick out.
+
+* Lemma (L1): The conditions of the Main Theorem imply that there is no
+              (a fs-> t) in S, s.t.  (fs >= fw).
+  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
+  S(fw,a)=a.  But since fs>=fw, S(fw,a) = s, hence s=a.  But now we
+  have (a -fs-> a) in S, which contradicts (WF2).
+
+* The extended substitution satisfies (WF1) and (WF2)
+  - (K1) plus (L1) guarantee that the extended substiution satisfies (WF1).
+  - (T3) guarantees (WF2).
+
+* (K2) is about inertness.  Intuitively, any infinite chain T^0(f,t),
+  T^1(f,t), T^2(f,T).... must pass through the new work item infnitely
+  often, since the substution without the work item is inert; and must
+  pass through at least one of the triples in S infnitely often.
+
+  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
+    and hence this triple never plays a role in application S(f,a).
+    It is always safe to extend S with such a triple.
+
+    (NB: we could strengten K1) in this way too, but see K3.
+
+  - (K2b): If this holds, we can't pass through this triple infinitely
+    often, because if we did then fs>=f, fw>=f, hence fs>=fw,
+
+  - (K2c): if a not in s, we hae no further opportunity to apply the
+    work item.
+
+  NB: this reasoning isn't water tight.
+
+Key lemma to make it watertight.
+  Under the conditions of the Main Theorem,
+  forall f st fw >= f, a is not in S^k(f,t), for any k
+
+
+Completeness
+~~~~~~~~~~~~~
+K3: completeness.  (K3) is not ncessary for the extended substitution
+to be inert.  In fact K1 could be made stronger by saying
+   ... then (not (fw >= fs) or not (fs >= fs))
+But it's not enough for S to be inert; we also want completeness.
+That is, we want to be able to solve all soluble wanted equalities.
+Suppose we have
+
+   work-item   b -G-> a
+   inert-item  a -W-> b
+
+Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
+so we could extend the inerts, thus:
+
+   inert-items   b -G-> a
+                 a -W-> b
+
+But if we kicked-out the inert item, we'd get
+
+   work-item     a -W-> b
+   inert-item    b -G-> a
+
+Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
+So we add one more clause to the kick-out criteria
+
+Another way to understand (K3) is that we treat an inert item
+        a -f-> b
+in the same way as
+        b -f-> a
+So if we kick out one, we should kick out the other.  The orientation
+is somewhat accidental.
+
+-----------------------
+RAE: To prove that K3 is sufficient for completeness (as opposed to a rule that
+looked for `a` *anywhere* on the RHS, not just at the top), we need this property:
+All types in the inert set are "rigid". Here, rigid means that a type is one of
+two things: a type that can equal only itself, or a type variable. Because the
+inert set defines rewritings for type variables, a type variable can be considered
+rigid because it will be rewritten only to a rigid type.
+
+In the current world, this rigidity property is true: all type families are
+flattened away before adding equalities to the inert set. But, when we add
+representational equality, that is no longer true! Newtypes are not rigid
+w.r.t. representational equality. Accordingly, we would to change (K3) thus:
+
+(K3) If (b -fs-> s) is in S with (fw >= fs), then
+  (K3a) If the role of fs is nominal: s /= a
+  (K3b) If the role of fs is representational: EITHER
+          a not in s, OR
+          the path from the top of s to a includes at least one non-newtype
+
+SPJ/DV: this looks important... follow up
+
+-----------------------
+RAE: Do we have evidence to support our belief that kicking out is bad? I can
+imagine scenarios where kicking out *more* equalities is more efficient, in that
+kicking out a Given, say, might then discover that the Given is reflexive and
+thus can be dropped. Once this happens, then the Given is no longer used in
+rewriting, making later flattenings faster. I tend to thing that, probably,
+kicking out is something to avoid, but it would be nice to have data to support
+this conclusion. And, that data is not terribly hard to produce: we can just
+twiddle some settings and then time the testsuite in some sort of controlled
+environment.
+
+SPJ: yes it would be good to do that.
+
-}

flattenTyVar :: FlattenEnv -> TcTyVar -> TcS (Xi, TcCoercion)
@@ -905,7 +1106,7 @@ flattenTyVarOuter ctxt_ev tv
Nothing ->

-- Try in the inert equalities
-    -- See Note [Applying the inert substitution]
+    -- See Definition [Applying a generalised substitution]
do { ieqs <- getInertEqs
; case lookupVarEnv ieqs tv of
Just (ct:_)   -- If the first doesn't work,
@@ -929,47 +1130,6 @@ flattenTyVarFinal ctxt_ev tv
; return (Left (setVarType tv new_knd)) }

{-
-Note [Applying the inert substitution]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  -- NB: 8 Dec 14: These notes are now not correct
-  --               Need to rewrite then when matters have settled
-
-The inert CTyEqCans (a ~ ty), inert_eqs, can be treated as a
-substitution, and indeed flattenTyVarOuter applies it to the type
-being flattened (recursively).  This process should terminate.
-
- * 'a' is not in fvs(ty)
- * They are *inert*; that is the eqCanRewrite relation is everywhere false
-
-An example of such an inert substitution is:
-
- [G] g1 : ta8 ~ ta4
- [W] g2 : ta4 ~ a5Fj
-
-If you ignored the G/W, it would not be an idempotent, but we don't ignore
-it.  When rewriting a constraint
-    ev_work :: blah
-we only rewrite it with an inert constraint
-    ev_inert1 :: a ~ ty
-if
-    ev_inert1 `eqCanRewrite` ev_work
-
-This process stops in exactly one step; that is, the RHS 'ty' cannot be further
-rewritten by any other inert.  Why not?  If it could, we'd have
-    ev_inert1 :: a ~ ty[b]
-    ev_inert2 :: b ~ ty'
-and
-    ev_inert2 `canRewrite` ev_work
-But by the EqCanRewrite Property (see Note [eqCanRewrite]), that means
-that ev_inert2 `eqCanRewrite` ev_inert1; but that means that 'b' can't
-appear free in ev_inert1's RHS.
-
-When we *unify* a variable, which we write
-  alpha := ty
-we must be sure we aren't creating an infinite type.  But that comes
-from the CTyEqCan invariant that 'a' not in fvs(ty), plus the fact that
-an inert CTyEqCan is fully zonked wrt the current unification assignments.
-In effect they become Givens, implemented via the side-effected substitution.

Note [An alternative story for the inert substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1059,13 +1219,8 @@ canRewriteOrSame _ _ = False
Note [eqCanRewrite]
~~~~~~~~~~~~~~~~~~~
(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
-tv ~ ty) can be used to rewrite ct2.
-
-The EqCanRewrite Property:
-  * For any a,b in {G,W,D}  if   a eqCanRewrite b
-                            then a eqCanRewrite a
-  This is what guarantees that canonicalisation will terminate.
-  See Note [Applying the inert substitution]
+tv ~ ty) can be used to rewrite ct2.  It must satisfy the properties of
+a can-rewrite relation, see Definition [Can-rewrite relation]

At the moment we don't allow Wanteds to rewrite Wanteds, because that can give
rise to very confusing type error messages.  A good example is Trac #8450.
index e3ce77e..026ff6d 100644 (file)
@@ -1010,15 +1010,14 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
where
(eqs_out, eqs_in) = partition kick_out_eq eqs

+    -- kick_out_eq implements kick-out criteria (K1-3)
+    -- in the main theorem of Note [The inert equalities] in TcFlatten
kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev })
=  eqCanRewrite new_ev ev
&& (tv == new_tv
|| (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty)
|| case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False })
kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct)
-    -- SLPJ new piece: Don't kick out a constraint unless it can rewrite itself,
-    --                 If not, it can't rewrite anything else, so no point in
-    --                 kicking it out

{-
Note [Kicking out inert constraints]
@@ -1060,50 +1059,6 @@ Now it can be decomposed.  Otherwise we end up with a "Can't match
[Int] ~ [[Int]]" which is true, but a bit confusing because the
outer type constructors match.

-Note [Delicate equality kick-out]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When adding an fully-rewritten work-item CTyEqCan (a ~ xi), we kick
-out an inert CTyEqCan (b ~ phi) when
-
-  a) the work item can rewrite the inert item
-
-AND one of the following hold
-
-(0) If the new tyvar is the same as the old one
-      Work item: [G] a ~ blah
-      Inert:     [W] a ~ foo
-    A particular case is when flatten-skolems get their value we must propagate
-
-(1) If the new tyvar appears in the kind vars of the LHS or RHS of
-    the inert.  Example:
-    Work item: [G] k ~ *
-    Inert:     [W] (a:k) ~ ty
-               [W] (b:*) ~ c :: k
-    We must kick out those blocked inerts so that we rewrite them
-    and can subsequently unify.
-
-(2) If the new tyvar appears in the RHS of the inert
-    AND not (the inert can rewrite the work item)   <---------------------------------
-
-          Work item:  [G] a ~ b
-          Inert:      [W] b ~ [a]
-    Now at this point the work item cannot be further rewritten by the
-    inert (due to the weaker inert flavor). But we can't add the work item
-    as-is because the inert set would then have a cyclic substitution,
-    when rewriting a wanted type mentioning 'a'. So we must kick the inert out.
-
-    We have to do this only if the inert *cannot* rewrite the work item;
-    it it can, then the work item will have been fully rewritten by the
-    inert set during canonicalisation.  So for example:
-         Work item: [W] a ~ Int
-         Inert:     [W] b ~ [a]
-    No need to kick out the inert, beause the inert substitution is not
-    necessarily idemopotent.  See Note [Non-idempotent inert substitution]
-    in TcFlatten.
-
-          Work item:  [G] a ~ Int
-          Inert:      [G] b ~ [a]
-See also Note [Detailed InertCans Invariants]

Note [Avoid double unifications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~