X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=b502b16a361b05de1173a5195597b940c21f4c66;hb=cbdeae8fc8a1c72d20d89241acae8a313214b51c;hp=c136846e14fddf0d5a9402bc2c770946cf88eac2;hpb=d133b73a4d4717892ced072d05e039a54ede0ceb;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index c136846..b502b16 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -8,36 +8,33 @@ updatable substitution).
 
 \begin{code}
 module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, 
-	         unifyFunTy, unifyListTy, unifyTupleTy, unifyUnboxedTupleTy,
-	 	 unifyKind, unifyKinds, unifyTypeKind
+	         unifyFunTy, unifyListTy, unifyTupleTy,
+	 	 unifyKind, unifyKinds, unifyOpenTypeKind
  ) where
 
 #include "HsVersions.h"
 
 -- friends: 
 import TcMonad
-import Type	( Type(..), tyVarsOfType, funTyCon,
+import TypeRep	( Type(..), PredType(..) )  -- friend
+import Type	( unliftedTypeKind, liftedTypeKind, openTypeKind, 
+		  typeCon, openKindCon, hasMoreBoxityInfo, 
+		  tyVarsOfType, typeKind,
 		  mkFunTy, splitFunTy_maybe, splitTyConApp_maybe,
-                  isNotUsgTy,
-		  Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind,
-		  splitAppTy_maybe,
+                  splitAppTy_maybe, mkTyConApp, 
 	   	  tidyOpenType, tidyOpenTypes, tidyTyVar
 		)
-import TyCon	( TyCon, isTupleTyCon, isUnboxedTupleTyCon, 
-		  tyConArity )
-import Name	( hasBetterProv )
-import Var	( TyVar, tyVarKind, varName, isSigTyVar )
-import VarEnv	
-import VarSet	( varSetElems )
-import TcType	( TcType, TcTauType, TcTyVar, TcKind, 
-		  newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind,
-		  tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind
+import TyCon	( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity )
+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 )
-import TysWiredIn ( listTyCon, mkListTy, mkTupleTy, mkUnboxedTupleTy )
-import PprType	()		-- Instances
-import Util
+import BasicTypes ( Arity, Boxity, isBoxed )
+import TysWiredIn ( listTyCon, mkListTy, mkTupleTy )
 import Outputable
 \end{code}
 
@@ -51,18 +48,39 @@ 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
 unifyKinds _ _ = panic "unifyKinds: length mis-match"
 \end{code}
 
+\begin{code}
+unifyOpenTypeKind :: TcKind -> TcM ()	
+-- Ensures that the argument kind is of the form (Type bx)
+-- for some boxity bx
+
+unifyOpenTypeKind ty@(TyVarTy tyvar)
+  = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
+    case maybe_ty of
+	Just ty' -> unifyOpenTypeKind ty'
+	other	 -> unify_open_kind_help ty
+
+unifyOpenTypeKind ty
+  = case splitTyConApp_maybe ty of
+	Just (tycon, [_]) | tycon == typeCon -> returnTc ()
+	other				     -> unify_open_kind_help ty
+
+unify_open_kind_help ty	-- Revert to ordinary unification
+  = newBoxityVar 	`thenNF_Tc` \ boxity ->
+    unifyKind ty (mkTyConApp typeCon [boxity])
+\end{code}
+
 
 %************************************************************************
 %*									*
@@ -76,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
@@ -88,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
@@ -100,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_`
@@ -123,33 +141,46 @@ We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 
 \begin{code}
 uTys :: TcTauType -> TcTauType	-- Error reporting ty1 and real ty1
+				-- ty1 is the *expected* type
+
      -> TcTauType -> TcTauType	-- Error reporting ty2 and real ty2
-     -> TcM s ()
+				-- ty2 is the *actual* type
+     -> 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
 					-- "True" means args swapped
 
+	-- Predicates
+uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
+  | n1 == n2 = uTys t1 t1 t2 t2
+uTys _ (PredTy (ClassP c1 tys1)) _ (PredTy (ClassP c2 tys2))
+  | c1 == c2 = unifyTauTyLists tys1 tys2
+
 	-- Functions; just check the two parts
 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
   = uTys fun1 fun1 fun2 fun2	`thenTc_`    uTys arg1 arg1 arg2 arg2
 
 	-- Type constructors must match
 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
-  = checkTcM (cons_match && length tys1 == length tys2) 
-	     (unifyMisMatch ps_ty1 ps_ty2)			`thenTc_`
-    unifyTauTyLists tys1 tys2
-  where
-	-- The AnyBox wild card matches anything
-    cons_match =  con1 == con2 
-	       || con1 == anyBoxCon
-	       || con2 == anyBoxCon
+  | con1 == con2 && length tys1 == length tys2
+  = unifyTauTyLists tys1 tys2
+
+  | con1 == openKindCon
+	-- When we are doing kind checking, we might match a kind '?' 
+	-- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
+	-- (CCallable Int) and (CCallable Int#) are both OK
+  = unifyOpenTypeKind ps_ty2
 
 	-- Applications need a bit of care!
 	-- They can match FunTy and TyConApp, so use splitAppTy_maybe
@@ -243,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 ->
@@ -252,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
 
@@ -271,66 +302,93 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
     case maybe_ty2 of
 	Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 
-	Nothing -> checkKinds swapped tv1 ty2			`thenTc_`
+	Nothing | update_tv2
+
+		-> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
+		   tcPutTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
+		   returnTc ()
+		|  otherwise
 
-		   if tv1 `dominates` tv2 then
-			tcPutTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
-			returnTc ()
-		   else
-                        ASSERT( isNotUsgTy ps_ty2 )
-			tcPutTyVar tv1 ps_ty2			`thenNF_Tc_`
-			returnTc ()
+		-> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
+                   (tcPutTyVar tv1 ps_ty2		`thenNF_Tc_`
+	  	    returnTc ())
   where
-    tv1 `dominates` tv2 =  isSigTyVar tv1 
+    k1 = tyVarKind tv1
+    k2 = tyVarKind tv2
+    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
-			|| 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
-  | non_var_ty2 == anyBoxKind
-	-- If the 
-  = returnTc ()
+  = 	-- Check that the kinds match
+    checkKinds swapped tv1 non_var_ty2			`thenTc_`
 
-  | otherwise
-  = checkKinds swapped tv1 non_var_ty2			`thenTc_`
-    occur_check non_var_ty2				`thenTc_`
-    ASSERT( isNotUsgTy ps_ty2 )
+	-- Check that tv1 isn't a type-signature type variable
     checkTcM (not (isSigTyVar tv1))
 	     (failWithTcM (unifyWithSigErr tv1 ps_ty2))	`thenTc_`
-    tcPutTyVar tv1 ps_ty2				`thenNF_Tc_`
-    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)
+	-- 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_` 
+
+	-- 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 -> ()) -> ()
+	--	f = \ _ -> ()
+	--
+	-- 	x :: ()
+	-- 	x = f (\ x p -> p x)
+	--
+	-- 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 lifted type variable with an
+-- unlifted type: e.g.  (id 3#) is illegal
+  | tk1 == liftedTypeKind && tk2 == unliftedTypeKind
   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
-
-	-- We have to use tcTypeKind not just typeKind to get the
-	-- kind of ty2, because there might be mutable kind variables
-	-- in the way.  For example, suppose that ty2 :: (a b), and
-	-- the kind of 'a' is a kind variable 'k' that has (presumably)
-	-- been unified with 'k1 -> k2'.
-    tcTypeKind ty2		`thenNF_Tc` \ k2 ->
-
-    if swapped then
-	unifyKind k2 (tyVarKind tv1)
-    else
-	unifyKind (tyVarKind tv1) k2
+    unifyMisMatch k1 k2
+  | otherwise
+  = returnTc ()
+  where
+    (k1,k2) | swapped   = (tk2,tk1)
+	    | otherwise = (tk1,tk2)
+    tk1 = tyVarKind tv1
+    tk2 = typeKind ty2
 \end{code}
 
+
 %************************************************************************
 %*									*
 \subsection[Unify-fun]{@unifyFunTy@}
@@ -341,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 ->
@@ -355,15 +413,15 @@ unifyFunTy ty
 	Nothing 	 -> unify_fun_ty_help ty
 
 unify_fun_ty_help ty	-- Special cases failed, so revert to ordinary unification
-  = newTyVarTy_OpenKind		`thenNF_Tc` \ arg ->
-    newTyVarTy_OpenKind		`thenNF_Tc` \ res ->
+  = newTyVarTy openTypeKind	`thenNF_Tc` \ arg ->
+    newTyVarTy openTypeKind	`thenNF_Tc` \ res ->
     unifyTauTy ty (mkFunTy arg res)	`thenTc_`
     returnTc (arg,res)
 \end{code}
 
 \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 ->
@@ -377,71 +435,35 @@ 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 :: Arity -> TcType -> TcM s [TcType]
-unifyTupleTy arity ty@(TyVarTy tyvar)
-  = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
-    case maybe_ty of
-	Just ty' -> unifyTupleTy arity ty'
-	other	    -> unify_tuple_ty_help arity ty
-
-unifyTupleTy arity ty
-  = case splitTyConApp_maybe ty of
-	Just (tycon, arg_tys) |  isTupleTyCon tycon 
-			 && tyConArity tycon == arity
-			 -> returnTc arg_tys
-	other -> unify_tuple_ty_help arity ty
-
-unify_tuple_ty_help arity ty
-  = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity]	`thenNF_Tc` \ arg_tys ->
-    unifyTauTy ty (mkTupleTy arity arg_tys)			`thenTc_`
-    returnTc arg_tys
-\end{code}
-
-\begin{code}
-unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType]
-unifyUnboxedTupleTy arity ty@(TyVarTy tyvar)
+unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
+unifyTupleTy boxity arity ty@(TyVarTy tyvar)
   = tcGetTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
     case maybe_ty of
