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