The final batch of changes for the new coercion representation
[ghc-hetmet.git] / compiler / types / FunDeps.lhs
index 665f231..f1c9347 100644 (file)
@@ -9,8 +9,9 @@ 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,
+        FDEq (..),
+       Equation(..), pprEquation,
+       oclose, improveFromInstEnv, improveFromAnother,
        checkInstCoverage, checkFunDeps,
        pprFundeps
     ) where
@@ -20,13 +21,16 @@ module FunDeps (
 import Name
 import Var
 import Class
-import TcGadt
 import TcType
+import Unify
 import InstEnv
 import VarSet
 import VarEnv
 import Outputable
 import Util
+import FastString
+
+import Data.List       ( nubBy )
 import Data.Maybe      ( isJust )
 \end{code}
 
@@ -37,6 +41,26 @@ import Data.Maybe    ( isJust )
 %*                                                                     *
 %************************************************************************
 
+  oclose(vs,C) The result of extending the set of tyvars vs
+               using the functional dependencies from C
+
+  grow(vs,C)   The result of extend the set of tyvars vs
+               using all conceivable links from C.
+
+               E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
+               Then grow(vs,C) = {a,b,c}
+
+               Note that grow(vs,C) `superset` grow(vs,simplify(C))
+               That is, simplfication can only shrink the result of grow.
+
+Notice that
+   oclose is conservative      v `elem` oclose(vs,C)
+          one way:                      => v is definitely fixed by vs
+
+   grow is conservative                if v might be fixed by vs 
+          the other way:       => v `elem` grow(vs,C)
+
+----------------------------------------------------------
 (oclose preds tvs) closes the set of type variables tvs, 
 wrt functional dependencies in preds.  The result is a superset
 of the argument set.  For example, if we have
@@ -45,60 +69,47 @@ then
        oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
 because if we know x and y then that fixes z.
 
-Using oclose
-~~~~~~~~~~~~
-oclose is used
-
-a) When determining ambiguity.  The type
-       forall a,b. C a b => a
-is not ambiguous (given the above class decl for C) because
-a determines b.  
-
-b) When generalising a type T.  Usually we take FV(T) \ FV(Env),
-but in fact we need
-       FV(T) \ (FV(Env)+)
-where the '+' is the oclosure operation.  Notice that we do not 
-take FV(T)+.  This puzzled me for a bit.  Consider
-
-       f = E
-
-and suppose e have that E :: C a b => a, and suppose that b is
-free in the environment. Then we quantify over 'a' only, giving
-the type forall a. C a b => a.  Since a->b but we don't have b->a,
-we might have instance decls like
-       instance C Bool Int where ...
-       instance C Char Int where ...
-so knowing that b=Int doesn't fix 'a'; so we quantify over it.
-
-               ---------------
-               A WORRY: ToDo!
-               ---------------
-If we have     class C a b => D a b where ....
-               class D a b | a -> b where ...
-and the preds are [C (x,y) z], then we want to see the fd in D,
-even though it is not explicit in C, giving [({x,y},{z})]
-
-Similarly for instance decls?  E.g. Suppose we have
-       instance C a b => Eq (T a b) where ...
-and we infer a type t with constraints Eq (T a b) for a particular
-expression, and suppose that 'a' is free in the environment.  
-We could generalise to
-       forall b. Eq (T a b) => t
-but if we reduced the constraint, to C a b, we'd see that 'a' determines
-b, so that a better type might be
-       t (with free constraint C a b) 
-Perhaps it doesn't matter, because we'll still force b to be a
-particular type at the call sites.  Generalising over too many
-variables (provided we don't shadow anything by quantifying over a
-variable that is actually free in the envt) may postpone errors; it
-won't hide them altogether.
-
+oclose is used (only) when generalising a type T; see extensive
+notes in TcSimplify.
+
+Note [Important subtlety in oclose]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (oclose (C Int t) {}), where class C a b | a->b
+Then, since a->b, 't' is fully determined by Int, and the
+uniform thing is to return {t}.
+
+However, consider
+       class D a b c | b->c
+       f x = e   -- 'e' generates constraint (D s Int t)
+                 -- \x.e has type s->s
+Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
+monomorphic in 't', thus
+       f :: forall s. D s Int t => s -> s
+
+But if this function is never called, 't' will never be instantiated;
+the functional dependencies that fix 't' may well be instance decls in
+some importing module.  But the top-level defaulting of unconstrained
+type variables will fix t=GHC.Prim.Any, and that's simply a bug.
+
+Conclusion: oclose only returns a type variable as "fixed" if it 
+depends on at least one type variable in the input fixed_tvs.
+
+Remember, it's always sound for oclose to return a smaller set.
+An interesting example is tcfail093, where we get this inferred type:
+    class C a b | a->b
+    dup :: forall h. (Call (IO Int) h) => () -> Int -> h
+This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
+previously GHC rejected this saying 'no instance for Call (IO Int) h'.
+But it's right on the borderline. If there was an extra, otherwise
+uninvolved type variable, like 's' in the type of 'f' above, then
+we must accept the function.  So, for now anyway, we accept 'dup' too.
 
 \begin{code}
 oclose :: [PredType] -> TyVarSet -> TyVarSet
 oclose preds fixed_tvs