-	Just ty' -> unifyUnboxedTupleTy arity ty'
-	other	 -> unify_unboxed_tuple_ty_help arity ty
+	Just ty' -> unifyTupleTy boxity arity ty'
+	other	 -> unify_tuple_ty_help boxity arity ty
 
-unifyUnboxedTupleTy arity ty
+unifyTupleTy boxity arity ty
   = case splitTyConApp_maybe ty of
-	Just (tycon, arg_tys) |  isUnboxedTupleTyCon tycon 
-			 && tyConArity tycon == arity
-			 -> returnTc arg_tys
-	other -> unify_tuple_ty_help arity ty
-
-unify_unboxed_tuple_ty_help arity ty
-  = mapNF_Tc (\ _ -> newTyVarTy_OpenKind) [1..arity]	`thenNF_Tc` \ arg_tys ->
-    unifyTauTy ty (mkUnboxedTupleTy arity arg_tys)	`thenTc_`
+	Just (tycon, arg_tys)
+		|  isTupleTyCon tycon 
+		&& tyConArity tycon == arity
+		&& tupleTyConBoxity tycon == boxity
+		-> returnTc arg_tys
+	other -> unify_tuple_ty_help boxity arity ty
+
+unify_tuple_ty_help boxity arity ty
+  = newTyVarTys arity kind				`thenNF_Tc` \ arg_tys ->
+    unifyTauTy ty (mkTupleTy boxity arity arg_tys)	`thenTc_`
     returnTc arg_tys
