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