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,
  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, 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 #ifdef UNUSED
  67 pprInstEnv :: InstEnv -> SDoc
  68 pprInstEnv env
  69   = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
  70            brackets (pprWithCommas ppr tys) <+> ppr dfun
  71          | cls_inst_env <-  eltsUFM env
  72          , (tyvars, tys, dfun) <- cls_inst_env
  73          ]
  74 #endif
  75
  76 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
  77 simpleDFunClassTyCon dfun
  78   = (clas, tycon)
  79   where
  80     (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
  81     tycon           = tcTyConAppTyCon ty
  82 \end{code}
  83
  84 %************************************************************************
  85 %*                                                                      *
  86 \subsection{Instance environments: InstEnv and ClsInstEnv}
  87 %*                                                                      *
  88 %************************************************************************
  89
  90 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
  91 ClsInstEnv mapping is the dfun for that instance.
  92
  93 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
  94
  95         forall a b, C t1 t2 t3  can be constructed by dfun
  96
  97 or, to put it another way, we have
  98
  99         instance (...) => C t1 t2 t3,  witnessed by dfun
 100
 101 There is an important consistency constraint in the elements of a ClsInstEnv:
 102
 103   * [a,b] must be a superset of the free vars of [t1,t2,t3]
 104
 105   * The dfun must itself be quantified over [a,b]
 106
 107   * More specific instances come before less specific ones,
 108     where they overlap
 109
 110 Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
 111         [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
 112 The "a" in the pattern must be one of the forall'd variables in
 113 the dfun type.
 114
 115
 116
 117 Notes on overlapping instances
 118 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 119 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
 120
 121 In others, overlap is permitted, but only in such a way that one can make
 122 a unique choice when looking up.  That is, overlap is only permitted if
 123 one template matches the other, or vice versa.  So this is ok:
 124
 125   [a]  [Int]
 126
 127 but this is not
 128
 129   (Int,a)  (b,Int)
 130
 131 If overlap is permitted, the list is kept most specific first, so that
 132 the first lookup is the right choice.
 133
 134
 135 For now we just use association lists.
 136
 137 \subsection{Avoiding a problem with overlapping}
 138
 139 Consider this little program:
 140
 141 \begin{pseudocode}
 142      class C a        where c :: a
 143      class C a => D a where d :: a
 144
 145      instance C Int where c = 17
 146      instance D Int where d = 13
 147
 148      instance C a => C [a] where c = [c]
 149      instance ({- C [a], -} D a) => D [a] where d = c
 150
 151      instance C [Int] where c = [37]
 152
 153      main = print (d :: [Int])
 154 \end{pseudocode}
 155
 156 What do you think `main' prints  (assuming we have overlapping instances, and
 157 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
 158 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
 159 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
 160 the `C [Int]' instance is more specific).
 161
 162 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
 163 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
 164 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
 165 doesn't even compile!  What's going on!?
 166
 167 What hugs complains about is the `D [a]' instance decl.
 168
 169 \begin{pseudocode}
 170      ERROR "mj.hs" (line 10): Cannot build superclass instance
 171      *** Instance            : D [a]
 172      *** Context supplied    : D a
 173      *** Required superclass : C [a]
 174 \end{pseudocode}
 175
 176 You might wonder what hugs is complaining about.  It's saying that you
 177 need to add `C [a]' to the context of the `D [a]' instance (as appears
 178 in comments).  But there's that `C [a]' instance decl one line above
 179 that says that I can reduce the need for a `C [a]' instance to the
 180 need for a `C a' instance, and in this case, I already have the
 181 necessary `C a' instance (since we have `D a' explicitly in the
 182 context, and `C' is a superclass of `D').
 183
 184 Unfortunately, the above reasoning indicates a premature commitment to the
 185 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
 186 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
 187 add the context that hugs suggests (uncomment the `C [a]'), effectively
 188 deferring the decision about which instance to use.
 189
 190 Now, interestingly enough, 4.04 has this same bug, but it's covered up
 191 in this case by a little known `optimization' that was disabled in
 192 4.06.  Ghc-4.04 silently inserts any missing superclass context into
 193 an instance declaration.  In this case, it silently inserts the `C
 194 [a]', and everything happens to work out.
 195
 196 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
 197 `Mark Jones', although Mark claims no credit for the `optimization' in
 198 question, and would rather it stopped being called the `Mark Jones
 199 optimization' ;-)
 200
 201 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
 202 something else out with ghc-4.04.  Let's add the following line:
 203
 204     d' :: D a => [a]
 205     d' = c
 206
 207 Everyone raise their hand who thinks that `d :: [Int]' should give a
 208 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
 209 `optimization' only applies to instance decls, not to regular
 210 bindings, giving inconsistent behavior.
 211
 212 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
 213 list of instances for a given class is ordered, so that more specific
 214 instances come before more generic ones.  For example, the instance
 215 list for C might contain:
 216     ..., C Int, ..., C a, ...
 217 When we go to look for a `C Int' instance we'll get that one first.
 218 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
 219 pass the `C Int' instance, and keep going.  But if `b' is
 220 unconstrained, then we don't know yet if the more specific instance
 221 will eventually apply.  GHC keeps going, and matches on the generic `C
 222 a'.  The fix is to, at each step, check to see if there's a reverse
 223 match, and if so, abort the search.  This prevents hugs from
 224 prematurely chosing a generic instance when a more specific one
 225 exists.
 226
 227 --Jeff
 228
 229 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
 230 this test.  Suppose the instance envt had
 231     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
 232 (still most specific first)
 233 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
 234         C x y Int  doesn't match the template {a,b} C a a b
 235 but neither does
 236         C a a b  match the template {x,y} C x y Int
 237 But still x and y might subsequently be unified so they *do* match.
 238
 239 Simple story: unify, don't match.
 240
 241
 242 %************************************************************************
 243 %*                                                                      *
 244 \subsection{Looking up an instance}
 245 %*                                                                      *
 246 %************************************************************************
 247
 248 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
 249 the env is kept ordered, the first match must be the only one.  The
 250 thing we are looking up can have an arbitrary "flexi" part.
 251
 252 \begin{code}
 253 lookupInstEnv :: DynFlags
 254               -> (InstEnv       -- External package inst-env
 255                  ,InstEnv)      -- Home-package inst-env
 256               -> Class -> [Type]                        -- What we are looking for
 257               -> ([(TyVarSubstEnv, InstEnvElt)],        -- Successful matches
 258                   [Id])                                 -- These don't match but do unify
 259         -- The second component of the tuple happens when we look up
 260         --      Foo [a]
 261         -- in an InstEnv that has entries for
 262         --      Foo [Int]
 263         --      Foo [b]
 264         -- Then which we choose would depend on the way in which 'a'
 265         -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
 266         -- but Foo [Int] is a unifier.  This gives the caller a better chance of
 267         -- giving a suitable error messagen
 268
 269 lookupInstEnv dflags (pkg_ie, home_ie) cls tys
 270   | not (null all_unifs) = (all_matches, all_unifs)     -- This is always an error situation,
 271                                                         -- so don't attempt to pune the matches
 272   | otherwise            = (pruned_matches, [])
 273   where
 274     incoherent_ok = dopt Opt_AllowIncoherentInstances  dflags
 275     overlap_ok    = dopt Opt_AllowOverlappingInstances dflags
 276     (home_matches, home_unifs) = lookup_inst_env home_ie cls tys
 277     (pkg_matches,  pkg_unifs)  = lookup_inst_env pkg_ie  cls tys
 278     all_matches = home_matches ++ pkg_matches
 279     all_unifs | incoherent_ok = []      -- Don't worry about these if incoherent is ok!
 280               | otherwise     = home_unifs ++ pkg_unifs
 281
 282     pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
 283                    | otherwise  = all_matches
 284
 285 lookup_inst_env :: InstEnv                              -- The envt
 286                 -> Class -> [Type]                      -- What we are looking for
 287                 -> ([(TyVarSubstEnv, InstEnvElt)],      -- Successful matches
 288                     [Id])                               -- These don't match but do unify
 289 lookup_inst_env env key_cls key_tys
 290   = find (classInstEnv env key_cls) [] []
 291   where
 292     key_vars = tyVarsOfTypes key_tys
 293
 294     find [] ms us = (ms, us)
 295     find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
 296       = case matchTys tpl_tyvars tpl key_tys of
 297           Just (subst, leftovers) -> ASSERT( null leftovers )
 298                                      find rest ((subst,item):ms) us
 299           Nothing
 300                 -- Does not match, so next check whether the things unify
 301                 -- [see notes about overlapping instances above]
 302            -> ASSERT( not (key_vars `intersectsVarSet` tpl_tyvars) )
 303                 -- Unification will break badly if the variables overlap
 304                 -- They shouldn't because we allocate separate uniques for them
 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 (pkg_ie, home_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}