ghc/compiler/types/InstEnv.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[InstEnv]{Utilities for typechecking instance declarations}
   5
   6 The bits common to TcInstDcls and TcDeriv.
   7
   8 \begin{code}
   9 module InstEnv (
  10         DFunId, InstEnv,
  11
  12         emptyInstEnv, extendInstEnv, pprInstEnv,
  13         lookupInstEnv,
  14         classInstEnv, simpleDFunClassTyCon, checkFunDeps
  15     ) where
  16
  17 #include "HsVersions.h"
  18
  19 import Class            ( Class, classTvsFds )
  20 import Var              ( Id )
  21 import VarSet
  22 import VarEnv
  23 import TcType           ( Type, tcTyConAppTyCon,
  24                           tcSplitDFunTy, tyVarsOfTypes,
  25                           matchTys, unifyTyListsX
  26                         )
  27 import FunDeps          ( checkClsFD )
  28 import TyCon            ( TyCon )
  29 import Outputable
  30 import UniqFM           ( UniqFM, lookupWithDefaultUFM, emptyUFM, eltsUFM, addToUFM_C )
  31 import Id               ( idType )
  32 import CmdLineOpts
  33 import Util             ( notNull )
  34 import Maybe            ( isJust )
  35 \end{code}
  36
  37
  38 %************************************************************************
  39 %*                                                                      *
  40 \subsection{The key types}
  41 %*                                                                      *
  42 %************************************************************************
  43
  44 \begin{code}
  45 type DFunId     = Id
  46 type InstEnv    = UniqFM ClsInstEnv     -- Maps Class to instances for that class
  47 type ClsInstEnv = [InstEnvElt]          -- The instances for a particular class
  48 type InstEnvElt = (TyVarSet, [Type], DFunId)
  49         -- INVARIANTs: see notes below
  50
  51 emptyInstEnv :: InstEnv
  52 emptyInstEnv = emptyUFM
  53
  54 classInstEnv :: InstEnv -> Class -> ClsInstEnv
  55 classInstEnv env cls = lookupWithDefaultUFM env [] cls
  56
  57 extendInstEnv :: InstEnv -> DFunId -> InstEnv
  58 extendInstEnv inst_env dfun_id
  59   = addToUFM_C add inst_env clas [ins_item]
  60   where
  61     add old _ = ins_item : old
  62     (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
  63     ins_tv_set = mkVarSet ins_tvs
  64     ins_item   = (ins_tv_set, ins_tys, dfun_id)
  65
  66 pprInstEnv :: InstEnv -> SDoc
  67 pprInstEnv env
  68   = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
  69            brackets (pprWithCommas ppr tys) <+> ppr dfun
  70          | cls_inst_env <-  eltsUFM env
  71          , (tyvars, tys, dfun) <- cls_inst_env
  72          ]
  73
  74
  75 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
  76 simpleDFunClassTyCon dfun
  77   = (clas, tycon)
  78   where
  79     (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
  80     tycon           = tcTyConAppTyCon ty
  81 \end{code}
  82
  83 %************************************************************************
  84 %*                                                                      *
  85 \subsection{Instance environments: InstEnv and ClsInstEnv}
  86 %*                                                                      *
  87 %************************************************************************
  88
  89 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
  90 ClsInstEnv mapping is the dfun for that instance.
  91
  92 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
  93
  94         forall a b, C t1 t2 t3  can be constructed by dfun
  95
  96 or, to put it another way, we have
  97
  98         instance (...) => C t1 t2 t3,  witnessed by dfun
  99
 100 There is an important consistency constraint in the elements of a ClsInstEnv:
 101
 102   * [a,b] must be a superset of the free vars of [t1,t2,t3]
 103
 104   * The dfun must itself be quantified over [a,b]
 105
 106   * More specific instances come before less specific ones,
 107     where they overlap
 108
 109 Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
 110         [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
 111 The "a" in the pattern must be one of the forall'd variables in
 112 the dfun type.
 113
 114
 115
 116 Notes on overlapping instances
 117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 118 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
 119
 120 In others, overlap is permitted, but only in such a way that one can make
 121 a unique choice when looking up.  That is, overlap is only permitted if
 122 one template matches the other, or vice versa.  So this is ok:
 123
 124   [a]  [Int]
 125
 126 but this is not
 127
 128   (Int,a)  (b,Int)
 129
 130 If overlap is permitted, the list is kept most specific first, so that
 131 the first lookup is the right choice.
 132
 133
 134 For now we just use association lists.
 135
 136 \subsection{Avoiding a problem with overlapping}
 137
 138 Consider this little program:
 139
 140 \begin{pseudocode}
 141      class C a        where c :: a
 142      class C a => D a where d :: a
 143
 144      instance C Int where c = 17
 145      instance D Int where d = 13
 146
 147      instance C a => C [a] where c = [c]
 148      instance ({- C [a], -} D a) => D [a] where d = c
 149
 150      instance C [Int] where c = [37]
 151
 152      main = print (d :: [Int])
 153 \end{pseudocode}
 154
 155 What do you think `main' prints  (assuming we have overlapping instances, and
 156 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
 157 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
 158 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
 159 the `C [Int]' instance is more specific).
 160
 161 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
 162 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
 163 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
 164 doesn't even compile!  What's going on!?
 165
 166 What hugs complains about is the `D [a]' instance decl.
 167
 168 \begin{pseudocode}
 169      ERROR "mj.hs" (line 10): Cannot build superclass instance
 170      *** Instance            : D [a]
 171      *** Context supplied    : D a
 172      *** Required superclass : C [a]
 173 \end{pseudocode}
 174
 175 You might wonder what hugs is complaining about.  It's saying that you
 176 need to add `C [a]' to the context of the `D [a]' instance (as appears
 177 in comments).  But there's that `C [a]' instance decl one line above
 178 that says that I can reduce the need for a `C [a]' instance to the
 179 need for a `C a' instance, and in this case, I already have the
 180 necessary `C a' instance (since we have `D a' explicitly in the
 181 context, and `C' is a superclass of `D').
 182
 183 Unfortunately, the above reasoning indicates a premature commitment to the
 184 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
 185 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
 186 add the context that hugs suggests (uncomment the `C [a]'), effectively
 187 deferring the decision about which instance to use.
 188
 189 Now, interestingly enough, 4.04 has this same bug, but it's covered up
 190 in this case by a little known `optimization' that was disabled in
 191 4.06.  Ghc-4.04 silently inserts any missing superclass context into
 192 an instance declaration.  In this case, it silently inserts the `C
 193 [a]', and everything happens to work out.
 194
 195 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
 196 `Mark Jones', although Mark claims no credit for the `optimization' in
 197 question, and would rather it stopped being called the `Mark Jones
 198 optimization' ;-)
 199
 200 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
 201 something else out with ghc-4.04.  Let's add the following line:
 202
 203     d' :: D a => [a]
 204     d' = c
 205
 206 Everyone raise their hand who thinks that `d :: [Int]' should give a
 207 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
 208 `optimization' only applies to instance decls, not to regular
 209 bindings, giving inconsistent behavior.
 210
 211 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
 212 list of instances for a given class is ordered, so that more specific
 213 instances come before more generic ones.  For example, the instance
 214 list for C might contain:
 215     ..., C Int, ..., C a, ...
 216 When we go to look for a `C Int' instance we'll get that one first.
 217 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
 218 pass the `C Int' instance, and keep going.  But if `b' is
 219 unconstrained, then we don't know yet if the more specific instance
 220 will eventually apply.  GHC keeps going, and matches on the generic `C
 221 a'.  The fix is to, at each step, check to see if there's a reverse
 222 match, and if so, abort the search.  This prevents hugs from
 223 prematurely chosing a generic instance when a more specific one
 224 exists.
 225
 226 --Jeff
 227
 228 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
 229 this test.  Suppose the instance envt had
 230     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
 231 (still most specific first)
 232 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
 233         C x y Int  doesn't match the template {a,b} C a a b
 234 but neither does
 235         C a a b  match the template {x,y} C x y Int
 236 But still x and y might subsequently be unified so they *do* match.
 237
 238 Simple story: unify, don't match.
 239
 240
 241 %************************************************************************
 242 %*                                                                      *
 243 \subsection{Looking up an instance}
 244 %*                                                                      *
 245 %************************************************************************
 246
 247 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
 248 the env is kept ordered, the first match must be the only one.  The
 249 thing we are looking up can have an arbitrary "flexi" part.
 250
 251 \begin{code}
 252 lookupInstEnv :: DynFlags
 253               -> (InstEnv,      -- Home-package inst-env
 254                   InstEnv)      -- External package inst-env
 255               -> Class -> [Type]                        -- What we are looking for
 256               -> ([(TyVarSubstEnv, InstEnvElt)],        -- Successful matches
 257                   [Id])                                 -- These don't match but do unify
 258         -- The second component of the tuple happens when we look up
 259         --      Foo [a]
 260         -- in an InstEnv that has entries for
 261         --      Foo [Int]
 262         --      Foo [b]
 263         -- Then which we choose would depend on the way in which 'a'
 264         -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
 265         -- but Foo [Int] is a unifier.  This gives the caller a better chance of
 266         -- giving a suitable error messagen
 267
 268 lookupInstEnv dflags (home_ie, pkg_ie) cls tys
 269   | not (null all_unifs) = (all_matches, all_unifs)     -- This is always an error situation,
 270                                                         -- so don't attempt to pune the matches
 271   | otherwise            = (pruned_matches, [])
 272   where
 273     incoherent_ok = dopt Opt_AllowIncoherentInstances  dflags
 274     overlap_ok    = dopt Opt_AllowOverlappingInstances dflags
 275     (home_matches, home_unifs) = lookup_inst_env incoherent_ok home_ie cls tys
 276     (pkg_matches,  pkg_unifs)  = lookup_inst_env incoherent_ok pkg_ie  cls tys
 277     all_matches = home_matches ++ pkg_matches
 278     all_unifs   = home_unifs ++ pkg_unifs
 279
 280     pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
 281                    | otherwise  = all_matches
 282
 283 lookup_inst_env :: Bool
 284               -> InstEnv                                -- The envt
 285               -> Class -> [Type]                        -- What we are looking for
 286               -> ([(TyVarSubstEnv, InstEnvElt)],        -- Successful matches
 287                   [Id])                                 -- These don't match but do unify
 288 lookup_inst_env incoherent_ok env key_cls key_tys
 289   = find (classInstEnv env key_cls) [] []
 290   where
 291     key_vars = tyVarsOfTypes key_tys
 292
 293     find [] ms us = (ms, us)
 294     find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
 295       = case matchTys tpl_tyvars tpl key_tys of
 296           Just (subst, leftovers) -> ASSERT( null leftovers )
 297                                      find rest ((subst,item):ms) us
 298           Nothing
 299            | incoherent_ok -> find rest ms us
 300                 -- If we allow incoherent instances we don't worry about the
 301                 -- test and just blaze on anyhow.  Requested by John Hughes.
 302            | otherwise
 303                 -- Does not match, so next check whether the things unify
 304                 -- [see notes about overlapping instances above]
 305            -> case unifyTyListsX (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
 306                 Just _   -> find rest ms (dfun_id:us)
 307                 Nothing  -> find rest ms us
 308
 309 insert_overlapping :: (TyVarSubstEnv, InstEnvElt) -> [(TyVarSubstEnv, InstEnvElt)]
 310                    -> [(TyVarSubstEnv, InstEnvElt)]
 311 -- Add a new solution, knocking out strictly less specific ones
 312 insert_overlapping new_item [] = [new_item]
 313 insert_overlapping new_item (item:items)
 314   | new_beats_old && old_beats_new = item : insert_overlapping new_item items
 315         -- Duplicate => keep both for error report
 316   | new_beats_old = insert_overlapping new_item items
 317         -- Keep new one
 318   | old_beats_new = item : items
 319         -- Keep old one
 320   | otherwise             = item : insert_overlapping new_item items
 321         -- Keep both
 322   where
 323     new_beats_old = new_item `beats` item
 324     old_beats_new = item `beats` new_item
 325
 326     (_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _))
 327         = isJust (matchTys tvs2 tys2 tys1)      -- A beats B if A is more specific than B
 328                                                 -- I.e. if B can be instantiated to match A
 329 \end{code}
 330
 331
 332 %************************************************************************
 333 %*                                                                      *
 334                 Functional dependencies
 335 %*                                                                      *
 336 %************************************************************************
 337
 338 Here is the bad case:
 339         class C a b | a->b where ...
 340         instance C Int Bool where ...
 341         instance C Int Char where ...
 342
 343 The point is that a->b, so Int in the first parameter must uniquely
 344 determine the second.  In general, given the same class decl, and given
 345
 346         instance C s1 s2 where ...
 347         instance C t1 t2 where ...
 348
 349 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
 350
 351 Matters are a little more complicated if there are free variables in
 352 the s2/t2.
 353
 354         class D a b c | a -> b
 355         instance D a b => D [(a,a)] [b] Int
 356         instance D a b => D [a]     [b] Bool
 357
 358 The instance decls don't overlap, because the third parameter keeps
 359 them separate.  But we want to make sure that given any constraint
 360         D s1 s2 s3
 361 if s1 matches
 362
 363
 364 \begin{code}
 365 checkFunDeps :: (InstEnv, InstEnv) -> DFunId
 366              -> Maybe [DFunId]  -- Nothing  <=> ok
 367                                 -- Just dfs <=> conflict with dfs
 368 -- Check wheher adding DFunId would break functional-dependency constraints
 369 checkFunDeps (home_ie, pkg_ie) dfun
 370   | null bad_fundeps = Nothing
 371   | otherwise        = Just bad_fundeps
 372   where
 373     (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun)
 374     ins_tv_set   = mkVarSet ins_tvs
 375     cls_inst_env = classInstEnv home_ie clas ++ classInstEnv pkg_ie clas
 376     bad_fundeps  = badFunDeps cls_inst_env clas ins_tv_set ins_tys
 377
 378 badFunDeps :: ClsInstEnv -> Class
 379            -> TyVarSet -> [Type]        -- Proposed new instance type
 380            -> [DFunId]
 381 badFunDeps cls_inst_env clas ins_tv_set ins_tys
 382   = [ dfun_id | fd <- fds,
 383                (tvs, tys, dfun_id) <- cls_inst_env,
 384                notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys)
 385     ]
 386   where
 387     (clas_tvs, fds) = classTvsFds clas
 388 \end{code}