[commit: ghc] ghc-kinds: kinding rules for partially applied arrow (4659f19)

[Julien Cretin]

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

On branch  : ghc-kinds

http://hackage.haskell.org/trac/ghc/changeset/4659f19976cb0b06c942b92022b3f3965d886c7f

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

commit 4659f19976cb0b06c942b92022b3f3965d886c7f
Author: Julien Cretin <ghc at ia0.eu>
Date:   Wed Sep 21 23:46:56 2011 +0200

    kinding rules for partially applied arrow

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

 compiler/coreSyn/CoreLint.lhs  |    8 ++++++--
 compiler/prelude/TysPrim.lhs   |   16 +++++++++++++++-
 compiler/typecheck/TcUnify.lhs |    7 ++++++-
 3 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 5e2fede..5fc9c5c 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -707,7 +707,11 @@ lintCoercion (Refl ty)
        ; return (ty', ty') }
 
 lintCoercion co@(TyConAppCo tc cos)
-  = do { let ki = tyConKind tc
+  = do { let ki | tc `hasKey` funTyConKey && length cos == 2
+                  = mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind
+                  -- It's a fully applied function, so we must use the
+                  -- most permissive type for the arrow constructor
+                | otherwise = tyConKind tc
              (kvs, _) = splitForAllTys ki
              (cokis, cotys) = splitAt (length kvs) cos
              -- we need to verify that kind instantiations are Refl
@@ -806,7 +810,7 @@ lintType ty@(AppTy t1 t2)
        ; lint_ty_app ty k1 [t2] }
 
 lintType ty@(FunTy t1 t2)
-  = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
+  = lint_ty_app ty (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind) [t1,t2]
 
 lintType ty@(TyConApp tc tys)
   | tc `hasKey` eqPrimTyConKey	-- See Note [The ~# TyCon] in TysPrim
diff --git a/compiler/prelude/TysPrim.lhs b/compiler/prelude/TysPrim.lhs
index 14495bd..aa680e2 100644
--- a/compiler/prelude/TysPrim.lhs
+++ b/compiler/prelude/TysPrim.lhs
@@ -223,7 +223,21 @@ funTyConName :: Name
 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
 
 funTyCon :: TyCon
-funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
+funTyCon = mkFunTyCon funTyConName (mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind)
+-- (->) :: * -> * -> *
+-- but we should have (and want) the following typing rule for fully applied arrows
+--      Gamma |- tau   :: k1    k1 in {*, #}
+--      Gamma |- sigma :: k2    k2 in {*, #, (#)}
+--      -----------------------------------------
+--      Gamma |- tau -> sigma :: *
+-- Currently we have the following rule which achieves more or less the same effect
+--      Gamma |- tau   :: ??
+--      Gamma |- sigma :: ?
+--      --------------------------
+--      Gamma |- tau -> sigma :: *
+-- In the end we don't want subkinding at all.
+
+-- funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
         -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
 	-- But if we do that we get kind errors when saying
 	--	instance Control.Arrow (->)
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 4b39b82..8e4ab0d 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -1156,6 +1156,11 @@ data SubKinding
   | SKEq  -- k1 == k2  -- new
   | SKGe  -- k1 >= k2  -- swapped == False
 
+instance Outputable SubKinding where
+  ppr SKLe = text "<="
+  ppr SKEq = text "=="
+  ppr SKGe = text ">="
+
 invSubKinding :: SubKinding -> SubKinding
 invSubKinding SKLe = SKGe
 invSubKinding SKEq = SKEq
@@ -1270,7 +1275,7 @@ kindSimpleKind orig_sk orig_kind
     go _ k@(TyVarTy _) = return k -- KindVars are always simple
     go _ k@(TyConApp tc _) | not (isSubOpenTypeKindCon tc) = return k  -- Promoted type constructors too
     go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:")
-                                  <+> ppr orig_kind)
+                                  <+> ppr orig_sk <+> ppr orig_kind)
         -- I think this can't actually happen
 
 -- T v = MkT v           v must be a type