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 DFunId, OverlapFlag(..),
12 Instance(..), pprInstance, pprInstanceHdr, pprInstances,
13 instanceHead, mkLocalInstance, mkImportedInstance,
14 instanceDFunId, setInstanceDFunId, instanceRoughTcs,
16 InstEnv, emptyInstEnv, extendInstEnv,
17 extendInstEnvList, lookupInstEnv, instEnvElts,
19 instanceCantMatch, roughMatchTcs
22 #include "HsVersions.h"
38 import Data.Maybe ( isJust, isNothing )
42 %************************************************************************
44 \subsection{The key types}
46 %************************************************************************
51 = Instance { is_cls :: Name -- Class name
53 -- Used for "rough matching"; see Note [Rough-match field]
54 -- INVARIANT: is_tcs = roughMatchTcs is_tys
55 , is_tcs :: [Maybe Name] -- Top of type args
57 -- Used for "proper matching"; see Note [Proper-match fields]
58 , is_tvs :: TyVarSet -- Template tyvars for full match
59 , is_tys :: [Type] -- Full arg types
60 -- INVARIANT: is_dfun Id has type
61 -- forall is_tvs. (...) => is_cls is_tys
64 , is_flag :: OverlapFlag -- See detailed comments with
65 -- the decl of BasicTypes.OverlapFlag
69 Note [Rough-match field]
70 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
71 The is_cls, is_tcs fields allow a "rough match" to be done
72 without poking inside the DFunId. Poking the DFunId forces
73 us to suck in all the type constructors etc it involves,
74 which is a total waste of time if it has no chance of matching
75 So the Name, [Maybe Name] fields allow us to say "definitely
76 does not match", based only on the Name.
79 Nothing means that this type arg is a type variable
81 (Just n) means that this type arg is a
82 TyConApp with a type constructor of n.
83 This is always a real tycon, never a synonym!
84 (Two different synonyms might match, but two
85 different real tycons can't.)
86 NB: newtypes are not transparent, though!
88 Note [Proper-match fields]
89 ~~~~~~~~~~~~~~~~~~~~~~~~~
90 The is_tvs, is_tys fields are simply cached values, pulled
91 out (lazily) from the dfun id. They are cached here simply so
92 that we don't need to decompose the DFunId each time we want
93 to match it. The hope is that the fast-match fields mean
94 that we often never poke th proper-match fields
97 * is_tvs must be a superset of the free vars of is_tys
99 * The is_dfun must itself be quantified over exactly is_tvs
100 (This is so that we can use the matching substitution to
101 instantiate the dfun's context.)
106 instanceDFunId :: Instance -> DFunId
107 instanceDFunId = is_dfun
109 setInstanceDFunId :: Instance -> DFunId -> Instance
110 setInstanceDFunId ispec dfun
111 = ASSERT( idType dfun `tcEqType` idType (is_dfun ispec) )
112 -- We need to create the cached fields afresh from
113 -- the new dfun id. In particular, the is_tvs in
114 -- the Instance must match those in the dfun!
115 -- We assume that the only thing that changes is
116 -- the quantified type variables, so the other fields
117 -- are ok; hence the assert
118 ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
120 (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
122 instanceRoughTcs :: Instance -> [Maybe Name]
123 instanceRoughTcs = is_tcs
127 instance NamedThing Instance where
128 getName ispec = getName (is_dfun ispec)
130 instance Outputable Instance where
133 pprInstance :: Instance -> SDoc
134 -- Prints the Instance as an instance declaration
135 pprInstance ispec@(Instance { is_flag = flag })
136 = hang (pprInstanceHdr ispec)
137 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcSpan ispec)))
139 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
140 pprInstanceHdr :: Instance -> SDoc
141 -- Prints the Instance as an instance declaration
142 pprInstanceHdr ispec@(Instance { is_flag = flag })
143 = ptext SLIT("instance") <+> ppr flag
144 <+> sep [pprThetaArrow theta, pprClassPred clas tys]
146 (_, theta, clas, tys) = instanceHead ispec
147 -- Print without the for-all, which the programmer doesn't write
149 pprInstances :: [Instance] -> SDoc
150 pprInstances ispecs = vcat (map pprInstance ispecs)
152 instanceHead :: Instance -> ([TyVar], [PredType], Class, [Type])
153 instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec))
155 mkLocalInstance :: DFunId -> OverlapFlag -> Instance
156 -- Used for local instances, where we can safely pull on the DFunId
157 mkLocalInstance dfun oflag
158 = Instance { is_flag = oflag, is_dfun = dfun,
159 is_tvs = mkVarSet tvs, is_tys = tys,
160 is_cls = className cls, is_tcs = roughMatchTcs tys }
162 (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
164 mkImportedInstance :: Name -> [Maybe Name]
165 -> DFunId -> OverlapFlag -> Instance
166 -- Used for imported instances, where we get the rough-match stuff
167 -- from the interface file
168 mkImportedInstance cls mb_tcs dfun oflag
169 = Instance { is_flag = oflag, is_dfun = dfun,
170 is_tvs = mkVarSet tvs, is_tys = tys,
171 is_cls = cls, is_tcs = mb_tcs }
173 (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
175 roughMatchTcs :: [Type] -> [Maybe Name]
176 roughMatchTcs tys = map rough tys
178 rough ty = case tcSplitTyConApp_maybe ty of
179 Just (tc,_) -> Just (tyConName tc)
182 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
183 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
184 -- possibly be instantiated to actual, nor vice versa;
185 -- False is non-committal
186 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
187 instanceCantMatch ts as = False -- Safe
191 Note [Overlapping instances]
192 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
193 Overlap is permitted, but only in such a way that one can make
194 a unique choice when looking up. That is, overlap is only permitted if
195 one template matches the other, or vice versa. So this is ok:
203 If overlap is permitted, the list is kept most specific first, so that
204 the first lookup is the right choice.
207 For now we just use association lists.
209 \subsection{Avoiding a problem with overlapping}
211 Consider this little program:
214 class C a where c :: a
215 class C a => D a where d :: a
217 instance C Int where c = 17
218 instance D Int where d = 13
220 instance C a => C [a] where c = [c]
221 instance ({- C [a], -} D a) => D [a] where d = c
223 instance C [Int] where c = [37]
225 main = print (d :: [Int])
228 What do you think `main' prints (assuming we have overlapping instances, and
229 all that turned on)? Well, the instance for `D' at type `[a]' is defined to
230 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
231 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
232 the `C [Int]' instance is more specific).
234 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong. That
235 was easy ;-) Let's just consult hugs for good measure. Wait - if I use old
236 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
237 doesn't even compile! What's going on!?
239 What hugs complains about is the `D [a]' instance decl.
242 ERROR "mj.hs" (line 10): Cannot build superclass instance
244 *** Context supplied : D a
245 *** Required superclass : C [a]
248 You might wonder what hugs is complaining about. It's saying that you
249 need to add `C [a]' to the context of the `D [a]' instance (as appears
250 in comments). But there's that `C [a]' instance decl one line above
251 that says that I can reduce the need for a `C [a]' instance to the
252 need for a `C a' instance, and in this case, I already have the
253 necessary `C a' instance (since we have `D a' explicitly in the
254 context, and `C' is a superclass of `D').
256 Unfortunately, the above reasoning indicates a premature commitment to the
257 generic `C [a]' instance. I.e., it prematurely rules out the more specific
258 instance `C [Int]'. This is the mistake that ghc-4.06 makes. The fix is to
259 add the context that hugs suggests (uncomment the `C [a]'), effectively
260 deferring the decision about which instance to use.
262 Now, interestingly enough, 4.04 has this same bug, but it's covered up
263 in this case by a little known `optimization' that was disabled in
264 4.06. Ghc-4.04 silently inserts any missing superclass context into
265 an instance declaration. In this case, it silently inserts the `C
266 [a]', and everything happens to work out.
268 (See `basicTypes/MkId:mkDictFunId' for the code in question. Search for
269 `Mark Jones', although Mark claims no credit for the `optimization' in
270 question, and would rather it stopped being called the `Mark Jones
273 So, what's the fix? I think hugs has it right. Here's why. Let's try
274 something else out with ghc-4.04. Let's add the following line:
279 Everyone raise their hand who thinks that `d :: [Int]' should give a
280 different answer from `d' :: [Int]'. Well, in ghc-4.04, it does. The
281 `optimization' only applies to instance decls, not to regular
282 bindings, giving inconsistent behavior.
284 Old hugs had this same bug. Here's how we fixed it: like GHC, the
285 list of instances for a given class is ordered, so that more specific
286 instances come before more generic ones. For example, the instance
287 list for C might contain:
288 ..., C Int, ..., C a, ...
289 When we go to look for a `C Int' instance we'll get that one first.
290 But what if we go looking for a `C b' (`b' is unconstrained)? We'll
291 pass the `C Int' instance, and keep going. But if `b' is
292 unconstrained, then we don't know yet if the more specific instance
293 will eventually apply. GHC keeps going, and matches on the generic `C
294 a'. The fix is to, at each step, check to see if there's a reverse
295 match, and if so, abort the search. This prevents hugs from
296 prematurely chosing a generic instance when a more specific one
301 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
302 this test. Suppose the instance envt had
303 ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
304 (still most specific first)
305 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
306 C x y Int doesn't match the template {a,b} C a a b
308 C a a b match the template {x,y} C x y Int
309 But still x and y might subsequently be unified so they *do* match.
311 Simple story: unify, don't match.
314 %************************************************************************
318 %************************************************************************
320 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
321 ClsInstEnv mapping is the dfun for that instance.
323 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
325 forall a b, C t1 t2 t3 can be constructed by dfun
327 or, to put it another way, we have
329 instance (...) => C t1 t2 t3, witnessed by dfun
332 ---------------------------------------------------
333 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
336 = ClsIE [Instance] -- The instances for a particular class, in any order
337 Bool -- True <=> there is an instance of form C a b c
338 -- If *not* then the common case of looking up
339 -- (C a b c) can fail immediately
342 -- * The is_tvs are distinct in each Instance
343 -- of a ClsInstEnv (so we can safely unify them)
345 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
346 -- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
347 -- The "a" in the pattern must be one of the forall'd variables in
350 emptyInstEnv :: InstEnv
351 emptyInstEnv = emptyUFM
353 instEnvElts :: InstEnv -> [Instance]
354 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
356 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
357 classInstances (pkg_ie, home_ie) cls
358 = get home_ie ++ get pkg_ie
360 get env = case lookupUFM env cls of
361 Just (ClsIE insts _) -> insts
364 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
365 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
367 extendInstEnv :: InstEnv -> Instance -> InstEnv
368 extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
369 = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
371 add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
372 (ins_tyvar || cur_tyvar)
373 ins_tyvar = not (any isJust mb_tcs)
377 %************************************************************************
379 \subsection{Looking up an instance}
381 %************************************************************************
383 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
384 the env is kept ordered, the first match must be the only one. The
385 thing we are looking up can have an arbitrary "flexi" part.
388 type InstTypes = [Either TyVar Type]
389 -- Right ty => Instantiate with this type
390 -- Left tv => Instantiate with any type of this tyvar's kind
392 type InstMatch = (Instance, InstTypes)
395 Note [InstTypes: instantiating types]
396 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
397 A successful match is an Instance, together with the types at which
398 the dfun_id in the Instance should be instantiated
399 The instantiating types are (Mabye Type)s because the dfun
400 might have some tyvars that *only* appear in arguments
401 dfun :: forall a b. C a b, Ord b => D [a]
402 When we match this against D [ty], we return the instantiating types
404 where the Nothing indicates that 'b' can be freely instantiated.
405 (The caller instantiates it to a flexi type variable, which will presumably
406 presumably later become fixed via functional dependencies.)
409 lookupInstEnv :: (InstEnv, InstEnv) -- External and home package inst-env
410 -> Class -> [Type] -- What we are looking for
411 -> ([InstMatch], -- Successful matches
412 [Instance]) -- These don't match but do unify
414 -- The second component of the result pair happens when we look up
416 -- in an InstEnv that has entries for
419 -- Then which we choose would depend on the way in which 'a'
420 -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
421 -- but Foo [Int] is a unifier. This gives the caller a better chance of
422 -- giving a suitable error messagen
424 lookupInstEnv (pkg_ie, home_ie) cls tys
425 = (pruned_matches, all_unifs)
427 rough_tcs = roughMatchTcs tys
428 all_tvs = all isNothing rough_tcs
429 (home_matches, home_unifs) = lookup home_ie
430 (pkg_matches, pkg_unifs) = lookup pkg_ie
431 all_matches = home_matches ++ pkg_matches
432 all_unifs = home_unifs ++ pkg_unifs
433 pruned_matches = foldr insert_overlapping [] all_matches
434 -- Even if the unifs is non-empty (an error situation)
435 -- we still prune the matches, so that the error message isn't
436 -- misleading (complaining of multiple matches when some should be
440 lookup env = case lookupUFM env cls of
441 Nothing -> ([],[]) -- No instances for this class
442 Just (ClsIE insts has_tv_insts)
443 | all_tvs && not has_tv_insts
444 -> ([],[]) -- Short cut for common case
445 -- The thing we are looking up is of form (C a b c), and
446 -- the ClsIE has no instances of that form, so don't bother to search
452 lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
453 -- See Note [InstTypes: instantiating types]
454 lookup_tv subst tv = case lookupTyVar subst tv of
458 find ms us [] = (ms, us)
459 find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs,
460 is_tys = tpl_tys, is_flag = oflag,
461 is_dfun = dfun }) : rest)
462 -- Fast check for no match, uses the "rough match" fields
463 | instanceCantMatch rough_tcs mb_tcs
466 | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
468 (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
470 ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant
471 find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
473 -- Does not match, so next check whether the things unify
474 -- See Note [overlapping instances] above
475 | Incoherent <- oflag
479 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
480 (ppr cls <+> ppr tys <+> ppr all_tvs) $$
481 (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
483 -- Unification will break badly if the variables overlap
484 -- They shouldn't because we allocate separate uniques for them
485 case tcUnifyTys bind_fn tpl_tys tys of
486 Just _ -> find ms (item:us) rest
487 Nothing -> find ms us rest
490 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
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
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.
505 -- We do this only for pattern-bound skolems. For example we reject
506 -- g :: forall a => [a] -> Int
508 -- on the grounds that the correct instance depends on the instantiation of 'a'
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
519 | old_beats_new = item : items
521 | otherwise = item : insert_overlapping new_item items
524 new_beats_old = new_item `beats` item
525 old_beats_new = item `beats` new_item
527 (instA, _) `beats` (instB, _)
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
533 overlap_ok = case is_flag instB of