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