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.

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 031fd61..869f276 100644 (file)
--- 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 4b3492b..d0495d7 100644 (file)
--- 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 (file)
--- 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)