5a9b57ace9b50d5180ac86a3f56fc069736cf895
[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( transSuperClasses )
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
36 import Pair ( Pair(..) )
37 import Data.List ( nubBy )
38 import Data.Maybe
39 import Data.Foldable ( fold )
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 [text "forall" <+> braces (pprWithCommas ppr qtvs),
188 nest 2 (vcat [ ppr t1 <+> text "~" <+> 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) <- improveClsFD cls_tvs fd ispec
218 tys trimmed_tcs -- NB: orientation
219 , let p_inst = mkClassPred cls (is_tys ispec)
220 ]
221 improveFromInstEnv _ _ _ = []
222
223
224 improveClsFD :: [TyVar] -> FunDep TyVar -- One functional dependency from the class
225 -> ClsInst -- An instance template
226 -> [Type] -> [Maybe Name] -- Arguments of this (C tys) predicate
227 -> [([TyCoVar], [Pair Type])] -- Empty or singleton
228
229 improveClsFD clas_tvs fd
230 (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
231 tys_actual rough_tcs_actual
232
233 -- Compare instance {a,b} C sx sp sy sq
234 -- with wanted [W] C tx tp ty tq
235 -- for fundep (x,y -> p,q) from class (C x p y q)
236 -- If (sx,sy) unifies with (tx,ty), take the subst S
237
238 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
239 -- to make the types match. For example, given
240 -- class C a b | a->b where ...
241 -- instance C (Maybe x) (Tree x) where ..
242 --
243 -- and a wanted constraint of form (C (Maybe t1) t2),
244 -- then we will call checkClsFD with
245 --
246 -- is_qtvs = {x}, is_tys = [Maybe x, Tree x]
247 -- tys_actual = [Maybe t1, t2]
248 --
249 -- We can instantiate x to t1, and then we want to force
250 -- (Tree x) [t1/x] ~ t2
251
252 | instanceCantMatch rough_tcs_inst rough_tcs_actual
253 = [] -- Filter out ones that can't possibly match,
254
255 | otherwise
256 = ASSERT2( length tys_inst == length tys_actual &&
257 length tys_inst == length clas_tvs
258 , ppr tys_inst <+> ppr tys_actual )
259
260 case tcMatchTys ltys1 ltys2 of
261 Nothing -> []
262 Just subst | isJust (tcMatchTysX subst rtys1 rtys2)
263 -- Don't include any equations that already hold.
264 -- Reason: then we know if any actual improvement has happened,
265 -- in which case we need to iterate the solver
266 -- In making this check we must taking account of the fact that any
267 -- qtvs that aren't already instantiated can be instantiated to anything
268 -- at all
269 -- NB: We can't do this 'is-useful-equation' check element-wise
270 -- because of:
271 -- class C a b c | a -> b c
272 -- instance C Int x x
273 -- [Wanted] C Int alpha Int
274 -- We would get that x -> alpha (isJust) and x -> Int (isJust)
275 -- so we would produce no FDs, which is clearly wrong.
276 -> []
277
278 | null fdeqs
279 -> []
280
281 | otherwise
282 -> [(meta_tvs, fdeqs)]
283 -- We could avoid this substTy stuff by producing the eqn
284 -- (qtvs, ls1++rs1, ls2++rs2)
285 -- which will re-do the ls1/ls2 unification when the equation is
286 -- executed. What we're doing instead is recording the partial
287 -- work of the ls1/ls2 unification leaving a smaller unification problem
288 where
289 rtys1' = map (substTyUnchecked subst) rtys1
290
291 fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2
292 -- Don't discard anything!
293 -- We could discard equal types but it's an overkill to call
294 -- eqType again, since we know for sure that /at least one/
295 -- equation in there is useful)
296
297 meta_tvs = [ setVarType tv (substTyUnchecked subst (varType tv))
298 | tv <- qtvs, tv `notElemTCvSubst` subst ]
299 -- meta_tvs are the quantified type variables
300 -- that have not been substituted out
301 --
302 -- Eg. class C a b | a -> b
303 -- instance C Int [y]
304 -- Given constraint C Int z
305 -- we generate the equation
306 -- ({y}, [y], z)
307 --
308 -- But note (a) we get them from the dfun_id, so they are *in order*
309 -- because the kind variables may be mentioned in the
310 -- type variabes' kinds
311 -- (b) we must apply 'subst' to the kinds, in case we have
312 -- matched out a kind variable, but not a type variable
313 -- whose kind mentions that kind variable!
314 -- Trac #6015, #6068
315 where
316 (ltys1, rtys1) = instFD fd clas_tvs tys_inst
317 (ltys2, rtys2) = instFD fd clas_tvs tys_actual
318
319 {-
320 %************************************************************************
321 %* *
322 The Coverage condition for instance declarations
323 * *
324 ************************************************************************
325
326 Note [Coverage condition]
327 ~~~~~~~~~~~~~~~~~~~~~~~~~
328 Example
329 class C a b | a -> b
330 instance theta => C t1 t2
331
332 For the coverage condition, we check
333 (normal) fv(t2) `subset` fv(t1)
334 (liberal) fv(t2) `subset` oclose(fv(t1), theta)
335
336 The liberal version ensures the self-consistency of the instance, but
337 it does not guarantee termination. Example:
338
339 class Mul a b c | a b -> c where
340 (.*.) :: a -> b -> c
341
342 instance Mul Int Int Int where (.*.) = (*)
343 instance Mul Int Float Float where x .*. y = fromIntegral x * y
344 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
345
346 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
347 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
348
349 But it is a mistake to accept the instance because then this defn:
350 f = \ b x y -> if b then x .*. [y] else y
351 makes instance inference go into a loop, because it requires the constraint
352 Mul a [b] b
353 -}
354
355 checkInstCoverage :: Bool -- Be liberal
356 -> Class -> [PredType] -> [Type]
357 -> Validity
358 -- "be_liberal" flag says whether to use "liberal" coverage of
359 -- See Note [Coverage Condition] below
360 --
361 -- Return values
362 -- Nothing => no problems
363 -- Just msg => coverage problem described by msg
364
365 checkInstCoverage be_liberal clas theta inst_taus
366 = allValid (map fundep_ok fds)
367 where
368 (tyvars, fds) = classTvsFds clas
369 fundep_ok fd
370 | and (isEmptyVarSet <$> undetermined_tvs) = IsValid
371 | otherwise = NotValid msg
372 where
373 (ls,rs) = instFD fd tyvars inst_taus
374 ls_tvs = tyCoVarsOfTypes ls
375 rs_tvs = splitVisVarsOfTypes rs
376
377 undetermined_tvs | be_liberal = liberal_undet_tvs
378 | otherwise = conserv_undet_tvs
379
380 closed_ls_tvs = oclose theta ls_tvs
381 liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
382 conserv_undet_tvs = (`minusVarSet` ls_tvs) <$> rs_tvs
383
384 undet_list = varSetElemsWellScoped (fold undetermined_tvs)
385
386 msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
387 -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
388 -- , text "theta" <+> ppr theta
389 -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
390 -- , text "rs_tvs" <+> ppr rs_tvs
391 sep [ text "The"
392 <+> ppWhen be_liberal (text "liberal")
393 <+> text "coverage condition fails in class"
394 <+> quotes (ppr clas)
395 , nest 2 $ text "for functional dependency:"
396 <+> quotes (pprFunDep fd) ]
397 , sep [ text "Reason: lhs type"<>plural ls <+> pprQuotedList ls
398 , nest 2 $
399 (if isSingleton ls
400 then text "does not"
401 else text "do not jointly")
402 <+> text "determine rhs type"<>plural rs
403 <+> pprQuotedList rs ]
404 , text "Un-determined variable" <> plural undet_list <> colon
405 <+> pprWithCommas ppr undet_list
406 , ppWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
407 text "(Use -fprint-explicit-kinds to see the kind variables in the types)"
408 , ppWhen (not be_liberal &&
409 and (isEmptyVarSet <$> liberal_undet_tvs)) $
410 text "Using UndecidableInstances might help" ]
411
412 {- Note [Closing over kinds in coverage]
413 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
414 Suppose we have a fundep (a::k) -> b
415 Then if 'a' is instantiated to (x y), where x:k2->*, y:k2,
416 then fixing x really fixes k2 as well, and so k2 should be added to
417 the lhs tyvars in the fundep check.
418
419 Example (Trac #8391), using liberal coverage
420 data Foo a = ... -- Foo :: forall k. k -> *
421 class Bar a b | a -> b
422 instance Bar a (Foo a)
423
424 In the instance decl, (a:k) does fix (Foo k a), but only if we notice
425 that (a:k) fixes k. Trac #10109 is another example.
426
427 Here is a more subtle example, from HList-0.4.0.0 (Trac #10564)
428
429 class HasFieldM (l :: k) r (v :: Maybe *)
430 | l r -> v where ...
431 class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
432 | b l r -> v where ...
433 class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
434 | e1 l -> r
435
436 data Label :: k -> *
437 type family LabelsOf (a :: [*]) :: *
438
439 instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
440 HasFieldM1 b l (r xs) v)
441 => HasFieldM l (r xs) v where
442
443 Is the instance OK? Does {l,r,xs} determine v? Well:
444
445 * From the instance constraint HMemberM (Label k l) (LabelsOf xs) b,
446 plus the fundep "| el l -> r" in class HMameberM,
447 we get {l,k,xs} -> b
448
449 * Note the 'k'!! We must call closeOverKinds on the seed set
450 ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b
451 fundep won't fire. This was the reason for #10564.
452
453 * So starting from seeds {l,r,xs,k} we do oclose to get
454 first {l,r,xs,k,b}, via the HMemberM constraint, and then
455 {l,r,xs,k,b,v}, via the HasFieldM1 constraint.
456
457 * And that fixes v.
458
459 However, we must closeOverKinds whenever augmenting the seed set
460 in oclose! Consider Trac #10109:
461
462 data Succ a -- Succ :: forall k. k -> *
463 class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
464 instance (Add a b ab) => Add (Succ {k1} (a :: k1))
465 b
466 (Succ {k3} (ab :: k3})
467
468 We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
469 Now use the fundep to extend to {a,k1,b,k2,ab}. But we need to
470 closeOverKinds *again* now to {a,k1,b,k2,ab,k3}, so that we fix all
471 the variables free in (Succ {k3} ab).
472
473 Bottom line:
474 * closeOverKinds on initial seeds (done automatically
475 by tyCoVarsOfTypes in checkInstCoverage)
476 * and closeOverKinds whenever extending those seeds (in oclose)
477
478 Note [The liberal coverage condition]
479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
480 (oclose preds tvs) closes the set of type variables tvs,
481 wrt functional dependencies in preds. The result is a superset
482 of the argument set. For example, if we have
483 class C a b | a->b where ...
484 then
485 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
486 because if we know x and y then that fixes z.
487
488 We also use equality predicates in the predicates; if we have an
489 assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
490 also know `t2` and the other way.
491 eg oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
492
493 oclose is used (only) when checking the coverage condition for
494 an instance declaration
495 -}
496
497 oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
498 -- See Note [The liberal coverage condition]
499 oclose preds fixed_tvs
500 | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
501 | otherwise = fixVarSet extend fixed_tvs
502 where
503 extend fixed_tvs = foldl add fixed_tvs tv_fds
504 where
505 add fixed_tvs (ls,rs)
506 | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs
507 | otherwise = fixed_tvs
508 -- closeOverKinds: see Note [Closing over kinds in coverage]
509
510 tv_fds :: [(TyCoVarSet,TyCoVarSet)]
511 tv_fds = [ (tyCoVarsOfTypes ls, tyCoVarsOfTypes rs)
512 | pred <- preds
513 , pred' <- pred : transSuperClasses pred
514 -- Look for fundeps in superclasses too
515 , (ls, rs) <- determined pred' ]
516
517 determined :: PredType -> [([Type],[Type])]
518 determined pred
519 = case classifyPredType pred of
520 EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
521 ClassPred cls tys -> [ instFD fd cls_tvs tys
522 | let (cls_tvs, cls_fds) = classTvsFds cls
523 , fd <- cls_fds ]
524 _ -> []
525
526 {-
527 ************************************************************************
528 * *
529 Check that a new instance decl is OK wrt fundeps
530 * *
531 ************************************************************************
532
533 Here is the bad case:
534 class C a b | a->b where ...
535 instance C Int Bool where ...
536 instance C Int Char where ...
537
538 The point is that a->b, so Int in the first parameter must uniquely
539 determine the second. In general, given the same class decl, and given
540
541 instance C s1 s2 where ...
542 instance C t1 t2 where ...
543
544 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
545
546 Matters are a little more complicated if there are free variables in
547 the s2/t2.
548
549 class D a b c | a -> b
550 instance D a b => D [(a,a)] [b] Int
551 instance D a b => D [a] [b] Bool
552
553 The instance decls don't overlap, because the third parameter keeps
554 them separate. But we want to make sure that given any constraint
555 D s1 s2 s3
556 if s1 matches
557
558 Note [Bogus consistency check]
559 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
560 In checkFunDeps we check that a new ClsInst is consistent with all the
561 ClsInsts in the environment.
562
563 The bogus aspect is discussed in Trac #10675. Currenty it if the two
564 types are *contradicatory*, using (isNothing . tcUnifyTys). But all
565 the papers say we should check if the two types are *equal* thus
566 not (substTys subst rtys1 `eqTypes` substTys subst rtys2)
567 For now I'm leaving the bogus form because that's the way it has
568 been for years.
569 -}
570
571 checkFunDeps :: InstEnvs -> ClsInst -> [ClsInst]
572 -- The Consistency Check.
573 -- Check whether adding DFunId would break functional-dependency constraints
574 -- Used only for instance decls defined in the module being compiled
575 -- Returns a list of the ClsInst in InstEnvs that are inconsistent
576 -- with the proposed new ClsInst
577 checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
578 , is_tys = tys1, is_tcs = rough_tcs1 })
579 | null fds
580 = []
581 | otherwise
582 = nubBy eq_inst $
583 [ ispec | ispec <- cls_insts
584 , fd <- fds
585 , is_inconsistent fd ispec ]
586 where
587 cls_insts = classInstances inst_envs cls
588 (cls_tvs, fds) = classTvsFds cls
589 qtv_set1 = mkVarSet qtvs1
590
591 is_inconsistent fd (ClsInst { is_tvs = qtvs2, is_tys = tys2, is_tcs = rough_tcs2 })
592 | instanceCantMatch trimmed_tcs rough_tcs2
593 = False
594 | otherwise
595 = case tcUnifyTys bind_fn ltys1 ltys2 of
596 Nothing -> False
597 Just subst
598 -> isNothing $ -- Bogus legacy test (Trac #10675)
599 -- See Note [Bogus consistency check]
600 tcUnifyTys bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
601
602 where
603 trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs1
604 (ltys1, rtys1) = instFD fd cls_tvs tys1
605 (ltys2, rtys2) = instFD fd cls_tvs tys2
606 qtv_set2 = mkVarSet qtvs2
607 bind_fn tv | tv `elemVarSet` qtv_set1 = BindMe
608 | tv `elemVarSet` qtv_set2 = BindMe
609 | otherwise = Skolem
610
611 eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
612 -- An single instance may appear twice in the un-nubbed conflict list
613 -- because it may conflict with more than one fundep. E.g.
614 -- class C a b c | a -> b, a -> c
615 -- instance C Int Bool Bool
616 -- instance C Int Char Char
617 -- The second instance conflicts with the first by *both* fundeps
618
619 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
620 -- Computing rough_tcs for a particular fundep
621 -- class C a b c | a -> b where ...
622 -- For each instance .... => C ta tb tc
623 -- we want to match only on the type ta; so our
624 -- rough-match thing must similarly be filtered.
625 -- Hence, we Nothing-ise the tb and tc types right here
626 --
627 -- Result list is same length as input list, just with more Nothings
628 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
629 = zipWith select clas_tvs mb_tcs
630 where
631 select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
632 | otherwise = Nothing