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 <g...@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 _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
