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