Improve comments about TcLevel invariants

3 files changed, 31 insertions, 17 deletions

diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 5e97935f55..00927d7374 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -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.
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 70c8f96d90..62a4800373 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -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.
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 441545ce24..de37aa862d 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -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