X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=201df05210c86c0cee24c243bb026b06dc101a02;hb=51a571c0f5b0201ea53bec60fcaafb78c01c017e;hp=e431580a112ab014e43b8124aac51374cb82f83f;hpb=861e836ed0cc1aa45932ecb3470967964440a0ef;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index e431580..201df05 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -17,20 +17,20 @@ module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists,
 -- friends: 
 import TcMonad
 import TypeRep	( Type(..), PredType(..) )  -- friend
-import Type	( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind, 
-		  superBoxity, typeCon, openKindCon, hasMoreBoxityInfo, 
+import Type	( unliftedTypeKind, liftedTypeKind, openTypeKind, 
+		  typeCon, openKindCon, hasMoreBoxityInfo, 
 		  tyVarsOfType, typeKind,
-		  mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
-                  isNotUsgTy, splitAppTy_maybe, mkTyConApp, 
+		  mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
+                  splitAppTy_maybe, mkTyConApp, 
 	   	  tidyOpenType, tidyOpenTypes, tidyTyVar
 		)
 import TyCon	( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
-import Name	( hasBetterProv )
-import Var	( TyVar, tyVarKind, varName, isSigTyVar )
-import VarSet	( varSetElems )
+import Var	( tyVarKind, varName, isSigTyVar )
+import VarSet	( elemVarSet )
 import TcType	( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar,
 		  newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType
 		)
+import Name	( isSystemName )
 
 -- others:
 import BasicTypes ( Arity, Boxity, isBoxed )
@@ -48,12 +48,12 @@ import Outputable
 \begin{code}
 unifyKind :: TcKind		    -- Expected
 	  -> TcKind		    -- Actual
-	  -> TcM s ()
+	  -> TcM ()
 unifyKind k1 k2 
   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
     uTys k1 k1 k2 k2
 
-unifyKinds :: [TcKind] -> [TcKind] -> TcM s ()
+unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 unifyKinds []       []       = returnTc ()
 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 	`thenTc_`
 			       unifyKinds ks1 ks2
@@ -61,7 +61,7 @@ unifyKinds _ _ = panic "unifyKinds: length mis-match"
 \end{code}
 
 \begin{code}
-unifyOpenTypeKind :: TcKind -> TcM s ()	
+unifyOpenTypeKind :: TcKind -> TcM ()	
 -- Ensures that the argument kind is of the form (Type bx)
 -- for some boxity bx
 
@@ -94,7 +94,7 @@ non-exported generic functions.
 Unify two @TauType@s.  Dead straightforward.
 
 \begin{code}
-unifyTauTy :: TcTauType -> TcTauType -> TcM s ()
+unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 unifyTauTy ty1 ty2 	-- ty1 expected, ty2 inferred
   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
     uTys ty1 ty1 ty2 ty2
@@ -106,7 +106,7 @@ of equal length.  We charge down the list explicitly so that we can
 complain if their lengths differ.
 
 \begin{code}
-unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM s ()
+unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM ()
 unifyTauTyLists [] 	     []	        = returnTc ()
 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
 					unifyTauTyLists tys1 tys2
@@ -118,7 +118,7 @@ all together.  It is used, for example, when typechecking explicit
 lists, when all the elts should be of the same type.
 
 \begin{code}
-unifyTauTyList :: [TcTauType] -> TcM s ()
+unifyTauTyList :: [TcTauType] -> TcM ()
 unifyTauTyList []		 = returnTc ()
 unifyTauTyList [ty]		 = returnTc ()
 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2	`thenTc_`
@@ -145,13 +145,17 @@ uTys :: TcTauType -> TcTauType	-- Error reporting ty1 and real ty1
 
      -> TcTauType -> TcTauType	-- Error reporting ty2 and real ty2
 				-- ty2 is the *actual* type
-     -> TcM s ()
+     -> TcM ()
 
 	-- Always expand synonyms (see notes at end)
-        -- (this also throws away FTVs and usage annots)
+        -- (this also throws away FTVs)
 uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 
+	-- Ignore usage annotations inside typechecker
+uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
+uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
+
 	-- Variables; go for uVar
 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
@@ -270,7 +274,7 @@ uVar :: Bool		-- False => tyvar is the "expected"
 			-- True  => ty    is the "expected" thing
      -> TcTyVar
      -> TcTauType -> TcTauType	-- printing and real versions
-     -> TcM s ()
+     -> TcM ()
 
 uVar swapped tv1 ps_ty2 ty2
   = tcGetTyVar tv1	`thenNF_Tc` \ maybe_ty1 ->
@@ -279,7 +283,7 @@ uVar swapped tv1 ps_ty2 ty2
 		 | otherwise -> uTys ty1 ty1 ps_ty2 ty2	-- Same order
 	other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 
-	-- Expand synonyms; ignore FTVs; ignore usage annots
+	-- Expand synonyms; ignore FTVs
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2)
   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 
@@ -298,7 +302,7 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
     case maybe_ty2 of
 	Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 
-	Nothing | tv1_dominates_tv2 
+	Nothing | update_tv2
 
 		-> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
 		   tcPutTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
@@ -306,36 +310,38 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 		|  otherwise
 
 		-> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
-                   (ASSERT( isNotUsgTy ps_ty2 )
-		    tcPutTyVar tv1 ps_ty2		`thenNF_Tc_`
+                   (tcPutTyVar tv1 ps_ty2		`thenNF_Tc_`
 	  	    returnTc ())
   where
     k1 = tyVarKind tv1
     k2 = tyVarKind tv2
-    tv1_dominates_tv2 =    isSigTyVar tv1 
+    update_tv2 = (k2 == openTypeKind) || (k1 /= openTypeKind && nicer_to_update_tv2)
+			-- Try to get rid of open type variables as soon as poss
+
+    nicer_to_update_tv2 =  isSigTyVar tv1 
 				-- Don't unify a signature type variable if poss
-			|| k2 == openTypeKind
-				-- Try to get rid of open type variables as soon as poss
-			|| varName tv1 `hasBetterProv` varName tv2 
+			|| isSystemName (varName tv2)
 				-- Try to update sys-y type variables in preference to sig-y ones
 
 	-- Second one isn't a type variable
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
-  = checkKinds swapped tv1 non_var_ty2			`thenTc_`
-    occur_check non_var_ty2				`thenTc_`
-    ASSERT( isNotUsgTy ps_ty2 )
+  = 	-- Check that the kinds match
+    checkKinds swapped tv1 non_var_ty2			`thenTc_`
+
+	-- Check that tv1 isn't a type-signature type variable
     checkTcM (not (isSigTyVar tv1))
 	     (failWithTcM (unifyWithSigErr tv1 ps_ty2))	`thenTc_`
 
+	-- Check that we aren't losing boxity info (shouldn't happen)
     warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
 	   ((ppr tv1 <+> ppr (tyVarKind tv1)) $$ 
 	     (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))		`thenNF_Tc_` 
 
-    tcPutTyVar tv1 non_var_ty2				`thenNF_Tc_`
-	-- This used to say "ps_ty2" instead of "non_var_ty2"
-
-	-- But that led to an infinite loop in the type checker!
-	-- Consider 
+	-- Occurs check
+	-- Basically we want to update     tv1 := ps_ty2
+	-- because ps_ty2 has type-synonym info, which improves later error messages
+	-- 
+	-- But consider 
 	--	type A a = ()
 	--
 	--	f :: (A a -> a -> ()) -> ()
@@ -344,33 +350,33 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 	-- 	x :: ()
 	-- 	x = f (\ x p -> p x)
 	--
-	-- Here, we try to match "t" with "A t", and succeed
-	-- because the unifier looks through synonyms.  The occurs
-	-- check doesn't kick in because we are "really" binding "t" to "()",
-	-- but we *actually* bind "t" to "A t" if we store ps_ty2.
-	-- That leads the typechecker into an infinite loop later.
-
-    returnTc ()
-  where
-    occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))	`thenTc_`
-		     returnTc ()
-
-    occur_check_tv tv2
-       | tv1 == tv2		-- Same tyvar; fail
-       = zonkTcType ps_ty2	`thenNF_Tc` \ zonked_ty2 ->
-	 failWithTcM (unifyOccurCheck tv1 zonked_ty2)
+	-- In the application (p x), we try to match "t" with "A t".  If we go
+	-- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into 
+	-- an infinite loop later.
+ 	-- But we should not reject the program, because A t = ().
+	-- Rather, we should bind t to () (= non_var_ty2).
+	-- 
+	-- That's why we have this two-state occurs-check
+    zonkTcType ps_ty2					`thenNF_Tc` \ ps_ty2' ->
+    if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
+	tcPutTyVar tv1 ps_ty2'				`thenNF_Tc_`
+	returnTc ()
+    else
+    zonkTcType non_var_ty2				`thenNF_Tc` \ non_var_ty2' ->
+    if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
+	-- This branch rarely succeeds, except in strange cases
+	-- like that in the example above
+	tcPutTyVar tv1 non_var_ty2'			`thenNF_Tc_`
+	returnTc ()
+    else
+    failWithTcM (unifyOccurCheck tv1 ps_ty2')
 
-       | otherwise		-- A different tyvar
-       = tcGetTyVar tv2	`thenNF_Tc` \ maybe_ty2 ->
-	 case maybe_ty2 of
-		Just ty2' -> occur_check ty2'
-		other	  -> returnTc ()
 
 checkKinds swapped tv1 ty2
 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
--- We need to check that we don't unify a boxed type variable with an
--- unboxed type: e.g.  (id 3#) is illegal
-  | tk1 == boxedTypeKind && tk2 == unboxedTypeKind
+-- We need to check that we don't unify a lifted type variable with an
+-- unlifted type: e.g.  (id 3#) is illegal
+  | tk1 == liftedTypeKind && tk2 == unliftedTypeKind
   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
     unifyMisMatch k1 k2
   | otherwise
@@ -393,7 +399,7 @@ checkKinds swapped tv1 ty2
 
 \begin{code}
 unifyFunTy :: TcType	 			-- Fail if ty isn't a function type
-	   -> TcM s (TcType, TcType)	-- otherwise return arg and result types
+	   -> TcM (TcType, TcType)	-- otherwise return arg and result types
 
 unifyFunTy ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
@@ -415,7 +421,7 @@ unify_fun_ty_help ty	-- Special cases failed, so revert to ordinary unification
 
 \begin{code}
 unifyListTy :: TcType              -- expected list type
-	    -> TcM s TcType      -- list element type
+	    -> TcM TcType      -- list element type
 
 unifyListTy ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
@@ -429,13 +435,13 @@ unifyListTy ty
 	other					    -> unify_list_ty_help ty
 
 unify_list_ty_help ty	-- Revert to ordinary unification
-  = newTyVarTy boxedTypeKind		`thenNF_Tc` \ elt_ty ->
+  = newTyVarTy liftedTypeKind		`thenNF_Tc` \ elt_ty ->
     unifyTauTy ty (mkListTy elt_ty)	`thenTc_`
     returnTc elt_ty
 \end{code}
 
 \begin{code}
-unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType]
+unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
@@ -456,7 +462,7 @@ unify_tuple_ty_help boxity arity ty
     unifyTauTy ty (mkTupleTy boxity arity arg_tys)	`thenTc_`
     returnTc arg_tys
   where
-    kind | isBoxed boxity = boxedTypeKind
+    kind | isBoxed boxity = liftedTypeKind
 	 | otherwise      = openTypeKind
 \end{code}