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,
18 classInstances, instanceBindFun,
19 instanceCantMatch, roughMatchTcs
22 #include "HsVersions.h"
37 import Data.Maybe ( isJust, isNothing )
41 %************************************************************************
43 \subsection{The key types}
45 %************************************************************************
50 = Instance { is_cls :: Name -- Class name
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
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
62 , is_dfun :: DFunId -- See Note [Haddock assumptions]
63 , is_flag :: OverlapFlag -- See detailed comments with
64 -- the decl of BasicTypes.OverlapFlag
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.
78 Nothing means that this type arg is a type variable
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!
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
96 * is_tvs must be a superset of the free vars of is_tys
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.)
102 Note [Haddock assumptions]
103 ~~~~~~~~~~~~~~~~~~~~~~~~~~
104 For normal user-written instances, Haddock relies on
114 * the instance head type of
115 * the InstDecl used to construct the Instance.
118 instanceDFunId :: Instance -> DFunId
119 instanceDFunId = is_dfun
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 }
132 (tvs, _, tys) = tcSplitDFunTy (idType dfun)
134 instanceRoughTcs :: Instance -> [Maybe Name]
135 instanceRoughTcs = is_tcs
139 instance NamedThing Instance where
140 getName ispec = getName (is_dfun ispec)
142 instance Outputable Instance where
145 pprInstance :: Instance -> SDoc
146 -- Prints the Instance as an instance declaration
148 = hang (pprInstanceHdr ispec)
149 2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
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]
158 (_, theta, res_ty) = tcSplitSigmaTy (idType (is_dfun ispec))
159 -- Print without the for-all, which the programmer doesn't write
161 pprInstances :: [Instance] -> SDoc
162 pprInstances ispecs = vcat (map pprInstance ispecs)
164 instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
166 = (tvs, theta, cls, tys)
168 (tvs, theta, tau) = tcSplitSigmaTy (idType (is_dfun ispec))
169 (cls, tys) = tcSplitDFunHead tau
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 }
178 (tvs, cls, tys) = tcSplitDFunTy (idType dfun)
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 }
189 (tvs, _, tys) = tcSplitDFunTy (idType dfun)
191 roughMatchTcs :: [Type] -> [Maybe Name]
192 roughMatchTcs tys = map rough tys
194 rough ty = case tcSplitTyConApp_maybe ty of
195 Just (tc,_) -> Just (tyConName tc)
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
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:
219 If overlap is permitted, the list is kept most specific first, so that
220 the first lookup is the right choice.
223 For now we just use association lists.
225 \subsection{Avoiding a problem with overlapping}
227 Consider this little program:
230 class C a where c :: a
231 class C a => D a where d :: a
233 instance C Int where c = 17
234 instance D Int where d = 13
236 instance C a => C [a] where c = [c]
237 instance ({- C [a], -} D a) => D [a] where d = c
239 instance C [Int] where c = [37]
241 main = print (d :: [Int])
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).
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!?
255 What hugs complains about is the `D [a]' instance decl.
258 ERROR "mj.hs" (line 10): Cannot build superclass instance
260 *** Context supplied : D a
261 *** Required superclass : C [a]
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').
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.
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.
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
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:
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.
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
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
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.
327 Simple story: unify, don't match.
330 %************************************************************************
334 %************************************************************************
336 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
337 ClsInstEnv mapping is the dfun for that instance.
339 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
341 forall a b, C t1 t2 t3 can be constructed by dfun
343 or, to put it another way, we have
345 instance (...) => C t1 t2 t3, witnessed by dfun
348 ---------------------------------------------------
349 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
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
358 -- * The is_tvs are distinct in each Instance
359 -- of a ClsInstEnv (so we can safely unify them)
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
366 emptyInstEnv :: InstEnv
367 emptyInstEnv = emptyUFM
369 instEnvElts :: InstEnv -> [Instance]
370 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
372 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
373 classInstances (pkg_ie, home_ie) cls
374 = get home_ie ++ get pkg_ie
376 get env = case lookupUFM env cls of
377 Just (ClsIE insts _) -> insts
380 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
381 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
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)
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)
393 %************************************************************************
395 Looking up an instance
397 %************************************************************************
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.
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
408 type InstMatch = (Instance, InstTypes)
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
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.)
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
430 -- The second component of the result pair happens when we look up
432 -- in an InstEnv that has entries for
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
440 lookupInstEnv (pkg_ie, home_ie) cls tys
441 = (pruned_matches, all_unifs)
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
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
468 lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
469 -- See Note [InstTypes: instantiating types]
470 lookup_tv subst tv = case lookupTyVar subst tv of
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
482 | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
484 (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
486 ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant
487 find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
489 -- Does not match, so next check whether the things unify
490 -- See Note [overlapping instances] above
491 | Incoherent <- oflag
495 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
496 (ppr cls <+> ppr tys <+> ppr all_tvs) $$
497 (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
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
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
515 | old_beats_new = item : items
517 | otherwise = item : insert_overlapping new_item items
520 new_beats_old = new_item `beats` item
521 old_beats_new = item `beats` new_item
523 (instA, _) `beats` (instB, _)
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
529 overlap_ok = case is_flag instB of
535 %************************************************************************
539 %************************************************************************
542 instanceBindFun :: TyVar -> BindFlag
543 instanceBindFun tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
545 -- Note [Binding when looking up instances]
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]
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
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.
567 We do this only for pattern-bound skolems. For example we reject
568 g :: forall a => [a] -> Int
570 on the grounds that the correct instance depends on the instantiation of 'a'