-  | null tv_fds = fixed_tvs    -- Fast escape hatch for common case
-  | otherwise   = loop fixed_tvs
+  | null tv_fds            = fixed_tvs    -- Fast escape hatch for common case
+  | isEmptyVarSet fixed_tvs = emptyVarSet  -- Note [Important subtlety in oclose]
+  | otherwise              = loop fixed_tvs
   where
     loop fixed_tvs
        | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
@@ -106,8 +117,10 @@ oclose preds 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
+    extend fixed_tvs (ls,rs) 
+       | not (isEmptyVarSet ls)        -- Note [Important subtlety in oclose]
+       , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
+       | otherwise                = fixed_tvs
 
     tv_fds  :: [(TyVarSet,TyVarSet)]
        -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
@@ -120,44 +133,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 = real_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}
     
 %************************************************************************
 %*                                                                     *
@@ -166,31 +141,67 @@ grow preds fixed_tvs
 %************************************************************************
 
 
+Each functional dependency with one variable in the RHS is responsible
+for generating a single equality. For instance:
+     class C a b | a -> b
+The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha 
+     FDEq { fd_pos      = 1
+          , fd_ty_left  = Bool 
+          , fd_ty_right = alpha }
+However notice that a functional dependency may have more than one variable
+in the RHS which will create more than one FDEq. Example: 
+     class C a b c | a -> b c 
+     [Wanted] C Int alpha alpha 
+     [Wanted] C Int Bool beta 
+Will generate: 
+        fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
+        fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
+
+We record the paremeter position so that can immediately rewrite a constraint
+using the produced FDEqs and remove it from our worklist.
+
+
+INVARIANT: Corresponding types aren't already equal 
+That is, there exists at least one non-identity equality in FDEqs. 
+
+Assume:
+       class C a b c | a -> b c
+       instance C Int x x
+And:   [Wanted] C Int Bool alpha
+We will /match/ the LHS of fundep equations, producing a matching substitution
+and create equations for the RHS sides. In our last example we'd have generated:
+      ({x}, [fd1,fd2])
+where 
+       fd1 = FDEq 1 Bool x
+       fd2 = FDEq 2 alpha x
+To ``execute'' the equation, make fresh type variable for each tyvar in the set,
+instantiate the two types with these fresh variables, and then unify or generate 
+a new constraint. In the above example we would generate a new unification 
+variable 'beta' for x and produce the following constraints:
+     [Wanted] (Bool ~ beta)
+     [Wanted] (alpha ~ beta)
+
+Notice the subtle difference between the above class declaration and:
+       class C a b c | a -> b, a -> c 
+where we would generate: 
+      ({x},[fd1]),({x},[fd2]) 
+This means that the template variable would be instantiated to different 
+unification variables when producing the FD constraints. 
+
+Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
+
 \begin{code}
-type Equation = (TyVarSet, [(Type, Type)])
--- These pairs of types should be equal, for some
--- substitution of the tyvars in the tyvar set
--- INVARIANT: corresponding types aren't already equal
-
--- It's important that we have a *list* of pairs of types.  Consider
---     class C a b c | a -> b c where ...
---     instance C Int x x where ...
--- Then, given the constraint (C Int Bool v) we should improve v to Bool,
--- via the equation ({x}, [(Bool,x), (v,x)])
--- This would not happen if the class had looked like
---     class C a b c | a -> b, a -> c
-
--- To "execute" the equation, make fresh type variable for each tyvar in the set,
--- instantiate the two types with these fresh variables, and then unify.
---
--- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
--- We unify z with Int, but since a and b are quantified we do nothing to them
--- We usually act on an equation by instantiating the quantified type varaibles
--- to fresh type variables, and then calling the standard unifier.
-
-pprEquation (qtvs, pairs) 
-  = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
-         nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])]
+type Pred_Loc = (PredType, SDoc)       -- SDoc says where the Pred comes from
+
+data Equation 
+   = FDEqn { fd_qtvs :: TyVarSet               -- Instantiate these to fresh unification vars
+           , fd_eqs  :: [FDEq]                 --   and then make these equal
+           , fd_pred1, fd_pred2 :: Pred_Loc }  -- The Equation arose from
+                                               -- combining these two constraints
+
+data FDEq = FDEq { fd_pos      :: Int -- We use '0' for the first position
+                 , fd_ty_left  :: Type
+                 , fd_ty_right :: Type }
 \end{code}
 
 Given a bunch of predicates that must hold, such as
