[commit: ghc] master: Comments (only) in TcFlatten (2d6d907)

[git at git.haskell.org]

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

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

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

commit 2d6d907d8dcc051a7656dafcc0bc827cc651c6c0
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Mon Mar 21 17:03:38 2016 -0400

    Comments (only) in TcFlatten


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

2d6d907d8dcc051a7656dafcc0bc827cc651c6c0
 compiler/typecheck/TcFlatten.hs | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 4971eb1..89e663f 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -797,19 +797,26 @@ flattenManyNom ev tys
 
 {- Note [Flattening]
 ~~~~~~~~~~~~~~~~~~~~
-  flatten ty  ==>   (xi, cc)
+  flatten ty  ==>   (xi, co)
     where
       xi has no type functions, unless they appear under ForAlls
-
-      cc = Auxiliary given (equality) constraints constraining
-           the fresh type variables in xi.  Evidence for these
-           is always the identity coercion, because internally the
-           fresh flattening skolem variables are actually identified
-           with the types they have been generated to stand in for.
+      co :: xi ~ ty
 
 Note that it is flatten's job to flatten *every type function it sees*.
 flatten is only called on *arguments* to type functions, by canEqGiven.
 
+Flattening also:
+  * zonks, removing any metavariables, and
+  * applies the substitution embodied in the inert set
+
+Because flattening zonks and the returned coercion ("co" above) is also
+zonked, it's possible that (co :: xi ~ ty) isn't quite true, as ty (the
+input to the flattener) might not be zonked. After zonking everything,
+(co :: xi ~ ty) will be true, however. It is for this reason that we
+occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
+even before we zonk the whole program. (In particular, this is why the
+zonk in flatten_tyvar3 is necessary.)
+
 Flattening a type also means flattening its kind. In the case of a type
 variable whose kind mentions a type family, this might mean that the result
 of flattening has a cast in it.
@@ -1349,6 +1356,7 @@ flatten_tyvar3 tv
              -- This zonk is necessary because we might later see the tv's kind
              -- in canEqTyVarTyVar (where we use getCastedTyVar_maybe).
              -- If you remove it, then e.g. dependent/should_fail/T11407 panics
+             -- See also Note [Flattening]
        ; return (FTRCasted (setTyVarKind tv orig_kind) kind_co) }
 
 {-