compiler/types/InstEnv.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5 \section[InstEnv]{Utilities for typechecking instance declarations}
   6
   7 The bits common to TcInstDcls and TcDeriv.
   8
   9 \begin{code}
  10 module InstEnv (
  11         DFunId, OverlapFlag(..),
  12         Instance(..), pprInstance, pprInstanceHdr, pprInstances,
  13         instanceHead, mkLocalInstance, mkImportedInstance,
  14         instanceDFunId, setInstanceDFunId, instanceRoughTcs,
  15
  16         InstEnv, emptyInstEnv, extendInstEnv,
  17         extendInstEnvList, lookupInstEnv, instEnvElts,
  18         classInstances, instanceBindFun,
  19         instanceCantMatch, roughMatchTcs
  20     ) where
  21
  22 #include "HsVersions.h"
  23
  24 import Class
  25 import Var
  26 import VarSet
  27 import Name
  28 import TcType
  29 import TyCon
  30 import Unify
  31 import Outputable
  32 import BasicTypes
  33 import UniqFM
  34 import Id
  35 import FastString
  36
  37 import Data.Maybe       ( isJust, isNothing )
  38 \end{code}
  39
  40
  41 %************************************************************************
  42 %*                                                                      *
  43 \subsection{The key types}
  44 %*                                                                      *
  45 %************************************************************************
  46
  47 \begin{code}
  48 data Instance
  49   = Instance { is_cls  :: Name          -- Class name
  50
  51                 -- Used for "rough matching"; see Note [Rough-match field]
  52                 -- INVARIANT: is_tcs = roughMatchTcs is_tys
  53              , is_tcs  :: [Maybe Name]  -- Top of type args
  54
  55                 -- Used for "proper matching"; see Note [Proper-match fields]
  56              , is_tvs  :: TyVarSet      -- Template tyvars for full match
  57              , is_tys  :: [Type]        -- Full arg types
  58                 -- INVARIANT: is_dfun Id has type
  59                 --      forall is_tvs. (...) => is_cls is_tys
  60
  61              , is_dfun :: DFunId -- See Note [Haddock assumptions]
  62              , is_flag :: OverlapFlag   -- See detailed comments with
  63                                         -- the decl of BasicTypes.OverlapFlag
  64     }
  65 \end{code}
  66
  67 Note [Rough-match field]
  68 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  69 The is_cls, is_tcs fields allow a "rough match" to be done
  70 without poking inside the DFunId.  Poking the DFunId forces
  71 us to suck in all the type constructors etc it involves,
  72 which is a total waste of time if it has no chance of matching
  73 So the Name, [Maybe Name] fields allow us to say "definitely
  74 does not match", based only on the Name.
  75
  76 In is_tcs,
  77     Nothing  means that this type arg is a type variable
  78
  79     (Just n) means that this type arg is a
  80                 TyConApp with a type constructor of n.
  81                 This is always a real tycon, never a synonym!
  82                 (Two different synonyms might match, but two
  83                 different real tycons can't.)
  84                 NB: newtypes are not transparent, though!
  85
  86 Note [Proper-match fields]
  87 ~~~~~~~~~~~~~~~~~~~~~~~~~
  88 The is_tvs, is_tys fields are simply cached values, pulled
  89 out (lazily) from the dfun id. They are cached here simply so
  90 that we don't need to decompose the DFunId each time we want
  91 to match it.  The hope is that the fast-match fields mean
  92 that we often never poke th proper-match fields
  93
  94 However, note that:
  95  * is_tvs must be a superset of the free vars of is_tys
  96
  97  * The is_dfun must itself be quantified over exactly is_tvs
  98    (This is so that we can use the matching substitution to
  99     instantiate the dfun's context.)
 100
 101 Note [Haddock assumptions]
 102 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 103 For normal user-written instances, Haddock relies on
 104
 105  * the SrcSpan of
 106  * the Name of
 107  * the is_dfun of
 108  * an Instance
 109
 110 being equal to
 111
 112   * the SrcSpan of
 113   * the instance head type of
 114   * the InstDecl used to construct the Instance.
 115
 116 \begin{code}
 117 instanceDFunId :: Instance -> DFunId
 118 instanceDFunId = is_dfun
 119
 120 setInstanceDFunId :: Instance -> DFunId -> Instance
 121 setInstanceDFunId ispec dfun
 122    = ASSERT( idType dfun `tcEqType` idType (is_dfun ispec) )
 123         -- We need to create the cached fields afresh from
 124         -- the new dfun id.  In particular, the is_tvs in
 125         -- the Instance must match those in the dfun!
 126         -- We assume that the only thing that changes is
 127         -- the quantified type variables, so the other fields
 128         -- are ok; hence the assert
 129      ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
 130    where
 131      (tvs, _, tys) = tcSplitDFunTy (idType dfun)
 132
 133 instanceRoughTcs :: Instance -> [Maybe Name]
 134 instanceRoughTcs = is_tcs
 135 \end{code}
 136
 137 \begin{code}
 138 instance NamedThing Instance where
 139    getName ispec = getName (is_dfun ispec)
 140
 141 instance Outputable Instance where
 142    ppr = pprInstance
 143
 144 pprInstance :: Instance -> SDoc
 145 -- Prints the Instance as an instance declaration
 146 pprInstance ispec
 147   = hang (pprInstanceHdr ispec)
 148         2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
 149
 150 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
 151 pprInstanceHdr :: Instance -> SDoc
 152 -- Prints the Instance as an instance declaration
 153 pprInstanceHdr ispec@(Instance { is_flag = flag })
 154   = ptext (sLit "instance") <+> ppr flag
 155     <+> sep [pprThetaArrow theta, ppr res_ty]
 156   where
 157     (_, theta, res_ty) = tcSplitSigmaTy (idType (is_dfun ispec))
 158         -- Print without the for-all, which the programmer doesn't write
 159
 160 pprInstances :: [Instance] -> SDoc
 161 pprInstances ispecs = vcat (map pprInstance ispecs)
 162
 163 instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
 164 instanceHead ispec
 165    = (tvs, theta, cls, tys)
 166    where
 167      (tvs, theta, tau) = tcSplitSigmaTy (idType (is_dfun ispec))
 168      (cls, tys) = tcSplitDFunHead tau
 169
 170 mkLocalInstance :: DFunId -> OverlapFlag -> Instance
 171 -- Used for local instances, where we can safely pull on the DFunId
 172 mkLocalInstance dfun oflag
 173   = Instance {  is_flag = oflag, is_dfun = dfun,
 174                 is_tvs = mkVarSet tvs, is_tys = tys,
 175                 is_cls = className cls, is_tcs = roughMatchTcs tys }
 176   where
 177     (tvs, cls, tys) = tcSplitDFunTy (idType dfun)
 178
 179 mkImportedInstance :: Name -> [Maybe Name]
 180                    -> DFunId -> OverlapFlag -> Instance
 181 -- Used for imported instances, where we get the rough-match stuff
 182 -- from the interface file
 183 mkImportedInstance cls mb_tcs dfun oflag
 184   = Instance {  is_flag = oflag, is_dfun = dfun,
 185                 is_tvs = mkVarSet tvs, is_tys = tys,
 186                 is_cls = cls, is_tcs = mb_tcs }
 187   where
 188     (tvs, _, tys) = tcSplitDFunTy (idType dfun)
 189
 190 roughMatchTcs :: [Type] -> [Maybe Name]
 191 roughMatchTcs tys = map rough tys
 192   where
 193     rough ty = case tcSplitTyConApp_maybe ty of
 194                   Just (tc,_) -> Just (tyConName tc)
 195                   Nothing     -> Nothing
 196
 197 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
 198 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
 199 -- possibly be instantiated to actual, nor vice versa;
 200 -- False is non-committal
 201 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
 202 instanceCantMatch _             _             =  False  -- Safe
 203 \end{code}
 204
 205
 206 Note [Overlapping instances]
 207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 208 Overlap is permitted, but only in such a way that one can make
 209 a unique choice when looking up.  That is, overlap is only permitted if
 210 one template matches the other, or vice versa.  So this is ok:
 211
 212   [a]  [Int]
 213
 214 but this is not
 215
 216   (Int,a)  (b,Int)
 217
 218 If overlap is permitted, the list is kept most specific first, so that
 219 the first lookup is the right choice.
 220
 221
 222 For now we just use association lists.
 223
 224 \subsection{Avoiding a problem with overlapping}
 225
 226 Consider this little program:
 227
 228 \begin{pseudocode}
 229      class C a        where c :: a
 230      class C a => D a where d :: a
 231
 232      instance C Int where c = 17
 233      instance D Int where d = 13
 234
 235      instance C a => C [a] where c = [c]
 236      instance ({- C [a], -} D a) => D [a] where d = c
 237
 238      instance C [Int] where c = [37]
 239
 240      main = print (d :: [Int])
 241 \end{pseudocode}
 242
 243 What do you think `main' prints  (assuming we have overlapping instances, and
 244 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
 245 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
 246 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
 247 the `C [Int]' instance is more specific).
 248
 249 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
 250 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
 251 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
 252 doesn't even compile!  What's going on!?
 253
 254 What hugs complains about is the `D [a]' instance decl.
 255
 256 \begin{pseudocode}
 257      ERROR "mj.hs" (line 10): Cannot build superclass instance
 258      *** Instance            : D [a]
 259      *** Context supplied    : D a
 260      *** Required superclass : C [a]
 261 \end{pseudocode}
 262
 263 You might wonder what hugs is complaining about.  It's saying that you
 264 need to add `C [a]' to the context of the `D [a]' instance (as appears
 265 in comments).  But there's that `C [a]' instance decl one line above
 266 that says that I can reduce the need for a `C [a]' instance to the
 267 need for a `C a' instance, and in this case, I already have the
 268 necessary `C a' instance (since we have `D a' explicitly in the
 269 context, and `C' is a superclass of `D').
 270
 271 Unfortunately, the above reasoning indicates a premature commitment to the
 272 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
 273 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
 274 add the context that hugs suggests (uncomment the `C [a]'), effectively
 275 deferring the decision about which instance to use.
 276
 277 Now, interestingly enough, 4.04 has this same bug, but it's covered up
 278 in this case by a little known `optimization' that was disabled in
 279 4.06.  Ghc-4.04 silently inserts any missing superclass context into
 280 an instance declaration.  In this case, it silently inserts the `C
 281 [a]', and everything happens to work out.
 282
 283 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
 284 `Mark Jones', although Mark claims no credit for the `optimization' in
 285 question, and would rather it stopped being called the `Mark Jones
 286 optimization' ;-)
 287
 288 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
 289 something else out with ghc-4.04.  Let's add the following line:
 290
 291     d' :: D a => [a]
 292     d' = c
 293
 294 Everyone raise their hand who thinks that `d :: [Int]' should give a
 295 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
 296 `optimization' only applies to instance decls, not to regular
 297 bindings, giving inconsistent behavior.
 298
 299 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
 300 list of instances for a given class is ordered, so that more specific
 301 instances come before more generic ones.  For example, the instance
 302 list for C might contain:
 303     ..., C Int, ..., C a, ...
 304 When we go to look for a `C Int' instance we'll get that one first.
 305 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
 306 pass the `C Int' instance, and keep going.  But if `b' is
 307 unconstrained, then we don't know yet if the more specific instance
 308 will eventually apply.  GHC keeps going, and matches on the generic `C
 309 a'.  The fix is to, at each step, check to see if there's a reverse
 310 match, and if so, abort the search.  This prevents hugs from
 311 prematurely chosing a generic instance when a more specific one
 312 exists.
 313
 314 --Jeff
 315
 316 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
 317 this test.  Suppose the instance envt had
 318     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
 319 (still most specific first)
 320 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
 321         C x y Int  doesn't match the template {a,b} C a a b
 322 but neither does
 323         C a a b  match the template {x,y} C x y Int
 324 But still x and y might subsequently be unified so they *do* match.
 325
 326 Simple story: unify, don't match.
 327
 328
 329 %************************************************************************
 330 %*                                                                      *
 331                 InstEnv, ClsInstEnv
 332 %*                                                                      *
 333 %************************************************************************
 334
 335 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
 336 ClsInstEnv mapping is the dfun for that instance.
 337
 338 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
 339
 340         forall a b, C t1 t2 t3  can be constructed by dfun
 341
 342 or, to put it another way, we have
 343
 344         instance (...) => C t1 t2 t3,  witnessed by dfun
 345
 346 \begin{code}
 347 ---------------------------------------------------
 348 type InstEnv = UniqFM ClsInstEnv        -- Maps Class to instances for that class
 349
 350 data ClsInstEnv
 351   = ClsIE [Instance]    -- The instances for a particular class, in any order
 352           Bool          -- True <=> there is an instance of form C a b c
 353                         --      If *not* then the common case of looking up
 354                         --      (C a b c) can fail immediately
 355
 356 -- INVARIANTS:
 357 --  * The is_tvs are distinct in each Instance
 358 --      of a ClsInstEnv (so we can safely unify them)
 359
 360 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
 361 --      [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
 362 -- The "a" in the pattern must be one of the forall'd variables in
 363 -- the dfun type.
 364
 365 emptyInstEnv :: InstEnv
 366 emptyInstEnv = emptyUFM
 367
 368 instEnvElts :: InstEnv -> [Instance]
 369 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
 370
 371 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
 372 classInstances (pkg_ie, home_ie) cls
 373   = get home_ie ++ get pkg_ie
 374   where
 375     get env = case lookupUFM env cls of
 376                 Just (ClsIE insts _) -> insts
 377                 Nothing              -> []
 378
 379 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
 380 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
 381
 382 extendInstEnv :: InstEnv -> Instance -> InstEnv
 383 extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
 384   = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
 385   where
 386     add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
 387                                               (ins_tyvar || cur_tyvar)
 388     ins_tyvar = not (any isJust mb_tcs)
 389 \end{code}
 390
 391
 392 %************************************************************************
 393 %*                                                                      *
 394         Looking up an instance
 395 %*                                                                      *
 396 %************************************************************************
 397
 398 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
 399 the env is kept ordered, the first match must be the only one.  The
 400 thing we are looking up can have an arbitrary "flexi" part.
 401
 402 \begin{code}
 403 type InstTypes = [Either TyVar Type]
 404         -- Right ty     => Instantiate with this type
 405         -- Left tv      => Instantiate with any type of this tyvar's kind
 406
 407 type InstMatch = (Instance, InstTypes)
 408 \end{code}
 409
 410 Note [InstTypes: instantiating types]
 411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 412 A successful match is an Instance, together with the types at which
 413         the dfun_id in the Instance should be instantiated
 414 The instantiating types are (Mabye Type)s because the dfun
 415 might have some tyvars that *only* appear in arguments
 416         dfun :: forall a b. C a b, Ord b => D [a]
 417 When we match this against D [ty], we return the instantiating types
 418         [Right ty, Left b]
 419 where the Nothing indicates that 'b' can be freely instantiated.
 420 (The caller instantiates it to a flexi type variable, which will presumably
 421  presumably later become fixed via functional dependencies.)
 422
 423 \begin{code}
 424 lookupInstEnv :: (InstEnv, InstEnv)     -- External and home package inst-env
 425               -> Class -> [Type]        -- What we are looking for
 426               -> ([InstMatch],          -- Successful matches
 427                   [Instance])           -- These don't match but do unify
 428
 429 -- The second component of the result pair happens when we look up
 430 --      Foo [a]
 431 -- in an InstEnv that has entries for
 432 --      Foo [Int]
 433 --      Foo [b]
 434 -- Then which we choose would depend on the way in which 'a'
 435 -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
 436 -- but Foo [Int] is a unifier.  This gives the caller a better chance of
 437 -- giving a suitable error messagen
 438
 439 lookupInstEnv (pkg_ie, home_ie) cls tys
 440   = (pruned_matches, all_unifs)
 441   where
 442     rough_tcs  = roughMatchTcs tys
 443     all_tvs    = all isNothing rough_tcs
 444     (home_matches, home_unifs) = lookup home_ie
 445     (pkg_matches,  pkg_unifs)  = lookup pkg_ie
 446     all_matches = home_matches ++ pkg_matches
 447     all_unifs   = home_unifs   ++ pkg_unifs
 448     pruned_matches = foldr insert_overlapping [] all_matches
 449         -- Even if the unifs is non-empty (an error situation)
 450         -- we still prune the matches, so that the error message isn't
 451         -- misleading (complaining of multiple matches when some should be
 452         -- overlapped away)
 453
 454     --------------
 455     lookup env = case lookupUFM env cls of
 456                    Nothing -> ([],[])   -- No instances for this class
 457                    Just (ClsIE insts has_tv_insts)
 458                         | all_tvs && not has_tv_insts
 459                         -> ([],[])      -- Short cut for common case
 460                         -- The thing we are looking up is of form (C a b c), and
 461                         -- the ClsIE has no instances of that form, so don't bother to search
 462
 463                         | otherwise
 464                         -> find [] [] insts
 465
 466     --------------
 467     lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
 468         -- See Note [InstTypes: instantiating types]
 469     lookup_tv subst tv = case lookupTyVar subst tv of
 470                                 Just ty -> Right ty
 471                                 Nothing -> Left tv
 472
 473     find ms us [] = (ms, us)
 474     find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs,
 475                                  is_tys = tpl_tys, is_flag = oflag,
 476                                  is_dfun = dfun }) : rest)
 477         -- Fast check for no match, uses the "rough match" fields
 478       | instanceCantMatch rough_tcs mb_tcs
 479       = find ms us rest
 480
 481       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
 482       = let
 483             (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
 484         in
 485         ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs )   -- Check invariant
 486         find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
 487
 488         -- Does not match, so next check whether the things unify
 489         -- See Note [overlapping instances] above
 490       | Incoherent <- oflag
 491       = find ms us rest
 492
 493       | otherwise
 494       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
 495                  (ppr cls <+> ppr tys <+> ppr all_tvs) $$
 496                  (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
 497                 )
 498                 -- Unification will break badly if the variables overlap
 499                 -- They shouldn't because we allocate separate uniques for them
 500         case tcUnifyTys instanceBindFun tpl_tys tys of
 501             Just _   -> find ms (item:us) rest
 502             Nothing  -> find ms us        rest
 503
 504 ---------------
 505 ---------------
 506 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
 507 -- Add a new solution, knocking out strictly less specific ones
 508 insert_overlapping new_item [] = [new_item]
 509 insert_overlapping new_item (item:items)
 510   | new_beats_old && old_beats_new = item : insert_overlapping new_item items
 511         -- Duplicate => keep both for error report
 512   | new_beats_old = insert_overlapping new_item items
 513         -- Keep new one
 514   | old_beats_new = item : items
 515         -- Keep old one
 516   | otherwise     = item : insert_overlapping new_item items
 517         -- Keep both
 518   where
 519     new_beats_old = new_item `beats` item
 520     old_beats_new = item `beats` new_item
 521
 522     (instA, _) `beats` (instB, _)
 523         = overlap_ok &&
 524           isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
 525                 -- A beats B if A is more specific than B, and B admits overlap
 526                 -- I.e. if B can be instantiated to match A
 527         where
 528           overlap_ok = case is_flag instB of
 529                         NoOverlap -> False
 530                         _         -> True
 531 \end{code}
 532
 533
 534 %************************************************************************
 535 %*                                                                      *
 536         Binding decisions
 537 %*                                                                      *
 538 %************************************************************************
 539
 540 \begin{code}
 541 instanceBindFun :: TyVar -> BindFlag
 542 instanceBindFun tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
 543                    | otherwise                          = BindMe
 544    -- Note [Binding when looking up instances]
 545 \end{code}
 546
 547 Note [Binding when looking up instances]
 548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 549 When looking up in the instance environment, or family-instance environment,
 550 we are careful about multiple matches, as described above in
 551 Note [Overlapping instances]
 552
 553 The key_tys can contain skolem constants, and we can guarantee that those
 554 are never going to be instantiated to anything, so we should not involve
 555 them in the unification test.  Example:
 556         class Foo a where { op :: a -> Int }
 557         instance Foo a => Foo [a]       -- NB overlap
 558         instance Foo [Int]              -- NB overlap
 559         data T = forall a. Foo a => MkT a
 560         f :: T -> Int
 561         f (MkT x) = op [x,x]
 562 The op [x,x] means we need (Foo [a]).  Without the filterVarSet we'd
 563 complain, saying that the choice of instance depended on the instantiation
 564 of 'a'; but of course it isn't *going* to be instantiated.
 565
 566 We do this only for pattern-bound skolems.  For example we reject
 567         g :: forall a => [a] -> Int
 568         g x = op x
 569 on the grounds that the correct instance depends on the instantiation of 'a'