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