Commit f9da5244 authored by dimitris's avatar dimitris

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

parent 5802ebdd
......@@ -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) } }
......
......@@ -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
......
......@@ -432,11 +432,37 @@ The InertCans represents a collection of constraints with the following properti
1 All canonical
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)
4 No two family equations with the same head
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}
......
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