[commit: ghc] master: Clarify Note [Kind coercions in Unify] (9f73e46)

[git at git.haskell.org]

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

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

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

commit 9f73e46c0f34b8b5e8318e6b488b7dade7db68e3
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date:   Fri Mar 25 17:25:25 2016 -0400

    Clarify Note [Kind coercions in Unify]


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

9f73e46c0f34b8b5e8318e6b488b7dade7db68e3
 compiler/types/Unify.hs | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index ed4b224..0b5df14 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -79,10 +79,31 @@ may look nothing alike.
 
 So, we pass a kind coercion to the match/unify worker. This coercion witnesses
 the equality between the substed kind of the left-hand type and the substed
-kind of the right-hand type. To get this coercion, we first have to match/unify
+kind of the right-hand type. Note that we do not unify kinds at the leaves
+(as we did previously). We thus have
+
+INVARIANT: In the call
+    unify_ty ty1 ty2 kco
+it must be that subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2)), where
+`subst` is the ambient substitution in the UM monad.
+
+To get this coercion, we first have to match/unify
 the kinds before looking at the types. Happily, we need look only one level
 up, as all kinds are guaranteed to have kind *.
 
+When we're working with type applications (either TyConApp or AppTy) we
+need to worry about establishing INVARIANT, as the kinds of the function
+& arguments aren't (necessarily) included in the kind of the result.
+When unifying two TyConApps, this is easy, because the two TyCons are
+the same. Their kinds are thus the same. As long as we unify left-to-right,
+we'll be sure to unify types' kinds before the types themselves. (For example,
+think about Proxy :: forall k. k -> *. Unifying the first args matches up
+the kinds of the second args.)
+
+For AppTy, we must unify the kinds of the functions, but once these are
+unified, we can continue unifying arguments without worrying further about
+kinds.
+
 We thought, at one point, that this was all unnecessary: why should casts
 be in types in the first place? But they do. In
 dependent/should_compile/KindEqualities2, we see, for example
@@ -760,6 +781,7 @@ unify_ty_app ty1 ty1args ty2 ty2args
   | otherwise
   = do { let ki1 = typeKind ty1
              ki2 = typeKind ty2
+           -- See Note [Kind coercions in Unify]
        ; unify_ty ki1 ki2 (mkNomReflCo liftedTypeKind)
        ; unify_ty ty1 ty2 (mkNomReflCo ki1)
        ; unify_tys ty1args ty2args }
@@ -770,6 +792,7 @@ unify_tys orig_xs orig_ys
   where
     go []     []     = return ()
     go (x:xs) (y:ys)
+      -- See Note [Kind coercions in Unify]
       = do { unify_ty x y (mkNomReflCo $ typeKind x)
            ; go xs ys }
     go _ _ = maybeApart  -- See Note [Lists of different lengths are MaybeApart]