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