From a7ba22ff9bdc25d23af38ff1a2c9bbcc12dd45b8 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Wed, 1 Nov 2006 12:21:20 +0000 Subject: [PATCH] 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 --- compiler/typecheck/TcDeriv.lhs | 13 +++------- compiler/typecheck/TcMType.lhs | 31 +++++++++++------------ compiler/typecheck/TcSimplify.lhs | 49 ++++++++++++++++++++++++++++--------- 3 files changed, 58 insertions(+), 35 deletions(-) diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index 68c5173..90ff3a7 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 5fe7db6..4aef899 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 247df7d..c0ae8ce 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. -- 1.7.10.4