Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : ghc-kinds
http://hackage.haskell.org/trac/ghc/changeset/d51c28d02777dee753552a16ba355493877fdb05 >--------------------------------------------------------------- commit d51c28d02777dee753552a16ba355493877fdb05 Author: Julien Cretin <g...@ia0.eu> Date: Wed Sep 14 20:02:30 2011 +0200 kind coercions >--------------------------------------------------------------- compiler/basicTypes/Var.lhs | 5 ++- compiler/coreSyn/CoreLint.lhs | 64 ++++++++++++++++++++++++++++++++------- compiler/typecheck/TcMType.lhs | 10 +++--- compiler/types/Kind.lhs | 7 ++++ 4 files changed, 68 insertions(+), 18 deletions(-) diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index 232c4d3..b026728 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -59,7 +59,7 @@ module Var ( tyVarName, tyVarKind, tcTyVarDetails, setTcTyVarDetails, -- ** Modifying 'TyVar's - setTyVarName, setTyVarUnique, setTyVarKind + setTyVarName, setTyVarUnique, setTyVarKind, updateTyVarKind ) where @@ -268,6 +268,9 @@ setTyVarName = setVarName setTyVarKind :: TyVar -> Kind -> TyVar setTyVarKind tv k = tv {varType = k} + +updateTyVarKind :: (Kind -> Kind) -> TyVar -> TyVar +updateTyVarKind update tv = tv {varType = update (tyVarKind tv)} \end{code} \begin{code} diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index e44b9b1..5e2fede 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -356,6 +356,27 @@ lintCoreExpr (Coercion co) ; return (mkCoercionType ty1 ty2) } \end{code} +Note [Kind instantiation in coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Consider the following coercion axiom: + ax_co [(k_ag :: BOX), (f_aa :: k_ag -> Constraint)] :: T k_ag f_aa ~ f_aa + +Consider the following instantiation: + ax_co <(* -> * :: BOX)> <Monad> + +We need to split the co_ax_tvs into kind and type variables in order +to find out the coercion kind instantiations. Those can only be Refl +since we don't have kind coercions. This is just a way to represent +kind instantiation. + +We use the number of kind variables to know how to split the coercions +instantiations between kind coercions and type coercions. We lint the +kind coercions and produce the following substitution which is to be +applied in the type variables: + k_ag |-> * -> * + + %************************************************************************ %* * \subsection[lintCoreArgs]{lintCoreArgs} @@ -447,6 +468,16 @@ checkTyCoKind tv co checkTyCoKinds :: [TyVar] -> [OutCoercion] -> LintM [(OutType, OutType)] checkTyCoKinds = zipWithM checkTyCoKind +checkKiCoKind :: KindVar -> OutCoercion -> LintM Kind +-- see lintCoercion (AxiomInstCo {}) and Note [Kind instantiation in coercions] +checkKiCoKind kv co + = do { ki <- lintKindCoercion co + ; unless (isSuperKind (tyVarKind kv)) (addErrL (mkTyCoAppErrMsg kv co)) + ; return ki } + +checkKiCoKinds :: [KindVar] -> [OutCoercion] -> LintM [Kind] +checkKiCoKinds = zipWithM checkKiCoKind + checkDeadIdOcc :: Id -> LintM () -- Occurrences of an Id should never be dead.... -- except when we are checking a case pattern @@ -634,6 +665,8 @@ lintKind (FunTy k1 k2) = lintKind k1 >> lintKind k2 lintKind kind@(TyConApp tc kis) + | isSuperKind kind = panic "lintKind called with BOX" + | isSuperKind tc_kind -- handles *, #, Constraint, etc. , null kis = return () @@ -660,6 +693,13 @@ lintTyBndrKind tv = else lintKind ki ------------------- +lintKindCoercion :: Coercion -> LintM Kind +lintKindCoercion (Refl k) + = do { k' <- applySubstTy k + ; lintKind k' + ; return k' } +lintKindCoercion _ = panic "lintKindCoercion" + lintCoercion :: OutCoercion -> LintM (OutType, OutType) -- Check the kind of a coercion term, returning the kind lintCoercion (Refl ty) @@ -675,13 +715,6 @@ lintCoercion co@(TyConAppCo tc cos) ; (ss,ts) <- mapAndUnzipM lintCoercion cotys ; check_co_app co ki (kis ++ ss) ; return (mkTyConApp tc (kis ++ ss), mkTyConApp tc (kis ++ ts)) } - where - lintKindCoercion :: Coercion -> LintM Kind - lintKindCoercion (Refl k) = do - k' <- applySubstTy k - lintKind k' - return k' - lintKindCoercion _ = panic "lintCoercion lintKindCoercion" lintCoercion co@(AppCo co1 co2) = do { (s1,t1) <- lintCoercion co1 @@ -690,7 +723,8 @@ lintCoercion co@(AppCo co1 co2) ; return (mkAppTy s1 s2, mkAppTy t1 t2) } lintCoercion (ForAllCo v co) - = do { lintKind (tyVarKind v) + = do { let kind = tyVarKind v + ; unless (isSuperKind kind) (lintKind kind) ; (s,t) <- addInScopeVar v (lintCoercion co) ; return (ForAllTy v s, ForAllTy v t) } @@ -702,13 +736,19 @@ lintCoercion (CoVarCo cv) = do { checkTyCoVarInScope cv ; return (coVarKind cv) } -lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs +lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = ktvs , co_ax_lhs = lhs , co_ax_rhs = rhs }) cos) - = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos) - ; return (substTyWith tvs tys1 lhs, - substTyWith tvs tys2 rhs) } + = do { kis <- checkKiCoKinds kvs kcos + ; let tvs' = map (updateTyVarKind (Type.substTy subst)) tvs + subst = zipOpenTvSubst kvs kis + ; (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs' tcos) + ; return (substTyWith ktvs (kis ++ tys1) lhs, + substTyWith ktvs (kis ++ tys2) rhs) } + where -- see Note [Kind instantiation in coercions] + (kvs, tvs) = splitKiTyVars ktvs + (kcos, tcos) = splitAt (length kvs) cos lintCoercion (UnsafeCo ty1 ty2) = do { ty1' <- lintInTy ty1 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 8bd7ed6..81ff7e0 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -70,7 +70,7 @@ module TcMType ( import TypeRep import TcType import Type -import Kind( isSuperKind ) +import Kind import Class import TyCon import Var @@ -206,7 +206,7 @@ tcSuperSkolTyVars :: [TyVar] -> [TcTyVar] tcSuperSkolTyVars tyvars = kvs' ++ tvs' where - (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars + (kvs, tvs) = splitKiTyVars tyvars kvs' = [ mkTcTyVar (tyVarName kv) (tyVarKind kv) superSkolemTv | kv <- kvs ] tvs' = [ mkTcTyVar (tyVarName tv) (substTy subst (tyVarKind tv)) superSkolemTv @@ -234,14 +234,14 @@ tcInstSkolTyVars tyvars = do { kvs' <- mapM (tcInstSkolTyVar False (mkTopTvSubst [])) kvs ; tvs' <- mapM (tcInstSkolTyVar False (zipTopTvSubst kvs (map mkTyVarTy kvs'))) tvs ; return (kvs' ++ tvs') } - where (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars + where (kvs, tvs) = splitKiTyVars tyvars tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar] tcInstSuperSkolTyVars tyvars = do { kvs' <- mapM (tcInstSkolTyVar True (mkTopTvSubst [])) kvs ; tvs' <- mapM (tcInstSkolTyVar True (zipTopTvSubst kvs (map mkTyVarTy kvs'))) tvs ; return (kvs' ++ tvs') } - where (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars + where (kvs, tvs) = splitKiTyVars tyvars tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type with fresh skolem constants @@ -259,7 +259,7 @@ tcInstSigTyVars tyvars = do { kvs' <- mapM (tcInstSigTyVar (mkTopTvSubst [])) kvs ; tvs' <- mapM (tcInstSigTyVar (zipTopTvSubst kvs (map mkTyVarTy kvs'))) tvs ; return (kvs' ++ tvs') } - where (kvs, tvs) = span (isSuperKind . tyVarKind) tyvars + where (kvs, tvs) = splitKiTyVars tyvars tcInstSigTyVar :: TvSubst -> TyVar -> TcM TcTyVar tcInstSigTyVar subst tyvar diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 2ca79ac..ed99492 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -34,6 +34,9 @@ module Kind ( isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, isSubKindCon, isSubOpenTypeKindCon, + -- ** Functions on variables + splitKiTyVars, + -- ** Promotion related functions promoteType, isPromotableType, isPromotableKind @@ -229,6 +232,10 @@ defaultKind k | isSubArgTypeKind k = liftedTypeKind | otherwise = k +splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar]) +-- Assumes we get [k1, k2, a, b, c], returns ([k1, k2], [a, b, c]) +splitKiTyVars = span (isSuperKind . tyVarKind) + -- About promoting a type to a kind _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
