511472c66c7b5f823e9012f9898402e00c8ac4d4
[ghc.git] / compiler / types / FunDeps.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 2000
4 %
5
6 FunDeps - functional dependencies
7
8 It's better to read it as: "if we know these, then we're going to know these"
9
10 \begin{code}
11 module FunDeps (
12         Equation, pprEquation, 
13         oclose, improveFromInstEnv, improveFromAnother,
14         checkInstCoverage, checkFunDeps,
15         pprFundeps
16     ) where
17
18 #include "HsVersions.h"
19
20 import Name
21 import Var
22 import Class
23 import TcType
24 import Unify
25 import InstEnv
26 import VarSet
27 import VarEnv
28 import Outputable
29 import Util
30 import FastString
31
32 import Data.List        ( nubBy )
33 import Data.Maybe       ( isJust )
34 \end{code}
35
36
37 %************************************************************************
38 %*                                                                      *
39 \subsection{Close type variables}
40 %*                                                                      *
41 %************************************************************************
42
43   oclose(vs,C)  The result of extending the set of tyvars vs
44                 using the functional dependencies from C
45
46   grow(vs,C)    The result of extend the set of tyvars vs
47                 using all conceivable links from C.
48
49                 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
50                 Then grow(vs,C) = {a,b,c}
51
52                 Note that grow(vs,C) `superset` grow(vs,simplify(C))
53                 That is, simplfication can only shrink the result of grow.
54
55 Notice that
56    oclose is conservative       v `elem` oclose(vs,C)
57           one way:               => v is definitely fixed by vs
58
59    grow is conservative         if v might be fixed by vs 
60           the other way:        => v `elem` grow(vs,C)
61
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 ...
67 then
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.
70
71 oclose is used (only) when generalising a type T; see extensive
72 notes in TcSimplify.
73
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}.
79
80 However, consider
81         class D a b c | b->c
82         f x = e   -- 'e' generates constraint (D s Int t)
83                   -- \x.e has type s->s
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
87
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.
92
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.
95
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:
98     class C a b | a->b
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.
105
106 \begin{code}
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
112   where
113     loop fixed_tvs
114         | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
115         | otherwise                           = loop new_fixed_tvs
116         where
117           new_fixed_tvs = foldl extend fixed_tvs tv_fds
118
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
123
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,
130                 fd <- cls_fds,
131                 let (xs,ys) = instFD fd cls_tvs tys
132               ]
133 \end{code}
134
135     
136 %************************************************************************
137 %*                                                                      *
138 \subsection{Generate equations from functional dependencies}
139 %*                                                                      *
140 %************************************************************************
141
142
143 \begin{code}
144 type Equation = (TyVarSet, [(Type, Type)])
145 -- These pairs of types should be equal, for some
146 -- substitution of the tyvars in the tyvar set
147 -- INVARIANT: corresponding types aren't already equal
148
149 -- It's important that we have a *list* of pairs of types.  Consider
150 --      class C a b c | a -> b c where ...
151 --      instance C Int x x where ...
152 -- Then, given the constraint (C Int Bool v) we should improve v to Bool,
153 -- via the equation ({x}, [(Bool,x), (v,x)])
154 -- This would not happen if the class had looked like
155 --      class C a b c | a -> b, a -> c
156
157 -- To "execute" the equation, make fresh type variable for each tyvar in the set,
158 -- instantiate the two types with these fresh variables, and then unify.
159 --
160 -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
161 -- We unify z with Int, but since a and b are quantified we do nothing to them
162 -- We usually act on an equation by instantiating the quantified type varaibles
163 -- to fresh type variables, and then calling the standard unifier.
164
165 pprEquation :: Equation -> SDoc
166 pprEquation (qtvs, pairs) 
167   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
168           nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])]
169 \end{code}
170
171 Given a bunch of predicates that must hold, such as
172
173         C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
174
175 improve figures out what extra equations must hold.
176 For example, if we have
177
178         class C a b | a->b where ...
179
180 then improve will return
181
182         [(t1,t2), (t4,t5)]
183
184 NOTA BENE:
185
186   * improve does not iterate.  It's possible that when we make
187     t1=t2, for example, that will in turn trigger a new equation.
188     This would happen if we also had
189         C t1 t7, C t2 t8
190     If t1=t2, we also get t7=t8.
191
192     improve does *not* do this extra step.  It relies on the caller
193     doing so.
194
195   * The equations unify types that are not already equal.  So there
196     is no effect iff the result of improve is empty
197
198
199
200 \begin{code}
201 type Pred_Loc = (PredType, SDoc)        -- SDoc says where the Pred comes from
202
203 improveFromInstEnv :: (Class -> [Instance]) 
204                      -> Pred_Loc 
205                      -> [(Equation,Pred_Loc,Pred_Loc)]
206 -- Improvement from top-level instances 
207 improveFromInstEnv _inst_env pred 
208   = improveOne _inst_env pred []        -- TODO: Refactor to directly use instance_eqnd? 
209
210
211 improveFromAnother :: Pred_Loc
212                    -> Pred_Loc
213                    -> [(Equation, Pred_Loc, Pred_Loc)]
214 -- Improvement from another local (given or wanted) constraint
215 improveFromAnother pred1 pred2 
216   = improveOne (\_ -> []) pred1 [pred2] -- TODO: Refactor to directly use pairwise_eqns?
217
218
219 improveOne :: (Class -> [Instance])             -- Gives instances for given class
220            -> Pred_Loc                          -- Do improvement triggered by this
221            -> [Pred_Loc]                        -- Current constraints 
222            -> [(Equation,Pred_Loc,Pred_Loc)]    -- Derived equalities that must also hold
223                                                 -- (NB the above INVARIANT for type Equation)
224                                                 -- The Pred_Locs explain which two predicates were
225                                                 -- combined (for error messages)
226 -- Just do improvement triggered by a single, distinguised predicate
227
228 improveOne _inst_env pred@(IParam ip ty, _) preds
229   = [ ((emptyVarSet, [(ty,ty2)]), pred, p2) 
230     | p2@(IParam ip2 ty2, _) <- preds
231     , ip==ip2
232     , not (ty `tcEqType` ty2)]
233
234 improveOne inst_env pred@(ClassP cls tys, _) preds
235   | tys `lengthAtLeast` 2
236   = instance_eqns ++ pairwise_eqns
237         -- NB: we put the instance equations first.   This biases the 
238         -- order so that we first improve individual constraints against the
239         -- instances (which are perhaps in a library and less likely to be
240         -- wrong; and THEN perform the pairwise checks.
241         -- The other way round, it's possible for the pairwise check to succeed
242         -- and cause a subsequent, misleading failure of one of the pair with an
243         -- instance declaration.  See tcfail143.hs for an example
244   where
245     (cls_tvs, cls_fds) = classTvsFds cls
246     instances          = inst_env cls
247     rough_tcs          = roughMatchTcs tys
248
249         -- NOTE that we iterate over the fds first; they are typically
250         -- empty, which aborts the rest of the loop.
251     pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
252     pairwise_eqns       -- This group comes from pairwise comparison
253       = [ (eqn, pred, p2)
254         | fd <- cls_fds
255         , p2@(ClassP cls2 tys2, _) <- preds
256         , cls == cls2
257         , eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
258         ]
259
260     instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
261     instance_eqns       -- This group comes from comparing with instance decls
262       = [ (eqn, p_inst, pred)
263         | fd <- cls_fds         -- Iterate through the fundeps first, 
264                                 -- because there often are none!
265         , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
266                 -- Trim the rough_tcs based on the head of the fundep.
267                 -- Remember that instanceCantMatch treats both argumnents
268                 -- symmetrically, so it's ok to trim the rough_tcs,
269                 -- rather than trimming each inst_tcs in turn
270         , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst, 
271                             is_tcs = inst_tcs }) <- instances
272         , not (instanceCantMatch inst_tcs trimmed_tcs)
273         , eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
274         , let p_inst = (mkClassPred cls tys_inst, 
275                         sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
276                             , ptext (sLit "in the instance declaration at") 
277                                   <+> ppr (getSrcLoc ispec)])
278         ]
279
280 improveOne _ _ _
281   = []
282
283
284 checkClsFD :: TyVarSet                  -- Quantified type variables; see note below
285            -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
286            -> [Type] -> [Type]
287            -> [Equation]
288
289 checkClsFD qtvs fd clas_tvs tys1 tys2
290 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 
291 -- to make the types match.  For example, given
292 --      class C a b | a->b where ...
293 --      instance C (Maybe x) (Tree x) where ..
294 --
295 -- and an Inst of form (C (Maybe t1) t2), 
296 -- then we will call checkClsFD with
297 --
298 --      qtvs = {x}, tys1 = [Maybe x,  Tree x]
299 --                  tys2 = [Maybe t1, t2]
300 --
301 -- We can instantiate x to t1, and then we want to force
302 --      (Tree x) [t1/x]  ~   t2
303 --
304 -- This function is also used when matching two Insts (rather than an Inst
305 -- against an instance decl. In that case, qtvs is empty, and we are doing
306 -- an equality check
307 -- 
308 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
309 -- For the one-sided matching case, the qtvs are just from the template,
310 -- so we get matching
311 --
312   = ASSERT2( length tys1 == length tys2     && 
313              length tys1 == length clas_tvs 
314             , ppr tys1 <+> ppr tys2 )
315
316     case tcUnifyTys bind_fn ls1 ls2 of
317         Nothing  -> []
318         Just subst | isJust (tcUnifyTys bind_fn rs1' rs2') 
319                         -- Don't include any equations that already hold. 
320                         -- Reason: then we know if any actual improvement has happened,
321                         --         in which case we need to iterate the solver
322                         -- In making this check we must taking account of the fact that any 
323                         -- qtvs that aren't already instantiated can be instantiated to anything 
324                         -- at all
325                   -> []
326
327                   | otherwise   -- Aha!  A useful equation
328                   -> [ (qtvs', zip rs1' rs2')]
329                         -- We could avoid this substTy stuff by producing the eqn
330                         -- (qtvs, ls1++rs1, ls2++rs2)
331                         -- which will re-do the ls1/ls2 unification when the equation is
332                         -- executed.  What we're doing instead is recording the partial
333                         -- work of the ls1/ls2 unification leaving a smaller unification problem
334                   where
335                     rs1'  = substTys subst rs1 
336                     rs2'  = substTys subst rs2
337                     qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
338                         -- qtvs' are the quantified type variables
339                         -- that have not been substituted out
340                         --      
341                         -- Eg.  class C a b | a -> b
342                         --      instance C Int [y]
343                         -- Given constraint C Int z
344                         -- we generate the equation
345                         --      ({y}, [y], z)
346   where
347     bind_fn tv | tv `elemVarSet` qtvs = BindMe
348                | otherwise            = Skolem
349
350     (ls1, rs1) = instFD fd clas_tvs tys1
351     (ls2, rs2) = instFD fd clas_tvs tys2
352
353 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
354 instFD (ls,rs) tvs tys
355   = (map lookup ls, map lookup rs)
356   where
357     env       = zipVarEnv tvs tys
358     lookup tv = lookupVarEnv_NF env tv
359 \end{code}
360
361 \begin{code}
362 checkInstCoverage :: Class -> [Type] -> Bool
363 -- Check that the Coverage Condition is obeyed in an instance decl
364 -- For example, if we have 
365 --      class theta => C a b | a -> b
366 --      instance C t1 t2 
367 -- Then we require fv(t2) `subset` fv(t1)
368 -- See Note [Coverage Condition] below
369
370 checkInstCoverage clas inst_taus
371   = all fundep_ok fds
372   where
373     (tyvars, fds) = classTvsFds clas
374     fundep_ok fd  = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
375                  where
376                    (ls,rs) = instFD fd tyvars inst_taus
377 \end{code}
378
379 Note [Coverage condition]
380 ~~~~~~~~~~~~~~~~~~~~~~~~~
381 For the coverage condition, we used to require only that 
382         fv(t2) `subset` oclose(fv(t1), theta)
383
384 Example:
385         class Mul a b c | a b -> c where
386                 (.*.) :: a -> b -> c
387
388         instance Mul Int Int Int where (.*.) = (*)
389         instance Mul Int Float Float where x .*. y = fromIntegral x * y
390         instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
391
392 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
393 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
394
395 But it is a mistake to accept the instance because then this defn:
396         f = \ b x y -> if b then x .*. [y] else y
397 makes instance inference go into a loop, because it requires the constraint
398         Mul a [b] b
399
400
401 %************************************************************************
402 %*                                                                      *
403         Check that a new instance decl is OK wrt fundeps
404 %*                                                                      *
405 %************************************************************************
406
407 Here is the bad case:
408         class C a b | a->b where ...
409         instance C Int Bool where ...
410         instance C Int Char where ...
411
412 The point is that a->b, so Int in the first parameter must uniquely
413 determine the second.  In general, given the same class decl, and given
414
415         instance C s1 s2 where ...
416         instance C t1 t2 where ...
417
418 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
419
420 Matters are a little more complicated if there are free variables in
421 the s2/t2.  
422
423         class D a b c | a -> b
424         instance D a b => D [(a,a)] [b] Int
425         instance D a b => D [a]     [b] Bool
426
427 The instance decls don't overlap, because the third parameter keeps
428 them separate.  But we want to make sure that given any constraint
429         D s1 s2 s3
430 if s1 matches 
431
432
433 \begin{code}
434 checkFunDeps :: (InstEnv, InstEnv) -> Instance
435              -> Maybe [Instance]        -- Nothing  <=> ok
436                                         -- Just dfs <=> conflict with dfs
437 -- Check wheher adding DFunId would break functional-dependency constraints
438 -- Used only for instance decls defined in the module being compiled
439 checkFunDeps inst_envs ispec
440   | null bad_fundeps = Nothing
441   | otherwise        = Just bad_fundeps
442   where
443     (ins_tvs, _, clas, ins_tys) = instanceHead ispec
444     ins_tv_set   = mkVarSet ins_tvs
445     cls_inst_env = classInstances inst_envs clas
446     bad_fundeps  = badFunDeps cls_inst_env clas ins_tv_set ins_tys
447
448 badFunDeps :: [Instance] -> Class
449            -> TyVarSet -> [Type]        -- Proposed new instance type
450            -> [Instance]
451 badFunDeps cls_insts clas ins_tv_set ins_tys 
452   = nubBy eq_inst $
453     [ ispec | fd <- fds,        -- fds is often empty, so do this first!
454               let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
455               ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs, 
456                                 is_tys = tys }) <- cls_insts,
457                 -- Filter out ones that can't possibly match, 
458                 -- based on the head of the fundep
459               not (instanceCantMatch inst_tcs trimmed_tcs),     
460               notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) 
461                                    fd clas_tvs tys ins_tys)
462     ]
463   where
464     (clas_tvs, fds) = classTvsFds clas
465     rough_tcs = roughMatchTcs ins_tys
466     eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
467         -- An single instance may appear twice in the un-nubbed conflict list
468         -- because it may conflict with more than one fundep.  E.g.
469         --      class C a b c | a -> b, a -> c
470         --      instance C Int Bool Bool
471         --      instance C Int Char Char
472         -- The second instance conflicts with the first by *both* fundeps
473
474 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
475 -- Computing rough_tcs for a particular fundep
476 --     class C a b c | a -> b where ...
477 -- For each instance .... => C ta tb tc
478 -- we want to match only on the type ta; so our
479 -- rough-match thing must similarly be filtered.  
480 -- Hence, we Nothing-ise the tb and tc types right here
481 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
482   = zipWith select clas_tvs mb_tcs
483   where
484     select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
485                          | otherwise           = Nothing
486 \end{code}
487
488
489