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