Comments only
[ghc.git] / compiler / typecheck / FunDeps.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 2000
4
5
6 FunDeps - functional dependencies
7
8 It's better to read it as: "if we know these, then we're going to know these"
9 -}
10
11 {-# LANGUAGE CPP #-}
12
13 module FunDeps (
14 FunDepEqn(..), pprEquation,
15 improveFromInstEnv, improveFromAnother,
16 checkInstCoverage, checkFunDeps,
17 pprFundeps
18 ) where
19
20 #include "HsVersions.h"
21
22 import Name
23 import Var
24 import Class
25 import Type
26 import TcType( immSuperClasses )
27 import Unify
28 import InstEnv
29 import VarSet
30 import VarEnv
31 import Outputable
32 import ErrUtils( Validity(..), allValid )
33 import SrcLoc
34 import Util
35 import FastString
36
37 import Pair ( Pair(..) )
38 import Data.List ( nubBy )
39 import Data.Maybe ( isJust )
40
41 {-
42 ************************************************************************
43 * *
44 \subsection{Generate equations from functional dependencies}
45 * *
46 ************************************************************************
47
48
49 Each functional dependency with one variable in the RHS is responsible
50 for generating a single equality. For instance:
51 class C a b | a -> b
52 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
53 will generate the folloing FunDepEqn
54 FDEqn { fd_qtvs = []
55 , fd_eqs = [Pair Bool alpha]
56 , fd_pred1 = C Int Bool
57 , fd_pred2 = C Int alpha
58 , fd_loc = ... }
59 However notice that a functional dependency may have more than one variable
60 in the RHS which will create more than one pair of types in fd_eqs. Example:
61 class C a b c | a -> b c
62 [Wanted] C Int alpha alpha
63 [Wanted] C Int Bool beta
64 Will generate:
65 FDEqn { fd_qtvs = []
66 , fd_eqs = [Pair Bool alpha, Pair alpha beta]
67 , fd_pred1 = C Int Bool
68 , fd_pred2 = C Int alpha
69 , fd_loc = ... }
70
71 INVARIANT: Corresponding types aren't already equal
72 That is, there exists at least one non-identity equality in FDEqs.
73
74 Assume:
75 class C a b c | a -> b c
76 instance C Int x x
77 And: [Wanted] C Int Bool alpha
78 We will /match/ the LHS of fundep equations, producing a matching substitution
79 and create equations for the RHS sides. In our last example we'd have generated:
80 ({x}, [fd1,fd2])
81 where
82 fd1 = FDEq 1 Bool x
83 fd2 = FDEq 2 alpha x
84 To ``execute'' the equation, make fresh type variable for each tyvar in the set,
85 instantiate the two types with these fresh variables, and then unify or generate
86 a new constraint. In the above example we would generate a new unification
87 variable 'beta' for x and produce the following constraints:
88 [Wanted] (Bool ~ beta)
89 [Wanted] (alpha ~ beta)
90
91 Notice the subtle difference between the above class declaration and:
92 class C a b c | a -> b, a -> c
93 where we would generate:
94 ({x},[fd1]),({x},[fd2])
95 This means that the template variable would be instantiated to different
96 unification variables when producing the FD constraints.
97
98 Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
99 -}
100
101 data FunDepEqn loc
102 = FDEqn { fd_qtvs :: [TyVar] -- Instantiate these type and kind vars
103 -- to fresh unification vars,
104 -- Non-empty only for FunDepEqns arising from instance decls
105
106 , fd_eqs :: [Pair Type] -- Make these pairs of types equal
107 , fd_pred1 :: PredType -- The FunDepEqn arose from
108 , fd_pred2 :: PredType -- combining these two constraints
109 , fd_loc :: loc }
110
111 {-
112 Given a bunch of predicates that must hold, such as
113
114 C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
115
116 improve figures out what extra equations must hold.
117 For example, if we have
118
119 class C a b | a->b where ...
120
121 then improve will return
122
123 [(t1,t2), (t4,t5)]
124
125 NOTA BENE:
126
127 * improve does not iterate. It's possible that when we make
128 t1=t2, for example, that will in turn trigger a new equation.
129 This would happen if we also had
130 C t1 t7, C t2 t8
131 If t1=t2, we also get t7=t8.
132
133 improve does *not* do this extra step. It relies on the caller
134 doing so.
135
136 * The equations unify types that are not already equal. So there
137 is no effect iff the result of improve is empty
138 -}
139
140 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
141 -- (instFD fd tvs tys) returns fd instantiated with (tvs -> tys)
142 instFD (ls,rs) tvs tys
143 = (map lookup ls, map lookup rs)
144 where
145 env = zipVarEnv tvs tys
146 lookup tv = lookupVarEnv_NF env tv
147
148 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
149 -> [Type] -> [Type]
150 -> [Pair Type]
151 -- Create a list of (Type,Type) pairs from two lists of types,
152 -- making sure that the types are not already equal
153 zipAndComputeFDEqs discard (ty1:tys1) (ty2:tys2)
154 | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
155 | otherwise = Pair ty1 ty2 : zipAndComputeFDEqs discard tys1 tys2
156 zipAndComputeFDEqs _ _ _ = []
157
158 -- Improve a class constraint from another class constraint
159 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
160 improveFromAnother :: loc
161 -> PredType -- Template item (usually given, or inert)
162 -> PredType -- Workitem [that can be improved]
163 -> [FunDepEqn loc]
164 -- Post: FDEqs always oriented from the other to the workitem
165 -- Equations have empty quantified variables
166 improveFromAnother loc pred1 pred2
167 | Just (cls1, tys1) <- getClassPredTys_maybe pred1
168 , Just (cls2, tys2) <- getClassPredTys_maybe pred2
169 , tys1 `lengthAtLeast` 2 && cls1 == cls2
170 = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
171 | let (cls_tvs, cls_fds) = classTvsFds cls1
172 , fd <- cls_fds
173 , let (ltys1, rs1) = instFD fd cls_tvs tys1
174 (ltys2, rs2) = instFD fd cls_tvs tys2
175 , eqTypes ltys1 ltys2 -- The LHSs match
176 , let eqs = zipAndComputeFDEqs eqType rs1 rs2
177 , not (null eqs) ]
178
179 improveFromAnother _ _ _ = []
180
181
182 -- Improve a class constraint from instance declarations
183 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
184
185 pprEquation :: FunDepEqn a -> SDoc
186 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
187 = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
188 nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2
189 | Pair t1 t2 <- pairs])]
190
191 improveFromInstEnv :: InstEnvs
192 -> (PredType -> SrcSpan -> loc)
193 -> PredType
194 -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
195 -- of quantified variables
196 -- Post: Equations oriented from the template (matching instance) to the workitem!
197 improveFromInstEnv _inst_env _ pred
198 | not (isClassPred pred)
199 = panic "improveFromInstEnv: not a class predicate"
200 improveFromInstEnv inst_env mk_loc pred
201 | Just (cls, tys) <- getClassPredTys_maybe pred
202 , tys `lengthAtLeast` 2
203 , let (cls_tvs, cls_fds) = classTvsFds cls
204 instances = classInstances inst_env cls
205 rough_tcs = roughMatchTcs tys
206 = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
207 , fd_pred1 = p_inst, fd_pred2 = pred
208 , fd_loc = mk_loc p_inst (getSrcSpan (is_dfun ispec)) }
209 | fd <- cls_fds -- Iterate through the fundeps first,
210 -- because there often are none!
211 , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
212 -- Trim the rough_tcs based on the head of the fundep.
213 -- Remember that instanceCantMatch treats both argumnents
214 -- symmetrically, so it's ok to trim the rough_tcs,
215 -- rather than trimming each inst_tcs in turn
216 , ispec <- instances
217 , (meta_tvs, eqs) <- checkClsFD fd cls_tvs ispec
218 emptyVarSet tys trimmed_tcs -- NB: orientation
219 , let p_inst = mkClassPred cls (is_tys ispec)
220 ]
221 improveFromInstEnv _ _ _ = []
222
223
224 checkClsFD :: FunDep TyVar -> [TyVar] -- One functional dependency from the class
225 -> ClsInst -- An instance template
226 -> TyVarSet -> [Type] -> [Maybe Name] -- Arguments of this (C tys) predicate
227 -- TyVarSet are extra tyvars that can be instantiated
228 -> [([TyVar], [Pair Type])] -- Empty or singleton
229
230 checkClsFD fd clas_tvs
231 (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
232 extra_qtvs tys_actual rough_tcs_actual
233
234 -- Compare instance {a,b} C sx sp sy sq
235 -- with {c,d,e} C tx tp ty tq
236 -- for fundep (x,y -> p,q) from class (C x p y q)
237 -- If (sx,sy) unifies with (tx,ty), take the subst S
238 --
239
240 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
241 -- to make the types match. For example, given
242 -- class C a b | a->b where ...
243 -- instance C (Maybe x) (Tree x) where ..
244 --
245 -- and an Inst of form (C (Maybe t1) t2),
246 -- then we will call checkClsFD with
247 --
248 -- is_qtvs = {x}, is_tys = [Maybe x, Tree x]
249 -- tys_actual = [Maybe t1, t2]
250 --
251 -- We can instantiate x to t1, and then we want to force
252 -- (Tree x) [t1/x] ~ t2
253 --
254 -- This function is also used when matching two Insts (rather than an Inst
255 -- against an instance decl. In that case, qtvs is empty, and we are doing
256 -- an equality check
257 --
258 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
259 -- For the one-sided matching case, the qtvs are just from the template,
260 -- so we get matching
261
262 | instanceCantMatch rough_tcs_inst rough_tcs_actual
263 = [] -- Filter out ones that can't possibly match,
264
265 | otherwise
266 = ASSERT2( length tys_inst == length tys_actual &&
267 length tys_inst == length clas_tvs
268 , ppr tys_inst <+> ppr tys_actual )
269
270 case tcUnifyTys bind_fn ltys1 ltys2 of
271 Nothing -> []
272 Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
273 -- Don't include any equations that already hold.
274 -- Reason: then we know if any actual improvement has happened,
275 -- in which case we need to iterate the solver
276 -- In making this check we must taking account of the fact that any
277 -- qtvs that aren't already instantiated can be instantiated to anything
278 -- at all
279 -- NB: We can't do this 'is-useful-equation' check element-wise
280 -- because of:
281 -- class C a b c | a -> b c
282 -- instance C Int x x
283 -- [Wanted] C Int alpha Int
284 -- We would get that x -> alpha (isJust) and x -> Int (isJust)
285 -- so we would produce no FDs, which is clearly wrong.
286 -> []
287
288 | null fdeqs
289 -> []
290
291 | otherwise
292 -> [(meta_tvs, fdeqs)]
293 -- We could avoid this substTy stuff by producing the eqn
294 -- (qtvs, ls1++rs1, ls2++rs2)
295 -- which will re-do the ls1/ls2 unification when the equation is
296 -- executed. What we're doing instead is recording the partial
297 -- work of the ls1/ls2 unification leaving a smaller unification problem
298 where
299 rtys1' = map (substTy subst) rtys1
300 rtys2' = map (substTy subst) rtys2
301
302 fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2'
303 -- Don't discard anything!
304 -- We could discard equal types but it's an overkill to call
305 -- eqType again, since we know for sure that /at least one/
306 -- equation in there is useful)
307
308 meta_tvs = [ setVarType tv (substTy subst (varType tv))
309 | tv <- qtvs, tv `notElemTvSubst` subst ]
310 -- meta_tvs are the quantified type variables
311 -- that have not been substituted out
312 --
313 -- Eg. class C a b | a -> b
314 -- instance C Int [y]
315 -- Given constraint C Int z
316 -- we generate the equation
317 -- ({y}, [y], z)
318 --
319 -- But note (a) we get them from the dfun_id, so they are *in order*
320 -- because the kind variables may be mentioned in the
321 -- type variabes' kinds
322 -- (b) we must apply 'subst' to the kinds, in case we have
323 -- matched out a kind variable, but not a type variable
324 -- whose kind mentions that kind variable!
325 -- Trac #6015, #6068
326 where
327 qtv_set = mkVarSet qtvs
328 bind_fn tv | tv `elemVarSet` qtv_set = BindMe
329 | tv `elemVarSet` extra_qtvs = BindMe
330 | otherwise = Skolem
331
332 (ltys1, rtys1) = instFD fd clas_tvs tys_inst
333 (ltys2, rtys2) = instFD fd clas_tvs tys_actual
334
335 {-
336 ************************************************************************
337 * *
338 The Coverage condition for instance declarations
339 * *
340 ************************************************************************
341
342 Note [Coverage condition]
343 ~~~~~~~~~~~~~~~~~~~~~~~~~
344 Example
345 class C a b | a -> b
346 instance theta => C t1 t2
347
348 For the coverage condition, we check
349 (normal) fv(t2) `subset` fv(t1)
350 (liberal) fv(t2) `subset` oclose(fv(t1), theta)
351
352 The liberal version ensures the self-consistency of the instance, but
353 it does not guarantee termination. Example:
354
355 class Mul a b c | a b -> c where
356 (.*.) :: a -> b -> c
357
358 instance Mul Int Int Int where (.*.) = (*)
359 instance Mul Int Float Float where x .*. y = fromIntegral x * y
360 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
361
362 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
363 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
364
365 But it is a mistake to accept the instance because then this defn:
366 f = \ b x y -> if b then x .*. [y] else y
367 makes instance inference go into a loop, because it requires the constraint
368 Mul a [b] b
369 -}
370
371 checkInstCoverage :: Bool -- Be liberal
372 -> Class -> [PredType] -> [Type]
373 -> Validity
374 -- "be_liberal" flag says whether to use "liberal" coverage of
375 -- See Note [Coverage Condition] below
376 --
377 -- Return values
378 -- Nothing => no problems
379 -- Just msg => coverage problem described by msg
380
381 checkInstCoverage be_liberal clas theta inst_taus
382 = allValid (map fundep_ok fds)
383 where
384 (tyvars, fds) = classTvsFds clas
385 fundep_ok fd
386 | isEmptyVarSet undetermined_tvs = IsValid
387 | otherwise = NotValid msg
388 where
389 (ls,rs) = instFD fd tyvars inst_taus
390 ls_tvs = tyVarsOfTypes ls
391 rs_tvs = tyVarsOfTypes rs
392
393 undetermined_tvs | be_liberal = liberal_undet_tvs
394 | otherwise = conserv_undet_tvs
395
396 liberal_undet_tvs = rs_tvs `minusVarSet`oclose theta (closeOverKinds ls_tvs)
397 conserv_undet_tvs = rs_tvs `minusVarSet` closeOverKinds ls_tvs
398 -- closeOverKinds: see Note [Closing over kinds in coverage]
399
400 undet_list = varSetElemsKvsFirst undetermined_tvs
401
402 msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
403 -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
404 -- , text "theta" <+> ppr theta
405 -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
406 -- , text "rs_tvs" <+> ppr rs_tvs
407 sep [ ptext (sLit "The")
408 <+> ppWhen be_liberal (ptext (sLit "liberal"))
409 <+> ptext (sLit "coverage condition fails in class")
410 <+> quotes (ppr clas)
411 , nest 2 $ ptext (sLit "for functional dependency:")
412 <+> quotes (pprFunDep fd) ]
413 , sep [ ptext (sLit "Reason: lhs type")<>plural ls <+> pprQuotedList ls
414 , nest 2 $
415 (if isSingleton ls
416 then ptext (sLit "does not")
417 else ptext (sLit "do not jointly"))
418 <+> ptext (sLit "determine rhs type")<>plural rs
419 <+> pprQuotedList rs ]
420 , ptext (sLit "Un-determined variable") <> plural undet_list <> colon
421 <+> pprWithCommas ppr undet_list
422 , ppWhen (all isKindVar undet_list) $
423 ptext (sLit "(Use -fprint-explicit-kinds to see the kind variables in the types)")
424 , ppWhen (not be_liberal && isEmptyVarSet liberal_undet_tvs) $
425 ptext (sLit "Using UndecidableInstances might help") ]
426
427 {- Note [Closing over kinds in coverage]
428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
429 Suppose we have a fundep (a::k) -> b
430 Then if 'a' is instantiated to (x y), where x:k2->*, y:k2,
431 then fixing x really fixes k2 as well, and so k2 should be added to
432 the lhs tyvars in the fundep check.
433
434 Example (Trac #8391), using liberal coverage
435 data Foo a = ... -- Foo :: forall k. k -> *
436 class Bar a b | a -> b
437 instance Bar a (Foo a)
438
439 In the instance decl, (a:k) does fix (Foo k a), but only if we notice
440 that (a:k) fixes k. Trac #10109 is another example.
441
442 Here is a more subtle example, from HList-0.4.0.0 (Trac #10564)
443
444 class HasFieldM (l :: k) r (v :: Maybe *)
445 | l r -> v where ...
446 class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
447 | b l r -> v where ...
448 class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
449 | e1 l -> r
450
451 data Label :: k -> *
452 type family LabelsOf (a :: [*]) :: *
453
454 instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
455 HasFieldM1 b l (r xs) v)
456 => HasFieldM l (r xs) v where
457
458 Is the instance OK? Does {l,r,xs} determine v? Well:
459
460 * From the instance constraint HMemberM (Label k l) (LabelsOf xs) b,
461 plus the fundep "| el l -> r" in class HMameberM,
462 we get {l,k,xs} -> b
463
464 * Note the 'k'!! We must call closeOverKinds on the seed set
465 ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b
466 fundep won't fire. This was the reason for #10564.
467
468 * So starting from seeds {l,r,xs,k} we do oclose to get
469 first {l,r,xs,k,b}, via the HMemberM constraint, and then
470 {l,r,xs,k,b,v}, via the HasFieldM1 constraint.
471
472 * And that fixes v.
473
474 However, we must closeOverKinds whenever augmenting the seed set
475 in oclose! Consider Trac #10109:
476
477 data Succ a -- Succ :: forall k. k -> *
478 class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
479 instance (Add a b ab) => Add (Succ {k1} (a :: k1))
480 b
481 (Succ {k3} (ab :: k3})
482
483 We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
484 Now use the fundep to extend to {a,k1,b,k2,ab}. But we need to
485 closeOverKinds *again* now to {a,k1,b,k2,ab,k3}, so that we fix all
486 the variables free in (Succ {k3} ab).
487
488 Bottom line:
489 * closeOverKinds on initial seeds (in checkInstCoverage)
490 * and closeOverKinds whenever extending those seeds (in oclose)
491
492 Note [The liberal coverage condition]
493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
494 (oclose preds tvs) closes the set of type variables tvs,
495 wrt functional dependencies in preds. The result is a superset
496 of the argument set. For example, if we have
497 class C a b | a->b where ...
498 then
499 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
500 because if we know x and y then that fixes z.
501
502 We also use equality predicates in the predicates; if we have an
503 assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
504 also know `t2` and the other way.
505 eg oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
506
507 oclose is used (only) when checking the coverage condition for
508 an instance declaration
509 -}
510
511 oclose :: [PredType] -> TyVarSet -> TyVarSet
512 -- See Note [The liberal coverage condition]
513 oclose preds fixed_tvs
514 | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
515 | otherwise = fixVarSet extend fixed_tvs
516 where
517 extend fixed_tvs = foldl add fixed_tvs tv_fds
518 where
519 add fixed_tvs (ls,rs)
520 | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs
521 | otherwise = fixed_tvs
522 -- closeOverKinds: see Note [Closing over kinds in coverage]
523
524 tv_fds :: [(TyVarSet,TyVarSet)]
525 tv_fds = [ (tyVarsOfTypes ls, tyVarsOfTypes rs)
526 | pred <- preds
527 , (ls, rs) <- determined pred ]
528
529 determined :: PredType -> [([Type],[Type])]
530 determined pred
531 = case classifyPredType pred of
532 EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
533 ClassPred cls tys -> local_fds ++ concatMap determined superclasses
534 where
535 local_fds = [ instFD fd cls_tvs tys
536 | fd <- cls_fds ]
537 (cls_tvs, cls_fds) = classTvsFds cls
538 superclasses = immSuperClasses cls tys
539 _ -> []
540
541 {-
542 ************************************************************************
543 * *
544 Check that a new instance decl is OK wrt fundeps
545 * *
546 ************************************************************************
547
548 Here is the bad case:
549 class C a b | a->b where ...
550 instance C Int Bool where ...
551 instance C Int Char where ...
552
553 The point is that a->b, so Int in the first parameter must uniquely
554 determine the second. In general, given the same class decl, and given
555
556 instance C s1 s2 where ...
557 instance C t1 t2 where ...
558
559 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
560
561 Matters are a little more complicated if there are free variables in
562 the s2/t2.
563
564 class D a b c | a -> b
565 instance D a b => D [(a,a)] [b] Int
566 instance D a b => D [a] [b] Bool
567
568 The instance decls don't overlap, because the third parameter keeps
569 them separate. But we want to make sure that given any constraint
570 D s1 s2 s3
571 if s1 matches
572 -}
573
574 checkFunDeps :: InstEnvs -> ClsInst
575 -> Maybe [ClsInst] -- Nothing <=> ok
576 -- Just dfs <=> conflict with dfs
577 -- Check whether adding DFunId would break functional-dependency constraints
578 -- Used only for instance decls defined in the module being compiled
579 checkFunDeps inst_envs ispec
580 | null bad_fundeps = Nothing
581 | otherwise = Just bad_fundeps
582 where
583 (ins_tvs, clas, ins_tys) = instanceHead ispec
584 ins_tv_set = mkVarSet ins_tvs
585 cls_inst_env = classInstances inst_envs clas
586 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
587
588 badFunDeps :: [ClsInst] -> Class
589 -> TyVarSet -> [Type] -- Proposed new instance type
590 -> [ClsInst]
591 badFunDeps cls_insts clas ins_tv_set ins_tys
592 = nubBy eq_inst $
593 [ ispec | fd <- fds, -- fds is often empty, so do this first!
594 let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
595 ispec <- cls_insts,
596 notNull (checkClsFD fd clas_tvs ispec ins_tv_set ins_tys trimmed_tcs)
597 ]
598 where
599 (clas_tvs, fds) = classTvsFds clas
600 rough_tcs = roughMatchTcs ins_tys
601 eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
602 -- An single instance may appear twice in the un-nubbed conflict list
603 -- because it may conflict with more than one fundep. E.g.
604 -- class C a b c | a -> b, a -> c
605 -- instance C Int Bool Bool
606 -- instance C Int Char Char
607 -- The second instance conflicts with the first by *both* fundeps
608
609 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
610 -- Computing rough_tcs for a particular fundep
611 -- class C a b c | a -> b where ...
612 -- For each instance .... => C ta tb tc
613 -- we want to match only on the type ta; so our
614 -- rough-match thing must similarly be filtered.
615 -- Hence, we Nothing-ise the tb and tc types right here
616 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
617 = zipWith select clas_tvs mb_tcs
618 where
619 select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
620 | otherwise = Nothing