@@ -223,72 +234,97 @@ NOTA BENE:
 
 
 \begin{code}
-type Pred_Loc = (PredType, SDoc)       -- SDoc says where the Pred comes from
+instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)]) 
+-- Returns a FunDep between the types accompanied along with their 
+-- position (<=0) in the types argument list.
+instFD_WithPos (ls,rs) tvs tys
+  = (map (snd . lookup) ls, map lookup rs)
+  where
+    ind_tys   = zip [0..] tys 
+    env       = zipVarEnv tvs ind_tys
+    lookup tv = lookupVarEnv_NF env tv
 
-improveOne :: (Class -> [Instance])            -- Gives instances for given class
-          -> Pred_Loc                          -- Do improvement triggered by this
-          -> [Pred_Loc]                        -- Current constraints 
-          -> [(Equation,Pred_Loc,Pred_Loc)]    -- Derived equalities that must also hold
-                                               -- (NB the above INVARIANT for type Equation)
-                                               -- The Pred_Locs explain which two predicates were
-                                               -- combined (for error messages)
--- Just do improvement triggered by a single, distinguised predicate
-
-improveOne inst_env pred@(IParam ip ty, _) preds
-  = [ ((emptyVarSet, [(ty,ty2)]), pred, p2) 
-    | p2@(IParam ip2 ty2, _) <- preds
-    , ip==ip2
-    , not (ty `tcEqType` ty2)]
-
-improveOne inst_env pred@(ClassP cls tys, _) preds
+zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
+                   -> [Type] 
+                   -> [(Int,Type)] 
+                   -> [FDEq]
+-- Create a list of FDEqs from two lists of types, making sure
+-- that the types are not equal.
+zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
+ | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
+ | otherwise = FDEq { fd_pos      = i2
+                    , fd_ty_left  = ty1
+                    , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
+zipAndComputeFDEqs _ _ _ = [] 
+
+-- Improve a class constraint from another class constraint
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+improveFromAnother :: Pred_Loc -- Template item (usually given, or inert) 
+                   -> Pred_Loc -- Workitem [that can be improved]
+                   -> [Equation]
+-- Post: FDEqs always oriented from the other to the workitem 
+--       Equations have empty quantified variables 
+improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
+  | tys1 `lengthAtLeast` 2 && cls1 == cls2
+  = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
+    | let (cls_tvs, cls_fds) = classTvsFds cls1
+    , fd <- cls_fds
+    , let (ltys1, rs1)  = instFD         fd cls_tvs tys1
+          (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
+    , eqTypes ltys1 ltys2              -- The LHSs match
+    , let eqs = zipAndComputeFDEqs eqType rs1 irs2
+    , not (null eqs) ]
+
+improveFromAnother _ _ = []
+
+
+-- Improve a class constraint from instance declarations
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+pprEquation :: Equation -> SDoc
+pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs }) 
+  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
+         nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
+
+improveFromInstEnv :: (InstEnv,InstEnv)
+                   -> Pred_Loc
+                   -> [Equation] -- Needs to be an Equation because
+                                 -- of quantified variables
+-- Post: Equations oriented from the template (matching instance) to the workitem!
+improveFromInstEnv _inst_env (pred,_loc)
+  | not (isClassPred pred)
+  = panic "improveFromInstEnv: not a class predicate"
+improveFromInstEnv inst_env pred@(ClassP cls tys, _)
   | tys `lengthAtLeast` 2
