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