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 %************************************************************************
49 = Instance { is_cls :: Name -- Class name
51 -- Used for "rough matching"; see Note [Rough-match field]
52 -- INVARIANT: is_tcs = roughMatchTcs is_tys
53 , is_tcs :: [Maybe Name] -- Top of type args
55 -- Used for "proper matching"; see Note [Proper-match fields]
56 , is_tvs :: TyVarSet -- Template tyvars for full match
57 , is_tys :: [Type] -- Full arg types
58 -- INVARIANT: is_dfun Id has type
59 -- forall is_tvs. (...) => is_cls is_tys
61 , is_dfun :: DFunId -- See Note [Haddock assumptions]
62 , is_flag :: OverlapFlag -- See detailed comments with
63 -- the decl of BasicTypes.OverlapFlag
67 Note [Rough-match field]
68 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
69 The is_cls, is_tcs fields allow a "rough match" to be done
70 without poking inside the DFunId. Poking the DFunId forces
71 us to suck in all the type constructors etc it involves,
72 which is a total waste of time if it has no chance of matching
73 So the Name, [Maybe Name] fields allow us to say "definitely
74 does not match", based only on the Name.
77 Nothing means that this type arg is a type variable
79 (Just n) means that this type arg is a
80 TyConApp with a type constructor of n.
81 This is always a real tycon, never a synonym!
82 (Two different synonyms might match, but two
83 different real tycons can't.)
84 NB: newtypes are not transparent, though!
86 Note [Proper-match fields]
87 ~~~~~~~~~~~~~~~~~~~~~~~~~
88 The is_tvs, is_tys fields are simply cached values, pulled
89 out (lazily) from the dfun id. They are cached here simply so
90 that we don't need to decompose the DFunId each time we want
91 to match it. The hope is that the fast-match fields mean
92 that we often never poke th proper-match fields
95 * is_tvs must be a superset of the free vars of is_tys
97 * The is_dfun must itself be quantified over exactly is_tvs
98 (This is so that we can use the matching substitution to
99 instantiate the dfun's context.)
101 Note [Haddock assumptions]
102 ~~~~~~~~~~~~~~~~~~~~~~~~~~
103 For normal user-written instances, Haddock relies on
113 * the instance head type of
114 * the InstDecl used to construct the Instance.
117 instanceDFunId :: Instance -> DFunId
118 instanceDFunId = is_dfun
120 setInstanceDFunId :: Instance -> DFunId -> Instance
121 setInstanceDFunId ispec dfun
122 = ASSERT( idType dfun `tcEqType` idType (is_dfun ispec) )
123 -- We need to create the cached fields afresh from
124 -- the new dfun id. In particular, the is_tvs in
125 -- the Instance must match those in the dfun!
126 -- We assume that the only thing that changes is
127 -- the quantified type variables, so the other fields
128 -- are ok; hence the assert
129 ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
131 (tvs, _, tys) = tcSplitDFunTy (idType dfun)
133 instanceRoughTcs :: Instance -> [Maybe Name]
134 instanceRoughTcs = is_tcs
138 instance NamedThing Instance where
139 getName ispec = getName (is_dfun ispec)
141 instance Outputable Instance where
144 pprInstance :: Instance -> SDoc
145 -- Prints the Instance as an instance declaration
147 = hang (pprInstanceHdr ispec)
148 2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
150 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
151 pprInstanceHdr :: Instance -> SDoc
152 -- Prints the Instance as an instance declaration
153 pprInstanceHdr ispec@(Instance { is_flag = flag })
154 = ptext (sLit "instance") <+> ppr flag
155 <+> sep [pprThetaArrow theta, ppr res_ty]
157 (_, theta, res_ty) = tcSplitSigmaTy (idType (is_dfun ispec))
158 -- Print without the for-all, which the programmer doesn't write
160 pprInstances :: [Instance] -> SDoc
161 pprInstances ispecs = vcat (map pprInstance ispecs)
163 instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
165 = (tvs, theta, cls, tys)
167 (tvs, theta, tau) = tcSplitSigmaTy (idType (is_dfun ispec))
168 (cls, tys) = tcSplitDFunHead tau
170 mkLocalInstance :: DFunId -> OverlapFlag -> Instance
171 -- Used for local instances, where we can safely pull on the DFunId
172 mkLocalInstance dfun oflag
173 = Instance { is_flag = oflag, is_dfun = dfun,
174 is_tvs = mkVarSet tvs, is_tys = tys,
175 is_cls = className cls, is_tcs = roughMatchTcs tys }
177 (tvs, cls, tys) = tcSplitDFunTy (idType dfun)
179 mkImportedInstance :: Name -> [Maybe Name]
180 -> DFunId -> OverlapFlag -> Instance
181 -- Used for imported instances, where we get the rough-match stuff
182 -- from the interface file
183 mkImportedInstance cls mb_tcs dfun oflag
184 = Instance { is_flag = oflag, is_dfun = dfun,
185 is_tvs = mkVarSet tvs, is_tys = tys,
186 is_cls = cls, is_tcs = mb_tcs }
188 (tvs, _, tys) = tcSplitDFunTy (idType dfun)
190 roughMatchTcs :: [Type] -> [Maybe Name]
191 roughMatchTcs tys = map rough tys
193 rough ty = case tcSplitTyConApp_maybe ty of
194 Just (tc,_) -> Just (tyConName tc)
197 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
198 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
199 -- possibly be instantiated to actual, nor vice versa;
200 -- False is non-committal
201 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
202 instanceCantMatch _ _ = False -- Safe
206 Note [Overlapping instances]
207 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
208 Overlap is permitted, but only in such a way that one can make
209 a unique choice when looking up. That is, overlap is only permitted if
210 one template matches the other, or vice versa. So this is ok:
218 If overlap is permitted, the list is kept most specific first, so that
219 the first lookup is the right choice.
222 For now we just use association lists.
224 \subsection{Avoiding a problem with overlapping}
226 Consider this little program:
229 class C a where c :: a
230 class C a => D a where d :: a
232 instance C Int where c = 17
233 instance D Int where d = 13
235 instance C a => C [a] where c = [c]
236 instance ({- C [a], -} D a) => D [a] where d = c
238 instance C [Int] where c = [37]
240 main = print (d :: [Int])
243 What do you think `main' prints (assuming we have overlapping instances, and
244 all that turned on)? Well, the instance for `D' at type `[a]' is defined to
245 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
246 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
247 the `C [Int]' instance is more specific).
249 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong. That
250 was easy ;-) Let's just consult hugs for good measure. Wait - if I use old
251 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
252 doesn't even compile! What's going on!?
254 What hugs complains about is the `D [a]' instance decl.
257 ERROR "mj.hs" (line 10): Cannot build superclass instance
259 *** Context supplied : D a
260 *** Required superclass : C [a]
263 You might wonder what hugs is complaining about. It's saying that you
264 need to add `C [a]' to the context of the `D [a]' instance (as appears
265 in comments). But there's that `C [a]' instance decl one line above
266 that says that I can reduce the need for a `C [a]' instance to the
267 need for a `C a' instance, and in this case, I already have the
268 necessary `C a' instance (since we have `D a' explicitly in the
269 context, and `C' is a superclass of `D').
271 Unfortunately, the above reasoning indicates a premature commitment to the
272 generic `C [a]' instance. I.e., it prematurely rules out the more specific
273 instance `C [Int]'. This is the mistake that ghc-4.06 makes. The fix is to
274 add the context that hugs suggests (uncomment the `C [a]'), effectively
275 deferring the decision about which instance to use.
277 Now, interestingly enough, 4.04 has this same bug, but it's covered up
278 in this case by a little known `optimization' that was disabled in
279 4.06. Ghc-4.04 silently inserts any missing superclass context into
280 an instance declaration. In this case, it silently inserts the `C
281 [a]', and everything happens to work out.
283 (See `basicTypes/MkId:mkDictFunId' for the code in question. Search for
284 `Mark Jones', although Mark claims no credit for the `optimization' in
285 question, and would rather it stopped being called the `Mark Jones
288 So, what's the fix? I think hugs has it right. Here's why. Let's try
289 something else out with ghc-4.04. Let's add the following line:
294 Everyone raise their hand who thinks that `d :: [Int]' should give a
295 different answer from `d' :: [Int]'. Well, in ghc-4.04, it does. The
296 `optimization' only applies to instance decls, not to regular
297 bindings, giving inconsistent behavior.
299 Old hugs had this same bug. Here's how we fixed it: like GHC, the
300 list of instances for a given class is ordered, so that more specific
301 instances come before more generic ones. For example, the instance
302 list for C might contain:
303 ..., C Int, ..., C a, ...
304 When we go to look for a `C Int' instance we'll get that one first.
305 But what if we go looking for a `C b' (`b' is unconstrained)? We'll
306 pass the `C Int' instance, and keep going. But if `b' is
307 unconstrained, then we don't know yet if the more specific instance
308 will eventually apply. GHC keeps going, and matches on the generic `C
309 a'. The fix is to, at each step, check to see if there's a reverse
310 match, and if so, abort the search. This prevents hugs from
311 prematurely chosing a generic instance when a more specific one
316 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
317 this test. Suppose the instance envt had
318 ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
319 (still most specific first)
320 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
321 C x y Int doesn't match the template {a,b} C a a b
323 C a a b match the template {x,y} C x y Int
324 But still x and y might subsequently be unified so they *do* match.
326 Simple story: unify, don't match.
329 %************************************************************************
333 %************************************************************************
335 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
336 ClsInstEnv mapping is the dfun for that instance.
338 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
340 forall a b, C t1 t2 t3 can be constructed by dfun
342 or, to put it another way, we have
344 instance (...) => C t1 t2 t3, witnessed by dfun
347 ---------------------------------------------------
348 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
351 = ClsIE [Instance] -- The instances for a particular class, in any order
352 Bool -- True <=> there is an instance of form C a b c
353 -- If *not* then the common case of looking up
354 -- (C a b c) can fail immediately
357 -- * The is_tvs are distinct in each Instance
358 -- of a ClsInstEnv (so we can safely unify them)
360 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
361 -- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
362 -- The "a" in the pattern must be one of the forall'd variables in
365 emptyInstEnv :: InstEnv
366 emptyInstEnv = emptyUFM
368 instEnvElts :: InstEnv -> [Instance]
369 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
371 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
372 classInstances (pkg_ie, home_ie) cls
373 = get home_ie ++ get pkg_ie
375 get env = case lookupUFM env cls of
376 Just (ClsIE insts _) -> insts
379 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
380 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
382 extendInstEnv :: InstEnv -> Instance -> InstEnv
383 extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
384 = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
386 add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
387 (ins_tyvar || cur_tyvar)
388 ins_tyvar = not (any isJust mb_tcs)
392 %************************************************************************
394 Looking up an instance
396 %************************************************************************
398 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
399 the env is kept ordered, the first match must be the only one. The
400 thing we are looking up can have an arbitrary "flexi" part.
403 type InstTypes = [Either TyVar Type]
404 -- Right ty => Instantiate with this type
405 -- Left tv => Instantiate with any type of this tyvar's kind
407 type InstMatch = (Instance, InstTypes)
410 Note [InstTypes: instantiating types]
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
412 A successful match is an Instance, together with the types at which
413 the dfun_id in the Instance should be instantiated
414 The instantiating types are (Mabye Type)s because the dfun
415 might have some tyvars that *only* appear in arguments
416 dfun :: forall a b. C a b, Ord b => D [a]
417 When we match this against D [ty], we return the instantiating types
419 where the Nothing indicates that 'b' can be freely instantiated.
420 (The caller instantiates it to a flexi type variable, which will presumably
421 presumably later become fixed via functional dependencies.)
424 lookupInstEnv :: (InstEnv, InstEnv) -- External and home package inst-env
425 -> Class -> [Type] -- What we are looking for
426 -> ([InstMatch], -- Successful matches
427 [Instance]) -- These don't match but do unify
429 -- The second component of the result pair happens when we look up
431 -- in an InstEnv that has entries for
434 -- Then which we choose would depend on the way in which 'a'
435 -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
436 -- but Foo [Int] is a unifier. This gives the caller a better chance of
437 -- giving a suitable error messagen
439 lookupInstEnv (pkg_ie, home_ie) cls tys
440 = (pruned_matches, all_unifs)
442 rough_tcs = roughMatchTcs tys
443 all_tvs = all isNothing rough_tcs
444 (home_matches, home_unifs) = lookup home_ie
445 (pkg_matches, pkg_unifs) = lookup pkg_ie
446 all_matches = home_matches ++ pkg_matches
447 all_unifs = home_unifs ++ pkg_unifs
448 pruned_matches = foldr insert_overlapping [] all_matches
449 -- Even if the unifs is non-empty (an error situation)
450 -- we still prune the matches, so that the error message isn't
451 -- misleading (complaining of multiple matches when some should be
455 lookup env = case lookupUFM env cls of
456 Nothing -> ([],[]) -- No instances for this class
457 Just (ClsIE insts has_tv_insts)
458 | all_tvs && not has_tv_insts
459 -> ([],[]) -- Short cut for common case
460 -- The thing we are looking up is of form (C a b c), and
461 -- the ClsIE has no instances of that form, so don't bother to search
467 lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
468 -- See Note [InstTypes: instantiating types]
469 lookup_tv subst tv = case lookupTyVar subst tv of
473 find ms us [] = (ms, us)
474 find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs,
475 is_tys = tpl_tys, is_flag = oflag,
476 is_dfun = dfun }) : rest)
477 -- Fast check for no match, uses the "rough match" fields
478 | instanceCantMatch rough_tcs mb_tcs
481 | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
483 (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
485 ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant
486 find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
488 -- Does not match, so next check whether the things unify
489 -- See Note [overlapping instances] above
490 | Incoherent <- oflag
494 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
495 (ppr cls <+> ppr tys <+> ppr all_tvs) $$
496 (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
498 -- Unification will break badly if the variables overlap
499 -- They shouldn't because we allocate separate uniques for them
500 case tcUnifyTys instanceBindFun tpl_tys tys of
501 Just _ -> find ms (item:us) rest
502 Nothing -> find ms us rest
506 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
507 -- Add a new solution, knocking out strictly less specific ones
508 insert_overlapping new_item [] = [new_item]
509 insert_overlapping new_item (item:items)
510 | new_beats_old && old_beats_new = item : insert_overlapping new_item items
511 -- Duplicate => keep both for error report
512 | new_beats_old = insert_overlapping new_item items
514 | old_beats_new = item : items
516 | otherwise = item : insert_overlapping new_item items
519 new_beats_old = new_item `beats` item
520 old_beats_new = item `beats` new_item
522 (instA, _) `beats` (instB, _)
524 isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
525 -- A beats B if A is more specific than B, and B admits overlap
526 -- I.e. if B can be instantiated to match A
528 overlap_ok = case is_flag instB of
534 %************************************************************************
538 %************************************************************************
541 instanceBindFun :: TyVar -> BindFlag
542 instanceBindFun tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
544 -- Note [Binding when looking up instances]
547 Note [Binding when looking up instances]
548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
549 When looking up in the instance environment, or family-instance environment,
550 we are careful about multiple matches, as described above in
551 Note [Overlapping instances]
553 The key_tys can contain skolem constants, and we can guarantee that those
554 are never going to be instantiated to anything, so we should not involve
555 them in the unification test. Example:
556 class Foo a where { op :: a -> Int }
557 instance Foo a => Foo [a] -- NB overlap
558 instance Foo [Int] -- NB overlap
559 data T = forall a. Foo a => MkT a
562 The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
563 complain, saying that the choice of instance depended on the instantiation
564 of 'a'; but of course it isn't *going* to be instantiated.
566 We do this only for pattern-bound skolems. For example we reject
567 g :: forall a => [a] -> Int
569 on the grounds that the correct instance depends on the instantiation of 'a'