-  = instance_eqns ++ pairwise_eqns
-       -- NB: we put the instance equations first.   This biases the 
-       -- order so that we first improve individual constraints against the
-       -- instances (which are perhaps in a library and less likely to be
-       -- wrong; and THEN perform the pairwise checks.
-       -- The other way round, it's possible for the pairwise check to succeed
-       -- and cause a subsequent, misleading failure of one of the pair with an
-       -- instance declaration.  See tcfail143.hs for an example
-  where
-    (cls_tvs, cls_fds) = classTvsFds cls
-    instances         = inst_env cls
-    rough_tcs         = roughMatchTcs tys
-
-       -- NOTE that we iterate over the fds first; they are typically
-       -- empty, which aborts the rest of the loop.
-    pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
-    pairwise_eqns      -- This group comes from pairwise comparison
-      = [ (eqn, pred, p2)
-       | fd <- cls_fds
-       , p2@(ClassP cls2 tys2, _) <- preds
-       , cls == cls2
-       , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
-       ]
-
-    instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
-    instance_eqns      -- This group comes from comparing with instance decls
-      = [ (eqn, p_inst, pred)
-       | fd <- cls_fds         -- Iterate through the fundeps first, 
+  = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
+    | fd <- cls_fds            -- Iterate through the fundeps first,
                                -- because there often are none!
-       , let rough_fd_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
-       , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, 
-                           is_tcs = mb_tcs_inst }) <- instances
-       , not (instanceCantMatch mb_tcs_inst rough_fd_tcs)
-       , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
-       , let p_inst = (mkClassPred cls tys_inst, 
-                       ptext SLIT("arising from the instance declaration at")
-                       <+> ppr (getSrcLoc ispec))
-       ]
-
-improveOne inst_env eq_pred preds
-  = []
+    , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
+               -- Trim the rough_tcs based on the head of the fundep.
+               -- Remember that instanceCantMatch treats both argumnents
+               -- symmetrically, so it's ok to trim the rough_tcs,
+               -- rather than trimming each inst_tcs in turn
+    , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
+                       is_tcs = inst_tcs }) <- instances
+    , not (instanceCantMatch inst_tcs trimmed_tcs)
+    , let p_inst = (mkClassPred cls tys_inst,
+                   sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)  
+                       , ptext (sLit "in the instance declaration at")
+                                   <+> ppr (getSrcLoc ispec)])
+    , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
+    , not (null eqs)
+    ]
+  where 
+     (cls_tvs, cls_fds) = classTvsFds cls
+     instances          = classInstances inst_env cls
+     rough_tcs          = roughMatchTcs tys
+improveFromInstEnv _ _ = []
 
 
 checkClsFD :: TyVarSet                         -- Quantified type variables; see note below
           -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
           -> [Type] -> [Type]
-          -> [Equation]
+          -> [(TyVarSet, [FDEq])]
 
 checkClsFD qtvs fd clas_tvs tys1 tys2
 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 
@@ -303,7 +339,7 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
 --                 tys2 = [Maybe t1, t2]
 --
 -- We can instantiate x to t1, and then we want to force
---     (Tree x) [t1/x]  :=:   t2
+--     (Tree x) [t1/x]  ~   t2
 --
 -- This function is also used when matching two Insts (rather than an Inst
 -- against an instance decl. In that case, qtvs is empty, and we are doing
@@ -317,52 +353,69 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
             length tys1 == length clas_tvs 
            , ppr tys1 <+> ppr tys2 )
 
-    case tcUnifyTys bind_fn ls1 ls2 of
+    case tcUnifyTys bind_fn ltys1 ltys2 of
        Nothing  -> []
-       Just subst | isJust (tcUnifyTys bind_fn rs1' rs2') 
-                       -- Don't include any equations that already hold. 
+       Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
+                       -- Don't include any equations that already hold.
                        -- Reason: then we know if any actual improvement has happened,
                        --         in which case we need to iterate the solver
-                       -- In making this check we must taking account of the fact that any 
-                       -- qtvs that aren't already instantiated can be instantiated to anything 
+                       -- In making this check we must taking account of the fact that any
+                       -- qtvs that aren't already instantiated can be instantiated to anything
                        -- at all
