Fix recursive superclasses (again). Fixes Trac #4809.
[ghc-hetmet.git] / compiler / types / InstEnv.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5 \section[InstEnv]{Utilities for typechecking instance declarations}
6
7 The bits common to TcInstDcls and TcDeriv.
8
9 \begin{code}
10 module InstEnv (
11         DFunId, OverlapFlag(..),
12         Instance(..), pprInstance, pprInstanceHdr, pprInstances, 
13         instanceHead, mkLocalInstance, mkImportedInstance,
14         instanceDFunId, setInstanceDFunId, instanceRoughTcs,
15
16         InstEnv, emptyInstEnv, extendInstEnv, 
17         extendInstEnvList, lookupInstEnv, instEnvElts,
18         classInstances, instanceBindFun,
19         instanceCantMatch, roughMatchTcs
20     ) where
21
22 #include "HsVersions.h"
23
24 import Class
25 import Var
26 import VarSet
27 import Name
28 import TcType
29 import TyCon
30 import Unify
31 import Outputable
32 import BasicTypes
33 import UniqFM
34 import Id
35 import FastString
36
37 import Data.Maybe       ( isJust, isNothing )
38 \end{code}
39
40
41 %************************************************************************
42 %*                                                                      *
43 \subsection{The key types}
44 %*                                                                      *
45 %************************************************************************
46
47 \begin{code}
48 data Instance 
49   = Instance { is_cls  :: Name          -- Class name
50         
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
54
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
60
61              , is_dfun :: DFunId -- See Note [Haddock assumptions]
62              , is_flag :: OverlapFlag   -- See detailed comments with
63                                         -- the decl of BasicTypes.OverlapFlag
64     }
65 \end{code}
66
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.
75
76 In is_tcs, 
77     Nothing  means that this type arg is a type variable
78
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!
85
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
93
94 However, note that:
95  * is_tvs must be a superset of the free vars of is_tys
96
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.)
100
101 Note [Haddock assumptions]
102 ~~~~~~~~~~~~~~~~~~~~~~~~~~
103 For normal user-written instances, Haddock relies on
104
105  * the SrcSpan of
106  * the Name of
107  * the is_dfun of
108  * an Instance
109
110 being equal to
111
112   * the SrcSpan of
113   * the instance head type of
114   * the InstDecl used to construct the Instance.
115
116 \begin{code}
117 instanceDFunId :: Instance -> DFunId
118 instanceDFunId = is_dfun
119
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 }
130    where 
131      (tvs, _, tys) = tcSplitDFunTy (idType dfun)
132
133 instanceRoughTcs :: Instance -> [Maybe Name]
134 instanceRoughTcs = is_tcs
135 \end{code}
136
137 \begin{code}
138 instance NamedThing Instance where
139    getName ispec = getName (is_dfun ispec)
140
141 instance Outputable Instance where
142    ppr = pprInstance
143
144 pprInstance :: Instance -> SDoc
145 -- Prints the Instance as an instance declaration
146 pprInstance ispec
147   = hang (pprInstanceHdr ispec)
148         2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
149
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   = getPprStyle $ \ sty ->
155     let theta_to_print
156           | debugStyle sty = theta
157           | otherwise = drop (dfunNSilent dfun) theta
158     in ptext (sLit "instance") <+> ppr flag
159        <+> sep [pprThetaArrow theta_to_print, ppr res_ty]
160   where
161     dfun = is_dfun ispec
162     (_, theta, res_ty) = tcSplitSigmaTy (idType dfun)
163         -- Print without the for-all, which the programmer doesn't write
164
165 pprInstances :: [Instance] -> SDoc
166 pprInstances ispecs = vcat (map pprInstance ispecs)
167
168 instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
169 instanceHead ispec 
170    = (tvs, theta, cls, tys)
171    where
172      (tvs, theta, tau) = tcSplitSigmaTy (idType (is_dfun ispec))
173      (cls, tys) = tcSplitDFunHead tau
174
175 mkLocalInstance :: DFunId
176                 -> OverlapFlag
177                 -> Instance
178 -- Used for local instances, where we can safely pull on the DFunId
179 mkLocalInstance dfun oflag
180   = Instance {  is_flag = oflag, is_dfun = dfun,
181                 is_tvs = mkVarSet tvs, is_tys = tys,
182                 is_cls = className cls, is_tcs = roughMatchTcs tys }
183   where
184     (tvs, cls, tys) = tcSplitDFunTy (idType dfun)
185
186 mkImportedInstance :: Name -> [Maybe Name]
187                    -> DFunId -> OverlapFlag -> Instance
188 -- Used for imported instances, where we get the rough-match stuff
189 -- from the interface file
190 mkImportedInstance cls mb_tcs dfun oflag
191   = Instance {  is_flag = oflag, is_dfun = dfun,
192                 is_tvs = mkVarSet tvs, is_tys = tys,
193                 is_cls = cls, is_tcs = mb_tcs }
194   where
195     (tvs, _, tys) = tcSplitDFunTy (idType dfun)
196
197 roughMatchTcs :: [Type] -> [Maybe Name]
198 roughMatchTcs tys = map rough tys
199   where
200     rough ty = case tcSplitTyConApp_maybe ty of
201                   Just (tc,_) -> Just (tyConName tc)
202                   Nothing     -> Nothing
203
204 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
205 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
206 -- possibly be instantiated to actual, nor vice versa; 
207 -- False is non-committal
208 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
209 instanceCantMatch _             _             =  False  -- Safe
210 \end{code}
211
212
213 Note [Overlapping instances]
214 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
215 Overlap is permitted, but only in such a way that one can make
216 a unique choice when looking up.  That is, overlap is only permitted if
217 one template matches the other, or vice versa.  So this is ok:
218
219   [a]  [Int]
220
221 but this is not
222
223   (Int,a)  (b,Int)
224
225 If overlap is permitted, the list is kept most specific first, so that
226 the first lookup is the right choice.
227
228
229 For now we just use association lists.
230
231 \subsection{Avoiding a problem with overlapping}
232
233 Consider this little program:
234
235 \begin{pseudocode}
236      class C a        where c :: a
237      class C a => D a where d :: a
238
239      instance C Int where c = 17
240      instance D Int where d = 13
241
242      instance C a => C [a] where c = [c]
243      instance ({- C [a], -} D a) => D [a] where d = c
244
245      instance C [Int] where c = [37]
246
247      main = print (d :: [Int])
248 \end{pseudocode}
249
250 What do you think `main' prints  (assuming we have overlapping instances, and
251 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
252 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
253 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
254 the `C [Int]' instance is more specific).
255
256 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
257 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
258 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
259 doesn't even compile!  What's going on!?
260
261 What hugs complains about is the `D [a]' instance decl.
262
263 \begin{pseudocode}
264      ERROR "mj.hs" (line 10): Cannot build superclass instance
265      *** Instance            : D [a]
266      *** Context supplied    : D a
267      *** Required superclass : C [a]
268 \end{pseudocode}
269
270 You might wonder what hugs is complaining about.  It's saying that you
271 need to add `C [a]' to the context of the `D [a]' instance (as appears
272 in comments).  But there's that `C [a]' instance decl one line above
273 that says that I can reduce the need for a `C [a]' instance to the
274 need for a `C a' instance, and in this case, I already have the
275 necessary `C a' instance (since we have `D a' explicitly in the
276 context, and `C' is a superclass of `D').
277
278 Unfortunately, the above reasoning indicates a premature commitment to the
279 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
280 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
281 add the context that hugs suggests (uncomment the `C [a]'), effectively
282 deferring the decision about which instance to use.
283
284 Now, interestingly enough, 4.04 has this same bug, but it's covered up
285 in this case by a little known `optimization' that was disabled in
286 4.06.  Ghc-4.04 silently inserts any missing superclass context into
287 an instance declaration.  In this case, it silently inserts the `C
288 [a]', and everything happens to work out.
289
290 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
291 `Mark Jones', although Mark claims no credit for the `optimization' in
292 question, and would rather it stopped being called the `Mark Jones
293 optimization' ;-)
294
295 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
296 something else out with ghc-4.04.  Let's add the following line:
297
298     d' :: D a => [a]
299     d' = c
300
301 Everyone raise their hand who thinks that `d :: [Int]' should give a
302 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
303 `optimization' only applies to instance decls, not to regular
304 bindings, giving inconsistent behavior.
305
306 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
307 list of instances for a given class is ordered, so that more specific
308 instances come before more generic ones.  For example, the instance
309 list for C might contain:
310     ..., C Int, ..., C a, ...  
311 When we go to look for a `C Int' instance we'll get that one first.
312 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
313 pass the `C Int' instance, and keep going.  But if `b' is
314 unconstrained, then we don't know yet if the more specific instance
315 will eventually apply.  GHC keeps going, and matches on the generic `C
316 a'.  The fix is to, at each step, check to see if there's a reverse
317 match, and if so, abort the search.  This prevents hugs from
318 prematurely chosing a generic instance when a more specific one
319 exists.
320
321 --Jeff
322
323 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
324 this test.  Suppose the instance envt had
325     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
326 (still most specific first)
327 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
328         C x y Int  doesn't match the template {a,b} C a a b
329 but neither does 
330         C a a b  match the template {x,y} C x y Int
331 But still x and y might subsequently be unified so they *do* match.
332
333 Simple story: unify, don't match.
334
335
336 %************************************************************************
337 %*                                                                      *
338                 InstEnv, ClsInstEnv
339 %*                                                                      *
340 %************************************************************************
341
342 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
343 ClsInstEnv mapping is the dfun for that instance.
344
345 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
346
347         forall a b, C t1 t2 t3  can be constructed by dfun
348
349 or, to put it another way, we have
350
351         instance (...) => C t1 t2 t3,  witnessed by dfun
352
353 \begin{code}
354 ---------------------------------------------------
355 type InstEnv = UniqFM ClsInstEnv        -- Maps Class to instances for that class
356
357 data ClsInstEnv 
358   = ClsIE [Instance]    -- The instances for a particular class, in any order
359           Bool          -- True <=> there is an instance of form C a b c
360                         --      If *not* then the common case of looking up
361                         --      (C a b c) can fail immediately
362
363 instance Outputable ClsInstEnv where
364   ppr (ClsIE is b) = ptext (sLit "ClsIE") <+> ppr b <+> pprInstances is
365
366 -- INVARIANTS:
367 --  * The is_tvs are distinct in each Instance
368 --      of a ClsInstEnv (so we can safely unify them)
369
370 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
371 --      [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
372 -- The "a" in the pattern must be one of the forall'd variables in
373 -- the dfun type.
374
375 emptyInstEnv :: InstEnv
376 emptyInstEnv = emptyUFM
377
378 instEnvElts :: InstEnv -> [Instance]
379 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
380
381 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
382 classInstances (pkg_ie, home_ie) cls 
383   = get home_ie ++ get pkg_ie
384   where
385     get env = case lookupUFM env cls of
386                 Just (ClsIE insts _) -> insts
387                 Nothing              -> []
388
389 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
390 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
391
392 extendInstEnv :: InstEnv -> Instance -> InstEnv
393 extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
394   = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
395   where
396     add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
397                                               (ins_tyvar || cur_tyvar)
398     ins_tyvar = not (any isJust mb_tcs)
399 \end{code}
400
401
402 %************************************************************************
403 %*                                                                      *
404         Looking up an instance
405 %*                                                                      *
406 %************************************************************************
407
408 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
409 the env is kept ordered, the first match must be the only one.  The
410 thing we are looking up can have an arbitrary "flexi" part.
411
412 \begin{code}
413 type InstTypes = [Either TyVar Type]
414         -- Right ty     => Instantiate with this type
415         -- Left tv      => Instantiate with any type of this tyvar's kind
416
417 type InstMatch = (Instance, InstTypes)
418 \end{code}
419
420 Note [InstTypes: instantiating types]
421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
422 A successful match is an Instance, together with the types at which
423         the dfun_id in the Instance should be instantiated
424 The instantiating types are (Mabye Type)s because the dfun
425 might have some tyvars that *only* appear in arguments
426         dfun :: forall a b. C a b, Ord b => D [a]
427 When we match this against D [ty], we return the instantiating types
428         [Right ty, Left b]
429 where the Nothing indicates that 'b' can be freely instantiated.  
430 (The caller instantiates it to a flexi type variable, which will presumably
431  presumably later become fixed via functional dependencies.)
432
433 \begin{code}
434 lookupInstEnv :: (InstEnv, InstEnv)     -- External and home package inst-env
435               -> Class -> [Type]        -- What we are looking for
436               -> ([InstMatch],          -- Successful matches
437                   [Instance])           -- These don't match but do unify
438
439 -- The second component of the result pair happens when we look up
440 --      Foo [a]
441 -- in an InstEnv that has entries for
442 --      Foo [Int]
443 --      Foo [b]
444 -- Then which we choose would depend on the way in which 'a'
445 -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
446 -- but Foo [Int] is a unifier.  This gives the caller a better chance of
447 -- giving a suitable error messagen
448
449 lookupInstEnv (pkg_ie, home_ie) cls tys
450   = (pruned_matches, all_unifs)
451   where
452     rough_tcs  = roughMatchTcs tys
453     all_tvs    = all isNothing rough_tcs
454     (home_matches, home_unifs) = lookup home_ie 
455     (pkg_matches,  pkg_unifs)  = lookup pkg_ie  
456     all_matches = home_matches ++ pkg_matches
457     all_unifs   = home_unifs   ++ pkg_unifs
458     pruned_matches = foldr insert_overlapping [] all_matches
459         -- Even if the unifs is non-empty (an error situation)
460         -- we still prune the matches, so that the error message isn't
461         -- misleading (complaining of multiple matches when some should be
462         -- overlapped away)
463
464     --------------
465     lookup env = case lookupUFM env cls of
466                    Nothing -> ([],[])   -- No instances for this class
467                    Just (ClsIE insts has_tv_insts)
468                         | all_tvs && not has_tv_insts
469                         -> ([],[])      -- Short cut for common case
470                         -- The thing we are looking up is of form (C a b c), and
471                         -- the ClsIE has no instances of that form, so don't bother to search
472         
473                         | otherwise
474                         -> find [] [] insts
475
476     --------------
477     lookup_tv :: TvSubst -> TyVar -> Either TyVar Type  
478         -- See Note [InstTypes: instantiating types]
479     lookup_tv subst tv = case lookupTyVar subst tv of
480                                 Just ty -> Right ty
481                                 Nothing -> Left tv
482
483     find ms us [] = (ms, us)
484     find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs, 
485                                  is_tys = tpl_tys, is_flag = oflag,
486                                  is_dfun = dfun }) : rest)
487         -- Fast check for no match, uses the "rough match" fields
488       | instanceCantMatch rough_tcs mb_tcs
489       = find ms us rest
490
491       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
492       = let 
493             (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
494         in 
495         ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs )   -- Check invariant
496         find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
497
498         -- Does not match, so next check whether the things unify
499         -- See Note [overlapping instances] above
500       | Incoherent <- oflag
501       = find ms us rest
502
503       | otherwise
504       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
505                  (ppr cls <+> ppr tys <+> ppr all_tvs) $$
506                  (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
507                 )
508                 -- Unification will break badly if the variables overlap
509                 -- They shouldn't because we allocate separate uniques for them
510         case tcUnifyTys instanceBindFun tpl_tys tys of
511             Just _   -> find ms (item:us) rest
512             Nothing  -> find ms us        rest
513
514 ---------------
515 ---------------
516 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
517 -- Add a new solution, knocking out strictly less specific ones
518 insert_overlapping new_item [] = [new_item]
519 insert_overlapping new_item (item:items)
520   | new_beats_old && old_beats_new = item : insert_overlapping new_item items
521         -- Duplicate => keep both for error report
522   | new_beats_old = insert_overlapping new_item items
523         -- Keep new one
524   | old_beats_new = item : items
525         -- Keep old one
526   | otherwise     = item : insert_overlapping new_item items
527         -- Keep both
528   where
529     new_beats_old = new_item `beats` item
530     old_beats_new = item `beats` new_item
531
532     (instA, _) `beats` (instB, _)
533         = overlap_ok && 
534           isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
535                 -- A beats B if A is more specific than B, and B admits overlap
536                 -- I.e. if B can be instantiated to match A
537         where
538           overlap_ok = case is_flag instB of
539                         NoOverlap -> False
540                         _         -> True
541 \end{code}
542
543
544 %************************************************************************
545 %*                                                                      *
546         Binding decisions
547 %*                                                                      *
548 %************************************************************************
549
550 \begin{code}
551 instanceBindFun :: TyVar -> BindFlag
552 instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar tv = Skolem
553                    | otherwise                              = BindMe
554    -- Note [Binding when looking up instances]
555 \end{code}
556
557 Note [Binding when looking up instances]
558 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
559 When looking up in the instance environment, or family-instance environment,
560 we are careful about multiple matches, as described above in 
561 Note [Overlapping instances]
562
563 The key_tys can contain skolem constants, and we can guarantee that those
564 are never going to be instantiated to anything, so we should not involve
565 them in the unification test.  Example:
566         class Foo a where { op :: a -> Int }
567         instance Foo a => Foo [a]       -- NB overlap
568         instance Foo [Int]              -- NB overlap
569         data T = forall a. Foo a => MkT a
570         f :: T -> Int
571         f (MkT x) = op [x,x]
572 The op [x,x] means we need (Foo [a]).  Without the filterVarSet we'd
573 complain, saying that the choice of instance depended on the instantiation
574 of 'a'; but of course it isn't *going* to be instantiated.
575
576 We do this only for isOverlappableTyVar skolems.  For example we reject
577         g :: forall a => [a] -> Int
578         g x = op x
579 on the grounds that the correct instance depends on the instantiation of 'a'