Fix error reporting for contexts during deriving (Trac 958)

When doing the fixpoint iteration for 'deriving' we have to be careful
not to end up in a loop, even if we have -fallow-undecidable-instances.

Test is tcfail169

3 files changed, 58 insertions, 35 deletions

diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index 68c5173be2..90ff3a7c8c 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -15,7 +15,6 @@ import DynFlags
 
 import Generics
 import TcRnMonad
-import TcMType
 import TcEnv
 import TcGenDeriv	-- Deriv stuff
 import InstEnv
@@ -763,9 +762,10 @@ solveDerivEqns overlap_flag orig_eqns
 	do { let inst_tys = [mkTyConApp tc (mkTyVarTys tyvars)]
 	   ; theta <- addErrCtxt (derivInstCtxt1 clas inst_tys) $
 		      tcSimplifyDeriv orig tc tyvars deriv_rhs
-	   ; addErrCtxt (derivInstCtxt2 theta clas inst_tys) $
-	     checkValidInstance tyvars theta clas inst_tys
-	   ; return (sortLe (<=) theta) }	-- Canonicalise before returning the soluction
+		-- Claim: the result instance declaration is guaranteed valid
+		-- Hence no need to call:
+		--   checkValidInstance tyvars theta clas inst_tys
+	   ; return (sortLe (<=) theta) }	-- Canonicalise before returning the solution
       where
 	
 
@@ -995,10 +995,5 @@ derivCtxt tycon
 
 derivInstCtxt1 clas inst_tys
   = ptext SLIT("When deriving the instance for") <+> quotes (pprClassPred clas inst_tys)
-
-derivInstCtxt2 theta clas inst_tys
-  = vcat [ptext SLIT("In the derived instance declaration"),
-          nest 2 (ptext SLIT("instance") <+> sep [pprThetaArrow theta, 
-						  pprClassPred clas inst_tys])]
 \end{code}
 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 5fe7db61ec..4aef899723 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -72,8 +72,10 @@ import TcRnMonad          -- TcType, amongst others
 import FunDeps
 import Name
 import VarSet
+import ErrUtils
 import DynFlags
 import Util
+import Maybes
 import ListSetOps
 import UniqSupply
 import Outputable
@@ -1102,7 +1104,7 @@ checkValidInstance tyvars theta clas inst_tys
 	-- Check that instance inference will terminate (if we care)
 	-- For Haskell 98, checkValidTheta has already done that
 	; when (gla_exts && not undecidable_ok) $
-	       checkInstTermination theta inst_tys
+	  mapM_ failWithTc (checkInstTermination inst_tys theta)
 	
 	-- The Coverage Condition
 	; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
@@ -1126,20 +1128,19 @@ The underlying idea is that
 
 
 \begin{code}
-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
-  = do	{ mappM_ (check_nomore (fvTypes tys))    theta
-	; mappM_ (check_smaller (sizeTypes tys)) theta }
-
-check_nomore :: [TyVar] -> PredType -> TcM ()
-check_nomore fvs pred
-  = checkTc (null (fvPred pred \\ fvs))
-	    (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
-
-check_smaller :: Int -> PredType -> TcM ()
-check_smaller n pred
-  = checkTc (sizePred pred < n)
-	    (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+checkInstTermination :: [TcType] -> ThetaType -> [Message]
+checkInstTermination tys theta
+  = mapCatMaybes check theta
+  where
+   fvs  = fvTypes tys
+   size = sizeTypes tys
+   check pred 
+      | not (null (fvPred pred \\ fvs)) 
+      = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+      | sizePred pred >= size
+      = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+      | otherwise
+      = Nothing
 
 predUndecErr pred msg = sep [msg,
 			nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 247df7d8ca..c0ae8ce45f 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -2150,29 +2150,35 @@ tcSimplifyDeriv orig tc tyvars theta
     doptM Opt_GlasgowExts			`thenM` \ gla_exts ->
     doptM Opt_AllowUndecidableInstances		`thenM` \ undecidable_ok ->
     let
- 	tv_set      = mkVarSet tvs
-
- 	(bad_insts, ok_insts) = partition is_bad_inst irreds
-	is_bad_inst dict 
-	   = let pred = dictPred dict	-- reduceMe squashes all non-dicts
-	     in isEmptyVarSet (tyVarsOfPred pred)
-		  -- Things like (Eq T) are bad
-	     || (not gla_exts && not (isTyVarClassPred pred))
-  
+	inst_ty = mkTyConApp tc (mkTyVarTys tvs)
+ 	(ok_insts, bad_insts) = partition is_ok_inst irreds
+	is_ok_inst dict 
+	   = isTyVarClassPred pred || (gla_exts && ok_gla_pred pred)
+	   where
+	     pred = dictPred dict	-- reduceMe squashes all non-dicts
+
+	ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred])
+	 	-- See Note [Deriving context]
+	   
+ 	tv_set = mkVarSet tvs
 	simpl_theta = map dictPred ok_insts
 	weird_preds = [pred | pred <- simpl_theta
 			    , not (tyVarsOfPred pred `subVarSet` tv_set)]  
+
 	  -- Check for a bizarre corner case, when the derived instance decl should
 	  -- have form 	instance C a b => D (T a) where ...
 	  -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
 	  -- of problems; in particular, it's hard to compare solutions for
 	  -- equality when finding the fixpoint.  So I just rule it out for now.
-  
+	
 	rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
 		-- This reverse-mapping is a Royal Pain, 
 		-- but the result should mention TyVars not TcTyVars
     in
-   
+	-- In effect, the bad and wierd insts cover all of the cases that
+	-- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv
+	--   * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance)
+	--   * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance)
     addNoInstanceErrs Nothing [] bad_insts		`thenM_`
     mapM_ (addErrTc . badDerivedPred) weird_preds	`thenM_`
     returnM (substTheta rev_env simpl_theta)
@@ -2180,6 +2186,27 @@ tcSimplifyDeriv orig tc tyvars theta
     doc    = ptext SLIT("deriving classes for a data type")
 \end{code}
 
+Note [Deriving context]
+~~~~~~~~~~~~~~~~~~~~~~~
+With -fglasgow-exts, we allow things like (C Int a) in the simplified
+context for a derived instance declaration, because at a use of this
+instance, we might know that a=Bool, and have an instance for (C Int
+Bool)
+
+We nevertheless insist that each predicate meets the termination
+conditions. If not, the deriving mechanism generates larger and larger
+constraints.  Example:
+  data Succ a = S a
+  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ.  First we'll generate
+  instance (Show (Succ a), Show a) => Show (Seq a)
+and then
+  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+and so on.  Instead we want to complain of no instance for (Show (Succ a)).
+  
+
+
 @tcSimplifyDefault@ just checks class-type constraints, essentially;
 used with \tr{default} declarations.  We are only interested in
 whether it worked or not.