Commit 3afdf90d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent 80f5e700
......@@ -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
......@@ -745,7 +747,18 @@ lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
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
......
......@@ -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}
......
......@@ -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)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment