[commit: ghc] master: Improve comments about TcLevel invariants (a3cde5f)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/a3cde5fd76b0e519f27267079e4ea89516ffdc04/ghc

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

commit a3cde5fd76b0e519f27267079e4ea89516ffdc04
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Jan 22 14:49:46 2018 +0000

    Improve comments about TcLevel invariants


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

a3cde5fd76b0e519f27267079e4ea89516ffdc04
 compiler/typecheck/TcRnTypes.hs  |  7 +++++--
 compiler/typecheck/TcSimplify.hs | 10 +++++-----
 compiler/typecheck/TcType.hs     | 31 +++++++++++++++++++++----------
 3 files changed, 31 insertions(+), 17 deletions(-)

diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 5e97935..00927d7 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 70c8f96..62a4800 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 441545c..de37aa8 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