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