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