2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[InstEnv]{Utilities for typechecking instance declarations}
6 The bits common to TcInstDcls and TcDeriv.
12 emptyInstEnv, extendInstEnv, extendInstEnvList,
13 lookupInstEnv, instEnvElts,
14 classInstances, simpleDFunClassTyCon, checkFunDeps
17 #include "HsVersions.h"
19 import Class ( Class, classTvsFds )
22 import Type ( TvSubstEnv )
23 import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy,
24 tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar
26 import Unify ( tcMatchTys, tcUnifyTys )
27 import FunDeps ( checkClsFD )
28 import TyCon ( TyCon )
30 import UniqFM ( UniqFM, lookupUFM, emptyUFM, addToUFM_C, eltsUFM )
33 import Util ( notNull )
34 import Maybe ( isJust )
38 %************************************************************************
40 \subsection{The key types}
42 %************************************************************************
46 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
49 = ClsIE [InstEnvElt] -- The instances for a particular class, in any order
50 Bool -- True <=> there is an instance of form C a b c
51 -- If *not* then the common case of looking up
52 -- (C a b c) can fail immediately
53 -- NB: use tcIsTyVarTy: don't look through newtypes!!
55 type InstEnvElt = (TyVarSet, [Type], DFunId)
56 -- INVARIANTs: see notes below
58 emptyInstEnv :: InstEnv
59 emptyInstEnv = emptyUFM
61 instEnvElts :: InstEnv -> [InstEnvElt]
62 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
64 classInstances :: (InstEnv,InstEnv) -> Class -> [InstEnvElt]
65 classInstances (pkg_ie, home_ie) cls
66 = get home_ie ++ get pkg_ie
68 get env = case lookupUFM env cls of
69 Just (ClsIE insts _) -> insts
72 extendInstEnvList :: InstEnv -> [DFunId] -> InstEnv
73 extendInstEnvList inst_env dfuns = foldl extendInstEnv inst_env dfuns
75 extendInstEnv :: InstEnv -> DFunId -> InstEnv
76 extendInstEnv inst_env dfun_id
77 = addToUFM_C add inst_env clas (ClsIE [ins_item] ins_tyvar)
79 add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
80 (ins_tyvar || cur_tyvar)
81 (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
82 ins_tv_set = mkVarSet ins_tvs
83 ins_item = (ins_tv_set, ins_tys, dfun_id)
84 ins_tyvar = all tcIsTyVarTy ins_tys
87 pprInstEnv :: InstEnv -> SDoc
89 = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
90 brackets (pprWithCommas ppr tys) <+> ppr dfun
91 | ClsIE cls_inst_env _ <- eltsUFM env
92 , (tyvars, tys, dfun) <- cls_inst_env
96 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
97 simpleDFunClassTyCon dfun
100 (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
101 tycon = tcTyConAppTyCon ty
104 %************************************************************************
106 \subsection{Instance environments: InstEnv and ClsInstEnv}
108 %************************************************************************
110 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
111 ClsInstEnv mapping is the dfun for that instance.
113 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
115 forall a b, C t1 t2 t3 can be constructed by dfun
117 or, to put it another way, we have
119 instance (...) => C t1 t2 t3, witnessed by dfun
121 There is an important consistency constraint in the elements of a ClsInstEnv:
123 * [a,b] must be a superset of the free vars of [t1,t2,t3]
125 * The dfun must itself be quantified over [a,b]
127 * More specific instances come before less specific ones,
130 Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
131 [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
132 The "a" in the pattern must be one of the forall'd variables in
137 Notes on overlapping instances
138 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
139 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
141 In others, overlap is permitted, but only in such a way that one can make
142 a unique choice when looking up. That is, overlap is only permitted if
143 one template matches the other, or vice versa. So this is ok:
151 If overlap is permitted, the list is kept most specific first, so that
152 the first lookup is the right choice.
155 For now we just use association lists.
157 \subsection{Avoiding a problem with overlapping}
159 Consider this little program:
162 class C a where c :: a
163 class C a => D a where d :: a
165 instance C Int where c = 17
166 instance D Int where d = 13
168 instance C a => C [a] where c = [c]
169 instance ({- C [a], -} D a) => D [a] where d = c
171 instance C [Int] where c = [37]
173 main = print (d :: [Int])
176 What do you think `main' prints (assuming we have overlapping instances, and
177 all that turned on)? Well, the instance for `D' at type `[a]' is defined to
178 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
179 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
180 the `C [Int]' instance is more specific).
182 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong. That
183 was easy ;-) Let's just consult hugs for good measure. Wait - if I use old
184 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
185 doesn't even compile! What's going on!?
187 What hugs complains about is the `D [a]' instance decl.
190 ERROR "mj.hs" (line 10): Cannot build superclass instance
192 *** Context supplied : D a
193 *** Required superclass : C [a]
196 You might wonder what hugs is complaining about. It's saying that you
197 need to add `C [a]' to the context of the `D [a]' instance (as appears
198 in comments). But there's that `C [a]' instance decl one line above
199 that says that I can reduce the need for a `C [a]' instance to the
200 need for a `C a' instance, and in this case, I already have the
201 necessary `C a' instance (since we have `D a' explicitly in the
202 context, and `C' is a superclass of `D').
204 Unfortunately, the above reasoning indicates a premature commitment to the
205 generic `C [a]' instance. I.e., it prematurely rules out the more specific
206 instance `C [Int]'. This is the mistake that ghc-4.06 makes. The fix is to
207 add the context that hugs suggests (uncomment the `C [a]'), effectively
208 deferring the decision about which instance to use.
210 Now, interestingly enough, 4.04 has this same bug, but it's covered up
211 in this case by a little known `optimization' that was disabled in
212 4.06. Ghc-4.04 silently inserts any missing superclass context into
213 an instance declaration. In this case, it silently inserts the `C
214 [a]', and everything happens to work out.
216 (See `basicTypes/MkId:mkDictFunId' for the code in question. Search for
217 `Mark Jones', although Mark claims no credit for the `optimization' in
218 question, and would rather it stopped being called the `Mark Jones
221 So, what's the fix? I think hugs has it right. Here's why. Let's try
222 something else out with ghc-4.04. Let's add the following line:
227 Everyone raise their hand who thinks that `d :: [Int]' should give a
228 different answer from `d' :: [Int]'. Well, in ghc-4.04, it does. The
229 `optimization' only applies to instance decls, not to regular
230 bindings, giving inconsistent behavior.
232 Old hugs had this same bug. Here's how we fixed it: like GHC, the
233 list of instances for a given class is ordered, so that more specific
234 instances come before more generic ones. For example, the instance
235 list for C might contain:
236 ..., C Int, ..., C a, ...
237 When we go to look for a `C Int' instance we'll get that one first.
238 But what if we go looking for a `C b' (`b' is unconstrained)? We'll
239 pass the `C Int' instance, and keep going. But if `b' is
240 unconstrained, then we don't know yet if the more specific instance
241 will eventually apply. GHC keeps going, and matches on the generic `C
242 a'. The fix is to, at each step, check to see if there's a reverse
243 match, and if so, abort the search. This prevents hugs from
244 prematurely chosing a generic instance when a more specific one
249 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
250 this test. Suppose the instance envt had
251 ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
252 (still most specific first)
253 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
254 C x y Int doesn't match the template {a,b} C a a b
256 C a a b match the template {x,y} C x y Int
257 But still x and y might subsequently be unified so they *do* match.
259 Simple story: unify, don't match.
262 %************************************************************************
264 \subsection{Looking up an instance}
266 %************************************************************************
268 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
269 the env is kept ordered, the first match must be the only one. The
270 thing we are looking up can have an arbitrary "flexi" part.
273 lookupInstEnv :: DynFlags
274 -> (InstEnv -- External package inst-env
275 ,InstEnv) -- Home-package inst-env
276 -> Class -> [Type] -- What we are looking for
277 -> ([(TvSubstEnv, InstEnvElt)], -- Successful matches
278 [Id]) -- These don't match but do unify
279 -- The second component of the tuple happens when we look up
281 -- in an InstEnv that has entries for
284 -- Then which we choose would depend on the way in which 'a'
285 -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
286 -- but Foo [Int] is a unifier. This gives the caller a better chance of
287 -- giving a suitable error messagen
289 lookupInstEnv dflags (pkg_ie, home_ie) cls tys
290 | not (null all_unifs) = (all_matches, all_unifs) -- This is always an error situation,
291 -- so don't attempt to pune the matches
292 | otherwise = (pruned_matches, [])
294 all_tvs = all tcIsTyVarTy tys
295 incoherent_ok = dopt Opt_AllowIncoherentInstances dflags
296 overlap_ok = dopt Opt_AllowOverlappingInstances dflags
297 (home_matches, home_unifs) = lookup_inst_env home_ie cls tys all_tvs
298 (pkg_matches, pkg_unifs) = lookup_inst_env pkg_ie cls tys all_tvs
299 all_matches = home_matches ++ pkg_matches
300 all_unifs | incoherent_ok = [] -- Don't worry about these if incoherent is ok!
301 | otherwise = home_unifs ++ pkg_unifs
303 pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
304 | otherwise = all_matches
306 lookup_inst_env :: InstEnv -- The envt
307 -> Class -> [Type] -- What we are looking for
308 -> Bool -- All the [Type] are tyvars
309 -> ([(TvSubstEnv, InstEnvElt)], -- Successful matches
310 [Id]) -- These don't match but do unify
311 lookup_inst_env env key_cls key_tys key_all_tvs
312 = case lookupUFM env key_cls of
313 Nothing -> ([],[]) -- No instances for this class
314 Just (ClsIE insts has_tv_insts)
315 | key_all_tvs && not has_tv_insts -> ([],[]) -- Short cut for common case
316 -- The thing we are looking up is of form (C a b c), and
317 -- the ClsIE has no instances of that form, so don't bother to search
318 | otherwise -> find insts [] []
320 key_vars = filterVarSet not_existential (tyVarsOfTypes key_tys)
321 not_existential tv = not (isExistentialTyVar tv)
322 -- The key_tys can contain skolem constants, and we can guarantee that those
323 -- are never going to be instantiated to anything, so we should not involve
324 -- them in the unification test. Example:
325 -- class Foo a where { op :: a -> Int }
326 -- instance Foo a => Foo [a] -- NB overlap
327 -- instance Foo [Int] -- NB overlap
328 -- data T = forall a. Foo a => MkT a
330 -- f (MkT x) = op [x,x]
331 -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
332 -- complain, saying that the choice of instance depended on the instantiation
333 -- of 'a'; but of course it isn't *going* to be instantiated.
335 -- We do this only for pattern-bound skolems. For example we reject
336 -- g :: forall a => [a] -> Int
338 -- on the grounds that the correct instance depends on the instantiation of 'a'
340 find [] ms us = (ms, us)
341 find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
342 = case tcMatchTys tpl_tyvars tpl key_tys of
343 Just subst -> find rest ((subst,item):ms) us
345 -- Does not match, so next check whether the things unify
346 -- [see notes about overlapping instances above]
347 -> ASSERT2( not (key_vars `intersectsVarSet` tpl_tyvars),
348 (ppr key_cls <+> ppr key_tys <+> ppr key_all_tvs) $$
349 (ppr dfun_id <+> ppr tpl_tyvars <+> ppr tpl)
351 -- Unification will break badly if the variables overlap
352 -- They shouldn't because we allocate separate uniques for them
353 case tcUnifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
354 Just _ -> find rest ms (dfun_id:us)
355 Nothing -> find rest ms us
357 insert_overlapping :: (TvSubstEnv, InstEnvElt) -> [(TvSubstEnv, InstEnvElt)]
358 -> [(TvSubstEnv, InstEnvElt)]
359 -- Add a new solution, knocking out strictly less specific ones
360 insert_overlapping new_item [] = [new_item]
361 insert_overlapping new_item (item:items)
362 | new_beats_old && old_beats_new = item : insert_overlapping new_item items
363 -- Duplicate => keep both for error report
364 | new_beats_old = insert_overlapping new_item items
366 | old_beats_new = item : items
368 | otherwise = item : insert_overlapping new_item items
371 new_beats_old = new_item `beats` item
372 old_beats_new = item `beats` new_item
374 (_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _))
375 = isJust (tcMatchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B
376 -- I.e. if B can be instantiated to match A
380 %************************************************************************
382 Functional dependencies
384 %************************************************************************
386 Here is the bad case:
387 class C a b | a->b where ...
388 instance C Int Bool where ...
389 instance C Int Char where ...
391 The point is that a->b, so Int in the first parameter must uniquely
392 determine the second. In general, given the same class decl, and given
394 instance C s1 s2 where ...
395 instance C t1 t2 where ...
397 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
399 Matters are a little more complicated if there are free variables in
402 class D a b c | a -> b
403 instance D a b => D [(a,a)] [b] Int
404 instance D a b => D [a] [b] Bool
406 The instance decls don't overlap, because the third parameter keeps
407 them separate. But we want to make sure that given any constraint
413 checkFunDeps :: (InstEnv, InstEnv) -> DFunId
414 -> Maybe [DFunId] -- Nothing <=> ok
415 -- Just dfs <=> conflict with dfs
416 -- Check wheher adding DFunId would break functional-dependency constraints
417 checkFunDeps inst_envs dfun
418 | null bad_fundeps = Nothing
419 | otherwise = Just bad_fundeps
421 (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun)
422 ins_tv_set = mkVarSet ins_tvs
423 cls_inst_env = classInstances inst_envs clas
424 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
426 badFunDeps :: [InstEnvElt] -> Class
427 -> TyVarSet -> [Type] -- Proposed new instance type
429 badFunDeps cls_inst_env clas ins_tv_set ins_tys
430 = [ dfun_id | fd <- fds,
431 (tvs, tys, dfun_id) <- cls_inst_env,
432 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys)
435 (clas_tvs, fds) = classTvsFds clas