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