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