2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 2000
6 FunDeps - functional dependencies
8 It's better to read it as: "if we know these, then we're going to know these"
13 Equation(..), pprEquation,
14 oclose, improveFromInstEnv, improveFromAnother,
15 checkInstCoverage, checkFunDeps,
19 #include "HsVersions.h"
33 import Data.List ( nubBy )
34 import Data.Maybe ( isJust )
38 %************************************************************************
40 \subsection{Close type variables}
42 %************************************************************************
44 oclose(vs,C) The result of extending the set of tyvars vs
45 using the functional dependencies from C
47 grow(vs,C) The result of extend the set of tyvars vs
48 using all conceivable links from C.
50 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
51 Then grow(vs,C) = {a,b,c}
53 Note that grow(vs,C) `superset` grow(vs,simplify(C))
54 That is, simplfication can only shrink the result of grow.
57 oclose is conservative v `elem` oclose(vs,C)
58 one way: => v is definitely fixed by vs
60 grow is conservative if v might be fixed by vs
61 the other way: => v `elem` grow(vs,C)
63 ----------------------------------------------------------
64 (oclose preds tvs) closes the set of type variables tvs,
65 wrt functional dependencies in preds. The result is a superset
66 of the argument set. For example, if we have
67 class C a b | a->b where ...
69 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
70 because if we know x and y then that fixes z.
72 oclose is used (only) when generalising a type T; see extensive
75 Note [Important subtlety in oclose]
76 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
77 Consider (oclose (C Int t) {}), where class C a b | a->b
78 Then, since a->b, 't' is fully determined by Int, and the
79 uniform thing is to return {t}.
83 f x = e -- 'e' generates constraint (D s Int t)
85 Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
86 monomorphic in 't', thus
87 f :: forall s. D s Int t => s -> s
89 But if this function is never called, 't' will never be instantiated;
90 the functional dependencies that fix 't' may well be instance decls in
91 some importing module. But the top-level defaulting of unconstrained
92 type variables will fix t=GHC.Prim.Any, and that's simply a bug.
94 Conclusion: oclose only returns a type variable as "fixed" if it
95 depends on at least one type variable in the input fixed_tvs.
97 Remember, it's always sound for oclose to return a smaller set.
98 An interesting example is tcfail093, where we get this inferred type:
100 dup :: forall h. (Call (IO Int) h) => () -> Int -> h
101 This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
102 previously GHC rejected this saying 'no instance for Call (IO Int) h'.
103 But it's right on the borderline. If there was an extra, otherwise
104 uninvolved type variable, like 's' in the type of 'f' above, then
105 we must accept the function. So, for now anyway, we accept 'dup' too.
108 oclose :: [PredType] -> TyVarSet -> TyVarSet
109 oclose preds fixed_tvs
110 | null tv_fds = fixed_tvs -- Fast escape hatch for common case
111 | isEmptyVarSet fixed_tvs = emptyVarSet -- Note [Important subtlety in oclose]
112 | otherwise = loop fixed_tvs
115 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
116 | otherwise = loop new_fixed_tvs
118 new_fixed_tvs = foldl extend fixed_tvs tv_fds
120 extend fixed_tvs (ls,rs)
121 | not (isEmptyVarSet ls) -- Note [Important subtlety in oclose]
122 , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
123 | otherwise = fixed_tvs
125 tv_fds :: [(TyVarSet,TyVarSet)]
126 -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
127 -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
128 tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
129 | ClassP cls tys <- preds, -- Ignore implicit params
130 let (cls_tvs, cls_fds) = classTvsFds cls,
132 let (xs,ys) = instFD fd cls_tvs tys
137 %************************************************************************
139 \subsection{Generate equations from functional dependencies}
141 %************************************************************************
144 Each functional dependency with one variable in the RHS is responsible
145 for generating a single equality. For instance:
147 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
150 , fd_ty_right = alpha }
151 However notice that a functional dependency may have more than one variable
152 in the RHS which will create more than one FDEq. Example:
153 class C a b c | a -> b c
154 [Wanted] C Int alpha alpha
155 [Wanted] C Int Bool beta
157 fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
158 fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
160 We record the paremeter position so that can immediately rewrite a constraint
161 using the produced FDEqs and remove it from our worklist.
164 INVARIANT: Corresponding types aren't already equal
165 That is, there exists at least one non-identity equality in FDEqs.
168 class C a b c | a -> b c
170 And: [Wanted] C Int Bool alpha
171 We will /match/ the LHS of fundep equations, producing a matching substitution
172 and create equations for the RHS sides. In our last example we'd have generated:
177 To ``execute'' the equation, make fresh type variable for each tyvar in the set,
178 instantiate the two types with these fresh variables, and then unify or generate
179 a new constraint. In the above example we would generate a new unification
180 variable 'beta' for x and produce the following constraints:
181 [Wanted] (Bool ~ beta)
182 [Wanted] (alpha ~ beta)
184 Notice the subtle difference between the above class declaration and:
185 class C a b c | a -> b, a -> c
186 where we would generate:
187 ({x},[fd1]),({x},[fd2])
188 This means that the template variable would be instantiated to different
189 unification variables when producing the FD constraints.
191 Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
194 type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
197 = FDEqn { fd_qtvs :: TyVarSet -- Instantiate these to fresh unification vars
198 , fd_eqs :: [FDEq] -- and then make these equal
199 , fd_pred1, fd_pred2 :: Pred_Loc } -- The Equation arose from
200 -- combining these two constraints
202 data FDEq = FDEq { fd_pos :: Int -- We use '0' for the first position
204 , fd_ty_right :: Type }
207 Given a bunch of predicates that must hold, such as
209 C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
211 improve figures out what extra equations must hold.
212 For example, if we have
214 class C a b | a->b where ...
216 then improve will return
222 * improve does not iterate. It's possible that when we make
223 t1=t2, for example, that will in turn trigger a new equation.
224 This would happen if we also had
226 If t1=t2, we also get t7=t8.
228 improve does *not* do this extra step. It relies on the caller
231 * The equations unify types that are not already equal. So there
232 is no effect iff the result of improve is empty
237 instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)])
238 -- Returns a FunDep between the types accompanied along with their
239 -- position (<=0) in the types argument list.
240 instFD_WithPos (ls,rs) tvs tys
241 = (map (snd . lookup) ls, map lookup rs)
243 ind_tys = zip [0..] tys
244 env = zipVarEnv tvs ind_tys
245 lookup tv = lookupVarEnv_NF env tv
247 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
251 -- Create a list of FDEqs from two lists of types, making sure
252 -- that the types are not equal.
253 zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
254 | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
255 | otherwise = FDEq { fd_pos = i2
257 , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
258 zipAndComputeFDEqs _ _ _ = []
260 -- Improve a class constraint from another class constraint
261 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
262 improveFromAnother :: Pred_Loc -- Template item (usually given, or inert)
263 -> Pred_Loc -- Workitem [that can be improved]
265 -- Post: FDEqs always oriented from the other to the workitem
266 -- Equations have empty quantified variables
267 improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
268 | tys1 `lengthAtLeast` 2 && cls1 == cls2
269 = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
270 | let (cls_tvs, cls_fds) = classTvsFds cls1
272 , let (ltys1, rs1) = instFD fd cls_tvs tys1
273 (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
274 , eqTypes ltys1 ltys2 -- The LHSs match
275 , let eqs = zipAndComputeFDEqs eqType rs1 irs2
278 improveFromAnother _ _ = []
281 -- Improve a class constraint from instance declarations
282 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
284 pprEquation :: Equation -> SDoc
285 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
286 = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
287 nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
289 improveFromInstEnv :: (InstEnv,InstEnv)
291 -> [Equation] -- Needs to be an Equation because
292 -- of quantified variables
293 -- Post: Equations oriented from the template (matching instance) to the workitem!
294 improveFromInstEnv _inst_env (pred,_loc)
295 | not (isClassPred pred)
296 = panic "improveFromInstEnv: not a class predicate"
297 improveFromInstEnv inst_env pred@(ClassP cls tys, _)
298 | tys `lengthAtLeast` 2
299 = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
300 | fd <- cls_fds -- Iterate through the fundeps first,
301 -- because there often are none!
302 , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
303 -- Trim the rough_tcs based on the head of the fundep.
304 -- Remember that instanceCantMatch treats both argumnents
305 -- symmetrically, so it's ok to trim the rough_tcs,
306 -- rather than trimming each inst_tcs in turn
307 , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
308 is_tcs = inst_tcs }) <- instances
309 , not (instanceCantMatch inst_tcs trimmed_tcs)
310 , let p_inst = (mkClassPred cls tys_inst,
311 sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
312 , ptext (sLit "in the instance declaration at")
313 <+> ppr (getSrcLoc ispec)])
314 , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
318 (cls_tvs, cls_fds) = classTvsFds cls
319 instances = classInstances inst_env cls
320 rough_tcs = roughMatchTcs tys
321 improveFromInstEnv _ _ = []
324 checkClsFD :: TyVarSet -- Quantified type variables; see note below
325 -> FunDep TyVar -> [TyVar] -- One functional dependency from the class
327 -> [(TyVarSet, [FDEq])]
329 checkClsFD qtvs fd clas_tvs tys1 tys2
330 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
331 -- to make the types match. For example, given
332 -- class C a b | a->b where ...
333 -- instance C (Maybe x) (Tree x) where ..
335 -- and an Inst of form (C (Maybe t1) t2),
336 -- then we will call checkClsFD with
338 -- qtvs = {x}, tys1 = [Maybe x, Tree x]
339 -- tys2 = [Maybe t1, t2]
341 -- We can instantiate x to t1, and then we want to force
342 -- (Tree x) [t1/x] ~ t2
344 -- This function is also used when matching two Insts (rather than an Inst
345 -- against an instance decl. In that case, qtvs is empty, and we are doing
348 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
349 -- For the one-sided matching case, the qtvs are just from the template,
350 -- so we get matching
352 = ASSERT2( length tys1 == length tys2 &&
353 length tys1 == length clas_tvs
354 , ppr tys1 <+> ppr tys2 )
356 case tcUnifyTys bind_fn ltys1 ltys2 of
358 Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
359 -- Don't include any equations that already hold.
360 -- Reason: then we know if any actual improvement has happened,
361 -- in which case we need to iterate the solver
362 -- In making this check we must taking account of the fact that any
363 -- qtvs that aren't already instantiated can be instantiated to anything
365 -- NB: We can't do this 'is-useful-equation' check element-wise
367 -- class C a b c | a -> b c
368 -- instance C Int x x
369 -- [Wanted] C Int alpha Int
370 -- We would get that x -> alpha (isJust) and x -> Int (isJust)
371 -- so we would produce no FDs, which is clearly wrong.
376 -- We could avoid this substTy stuff by producing the eqn
377 -- (qtvs, ls1++rs1, ls2++rs2)
378 -- which will re-do the ls1/ls2 unification when the equation is
379 -- executed. What we're doing instead is recording the partial
380 -- work of the ls1/ls2 unification leaving a smaller unification problem
382 rtys1' = map (substTy subst) rtys1
383 irs2' = map (\(i,x) -> (i,substTy subst x)) irs2
384 rtys2' = map snd irs2'
386 fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
387 -- Don't discard anything!
388 -- We could discard equal types but it's an overkill to call
389 -- eqType again, since we know for sure that /at least one/
390 -- equation in there is useful)
392 qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
393 -- qtvs' are the quantified type variables
394 -- that have not been substituted out
396 -- Eg. class C a b | a -> b
397 -- instance C Int [y]
398 -- Given constraint C Int z
399 -- we generate the equation
402 bind_fn tv | tv `elemVarSet` qtvs = BindMe
405 (ltys1, rtys1) = instFD fd clas_tvs tys1
406 (ltys2, irs2) = instFD_WithPos fd clas_tvs tys2
411 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
412 -- A simpler version of instFD_WithPos to be used in checking instance coverage etc.
413 instFD (ls,rs) tvs tys
414 = (map lookup ls, map lookup rs)
416 env = zipVarEnv tvs tys
417 lookup tv = lookupVarEnv_NF env tv
419 checkInstCoverage :: Class -> [Type] -> Bool
420 -- Check that the Coverage Condition is obeyed in an instance decl
421 -- For example, if we have
422 -- class theta => C a b | a -> b
424 -- Then we require fv(t2) `subset` fv(t1)
425 -- See Note [Coverage Condition] below
427 checkInstCoverage clas inst_taus
430 (tyvars, fds) = classTvsFds clas
431 fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
433 (ls,rs) = instFD fd tyvars inst_taus
436 Note [Coverage condition]
437 ~~~~~~~~~~~~~~~~~~~~~~~~~
438 For the coverage condition, we used to require only that
439 fv(t2) `subset` oclose(fv(t1), theta)
442 class Mul a b c | a b -> c where
445 instance Mul Int Int Int where (.*.) = (*)
446 instance Mul Int Float Float where x .*. y = fromIntegral x * y
447 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
449 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
450 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
452 But it is a mistake to accept the instance because then this defn:
453 f = \ b x y -> if b then x .*. [y] else y
454 makes instance inference go into a loop, because it requires the constraint
458 %************************************************************************
460 Check that a new instance decl is OK wrt fundeps
462 %************************************************************************
464 Here is the bad case:
465 class C a b | a->b where ...
466 instance C Int Bool where ...
467 instance C Int Char where ...
469 The point is that a->b, so Int in the first parameter must uniquely
470 determine the second. In general, given the same class decl, and given
472 instance C s1 s2 where ...
473 instance C t1 t2 where ...
475 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
477 Matters are a little more complicated if there are free variables in
480 class D a b c | a -> b
481 instance D a b => D [(a,a)] [b] Int
482 instance D a b => D [a] [b] Bool
484 The instance decls don't overlap, because the third parameter keeps
485 them separate. But we want to make sure that given any constraint
491 checkFunDeps :: (InstEnv, InstEnv) -> Instance
492 -> Maybe [Instance] -- Nothing <=> ok
493 -- Just dfs <=> conflict with dfs
494 -- Check wheher adding DFunId would break functional-dependency constraints
495 -- Used only for instance decls defined in the module being compiled
496 checkFunDeps inst_envs ispec
497 | null bad_fundeps = Nothing
498 | otherwise = Just bad_fundeps
500 (ins_tvs, _, clas, ins_tys) = instanceHead ispec
501 ins_tv_set = mkVarSet ins_tvs
502 cls_inst_env = classInstances inst_envs clas
503 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
505 badFunDeps :: [Instance] -> Class
506 -> TyVarSet -> [Type] -- Proposed new instance type
508 badFunDeps cls_insts clas ins_tv_set ins_tys
510 [ ispec | fd <- fds, -- fds is often empty, so do this first!
511 let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
512 ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs,
513 is_tys = tys }) <- cls_insts,
514 -- Filter out ones that can't possibly match,
515 -- based on the head of the fundep
516 not (instanceCantMatch inst_tcs trimmed_tcs),
517 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set)
518 fd clas_tvs tys ins_tys)
521 (clas_tvs, fds) = classTvsFds clas
522 rough_tcs = roughMatchTcs ins_tys
523 eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
524 -- An single instance may appear twice in the un-nubbed conflict list
525 -- because it may conflict with more than one fundep. E.g.
526 -- class C a b c | a -> b, a -> c
527 -- instance C Int Bool Bool
528 -- instance C Int Char Char
529 -- The second instance conflicts with the first by *both* fundeps
531 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
532 -- Computing rough_tcs for a particular fundep
533 -- class C a b c | a -> b where ...
534 -- For each instance .... => C ta tb tc
535 -- we want to match only on the type ta; so our
536 -- rough-match thing must similarly be filtered.
537 -- Hence, we Nothing-ise the tb and tc types right here
538 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
539 = zipWith select clas_tvs mb_tcs
541 select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
542 | otherwise = Nothing