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

diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index 68c5173..90ff3a7 100644 (file)
--- 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 5fe7db6..4aef899 100644 (file)
--- 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 247df7d..c0ae8ce 100644 (file)
--- 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.