[commit: ghc] master: Use a version of the coverage condition even with UndecidableInstances. (fe61599)
Simon Peyton-Jones
simonpj at microsoft.com
Tue Jan 15 14:12:06 CET 2013
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 at haskell.org [mailto:ghc-commits-
| bounces at haskell.org] On Behalf Of Iavor Diatchki
| Sent: 14 January 2013 00:30
| To: ghc-commits at 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 <iavor.diatchki at gmail.com>
| 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/ghc-commits
More information about the ghc-devs
mailing list