From e5a8d57c85d42007c8cc561e6d6b805c23603fc0 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Wed, 11 Feb 2009 17:47:33 +0000 Subject: [PATCH] Fix Trac #3017: ensure that we quantify over enough type variables when equalities are involved The function FunDeps.grow was not doing the right thing when type equality constraints were involved. That wasn't really its fault: its input was being filtered by fdPredsOfInsts. To fix this I did a bit of refactoring, so that the (revolting) fdPredsOfInsts is now less important (maybe we can get rid of it in due course). The 'grow' function moves from FunDeps to Inst.growInstsTyVars TcMTType.growThetaTyVars TcMType.growTyVars The main comments are with the first of these, in Note [Growing the tau-tvs using constraints] in Inst. Push to the branch if conflict free. --- compiler/basicTypes/VarSet.lhs | 9 ++++++- compiler/typecheck/Inst.lhs | 50 +++++++++++++++++++++++++++++++---- compiler/typecheck/TcMType.lhs | 25 +++++++++++++++++- compiler/typecheck/TcSimplify.lhs | 6 ++--- compiler/typecheck/TcTyClsDecls.lhs | 3 +-- compiler/types/FunDeps.lhs | 40 +--------------------------- 6 files changed, 82 insertions(+), 51 deletions(-) diff --git a/compiler/basicTypes/VarSet.lhs b/compiler/basicTypes/VarSet.lhs index 67a3dbf..6f03aad 100644 --- a/compiler/basicTypes/VarSet.lhs +++ b/compiler/basicTypes/VarSet.lhs @@ -15,7 +15,7 @@ module VarSet ( unionVarSet, unionVarSets, intersectVarSet, intersectsVarSet, disjointVarSet, isEmptyVarSet, delVarSet, delVarSetList, delVarSetByKey, - minusVarSet, foldVarSet, filterVarSet, + minusVarSet, foldVarSet, filterVarSet, fixVarSet, lookupVarSet, mapVarSet, sizeVarSet, seqVarSet, elemVarSetByKey ) where @@ -63,6 +63,7 @@ extendVarSet_C :: (Var->Var->Var) -> VarSet -> Var -> VarSet delVarSetByKey :: VarSet -> Unique -> VarSet elemVarSetByKey :: Unique -> VarSet -> Bool +fixVarSet :: (VarSet -> VarSet) -> VarSet -> VarSet emptyVarSet = emptyUniqSet unitVarSet = unitUniqSet @@ -100,6 +101,12 @@ elemVarSetByKey = elemUniqSet_Directly intersectsVarSet s1 s2 = not (s1 `disjointVarSet` s2) disjointVarSet s1 s2 = isEmptyVarSet (s1 `intersectVarSet` s2) subVarSet s1 s2 = isEmptyVarSet (s1 `minusVarSet` s2) + +-- Iterate f to a fixpoint +fixVarSet f s | new_s `subVarSet` s = s + | otherwise = fixVarSet f new_s + where + new_s = f s \end{code} \begin{code} diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index b5eeff0..8a014bc 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -24,7 +24,7 @@ module Inst ( tyVarsOfInst, tyVarsOfInsts, tyVarsOfLIE, ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts, - getDictClassTys, dictPred, + growInstsTyVars, getDictClassTys, dictPred, lookupSimpleInst, LookupInstResult(..), tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag, @@ -152,6 +152,7 @@ getDictClassTys :: Inst -> (Class, [Type]) getDictClassTys (Dict {tci_pred = pred}) = getClassPredTys pred getDictClassTys inst = pprPanic "getDictClassTys" (ppr inst) +-------------------------------- -- fdPredsOfInst is used to get predicates that contain functional -- dependencies *or* might do so. The "might do" part is because -- a constraint (C a b) might have a superclass with FDs @@ -161,14 +162,16 @@ getDictClassTys inst = pprPanic "getDictClassTys" (ppr inst) fdPredsOfInst :: Inst -> [TcPredType] fdPredsOfInst (Dict {tci_pred = pred}) = [pred] fdPredsOfInst (Method {tci_theta = theta}) = theta -fdPredsOfInst (ImplicInst {tci_given = gs, - tci_wanted = ws}) = fdPredsOfInsts (gs ++ ws) +fdPredsOfInst (ImplicInst {tci_wanted = ws}) = fdPredsOfInsts ws + -- The ImplicInst case doesn't look right; + -- what if ws mentions skolem variables? fdPredsOfInst (LitInst {}) = [] fdPredsOfInst (EqInst {}) = [] fdPredsOfInsts :: [Inst] -> [PredType] fdPredsOfInsts insts = concatMap fdPredsOfInst insts +--------------------------------- isInheritableInst :: Inst -> Bool isInheritableInst (Dict {tci_pred = pred}) = isInheritablePred pred isInheritableInst (Method {tci_theta = theta}) = all isInheritablePred theta @@ -216,8 +219,45 @@ addInstToDictBind :: TcDictBinds -> Inst -> LHsExpr TcId -> TcDictBinds addInstToDictBind binds inst rhs = binds `unionBags` instToDictBind inst rhs \end{code} -Predicates -~~~~~~~~~~ +Note [Growing the tau-tvs using constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(growInstsTyVars insts tvs) is the result of extending the set + of tyvars tvs using all conceivable links from pred + +E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} +Then grow precs tvs = {a,b,c} + +All the type variables from an implicit parameter are added, whether or +not they are mentioned in tvs; see Note [Implicit parameters and ambiguity] +in TcSimplify. + +See also Note [Ambiguity] in TcSimplify + +\begin{code} +growInstsTyVars :: [Inst] -> TyVarSet -> TyVarSet +growInstsTyVars insts tvs + | null insts = tvs + | otherwise = fixVarSet mk_next tvs + where + mk_next tvs = foldr grow_inst_tvs tvs insts + +grow_inst_tvs :: Inst -> TyVarSet -> TyVarSet +grow_inst_tvs (Dict {tci_pred = pred}) tvs = growPredTyVars pred tvs +grow_inst_tvs (Method {tci_theta = theta}) tvs = foldr growPredTyVars tvs theta +grow_inst_tvs (ImplicInst {tci_tyvars = tvs1, tci_wanted = ws}) tvs + = tvs `unionVarSet` (foldr grow_inst_tvs (tvs `delVarSetList` tvs1) ws + `delVarSetList` tvs1) +grow_inst_tvs inst tvs -- EqInst, LitInst + = growTyVars (tyVarsOfInst inst) tvs +\end{code} + + +%************************************************************************ +%* * + Predicates +%* * +%************************************************************************ + \begin{code} isAbstractableInst :: Inst -> Bool diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 47592f5..9a17b0f 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -45,6 +45,7 @@ module TcMType ( checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt, unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs, + growPredTyVars, growTyVars, growThetaTyVars, -------------------------------- -- Zonking @@ -1421,7 +1422,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars = mapM_ complain (filter is_ambig theta) where complain pred = addErrTc (ambigErr pred) - extended_tau_vars = grow theta tau_tyvars + extended_tau_vars = growThetaTyVars theta tau_tyvars -- See Note [Implicit parameters and ambiguity] in TcSimplify is_ambig pred = isClassPred pred && @@ -1435,6 +1436,28 @@ ambigErr pred = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$ ptext (sLit "must be reachable from the type after the '=>'"))] + +-------------------------- +-- For this 'grow' stuff see Note [Growing the tau-tvs using constraints] in Inst + +growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet +-- Finds a fixpoint +growThetaTyVars theta tvs + | null theta = tvs + | otherwise = fixVarSet mk_next tvs + where + mk_next tvs = foldr growPredTyVars tvs theta + + +growPredTyVars :: TcPredType -> TyVarSet -> TyVarSet +-- Here is where the special case for inplicit parameters happens +growPredTyVars (IParam _ ty) tvs = tvs `unionVarSet` tyVarsOfType ty +growPredTyVars pred tvs = growTyVars (tyVarsOfPred pred) tvs + +growTyVars :: TyVarSet -> TyVarSet -> TyVarSet +growTyVars new_tvs tvs + | new_tvs `intersectsVarSet` tvs = tvs `unionVarSet` new_tvs + | otherwise = tvs \end{code} In addition, GHC insists that at least one type variable diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 071d4c0..0e1e5b0 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -659,7 +659,7 @@ tcSimplifyInfer doc tau_tvs wanted ; gbl_tvs <- tcGetGlobalTyVars ; let preds1 = fdPredsOfInsts wanted' gbl_tvs1 = oclose preds1 gbl_tvs - qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1 + qtvs = growInstsTyVars wanted' tau_tvs1 `minusVarSet` gbl_tvs1 -- See Note [Choosing which variables to quantify] -- To maximise sharing, remove from consideration any @@ -668,7 +668,7 @@ tcSimplifyInfer doc tau_tvs wanted ; extendLIEs free -- To make types simple, reduce as much as possible - ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ + ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (growInstsTyVars wanted' tau_tvs1) $$ ppr gbl_tvs $$ ppr gbl_tvs1 $$ ppr free $$ ppr bound)) ; (irreds1, binds1) <- tryHardCheckLoop doc bound @@ -709,7 +709,7 @@ tcSimplifyInfer doc tau_tvs wanted -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and -- irreds2 will be empty. But we don't want to generalise over b! ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked - qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2 + qtvs = growInstsTyVars irreds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2 ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2 ; extendLIEs free diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 1a9e054..158eb64 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -25,7 +25,6 @@ import TcHsType import TcMType import TcType import TysWiredIn ( unitTy ) -import FunDeps import Type import Generics import Class @@ -1172,7 +1171,7 @@ checkValidClass cls -- class Error e => Game b mv e | b -> mv e where -- newBoard :: MonadState b m => m () -- Here, MonadState has a fundep m->b, so newBoard is fine - ; let grown_tyvars = grow theta (mkVarSet tyvars) + ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars) ; checkTc (tyVarsOfType tau `intersectsVarSet` grown_tyvars) (noClassTyVarErr cls sel_id) diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs index af7cfec..02b0a2a 100644 --- a/compiler/types/FunDeps.lhs +++ b/compiler/types/FunDeps.lhs @@ -10,7 +10,7 @@ It's better to read it as: "if we know these, then we're going to know these" \begin{code} module FunDeps ( Equation, pprEquation, - oclose, grow, improveOne, + oclose, improveOne, checkInstCoverage, checkFunDeps, pprFundeps ) where @@ -132,44 +132,6 @@ oclose preds fixed_tvs ] \end{code} -Note [Growing the tau-tvs using constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -(grow preds tvs) is the result of extend the set of tyvars tvs - using all conceivable links from pred - -E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} -Then grow precs tvs = {a,b,c} - -All the type variables from an implicit parameter are added, whether or -not they are mentioned in tvs; see Note [Implicit parameters and ambiguity] -in TcSimplify. - -See also Note [Ambiguity] in TcSimplify - -\begin{code} -grow :: [PredType] -> TyVarSet -> TyVarSet -grow preds fixed_tvs - | null preds = fixed_tvs - | otherwise = loop real_fixed_tvs - where - -- Add the implicit parameters; - -- see Note [Implicit parameters and ambiguity] in TcSimplify - real_fixed_tvs = foldr unionVarSet fixed_tvs ip_tvs - - loop fixed_tvs - | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs - | otherwise = loop new_fixed_tvs - where - new_fixed_tvs = foldl extend fixed_tvs non_ip_tvs - - extend fixed_tvs pred_tvs - | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs - | otherwise = fixed_tvs - - (ip_tvs, non_ip_tvs) = partitionWith get_ip preds - get_ip (IParam _ ty) = Left (tyVarsOfType ty) - get_ip other = Right (tyVarsOfPred other) -\end{code} %************************************************************************ %* * -- 1.7.10.4