From: simonpj@microsoft.com <unknown>
Date: Tue, 6 Feb 2007 16:54:56 +0000 (+0000)
Subject: Check for escape when unifying forall-types
X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=e975c8f09ac8d85059a4b42cf56ebe036aa95dc7;ds=sidebyside

Check for escape when unifying forall-types

This egregious omission led to Trac #1128.
---

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index b8cb1f4..4a5b2cc 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -962,17 +962,23 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
 			-- Get location from monad, not from tvs1
 	     ; let tys      = mkTyVarTys tvs
 	           in_scope = mkInScopeSet (mkVarSet tvs)
- 	           subst1   = mkTvSubst in_scope (zipTyEnv tvs1 tys)
-	           subst2   = mkTvSubst in_scope (zipTyEnv tvs2 tys)
-		   (theta1,tau1) = tcSplitPhiTy (substTy subst1 body1)
-		   (theta2,tau2) = tcSplitPhiTy (substTy subst2 body2)
+ 	           phi1   = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+ 	           phi2   = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+		   (theta1,tau1) = tcSplitPhiTy phi1
+		   (theta2,tau2) = tcSplitPhiTy phi2
 
-	     ; checkM (equalLength theta1 theta2)
+	     ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+	     { checkM (equalLength theta1 theta2)
 		      (unifyMisMatch outer False orig_ty1 orig_ty2)
 	     
 	     ; uPreds False nb1 theta1 nb2 theta2
 	     ; uTys nb1 tau1 nb2 tau2
 
+		-- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
+	     ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+	     ; ifM (any (`elemVarSet` free_tvs) tvs)
+		   (bleatEscapedTvs free_tvs tvs tvs)
+
 		-- If both sides are inside a box, we are in a "box-meets-box"
 		-- situation, and we should not have a polytype at all.  
 		-- If we get here we have two boxes, already filled with
@@ -980,7 +986,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
 		-- This check comes last, because the error message is 
 		-- extremely unhelpful.  
 	     ; ifM (nb1 && nb2) (notMonoType ty1)
-	     }
+	     }}
       where
 	(tvs1, body1) = tcSplitForAllTys ty1
 	(tvs2, body2) = tcSplitForAllTys ty2
@@ -1537,6 +1543,16 @@ addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
 	<+> ptext SLIT("arguments")
 
 ------------------
+unifyForAllCtxt tvs phi1 phi2 env
+  = returnM (env2, msg)
+  where
+    (env', tvs') = tidyOpenTyVars env tvs	-- NB: not tidyTyVarBndrs
+    (env1, phi1') = tidyOpenType env' phi1
+    (env2, phi2') = tidyOpenType env1 phi2
+    msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
+	        ptext SLIT("          and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
+
+------------------
 unifyKindCtxt swapped tv1 ty2 tidy_env	-- not swapped => tv1 expected, ty2 inferred
 	-- tv1 and ty2 are zonked already
   = returnM msg