[commit: ghc] master: Comments about TcLevel assignment (3833e71)

[git at git.haskell.org]

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

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

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

commit 3833e71dba10b0a347b5a297a75dcdb6c69d7e72
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Oct 6 12:36:30 2015 +0100

    Comments about TcLevel assignment
    
    Triggered by investigations around Trac 10845


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

3833e71dba10b0a347b5a297a75dcdb6c69d7e72
 compiler/typecheck/TcType.hs | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index e5f49e4..bb937c6 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -433,6 +433,7 @@ data UserTypeCtxt
 
 newtype TcLevel = TcLevel Int deriving( Eq, Ord )
   -- See Note [TcLevel and untouchable type variables] for what this Int is
+  -- See also Note [TcLevel assignment]
 
 {-
 Note [TcLevel and untouchable type variables]
@@ -458,7 +459,6 @@ Note [TcLevel and untouchable type variables]
                 implication are all untouchable; ie their level
                 numbers are LESS THAN the ic_tclvl of the implication
 
-
 Note [Skolem escape prevention]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We only unify touchable unification variables.  Because of
@@ -491,15 +491,35 @@ emerges. If we (wrongly) spontaneously solved it to get uf := beta,
 the whole implication disappears but when we pop out again we are left with
 (F Int ~ uf) which will be unified by our final zonking stage and
 uf will get unified *once more* to (F Int).
+
+Note [TcLevel assignment]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+We arrange the TcLevels like this
+
+   1   Top level
+   2     Flatten-meta-vars of level 3
+   3   First-level implication constraints
+   4     Flatten-meta-vars of level 5
+   5   Second-level implication constraints
+   ...etc...
+
+The even-numbered levels are for the flatten-meta-variables assigned
+at the next level in.  Eg for a second-level implication conststraint
+(level 5), the flatten meta-vars are level 4, which makes them untouchable.
+The flatten meta-vars could equally well all have level 0, or just NotALevel
+since they do not live across implications.
 -}
 
 fmvTcLevel :: TcLevel -> TcLevel
+-- See Note [TcLevel assignment]
 fmvTcLevel (TcLevel n) = TcLevel (n-1)
 
 topTcLevel :: TcLevel
+-- See Note [TcLevel assignment]
 topTcLevel = TcLevel 1   -- 1 = outermost level
 
 pushTcLevel :: TcLevel -> TcLevel
+-- See Note [TcLevel assignment]
 pushTcLevel (TcLevel us) = TcLevel (us + 2)
 
 strictlyDeeperThan :: TcLevel -> TcLevel -> Bool