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