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 <[email protected]> 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} _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
