1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 2000
4 %
6 FunDeps - functional dependencies
8 It's better to read it as: "if we know these, then we're going to know these"
10 \begin{code}
11 module FunDeps (
12         FDEq (..),
13         Equation(..), pprEquation,
14         oclose, improveFromInstEnv, improveFromAnother,
15         checkInstCoverage, checkFunDeps,
16         pprFundeps
17     ) where
19 #include "HsVersions.h"
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
33 import Data.List        ( nubBy )
34 import Data.Maybe       ( isJust )
35 \end{code}
38 %************************************************************************
39 %*                                                                      *
40 \subsection{Close type variables}
41 %*                                                                      *
42 %************************************************************************
44   oclose(vs,C)  The result of extending the set of tyvars vs
45                 using the functional dependencies from C
47   grow(vs,C)    The result of extend the set of tyvars vs
48                 using all conceivable links from C.
50                 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
51                 Then grow(vs,C) = {a,b,c}
53                 Note that grow(vs,C) superset grow(vs,simplify(C))
54                 That is, simplfication can only shrink the result of grow.
56 Notice that
57    oclose is conservative       v elem oclose(vs,C)
58           one way:               => v is definitely fixed by vs
60    grow is conservative         if v might be fixed by vs
61           the other way:        => v elem grow(vs,C)
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.
72 oclose is used (only) when generalising a type T; see extensive
73 notes in TcSimplify.
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}.
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
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.
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.
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.
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
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
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}
137 %************************************************************************
138 %*                                                                      *
139 \subsection{Generate equations from functional dependencies}
140 %*                                                                      *
141 %************************************************************************
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 }
160 We record the paremeter position so that can immediately rewrite a constraint
161 using the produced FDEqs and remove it from our worklist.
164 INVARIANT: Corresponding types aren't already equal
165 That is, there exists at least one non-identity equality in FDEqs.
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)
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.
191 Finally, the position parameters will help us rewrite the wanted constraint on the spot''
193 \begin{code}
194 type Pred_Loc = (PredType, SDoc)        -- SDoc says where the Pred comes from
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
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}
207 Given a bunch of predicates that must hold, such as
209         C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
211 improve figures out what extra equations must hold.
212 For example, if we have
214         class C a b | a->b where ...
216 then improve will return
218         [(t1,t2), (t4,t5)]
220 NOTA BENE:
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.
228     improve does *not* do this extra step.  It relies on the caller
229     doing so.
231   * The equations unify types that are not already equal.  So there
232     is no effect iff the result of improve is empty
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
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.
255  | otherwise = FDEq { fd_pos      = i2
256                     , fd_ty_left  = ty1
257                     , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
258 zipAndComputeFDEqs _ _ _ = []
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) ]
278 improveFromAnother _ _ = []
281 -- Improve a class constraint from instance declarations
282 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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])]
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 _ _ = []
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])]
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 )
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                   -> []
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'
386                     fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
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)
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
405     (ltys1, rtys1) = instFD         fd clas_tvs tys1
406     (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys2
407 \end{code}
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
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
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}
436 Note [Coverage condition]
437 ~~~~~~~~~~~~~~~~~~~~~~~~~
438 For the coverage condition, we used to require only that
439         fv(t2) subset oclose(fv(t1), theta)
441 Example:
442         class Mul a b c | a b -> c where
443                 (.*.) :: a -> b -> c
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
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]) )
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
458 %************************************************************************
459 %*                                                                      *
460         Check that a new instance decl is OK wrt fundeps
461 %*                                                                      *
462 %************************************************************************
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 ...
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
472         instance C s1 s2 where ...
473         instance C t1 t2 where ...
475 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
477 Matters are a little more complicated if there are free variables in
478 the s2/t2.
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
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
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
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
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}