2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
5 \section[InstEnv]{Utilities for typechecking instance declarations}
7 The bits common to TcInstDcls and TcDeriv.
11 -- The above warning supression flag is a temporary kludge.
12 -- While working on this module you are encouraged to remove it and fix
13 -- any warnings in the module. See
14 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
18 DFunId, OverlapFlag(..),
19 Instance(..), pprInstance, pprInstanceHdr, pprInstances,
20 instanceHead, mkLocalInstance, mkImportedInstance,
21 instanceDFunId, setInstanceDFunId, instanceRoughTcs,
23 InstEnv, emptyInstEnv, extendInstEnv,
24 extendInstEnvList, lookupInstEnv, instEnvElts,
26 instanceCantMatch, roughMatchTcs
29 #include "HsVersions.h"
45 import Data.Maybe ( isJust, isNothing )
49 %************************************************************************
51 \subsection{The key types}
53 %************************************************************************
58 = Instance { is_cls :: Name -- Class name
60 -- Used for "rough matching"; see Note [Rough-match field]
61 -- INVARIANT: is_tcs = roughMatchTcs is_tys
62 , is_tcs :: [Maybe Name] -- Top of type args
64 -- Used for "proper matching"; see Note [Proper-match fields]
65 , is_tvs :: TyVarSet -- Template tyvars for full match
66 , is_tys :: [Type] -- Full arg types
67 -- INVARIANT: is_dfun Id has type
68 -- forall is_tvs. (...) => is_cls is_tys
71 , is_flag :: OverlapFlag -- See detailed comments with
72 -- the decl of BasicTypes.OverlapFlag
76 Note [Rough-match field]
77 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
78 The is_cls, is_tcs fields allow a "rough match" to be done
79 without poking inside the DFunId. Poking the DFunId forces
80 us to suck in all the type constructors etc it involves,
81 which is a total waste of time if it has no chance of matching
82 So the Name, [Maybe Name] fields allow us to say "definitely
83 does not match", based only on the Name.
86 Nothing means that this type arg is a type variable
88 (Just n) means that this type arg is a
89 TyConApp with a type constructor of n.
90 This is always a real tycon, never a synonym!
91 (Two different synonyms might match, but two
92 different real tycons can't.)
93 NB: newtypes are not transparent, though!
95 Note [Proper-match fields]
96 ~~~~~~~~~~~~~~~~~~~~~~~~~
97 The is_tvs, is_tys fields are simply cached values, pulled
98 out (lazily) from the dfun id. They are cached here simply so
99 that we don't need to decompose the DFunId each time we want
100 to match it. The hope is that the fast-match fields mean
101 that we often never poke th proper-match fields
104 * is_tvs must be a superset of the free vars of is_tys
106 * The is_dfun must itself be quantified over exactly is_tvs
107 (This is so that we can use the matching substitution to
108 instantiate the dfun's context.)
113 instanceDFunId :: Instance -> DFunId
114 instanceDFunId = is_dfun
116 setInstanceDFunId :: Instance -> DFunId -> Instance
117 setInstanceDFunId ispec dfun
118 = ASSERT( idType dfun `tcEqType` idType (is_dfun ispec) )
119 -- We need to create the cached fields afresh from
120 -- the new dfun id. In particular, the is_tvs in
121 -- the Instance must match those in the dfun!
122 -- We assume that the only thing that changes is
123 -- the quantified type variables, so the other fields
124 -- are ok; hence the assert
125 ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
127 (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
129 instanceRoughTcs :: Instance -> [Maybe Name]
130 instanceRoughTcs = is_tcs
134 instance NamedThing Instance where
135 getName ispec = getName (is_dfun ispec)
137 instance Outputable Instance where
140 pprInstance :: Instance -> SDoc
141 -- Prints the Instance as an instance declaration
142 pprInstance ispec@(Instance { is_flag = flag })
143 = hang (pprInstanceHdr ispec)
144 2 (ptext SLIT("--") <+> pprNameLoc (getName ispec))
146 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
147 pprInstanceHdr :: Instance -> SDoc
148 -- Prints the Instance as an instance declaration
149 pprInstanceHdr ispec@(Instance { is_flag = flag })
150 = ptext SLIT("instance") <+> ppr flag
151 <+> sep [pprThetaArrow theta, pprClassPred clas tys]
153 (_, theta, clas, tys) = instanceHead ispec
154 -- Print without the for-all, which the programmer doesn't write
156 pprInstances :: [Instance] -> SDoc
157 pprInstances ispecs = vcat (map pprInstance ispecs)
159 instanceHead :: Instance -> ([TyVar], [PredType], Class, [Type])
160 instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec))
162 mkLocalInstance :: DFunId -> OverlapFlag -> Instance
163 -- Used for local instances, where we can safely pull on the DFunId
164 mkLocalInstance dfun oflag
165 = Instance { is_flag = oflag, is_dfun = dfun,
166 is_tvs = mkVarSet tvs, is_tys = tys,
167 is_cls = className cls, is_tcs = roughMatchTcs tys }
169 (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
171 mkImportedInstance :: Name -> [Maybe Name]
172 -> DFunId -> OverlapFlag -> Instance
173 -- Used for imported instances, where we get the rough-match stuff
174 -- from the interface file
175 mkImportedInstance cls mb_tcs dfun oflag
176 = Instance { is_flag = oflag, is_dfun = dfun,
177 is_tvs = mkVarSet tvs, is_tys = tys,
178 is_cls = cls, is_tcs = mb_tcs }
180 (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
182 roughMatchTcs :: [Type] -> [Maybe Name]
183 roughMatchTcs tys = map rough tys
185 rough ty = case tcSplitTyConApp_maybe ty of
186 Just (tc,_) -> Just (tyConName tc)
189 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
190 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
191 -- possibly be instantiated to actual, nor vice versa;
192 -- False is non-committal
193 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
194 instanceCantMatch ts as = False -- Safe
198 Note [Overlapping instances]
199 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
200 Overlap is permitted, but only in such a way that one can make
201 a unique choice when looking up. That is, overlap is only permitted if
202 one template matches the other, or vice versa. So this is ok:
210 If overlap is permitted, the list is kept most specific first, so that
211 the first lookup is the right choice.
214 For now we just use association lists.
216 \subsection{Avoiding a problem with overlapping}
218 Consider this little program:
221 class C a where c :: a
222 class C a => D a where d :: a
224 instance C Int where c = 17
225 instance D Int where d = 13
227 instance C a => C [a] where c = [c]
228 instance ({- C [a], -} D a) => D [a] where d = c
230 instance C [Int] where c = [37]
232 main = print (d :: [Int])
235 What do you think `main' prints (assuming we have overlapping instances, and
236 all that turned on)? Well, the instance for `D' at type `[a]' is defined to
237 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
238 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
239 the `C [Int]' instance is more specific).
241 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong. That
242 was easy ;-) Let's just consult hugs for good measure. Wait - if I use old
243 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
244 doesn't even compile! What's going on!?
246 What hugs complains about is the `D [a]' instance decl.
249 ERROR "mj.hs" (line 10): Cannot build superclass instance
251 *** Context supplied : D a
252 *** Required superclass : C [a]
255 You might wonder what hugs is complaining about. It's saying that you
256 need to add `C [a]' to the context of the `D [a]' instance (as appears
257 in comments). But there's that `C [a]' instance decl one line above
258 that says that I can reduce the need for a `C [a]' instance to the
259 need for a `C a' instance, and in this case, I already have the
260 necessary `C a' instance (since we have `D a' explicitly in the
261 context, and `C' is a superclass of `D').
263 Unfortunately, the above reasoning indicates a premature commitment to the
264 generic `C [a]' instance. I.e., it prematurely rules out the more specific
265 instance `C [Int]'. This is the mistake that ghc-4.06 makes. The fix is to
266 add the context that hugs suggests (uncomment the `C [a]'), effectively
267 deferring the decision about which instance to use.
269 Now, interestingly enough, 4.04 has this same bug, but it's covered up
270 in this case by a little known `optimization' that was disabled in
271 4.06. Ghc-4.04 silently inserts any missing superclass context into
272 an instance declaration. In this case, it silently inserts the `C
273 [a]', and everything happens to work out.
275 (See `basicTypes/MkId:mkDictFunId' for the code in question. Search for
276 `Mark Jones', although Mark claims no credit for the `optimization' in
277 question, and would rather it stopped being called the `Mark Jones
280 So, what's the fix? I think hugs has it right. Here's why. Let's try
281 something else out with ghc-4.04. Let's add the following line:
286 Everyone raise their hand who thinks that `d :: [Int]' should give a
287 different answer from `d' :: [Int]'. Well, in ghc-4.04, it does. The
288 `optimization' only applies to instance decls, not to regular
289 bindings, giving inconsistent behavior.
291 Old hugs had this same bug. Here's how we fixed it: like GHC, the
292 list of instances for a given class is ordered, so that more specific
293 instances come before more generic ones. For example, the instance
294 list for C might contain:
295 ..., C Int, ..., C a, ...
296 When we go to look for a `C Int' instance we'll get that one first.
297 But what if we go looking for a `C b' (`b' is unconstrained)? We'll
298 pass the `C Int' instance, and keep going. But if `b' is
299 unconstrained, then we don't know yet if the more specific instance
300 will eventually apply. GHC keeps going, and matches on the generic `C
301 a'. The fix is to, at each step, check to see if there's a reverse
302 match, and if so, abort the search. This prevents hugs from
303 prematurely chosing a generic instance when a more specific one
308 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
309 this test. Suppose the instance envt had
310 ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
311 (still most specific first)
312 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
313 C x y Int doesn't match the template {a,b} C a a b
315 C a a b match the template {x,y} C x y Int
316 But still x and y might subsequently be unified so they *do* match.
318 Simple story: unify, don't match.
321 %************************************************************************
325 %************************************************************************
327 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
328 ClsInstEnv mapping is the dfun for that instance.
330 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
332 forall a b, C t1 t2 t3 can be constructed by dfun
334 or, to put it another way, we have
336 instance (...) => C t1 t2 t3, witnessed by dfun
339 ---------------------------------------------------
340 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
343 = ClsIE [Instance] -- The instances for a particular class, in any order
344 Bool -- True <=> there is an instance of form C a b c
345 -- If *not* then the common case of looking up
346 -- (C a b c) can fail immediately
349 -- * The is_tvs are distinct in each Instance
350 -- of a ClsInstEnv (so we can safely unify them)
352 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
353 -- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
354 -- The "a" in the pattern must be one of the forall'd variables in
357 emptyInstEnv :: InstEnv
358 emptyInstEnv = emptyUFM
360 instEnvElts :: InstEnv -> [Instance]
361 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
363 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
364 classInstances (pkg_ie, home_ie) cls
365 = get home_ie ++ get pkg_ie
367 get env = case lookupUFM env cls of
368 Just (ClsIE insts _) -> insts
371 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
372 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
374 extendInstEnv :: InstEnv -> Instance -> InstEnv
375 extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
376 = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
378 add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
379 (ins_tyvar || cur_tyvar)
380 ins_tyvar = not (any isJust mb_tcs)
384 %************************************************************************
386 \subsection{Looking up an instance}
388 %************************************************************************
390 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
391 the env is kept ordered, the first match must be the only one. The
392 thing we are looking up can have an arbitrary "flexi" part.
395 type InstTypes = [Either TyVar Type]
396 -- Right ty => Instantiate with this type
397 -- Left tv => Instantiate with any type of this tyvar's kind
399 type InstMatch = (Instance, InstTypes)
402 Note [InstTypes: instantiating types]
403 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
404 A successful match is an Instance, together with the types at which
405 the dfun_id in the Instance should be instantiated
406 The instantiating types are (Mabye Type)s because the dfun
407 might have some tyvars that *only* appear in arguments
408 dfun :: forall a b. C a b, Ord b => D [a]
409 When we match this against D [ty], we return the instantiating types
411 where the Nothing indicates that 'b' can be freely instantiated.
412 (The caller instantiates it to a flexi type variable, which will presumably
413 presumably later become fixed via functional dependencies.)
416 lookupInstEnv :: (InstEnv, InstEnv) -- External and home package inst-env
417 -> Class -> [Type] -- What we are looking for
418 -> ([InstMatch], -- Successful matches
419 [Instance]) -- These don't match but do unify
421 -- The second component of the result pair happens when we look up
423 -- in an InstEnv that has entries for
426 -- Then which we choose would depend on the way in which 'a'
427 -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
428 -- but Foo [Int] is a unifier. This gives the caller a better chance of
429 -- giving a suitable error messagen
431 lookupInstEnv (pkg_ie, home_ie) cls tys
432 = (pruned_matches, all_unifs)
434 rough_tcs = roughMatchTcs tys
435 all_tvs = all isNothing rough_tcs
436 (home_matches, home_unifs) = lookup home_ie
437 (pkg_matches, pkg_unifs) = lookup pkg_ie
438 all_matches = home_matches ++ pkg_matches
439 all_unifs = home_unifs ++ pkg_unifs
440 pruned_matches = foldr insert_overlapping [] all_matches
441 -- Even if the unifs is non-empty (an error situation)
442 -- we still prune the matches, so that the error message isn't
443 -- misleading (complaining of multiple matches when some should be
447 lookup env = case lookupUFM env cls of
448 Nothing -> ([],[]) -- No instances for this class
449 Just (ClsIE insts has_tv_insts)
450 | all_tvs && not has_tv_insts
451 -> ([],[]) -- Short cut for common case
452 -- The thing we are looking up is of form (C a b c), and
453 -- the ClsIE has no instances of that form, so don't bother to search
459 lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
460 -- See Note [InstTypes: instantiating types]
461 lookup_tv subst tv = case lookupTyVar subst tv of
465 find ms us [] = (ms, us)
466 find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs,
467 is_tys = tpl_tys, is_flag = oflag,
468 is_dfun = dfun }) : rest)
469 -- Fast check for no match, uses the "rough match" fields
470 | instanceCantMatch rough_tcs mb_tcs
473 | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
475 (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
477 ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant
478 find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
480 -- Does not match, so next check whether the things unify
481 -- See Note [overlapping instances] above
482 | Incoherent <- oflag
486 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
487 (ppr cls <+> ppr tys <+> ppr all_tvs) $$
488 (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
490 -- Unification will break badly if the variables overlap
491 -- They shouldn't because we allocate separate uniques for them
492 case tcUnifyTys bind_fn tpl_tys tys of
493 Just _ -> find ms (item:us) rest
494 Nothing -> find ms us rest
497 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
499 -- The key_tys can contain skolem constants, and we can guarantee that those
500 -- are never going to be instantiated to anything, so we should not involve
501 -- them in the unification test. Example:
502 -- class Foo a where { op :: a -> Int }
503 -- instance Foo a => Foo [a] -- NB overlap
504 -- instance Foo [Int] -- NB overlap
505 -- data T = forall a. Foo a => MkT a
507 -- f (MkT x) = op [x,x]
508 -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
509 -- complain, saying that the choice of instance depended on the instantiation
510 -- of 'a'; but of course it isn't *going* to be instantiated.
512 -- We do this only for pattern-bound skolems. For example we reject
513 -- g :: forall a => [a] -> Int
515 -- on the grounds that the correct instance depends on the instantiation of 'a'
518 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
519 -- Add a new solution, knocking out strictly less specific ones
520 insert_overlapping new_item [] = [new_item]
521 insert_overlapping new_item (item:items)
522 | new_beats_old && old_beats_new = item : insert_overlapping new_item items
523 -- Duplicate => keep both for error report
524 | new_beats_old = insert_overlapping new_item items
526 | old_beats_new = item : items
528 | otherwise = item : insert_overlapping new_item items
531 new_beats_old = new_item `beats` item
532 old_beats_new = item `beats` new_item
534 (instA, _) `beats` (instB, _)
536 isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
537 -- A beats B if A is more specific than B, and B admits overlap
538 -- I.e. if B can be instantiated to match A
540 overlap_ok = case is_flag instB of