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 ( TvSubst )
23 import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy,
24 tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar
26 import Unify ( tcMatchTys, tcUnifyTys, BindFlag(..) )
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 %************************************************************************
44 A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
45 ClsInstEnv mapping is the dfun for that instance.
47 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
49 forall a b, C t1 t2 t3 can be constructed by dfun
51 or, to put it another way, we have
53 instance (...) => C t1 t2 t3, witnessed by dfun
57 type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
60 = ClsIE [InstEnvElt] -- The instances for a particular class, in any order
61 Bool -- True <=> there is an instance of form C a b c
62 -- If *not* then the common case of looking up
63 -- (C a b c) can fail immediately
64 -- NB: use tcIsTyVarTy: don't look through newtypes!!
66 type InstEnvElt = (TyVarSet, [Type], DFunId)
69 -- * [a,b] must be a superset of the free vars of [t1,t2,t3]
71 -- * The dfun must itself be quantified over [a,b]
73 -- * The template type variables [a,b] are distinct in each item
74 -- of a ClsInstEnv (so we can safely unify them)
76 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
77 -- [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
78 -- The "a" in the pattern must be one of the forall'd variables in
82 emptyInstEnv :: InstEnv
83 emptyInstEnv = emptyUFM
85 instEnvElts :: InstEnv -> [InstEnvElt]
86 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
88 classInstances :: (InstEnv,InstEnv) -> Class -> [InstEnvElt]
89 classInstances (pkg_ie, home_ie) cls
90 = get home_ie ++ get pkg_ie
92 get env = case lookupUFM env cls of
93 Just (ClsIE insts _) -> insts
96 extendInstEnvList :: InstEnv -> [DFunId] -> InstEnv
97 extendInstEnvList inst_env dfuns = foldl extendInstEnv inst_env dfuns
99 extendInstEnv :: InstEnv -> DFunId -> InstEnv
100 extendInstEnv inst_env dfun_id
101 = addToUFM_C add inst_env clas (ClsIE [ins_item] ins_tyvar)
103 add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
104 (ins_tyvar || cur_tyvar)
105 (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
106 ins_tv_set = mkVarSet ins_tvs
107 ins_item = (ins_tv_set, ins_tys, dfun_id)
108 ins_tyvar = all tcIsTyVarTy ins_tys
111 pprInstEnv :: InstEnv -> SDoc
113 = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
114 brackets (pprWithCommas ppr tys) <+> ppr dfun
115 | ClsIE cls_inst_env _ <- eltsUFM env
116 , (tyvars, tys, dfun) <- cls_inst_env
120 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
121 simpleDFunClassTyCon dfun
124 (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
125 tycon = tcTyConAppTyCon ty
128 %************************************************************************
130 \subsection{Instance environments: InstEnv and ClsInstEnv}
132 %************************************************************************
135 Notes on overlapping instances
136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
137 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
139 In others, overlap is permitted, but only in such a way that one can make
140 a unique choice when looking up. That is, overlap is only permitted if
141 one template matches the other, or vice versa. So this is ok:
149 If overlap is permitted, the list is kept most specific first, so that
150 the first lookup is the right choice.
153 For now we just use association lists.
155 \subsection{Avoiding a problem with overlapping}
157 Consider this little program:
160 class C a where c :: a
161 class C a => D a where d :: a
163 instance C Int where c = 17
164 instance D Int where d = 13
166 instance C a => C [a] where c = [c]
167 instance ({- C [a], -} D a) => D [a] where d = c
169 instance C [Int] where c = [37]
171 main = print (d :: [Int])
174 What do you think `main' prints (assuming we have overlapping instances, and
175 all that turned on)? Well, the instance for `D' at type `[a]' is defined to
176 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
177 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
178 the `C [Int]' instance is more specific).
180 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong. That
181 was easy ;-) Let's just consult hugs for good measure. Wait - if I use old
182 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
183 doesn't even compile! What's going on!?
185 What hugs complains about is the `D [a]' instance decl.
188 ERROR "mj.hs" (line 10): Cannot build superclass instance
190 *** Context supplied : D a
191 *** Required superclass : C [a]
194 You might wonder what hugs is complaining about. It's saying that you
195 need to add `C [a]' to the context of the `D [a]' instance (as appears
196 in comments). But there's that `C [a]' instance decl one line above
197 that says that I can reduce the need for a `C [a]' instance to the
198 need for a `C a' instance, and in this case, I already have the
199 necessary `C a' instance (since we have `D a' explicitly in the
200 context, and `C' is a superclass of `D').
202 Unfortunately, the above reasoning indicates a premature commitment to the
203 generic `C [a]' instance. I.e., it prematurely rules out the more specific
204 instance `C [Int]'. This is the mistake that ghc-4.06 makes. The fix is to
205 add the context that hugs suggests (uncomment the `C [a]'), effectively
206 deferring the decision about which instance to use.
208 Now, interestingly enough, 4.04 has this same bug, but it's covered up
209 in this case by a little known `optimization' that was disabled in
210 4.06. Ghc-4.04 silently inserts any missing superclass context into
211 an instance declaration. In this case, it silently inserts the `C
212 [a]', and everything happens to work out.
214 (See `basicTypes/MkId:mkDictFunId' for the code in question. Search for
215 `Mark Jones', although Mark claims no credit for the `optimization' in
216 question, and would rather it stopped being called the `Mark Jones
219 So, what's the fix? I think hugs has it right. Here's why. Let's try
220 something else out with ghc-4.04. Let's add the following line:
225 Everyone raise their hand who thinks that `d :: [Int]' should give a
226 different answer from `d' :: [Int]'. Well, in ghc-4.04, it does. The
227 `optimization' only applies to instance decls, not to regular
228 bindings, giving inconsistent behavior.
230 Old hugs had this same bug. Here's how we fixed it: like GHC, the
231 list of instances for a given class is ordered, so that more specific
232 instances come before more generic ones. For example, the instance
233 list for C might contain:
234 ..., C Int, ..., C a, ...
235 When we go to look for a `C Int' instance we'll get that one first.
236 But what if we go looking for a `C b' (`b' is unconstrained)? We'll
237 pass the `C Int' instance, and keep going. But if `b' is
238 unconstrained, then we don't know yet if the more specific instance
239 will eventually apply. GHC keeps going, and matches on the generic `C
240 a'. The fix is to, at each step, check to see if there's a reverse
241 match, and if so, abort the search. This prevents hugs from
242 prematurely chosing a generic instance when a more specific one
247 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
248 this test. Suppose the instance envt had
249 ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
250 (still most specific first)
251 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
252 C x y Int doesn't match the template {a,b} C a a b
254 C a a b match the template {x,y} C x y Int
255 But still x and y might subsequently be unified so they *do* match.
257 Simple story: unify, don't match.
260 %************************************************************************
262 \subsection{Looking up an instance}
264 %************************************************************************
266 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
267 the env is kept ordered, the first match must be the only one. The
268 thing we are looking up can have an arbitrary "flexi" part.
271 lookupInstEnv :: DynFlags
272 -> (InstEnv -- External package inst-env
273 ,InstEnv) -- Home-package inst-env
274 -> Class -> [Type] -- What we are looking for
275 -> ([(TvSubst, InstEnvElt)], -- Successful matches
276 [Id]) -- These don't match but do unify
277 -- The second component of the tuple happens when we look up
279 -- in an InstEnv that has entries for
282 -- Then which we choose would depend on the way in which 'a'
283 -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
284 -- but Foo [Int] is a unifier. This gives the caller a better chance of
285 -- giving a suitable error messagen
287 lookupInstEnv dflags (pkg_ie, home_ie) cls tys
288 | not (null all_unifs) = (all_matches, all_unifs) -- This is always an error situation,
289 -- so don't attempt to pune the matches
290 | otherwise = (pruned_matches, [])
292 all_tvs = all tcIsTyVarTy tys
293 incoherent_ok = dopt Opt_AllowIncoherentInstances dflags
294 overlap_ok = dopt Opt_AllowOverlappingInstances dflags
295 (home_matches, home_unifs) = lookup_inst_env home_ie cls tys all_tvs
296 (pkg_matches, pkg_unifs) = lookup_inst_env pkg_ie cls tys all_tvs
297 all_matches = home_matches ++ pkg_matches
298 all_unifs | incoherent_ok = [] -- Don't worry about these if incoherent is ok!
299 | otherwise = home_unifs ++ pkg_unifs
301 pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
302 | otherwise = all_matches
304 lookup_inst_env :: InstEnv -- The envt
305 -> Class -> [Type] -- What we are looking for
306 -> Bool -- All the [Type] are tyvars
307 -> ([(TvSubst, InstEnvElt)], -- Successful matches
308 [Id]) -- These don't match but do unify
309 lookup_inst_env env key_cls key_tys key_all_tvs
310 = case lookupUFM env key_cls of
311 Nothing -> ([],[]) -- No instances for this class
312 Just (ClsIE insts has_tv_insts)
313 | key_all_tvs && not has_tv_insts -> ([],[]) -- Short cut for common case
314 -- The thing we are looking up is of form (C a b c), and
315 -- the ClsIE has no instances of that form, so don't bother to search
316 | otherwise -> find insts [] []
318 find [] ms us = (ms, us)
319 find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
320 = case tcMatchTys tpl_tyvars tpl key_tys of
321 Just subst -> find rest ((subst,item):ms) us
323 -- Does not match, so next check whether the things unify
324 -- [see notes about overlapping instances above]
325 -> ASSERT2( not (tyVarsOfTypes key_tys `intersectsVarSet` tpl_tyvars),
326 (ppr key_cls <+> ppr key_tys <+> ppr key_all_tvs) $$
327 (ppr dfun_id <+> ppr tpl_tyvars <+> ppr tpl)
329 -- Unification will break badly if the variables overlap
330 -- They shouldn't because we allocate separate uniques for them
331 case tcUnifyTys bind_fn tpl key_tys of
332 Just _ -> find rest ms (dfun_id:us)
333 Nothing -> find rest ms us
335 bind_fn tv | isExistentialTyVar tv = Skolem
337 -- The key_tys can contain skolem constants, and we can guarantee that those
338 -- are never going to be instantiated to anything, so we should not involve
339 -- them in the unification test. Example:
340 -- class Foo a where { op :: a -> Int }
341 -- instance Foo a => Foo [a] -- NB overlap
342 -- instance Foo [Int] -- NB overlap
343 -- data T = forall a. Foo a => MkT a
345 -- f (MkT x) = op [x,x]
346 -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
347 -- complain, saying that the choice of instance depended on the instantiation
348 -- of 'a'; but of course it isn't *going* to be instantiated.
350 -- We do this only for pattern-bound skolems. For example we reject
351 -- g :: forall a => [a] -> Int
353 -- on the grounds that the correct instance depends on the instantiation of 'a'
355 insert_overlapping :: (TvSubst, InstEnvElt) -> [(TvSubst, InstEnvElt)]
356 -> [(TvSubst, InstEnvElt)]
357 -- Add a new solution, knocking out strictly less specific ones
358 insert_overlapping new_item [] = [new_item]
359 insert_overlapping new_item (item:items)
360 | new_beats_old && old_beats_new = item : insert_overlapping new_item items
361 -- Duplicate => keep both for error report
362 | new_beats_old = insert_overlapping new_item items
364 | old_beats_new = item : items
366 | otherwise = item : insert_overlapping new_item items
369 new_beats_old = new_item `beats` item
370 old_beats_new = item `beats` new_item
372 (_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _))
373 = isJust (tcMatchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B
374 -- I.e. if B can be instantiated to match A
378 %************************************************************************
380 Functional dependencies
382 %************************************************************************
384 Here is the bad case:
385 class C a b | a->b where ...
386 instance C Int Bool where ...
387 instance C Int Char where ...
389 The point is that a->b, so Int in the first parameter must uniquely
390 determine the second. In general, given the same class decl, and given
392 instance C s1 s2 where ...
393 instance C t1 t2 where ...
395 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
397 Matters are a little more complicated if there are free variables in
400 class D a b c | a -> b
401 instance D a b => D [(a,a)] [b] Int
402 instance D a b => D [a] [b] Bool
404 The instance decls don't overlap, because the third parameter keeps
405 them separate. But we want to make sure that given any constraint
411 checkFunDeps :: (InstEnv, InstEnv) -> DFunId
412 -> Maybe [DFunId] -- Nothing <=> ok
413 -- Just dfs <=> conflict with dfs
414 -- Check wheher adding DFunId would break functional-dependency constraints
415 checkFunDeps inst_envs dfun
416 | null bad_fundeps = Nothing
417 | otherwise = Just bad_fundeps
419 (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun)
420 ins_tv_set = mkVarSet ins_tvs
421 cls_inst_env = classInstances inst_envs clas
422 bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
424 badFunDeps :: [InstEnvElt] -> Class
425 -> TyVarSet -> [Type] -- Proposed new instance type
427 badFunDeps cls_inst_env clas ins_tv_set ins_tys
428 = [ dfun_id | fd <- fds,
429 (tvs, tys, dfun_id) <- cls_inst_env,
430 notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys)
433 (clas_tvs, fds) = classTvsFds clas