Add comments about invariants
[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, 
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 OccName
29 import NameSet
30 import Type
31 import TcType
32 import TyCon
33 import TcGadt
34 import Unify
35 import Outputable
36 import BasicTypes
37 import UniqFM
38 import Id
39 import SrcLoc
40
41 import Data.Maybe       ( isJust, isNothing )
42 \end{code}
43
44
45 %************************************************************************
46 %*                                                                      *
47 \subsection{The key types}
48 %*                                                                      *
49 %************************************************************************
50
51 \begin{code}
52 type DFunId = Id
53 data Instance 
54   = Instance { is_cls  :: Name          -- Class name
55         
56                 -- Used for "rough matching"; see note below
57                 -- INVARIANT: is_tcs = roughMatchTcs is_tys
58              , is_tcs  :: [Maybe Name]  -- Top of type args
59
60                 -- Used for "proper matching"; see note
61              , is_tvs  :: TyVarSet      -- Template tyvars for full match
62              , is_tys  :: [Type]        -- Full arg types
63                 -- INVARIANT: is_dfun Id has type 
64                 --      forall is_tvs. (...) => is_cls is_tys
65
66              , is_dfun :: DFunId
67              , is_flag :: OverlapFlag   -- See detailed comments with
68                                         -- the decl of BasicTypes.OverlapFlag
69
70              , is_orph :: Maybe OccName }
71 \end{code}
72
73 The "rough-match" fields
74 ~~~~~~~~~~~~~~~~~~~~~~~~~
75 The is_cls, is_args fields allow a "rough match" to be done
76 without poking inside the DFunId.  Poking the DFunId forces
77 us to suck in all the type constructors etc it involves,
78 which is a total waste of time if it has no chance of matching
79 So the Name, [Maybe Name] fields allow us to say "definitely
80 does not match", based only on the Name.
81
82 In is_tcs, 
83     Nothing  means that this type arg is a type variable
84
85     (Just n) means that this type arg is a
86                 TyConApp with a type constructor of n.
87                 This is always a real tycon, never a synonym!
88                 (Two different synonyms might match, but two
89                 different real tycons can't.)
90                 NB: newtypes are not transparent, though!
91
92 The "proper-match" fields
93 ~~~~~~~~~~~~~~~~~~~~~~~~~
94 The is_tvs, is_tys fields are simply cached values, pulled
95 out (lazily) from the dfun id. They are cached here simply so 
96 that we don't need to decompose the DFunId each time we want 
97 to match it.  The hope is that the fast-match fields mean
98 that we often never poke th proper-match fields
99
100 However, note that:
101  * is_tvs must be a superset of the free vars of is_tys
102
103  * The is_dfun must itself be quantified over exactly is_tvs
104    (This is so that we can use the matching substitution to
105     instantiate the dfun's context.)
106
107
108 Note [Orphans]: the "is_orph" field
109 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
110 An instance is an orphan if its head (after the =>) mentions
111 nothing defined in this module.  
112
113    Just n       The head mentions n, which is defined in this module
114                 This is used for versioning; the instance decl is
115                 considered part of the defn of n when computing versions
116
117    Nothing      The head mentions nothing defined in this module
118
119 If a module contains any orphans, then its interface file is read 
120 regardless, so that its instances are not missed. 
121
122 Functional dependencies worsen the situation a bit. Consider
123         class C a b | a -> b
124 In some other module we might have
125    module M where
126         data T = ...
127         instance C Int T where ...
128 This isn't considered an orphan, so we will only read M's interface
129 if something from M is used (e.g. T).  So there's a risk we'll
130 miss the improvement from the instance.  Workaround: import M.
131
132 Rules are orphans and versioned in much the same way.
133
134 \begin{code}
135 instanceDFunId :: Instance -> DFunId
136 instanceDFunId = is_dfun
137
138 setInstanceDFunId :: Instance -> DFunId -> Instance
139 setInstanceDFunId ispec dfun
140    = ASSERT( idType dfun `tcEqType` idType (is_dfun ispec) )
141         -- We need to create the cached fields afresh from
142         -- the new dfun id.  In particular, the is_tvs in
143         -- the Instance must match those in the dfun!
144         -- We assume that the only thing that changes is
145         -- the quantified type variables, so the other fields
146         -- are ok; hence the assert
147      ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
148    where 
149      (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
150
151 instanceRoughTcs :: Instance -> [Maybe Name]
152 instanceRoughTcs = is_tcs
153 \end{code}
154
155 \begin{code}
156 instance NamedThing Instance where
157    getName ispec = getName (is_dfun ispec)
158
159 instance Outputable Instance where
160    ppr = pprInstance
161
162 pprInstance :: Instance -> SDoc
163 -- Prints the Instance as an instance declaration
164 pprInstance ispec@(Instance { is_flag = flag })
165   = hang (pprInstanceHdr ispec)
166         2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc ispec)))
167
168 -- * pprInstanceHdr is used in VStudio to populate the ClassView tree
169 pprInstanceHdr :: Instance -> SDoc
170 -- Prints the Instance as an instance declaration
171 pprInstanceHdr ispec@(Instance { is_flag = flag })
172   = ptext SLIT("instance") <+> ppr flag
173     <+> sep [pprThetaArrow theta, pprClassPred clas tys]
174   where
175     (_, theta, clas, tys) = instanceHead ispec
176         -- Print without the for-all, which the programmer doesn't write
177
178 pprInstances :: [Instance] -> SDoc
179 pprInstances ispecs = vcat (map pprInstance ispecs)
180
181 instanceHead :: Instance -> ([TyVar], [PredType], Class, [Type])
182 instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec))
183
184 mkLocalInstance :: DFunId -> OverlapFlag -> Instance
185 -- Used for local instances, where we can safely pull on the DFunId
186 mkLocalInstance dfun oflag
187   = Instance {  is_flag = oflag, is_dfun = dfun,
188                 is_tvs = mkVarSet tvs, is_tys = tys,
189                 is_cls = cls_name, is_tcs = roughMatchTcs tys,
190                 is_orph = orph }
191   where
192     (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
193     mod = nameModule (idName dfun)
194     cls_name = getName cls
195     tycl_names = foldr (unionNameSets . tyClsNamesOfType) 
196                        (unitNameSet cls_name) tys
197     orph = case filter (nameIsLocalOrFrom mod) (nameSetToList tycl_names) of
198                 []     -> Nothing
199                 (n:ns) -> Just (getOccName n)
200
201 mkImportedInstance :: Name -> [Maybe Name] -> Maybe OccName
202                    -> DFunId -> OverlapFlag -> Instance
203 -- Used for imported instances, where we get the rough-match stuff
204 -- from the interface file
205 mkImportedInstance cls mb_tcs orph dfun oflag
206   = Instance {  is_flag = oflag, is_dfun = dfun,
207                 is_tvs = mkVarSet tvs, is_tys = tys,
208                 is_cls = cls, is_tcs = mb_tcs, is_orph = orph }
209   where
210     (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
211
212 roughMatchTcs :: [Type] -> [Maybe Name]
213 roughMatchTcs tys = map rough tys
214   where
215     rough ty = case tcSplitTyConApp_maybe ty of
216                   Just (tc,_) -> Just (tyConName tc)
217                   Nothing     -> Nothing
218
219 instanceCantMatch :: [Maybe Name] -> [Maybe Name] -> Bool
220 -- (instanceCantMatch tcs1 tcs2) returns True if tcs1 cannot
221 -- possibly be instantiated to actual, nor vice versa; 
222 -- False is non-committal
223 instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
224 instanceCantMatch ts            as            =  False  -- Safe
225 \end{code}
226
227
228 Note [Overlapping instances]
229 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
230 Overlap is permitted, but only in such a way that one can make
231 a unique choice when looking up.  That is, overlap is only permitted if
232 one template matches the other, or vice versa.  So this is ok:
233
234   [a]  [Int]
235
236 but this is not
237
238   (Int,a)  (b,Int)
239
240 If overlap is permitted, the list is kept most specific first, so that
241 the first lookup is the right choice.
242
243
244 For now we just use association lists.
245
246 \subsection{Avoiding a problem with overlapping}
247
248 Consider this little program:
249
250 \begin{pseudocode}
251      class C a        where c :: a
252      class C a => D a where d :: a
253
254      instance C Int where c = 17
255      instance D Int where d = 13
256
257      instance C a => C [a] where c = [c]
258      instance ({- C [a], -} D a) => D [a] where d = c
259
260      instance C [Int] where c = [37]
261
262      main = print (d :: [Int])
263 \end{pseudocode}
264
265 What do you think `main' prints  (assuming we have overlapping instances, and
266 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
267 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
268 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
269 the `C [Int]' instance is more specific).
270
271 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
272 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
273 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
274 doesn't even compile!  What's going on!?
275
276 What hugs complains about is the `D [a]' instance decl.
277
278 \begin{pseudocode}
279      ERROR "mj.hs" (line 10): Cannot build superclass instance
280      *** Instance            : D [a]
281      *** Context supplied    : D a
282      *** Required superclass : C [a]
283 \end{pseudocode}
284
285 You might wonder what hugs is complaining about.  It's saying that you
286 need to add `C [a]' to the context of the `D [a]' instance (as appears
287 in comments).  But there's that `C [a]' instance decl one line above
288 that says that I can reduce the need for a `C [a]' instance to the
289 need for a `C a' instance, and in this case, I already have the
290 necessary `C a' instance (since we have `D a' explicitly in the
291 context, and `C' is a superclass of `D').
292
293 Unfortunately, the above reasoning indicates a premature commitment to the
294 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
295 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
296 add the context that hugs suggests (uncomment the `C [a]'), effectively
297 deferring the decision about which instance to use.
298
299 Now, interestingly enough, 4.04 has this same bug, but it's covered up
300 in this case by a little known `optimization' that was disabled in
301 4.06.  Ghc-4.04 silently inserts any missing superclass context into
302 an instance declaration.  In this case, it silently inserts the `C
303 [a]', and everything happens to work out.
304
305 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
306 `Mark Jones', although Mark claims no credit for the `optimization' in
307 question, and would rather it stopped being called the `Mark Jones
308 optimization' ;-)
309
310 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
311 something else out with ghc-4.04.  Let's add the following line:
312
313     d' :: D a => [a]
314     d' = c
315
316 Everyone raise their hand who thinks that `d :: [Int]' should give a
317 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
318 `optimization' only applies to instance decls, not to regular
319 bindings, giving inconsistent behavior.
320
321 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
322 list of instances for a given class is ordered, so that more specific
323 instances come before more generic ones.  For example, the instance
324 list for C might contain:
325     ..., C Int, ..., C a, ...  
326 When we go to look for a `C Int' instance we'll get that one first.
327 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
328 pass the `C Int' instance, and keep going.  But if `b' is
329 unconstrained, then we don't know yet if the more specific instance
330 will eventually apply.  GHC keeps going, and matches on the generic `C
331 a'.  The fix is to, at each step, check to see if there's a reverse
332 match, and if so, abort the search.  This prevents hugs from
333 prematurely chosing a generic instance when a more specific one
334 exists.
335
336 --Jeff
337
338 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
339 this test.  Suppose the instance envt had
340     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
341 (still most specific first)
342 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
343         C x y Int  doesn't match the template {a,b} C a a b
344 but neither does 
345         C a a b  match the template {x,y} C x y Int
346 But still x and y might subsequently be unified so they *do* match.
347
348 Simple story: unify, don't match.
349
350
351 %************************************************************************
352 %*                                                                      *
353                 InstEnv, ClsInstEnv
354 %*                                                                      *
355 %************************************************************************
356
357 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
358 ClsInstEnv mapping is the dfun for that instance.
359
360 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
361
362         forall a b, C t1 t2 t3  can be constructed by dfun
363
364 or, to put it another way, we have
365
366         instance (...) => C t1 t2 t3,  witnessed by dfun
367
368 \begin{code}
369 ---------------------------------------------------
370 type InstEnv = UniqFM ClsInstEnv        -- Maps Class to instances for that class
371
372 data ClsInstEnv 
373   = ClsIE [Instance]    -- The instances for a particular class, in any order
374           Bool          -- True <=> there is an instance of form C a b c
375                         --      If *not* then the common case of looking up
376                         --      (C a b c) can fail immediately
377
378 -- INVARIANTS:
379 --  * The is_tvs are distinct in each Instance
380 --      of a ClsInstEnv (so we can safely unify them)
381
382 -- Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
383 --      [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
384 -- The "a" in the pattern must be one of the forall'd variables in
385 -- the dfun type.
386
387 emptyInstEnv :: InstEnv
388 emptyInstEnv = emptyUFM
389
390 instEnvElts :: InstEnv -> [Instance]
391 instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
392
393 classInstances :: (InstEnv,InstEnv) -> Class -> [Instance]
394 classInstances (pkg_ie, home_ie) cls 
395   = get home_ie ++ get pkg_ie
396   where
397     get env = case lookupUFM env cls of
398                 Just (ClsIE insts _) -> insts
399                 Nothing              -> []
400
401 extendInstEnvList :: InstEnv -> [Instance] -> InstEnv
402 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
403
404 extendInstEnv :: InstEnv -> Instance -> InstEnv
405 extendInstEnv inst_env ins_item@(Instance { is_cls = cls_nm, is_tcs = mb_tcs })
406   = addToUFM_C add inst_env cls_nm (ClsIE [ins_item] ins_tyvar)
407   where
408     add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
409                                               (ins_tyvar || cur_tyvar)
410     ins_tyvar = not (any isJust mb_tcs)
411 \end{code}                    
412
413
414 %************************************************************************
415 %*                                                                      *
416 \subsection{Looking up an instance}
417 %*                                                                      *
418 %************************************************************************
419
420 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
421 the env is kept ordered, the first match must be the only one.  The
422 thing we are looking up can have an arbitrary "flexi" part.
423
424 \begin{code}
425 lookupInstEnv :: (InstEnv       -- External package inst-env
426                  ,InstEnv)      -- Home-package inst-env
427               -> Class -> [Type]                -- What we are looking for
428               -> ([(TvSubst, Instance)],        -- Successful matches
429                   [Instance])                   -- These don't match but do unify
430         -- The second component of the tuple happens when we look up
431         --      Foo [a]
432         -- in an InstEnv that has entries for
433         --      Foo [Int]
434         --      Foo [b]
435         -- Then which we choose would depend on the way in which 'a'
436         -- is instantiated.  So we report that Foo [b] is a match (mapping b->a)
437         -- but Foo [Int] is a unifier.  This gives the caller a better chance of
438         -- giving a suitable error messagen
439
440 lookupInstEnv (pkg_ie, home_ie) cls tys
441   = (pruned_matches, all_unifs)
442   where
443     rough_tcs  = roughMatchTcs tys
444     all_tvs    = all isNothing rough_tcs
445     (home_matches, home_unifs) = lookup home_ie 
446     (pkg_matches,  pkg_unifs)  = lookup pkg_ie  
447     all_matches = home_matches ++ pkg_matches
448     all_unifs   = home_unifs   ++ pkg_unifs
449     pruned_matches 
450         | null all_unifs = foldr insert_overlapping [] all_matches
451         | otherwise      = all_matches  -- Non-empty unifs is always an error situation,
452                                         -- so don't attempt to pune the matches
453
454     --------------
455     lookup env = case lookupUFM env cls of
456                    Nothing -> ([],[])   -- No instances for this class
457                    Just (ClsIE insts has_tv_insts)
458                         | all_tvs && not has_tv_insts
459                         -> ([],[])      -- Short cut for common case
460                         -- The thing we are looking up is of form (C a b c), and
461                         -- the ClsIE has no instances of that form, so don't bother to search
462         
463                         | otherwise
464                         -> find [] [] insts
465
466     --------------
467     find ms us [] = (ms, us)
468     find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs, 
469                                  is_tys = tpl_tys, is_flag = oflag,
470                                  is_dfun = dfun }) : rest)
471         -- Fast check for no match, uses the "rough match" fields
472       | instanceCantMatch rough_tcs mb_tcs
473       = find ms us rest
474
475       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
476       = find ((subst,item):ms) us rest
477
478         -- Does not match, so next check whether the things unify
479         -- See Note [overlapping instances] above
480       | Incoherent <- oflag
481       = find ms us rest
482
483       | otherwise
484       = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
485                  (ppr cls <+> ppr tys <+> ppr all_tvs) $$
486                  (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
487                 )
488                 -- Unification will break badly if the variables overlap
489                 -- They shouldn't because we allocate separate uniques for them
490         case tcUnifyTys bind_fn tpl_tys tys of
491             Just _   -> find ms (item:us) rest
492             Nothing  -> find ms us         rest
493
494 ---------------
495 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
496            | otherwise                             = BindMe
497         -- The key_tys can contain skolem constants, and we can guarantee that those
498         -- are never going to be instantiated to anything, so we should not involve
499         -- them in the unification test.  Example:
500         --      class Foo a where { op :: a -> Int }
501         --      instance Foo a => Foo [a]       -- NB overlap
502         --      instance Foo [Int]              -- NB overlap
503         --      data T = forall a. Foo a => MkT a
504         --      f :: T -> Int
505         --      f (MkT x) = op [x,x]
506         -- The op [x,x] means we need (Foo [a]).  Without the filterVarSet we'd
507         -- complain, saying that the choice of instance depended on the instantiation
508         -- of 'a'; but of course it isn't *going* to be instantiated.
509         --
510         -- We do this only for pattern-bound skolems.  For example we reject
511         --      g :: forall a => [a] -> Int
512         --      g x = op x
513         -- on the grounds that the correct instance depends on the instantiation of 'a'
514
515 ---------------
516 insert_overlapping :: (TvSubst, Instance) -> [(TvSubst, Instance)] 
517                    -> [(TvSubst, Instance)]
518 -- Add a new solution, knocking out strictly less specific ones
519 insert_overlapping new_item [] = [new_item]
520 insert_overlapping new_item (item:items)
521   | new_beats_old && old_beats_new = item : insert_overlapping new_item items
522         -- Duplicate => keep both for error report
523   | new_beats_old = insert_overlapping new_item items
524         -- Keep new one
525   | old_beats_new = item : items
526         -- Keep old one
527   | otherwise     = item : insert_overlapping new_item items
528         -- Keep both
529   where
530     new_beats_old = new_item `beats` item
531     old_beats_new = item `beats` new_item
532
533     (_, instA) `beats` (_, instB)
534         = overlap_ok && 
535           isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
536                 -- A beats B if A is more specific than B, and B admits overlap
537                 -- I.e. if B can be instantiated to match A
538         where
539           overlap_ok = case is_flag instB of
540                         NoOverlap -> False
541                         other     -> True
542 \end{code}
543