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
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.)
105 instanceDFunId :: Instance -> DFunId
106 instanceDFunId = is_dfun
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 }
119 (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
121 instanceRoughTcs :: Instance -> [Maybe Name]
122 instanceRoughTcs = is_tcs
126 instance NamedThing Instance where
127 getName ispec = getName (is_dfun ispec)
129 instance Outputable Instance where
132 pprInstance :: Instance -> SDoc
133 -- Prints the Instance as an instance declaration
135 = hang (pprInstanceHdr ispec)
136 2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
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]
145 (_, theta, clas, tys) = instanceHead ispec
146 -- Print without the for-all, which the programmer doesn't write
148 pprInstances :: [Instance] -> SDoc
149 pprInstances ispecs = vcat (map pprInstance ispecs)
151 instanceHead :: Instance -> ([TyVar], [PredType], Class, [Type])
152 instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec))
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 }
161 (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
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 }
172 (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
174 roughMatchTcs :: [Type] -> [Maybe Name]
175 roughMatchTcs tys = map rough tys
177 rough ty = case tcSplitTyConApp_maybe ty of
178 Just (tc,_) -> Just (tyConName tc)
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
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:
202 If overlap is permitted, the list is kept most specific first, so that
203 the first lookup is the right choice.
206 For now we just use association lists.
208 \subsection{Avoiding a problem with overlapping}
210 Consider this little program:
213 class C a where c :: a
214 class C a => D a where d :: a
216 instance C Int where c = 17
217 instance D Int where d = 13
219 instance C a => C [a] where c = [c]
220 instance ({- C [a], -} D a) => D [a] where d = c
222 instance C [Int] where c = [37]
224 main = print (d :: [Int])
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).
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!?
238 What hugs complains about is the `D [a]' instance decl.
241 ERROR "mj.hs" (line 10): Cannot build superclass instance
243 *** Context supplied : D a
244 *** Required superclass : C [a]
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').
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.
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.
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
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:
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.
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
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
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.
310 Simple story: unify, don't match.
313 %************************************************************************
317 %************************************************************************
319 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
320 ClsInstEnv mapping is the dfun for that instance.
322 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
324 forall a b, C t1 t2 t3 can be constructed by dfun
326 or, to put it another way, we have
328 instance (...) => C t1 t2 t3, witnessed by dfun
331 ---------------------------------------------------
332 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
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
341 -- * The is_tvs are distinct in each Instance
342 -- of a ClsInstEnv (so we can safely unify them)
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
349 emptyInstEnv :: InstEnv
350 emptyInstEnv = emptyUFM
352 instEnvElts :: InstEnv -> [Instance]
353 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
355 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
356 classInstances (pkg_ie, home_ie) cls
357 = get home_ie ++ get pkg_ie
359 get env = case lookupUFM env cls of
360 Just (ClsIE insts _) -> insts
363 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
364 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
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)
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)
376 %************************************************************************
378 Looking up an instance
380 %************************************************************************
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.
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
391 type InstMatch = (Instance, InstTypes)
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
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.)
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
413 -- The second component of the result pair happens when we look up
415 -- in an InstEnv that has entries for
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
423 lookupInstEnv (pkg_ie, home_ie) cls tys
424 = (pruned_matches, all_unifs)
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
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
451 lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
452 -- See Note [InstTypes: instantiating types]
453 lookup_tv subst tv = case lookupTyVar subst tv of
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
465 | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
467 (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
469 ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant
470 find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
472 -- Does not match, so next check whether the things unify
473 -- See Note [overlapping instances] above
474 | Incoherent <- oflag
478 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
479 (ppr cls <+> ppr tys <+> ppr all_tvs) $$
480 (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
482 -- Unification will break badly if the variables overlap
483 -- They shouldn't because we allocate separate uniques for them
484 case tcUnifyTys instanceBindFun tpl_tys tys of
485 Just _ -> find ms (item:us) rest
486 Nothing -> find ms us rest
490 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
491 -- Add a new solution, knocking out strictly less specific ones
492 insert_overlapping new_item [] = [new_item]
493 insert_overlapping new_item (item:items)
494 | new_beats_old && old_beats_new = item : insert_overlapping new_item items
495 -- Duplicate => keep both for error report
496 | new_beats_old = insert_overlapping new_item items
498 | old_beats_new = item : items
500 | otherwise = item : insert_overlapping new_item items
503 new_beats_old = new_item `beats` item
504 old_beats_new = item `beats` new_item
506 (instA, _) `beats` (instB, _)
508 isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
509 -- A beats B if A is more specific than B, and B admits overlap
510 -- I.e. if B can be instantiated to match A
512 overlap_ok = case is_flag instB of
518 %************************************************************************
522 %************************************************************************
525 instanceBindFun :: TyVar -> BindFlag
526 instanceBindFun tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
528 -- Note [Binding when looking up instances]
531 Note [Binding when looking up instances]
532 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
533 When looking up in the instance environment, or family-instance environment,
534 we are careful about multiple matches, as described above in
535 Note [Overlapping instances]
537 The key_tys can contain skolem constants, and we can guarantee that those
538 are never going to be instantiated to anything, so we should not involve
539 them in the unification test. Example:
540 class Foo a where { op :: a -> Int }
541 instance Foo a => Foo [a] -- NB overlap
542 instance Foo [Int] -- NB overlap
543 data T = forall a. Foo a => MkT a
546 The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
547 complain, saying that the choice of instance depended on the instantiation
548 of 'a'; but of course it isn't *going* to be instantiated.
550 We do this only for pattern-bound skolems. For example we reject
551 g :: forall a => [a] -> Int
553 on the grounds that the correct instance depends on the instantiation of 'a'