From 1d051fbc5df6586298357580fd48de1a51e645b4 Mon Sep 17 00:00:00 2001
From: Manuel M T Chakravarty <chak@cse.unsw.edu.au>
Date: Wed, 19 Sep 2007 15:07:38 +0000
Subject: [PATCH] FIX #1688: Givens in checkLoop are not that rigid after all
 - This patch re-instates the policy of 6.6.1 to zonk the
 given constraints   in the simplifier loop.

MERGE TO STABLE
---
 compiler/typecheck/TcSimplify.lhs |   49 ++++++++++++++++++++++++++++++++++---
 1 file changed, 45 insertions(+), 4 deletions(-)

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 872a7a8..292c231 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1085,10 +1085,11 @@ checkLoop :: RedEnv
 checkLoop env wanteds
   = go env wanteds []
   where go env wanteds needed_givens
-	  = do { -- Givens are skolems, so no need to zonk them
-		 wanteds' <- zonkInsts wanteds
+	  = do {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+                ; env'     <- zonkRedEnv env
+		; wanteds' <- zonkInsts  wanteds
 	
-		; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
+		; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'
 
 		; let all_needed_givens = needed_givens ++ more_needed_givens
 	
@@ -1101,10 +1102,44 @@ checkLoop env wanteds
 		-- Using an instance decl might have introduced a fresh type variable
 		-- which might have been unified, so we'd get an infinite loop
 		-- if we started again with wanteds!  See Note [LOOP]
-		{ (irreds1, binds1, all_needed_givens1) <- go env irreds all_needed_givens
+		{ (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens
 		; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
 \end{code}
 
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables.  An example from tc237 in the
+testsuite is
+
+  class Modular s a | s -> a
+
+  wim ::  forall a w. Integral a 
+                        => a -> (forall s. Modular s a => M s w) -> w
+  wim i k = error "urk"
+
+  test5  ::  (Modular s a, Integral a) => M s a
+  test5  =   error "urk"
+
+  test4   =   wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside.  When type checking test4, we have to check
+whether the signature of test5 is an instance of 
+
+  (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens. 
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature).  If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
+
+
 Note [LOOP]
 ~~~~~~~~~~~
 	class If b t e r | b t e -> r
@@ -1655,6 +1690,12 @@ data WantSCs = NoSCs | AddSCs	-- Tells whether we should add the superclasses
 				-- of a predicate when adding it to the avails
 	-- The reason for this flag is entirely the super-class loop problem
 	-- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env 
+  = do { givens' <- mappM zonkInst (red_givens env)
+       ; return $ env {red_givens = givens'}
+       }
 \end{code}
 
 
-- 
1.7.10.4