From 3afdf90d0f9fb18f13a6b76fe41e5fc60bbdaac3 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Thu, 26 May 2011 17:19:18 +0100
Subject: [PATCH] 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 |   15 ++++++++++++++-
 compiler/prelude/TysPrim.lhs  |   20 ++++++++++++++++++--
 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 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
@@ -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
--- 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)
-- 
1.7.10.4