[commit: ghc] master: Use a version of the coverage condition even with UndecidableInstances. (fe61599)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

[commit: ghc] master: Use a version of the coverage condition even with UndecidableInstances. (fe61599)

Simon Peyton Jones
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