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 -- The above warning supression flag is a temporary kludge.
13 -- While working on this module you are encouraged to remove it and fix
14 -- any warnings in the module. See
15 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
19 Equation, pprEquation,
20 oclose, grow, improveOne,
21 checkInstCoverage, checkFunDeps,
25 #include "HsVersions.h"
37 import Data.Maybe ( isJust )
41 %************************************************************************
43 \subsection{Close type variables}
45 %************************************************************************
47 oclose(vs,C) The result of extending the set of tyvars vs
48 using the functional dependencies from C
50 grow(vs,C) The result of extend the set of tyvars vs
51 using all conceivable links from C.
53 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
54 Then grow(vs,C) = {a,b,c}
56 Note that grow(vs,C) `superset` grow(vs,simplify(C))
57 That is, simplfication can only shrink the result of grow.
60 oclose is conservative v `elem` oclose(vs,C)
61 one way: => v is definitely fixed by vs
63 grow is conservative if v might be fixed by vs
64 the other way: => v `elem` grow(vs,C)
66 ----------------------------------------------------------
67 (oclose preds tvs) closes the set of type variables tvs,
68 wrt functional dependencies in preds. The result is a superset
69 of the argument set. For example, if we have
70 class C a b | a->b where ...
72 oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
73 because if we know x and y then that fixes z.
75 oclose is used (only) when generalising a type T; see extensive
78 Note [Important subtlety in oclose]
79 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
80 Consider (oclose (C Int t) {}), where class C a b | a->b
81 Then, since a->b, 't' is fully determined by Int, and the
82 uniform thing is to return {t}.
86 f x = e -- 'e' generates constraint (D s Int t)
88 Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
89 monomorphic in 't', thus
90 f :: forall s. D s Int t => s -> s
92 But if this function is never called, 't' will never be instantiated;
93 the functional dependencies that fix 't' may well be instance decls in
94 some importing module. But the top-level defaulting of unconstrained
95 type variables will fix t=GHC.Prim.Any, and that's simply a bug.
97 Conclusion: oclose only returns a type variable as "fixed" if it
98 depends on at least one type variable in the input fixed_tvs.
100 Remember, it's always sound for oclose to return a smaller set.
101 An interesting example is tcfail093, where we get this inferred type:
103 dup :: forall h. (Call (IO Int) h) => () -> Int -> h
104 This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
105 previously GHC rejected this saying 'no instance for Call (IO Int) h'.
106 But it's right on the borderline. If there was an extra, otherwise
107 uninvolved type variable, like 's' in the type of 'f' above, then
108 we must accept the function. So, for now anyway, we accept 'dup' too.
111 oclose :: [PredType] -> TyVarSet -> TyVarSet
112 oclose preds fixed_tvs
113 | null tv_fds = fixed_tvs -- Fast escape hatch for common case
114 | isEmptyVarSet fixed_tvs = emptyVarSet -- Note [Important subtlety in oclose]
115 | otherwise = loop fixed_tvs
118 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
119 | otherwise = loop new_fixed_tvs
121 new_fixed_tvs = foldl extend fixed_tvs tv_fds
123 extend fixed_tvs (ls,rs)
124 | not (isEmptyVarSet ls) -- Note [Important subtlety in oclose]
125 , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
126 | otherwise = fixed_tvs
128 tv_fds :: [(TyVarSet,TyVarSet)]
129 -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
130 -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
131 tv_fds = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
132 | ClassP cls tys <- preds, -- Ignore implicit params
133 let (cls_tvs, cls_fds) = classTvsFds cls,
135 let (xs,ys) = instFD fd cls_tvs tys
139 Note [Growing the tau-tvs using constraints]
140 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
141 (grow preds tvs) is the result of extend the set of tyvars tvs
142 using all conceivable links from pred
144 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
145 Then grow precs tvs = {a,b,c}
147 All the type variables from an implicit parameter are added, whether or
148 not they are mentioned in tvs; see Note [Implicit parameters and ambiguity]
151 See also Note [Ambiguity] in TcSimplify
154 grow :: [PredType] -> TyVarSet -> TyVarSet
156 | null preds = fixed_tvs
157 | otherwise = loop real_fixed_tvs
159 -- Add the implicit parameters;
160 -- see Note [Implicit parameters and ambiguity] in TcSimplify
161 real_fixed_tvs = foldr unionVarSet fixed_tvs ip_tvs
164 | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
165 | otherwise = loop new_fixed_tvs
167 new_fixed_tvs = foldl extend fixed_tvs non_ip_tvs
169 extend fixed_tvs pred_tvs
170 | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs
171 | otherwise = fixed_tvs
173 (ip_tvs, non_ip_tvs) = partitionWith get_ip preds
174 get_ip (IParam _ ty) = Left (tyVarsOfType ty)
175 get_ip other = Right (tyVarsOfPred other)
178 %************************************************************************
180 \subsection{Generate equations from functional dependencies}
182 %************************************************************************
186 type Equation = (TyVarSet, [(Type, Type)])
187 -- These pairs of types should be equal, for some
188 -- substitution of the tyvars in the tyvar set
189 -- INVARIANT: corresponding types aren't already equal
191 -- It's important that we have a *list* of pairs of types. Consider
192 -- class C a b c | a -> b c where ...
193 -- instance C Int x x where ...
194 -- Then, given the constraint (C Int Bool v) we should improve v to Bool,
195 -- via the equation ({x}, [(Bool,x), (v,x)])
196 -- This would not happen if the class had looked like
197 -- class C a b c | a -> b, a -> c
199 -- To "execute" the equation, make fresh type variable for each tyvar in the set,
200 -- instantiate the two types with these fresh variables, and then unify.
202 -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
203 -- We unify z with Int, but since a and b are quantified we do nothing to them
204 -- We usually act on an equation by instantiating the quantified type varaibles
205 -- to fresh type variables, and then calling the standard unifier.
207 pprEquation (qtvs, pairs)
208 = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
209 nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])]
212 Given a bunch of predicates that must hold, such as
214 C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
216 improve figures out what extra equations must hold.
217 For example, if we have
219 class C a b | a->b where ...
221 then improve will return
227 * improve does not iterate. It's possible that when we make
228 t1=t2, for example, that will in turn trigger a new equation.
229 This would happen if we also had
231 If t1=t2, we also get t7=t8.
233 improve does *not* do this extra step. It relies on the caller
236 * The equations unify types that are not already equal. So there
237 is no effect iff the result of improve is empty
242 type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
244 improveOne :: (Class -> [Instance]) -- Gives instances for given class
245 -> Pred_Loc -- Do improvement triggered by this
246 -> [Pred_Loc] -- Current constraints
247 -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
248 -- (NB the above INVARIANT for type Equation)
249 -- The Pred_Locs explain which two predicates were
250 -- combined (for error messages)
251 -- Just do improvement triggered by a single, distinguised predicate
253 improveOne inst_env pred@(IParam ip ty, _) preds
254 = [ ((emptyVarSet, [(ty,ty2)]), pred, p2)
255 | p2@(IParam ip2 ty2, _) <- preds
257 , not (ty `tcEqType` ty2)]
259 improveOne inst_env pred@(ClassP cls tys, _) preds
260 | tys `lengthAtLeast` 2
261 = instance_eqns ++ pairwise_eqns
262 -- NB: we put the instance equations first. This biases the
263 -- order so that we first improve individual constraints against the
264 -- instances (which are perhaps in a library and less likely to be
265 -- wrong; and THEN perform the pairwise checks.
266 -- The other way round, it's possible for the pairwise check to succeed
267 -- and cause a subsequent, misleading failure of one of the pair with an
268 -- instance declaration. See tcfail143.hs for an example
270 (cls_tvs, cls_fds) = classTvsFds cls
271 instances = inst_env cls
272 rough_tcs = roughMatchTcs tys
274 -- NOTE that we iterate over the fds first; they are typically
275 -- empty, which aborts the rest of the loop.
276 pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
277 pairwise_eqns -- This group comes from pairwise comparison
280 , p2@(ClassP cls2 tys2, _) <- preds
282 , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
285 instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
286 instance_eqns -- This group comes from comparing with instance decls
287 = [ (eqn, p_inst, pred)
288 | fd <- cls_fds -- Iterate through the fundeps first,
289 -- because there often are none!
290 , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
291 -- Trim the rough_tcs based on the head of the fundep.
292 -- Remember that instanceCantMatch treats both argumnents
293 -- symmetrically, so it's ok to trim the rough_tcs,
294 -- rather than trimming each inst_tcs in turn
295 , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
296 is_tcs = inst_tcs }) <- instances
297 , not (instanceCantMatch inst_tcs trimmed_tcs)
298 , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
299 , let p_inst = (mkClassPred cls tys_inst,
300 ptext SLIT("arising from the instance declaration at")
301 <+> ppr (getSrcLoc ispec))
304 improveOne inst_env eq_pred preds
308 checkClsFD :: TyVarSet -- Quantified type variables; see note below
309 -> FunDep TyVar -> [TyVar] -- One functional dependency from the class
313 checkClsFD qtvs fd clas_tvs tys1 tys2
314 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
315 -- to make the types match. For example, given
316 -- class C a b | a->b where ...
317 -- instance C (Maybe x) (Tree x) where ..
319 -- and an Inst of form (C (Maybe t1) t2),
320 -- then we will call checkClsFD with
322 -- qtvs = {x}, tys1 = [Maybe x, Tree x]
323 -- tys2 = [Maybe t1, t2]
325 -- We can instantiate x to t1, and then we want to force
326 -- (Tree x) [t1/x] :=: t2
328 -- This function is also used when matching two Insts (rather than an Inst
329 -- against an instance decl. In that case, qtvs is empty, and we are doing
332 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
333 -- For the one-sided matching case, the qtvs are just from the template,
334 -- so we get matching
336 = ASSERT2( length tys1 == length tys2 &&
337 length tys1 == length clas_tvs
338 , ppr tys1 <+> ppr tys2 )
340 case tcUnifyTys bind_fn ls1 ls2 of
342 Just subst | isJust (tcUnifyTys bind_fn rs1' rs2')
343 -- Don't include any equations that already hold.
344 -- Reason: then we know if any actual improvement has happened,
345 -- in which case we need to iterate the solver
346 -- In making this check we must taking account of the fact that any
347 -- qtvs that aren't already instantiated can be instantiated to anything
351 | otherwise -- Aha! A useful equation
352 -> [ (qtvs', zip rs1' rs2')]
353 -- We could avoid this substTy stuff by producing the eqn
354 -- (qtvs, ls1++rs1, ls2++rs2)
355 -- which will re-do the ls1/ls2 unification when the equation is
356 -- executed. What we're doing instead is recording the partial
357 -- work of the ls1/ls2 unification leaving a smaller unification problem
359 rs1' = substTys subst rs1
360 rs2' = substTys subst rs2
361 qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
362 -- qtvs' are the quantified type variables
363 -- that have not been substituted out
365 -- Eg. class C a b | a -> b
366 -- instance C Int [y]
367 -- Given constraint C Int z
368 -- we generate the equation
371 bind_fn tv | tv `elemVarSet` qtvs = BindMe
374 (ls1, rs1) = instFD fd clas_tvs tys1
375 (ls2, rs2) = instFD fd clas_tvs tys2
377 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
378 instFD (ls,rs) tvs tys
379 = (map lookup ls, map lookup rs)
381 env = zipVarEnv tvs tys
382 lookup tv = lookupVarEnv_NF env tv
386 checkInstCoverage :: Class -> [Type] -> Bool
387 -- Check that the Coverage Condition is obeyed in an instance decl
388 -- For example, if we have
389 -- class theta => C a b | a -> b
391 -- Then we require fv(t2) `subset` fv(t1)
392 -- See Note [Coverage Condition] below
394 checkInstCoverage clas inst_taus
397 (tyvars, fds) = classTvsFds clas
398 fundep_ok fd = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
400 (ls,rs) = instFD fd tyvars inst_taus
403 Note [Coverage condition]
404 ~~~~~~~~~~~~~~~~~~~~~~~~~
405 For the coverage condition, we used to require only that
406 fv(t2) `subset` oclose(fv(t1), theta)
409 class Mul a b c | a b -> c where
412 instance Mul Int Int Int where (.*.) = (*)
413 instance Mul Int Float Float where x .*. y = fromIntegral x * y
414 instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
416 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
417 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
419 But it is a mistake to accept the instance because then this defn:
420 f = \ b x y -> if b then x .*. [y] else y
421 makes instance inference go into a loop, because it requires the constraint
425 %************************************************************************
427 Check that a new instance decl is OK wrt fundeps
429 %************************************************************************
431 Here is the bad case:
432 class C a b | a->b where ...
433 instance C Int Bool where ...
434 instance C Int Char where ...
436 The point is that a->b, so Int in the first parameter must uniquely
437 determine the second. In general, given the same class decl, and given
439 instance C s1 s2 where ...
440 instance C t1 t2 where ...
442 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
444 Matters are a little more complicated if there are free variables in
447 class D a b c | a -> b
448 instance D a b => D [(a,a)] [b] Int
449 instance D a b => D [a] [b] Bool
451 The instance decls don't overlap, because the third parameter keeps
452 them separate. But we want to make sure that given any constraint
458 checkFunDeps :: (InstEnv, InstEnv) -> Instance
459 -> Maybe [Instance] -- Nothing <=> ok
460 -- Just dfs <=> conflict with dfs
461 -- Check wheher adding DFunId would break functional-dependency constraints
462 -- Used only for instance decls defined in the module being compiled
463 checkFunDeps inst_envs ispec
464 | null bad_fundeps = Nothing
465 | otherwise = Just bad_fundeps
467 (ins_tvs, _, clas, ins_tys) = instanceHead ispec
468 ins_tv_set = mkVarSet ins_tvs
469 cls_inst_env = classInstances inst_envs clas
470 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
472 badFunDeps :: [Instance] -> Class
473 -> TyVarSet -> [Type] -- Proposed new instance type
475 badFunDeps cls_insts clas ins_tv_set ins_tys
476 = [ ispec | fd <- fds, -- fds is often empty
477 let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
478 ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs,
479 is_tys = tys }) <- cls_insts,
480 -- Filter out ones that can't possibly match,
481 -- based on the head of the fundep
482 not (instanceCantMatch inst_tcs trimmed_tcs),
483 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set)
484 fd clas_tvs tys ins_tys)
487 (clas_tvs, fds) = classTvsFds clas
488 rough_tcs = roughMatchTcs ins_tys
490 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
491 -- Computing rough_tcs for a particular fundep
492 -- class C a b c | a -> b where ...
493 -- For each instance .... => C ta tb tc
494 -- we want to match only on the types ta, tc; so our
495 -- rough-match thing must similarly be filtered.
496 -- Hence, we Nothing-ise the tb type right here
497 trimRoughMatchTcs clas_tvs (_,rtvs) mb_tcs
498 = zipWith select clas_tvs mb_tcs
500 select clas_tv mb_tc | clas_tv `elem` rtvs = Nothing