Use "on the spot" solving for fundeps
[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         FDEq (..),
13         Equation(..), pprEquation,
14         oclose, improveFromInstEnv, improveFromAnother,
15         checkInstCoverage, checkFunDeps,
16         pprFundeps
17     ) where
18
19 #include "HsVersions.h"
20
21 import Name
22 import Var
23 import Class
24 import TcType
25 import Unify
26 import InstEnv
27 import VarSet
28 import VarEnv
29 import Outputable
30 import Util
31 import FastString
32
33 import Data.List        ( nubBy )
34 import Data.Maybe       ( isJust )
35 \end{code}
36
37
38 %************************************************************************
39 %*                                                                      *
40 \subsection{Close type variables}
41 %*                                                                      *
42 %************************************************************************
43
44   oclose(vs,C)  The result of extending the set of tyvars vs
45                 using the functional dependencies from C
46
47   grow(vs,C)    The result of extend the set of tyvars vs
48                 using all conceivable links from C.
49
50                 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
51                 Then grow(vs,C) = {a,b,c}
52
53                 Note that grow(vs,C) `superset` grow(vs,simplify(C))
54                 That is, simplfication can only shrink the result of grow.
55
56 Notice that
57    oclose is conservative       v `elem` oclose(vs,C)
58           one way:               => v is definitely fixed by vs
59
60    grow is conservative         if v might be fixed by vs 
61           the other way:        => v `elem` grow(vs,C)
62
63 ----------------------------------------------------------
64 (oclose preds tvs) closes the set of type variables tvs, 
65 wrt functional dependencies in preds.  The result is a superset
66 of the argument set.  For example, if we have
67         class C a b | a->b where ...
68 then
69         oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
70 because if we know x and y then that fixes z.
71
72 oclose is used (only) when generalising a type T; see extensive
73 notes in TcSimplify.
74
75 Note [Important subtlety in oclose]
76 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
77 Consider (oclose (C Int t) {}), where class C a b | a->b
78 Then, since a->b, 't' is fully determined by Int, and the
79 uniform thing is to return {t}.
80
81 However, consider
82         class D a b c | b->c
83         f x = e   -- 'e' generates constraint (D s Int t)
84                   -- \x.e has type s->s
85 Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
86 monomorphic in 't', thus
87         f :: forall s. D s Int t => s -> s
88
89 But if this function is never called, 't' will never be instantiated;
90 the functional dependencies that fix 't' may well be instance decls in
91 some importing module.  But the top-level defaulting of unconstrained
92 type variables will fix t=GHC.Prim.Any, and that's simply a bug.
93
94 Conclusion: oclose only returns a type variable as "fixed" if it 
95 depends on at least one type variable in the input fixed_tvs.
96
97 Remember, it's always sound for oclose to return a smaller set.
98 An interesting example is tcfail093, where we get this inferred type:
99     class C a b | a->b
100     dup :: forall h. (Call (IO Int) h) => () -> Int -> h
101 This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
102 previously GHC rejected this saying 'no instance for Call (IO Int) h'.
103 But it's right on the borderline. If there was an extra, otherwise
104 uninvolved type variable, like 's' in the type of 'f' above, then
105 we must accept the function.  So, for now anyway, we accept 'dup' too.
106
107 \begin{code}
108 oclose :: [PredType] -> TyVarSet -> TyVarSet
109 oclose preds fixed_tvs
110   | null tv_fds             = fixed_tvs    -- Fast escape hatch for common case
111   | isEmptyVarSet fixed_tvs = emptyVarSet  -- Note [Important subtlety in oclose]
112   | otherwise               = loop fixed_tvs
113   where
114     loop fixed_tvs
115         | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
116         | otherwise                           = loop new_fixed_tvs
117         where
118           new_fixed_tvs = foldl extend fixed_tvs tv_fds
119
120     extend fixed_tvs (ls,rs) 
121         | not (isEmptyVarSet ls)        -- Note [Important subtlety in oclose]
122         , ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
123         | otherwise                = fixed_tvs
124
125     tv_fds  :: [(TyVarSet,TyVarSet)]
126         -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
127         -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
128     tv_fds  = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
129               | ClassP cls tys <- preds,                -- Ignore implicit params
130                 let (cls_tvs, cls_fds) = classTvsFds cls,
131                 fd <- cls_fds,
132                 let (xs,ys) = instFD fd cls_tvs tys
133               ]
134 \end{code}
135
136     
137 %************************************************************************
138 %*                                                                      *
139 \subsection{Generate equations from functional dependencies}
140 %*                                                                      *
141 %************************************************************************
142
143
144 Each functional dependency with one variable in the RHS is responsible
145 for generating a single equality. For instance:
146      class C a b | a -> b
147 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha 
148      FDEq { fd_pos      = 1
149           , fd_ty_left  = Bool 
150           , fd_ty_right = alpha }
151 However notice that a functional dependency may have more than one variable
152 in the RHS which will create more than one FDEq. Example: 
153      class C a b c | a -> b c 
154      [Wanted] C Int alpha alpha 
155      [Wanted] C Int Bool beta 
156 Will generate: 
157         fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
158         fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
159
160 We record the paremeter position so that can immediately rewrite a constraint
161 using the produced FDEqs and remove it from our worklist.
162
163
164 INVARIANT: Corresponding types aren't already equal 
165 That is, there exists at least one non-identity equality in FDEqs. 
166
167 Assume:
168        class C a b c | a -> b c
169        instance C Int x x
170 And:   [Wanted] C Int Bool alpha
171 We will /match/ the LHS of fundep equations, producing a matching substitution
172 and create equations for the RHS sides. In our last example we'd have generated:
173       ({x}, [fd1,fd2])
174 where 
175        fd1 = FDEq 1 Bool x
176        fd2 = FDEq 2 alpha x
177 To ``execute'' the equation, make fresh type variable for each tyvar in the set,
178 instantiate the two types with these fresh variables, and then unify or generate 
179 a new constraint. In the above example we would generate a new unification 
180 variable 'beta' for x and produce the following constraints:
181      [Wanted] (Bool ~ beta)
182      [Wanted] (alpha ~ beta)
183
184 Notice the subtle difference between the above class declaration and:
185        class C a b c | a -> b, a -> c 
186 where we would generate: 
187       ({x},[fd1]),({x},[fd2]) 
188 This means that the template variable would be instantiated to different 
189 unification variables when producing the FD constraints. 
190
191 Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
192
193 \begin{code}
194 type Pred_Loc = (PredType, SDoc)        -- SDoc says where the Pred comes from
195
196 data Equation 
197    = FDEqn { fd_qtvs :: TyVarSet                -- Instantiate these to fresh unification vars
198            , fd_eqs  :: [FDEq]                  --   and then make these equal
199            , fd_pred1, fd_pred2 :: Pred_Loc }   -- The Equation arose from
200                                                 -- combining these two constraints
201
202 data FDEq = FDEq { fd_pos      :: Int -- We use '0' for the first position
203                  , fd_ty_left  :: Type
204                  , fd_ty_right :: Type }
205 \end{code}
206
207 Given a bunch of predicates that must hold, such as
208
209         C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
210
211 improve figures out what extra equations must hold.
212 For example, if we have
213
214         class C a b | a->b where ...
215
216 then improve will return
217
218         [(t1,t2), (t4,t5)]
219
220 NOTA BENE:
221
222   * improve does not iterate.  It's possible that when we make
223     t1=t2, for example, that will in turn trigger a new equation.
224     This would happen if we also had
225         C t1 t7, C t2 t8
226     If t1=t2, we also get t7=t8.
227
228     improve does *not* do this extra step.  It relies on the caller
229     doing so.
230
231   * The equations unify types that are not already equal.  So there
232     is no effect iff the result of improve is empty
233
234
235
236 \begin{code}
237 instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)]) 
238 -- Returns a FunDep between the types accompanied along with their 
239 -- position (<=0) in the types argument list.
240 instFD_WithPos (ls,rs) tvs tys
241   = (map (snd . lookup) ls, map lookup rs)
242   where
243     ind_tys   = zip [0..] tys 
244     env       = zipVarEnv tvs ind_tys
245     lookup tv = lookupVarEnv_NF env tv
246
247 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
248                    -> [Type] 
249                    -> [(Int,Type)] 
250                    -> [FDEq]
251 -- Create a list of FDEqs from two lists of types, making sure
252 -- that the types are not equal.
253 zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
254  | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
255  | otherwise = FDEq { fd_pos      = i2
256                     , fd_ty_left  = ty1
257                     , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
258 zipAndComputeFDEqs _ _ _ = [] 
259
260 -- Improve a class constraint from another class constraint
261 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
262 improveFromAnother :: Pred_Loc -- Template item (usually given, or inert) 
263                    -> Pred_Loc -- Workitem [that can be improved]
264                    -> [Equation]
265 -- Post: FDEqs always oriented from the other to the workitem 
266 --       Equations have empty quantified variables 
267 improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
268   | tys1 `lengthAtLeast` 2 && cls1 == cls2
269   = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
270     | let (cls_tvs, cls_fds) = classTvsFds cls1
271     , fd <- cls_fds
272     , let (ltys1, rs1)  = instFD         fd cls_tvs tys1
273           (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
274     , tcEqTypes ltys1 ltys2             -- The LHSs match
275     , let eqs = zipAndComputeFDEqs tcEqType rs1 irs2
276     , not (null eqs) ]
277
278 improveFromAnother _ _ = []
279
280
281 -- Improve a class constraint from instance declarations
282 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
283
284 pprEquation :: Equation -> SDoc
285 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs }) 
286   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
287           nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
288
289 improveFromInstEnv :: (InstEnv,InstEnv)
290                    -> Pred_Loc
291                    -> [Equation] -- Needs to be an Equation because
292                                  -- of quantified variables
293 -- Post: Equations oriented from the template (matching instance) to the workitem!
294 improveFromInstEnv _inst_env (pred,_loc)
295   | not (isClassPred pred)
296   = panic "improveFromInstEnv: not a class predicate"
297 improveFromInstEnv inst_env pred@(ClassP cls tys, _)
298   | tys `lengthAtLeast` 2
299   = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
300     | fd <- cls_fds             -- Iterate through the fundeps first,
301                                 -- because there often are none!
302     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
303                 -- Trim the rough_tcs based on the head of the fundep.
304                 -- Remember that instanceCantMatch treats both argumnents
305                 -- symmetrically, so it's ok to trim the rough_tcs,
306                 -- rather than trimming each inst_tcs in turn
307     , ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
308                         is_tcs = inst_tcs }) <- instances
309     , not (instanceCantMatch inst_tcs trimmed_tcs)
310     , let p_inst = (mkClassPred cls tys_inst,
311                     sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)  
312                         , ptext (sLit "in the instance declaration at")
313                                     <+> ppr (getSrcLoc ispec)])
314     , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
315     , not (null eqs)
316     ]
317   where 
318      (cls_tvs, cls_fds) = classTvsFds cls
319      instances          = classInstances inst_env cls
320      rough_tcs          = roughMatchTcs tys
321 improveFromInstEnv _ _ = []
322
323
324 checkClsFD :: TyVarSet                  -- Quantified type variables; see note below
325            -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
326            -> [Type] -> [Type]
327            -> [(TyVarSet, [FDEq])]
328
329 checkClsFD qtvs fd clas_tvs tys1 tys2
330 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 
331 -- to make the types match.  For example, given
332 --      class C a b | a->b where ...
333 --      instance C (Maybe x) (Tree x) where ..
334 --
335 -- and an Inst of form (C (Maybe t1) t2), 
336 -- then we will call checkClsFD with
337 --
338 --      qtvs = {x}, tys1 = [Maybe x,  Tree x]
339 --                  tys2 = [Maybe t1, t2]
340 --
341 -- We can instantiate x to t1, and then we want to force
342 --      (Tree x) [t1/x]  ~   t2
343 --
344 -- This function is also used when matching two Insts (rather than an Inst
345 -- against an instance decl. In that case, qtvs is empty, and we are doing
346 -- an equality check
347 -- 
348 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
349 -- For the one-sided matching case, the qtvs are just from the template,
350 -- so we get matching
351 --
352   = ASSERT2( length tys1 == length tys2     && 
353              length tys1 == length clas_tvs 
354             , ppr tys1 <+> ppr tys2 )
355
356     case tcUnifyTys bind_fn ltys1 ltys2 of
357         Nothing  -> []
358         Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
359                         -- Don't include any equations that already hold.
360                         -- Reason: then we know if any actual improvement has happened,
361                         --         in which case we need to iterate the solver
362                         -- In making this check we must taking account of the fact that any
363                         -- qtvs that aren't already instantiated can be instantiated to anything
364                         -- at all
365                         -- NB: We can't do this 'is-useful-equation' check element-wise 
366                         --     because of:
367                         --           class C a b c | a -> b c
368                         --           instance C Int x x
369                         --           [Wanted] C Int alpha Int
370                         -- We would get that  x -> alpha  (isJust) and x -> Int (isJust)
371                         -- so we would produce no FDs, which is clearly wrong. 
372                   -> [] 
373
374                   | otherwise
375                   -> [(qtvs', fdeqs)]
376                         -- We could avoid this substTy stuff by producing the eqn
377                         -- (qtvs, ls1++rs1, ls2++rs2)
378                         -- which will re-do the ls1/ls2 unification when the equation is
379                         -- executed.  What we're doing instead is recording the partial
380                         -- work of the ls1/ls2 unification leaving a smaller unification problem
381                   where
382                     rtys1' = map (substTy subst) rtys1
383                     irs2'  = map (\(i,x) -> (i,substTy subst x)) irs2
384                     rtys2' = map snd irs2'
385  
386                     fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
387                         -- Don't discard anything! 
388                         -- We could discard equal types but it's an overkill to call 
389                         -- tcEqType again, since we know for sure that /at least one/ 
390                         -- equation in there is useful)
391
392                     qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
393                         -- qtvs' are the quantified type variables
394                         -- that have not been substituted out
395                         --      
396                         -- Eg.  class C a b | a -> b
397                         --      instance C Int [y]
398                         -- Given constraint C Int z
399                         -- we generate the equation
400                         --      ({y}, [y], z)
401   where
402     bind_fn tv | tv `elemVarSet` qtvs = BindMe
403                | otherwise            = Skolem
404
405     (ltys1, rtys1) = instFD         fd clas_tvs tys1
406     (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys2
407 \end{code}
408
409
410 \begin{code}
411 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
412 -- A simpler version of instFD_WithPos to be used in checking instance coverage etc.
413 instFD (ls,rs) tvs tys
414   = (map lookup ls, map lookup rs)
415   where
416     env       = zipVarEnv tvs tys
417     lookup tv = lookupVarEnv_NF env tv
418
419 checkInstCoverage :: Class -> [Type] -> Bool
420 -- Check that the Coverage Condition is obeyed in an instance decl
421 -- For example, if we have 
422 --      class theta => C a b | a -> b
423 --      instance C t1 t2 
424 -- Then we require fv(t2) `subset` fv(t1)
425 -- See Note [Coverage Condition] below
426
427 checkInstCoverage clas inst_taus
428   = all fundep_ok fds
429   where
430     (tyvars, fds) = classTvsFds clas
431     fundep_ok fd  = tyVarsOfTypes rs `subVarSet` tyVarsOfTypes ls
432                  where
433                    (ls,rs) = instFD fd tyvars inst_taus
434 \end{code}
435
436 Note [Coverage condition]
437 ~~~~~~~~~~~~~~~~~~~~~~~~~
438 For the coverage condition, we used to require only that 
439         fv(t2) `subset` oclose(fv(t1), theta)
440
441 Example:
442         class Mul a b c | a b -> c where
443                 (.*.) :: a -> b -> c
444
445         instance Mul Int Int Int where (.*.) = (*)
446         instance Mul Int Float Float where x .*. y = fromIntegral x * y
447         instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
448
449 In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
450 But it is the case that fv([c]) `subset` oclose( theta, fv(a,[b]) )
451
452 But it is a mistake to accept the instance because then this defn:
453         f = \ b x y -> if b then x .*. [y] else y
454 makes instance inference go into a loop, because it requires the constraint
455         Mul a [b] b
456
457
458 %************************************************************************
459 %*                                                                      *
460         Check that a new instance decl is OK wrt fundeps
461 %*                                                                      *
462 %************************************************************************
463
464 Here is the bad case:
465         class C a b | a->b where ...
466         instance C Int Bool where ...
467         instance C Int Char where ...
468
469 The point is that a->b, so Int in the first parameter must uniquely
470 determine the second.  In general, given the same class decl, and given
471
472         instance C s1 s2 where ...
473         instance C t1 t2 where ...
474
475 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
476
477 Matters are a little more complicated if there are free variables in
478 the s2/t2.  
479
480         class D a b c | a -> b
481         instance D a b => D [(a,a)] [b] Int
482         instance D a b => D [a]     [b] Bool
483
484 The instance decls don't overlap, because the third parameter keeps
485 them separate.  But we want to make sure that given any constraint
486         D s1 s2 s3
487 if s1 matches 
488
489
490 \begin{code}
491 checkFunDeps :: (InstEnv, InstEnv) -> Instance
492              -> Maybe [Instance]        -- Nothing  <=> ok
493                                         -- Just dfs <=> conflict with dfs
494 -- Check wheher adding DFunId would break functional-dependency constraints
495 -- Used only for instance decls defined in the module being compiled
496 checkFunDeps inst_envs ispec
497   | null bad_fundeps = Nothing
498   | otherwise        = Just bad_fundeps
499   where
500     (ins_tvs, _, clas, ins_tys) = instanceHead ispec
501     ins_tv_set   = mkVarSet ins_tvs
502     cls_inst_env = classInstances inst_envs clas
503     bad_fundeps  = badFunDeps cls_inst_env clas ins_tv_set ins_tys
504
505 badFunDeps :: [Instance] -> Class
506            -> TyVarSet -> [Type]        -- Proposed new instance type
507            -> [Instance]
508 badFunDeps cls_insts clas ins_tv_set ins_tys 
509   = nubBy eq_inst $
510     [ ispec | fd <- fds,        -- fds is often empty, so do this first!
511               let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
512               ispec@(Instance { is_tcs = inst_tcs, is_tvs = tvs, 
513                                 is_tys = tys }) <- cls_insts,
514                 -- Filter out ones that can't possibly match, 
515                 -- based on the head of the fundep
516               not (instanceCantMatch inst_tcs trimmed_tcs),     
517               notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) 
518                                    fd clas_tvs tys ins_tys)
519     ]
520   where
521     (clas_tvs, fds) = classTvsFds clas
522     rough_tcs = roughMatchTcs ins_tys
523     eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
524         -- An single instance may appear twice in the un-nubbed conflict list
525         -- because it may conflict with more than one fundep.  E.g.
526         --      class C a b c | a -> b, a -> c
527         --      instance C Int Bool Bool
528         --      instance C Int Char Char
529         -- The second instance conflicts with the first by *both* fundeps
530
531 trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
532 -- Computing rough_tcs for a particular fundep
533 --     class C a b c | a -> b where ...
534 -- For each instance .... => C ta tb tc
535 -- we want to match only on the type ta; so our
536 -- rough-match thing must similarly be filtered.  
537 -- Hence, we Nothing-ise the tb and tc types right here
538 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
539   = zipWith select clas_tvs mb_tcs
540   where
541     select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
542                          | otherwise           = Nothing
543 \end{code}
544
545
546