Fix Trac #3017: ensure that we quantify over enough type variables when equalities...
authorsimonpj@microsoft.com <unknown>
Wed, 11 Feb 2009 17:47:33 +0000 (17:47 +0000)
committersimonpj@microsoft.com <unknown>
Wed, 11 Feb 2009 17:47:33 +0000 (17:47 +0000)
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
compiler/typecheck/Inst.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/types/FunDeps.lhs

index 67a3dbf..6f03aad 100644 (file)
@@ -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}
index b5eeff0..8a014bc 100644 (file)
@@ -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
index 47592f5..9a17b0f 100644 (file)
@@ -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
index 071d4c0..0e1e5b0 100644 (file)
@@ -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
 
index 1a9e054..158eb64 100644 (file)
@@ -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)
 
index af7cfec..02b0a2a 100644 (file)
@@ -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}
     
 %************************************************************************
 %*                                                                     *