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