diff options
| -rw-r--r-- | compiler/coreSyn/CoreLint.lhs | 15 | ||||
| -rw-r--r-- | compiler/prelude/TysPrim.lhs | 20 | ||||
| -rw-r--r-- | compiler/types/Kind.lhs | 7 |
3 files changed, 37 insertions, 5 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index 031fd613cc..869f276c50 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 @@ -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 diff --git a/compiler/prelude/TysPrim.lhs b/compiler/prelude/TysPrim.lhs index 4b3492b2c0..d0495d7b29 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 23787d20e2..0594f7f53a 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) |