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,
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 ( matchTys, unifyTys )
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 extendInstEnv :: InstEnv -> DFunId -> InstEnv
73 extendInstEnv inst_env dfun_id
74 = addToUFM_C add inst_env clas (ClsIE [ins_item] ins_tyvar)
76 add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
77 (ins_tyvar || cur_tyvar)
78 (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
79 ins_tv_set = mkVarSet ins_tvs
80 ins_item = (ins_tv_set, ins_tys, dfun_id)
81 ins_tyvar = all tcIsTyVarTy ins_tys
84 pprInstEnv :: InstEnv -> SDoc
86 = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
87 brackets (pprWithCommas ppr tys) <+> ppr dfun
88 | ClsIE cls_inst_env _ <- eltsUFM env
89 , (tyvars, tys, dfun) <- cls_inst_env
93 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
94 simpleDFunClassTyCon dfun
97 (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
98 tycon = tcTyConAppTyCon ty
101 %************************************************************************
103 \subsection{Instance environments: InstEnv and ClsInstEnv}
105 %************************************************************************
107 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
108 ClsInstEnv mapping is the dfun for that instance.
110 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
112 forall a b, C t1 t2 t3 can be constructed by dfun
114 or, to put it another way, we have
116 instance (...) => C t1 t2 t3, witnessed by dfun
118 There is an important consistency constraint in the elements of a ClsInstEnv:
120 * [a,b] must be a superset of the free vars of [t1,t2,t3]
122 * The dfun must itself be quantified over [a,b]
124 * More specific instances come before less specific ones,
127 Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
128 [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
129 The "a" in the pattern must be one of the forall'd variables in
134 Notes on overlapping instances
135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
136 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
138 In others, overlap is permitted, but only in such a way that one can make
139 a unique choice when looking up. That is, overlap is only permitted if
140 one template matches the other, or vice versa. So this is ok:
148 If overlap is permitted, the list is kept most specific first, so that
149 the first lookup is the right choice.
152 For now we just use association lists.
154 \subsection{Avoiding a problem with overlapping}
156 Consider this little program:
159 class C a where c :: a
160 class C a => D a where d :: a
162 instance C Int where c = 17
163 instance D Int where d = 13
165 instance C a => C [a] where c = [c]
166 instance ({- C [a], -} D a) => D [a] where d = c
168 instance C [Int] where c = [37]
170 main = print (d :: [Int])
173 What do you think `main' prints (assuming we have overlapping instances, and
174 all that turned on)? Well, the instance for `D' at type `[a]' is defined to
175 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
176 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
177 the `C [Int]' instance is more specific).
179 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong. That
180 was easy ;-) Let's just consult hugs for good measure. Wait - if I use old
181 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
182 doesn't even compile! What's going on!?
184 What hugs complains about is the `D [a]' instance decl.
187 ERROR "mj.hs" (line 10): Cannot build superclass instance
189 *** Context supplied : D a
190 *** Required superclass : C [a]
193 You might wonder what hugs is complaining about. It's saying that you
194 need to add `C [a]' to the context of the `D [a]' instance (as appears
195 in comments). But there's that `C [a]' instance decl one line above
196 that says that I can reduce the need for a `C [a]' instance to the
197 need for a `C a' instance, and in this case, I already have the
198 necessary `C a' instance (since we have `D a' explicitly in the
199 context, and `C' is a superclass of `D').
201 Unfortunately, the above reasoning indicates a premature commitment to the
202 generic `C [a]' instance. I.e., it prematurely rules out the more specific
203 instance `C [Int]'. This is the mistake that ghc-4.06 makes. The fix is to
204 add the context that hugs suggests (uncomment the `C [a]'), effectively
205 deferring the decision about which instance to use.
207 Now, interestingly enough, 4.04 has this same bug, but it's covered up
208 in this case by a little known `optimization' that was disabled in
209 4.06. Ghc-4.04 silently inserts any missing superclass context into
210 an instance declaration. In this case, it silently inserts the `C
211 [a]', and everything happens to work out.
213 (See `basicTypes/MkId:mkDictFunId' for the code in question. Search for
214 `Mark Jones', although Mark claims no credit for the `optimization' in
215 question, and would rather it stopped being called the `Mark Jones
218 So, what's the fix? I think hugs has it right. Here's why. Let's try
219 something else out with ghc-4.04. Let's add the following line:
224 Everyone raise their hand who thinks that `d :: [Int]' should give a
225 different answer from `d' :: [Int]'. Well, in ghc-4.04, it does. The
226 `optimization' only applies to instance decls, not to regular
227 bindings, giving inconsistent behavior.
229 Old hugs had this same bug. Here's how we fixed it: like GHC, the
230 list of instances for a given class is ordered, so that more specific
231 instances come before more generic ones. For example, the instance
232 list for C might contain:
233 ..., C Int, ..., C a, ...
234 When we go to look for a `C Int' instance we'll get that one first.
235 But what if we go looking for a `C b' (`b' is unconstrained)? We'll
236 pass the `C Int' instance, and keep going. But if `b' is
237 unconstrained, then we don't know yet if the more specific instance
238 will eventually apply. GHC keeps going, and matches on the generic `C
239 a'. The fix is to, at each step, check to see if there's a reverse
240 match, and if so, abort the search. This prevents hugs from
241 prematurely chosing a generic instance when a more specific one
246 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
247 this test. Suppose the instance envt had
248 ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
249 (still most specific first)
250 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
251 C x y Int doesn't match the template {a,b} C a a b
253 C a a b match the template {x,y} C x y Int
254 But still x and y might subsequently be unified so they *do* match.
256 Simple story: unify, don't match.
259 %************************************************************************
261 \subsection{Looking up an instance}
263 %************************************************************************
265 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
266 the env is kept ordered, the first match must be the only one. The
267 thing we are looking up can have an arbitrary "flexi" part.
270 lookupInstEnv :: DynFlags
271 -> (InstEnv -- External package inst-env
272 ,InstEnv) -- Home-package inst-env
273 -> Class -> [Type] -- What we are looking for
274 -> ([(TvSubstEnv, InstEnvElt)], -- Successful matches
275 [Id]) -- These don't match but do unify
276 -- The second component of the tuple happens when we look up
278 -- in an InstEnv that has entries for
281 -- Then which we choose would depend on the way in which 'a'
282 -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
283 -- but Foo [Int] is a unifier. This gives the caller a better chance of
284 -- giving a suitable error messagen
286 lookupInstEnv dflags (pkg_ie, home_ie) cls tys
287 | not (null all_unifs) = (all_matches, all_unifs) -- This is always an error situation,
288 -- so don't attempt to pune the matches
289 | otherwise = (pruned_matches, [])
291 all_tvs = all tcIsTyVarTy tys
292 incoherent_ok = dopt Opt_AllowIncoherentInstances dflags
293 overlap_ok = dopt Opt_AllowOverlappingInstances dflags
294 (home_matches, home_unifs) = lookup_inst_env home_ie cls tys all_tvs
295 (pkg_matches, pkg_unifs) = lookup_inst_env pkg_ie cls tys all_tvs
296 all_matches = home_matches ++ pkg_matches
297 all_unifs | incoherent_ok = [] -- Don't worry about these if incoherent is ok!
298 | otherwise = home_unifs ++ pkg_unifs
300 pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
301 | otherwise = all_matches
303 lookup_inst_env :: InstEnv -- The envt
304 -> Class -> [Type] -- What we are looking for
305 -> Bool -- All the [Type] are tyvars
306 -> ([(TvSubstEnv, InstEnvElt)], -- Successful matches
307 [Id]) -- These don't match but do unify
308 lookup_inst_env env key_cls key_tys key_all_tvs
309 = case lookupUFM env key_cls of
310 Nothing -> ([],[]) -- No instances for this class
311 Just (ClsIE insts has_tv_insts)
312 | key_all_tvs && not has_tv_insts -> ([],[]) -- Short cut for common case
313 -- The thing we are looking up is of form (C a b c), and
314 -- the ClsIE has no instances of that form, so don't bother to search
315 | otherwise -> find insts [] []
317 key_vars = filterVarSet not_existential (tyVarsOfTypes key_tys)
318 not_existential tv = not (isExistentialTyVar tv)
319 -- The key_tys can contain skolem constants, and we can guarantee that those
320 -- are never going to be instantiated to anything, so we should not involve
321 -- them in the unification test. Example:
322 -- class Foo a where { op :: a -> Int }
323 -- instance Foo a => Foo [a] -- NB overlap
324 -- instance Foo [Int] -- NB overlap
325 -- data T = forall a. Foo a => MkT a
327 -- f (MkT x) = op [x,x]
328 -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
329 -- complain, saying that the choice of instance depended on the instantiation
330 -- of 'a'; but of course it isn't *going* to be instantiated.
332 -- We do this only for pattern-bound skolems. For example we reject
333 -- g :: forall a => [a] -> Int
335 -- on the grounds that the correct instance depends on the instantiation of 'a'
337 find [] ms us = (ms, us)
338 find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
339 = case matchTys tpl_tyvars tpl key_tys of
340 Just subst -> find rest ((subst,item):ms) us
342 -- Does not match, so next check whether the things unify
343 -- [see notes about overlapping instances above]
344 -> ASSERT2( not (key_vars `intersectsVarSet` tpl_tyvars),
345 (ppr key_cls <+> ppr key_tys <+> ppr key_all_tvs) $$
346 (ppr dfun_id <+> ppr tpl_tyvars <+> ppr tpl)
348 -- Unification will break badly if the variables overlap
349 -- They shouldn't because we allocate separate uniques for them
350 case unifyTys (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
351 Just _ -> find rest ms (dfun_id:us)
352 Nothing -> find rest ms us
354 insert_overlapping :: (TvSubstEnv, InstEnvElt) -> [(TvSubstEnv, InstEnvElt)]
355 -> [(TvSubstEnv, InstEnvElt)]
356 -- Add a new solution, knocking out strictly less specific ones
357 insert_overlapping new_item [] = [new_item]
358 insert_overlapping new_item (item:items)
359 | new_beats_old && old_beats_new = item : insert_overlapping new_item items
360 -- Duplicate => keep both for error report
361 | new_beats_old = insert_overlapping new_item items
363 | old_beats_new = item : items
365 | otherwise = item : insert_overlapping new_item items
368 new_beats_old = new_item `beats` item
369 old_beats_new = item `beats` new_item
371 (_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _))
372 = isJust (matchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B
373 -- I.e. if B can be instantiated to match A
377 %************************************************************************
379 Functional dependencies
381 %************************************************************************
383 Here is the bad case:
384 class C a b | a->b where ...
385 instance C Int Bool where ...
386 instance C Int Char where ...
388 The point is that a->b, so Int in the first parameter must uniquely
389 determine the second. In general, given the same class decl, and given
391 instance C s1 s2 where ...
392 instance C t1 t2 where ...
394 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
396 Matters are a little more complicated if there are free variables in
399 class D a b c | a -> b
400 instance D a b => D [(a,a)] [b] Int
401 instance D a b => D [a] [b] Bool
403 The instance decls don't overlap, because the third parameter keeps
404 them separate. But we want to make sure that given any constraint
410 checkFunDeps :: (InstEnv, InstEnv) -> DFunId
411 -> Maybe [DFunId] -- Nothing <=> ok
412 -- Just dfs <=> conflict with dfs
413 -- Check wheher adding DFunId would break functional-dependency constraints
414 checkFunDeps inst_envs dfun
415 | null bad_fundeps = Nothing
416 | otherwise = Just bad_fundeps
418 (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun)
419 ins_tv_set = mkVarSet ins_tvs
420 cls_inst_env = classInstances inst_envs clas
421 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
423 badFunDeps :: [InstEnvElt] -> Class
424 -> TyVarSet -> [Type] -- Proposed new instance type
426 badFunDeps cls_inst_env clas ins_tv_set ins_tys
427 = [ dfun_id | fd <- fds,
428 (tvs, tys, dfun_id) <- cls_inst_env,
429 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys)
432 (clas_tvs, fds) = classTvsFds clas