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

Improve comments about TcLevel invariants

parent 24e56ebd
......@@ -2391,7 +2391,9 @@ Yuk!
-}
data Implication
= Implic {
= Implic { -- Invariants for a tree of implications:
-- see TcType Note [TcLevel and untouchable type variables]
ic_tclvl :: TcLevel, -- TcLevel of unification variables
-- allocated /inside/ this implication
......@@ -2410,7 +2412,8 @@ data Implication
-- for the implication, and hence for all the
-- given evidence variables
ic_wanted :: WantedConstraints, -- The wanted
ic_wanted :: WantedConstraints, -- The wanteds
-- See Invariang (WantedInf) in TcType
ic_binds :: EvBindsVar, -- Points to the place to fill in the
-- abstraction and bindings.
......
......@@ -1910,7 +1910,7 @@ allow the implication to make progress.
promoteTyVar :: TcLevel -> TcTyVar -> TcM Bool
-- When we float a constraint out of an implication we must restore
-- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
-- Return True <=> we did some promotion
-- See Note [Promoting unification variables]
promoteTyVar tclvl tv
......@@ -1924,7 +1924,7 @@ promoteTyVar tclvl tv
promoteTyVarTcS :: TcLevel -> TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
-- invariant (MetaTvInv) in Note [TcLevel and untouchable type variables] in TcType
-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
-- See Note [Promoting unification variables]
-- We don't just call promoteTyVar because we want to use unifyTyVar,
-- not writeMetaTyVar
......@@ -2067,7 +2067,7 @@ When we are inferring a type, we simplify the constraint, and then use
approximateWC to produce a list of candidate constraints. Then we MUST
a) Promote any meta-tyvars that have been floated out by
approximateWC, to restore invariant (MetaTvInv) described in
approximateWC, to restore invariant (WantedInv) described in
Note [TcLevel and untouchable type variables] in TcType.
b) Default the kind of any meta-tyvars that are not mentioned in
......@@ -2084,8 +2084,8 @@ Note [Promoting unification variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we float an equality out of an implication we must "promote" free
unification variables of the equality, in order to maintain Invariant
(MetaTvInv) from Note [TcLevel and untouchable type variables] in TcType. for the
leftover implication.
(WantedInv) from Note [TcLevel and untouchable type variables] in
TcType. for the leftover implication.
This is absolutely necessary. Consider the following example. We start
with two implications and a class with a functional dependency.
......
......@@ -680,25 +680,36 @@ Note [TcLevel and untouchable type variables]
* INVARIANTS. In a tree of Implications,
(ImplicInv) The level number of an Implication is
(ImplicInv) The level number (ic_tclvl) of an Implication is
STRICTLY GREATER THAN that of its parent
(MetaTvInv) The level number of a unification variable is
LESS THAN OR EQUAL TO that of its parent
implication
(GivenInv) The level number of a unification variable appearing
in the 'ic_given' of an implication I should be
STRICTLY LESS THAN the ic_tclvl of I
(WantedInv) The level number of a unification variable appearing
in the 'ic_wanted' of an implication I should be
LESS THAN OR EQUAL TO the ic_tclvl of I
See Note [WantedInv]
* A unification variable is *touchable* if its level number
is EQUAL TO that of its immediate parent implication.
* INVARIANT
(GivenInv) The free variables of the ic_given of an
implication are all untouchable; ie their level
numbers are LESS THAN the ic_tclvl of the implication
Note [WantedInv]
~~~~~~~~~~~~~~~~
Why is WantedInv important? Consider this implication, where
the constraint (C alpha[3]) disobeys WantedInv:
forall[2] a. blah => (C alpha[3])
(forall[3] b. alpha[3] ~ b)
We can unify alpha:=b in the inner implication, because 'alpha' is
touchable; but then 'b' has excaped its scope into the outer implication.
Note [Skolem escape prevention]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only unify touchable unification variables. Because of
(MetaTvInv), there can be no occurrences of the variable further out,
(WantedInv), there can be no occurrences of the variable further out,
so the unification can't cause the skolems to escape. Example:
data T = forall a. MkT a (a->Int)
f x (MkT v f) = length [v,x]
......@@ -770,7 +781,7 @@ sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
-- So <= would be equivalent
checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
-- Checks (MetaTvInv) from Note [TcLevel and untouchable type variables]
-- Checks (WantedInv) from Note [TcLevel and untouchable type variables]
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
= ctxt_tclvl >= tv_tclvl
......
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