[commit: ghc] ghc-8.2: Comment coercion flattening [skip ci] (db0111c)

[git at git.haskell.org]

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

On branch  : ghc-8.2
Link       : http://ghc.haskell.org/trac/ghc/changeset/db0111cd458ed59c439456a6ce1e7c5f8d52fe33/ghc

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

commit db0111cd458ed59c439456a6ce1e7c5f8d52fe33
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Fri Mar 3 14:23:24 2017 -0500

    Comment coercion flattening [skip ci]
    
    (cherry picked from commit 4dc993008a66d6a54909da462363a25e8449f000)


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

db0111cd458ed59c439456a6ce1e7c5f8d52fe33
 compiler/typecheck/TcFlatten.hs | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 700412b..933bacc 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -951,7 +951,7 @@ flatten_one (CastTy ty g)
 flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
 
 -- | "Flatten" a coercion. Really, just flatten the types that it coerces
--- between and then use transitivity.
+-- between and then use transitivity. See Note [Flattening coercions]
 flatten_co :: Coercion -> FlatM (Coercion, Coercion)
 flatten_co co
   = do { let (Pair ty1 ty2, role) = coercionKindRole co
@@ -980,6 +980,31 @@ flatten_ty_con_app tc tys
        ; return (mkTyConApp tc xis, mkTyConAppCo role tc cos) }
 
 {-
+Note [Flattening coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Because a flattened type has a flattened kind, we also must "flatten"
+coercions as we walk through a type. Otherwise, the "from" type of
+the coercion might not match the (now flattened) kind of the type
+that it's casting. flatten_co does the work, taking a coercion of
+type (ty1 ~ ty2) and flattening it to have type (fty1 ~ fty2),
+where flatten(ty1) = fty1 and flatten(ty2) = fty2.
+
+In other words:
+
+  If  r1 is a role
+      co :: s ~r1 t
+      flatten_co co = (fco, kco)
+      r2 is the role in the FlatM
+
+  then
+      fco :: fs ~r1 ft
+      fs, ft are flattened types
+      kco :: (fs ~r1 ft) ~r2 (s ~r1 t)
+
+The second return value of flatten_co is always a ProofIrrelCo. As
+such, it doesn't contain any information the caller doesn't have and
+might not be necessary in whatever comes next.
+
 Note [Flattening synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 Not expanding synonyms aggressively improves error messages, and