ghc/compiler/types/FunDeps.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 2000
   3 %
   4 \section[FunDeps]{FunDeps - functional dependencies}
   5
   6 It's better to read it as: "if we know these, then we're going to know these"
   7
   8 \begin{code}
   9 module FunDeps (
  10         oclose, grow, improve, checkInstFDs, checkClsFD, pprFundeps
  11     ) where
  12
  13 #include "HsVersions.h"
  14
  15 import Name             ( getSrcLoc )
  16 import Var              ( Id, TyVar )
  17 import Class            ( Class, FunDep, classTvsFds )
  18 import Type             ( Type, ThetaType, PredType(..), predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
  19 import Subst            ( mkSubst, emptyInScopeSet, substTy )
  20 import Unify            ( unifyTyListsX, unifyExtendTysX )
  21 import VarSet
  22 import VarEnv
  23 import Outputable
  24 import List             ( tails )
  25 import Maybes           ( maybeToBool )
  26 import ListSetOps       ( equivClassesByUniq )
  27 \end{code}
  28
  29
  30 %************************************************************************
  31 %*                                                                      *
  32 \subsection{Close type variables}
  33 %*                                                                      *
  34 %************************************************************************
  35
  36 (oclose preds tvs) closes the set of type variables tvs,
  37 wrt functional dependencies in preds.  The result is a superset
  38 of the argument set.  For example, if we have
  39         class C a b | a->b where ...
  40 then
  41         oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
  42 because if we know x and y then that fixes z.
  43
  44 Using oclose
  45 ~~~~~~~~~~~~
  46 oclose is used
  47
  48 a) When determining ambiguity.  The type
  49         forall a,b. C a b => a
  50 is not ambiguous (given the above class decl for C) because
  51 a determines b.
  52
  53 b) When generalising a type T.  Usually we take FV(T) \ FV(Env),
  54 but in fact we need
  55         FV(T) \ (FV(Env)+)
  56 where the '+' is the oclosure operation.  Notice that we do not
  57 take FV(T)+.  This puzzled me for a bit.  Consider
  58
  59         f = E
  60
  61 and suppose e have that E :: C a b => a, and suppose that b is
  62 free in the environment. Then we quantify over 'a' only, giving
  63 the type forall a. C a b => a.  Since a->b but we don't have b->a,
  64 we might have instance decls like
  65         instance C Bool Int where ...
  66         instance C Char Int where ...
  67 so knowing that b=Int doesn't fix 'a'; so we quantify over it.
  68
  69                 ---------------
  70                 A WORRY: ToDo!
  71                 ---------------
  72 If we have      class C a b => D a b where ....
  73                 class D a b | a -> b where ...
  74 and the preds are [C (x,y) z], then we want to see the fd in D,
  75 even though it is not explicit in C, giving [({x,y},{z})]
  76
  77 Similarly for instance decls?  E.g. Suppose we have
  78         instance C a b => Eq (T a b) where ...
  79 and we infer a type t with constraints Eq (T a b) for a particular
  80 expression, and suppose that 'a' is free in the environment.
  81 We could generalise to
  82         forall b. Eq (T a b) => t
  83 but if we reduced the constraint, to C a b, we'd see that 'a' determines
  84 b, so that a better type might be
  85         t (with free constraint C a b)
  86 Perhaps it doesn't matter, because we'll still force b to be a
  87 particular type at the call sites.  Generalising over too many
  88 variables (provided we don't shadow anything by quantifying over a
  89 variable that is actually free in the envt) may postpone errors; it
  90 won't hide them altogether.
  91
  92
  93 \begin{code}
  94 oclose :: [PredType] -> TyVarSet -> TyVarSet
  95 oclose preds fixed_tvs
  96   | null tv_fds = fixed_tvs     -- Fast escape hatch for common case
  97   | otherwise   = loop fixed_tvs
  98   where
  99     loop fixed_tvs
 100         | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
 101         | otherwise                           = loop new_fixed_tvs
 102         where
 103           new_fixed_tvs = foldl extend fixed_tvs tv_fds
 104
 105     extend fixed_tvs (ls,rs) | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
 106                              | otherwise                = fixed_tvs
 107
 108     tv_fds  :: [(TyVarSet,TyVarSet)]
 109         -- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
 110         -- Meaning "knowing x,y fixes z, knowing x,p fixes q"
 111     tv_fds  = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
 112               | ClassP cls tys <- preds,                -- Ignore implicit params
 113                 let (cls_tvs, cls_fds) = classTvsFds cls,
 114                 fd <- cls_fds,
 115                 let (xs,ys) = instFD fd cls_tvs tys
 116               ]
 117 \end{code}
 118
 119 \begin{code}
 120 grow :: [PredType] -> TyVarSet -> TyVarSet
 121 grow preds fixed_tvs
 122   | null pred_sets = fixed_tvs
 123   | otherwise      = loop fixed_tvs
 124   where
 125     loop fixed_tvs
 126         | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
 127         | otherwise                           = loop new_fixed_tvs
 128         where
 129           new_fixed_tvs = foldl extend fixed_tvs pred_sets
 130
 131     extend fixed_tvs pred_tvs
 132         | fixed_tvs `intersectsVarSet` pred_tvs = fixed_tvs `unionVarSet` pred_tvs
 133         | otherwise                             = fixed_tvs
 134
 135     pred_sets = [tyVarsOfPred pred | pred <- preds]
 136 \end{code}
 137
 138 %************************************************************************
 139 %*                                                                      *
 140 \subsection{Generate equations from functional dependencies}
 141 %*                                                                      *
 142 %************************************************************************
 143
 144
 145 \begin{code}
 146 ----------
 147 type Equation = (TyVarSet, Type, Type)  -- These two types should be equal, for some
 148                                         -- substitution of the tyvars in the tyvar set
 149         -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
 150         -- We unify z with Int, but since a and b are quantified we do nothing to them
 151         -- We usually act on an equation by instantiating the quantified type varaibles
 152         -- to fresh type variables, and then calling the standard unifier.
 153         --
 154         -- INVARIANT: they aren't already equal
 155         --
 156
 157
 158
 159 ----------
 160 improve :: InstEnv Id           -- Gives instances for given class
 161         -> [(PredType,SDoc)]    -- Current constraints; doc says where they come from
 162         -> [(Equation,SDoc)]    -- Derived equalities that must also hold
 163                                 -- (NB the above INVARIANT for type Equation)
 164                                 -- The SDoc explains why the equation holds (for error messages)
 165
 166 type InstEnv a = Class -> [(TyVarSet, [Type], a)]
 167 -- This is a bit clumsy, because InstEnv is really
 168 -- defined in module InstEnv.  However, we don't want
 169 -- to define it (and ClsInstEnv) here because InstEnv
 170 -- is their home.  Nor do we want to make a recursive
 171 -- module group (InstEnv imports stuff from FunDeps).
 172 \end{code}
 173
 174 Given a bunch of predicates that must hold, such as
 175
 176         C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
 177
 178 improve figures out what extra equations must hold.
 179 For example, if we have
 180
 181         class C a b | a->b where ...
 182
 183 then improve will return
 184
 185         [(t1,t2), (t4,t5)]
 186
 187 NOTA BENE:
 188
 189   * improve does not iterate.  It's possible that when we make
 190     t1=t2, for example, that will in turn trigger a new equation.
 191     This would happen if we also had
 192         C t1 t7, C t2 t8
 193     If t1=t2, we also get t7=t8.
 194
 195     improve does *not* do this extra step.  It relies on the caller
 196     doing so.
 197
 198   * The equations unify types that are not already equal.  So there
 199     is no effect iff the result of improve is empty
 200
 201
 202
 203 \begin{code}
 204 improve inst_env preds
 205   = [ eqn | group <- equivClassesByUniq (predTyUnique . fst) preds,
 206             eqn   <- checkGroup inst_env group ]
 207
 208 ----------
 209 checkGroup :: InstEnv Id -> [(PredType,SDoc)] -> [(Equation, SDoc)]
 210   -- The preds are all for the same class or implicit param
 211
 212 checkGroup inst_env (p1@(IParam _ ty, _) : ips)
 213   =     -- For implicit parameters, all the types must match
 214     [((emptyVarSet, ty, ty'), mkEqnMsg p1 p2) | p2@(IParam _ ty', _) <- ips, ty /= ty']
 215
 216 checkGroup inst_env clss@((ClassP cls _, _) : _)
 217   =     -- For classes life is more complicated
 218         -- Suppose the class is like
 219         --      classs C as | (l1 -> r1), (l2 -> r2), ... where ...
 220         -- Then FOR EACH PAIR (ClassP c tys1, ClassP c tys2) in the list clss
 221         -- we check whether
 222         --      U l1[tys1/as] = U l2[tys2/as]
 223         --  (where U is a unifier)
 224         --
 225         -- If so, we return the pair
 226         --      U r1[tys1/as] = U l2[tys2/as]
 227         --
 228         -- We need to do something very similar comparing each predicate
 229         -- with relevant instance decls
 230     pairwise_eqns ++ instance_eqns
 231
 232   where
 233     (cls_tvs, cls_fds) = classTvsFds cls
 234     cls_inst_env       = inst_env cls
 235
 236         -- NOTE that we iterate over the fds first; they are typically
 237         -- empty, which aborts the rest of the loop.
 238     pairwise_eqns :: [(Equation,SDoc)]
 239     pairwise_eqns       -- This group comes from pairwise comparison
 240       = [ (eqn, mkEqnMsg p1 p2)
 241         | fd <- cls_fds,
 242           p1@(ClassP _ tys1, _) : rest <- tails clss,
 243           p2@(ClassP _ tys2, _) <- rest,
 244           eqn <- checkClsFD emptyVarSet fd cls_tvs tys1 tys2
 245         ]
 246
 247     instance_eqns :: [(Equation,SDoc)]
 248     instance_eqns       -- This group comes from comparing with instance decls
 249       = [ (eqn, mkEqnMsg p1 p2)
 250         | fd <- cls_fds,
 251           (qtvs, tys1, dfun_id)  <- cls_inst_env,
 252           let p1 = (mkClassPred cls tys1,
 253                     ptext SLIT("arising from the instance declaration at") <+> ppr (getSrcLoc dfun_id)),
 254           p2@(ClassP _ tys2, _) <- clss,
 255           eqn <- checkClsFD qtvs fd cls_tvs tys1 tys2
 256         ]
 257
 258 mkEqnMsg (pred1,from1) (pred2,from2)
 259   = vcat [ptext SLIT("When using functional dependencies to combine"),
 260           nest 2 (sep [ppr pred1 <> comma, nest 2 from1]),
 261           nest 2 (sep [ppr pred2 <> comma, nest 2 from2])]
 262
 263 ----------
 264 checkClsFD :: TyVarSet                  -- The quantified type variables, which
 265                                         -- can be instantiated to make the types match
 266            -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
 267            -> [Type] -> [Type]
 268            -> [Equation]
 269
 270 checkClsFD qtvs fd clas_tvs tys1 tys2
 271 -- We use 'unify' even though we are often only matching
 272 -- unifyTyListsX will only bind variables in qtvs, so it's OK!
 273   = case unifyTyListsX qtvs ls1 ls2 of
 274         Nothing   -> []
 275         Just unif -> [ (qtvs', substTy full_unif r1, substTy full_unif r2)
 276                      | (r1,r2) <- rs1 `zip` rs2,
 277                        not (maybeToBool (unifyExtendTysX qtvs unif r1 r2))]
 278                   where
 279                     full_unif = mkSubst emptyInScopeSet unif
 280                         -- No for-alls in sight; hmm
 281
 282                     qtvs' = filterVarSet (\v -> not (v `elemSubstEnv` unif)) qtvs
 283                         -- qtvs' are the quantified type variables
 284                         -- that have not been substituted out
 285   where
 286     (ls1, rs1) = instFD fd clas_tvs tys1
 287     (ls2, rs2) = instFD fd clas_tvs tys2
 288
 289 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
 290 instFD (ls,rs) tvs tys
 291   = (map lookup ls, map lookup rs)
 292   where
 293     env       = zipVarEnv tvs tys
 294     lookup tv = lookupVarEnv_NF env tv
 295 \end{code}
 296
 297 \begin{code}
 298 checkInstFDs :: ThetaType -> Class -> [Type] -> Bool
 299 -- Check that functional dependencies are obeyed in an instance decl
 300 -- For example, if we have
 301 --      class theta => C a b | a -> b
 302 --      instance C t1 t2
 303 -- Then we require fv(t2) `subset` oclose(fv(t1), theta)
 304
 305 checkInstFDs theta clas inst_taus
 306   = all fundep_ok fds
 307   where
 308     (tyvars, fds) = classTvsFds clas
 309     fundep_ok fd  = tyVarsOfTypes rs `subVarSet` oclose theta (tyVarsOfTypes ls)
 310                  where
 311                    (ls,rs) = instFD fd tyvars inst_taus
 312 \end{code}
 313
 314 %************************************************************************
 315 %*                                                                      *
 316 \subsection{Miscellaneous}
 317 %*                                                                      *
 318 %************************************************************************
 319
 320 \begin{code}
 321 pprFundeps :: Outputable a => [FunDep a] -> SDoc
 322 pprFundeps [] = empty
 323 pprFundeps fds = hsep (ptext SLIT("|") : punctuate comma (map ppr_fd fds))
 324
 325 ppr_fd (us, vs) = hsep [interppSP us, ptext SLIT("->"), interppSP vs]
 326 \end{code}