From fd7f8e936e50b3ee589efc36ac2fc54cc6c05300 Mon Sep 17 00:00:00 2001
From: "simonpj@microsoft.com" <unknown>
Date: Wed, 30 May 2007 08:12:40 +0000
Subject: [PATCH] Fix bug in tcSimplifyInfer (Trac #1382)

When I rejigged constraint simplification when inferring types, I missed
a corner case.  Somethign that it's distressingly easy to do.  Anyway
this fixes it; see the comments in tcSimplifyInfer with the second call
to partition and extendLIEs.

The test is tcfail181.
---
 compiler/typecheck/TcSimplify.lhs |   33 +++++++++++++++++++++++++--------
 1 file changed, 25 insertions(+), 8 deletions(-)

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index b9ff789..6819d5a 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -209,8 +209,8 @@ Notice that
 
 -----------------------------------------
 
-Choosing Q
-~~~~~~~~~~
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Here's a good way to choose Q:
 
 	Q = grow( fv(T), C ) \ oclose( fv(G), C )
@@ -670,18 +670,35 @@ tcSimplifyInfer doc tau_tvs wanted
 	; gbl_tvs  <- tcGetGlobalTyVars
 	; let preds = fdPredsOfInsts wanted'
 	      qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
-	      (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
-	; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
-	; extendLIEs free
+			-- See Note [Choosing which variables to quantify]
+
+		-- To maximise sharing, remove from consideration any 
+		-- constraints that don't mention qtvs at all
+	; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
+	; extendLIEs free1
 
 		-- To make types simple, reduce as much as possible
+	; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ 
+		   ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
 	; let try_me inst = ReduceMe AddSCs
 	; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
-
 	; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
 
-	-- We can't abstract over implications
-	; let (dicts, implics) = partition isDict irreds
+		-- Do not quantify over constraints that *now* do not
+		-- mention quantified type variables, because they are
+		-- simply ambiguous.  Example:
+		-- 	f :: Eq b => a -> (a, b)
+		--	g x = fst (f x)
+		-- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+		-- We decide to quantify over 'alpha' alone, bur free1 does not include f77
+		-- because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
+		-- constraint (Eq beta), which we dump back into the free set
+		-- See test tcfail181
+	; let (free2, irreds2) = partition (isFreeWhenInferring (mkVarSet qtvs')) irreds
+	; extendLIEs free2
+	
+		-- We can't abstract over implications
+	; let (dicts, implics) = partition isDict irreds2
 	; loc <- getInstLoc (ImplicOrigin doc)
 	; implic_bind <- bindIrreds loc qtvs' dicts implics
 
-- 
1.7.10.4