-                 -> []
-
-                 | otherwise   -- Aha!  A useful equation
-                 -> [ (qtvs', zip rs1' rs2')]
+                        -- NB: We can't do this 'is-useful-equation' check element-wise 
+                        --     because of:
+                        --           class C a b c | a -> b c
+                        --           instance C Int x x
+                        --           [Wanted] C Int alpha Int
+                        -- We would get that  x -> alpha  (isJust) and x -> Int (isJust)
+                        -- so we would produce no FDs, which is clearly wrong. 
+                  -> [] 
+
+                  | otherwise
+                  -> [(qtvs', fdeqs)]
                        -- We could avoid this substTy stuff by producing the eqn
                        -- (qtvs, ls1++rs1, ls2++rs2)
                        -- which will re-do the ls1/ls2 unification when the equation is
                        -- executed.  What we're doing instead is recording the partial
                        -- work of the ls1/ls2 unification leaving a smaller unification problem
-                 where
-                   rs1'  = substTys subst rs1 
-                   rs2'  = substTys subst rs2
+                 where
+                    rtys1' = map (substTy subst) rtys1
+                    irs2'  = map (\(i,x) -> (i,substTy subst x)) irs2
+                    rtys2' = map snd irs2'
+                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
+                        -- Don't discard anything! 
+                        -- We could discard equal types but it's an overkill to call 
+                        -- eqType again, since we know for sure that /at least one/ 
+                        -- equation in there is useful)
+
                    qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
-                       -- qtvs' are the quantified type variables
-                       -- that have not been substituted out
-                       --      
-                       -- Eg.  class C a b | a -> b
-                       --      instance C Int [y]
-                       -- Given constraint C Int z
-                       -- we generate the equation
-                       --      ({y}, [y], z)
+                       -- qtvs' are the quantified type variables
+                       -- that have not been substituted out
+                       --      
+                       -- Eg.  class C a b | a -> b
+                       --      instance C Int [y]
+                       -- Given constraint C Int z
+                       -- we generate the equation
+                       --      ({y}, [y], z)
   where
     bind_fn tv | tv `elemVarSet` qtvs = BindMe
               | otherwise            = Skolem
 
-    (ls1, rs1) = instFD fd clas_tvs tys1
-    (ls2, rs2) = instFD fd clas_tvs tys2
+    (ltys1, rtys1) = instFD         fd clas_tvs tys1
+    (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys2
+\end{code}
+
 
+\begin{code}
 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
+-- A simpler version of instFD_WithPos to be used in checking instance coverage etc.
 instFD (ls,rs) tvs tys
   = (map lookup ls, map lookup rs)
   where
     env       = zipVarEnv tvs tys
     lookup tv = lookupVarEnv_NF env tv
-\end{code}
 
-\begin{code}
 checkInstCoverage :: Class -> [Type] -> Bool
 -- Check that the Coverage Condition is obeyed in an instance decl
 -- For example, if we have 
@@ -453,32 +506,40 @@ badFunDeps :: [Instance] -> Class
           -> TyVarSet -> [Type]        -- Proposed new instance type
           -> [Instance]
 badFunDeps cls_insts clas ins_tv_set ins_tys 
-  = [ ispec | fd <- fds,       -- fds is often empty
+  = nubBy eq_inst $
+    [ ispec | fd <- fds,       -- fds is often empty, so do this first!
              let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
-             ispec@(Instance { is_tcs = mb_tcs, is_tvs = tvs, 
+             ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs, 
                                is_tys = tys }) <- cls_insts,
                -- Filter out ones that can't possibly match, 
                -- based on the head of the fundep
-             not (instanceCantMatch trimmed_tcs mb_tcs),       
+             not (instanceCantMatch inst_tcs trimmed_tcs),     
              notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) 
                                   fd clas_tvs tys ins_tys)
     ]
   where
     (clas_tvs, fds) = classTvsFds clas
     rough_tcs = roughMatchTcs ins_tys
+    eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
+       -- An single instance may appear twice in the un-nubbed conflict list
+       -- because it may conflict with more than one fundep.  E.g.
+       --      class C a b c | a -> b, a -> c
+       --      instance C Int Bool Bool
+       --      instance C Int Char Char
+       -- The second instance conflicts with the first by *both* fundeps
 
 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
 -- Computing rough_tcs for a particular fundep
---     class C a b c | a c -> b where ... 
+--     class C a b c | a -> b where ...
 -- For each instance .... => C ta tb tc
--- we want to match only on the types ta, tb; so our
+-- we want to match only on the type ta; so our
 -- rough-match thing must similarly be filtered.  
--- Hence, we Nothing-ise the tb type right here
-trimRoughMatchTcs clas_tvs (ltvs,_) mb_tcs
+-- Hence, we Nothing-ise the tb and tc types right here
+trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
   = zipWith select clas_tvs mb_tcs
   where
     select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
-                        | otherwise           = Nothing
+                         | otherwise           = Nothing
 \end{code}