-\end{code}
-
-Make sure a kind is of the form (Type b) for some boxity b.
-
-\begin{code}
-unifyTypeKind  :: TcKind -> TcM s ()
-unifyTypeKind kind@(TyVarTy kv)
-  = tcGetTyVar kv 	`thenNF_Tc` \ maybe_kind ->
-    case maybe_kind of
-	Just kind' -> unifyTypeKind kind'
-	Nothing    -> unify_type_kind_help kind
-
-unifyTypeKind kind
-  = case splitTyConApp_maybe kind of
-	Just (tycon, [_]) | tycon == typeCon -> returnTc ()
-	other				     -> unify_type_kind_help kind
-
-unify_type_kind_help kind
-  = newOpenTypeKind	`thenNF_Tc` \ expected_kind ->
-    unifyKind expected_kind kind
+  where
+    kind | isBoxed boxity = liftedTypeKind
+	 | otherwise      = openTypeKind
 \end{code}
 
 
@@ -470,15 +492,19 @@ unifyCtxt s ty1 ty2 tidy_env	-- ty1 expected, ty2 inferred
 		    (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 
 unifyKindCtxt swapped tv1 ty2 tidy_env	-- not swapped => tv1 expected, ty2 inferred
-  = returnNF_Tc (env2, ptext SLIT("When matching types") <+> 
-		       sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
+	-- tv1 is zonked already
+  = zonkTcType ty2	`thenNF_Tc` \ ty2' ->
+    returnNF_Tc (err ty2')
   where
-    (pp_expected, pp_actual) | swapped   = (pp2, pp1)
-			     | otherwise = (pp1, pp2)
-    (env1, tv1') = tidyTyVar tidy_env tv1
-    (env2, ty2') = tidyOpenType  env1     ty2
-    pp1 = ppr tv1'
-    pp2 = ppr ty2'
+    err ty2 = (env2, ptext SLIT("When matching types") <+> 
+		     sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
+	    where
+	      (pp_expected, pp_actual) | swapped   = (pp2, pp1)
+				       | otherwise = (pp1, pp2)
+	      (env1, tv1') = tidyTyVar tidy_env tv1
+	      (env2, ty2') = tidyOpenType  env1 ty2
+	      pp1 = ppr tv1'
+	      pp2 = ppr ty2'
 
 unifyMisMatch ty1 ty2
   = zonkTcType ty1	`thenNF_Tc` \ ty1' ->