Commit 6d404707 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments only

parent c5a39389
......@@ -925,6 +925,9 @@ In effect they become Givens, implemented via the side-effected substitution.
Note [An alternative story for the inert substitution]
(This entire note is just background, left here in case we ever want
to return the the previousl state of affairs)
We used (GHC 7.8) to have this story for the inert substitution inert_eqs
* 'a' is not in fvs(ty)
......@@ -1012,8 +1015,8 @@ Note [eqCanRewrite]
tv ~ ty) can be used to rewrite ct2.
The EqCanRewrite Property:
* For any a,b in {G,W,D} if a canRewrite b
then a canRewrite a
* 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]
......@@ -328,34 +328,8 @@ The InertCans represents a collection of constraints with the following properti
to the CTyEqCan equalities (modulo canRewrite of course;
eg a wanted cannot rewrite a given)
* CTyEqCan equalities _do_not_ form an idempotent substitution, but
they are guaranteed to not have any occurs errors. Additional notes:
- The lack of idempotence of the inert substitution implies
that we must make sure that when we rewrite a constraint we
apply the substitution /recursively/ to the types
involved. Currently the one AND ONLY way in the whole
constraint solver that we rewrite types and constraints wrt
to the inert substitution is TcFlatten/flattenTyVar.
- In the past we did try to have the inert substitution as
idempotent as possible but this would only be true for
constraints of the same flavor, so in total the inert
substitution could not be idempotent, due to flavor-related
issued. Note [Non-idempotent inert substitution] in TcFlatten
explains what is going on.
- Whenever a constraint ends up in the worklist we do
recursively apply exhaustively the inert substitution to it
to check for occurs errors. But if an equality is already in
the inert set and we can guarantee that adding a new equality
will not cause the first equality to have an occurs check
then we do not rewrite the inert equality. This happens in
TcInteract, rewriteInertEqsFromInertEq.
See Note [Delicate equality kick-out] to see which inert
equalities can safely stay in the inert set and which must be
kicked out to be rewritten and re-checked for occurs errors.
* CTyEqCan equalities: see Note [Applying the inert substitution]
in TcFlatten
Note [Type family equations]
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment