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"
30 import Data.Maybe ( isJust )
34 %************************************************************************
36 \subsection{Close type variables}
38 %************************************************************************
40 oclose(vs,C) The result of extending the set of tyvars vs
41 using the functional dependencies from C
43 grow(vs,C) The result of extend the set of tyvars vs
44 using all conceivable links from C.
46 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
47 Then grow(vs,C) = {a,b,c}
49 Note that grow(vs,C) `superset` grow(vs,simplify(C))
50 That is, simplfication can only shrink the result of grow.
53 oclose is conservative v `elem` oclose(vs,C)
54 one way: => v is definitely fixed by vs
56 grow is conservative if v might be fixed by vs
57 the other way: => v `elem` grow(vs,C)
59 ----------------------------------------------------------
60 (oclose preds tvs) closes the set of type variables tvs,
61 wrt functional dependencies in preds. The result is a superset
62 of the argument set. For example, if we have
63 class C a b | a->b where ...
65 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
66 because if we know x and y then that fixes z.
68 oclose is used (only) when generalising a type T; see extensive
71 Note [Important subtlety in oclose]
72 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
73 Consider (oclose (C Int t) {}), where class C a b | a->b
74 Then, since a->b, 't' is fully determined by Int, and the
75 uniform thing is to return {t}.
79 f x = e -- 'e' generates constraint (D s Int t)
81 Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
82 monomorphic in 't', thus
83 f :: forall s. D s Int t => s -> s
85 But if this function is never called, 't' will never be instantiated;
86 the functional dependencies that fix 't' may well be instance decls in
87 some importing module. But the top-level defaulting of unconstrained
88 type variables will fix t=GHC.Prim.Any, and that's simply a bug.
90 Conclusion: oclose only returns a type variable as "fixed" if it
91 depends on at least one type variable in the input fixed_tvs.
93 Remember, it's always sound for oclose to return a smaller set.
94 An interesting example is tcfail093, where we get this inferred type:
96 dup :: forall h. (Call (IO Int) h) => () -> Int -> h
97 This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
98 previously GHC rejected this saying 'no instance for Call (IO Int) h'.
99 But it's right on the borderline. If there was an extra, otherwise
100 uninvolved type variable, like 's' in the type of 'f' above, then
101 we must accept the function. So, for now anyway, we accept 'dup' too.
104 oclose :: [PredType] -> TyVarSet -> TyVarSet
105 oclose preds fixed_tvs
106 | null tv_fds = fixed_tvs -- Fast escape hatch for common case
107 | isEmptyVarSet fixed_tvs = emptyVarSet -- Note [Important subtlety in oclose]
108 | otherwise = loop fixed_tvs
111 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
112 | otherwise = loop new_fixed_tvs
114 new_fixed_tvs = foldl extend fixed_tvs tv_fds
116 extend fixed_tvs (ls,rs)
117 | not (isEmptyVarSet ls) -- Note [Important subtlety in oclose]
118 , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
119 | otherwise = fixed_tvs
121 tv_fds :: [(TyVarSet,TyVarSet)]
122 -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
123 -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
124 tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
125 | ClassP cls tys <- preds, -- Ignore implicit params
126 let (cls_tvs, cls_fds) = classTvsFds cls,
128 let (xs,ys) = instFD fd cls_tvs tys
132 Note [Growing the tau-tvs using constraints]
133 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
134 (grow preds tvs) is the result of extend the set of tyvars tvs
135 using all conceivable links from pred
137 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
138 Then grow precs tvs = {a,b,c}
140 All the type variables from an implicit parameter are added, whether or
141 not they are mentioned in tvs; see Note [Implicit parameters and ambiguity]
144 See also Note [Ambiguity] in TcSimplify
147 grow :: [PredType] -> TyVarSet -> TyVarSet
149 | null preds = real_fixed_tvs
150 | otherwise = loop real_fixed_tvs
152 -- Add the implicit parameters;
153 -- see Note [Implicit parameters and ambiguity] in TcSimplify
154 real_fixed_tvs = foldr unionVarSet fixed_tvs ip_tvs
157 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
158 | otherwise = loop new_fixed_tvs
160 new_fixed_tvs = foldl extend fixed_tvs non_ip_tvs
162 extend fixed_tvs pred_tvs
163 | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs
164 | otherwise = fixed_tvs
166 (ip_tvs, non_ip_tvs) = partitionWith get_ip preds
167 get_ip (IParam _ ty) = Left (tyVarsOfType ty)
168 get_ip other = Right (tyVarsOfPred other)
171 %************************************************************************
173 \subsection{Generate equations from functional dependencies}
175 %************************************************************************
179 type Equation = (TyVarSet, [(Type, Type)])
180 -- These pairs of types should be equal, for some
181 -- substitution of the tyvars in the tyvar set
182 -- INVARIANT: corresponding types aren't already equal
184 -- It's important that we have a *list* of pairs of types. Consider
185 -- class C a b c | a -> b c where ...
186 -- instance C Int x x where ...
187 -- Then, given the constraint (C Int Bool v) we should improve v to Bool,
188 -- via the equation ({x}, [(Bool,x), (v,x)])
189 -- This would not happen if the class had looked like
190 -- class C a b c | a -> b, a -> c
192 -- To "execute" the equation, make fresh type variable for each tyvar in the set,
193 -- instantiate the two types with these fresh variables, and then unify.
195 -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
196 -- We unify z with Int, but since a and b are quantified we do nothing to them
197 -- We usually act on an equation by instantiating the quantified type varaibles
198 -- to fresh type variables, and then calling the standard unifier.
200 pprEquation (qtvs, pairs)
201 = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
202 nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])]
205 Given a bunch of predicates that must hold, such as
207 C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
209 improve figures out what extra equations must hold.
210 For example, if we have
212 class C a b | a->b where ...
214 then improve will return
220 * improve does not iterate. It's possible that when we make
221 t1=t2, for example, that will in turn trigger a new equation.
222 This would happen if we also had
224 If t1=t2, we also get t7=t8.
226 improve does *not* do this extra step. It relies on the caller
229 * The equations unify types that are not already equal. So there
230 is no effect iff the result of improve is empty
235 type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
237 improveOne :: (Class -> [Instance]) -- Gives instances for given class
238 -> Pred_Loc -- Do improvement triggered by this
239 -> [Pred_Loc] -- Current constraints
240 -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
241 -- (NB the above INVARIANT for type Equation)
242 -- The Pred_Locs explain which two predicates were
243 -- combined (for error messages)
244 -- Just do improvement triggered by a single, distinguised predicate
246 improveOne inst_env pred@(IParam ip ty, _) preds
247 = [ ((emptyVarSet, [(ty,ty2)]), pred, p2)
248 | p2@(IParam ip2 ty2, _) <- preds
250 , not (ty `tcEqType` ty2)]
252 improveOne inst_env pred@(ClassP cls tys, _) preds
253 | tys `lengthAtLeast` 2
254 = instance_eqns ++ pairwise_eqns
255 -- NB: we put the instance equations first. This biases the
256 -- order so that we first improve individual constraints against the
257 -- instances (which are perhaps in a library and less likely to be
258 -- wrong; and THEN perform the pairwise checks.
259 -- The other way round, it's possible for the pairwise check to succeed
260 -- and cause a subsequent, misleading failure of one of the pair with an
261 -- instance declaration. See tcfail143.hs for an example
263 (cls_tvs, cls_fds) = classTvsFds cls
264 instances = inst_env cls
265 rough_tcs = roughMatchTcs tys
267 -- NOTE that we iterate over the fds first; they are typically
268 -- empty, which aborts the rest of the loop.
269 pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
270 pairwise_eqns -- This group comes from pairwise comparison
273 , p2@(ClassP cls2 tys2, _) <- preds
275 , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
278 instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
279 instance_eqns -- This group comes from comparing with instance decls
280 = [ (eqn, p_inst, pred)
281 | fd <- cls_fds -- Iterate through the fundeps first,
282 -- because there often are none!
283 , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
284 -- Trim the rough_tcs based on the head of the fundep.
285 -- Remember that instanceCantMatch treats both argumnents
286 -- symmetrically, so it's ok to trim the rough_tcs,
287 -- rather than trimming each inst_tcs in turn
288 , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
289 is_tcs = inst_tcs }) <- instances
290 , not (instanceCantMatch inst_tcs trimmed_tcs)
291 , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
292 , let p_inst = (mkClassPred cls tys_inst,
293 ptext SLIT("arising from the instance declaration at")
294 <+> ppr (getSrcLoc ispec))
297 improveOne inst_env eq_pred preds
301 checkClsFD :: TyVarSet -- Quantified type variables; see note below
302 -> FunDep TyVar -> [TyVar] -- One functional dependency from the class
306 checkClsFD qtvs fd clas_tvs tys1 tys2
307 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
308 -- to make the types match. For example, given
309 -- class C a b | a->b where ...
310 -- instance C (Maybe x) (Tree x) where ..
312 -- and an Inst of form (C (Maybe t1) t2),
313 -- then we will call checkClsFD with
315 -- qtvs = {x}, tys1 = [Maybe x, Tree x]
316 -- tys2 = [Maybe t1, t2]
318 -- We can instantiate x to t1, and then we want to force
319 -- (Tree x) [t1/x] :=: t2
321 -- This function is also used when matching two Insts (rather than an Inst
322 -- against an instance decl. In that case, qtvs is empty, and we are doing
325 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
326 -- For the one-sided matching case, the qtvs are just from the template,
327 -- so we get matching
329 = ASSERT2( length tys1 == length tys2 &&
330 length tys1 == length clas_tvs
331 , ppr tys1 <+> ppr tys2 )
333 case tcUnifyTys bind_fn ls1 ls2 of
335 Just subst | isJust (tcUnifyTys bind_fn rs1' rs2')
336 -- Don't include any equations that already hold.
337 -- Reason: then we know if any actual improvement has happened,
338 -- in which case we need to iterate the solver
339 -- In making this check we must taking account of the fact that any
340 -- qtvs that aren't already instantiated can be instantiated to anything
344 | otherwise -- Aha! A useful equation
345 -> [ (qtvs', zip rs1' rs2')]
346 -- We could avoid this substTy stuff by producing the eqn
347 -- (qtvs, ls1++rs1, ls2++rs2)
348 -- which will re-do the ls1/ls2 unification when the equation is
349 -- executed. What we're doing instead is recording the partial
350 -- work of the ls1/ls2 unification leaving a smaller unification problem
352 rs1' = substTys subst rs1
353 rs2' = substTys subst rs2
354 qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
355 -- qtvs' are the quantified type variables
356 -- that have not been substituted out
358 -- Eg. class C a b | a -> b
359 -- instance C Int [y]
360 -- Given constraint C Int z
361 -- we generate the equation
364 bind_fn tv | tv `elemVarSet` qtvs = BindMe
367 (ls1, rs1) = instFD fd clas_tvs tys1
368 (ls2, rs2) = instFD fd clas_tvs tys2
370 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
371 instFD (ls,rs) tvs tys
372 = (map lookup ls, map lookup rs)
374 env = zipVarEnv tvs tys
375 lookup tv = lookupVarEnv_NF env tv
379 checkInstCoverage :: Class -> [Type] -> Bool
380 -- Check that the Coverage Condition is obeyed in an instance decl
381 -- For example, if we have
382 -- class theta => C a b | a -> b
384 -- Then we require fv(t2) `subset` fv(t1)
385 -- See Note [Coverage Condition] below
387 checkInstCoverage clas inst_taus
390 (tyvars, fds) = classTvsFds clas
391 fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
393 (ls,rs) = instFD fd tyvars inst_taus
396 Note [Coverage condition]
397 ~~~~~~~~~~~~~~~~~~~~~~~~~
398 For the coverage condition, we used to require only that
399 fv(t2) `subset` oclose(fv(t1), theta)
402 class Mul a b c | a b -> c where
405 instance Mul Int Int Int where (.*.) = (*)
406 instance Mul Int Float Float where x .*. y = fromIntegral x * y
407 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
409 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
410 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
412 But it is a mistake to accept the instance because then this defn:
413 f = \ b x y -> if b then x .*. [y] else y
414 makes instance inference go into a loop, because it requires the constraint
418 %************************************************************************
420 Check that a new instance decl is OK wrt fundeps
422 %************************************************************************
424 Here is the bad case:
425 class C a b | a->b where ...
426 instance C Int Bool where ...
427 instance C Int Char where ...
429 The point is that a->b, so Int in the first parameter must uniquely
430 determine the second. In general, given the same class decl, and given
432 instance C s1 s2 where ...
433 instance C t1 t2 where ...
435 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
437 Matters are a little more complicated if there are free variables in
440 class D a b c | a -> b
441 instance D a b => D [(a,a)] [b] Int
442 instance D a b => D [a] [b] Bool
444 The instance decls don't overlap, because the third parameter keeps
445 them separate. But we want to make sure that given any constraint
451 checkFunDeps :: (InstEnv, InstEnv) -> Instance
452 -> Maybe [Instance] -- Nothing <=> ok
453 -- Just dfs <=> conflict with dfs
454 -- Check wheher adding DFunId would break functional-dependency constraints
455 -- Used only for instance decls defined in the module being compiled
456 checkFunDeps inst_envs ispec
457 | null bad_fundeps = Nothing
458 | otherwise = Just bad_fundeps
460 (ins_tvs, _, clas, ins_tys) = instanceHead ispec
461 ins_tv_set = mkVarSet ins_tvs
462 cls_inst_env = classInstances inst_envs clas
463 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
465 badFunDeps :: [Instance] -> Class
466 -> TyVarSet -> [Type] -- Proposed new instance type
468 badFunDeps cls_insts clas ins_tv_set ins_tys
469 = [ ispec | fd <- fds, -- fds is often empty
470 let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
471 ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs,
472 is_tys = tys }) <- cls_insts,
473 -- Filter out ones that can't possibly match,
474 -- based on the head of the fundep
475 not (instanceCantMatch inst_tcs trimmed_tcs),
476 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set)
477 fd clas_tvs tys ins_tys)
480 (clas_tvs, fds) = classTvsFds clas
481 rough_tcs = roughMatchTcs ins_tys
483 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
484 -- Computing rough_tcs for a particular fundep
485 -- class C a b c | a -> b where ...
486 -- For each instance .... => C ta tb tc
487 -- we want to match only on the types ta, tc; so our
488 -- rough-match thing must similarly be filtered.
489 -- Hence, we Nothing-ise the tb type right here
490 trimRoughMatchTcs clas_tvs (_,rtvs) mb_tcs
491 = zipWith select clas_tvs mb_tcs
493 select clas_tv mb_tc | clas_tv `elem` rtvs = Nothing