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