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"
12 Equation, pprEquation,
13 oclose, grow, improveOne,
14 checkInstCoverage, checkFunDeps,
18 #include "HsVersions.h"
32 import Data.List ( nubBy )
33 import Data.Maybe ( isJust )
37 %************************************************************************
39 \subsection{Close type variables}
41 %************************************************************************
43 oclose(vs,C) The result of extending the set of tyvars vs
44 using the functional dependencies from C
46 grow(vs,C) The result of extend the set of tyvars vs
47 using all conceivable links from C.
49 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
50 Then grow(vs,C) = {a,b,c}
52 Note that grow(vs,C) `superset` grow(vs,simplify(C))
53 That is, simplfication can only shrink the result of grow.
56 oclose is conservative v `elem` oclose(vs,C)
57 one way: => v is definitely fixed by vs
59 grow is conservative if v might be fixed by vs
60 the other way: => v `elem` grow(vs,C)
62 ----------------------------------------------------------
63 (oclose preds tvs) closes the set of type variables tvs,
64 wrt functional dependencies in preds. The result is a superset
65 of the argument set. For example, if we have
66 class C a b | a->b where ...
68 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
69 because if we know x and y then that fixes z.
71 oclose is used (only) when generalising a type T; see extensive
74 Note [Important subtlety in oclose]
75 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
76 Consider (oclose (C Int t) {}), where class C a b | a->b
77 Then, since a->b, 't' is fully determined by Int, and the
78 uniform thing is to return {t}.
82 f x = e -- 'e' generates constraint (D s Int t)
84 Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
85 monomorphic in 't', thus
86 f :: forall s. D s Int t => s -> s
88 But if this function is never called, 't' will never be instantiated;
89 the functional dependencies that fix 't' may well be instance decls in
90 some importing module. But the top-level defaulting of unconstrained
91 type variables will fix t=GHC.Prim.Any, and that's simply a bug.
93 Conclusion: oclose only returns a type variable as "fixed" if it
94 depends on at least one type variable in the input fixed_tvs.
96 Remember, it's always sound for oclose to return a smaller set.
97 An interesting example is tcfail093, where we get this inferred type:
99 dup :: forall h. (Call (IO Int) h) => () -> Int -> h
100 This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
101 previously GHC rejected this saying 'no instance for Call (IO Int) h'.
102 But it's right on the borderline. If there was an extra, otherwise
103 uninvolved type variable, like 's' in the type of 'f' above, then
104 we must accept the function. So, for now anyway, we accept 'dup' too.
107 oclose :: [PredType] -> TyVarSet -> TyVarSet
108 oclose preds fixed_tvs
109 | null tv_fds = fixed_tvs -- Fast escape hatch for common case
110 | isEmptyVarSet fixed_tvs = emptyVarSet -- Note [Important subtlety in oclose]
111 | otherwise = loop fixed_tvs
114 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
115 | otherwise = loop new_fixed_tvs
117 new_fixed_tvs = foldl extend fixed_tvs tv_fds
119 extend fixed_tvs (ls,rs)
120 | not (isEmptyVarSet ls) -- Note [Important subtlety in oclose]
121 , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
122 | otherwise = fixed_tvs
124 tv_fds :: [(TyVarSet,TyVarSet)]
125 -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
126 -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
127 tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
128 | ClassP cls tys <- preds, -- Ignore implicit params
129 let (cls_tvs, cls_fds) = classTvsFds cls,
131 let (xs,ys) = instFD fd cls_tvs tys
135 Note [Growing the tau-tvs using constraints]
136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
137 (grow preds tvs) is the result of extend the set of tyvars tvs
138 using all conceivable links from pred
140 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
141 Then grow precs tvs = {a,b,c}
143 All the type variables from an implicit parameter are added, whether or
144 not they are mentioned in tvs; see Note [Implicit parameters and ambiguity]
147 See also Note [Ambiguity] in TcSimplify
150 grow :: [PredType] -> TyVarSet -> TyVarSet
152 | null preds = fixed_tvs
153 | otherwise = loop real_fixed_tvs
155 -- Add the implicit parameters;
156 -- see Note [Implicit parameters and ambiguity] in TcSimplify
157 real_fixed_tvs = foldr unionVarSet fixed_tvs ip_tvs
160 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
161 | otherwise = loop new_fixed_tvs
163 new_fixed_tvs = foldl extend fixed_tvs non_ip_tvs
165 extend fixed_tvs pred_tvs
166 | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs
167 | otherwise = fixed_tvs
169 (ip_tvs, non_ip_tvs) = partitionWith get_ip preds
170 get_ip (IParam _ ty) = Left (tyVarsOfType ty)
171 get_ip other = Right (tyVarsOfPred other)
174 %************************************************************************
176 \subsection{Generate equations from functional dependencies}
178 %************************************************************************
182 type Equation = (TyVarSet, [(Type, Type)])
183 -- These pairs of types should be equal, for some
184 -- substitution of the tyvars in the tyvar set
185 -- INVARIANT: corresponding types aren't already equal
187 -- It's important that we have a *list* of pairs of types. Consider
188 -- class C a b c | a -> b c where ...
189 -- instance C Int x x where ...
190 -- Then, given the constraint (C Int Bool v) we should improve v to Bool,
191 -- via the equation ({x}, [(Bool,x), (v,x)])
192 -- This would not happen if the class had looked like
193 -- class C a b c | a -> b, a -> c
195 -- To "execute" the equation, make fresh type variable for each tyvar in the set,
196 -- instantiate the two types with these fresh variables, and then unify.
198 -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
199 -- We unify z with Int, but since a and b are quantified we do nothing to them
200 -- We usually act on an equation by instantiating the quantified type varaibles
201 -- to fresh type variables, and then calling the standard unifier.
203 pprEquation :: Equation -> SDoc
204 pprEquation (qtvs, pairs)
205 = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
206 nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])]
209 Given a bunch of predicates that must hold, such as
211 C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
213 improve figures out what extra equations must hold.
214 For example, if we have
216 class C a b | a->b where ...
218 then improve will return
224 * improve does not iterate. It's possible that when we make
225 t1=t2, for example, that will in turn trigger a new equation.
226 This would happen if we also had
228 If t1=t2, we also get t7=t8.
230 improve does *not* do this extra step. It relies on the caller
233 * The equations unify types that are not already equal. So there
234 is no effect iff the result of improve is empty
239 type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
241 improveOne :: (Class -> [Instance]) -- Gives instances for given class
242 -> Pred_Loc -- Do improvement triggered by this
243 -> [Pred_Loc] -- Current constraints
244 -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
245 -- (NB the above INVARIANT for type Equation)
246 -- The Pred_Locs explain which two predicates were
247 -- combined (for error messages)
248 -- Just do improvement triggered by a single, distinguised predicate
250 improveOne _inst_env pred@(IParam ip ty, _) preds
251 = [ ((emptyVarSet, [(ty,ty2)]), pred, p2)
252 | p2@(IParam ip2 ty2, _) <- preds
254 , not (ty `tcEqType` ty2)]
256 improveOne inst_env pred@(ClassP cls tys, _) preds
257 | tys `lengthAtLeast` 2
258 = instance_eqns ++ pairwise_eqns
259 -- NB: we put the instance equations first. This biases the
260 -- order so that we first improve individual constraints against the
261 -- instances (which are perhaps in a library and less likely to be
262 -- wrong; and THEN perform the pairwise checks.
263 -- The other way round, it's possible for the pairwise check to succeed
264 -- and cause a subsequent, misleading failure of one of the pair with an
265 -- instance declaration. See tcfail143.hs for an example
267 (cls_tvs, cls_fds) = classTvsFds cls
268 instances = inst_env cls
269 rough_tcs = roughMatchTcs tys
271 -- NOTE that we iterate over the fds first; they are typically
272 -- empty, which aborts the rest of the loop.
273 pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
274 pairwise_eqns -- This group comes from pairwise comparison
277 , p2@(ClassP cls2 tys2, _) <- preds
279 , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
282 instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
283 instance_eqns -- This group comes from comparing with instance decls
284 = [ (eqn, p_inst, pred)
285 | fd <- cls_fds -- Iterate through the fundeps first,
286 -- because there often are none!
287 , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
288 -- Trim the rough_tcs based on the head of the fundep.
289 -- Remember that instanceCantMatch treats both argumnents
290 -- symmetrically, so it's ok to trim the rough_tcs,
291 -- rather than trimming each inst_tcs in turn
292 , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
293 is_tcs = inst_tcs }) <- instances
294 , not (instanceCantMatch inst_tcs trimmed_tcs)
295 , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
296 , let p_inst = (mkClassPred cls tys_inst,
297 sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
298 , ptext (sLit "in the instance declaration at")
299 <+> ppr (getSrcLoc ispec)])
306 checkClsFD :: TyVarSet -- Quantified type variables; see note below
307 -> FunDep TyVar -> [TyVar] -- One functional dependency from the class
311 checkClsFD qtvs fd clas_tvs tys1 tys2
312 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
313 -- to make the types match. For example, given
314 -- class C a b | a->b where ...
315 -- instance C (Maybe x) (Tree x) where ..
317 -- and an Inst of form (C (Maybe t1) t2),
318 -- then we will call checkClsFD with
320 -- qtvs = {x}, tys1 = [Maybe x, Tree x]
321 -- tys2 = [Maybe t1, t2]
323 -- We can instantiate x to t1, and then we want to force
324 -- (Tree x) [t1/x] ~ t2
326 -- This function is also used when matching two Insts (rather than an Inst
327 -- against an instance decl. In that case, qtvs is empty, and we are doing
330 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
331 -- For the one-sided matching case, the qtvs are just from the template,
332 -- so we get matching
334 = ASSERT2( length tys1 == length tys2 &&
335 length tys1 == length clas_tvs
336 , ppr tys1 <+> ppr tys2 )
338 case tcUnifyTys bind_fn ls1 ls2 of
340 Just subst | isJust (tcUnifyTys bind_fn rs1' rs2')
341 -- Don't include any equations that already hold.
342 -- Reason: then we know if any actual improvement has happened,
343 -- in which case we need to iterate the solver
344 -- In making this check we must taking account of the fact that any
345 -- qtvs that aren't already instantiated can be instantiated to anything
349 | otherwise -- Aha! A useful equation
350 -> [ (qtvs', zip rs1' rs2')]
351 -- We could avoid this substTy stuff by producing the eqn
352 -- (qtvs, ls1++rs1, ls2++rs2)
353 -- which will re-do the ls1/ls2 unification when the equation is
354 -- executed. What we're doing instead is recording the partial
355 -- work of the ls1/ls2 unification leaving a smaller unification problem
357 rs1' = substTys subst rs1
358 rs2' = substTys subst rs2
359 qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
360 -- qtvs' are the quantified type variables
361 -- that have not been substituted out
363 -- Eg. class C a b | a -> b
364 -- instance C Int [y]
365 -- Given constraint C Int z
366 -- we generate the equation
369 bind_fn tv | tv `elemVarSet` qtvs = BindMe
372 (ls1, rs1) = instFD fd clas_tvs tys1
373 (ls2, rs2) = instFD fd clas_tvs tys2
375 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
376 instFD (ls,rs) tvs tys
377 = (map lookup ls, map lookup rs)
379 env = zipVarEnv tvs tys
380 lookup tv = lookupVarEnv_NF env tv
384 checkInstCoverage :: Class -> [Type] -> Bool
385 -- Check that the Coverage Condition is obeyed in an instance decl
386 -- For example, if we have
387 -- class theta => C a b | a -> b
389 -- Then we require fv(t2) `subset` fv(t1)
390 -- See Note [Coverage Condition] below
392 checkInstCoverage clas inst_taus
395 (tyvars, fds) = classTvsFds clas
396 fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
398 (ls,rs) = instFD fd tyvars inst_taus
401 Note [Coverage condition]
402 ~~~~~~~~~~~~~~~~~~~~~~~~~
403 For the coverage condition, we used to require only that
404 fv(t2) `subset` oclose(fv(t1), theta)
407 class Mul a b c | a b -> c where
410 instance Mul Int Int Int where (.*.) = (*)
411 instance Mul Int Float Float where x .*. y = fromIntegral x * y
412 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
414 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
415 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
417 But it is a mistake to accept the instance because then this defn:
418 f = \ b x y -> if b then x .*. [y] else y
419 makes instance inference go into a loop, because it requires the constraint
423 %************************************************************************
425 Check that a new instance decl is OK wrt fundeps
427 %************************************************************************
429 Here is the bad case:
430 class C a b | a->b where ...
431 instance C Int Bool where ...
432 instance C Int Char where ...
434 The point is that a->b, so Int in the first parameter must uniquely
435 determine the second. In general, given the same class decl, and given
437 instance C s1 s2 where ...
438 instance C t1 t2 where ...
440 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
442 Matters are a little more complicated if there are free variables in
445 class D a b c | a -> b
446 instance D a b => D [(a,a)] [b] Int
447 instance D a b => D [a] [b] Bool
449 The instance decls don't overlap, because the third parameter keeps
450 them separate. But we want to make sure that given any constraint
456 checkFunDeps :: (InstEnv, InstEnv) -> Instance
457 -> Maybe [Instance] -- Nothing <=> ok
458 -- Just dfs <=> conflict with dfs
459 -- Check wheher adding DFunId would break functional-dependency constraints
460 -- Used only for instance decls defined in the module being compiled
461 checkFunDeps inst_envs ispec
462 | null bad_fundeps = Nothing
463 | otherwise = Just bad_fundeps
465 (ins_tvs, _, clas, ins_tys) = instanceHead ispec
466 ins_tv_set = mkVarSet ins_tvs
467 cls_inst_env = classInstances inst_envs clas
468 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
470 badFunDeps :: [Instance] -> Class
471 -> TyVarSet -> [Type] -- Proposed new instance type
473 badFunDeps cls_insts clas ins_tv_set ins_tys
475 [ ispec | fd <- fds, -- fds is often empty, so do this first!
476 let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
477 ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs,
478 is_tys = tys }) <- cls_insts,
479 -- Filter out ones that can't possibly match,
480 -- based on the head of the fundep
481 not (instanceCantMatch inst_tcs trimmed_tcs),
482 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set)
483 fd clas_tvs tys ins_tys)
486 (clas_tvs, fds) = classTvsFds clas
487 rough_tcs = roughMatchTcs ins_tys
488 eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
489 -- An single instance may appear twice in the un-nubbed conflict list
490 -- because it may conflict with more than one fundep. E.g.
491 -- class C a b c | a -> b, a -> c
492 -- instance C Int Bool Bool
493 -- instance C Int Char Char
494 -- The second instance conflicts with the first by *both* fundeps
496 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
497 -- Computing rough_tcs for a particular fundep
498 -- class C a b c | a -> b where ...
499 -- For each instance .... => C ta tb tc
500 -- we want to match only on the type ta; so our
501 -- rough-match thing must similarly be filtered.
502 -- Hence, we Nothing-ise the tb and tc types right here
503 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
504 = zipWith select clas_tvs mb_tcs
506 select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
507 | otherwise = Nothing