Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master
http://hackage.haskell.org/trac/ghc/changeset/3afdf90d0f9fb18f13a6b76fe41e5fc60bbdaac3 >--------------------------------------------------------------- commit 3afdf90d0f9fb18f13a6b76fe41e5fc60bbdaac3 Author: Simon Peyton Jones <[email protected]> Date: Thu May 26 17:19:18 2011 +0100 Treat the (~) type constructor a bit specially when kind-checking in Core Lint. It's unusual becuase it is poly-kinded; for example (~) Int a and (~) Maybe b are both ok. We don't want the full generality of kind polymorphism (yet anyway) so these changes in effect give (~) its own private kinding rule. It won't work right if (~) appears un-saturated, and Lint now checks for that too. >--------------------------------------------------------------- compiler/coreSyn/CoreLint.lhs | 13 +++++++++++++ compiler/prelude/TysPrim.lhs | 20 ++++++++++++++++++-- compiler/types/Kind.lhs | 7 +++++-- 3 files changed, 36 insertions(+), 4 deletions(-) diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index 031fd61..869f276 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -717,6 +717,8 @@ lintType ty@(FunTy t1 t2) = lint_ty_app ty (tyConKind funTyCon) [t1,t2] lintType ty@(TyConApp tc tys) + | tc `hasKey` eqPredPrimTyConKey -- See Note [The (~) TyCon] in TysPrim + = lint_eq_pred ty tys | tyConHasKind tc = lint_ty_app ty (tyConKind tc) tys | otherwise @@ -746,6 +748,17 @@ lint_ty_app ty k tys = do { ks <- mapM lintType tys ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks } +lint_eq_pred :: Type -> [OutType] -> LintM Kind +lint_eq_pred ty arg_tys + | [ty1,ty2] <- arg_tys + = do { k1 <- lintType ty1 + ; k2 <- lintType ty2 + ; checkL (k1 `eqKind` k2) + (ptext (sLit "Mismatched arg kinds:") <+> ppr ty) + ; return unliftedTypeKind } + | otherwise + = failWithL (ptext (sLit "Unsaturated (~) type") <+> ppr ty) + ---------------- check_co_app :: Coercion -> Kind -> [OutType] -> LintM () check_co_app ty k tys diff --git a/compiler/prelude/TysPrim.lhs b/compiler/prelude/TysPrim.lhs index 4b3492b..d0495d7 100644 --- a/compiler/prelude/TysPrim.lhs +++ b/compiler/prelude/TysPrim.lhs @@ -379,6 +379,22 @@ doublePrimTyCon = pcPrimTyCon0 doublePrimTyConName DoubleRep %* * %************************************************************************ +Note [The (~) TyCon) +~~~~~~~~~~~~~~~~~~~~ +There is a perfectly ordinary type constructor (~) that represents the type +of coercions (which, remember, are values). For example + Refl Int :: Int ~ Int + +Atcually it is not quite "perfectly ordinary" because it is kind-polymorphic: + Refl Maybe :: Maybe ~ Maybe + +So the true kind of (~) :: forall k. k -> k -> #. But we don't have +polymorphic kinds (yet). However, (~) really only appears saturated in +which case there is no problem in finding the kind of (ty1 ~ ty2). So +we check that in CoreLint (and, in an assertion, in Kind.typeKind). + +Note [The State# TyCon] +~~~~~~~~~~~~~~~~~~~~~~~ State# is the primitive, unlifted type of states. It has one type parameter, thus State# RealWorld @@ -392,10 +408,11 @@ keep different state threads separate. It is represented by nothing at all. mkStatePrimTy :: Type -> Type mkStatePrimTy ty = mkTyConApp statePrimTyCon [ty] -statePrimTyCon :: TyCon +statePrimTyCon :: TyCon -- See Note [The State# TyCon] statePrimTyCon = pcPrimTyCon statePrimTyConName 1 VoidRep eqPredPrimTyCon :: TyCon -- The representation type for equality predicates + -- See Note [The (~) TyCon] eqPredPrimTyCon = pcPrimTyCon eqPredPrimTyConName 2 VoidRep \end{code} @@ -415,7 +432,6 @@ realWorldStatePrimTy = mkStatePrimTy realWorldTy -- State# RealWorld Note: the ``state-pairing'' types are not truly primitive, so they are defined in \tr{TysWiredIn.lhs}, not here. - %************************************************************************ %* * \subsection[TysPrim-arrays]{The primitive array types} diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 23787d2..0594f7f 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -72,8 +72,11 @@ isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey \begin{code} typeKind :: Type -> Kind -typeKind (TyConApp tc tys) - = kindAppResult (tyConKind tc) tys +typeKind _ty@(TyConApp tc tys) + = ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty ) + -- Assertion checks for unsaturated application of (~) + -- See Note [The (~) TyCon] in TysPrim + kindAppResult (tyConKind tc) tys typeKind (PredTy pred) = predKind pred typeKind (AppTy fun _) = kindFunResult (typeKind fun) _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
