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         -- To "execute" the equation, make fresh type variable for each tyvar in the set,
 154         -- instantiate the two types with these fresh variables, and then unify.
 155         --
 156         -- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
 157         -- We unify z with Int, but since a and b are quantified we do nothing to them
 158         -- We usually act on an equation by instantiating the quantified type varaibles
 159         -- to fresh type variables, and then calling the standard unifier.
 160         --
 161         -- INVARIANT: they aren't already equal
 162         --
 163
 164
 165 pprEquationDoc (eqn, doc) = vcat [pprEquation eqn, nest 2 doc]
 166
 167 pprEquation (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
 168                                                   <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2
 169
 170 ----------
 171 improve :: InstEnv Id           -- Gives instances for given class
 172         -> [(PredType,SDoc)]    -- Current constraints; doc says where they come from
 173         -> [(Equation,SDoc)]    -- Derived equalities that must also hold
 174                                 -- (NB the above INVARIANT for type Equation)
 175                                 -- The SDoc explains why the equation holds (for error messages)
 176
 177 type InstEnv a = Class -> [(TyVarSet, [Type], a)]
 178 -- This is a bit clumsy, because InstEnv is really
 179 -- defined in module InstEnv.  However, we don't want
 180 -- to define it (and ClsInstEnv) here because InstEnv
 181 -- is their home.  Nor do we want to make a recursive
 182 -- module group (InstEnv imports stuff from FunDeps).
 183 \end{code}
 184
 185 Given a bunch of predicates that must hold, such as
 186
 187         C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
 188
 189 improve figures out what extra equations must hold.
 190 For example, if we have
 191
 192         class C a b | a->b where ...
 193
 194 then improve will return
 195
 196         [(t1,t2), (t4,t5)]
 197
 198 NOTA BENE:
 199
 200   * improve does not iterate.  It's possible that when we make
 201     t1=t2, for example, that will in turn trigger a new equation.
 202     This would happen if we also had
 203         C t1 t7, C t2 t8
 204     If t1=t2, we also get t7=t8.
 205
 206     improve does *not* do this extra step.  It relies on the caller
 207     doing so.
 208
 209   * The equations unify types that are not already equal.  So there
 210     is no effect iff the result of improve is empty
 211
 212
 213
 214 \begin{code}
 215 improve inst_env preds
 216   = [ eqn | group <- equivClassesByUniq (predTyUnique . fst) preds,
 217             eqn   <- checkGroup inst_env group ]
 218
 219 ----------
 220 checkGroup :: InstEnv Id -> [(PredType,SDoc)] -> [(Equation, SDoc)]
 221   -- The preds are all for the same class or implicit param
 222
 223 checkGroup inst_env (p1@(IParam _ ty, _) : ips)
 224   =     -- For implicit parameters, all the types must match
 225     [ ((emptyVarSet, ty, ty'), mkEqnMsg p1 p2)
 226     | p2@(IParam _ ty', _) <- ips, not (ty `tcEqType` ty')]
 227
 228 checkGroup inst_env clss@((ClassP cls _, _) : _)
 229   =     -- For classes life is more complicated
 230         -- Suppose the class is like
 231         --      classs C as | (l1 -> r1), (l2 -> r2), ... where ...
 232         -- Then FOR EACH PAIR (ClassP c tys1, ClassP c tys2) in the list clss
 233         -- we check whether
 234         --      U l1[tys1/as] = U l2[tys2/as]
 235         --  (where U is a unifier)
 236         --
 237         -- If so, we return the pair
 238         --      U r1[tys1/as] = U l2[tys2/as]
 239         --
 240         -- We need to do something very similar comparing each predicate
 241         -- with relevant instance decls
 242     pairwise_eqns ++ instance_eqns
 243
 244   where
 245     (cls_tvs, cls_fds) = classTvsFds cls
 246     cls_inst_env       = inst_env cls
 247
 248         -- NOTE that we iterate over the fds first; they are typically
 249         -- empty, which aborts the rest of the loop.
 250     pairwise_eqns :: [(Equation,SDoc)]
 251     pairwise_eqns       -- This group comes from pairwise comparison
 252       = [ (eqn, mkEqnMsg p1 p2)
 253         | fd <- cls_fds,
 254           p1@(ClassP _ tys1, _) : rest <- tails clss,
 255           p2@(ClassP _ tys2, _) <- rest,
 256           eqn <- checkClsFD emptyVarSet fd cls_tvs tys1 tys2
 257         ]
 258
 259     instance_eqns :: [(Equation,SDoc)]
 260     instance_eqns       -- This group comes from comparing with instance decls
 261       = [ (eqn, mkEqnMsg p1 p2)
 262         | fd <- cls_fds,
 263           (qtvs, tys1, dfun_id)  <- cls_inst_env,
 264           let p1 = (mkClassPred cls tys1,
 265                     ptext SLIT("arising from the instance declaration at") <+> ppr (getSrcLoc dfun_id)),
 266           p2@(ClassP _ tys2, _) <- clss,
 267           eqn <- checkClsFD qtvs fd cls_tvs tys1 tys2
 268         ]
 269
 270 mkEqnMsg (pred1,from1) (pred2,from2)
 271   = vcat [ptext SLIT("When using functional dependencies to combine"),
 272           nest 2 (sep [ppr pred1 <> comma, nest 2 from1]),
 273           nest 2 (sep [ppr pred2 <> comma, nest 2 from2])]
 274
 275 ----------
 276 checkClsFD :: TyVarSet                  -- Quantified type variables; see note below
 277            -> FunDep TyVar -> [TyVar]   -- One functional dependency from the class
 278            -> [Type] -> [Type]
 279            -> [Equation]
 280
 281 checkClsFD qtvs fd clas_tvs tys1 tys2
 282 -- 'qtvs' are the quantified type variables, the ones which an be instantiated
 283 -- to make the types match.  For example, given
 284 --      class C a b | a->b where ...
 285 --      instance C (Maybe x) (Tree x) where ..
 286 --
 287 -- and an Inst of form (C (Maybe t1) t2),
 288 -- then we will call checkClsFD with
 289 --
 290 --      qtvs = {x}, tys1 = [Maybe x,  Tree x]
 291 --                  tys2 = [Maybe t1, t2]
 292 --
 293 -- We can instantiate x to t1, and then we want to force
 294 --      (Tree x) [t1/x]  :=:   t2
 295
 296 -- We use 'unify' even though we are often only matching
 297 -- unifyTyListsX will only bind variables in qtvs, so it's OK!
 298   = case unifyTyListsX qtvs ls1 ls2 of
 299         Nothing   -> []
 300         Just unif -> -- pprTrace "checkFD" (vcat [ppr_fd fd,
 301                      --                        ppr (varSetElems qtvs) <+> (ppr ls1 $$ ppr ls2),
 302                      --                        ppr unif]) $
 303                      [ (qtvs', substTy full_unif r1, substTy full_unif r2)
 304                      | (r1,r2) <- rs1 `zip` rs2,
 305                        not (maybeToBool (unifyExtendTysX qtvs unif r1 r2))]
 306                         -- Don't include any equations that already hold
 307                         -- taking account of the fact that any qtvs that aren't
 308                         -- already instantiated can be instantiated to anything at all
 309                         -- NB: qtvs, not qtvs' because unifyExtendTysX only tries to
 310                         --     look template tyvars up in the substitution
 311                   where
 312                     full_unif = mkSubst emptyInScopeSet unif
 313                         -- No for-alls in sight; hmm
 314
 315                     qtvs' = filterVarSet (\v -> not (v `elemSubstEnv` unif)) qtvs
 316                         -- qtvs' are the quantified type variables
 317                         -- that have not been substituted out
 318                         --
 319                         -- Eg.  class C a b | a -> b
 320                         --      instance C Int [y]
 321                         -- Given constraint C Int z
 322                         -- we generate the equation
 323                         --      ({y}, [y], z)
 324   where
 325     (ls1, rs1) = instFD fd clas_tvs tys1
 326     (ls2, rs2) = instFD fd clas_tvs tys2
 327
 328 instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
 329 instFD (ls,rs) tvs tys
 330   = (map lookup ls, map lookup rs)
 331   where
 332     env       = zipVarEnv tvs tys
 333     lookup tv = lookupVarEnv_NF env tv
 334 \end{code}
 335
 336 \begin{code}
 337 checkInstFDs :: ThetaType -> Class -> [Type] -> Bool
 338 -- Check that functional dependencies are obeyed in an instance decl
 339 -- For example, if we have
 340 --      class theta => C a b | a -> b
 341 --      instance C t1 t2
 342 -- Then we require fv(t2) `subset` oclose(fv(t1), theta)
 343
 344 checkInstFDs theta clas inst_taus
 345   = all fundep_ok fds
 346   where
 347     (tyvars, fds) = classTvsFds clas
 348     fundep_ok fd  = tyVarsOfTypes rs `subVarSet` oclose theta (tyVarsOfTypes ls)
 349                  where
 350                    (ls,rs) = instFD fd tyvars inst_taus
 351 \end{code}
 352
 353 %************************************************************************
 354 %*                                                                      *
 355 \subsection{Miscellaneous}
 356 %*                                                                      *
 357 %************************************************************************
 358
 359 \begin{code}
 360 pprFundeps :: Outputable a => [FunDep a] -> SDoc
 361 pprFundeps [] = empty
 362 pprFundeps fds = hsep (ptext SLIT("|") : punctuate comma (map ppr_fd fds))
 363
 364 ppr_fd (us, vs) = hsep [interppSP us, ptext SLIT("->"), interppSP vs]
 365 \end{code}