Commit a225c70e authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments only: move flattening notes to TcFlatten

parent fca85c9b
......@@ -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,
contradicting (L1), or fw>=fs contradicting K2b.
- (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.
......@@ -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,
contradicting (L1), or fw>=fs contradicting K2b.
- (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.
......
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
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