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