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