2 files changed, 71 insertions, 2 deletions

diff --git a/compiler/typecheck/TcValidity.lhs b/compiler/typecheck/TcValidity.lhs
index 80e7aa0415..44d7d4c6db 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 09d0be07bb..6bca407c67 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]