[commit: ghc] master: Comments (TcSMonad) (b564731)

[git at git.haskell.org]

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

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

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

commit b5647315f778f3efd2be8a2f5b2aea7535179232
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Dec 2 14:41:12 2015 +0000

    Comments (TcSMonad)


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

b5647315f778f3efd2be8a2f5b2aea7535179232
 compiler/typecheck/TcSMonad.hs | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index bf3f397..4a4d766 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -705,6 +705,9 @@ A generalised substitution S is "inert" iff
   (IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
         that is, each individual binding is "self-stable"
 
+By (IG1) we define S*(f,t) to be the result of exahaustively
+applying S(f,_) to t.
+
 ----------------------------------------------------------------
 Our main invariant:
    the inert CTyEqCans should be an inert generalised substitution
@@ -737,7 +740,8 @@ This is the main theorem!
            or (K2c) not (fw >= fs)
            or (K2d) a not in s
 
-      (K3) If (b -fs-> s) is in S with (fw >= fs), then
+      (K3) See Note [K3: completeness of solving]
+           If (b -fs-> s) is in S with (fw >= fs), then
         (K3a) If the role of fs is nominal: s /= a
         (K3b) If the role of fs is representational: EITHER
                 a not in s, OR
@@ -818,9 +822,9 @@ Key lemma to make it watertight.
 
 Also, consider roles more carefully. See Note [Flavours with roles].
 
-Completeness
-~~~~~~~~~~~~~
-K3: completeness.  (K3) is not necessary for the extended substitution
+Note [K3: completeness of solving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(K3) is not necessary for the extended substitution
 to be inert.  In fact K1 could be made stronger by saying
    ... then (not (fw >= fs) or not (fs >= fs))
 But it's not enough for S to be inert; we also want completeness.