[commit: ghc] ghc-new-flavor: Commentary, following the relaxation of idempotence of the inert substitution. (f9da524)

[dimitris at microsoft.com]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : ghc-new-flavor

http://hackage.haskell.org/trac/ghc/changeset/f9da5244ecbdbc87bf52a5aace0d245702c783f7

>---------------------------------------------------------------

commit f9da5244ecbdbc87bf52a5aace0d245702c783f7
Author: Dimitrios.Vytiniotis <dimitris at microsoft.com>
Date:   Tue Apr 3 10:48:47 2012 +0100

    Commentary, following the relaxation of idempotence of the inert substitution.

>---------------------------------------------------------------

 compiler/typecheck/TcCanonical.lhs |    5 +++--
 compiler/typecheck/TcInteract.lhs  |    5 +++--
 compiler/typecheck/TcSMonad.lhs    |   34 ++++++++++++++++++++++++++++++----
 3 files changed, 36 insertions(+), 8 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index b94c768..3ea27b2 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -682,8 +682,9 @@ flattenTyVar d ctxt tv
                   ; let ty = mkTyVarTy (setVarType tv new_knd)
                   ; return (ty, mkTcReflCo ty) }
            -- NB recursive call. 
-           -- Why? See Note [Non-idempotent inert substitution]
-           -- Actually, I think applying the substition just twice will suffice
+           -- Why? Because inert subst. non-idempotent, Note [Detailed InertCans Invariants]
+           -- In fact, because of flavors, it couldn't possibly be idempotent,
+           -- this is explained in Note [Non-idempotent inert substitution]
            Just (co,ty) -> 
                do { (ty_final,co') <- flatten d ctxt ty
                   ; return (ty_final, co' `mkTcTransCo` mkTcSymCo co) } }  
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 879a8f4..7dfc75e 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -319,7 +319,7 @@ rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitut
 rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
 -- The goal: traverse the inert equalities and throw some of them back to the worklist
 -- if you have to rewrite and recheck them for occurs check errors. 
--- This is delicate, see Note [Delicate equality kick-out]
+-- To see which ones we must throw out see Note [Delicate equality kick-out]
  = do { mieqs <- Traversable.mapM do_one ieqs 
       ; traceTcS "Original inert equalities:" (ppr ieqs)
       ; let flatten_justs elem venv
@@ -334,7 +334,8 @@ rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs
          = if fl `canRewrite` subst_fl then
                -- If also the inert can rewrite the subst then there is no danger of 
                -- occurs check errors sor keep it there. No need to rewrite the inert equality
-               -- (as we did in the past): See Note [Non-idempotent inert substitution]
+               -- (as we did in the past) because of point (8) of 
+               -- Note [Detailed InertCans Invariants] and 
              return (Just ct)
              -- used to be: rewrite_on_the_spot ct >>= ( return . Just )
            else -- We have to throw inert back to worklist for occurs checks 
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 4291fd8..01b8488 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -433,10 +433,36 @@ The InertCans represents a collection of constraints with the following properti
   2 All Given or Wanted or Derived. No (partially) Solved
   3 No two dictionaries with the same head
   4 No two family equations with the same head
-  5 Family equations inert with top-level
-  6 Dictionaries have no matching instance at top level
-  7 Constraints are fully rewritten with respect to the equality constraints (CTyEqCan)
-  8 Equalities form an idempotent substitution (taking flavors into consideration)
+      NB: This is enforced by construction since we use a CtFamHeadMap for inert_funeqs
+  5 Family equations inert wrt top-level family axioms
+  6 Dictionaries have no matching top-level instance 
+  
+  7 Non-equality constraints are fully rewritten with respect to the equalities (CTyEqCan)
+
+  8 Equalities _do_not_ form an idempotent substitution but they are guarranteed 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 
+         TcCanonical/flattenTyVar.
+
+       - In the past we did try to have the inert substituion 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] 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. 
+
   9 Given family or dictionary constraints don't mention touchable unification variables
 \begin{code}