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