OK. I see that * oclose is never used * Note [Important subtlety in oclose] is out of date; it relates to when oclose was used with the global tyvars. This relates to change (1) of yours, behaving uniformly when the fixed tyvars are empty. So I nuked oclose altogether (hurrah), and renamed oclose1 to oclose. I'm happy with (2) using equalities. I'll commit these simplifications shortly. Simon | -----Original Message----- | From: ghc-commits-bounces@haskell.org [mailto:ghc-commits- | bounces@haskell.org] On Behalf Of Iavor Diatchki | Sent: 14 January 2013 00:30 | To: ghc-commits@haskell.org | Subject: [commit: ghc] master: Use a version of the coverage condition | even with UndecidableInstances. (fe61599) | | Repository : ssh://darcs.haskell.org//srv/darcs/ghc | | On branch : master | | http://hackage.haskell.org/trac/ghc/changeset/fe61599ffebb27924c4beef47b | 6237542644f3f4 | | >--------------------------------------------------------------- | | commit fe61599ffebb27924c4beef47b6237542644f3f4 | Author: Iavor S. Diatchki | Date: Sun Jan 13 16:29:10 2013 -0800 | | Use a version of the coverage condition even with | UndecidableInstances. | | This fixes bug #1241 and #2247. When UndecidableInstances are on, | we use the "Liberal Coverage Condition", which is what GHC used to | do in | the past. This is the gist of the check: | | class C a b | a -> b | instance theta => C t1 t2 | | we check that `fvs t2` is a subset of `fd-closure(theta,fvs t1)`. | | This is strictly more general than the coverage condition, while | it still guarantees consistency with the FDs of the class. This | check is completely orthogonal to termination (it by no means | guarantees | it). | | I am not sure of the role of the "coverage condition" in | termination--- | the comments suggest that it is important. This is why, for the | moment, | we only use this check when UndecidableInstances are on. | | >--------------------------------------------------------------- | | compiler/typecheck/TcValidity.lhs | 8 ++++- | compiler/types/FunDeps.lhs | 65 | ++++++++++++++++++++++++++++++++++++- | 2 files changed, 71 insertions(+), 2 deletions(-) | | diff --git a/compiler/typecheck/TcValidity.lhs | b/compiler/typecheck/TcValidity.lhs | index 80e7aa0..44d7d4c 100644 | --- a/compiler/typecheck/TcValidity.lhs | +++ b/compiler/typecheck/TcValidity.lhs | @@ -827,7 +827,9 @@ checkValidInstance ctxt hs_type ty | -- in the constraint than in the head | ; undecidable_ok <- xoptM Opt_UndecidableInstances | ; if undecidable_ok | - then checkAmbiguity ctxt ty | + then do checkAmbiguity ctxt ty | + checkTc (checkInstLiberalCoverage clas theta | inst_tys) | + (instTypeErr clas inst_tys liberal_msg) | else do { checkInstTermination inst_tys theta | ; checkTc (checkInstCoverage clas inst_tys) | (instTypeErr clas inst_tys msg) } @@ -837,6 | +839,10 @@ checkValidInstance ctxt hs_type ty | msg = parens (vcat [ptext (sLit "the Coverage Condition fails for | one of the functional dependencies;"), | undecidableMsg]) | | + liberal_msg = vcat | + [ ptext $ sLit "Multiple uses of this instance may be | inconsistent" | + , ptext $ sLit "with the functional dependencies of the class." | + ] | -- The location of the "head" of the instance | head_loc = case hs_type of | L _ (HsForAllTy _ _ _ (L loc _)) -> loc diff --git | a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs index | 09d0be0..6bca407 100644 | --- a/compiler/types/FunDeps.lhs | +++ b/compiler/types/FunDeps.lhs | @@ -19,7 +19,7 @@ module FunDeps ( | FDEq (..), | Equation(..), pprEquation, | oclose, improveFromInstEnv, improveFromAnother, | - checkInstCoverage, checkFunDeps, | + checkInstCoverage, checkInstLiberalCoverage, checkFunDeps, | pprFundeps | ) where | | @@ -145,6 +145,52 @@ oclose preds fixed_tvs | ClassPred cls tys -> [(cls, tys)] | TuplePred ts -> concatMap classesOfPredTy ts | _ -> [] | + | +-- An alternative implementation of `oclose`. Differences: | +-- 1. The empty set of variables is allowed to determine stuff, | +-- 2. We also use equality predicates as FDs. | +-- | +-- I (Iavor) believe that this is the correct implementation of oclose. | +-- For 1: the above argument about `t` being monomorphic seems | incorrect. | +-- The correct behavior is to quantify over `t`, even though we know | that | +-- it may be instantiated to at most one type. The point is that we | might | +-- only find out what that type is later, at the class site to the | function. | +-- In genral, we should be quantifying all variables that are not | mentioned | +-- in the environment + the variables that are determined by them. | +-- For 2: This is just a nicity, but it makes things a bit more | general: | +-- if we have an assumption `t1 ~ t2`, then we use the fact that if | we know | +-- `t1` we also know `t2` and the other way. | + | +oclose1 :: [PredType] -> TyVarSet -> TyVarSet | +oclose1 preds fixed_tvs | + | null tv_fds = fixed_tvs -- Fast escape hatch for common case. | + | otherwise = loop fixed_tvs | + where | + loop fixed_tvs | + | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs | + | otherwise = loop new_fixed_tvs | + where new_fixed_tvs = foldl extend fixed_tvs tv_fds | + | + extend fixed_tvs (ls,rs) | + | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs | + | otherwise = fixed_tvs | + | + tv_fds :: [(TyVarSet,TyVarSet)] | + tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys) | + | (xs, ys) <- concatMap deterimned preds | + ] | + | + deterimned :: PredType -> [([Type],[Type])] | + deterimned pred | + = case classifyPredType pred of | + ClassPred cls tys -> | + do let (cls_tvs, cls_fds) = classTvsFds cls | + fd <- cls_fds | + return (instFD fd cls_tvs tys) | + EqPred t1 t2 -> [([t1],[t2]), ([t2],[t1])] | + TuplePred ts -> concatMap deterimned ts | + _ -> [] | + | \end{code} | | | @@ -471,6 +517,23 @@ checkInstCoverage clas inst_taus | fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls | where | (ls,rs) = instFD fd tyvars inst_taus | + | +checkInstLiberalCoverage :: Class -> [PredType] -> [Type] -> Bool | +-- Check that the Liberal Coverage Condition is obeyed in an instance | +decl | +-- For example, if we have: | +-- class C a b | a -> b | +-- instance theta => C t1 t2 | +-- Then we require fv(t2) `subset` oclose(fv(t1), theta) | +-- This ensures the self-consistency of the instance, but | +-- it does not guarantee termination. | +-- See Note [Coverage Condition] below | + | +checkInstLiberalCoverage clas theta inst_taus | + = all fundep_ok fds | + where | + (tyvars, fds) = classTvsFds clas | + fundep_ok fd = tyVarsOfTypes rs `subVarSet` oclose1 theta | (tyVarsOfTypes ls) | + where (ls,rs) = instFD fd tyvars inst_taus | \end{code} | | Note [Coverage condition] | | | | _______________________________________________ | ghc-commits mailing list | ghc-commits@haskell.org | http://www.haskell.org/mailman/listinfo/ghc-commits