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