Complete work on new OVERLAPPABLE/OVERLAPPING pragmas (Trac #9242)
[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 {-# LANGUAGE CPP, DeriveDataTypeable #-}
11
12 module InstEnv (
13         DFunId, InstMatch, ClsInstLookupResult,
14         OverlapFlag(..), OverlapMode(..), setOverlapModeMaybe,
15         ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances,
16         instanceHead, instanceSig, mkLocalInstance, mkImportedInstance,
17         instanceDFunId, tidyClsInstDFun, instanceRoughTcs,
18
19         InstEnv, emptyInstEnv, extendInstEnv, deleteFromInstEnv, identicalInstHead, 
20         extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv', lookupInstEnv, instEnvElts,
21         classInstances, orphNamesOfClsInst, instanceBindFun,
22         instanceCantMatch, roughMatchTcs
23     ) where
24
25 #include "HsVersions.h"
26
27 import Class
28 import Var
29 import VarSet
30 import Name
31 import NameSet
32 import TcType
33 import TyCon
34 import Unify
35 import Outputable
36 import ErrUtils
37 import BasicTypes
38 import UniqFM
39 import Util
40 import Id
41 import FastString
42 import Data.Data        ( Data, Typeable )
43 import Data.Maybe       ( isJust, isNothing )
44 \end{code}
45
46
47 %************************************************************************
48 %*                                                                      *
49 \subsection{The key types}
50 %*                                                                      *
51 %************************************************************************
52
53 \begin{code}
54 data ClsInst 
55   = ClsInst {   -- Used for "rough matching"; see Note [Rough-match field]
56                 -- INVARIANT: is_tcs = roughMatchTcs is_tys
57                is_cls_nm :: Name  -- Class name
58              , is_tcs  :: [Maybe Name]  -- Top of type args
59
60                 -- Used for "proper matching"; see Note [Proper-match fields]
61              , is_tvs  :: [TyVar]       -- Fresh template tyvars for full match
62                                         -- See Note [Template tyvars are fresh]
63              , is_cls  :: Class         -- The real class
64              , is_tys  :: [Type]        -- Full arg types (mentioning is_tvs)
65                 -- INVARIANT: is_dfun Id has type 
66                 --      forall is_tvs. (...) => is_cls is_tys
67                 -- (modulo alpha conversion)
68
69              , is_dfun :: DFunId -- See Note [Haddock assumptions]
70                     -- See Note [Silent superclass arguments] in TcInstDcls
71                     -- for how to map the DFun's type back to the source
72                     -- language instance decl
73
74              , is_flag :: OverlapFlag   -- See detailed comments with
75                                         -- the decl of BasicTypes.OverlapFlag
76     }
77   deriving (Data, Typeable)
78 \end{code}
79
80 Note [Template tyvars are fresh]
81 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
82 The is_tvs field of a ClsInst has *completely fresh* tyvars.  
83 That is, they are
84   * distinct from any other ClsInst
85   * distinct from any tyvars free in predicates that may
86     be looked up in the class instance environment
87 Reason for freshness: we use unification when checking for overlap
88 etc, and that requires the tyvars to be distinct.
89
90 The invariant is checked by the ASSERT in lookupInstEnv'.
91
92 Note [Rough-match field]
93 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
94 The is_cls_nm, is_tcs fields allow a "rough match" to be done
95 *without* poking inside the DFunId.  Poking the DFunId forces
96 us to suck in all the type constructors etc it involves,
97 which is a total waste of time if it has no chance of matching
98 So the Name, [Maybe Name] fields allow us to say "definitely
99 does not match", based only on the Name.
100
101 In is_tcs, 
102     Nothing  means that this type arg is a type variable
103
104     (Just n) means that this type arg is a
105                 TyConApp with a type constructor of n.
106                 This is always a real tycon, never a synonym!
107                 (Two different synonyms might match, but two
108                 different real tycons can't.)
109                 NB: newtypes are not transparent, though!
110
111 Note [Proper-match fields]
112 ~~~~~~~~~~~~~~~~~~~~~~~~~
113 The is_tvs, is_cls, is_tys fields are simply cached values, pulled
114 out (lazily) from the dfun id. They are cached here simply so 
115 that we don't need to decompose the DFunId each time we want 
116 to match it.  The hope is that the fast-match fields mean
117 that we often never poke the proper-match fields.
118
119 However, note that:
120  * is_tvs must be a superset of the free vars of is_tys
121
122  * is_tvs, is_tys may be alpha-renamed compared to the ones in
123    the dfun Id
124
125 Note [Haddock assumptions]
126 ~~~~~~~~~~~~~~~~~~~~~~~~~~
127 For normal user-written instances, Haddock relies on
128
129  * the SrcSpan of
130  * the Name of
131  * the is_dfun of
132  * an Instance
133
134 being equal to
135
136   * the SrcSpan of
137   * the instance head type of
138   * the InstDecl used to construct the Instance.
139
140 \begin{code}
141 instanceDFunId :: ClsInst -> DFunId
142 instanceDFunId = is_dfun
143
144 tidyClsInstDFun :: (DFunId -> DFunId) -> ClsInst -> ClsInst
145 tidyClsInstDFun tidy_dfun ispec
146   = ispec { is_dfun = tidy_dfun (is_dfun ispec) }
147
148 instanceRoughTcs :: ClsInst -> [Maybe Name]
149 instanceRoughTcs = is_tcs
150 \end{code}
151
152 \begin{code}
153 instance NamedThing ClsInst where
154    getName ispec = getName (is_dfun ispec)
155
156 instance Outputable ClsInst where
157    ppr = pprInstance
158
159 pprInstance :: ClsInst -> SDoc
160 -- Prints the ClsInst as an instance declaration
161 pprInstance ispec
162   = hang (pprInstanceHdr ispec)
163         2 (vcat [ ptext (sLit "--") <+> pprDefinedAt (getName ispec)
164                 , ifPprDebug (ppr (is_dfun ispec)) ])
165
166 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
167 pprInstanceHdr :: ClsInst -> SDoc
168 -- Prints the ClsInst as an instance declaration
169 pprInstanceHdr (ClsInst { is_flag = flag, is_dfun = dfun })
170   = getPprStyle $ \ sty ->
171     let dfun_ty = idType dfun
172         (tvs, theta, res_ty) = tcSplitSigmaTy dfun_ty
173         theta_to_print = drop (dfunNSilent dfun) theta
174           -- See Note [Silent superclass arguments] in TcInstDcls
175         ty_to_print | debugStyle sty = dfun_ty
176                     | otherwise      = mkSigmaTy tvs theta_to_print res_ty
177     in ptext (sLit "instance") <+> ppr flag <+> pprSigmaType ty_to_print
178
179 pprInstances :: [ClsInst] -> SDoc
180 pprInstances ispecs = vcat (map pprInstance ispecs)
181
182 instanceHead :: ClsInst -> ([TyVar], Class, [Type])
183 -- Returns the head, using the fresh tyavs from the ClsInst
184 instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
185    = (tvs, cls, tys)
186    where
187      (_, _, cls, _) = tcSplitDFunTy (idType dfun)
188
189 instanceSig :: ClsInst -> ([TyVar], [Type], Class, [Type])
190 -- Decomposes the DFunId
191 instanceSig ispec = tcSplitDFunTy (idType (is_dfun ispec))
192
193 mkLocalInstance :: DFunId -> OverlapFlag
194                 -> [TyVar] -> Class -> [Type]
195                 -> ClsInst
196 -- Used for local instances, where we can safely pull on the DFunId
197 mkLocalInstance dfun oflag tvs cls tys
198   = ClsInst { is_flag = oflag, is_dfun = dfun
199             , is_tvs = tvs
200             , is_cls = cls, is_cls_nm = className cls
201             , is_tys = tys, is_tcs = roughMatchTcs tys }
202
203 mkImportedInstance :: Name -> [Maybe Name]
204                    -> DFunId -> OverlapFlag -> ClsInst
205 -- Used for imported instances, where we get the rough-match stuff
206 -- from the interface file
207 -- The bound tyvars of the dfun are guaranteed fresh, because
208 -- the dfun has been typechecked out of the same interface file
209 mkImportedInstance cls_nm mb_tcs dfun oflag
210   = ClsInst { is_flag = oflag, is_dfun = dfun
211             , is_tvs = tvs, is_tys = tys
212             , is_cls_nm = cls_nm, is_cls = cls, is_tcs = mb_tcs }
213   where
214     (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
215
216 roughMatchTcs :: [Type] -> [Maybe Name]
217 roughMatchTcs tys = map rough tys
218   where
219     rough ty = case tcSplitTyConApp_maybe ty of
220                   Just (tc,_) -> Just (tyConName tc)
221                   Nothing     -> Nothing
222
223 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
224 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
225 -- possibly be instantiated to actual, nor vice versa; 
226 -- False is non-committal
227 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
228 instanceCantMatch _             _             =  False  -- Safe
229 \end{code}
230
231
232 Note [Overlapping instances]
233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
234 Overlap is permitted, but only in such a way that one can make
235 a unique choice when looking up.  That is, overlap is only permitted if
236 one template matches the other, or vice versa.  So this is ok:
237
238   [a]  [Int]
239
240 but this is not
241
242   (Int,a)  (b,Int)
243
244 If overlap is permitted, the list is kept most specific first, so that
245 the first lookup is the right choice.
246
247
248 For now we just use association lists.
249
250 \subsection{Avoiding a problem with overlapping}
251
252 Consider this little program:
253
254 \begin{pseudocode}
255      class C a        where c :: a
256      class C a => D a where d :: a
257
258      instance C Int where c = 17
259      instance D Int where d = 13
260
261      instance C a => C [a] where c = [c]
262      instance ({- C [a], -} D a) => D [a] where d = c
263
264      instance C [Int] where c = [37]
265
266      main = print (d :: [Int])
267 \end{pseudocode}
268
269 What do you think `main' prints  (assuming we have overlapping instances, and
270 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
271 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
272 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
273 the `C [Int]' instance is more specific).
274
275 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
276 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
277 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
278 doesn't even compile!  What's going on!?
279
280 What hugs complains about is the `D [a]' instance decl.
281
282 \begin{pseudocode}
283      ERROR "mj.hs" (line 10): Cannot build superclass instance
284      *** Instance            : D [a]
285      *** Context supplied    : D a
286      *** Required superclass : C [a]
287 \end{pseudocode}
288
289 You might wonder what hugs is complaining about.  It's saying that you
290 need to add `C [a]' to the context of the `D [a]' instance (as appears
291 in comments).  But there's that `C [a]' instance decl one line above
292 that says that I can reduce the need for a `C [a]' instance to the
293 need for a `C a' instance, and in this case, I already have the
294 necessary `C a' instance (since we have `D a' explicitly in the
295 context, and `C' is a superclass of `D').
296
297 Unfortunately, the above reasoning indicates a premature commitment to the
298 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
299 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
300 add the context that hugs suggests (uncomment the `C [a]'), effectively
301 deferring the decision about which instance to use.
302
303 Now, interestingly enough, 4.04 has this same bug, but it's covered up
304 in this case by a little known `optimization' that was disabled in
305 4.06.  Ghc-4.04 silently inserts any missing superclass context into
306 an instance declaration.  In this case, it silently inserts the `C
307 [a]', and everything happens to work out.
308
309 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
310 `Mark Jones', although Mark claims no credit for the `optimization' in
311 question, and would rather it stopped being called the `Mark Jones
312 optimization' ;-)
313
314 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
315 something else out with ghc-4.04.  Let's add the following line:
316
317     d' :: D a => [a]
318     d' = c
319
320 Everyone raise their hand who thinks that `d :: [Int]' should give a
321 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
322 `optimization' only applies to instance decls, not to regular
323 bindings, giving inconsistent behavior.
324
325 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
326 list of instances for a given class is ordered, so that more specific
327 instances come before more generic ones.  For example, the instance
328 list for C might contain:
329     ..., C Int, ..., C a, ...  
330 When we go to look for a `C Int' instance we'll get that one first.
331 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
332 pass the `C Int' instance, and keep going.  But if `b' is
333 unconstrained, then we don't know yet if the more specific instance
334 will eventually apply.  GHC keeps going, and matches on the generic `C
335 a'.  The fix is to, at each step, check to see if there's a reverse
336 match, and if so, abort the search.  This prevents hugs from
337 prematurely chosing a generic instance when a more specific one
338 exists.
339
340 --Jeff
341
342 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
343 this test.  Suppose the instance envt had
344     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
345 (still most specific first)
346 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
347         C x y Int  doesn't match the template {a,b} C a a b
348 but neither does 
349         C a a b  match the template {x,y} C x y Int
350 But still x and y might subsequently be unified so they *do* match.
351
352 Simple story: unify, don't match.
353
354
355 %************************************************************************
356 %*                                                                      *
357                 InstEnv, ClsInstEnv
358 %*                                                                      *
359 %************************************************************************
360
361 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
362 ClsInstEnv mapping is the dfun for that instance.
363
364 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
365
366         forall a b, C t1 t2 t3  can be constructed by dfun
367
368 or, to put it another way, we have
369
370         instance (...) => C t1 t2 t3,  witnessed by dfun
371
372 \begin{code}
373 ---------------------------------------------------
374 type InstEnv = UniqFM ClsInstEnv        -- Maps Class to instances for that class
375
376 newtype ClsInstEnv 
377   = ClsIE [ClsInst]    -- The instances for a particular class, in any order
378
379 instance Outputable ClsInstEnv where
380   ppr (ClsIE is) = pprInstances is
381
382 -- INVARIANTS:
383 --  * The is_tvs are distinct in each ClsInst
384 --      of a ClsInstEnv (so we can safely unify them)
385
386 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
387 --      [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
388 -- The "a" in the pattern must be one of the forall'd variables in
389 -- the dfun type.
390
391 emptyInstEnv :: InstEnv
392 emptyInstEnv = emptyUFM
393
394 instEnvElts :: InstEnv -> [ClsInst]
395 instEnvElts ie = [elt | ClsIE elts <- eltsUFM ie, elt <- elts]
396
397 classInstances :: (InstEnv,InstEnv) -> Class -> [ClsInst]
398 classInstances (pkg_ie, home_ie) cls 
399   = get home_ie ++ get pkg_ie
400   where
401     get env = case lookupUFM env cls of
402                 Just (ClsIE insts) -> insts
403                 Nothing            -> []
404
405 -- | Collects the names of concrete types and type constructors that make
406 -- up the head of a class instance. For instance, given `class Foo a b`:
407 --
408 -- `instance Foo (Either (Maybe Int) a) Bool` would yield
409 --      [Either, Maybe, Int, Bool]
410 --
411 -- Used in the implementation of ":info" in GHCi.
412 orphNamesOfClsInst :: ClsInst -> NameSet
413 orphNamesOfClsInst = orphNamesOfDFunHead . idType . instanceDFunId
414
415 extendInstEnvList :: InstEnv -> [ClsInst] -> InstEnv
416 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
417
418 extendInstEnv :: InstEnv -> ClsInst -> InstEnv
419 extendInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
420   = addToUFM_C add inst_env cls_nm (ClsIE [ins_item])
421   where
422     add (ClsIE cur_insts) _ = ClsIE (ins_item : cur_insts)
423
424 deleteFromInstEnv :: InstEnv -> ClsInst -> InstEnv
425 deleteFromInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
426   = adjustUFM adjust inst_env cls_nm
427   where
428     adjust (ClsIE items) = ClsIE (filterOut (identicalInstHead ins_item) items)
429
430 identicalInstHead :: ClsInst -> ClsInst -> Bool
431 -- ^ True when when the instance heads are the same
432 -- e.g.  both are   Eq [(a,b)]
433 -- Obviously should be insenstive to alpha-renaming
434 identicalInstHead (ClsInst { is_cls_nm = cls_nm1, is_tcs = rough1, is_tvs = tvs1, is_tys = tys1 })
435                   (ClsInst { is_cls_nm = cls_nm2, is_tcs = rough2, is_tvs = tvs2, is_tys = tys2 })
436   =  cls_nm1 == cls_nm2
437   && not (instanceCantMatch rough1 rough2)  -- Fast check for no match, uses the "rough match" fields
438   && isJust (tcMatchTys (mkVarSet tvs1) tys1 tys2)
439   && isJust (tcMatchTys (mkVarSet tvs2) tys2 tys1)
440 \end{code}
441
442
443 %************************************************************************
444 %*                                                                      *
445         Looking up an instance
446 %*                                                                      *
447 %************************************************************************
448
449 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
450 the env is kept ordered, the first match must be the only one.  The
451 thing we are looking up can have an arbitrary "flexi" part.
452
453 Note [Rules for instance lookup]
454 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
455 These functions implement the carefully-written rules in the user
456 manual section on "overlapping instances". At risk of duplication,
457 here are the rules.  If the rules change, change this text and the
458 user manual simultaneously.  The link may be this:
459 http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap
460
461 The willingness to be overlapped or incoherent is a property of the
462 instance declaration itself, controlled as follows:
463
464  * An instance is "incoherent"
465    if it has an INCOHERENT pragama, or
466    if it appears in a module compiled with -XIncoherentInstances.
467
468  * An instance is "overlappable"
469    if it has an OVERLAPPABLE or OVERLAPS pragama, or
470    if it appears in a module compiled with -XOverlappingInstances, or
471    if the instance is incoherent.
472
473  * An instance is "overlapping"
474    if it has an OVERLAPPING or OVERLAPS pragama, or
475    if it appears in a module compiled with -XOverlappingInstances, or
476    if the instance is incoherent.
477      compiled with -XOverlappingInstances.
478
479 Now suppose that, in some client module, we are searching for an instance
480 of the target constraint (C ty1 .. tyn). The search works like this.
481
482  * Find all instances I that match the target constraint; that is, the
483    target constraint is a substitution instance of I. These instance
484    declarations are the candidates.
485
486  * Find all non-candidate instances that unify with the target
487    constraint. Such non-candidates instances might match when the
488    target constraint is further instantiated. If all of them are
489    incoherent, proceed; if not, the search fails.
490
491  * Eliminate any candidate IX for which both of the following hold:
492    * There is another candidate IY that is strictly more specific;
493      that is, IY is a substitution instance of IX but not vice versa.
494
495    * Either IX is overlappable or IY is overlapping.
496
497  * If only one candidate remains, pick it. Otherwise if all remaining
498    candidates are incoherent, pick an arbitrary candidate. Otherwise fail.
499
500
501 \begin{code}
502 type DFunInstType = Maybe Type
503         -- Just ty   => Instantiate with this type
504         -- Nothing   => Instantiate with any type of this tyvar's kind
505         -- See Note [DFunInstType: instantiating types]
506
507 type InstMatch = (ClsInst, [DFunInstType])
508
509 type ClsInstLookupResult 
510      = ( [InstMatch]     -- Successful matches
511        , [ClsInst]       -- These don't match but do unify
512        , Bool)           -- True if error condition caused by
513                          -- SafeHaskell condition.
514 \end{code}
515
516 Note [DFunInstType: instantiating types]
517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
518 A successful match is a ClsInst, together with the types at which
519         the dfun_id in the ClsInst should be instantiated
520 The instantiating types are (Either TyVar Type)s because the dfun
521 might have some tyvars that *only* appear in arguments
522         dfun :: forall a b. C a b, Ord b => D [a]
523 When we match this against D [ty], we return the instantiating types
524         [Just ty, Nothing]
525 where the 'Nothing' indicates that 'b' can be freely instantiated.  
526 (The caller instantiates it to a flexi type variable, which will 
527  presumably later become fixed via functional dependencies.)
528
529 \begin{code}
530 -- |Look up an instance in the given instance environment. The given class application must match exactly
531 -- one instance and the match may not contain any flexi type variables.  If the lookup is unsuccessful,
532 -- yield 'Left errorMessage'.
533 --
534 lookupUniqueInstEnv :: (InstEnv, InstEnv) 
535                     -> Class -> [Type]
536                     -> Either MsgDoc (ClsInst, [Type])
537 lookupUniqueInstEnv instEnv cls tys
538   = case lookupInstEnv instEnv cls tys of
539       ([(inst, inst_tys)], _, _) 
540              | noFlexiVar -> Right (inst, inst_tys')
541              | otherwise  -> Left $ ptext (sLit "flexible type variable:") <+>
542                                     (ppr $ mkTyConApp (classTyCon cls) tys)
543              where
544                inst_tys'  = [ty | Just ty <- inst_tys]
545                noFlexiVar = all isJust inst_tys
546       _other -> Left $ ptext (sLit "instance not found") <+> (ppr $ mkTyConApp (classTyCon cls) tys)
547
548 lookupInstEnv' :: InstEnv          -- InstEnv to look in
549                -> Class -> [Type]  -- What we are looking for
550                -> ([InstMatch],    -- Successful matches
551                    [ClsInst])     -- These don't match but do unify
552 -- The second component of the result pair happens when we look up
553 --      Foo [a]
554 -- in an InstEnv that has entries for
555 --      Foo [Int]
556 --      Foo [b]
557 -- Then which we choose would depend on the way in which 'a'
558 -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
559 -- but Foo [Int] is a unifier.  This gives the caller a better chance of
560 -- giving a suitable error message
561
562 lookupInstEnv' ie cls tys
563   = lookup ie
564   where
565     rough_tcs  = roughMatchTcs tys
566     all_tvs    = all isNothing rough_tcs
567     --------------
568     lookup env = case lookupUFM env cls of
569                    Nothing -> ([],[])   -- No instances for this class
570                    Just (ClsIE insts) -> find [] [] insts
571
572     --------------
573     find ms us [] = (ms, us)
574     find ms us (item@(ClsInst { is_tcs = mb_tcs, is_tvs = tpl_tvs
575                               , is_tys = tpl_tys, is_flag = oflag }) : rest)
576         -- Fast check for no match, uses the "rough match" fields
577       | instanceCantMatch rough_tcs mb_tcs
578       = find ms us rest
579
580       | Just subst <- tcMatchTys tpl_tv_set tpl_tys tys
581       = find ((item, map (lookup_tv subst) tpl_tvs) : ms) us rest
582
583         -- Does not match, so next check whether the things unify
584         -- See Note [Overlapping instances] and Note [Incoherent instances]
585       | Incoherent <- overlapMode oflag
586       = find ms us rest
587
588       | otherwise
589       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tv_set,
590                  (ppr cls <+> ppr tys <+> ppr all_tvs) $$
591                  (ppr tpl_tvs <+> ppr tpl_tys)
592                 )
593                 -- Unification will break badly if the variables overlap
594                 -- They shouldn't because we allocate separate uniques for them
595                 -- See Note [Template tyvars are fresh]
596         case tcUnifyTys instanceBindFun tpl_tys tys of
597             Just _   -> find ms (item:us) rest
598             Nothing  -> find ms us        rest
599       where
600         tpl_tv_set = mkVarSet tpl_tvs
601
602     ----------------
603     lookup_tv :: TvSubst -> TyVar -> DFunInstType
604         -- See Note [DFunInstType: instantiating types]
605     lookup_tv subst tv = case lookupTyVar subst tv of
606                                 Just ty -> Just ty
607                                 Nothing -> Nothing
608
609 ---------------
610 -- This is the common way to call this function.
611 lookupInstEnv :: (InstEnv, InstEnv)     -- External and home package inst-env
612               -> Class -> [Type]   -- What we are looking for
613               -> ClsInstLookupResult
614 -- ^ See Note [Rules for instance lookup]
615 lookupInstEnv (pkg_ie, home_ie) cls tys
616   = (safe_matches, all_unifs, safe_fail)
617   where
618     (home_matches, home_unifs) = lookupInstEnv' home_ie cls tys
619     (pkg_matches,  pkg_unifs)  = lookupInstEnv' pkg_ie  cls tys
620     all_matches = home_matches ++ pkg_matches
621     all_unifs   = home_unifs   ++ pkg_unifs
622     pruned_matches = foldr insert_overlapping [] all_matches
623     (safe_matches, safe_fail) = if length pruned_matches == 1 
624                         then check_safe (head pruned_matches) all_matches
625                         else (pruned_matches, False)
626         -- Even if the unifs is non-empty (an error situation)
627         -- we still prune the matches, so that the error message isn't
628         -- misleading (complaining of multiple matches when some should be
629         -- overlapped away)
630
631     -- NOTE [Safe Haskell isSafeOverlap]
632     -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
633     -- We restrict code compiled in 'Safe' mode from overriding code
634     -- compiled in any other mode. The rationale is that code compiled
635     -- in 'Safe' mode is code that is untrusted by the ghc user. So
636     -- we shouldn't let that code change the behaviour of code the
637     -- user didn't compile in 'Safe' mode since that's the code they
638     -- trust. So 'Safe' instances can only overlap instances from the
639     -- same module. A same instance origin policy for safe compiled
640     -- instances.
641     check_safe match@(inst,_) others
642         = case isSafeOverlap (is_flag inst) of
643                 -- most specific isn't from a Safe module so OK
644                 False -> ([match], False)
645                 -- otherwise we make sure it only overlaps instances from
646                 -- the same module
647                 True -> (go [] others, True)
648         where
649             go bad [] = match:bad
650             go bad (i@(x,_):unchecked) =
651                 if inSameMod x
652                     then go bad unchecked
653                     else go (i:bad) unchecked
654
655             inSameMod b =
656                 let na = getName $ getName inst
657                     la = isInternalName na
658                     nb = getName $ getName b
659                     lb = isInternalName nb
660                 in (la && lb) || (nameModule na == nameModule nb)
661
662 ---------------
663 ---------------
664 insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
665 -- ^ Add a new solution, knocking out strictly less specific ones
666 -- See Note [Rules for instance lookup]
667 insert_overlapping new_item [] = [new_item]
668 insert_overlapping new_item (item:items)
669   | new_beats_old && old_beats_new = item : insert_overlapping new_item items
670         -- Duplicate => keep both for error report
671   | new_beats_old = insert_overlapping new_item items
672         -- Keep new one
673   | old_beats_new = item : items
674         -- Keep old one
675   | incoherent new_item = item : items -- note [Incoherent instances]
676         -- Keep old one
677   | incoherent item = new_item : items
678         -- Keep new one
679   | otherwise     = item : insert_overlapping new_item items
680         -- Keep both
681   where
682     new_beats_old = new_item `beats` item
683     old_beats_new = item `beats` new_item
684
685     incoherent (inst, _) = overlapMode (is_flag inst) == Incoherent
686
687     -- `instB` can be instantiated to match `instA`
688     instA `moreSpecificThan` instB =
689       isJust (tcMatchTys (mkVarSet (is_tvs instB))
690              (is_tys instB) (is_tys instA))
691
692     (instA, _) `beats` (instB, _)
693           = overlap_ok && (instA `moreSpecificThan` instB)
694           where
695             {- Overlap permitted if either the more specific instance
696             is marked as overlapping, or the more general one is
697             marked as overlappable.
698             Latest change described in: Trac #9242.
699             Previous change: Trac #3877, Dec 10.  -}
700             overlap_ok = hasOverlappingFlag  (overlapMode (is_flag instA))
701                       || hasOverlappableFlag (overlapMode (is_flag instB))
702 \end{code}
703
704 Note [Incoherent instances]
705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 For some classes, the choice of a particular instance does not matter, any one
707 is good. E.g. consider
708
709         class D a b where { opD :: a -> b -> String }
710         instance D Int b where ...
711         instance D a Int where ...
712
713         g (x::Int) = opD x x  -- Wanted: D Int Int
714
715 For such classes this should work (without having to add an "instance D Int
716 Int", and using -XOverlappingInstances, which would then work). This is what
717 -XIncoherentInstances is for: Telling GHC "I don't care which instance you use;
718 if you can use one, use it."
719
720 Should this logic only work when *all* candidates have the incoherent flag, or
721 even when all but one have it? The right choice is the latter, which can be
722 justified by comparing the behaviour with how -XIncoherentInstances worked when
723 it was only about the unify-check (note [Overlapping instances]):
724
725 Example:
726         class C a b c where foo :: (a,b,c)
727         instance C [a] b Int
728         instance [incoherent] [Int] b c
729         instance [incoherent] C a Int c
730 Thanks to the incoherent flags,
731         [Wanted]  C [a] b Int
732 works: Only instance one matches, the others just unify, but are marked
733 incoherent.
734
735 So I can write
736         (foo :: ([a],b,Int)) :: ([Int], Int, Int).
737 but if that works then I really want to be able to write
738         foo :: ([Int], Int, Int)
739 as well. Now all three instances from above match. None is more specific than
740 another, so none is ruled out by the normal overlapping rules. One of them is
741 not incoherent, but we still want this to compile. Hence the
742 "all-but-one-logic".
743
744 The implementation is in insert_overlapping, where we remove matching
745 incoherent instances as long as there are are others.
746
747
748
749 %************************************************************************
750 %*                                                                      *
751         Binding decisions
752 %*                                                                      *
753 %************************************************************************
754
755 \begin{code}
756 instanceBindFun :: TyVar -> BindFlag
757 instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar tv = Skolem
758                    | otherwise                              = BindMe
759    -- Note [Binding when looking up instances]
760 \end{code}
761
762 Note [Binding when looking up instances]
763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
764 When looking up in the instance environment, or family-instance environment,
765 we are careful about multiple matches, as described above in 
766 Note [Overlapping instances]
767
768 The key_tys can contain skolem constants, and we can guarantee that those
769 are never going to be instantiated to anything, so we should not involve
770 them in the unification test.  Example:
771         class Foo a where { op :: a -> Int }
772         instance Foo a => Foo [a]       -- NB overlap
773         instance Foo [Int]              -- NB overlap
774         data T = forall a. Foo a => MkT a
775         f :: T -> Int
776         f (MkT x) = op [x,x]
777 The op [x,x] means we need (Foo [a]).  Without the filterVarSet we'd
778 complain, saying that the choice of instance depended on the instantiation
779 of 'a'; but of course it isn't *going* to be instantiated.
780
781 We do this only for isOverlappableTyVar skolems.  For example we reject
782         g :: forall a => [a] -> Int
783         g x = op x
784 on the grounds that the correct instance depends on the instantiation of 'a'