From 20f50b2a3651ce7dacdcb86a83afb5c5d444cb0b Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Thu, 7 Feb 2002 12:51:35 +0000
Subject: [PATCH] [project @ 2002-02-07 12:51:34 by simonpj]
 ---------------------------------------------------- 	Make
 TcType.match and TcUnify.uUnboundVar kind-aware 
 ----------------------------------------------------

George Russel had apparently-overlapping (ha) instance decls like

	instance .. => C (a b) where
	instance .. => C (x y) where

But the a,b and x,y were different kinds!  Turned out that TcType.unify
was kind-aware (so we didn't report a duplicate instance decl, but TcType.match
was not (so we simply selected the wrong one, and got a mis-kinded constraint
popping up from the ".."  part.  Very exciting to track down.

I also make the ordinary unification kind-aware in the same way.  It's
quite legitimate to attempt to unify, say,
	(a b)    with     (c d)
but the unification should fail if a's kind differs from c's.
(There was a kind of debug warning before, but it's actually not an error
in the compiler... so it should just make unification fail gracefully.)
---
 ghc/compiler/typecheck/TcType.lhs  |   10 +++++++++-
 ghc/compiler/typecheck/TcUnify.lhs |   17 ++++++++---------
 ghc/compiler/types/Type.lhs        |   21 +++++++++++++--------
 3 files changed, 30 insertions(+), 18 deletions(-)

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 5db0ad7..ee7a060 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -1087,7 +1087,15 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-	Nothing -> k (extendSubstEnv senv v (DoneTy ty))
+	Nothing | typeKind ty `eqKind` tyVarKind v	
+			-- We do a kind check, just as in the uVarX above
+			-- The kind check is needed to avoid bogus matches
+			-- of 	(a b) with (c d), where the kinds don't match
+			-- An occur check isn't needed when matching.
+		-> k (extendSubstEnv senv v (DoneTy ty))
+
+		| otherwise  -> Nothing -- Fails
+
 	Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
 			   | otherwise	         -> Nothing  -- Fails
 
diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index 6b74930..8ee07bc 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -637,19 +637,18 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 
 checkKinds swapped tv1 ty2
 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- ty2 has been zonked at this stage
+-- ty2 has been zonked at this stage.
 
-  | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
-	-- Check that we don't unify a lifted type variable with an
-	-- unlifted type: e.g.  (id 3#) is illegal
+  | tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
+
+  | otherwise
+	-- Either the kinds aren't compatible
+	--	(can happen if we unify (a b) with (c d))
+	-- or we are unifying a lifted type variable with an
+	-- 	unlifted type: e.g.  (id 3#) is illegal
   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
     unifyMisMatch k1 k2
 
-  | otherwise
-  =	-- Check that we aren't losing boxity info (shouldn't happen)
-    WARN (not (tk2 `hasMoreBoxityInfo` tk1),
-	  (ppr tv1 <+> ppr tk1) $$ (ppr ty2 <+> ppr tk2))
-    returnTc ()
   where
     (k1,k2) | swapped   = (tk2,tk1)
 	    | otherwise = (tk1,tk2)
diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs
index f901d91..9a67311 100644
--- a/ghc/compiler/types/Type.lhs
+++ b/ghc/compiler/types/Type.lhs
@@ -119,20 +119,25 @@ import UniqSet		( sizeUniqSet )		-- Should come via VarSet
 
 \begin{code}
 hasMoreBoxityInfo :: Kind -> Kind -> Bool
+-- (k1 `hasMoreBoxityInfo` k2) checks that k1 <: k2
 hasMoreBoxityInfo k1 k2
-  | k2 `eqKind` openTypeKind = True
-  | otherwise	  	     = k1 `eqType` k2
+  | k2 `eqKind` openTypeKind = ok k1
+  | otherwise	  	     = k1 `eqKind` k2
+  where
+    ok (TyConApp tc _) = tc == typeCon || tc == openKindCon
+    ok (NoteTy _ k)    = ok k
+    ok other	       = False
+
+isTypeKind :: Kind -> Bool
+-- True of kind * and *#
+isTypeKind (TyConApp tc _) = tc == typeCon
+isTypeKind (NoteTy _ k)    = isTypeKind k
+isTypeKind other	   = False
 
 defaultKind :: Kind -> Kind
 -- Used when generalising: default kind '?' to '*'
 defaultKind kind | kind `eqKind` openTypeKind = liftedTypeKind
 	         | otherwise	 	      = kind
-
-isTypeKind :: Kind -> Bool
--- True of kind * and *#
-isTypeKind k = case splitTyConApp_maybe k of
-		 Just (tc,[k]) -> tc == typeCon
-		 other	       -> False
 \end{code}
 
 
-- 
1.7.10.4