[commit: ghc] tc-untouchables: Be careful about kinds when eta-expanding AppCo (19dd108)

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : tc-untouchables

http://hackage.haskell.org/trac/ghc/changeset/19dd108cd15ab3d0cc538903217eef9be54a02e5

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

commit 19dd108cd15ab3d0cc538903217eef9be54a02e5
Author: Simon Peyton Jones <[email protected]>
Date:   Tue Sep 18 17:32:42 2012 +0100

    Be careful about kinds when eta-expanding AppCo
    
    See Note [Eta for AppCo] in OptCoercion

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

 compiler/types/OptCoercion.lhs |   27 +++++++++++++++++++++++++--
 1 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index c699163..a039fe5 100644
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -391,8 +391,9 @@ etaAppCo_maybe co
   | Just (co1,co2) <- splitAppCo_maybe co
   = Just (co1,co2)
   | Pair ty1 ty2 <- coercionKind co
-  , Just {} <- splitAppTy_maybe ty1
-  , Just {} <- splitAppTy_maybe ty2
+  , Just (_,t1) <- splitAppTy_maybe ty1
+  , Just (_,t2) <- splitAppTy_maybe ty2
+  , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
   = Just (LRCo CLeft co, LRCo CRight co)
   | otherwise
   = Nothing
@@ -421,3 +422,25 @@ etaTyConAppCo_maybe tc co
   | otherwise
   = Nothing
 \end{code}  
+
+Note [Eta for AppCo]
+~~~~~~~~~~~~~~~~~~~~
+Supopse we have 
+   g :: s1 t1 ~ s2 t2
+
+Then we can't necessarily make
+   left  g :: s1 ~ s2
+   right g :: t1 ~ t2
+becuase it's poossible that
+   s1 :: * -> *         t1 :: *
+   s2 :: (*->*) -> *    t2 :: * -> *
+and in that case (left g) does not have the same
+kind on either side.
+
+It's enough to check that 
+  kind t1 = kind t2
+because if g is well-kinded then
+  kind (s1 t2) = kind (s2 t2)
+and these two imply
+  kind s1 = kind s2
+