[project @ 2001-12-20 11:19:05 by simonpj]
[ghc-hetmet.git] / ghc / compiler / types / InstEnv.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4 \section[InstEnv]{Utilities for typechecking instance declarations}
5
6 The bits common to TcInstDcls and TcDeriv.
7
8 \begin{code}
9 module InstEnv (
10         DFunId, ClsInstEnv, InstEnv,
11
12         emptyInstEnv, extendInstEnv, pprInstEnv,
13         lookupInstEnv, InstLookupResult(..),
14         classInstEnv, simpleDFunClassTyCon
15     ) where
16
17 #include "HsVersions.h"
18
19 import Class            ( Class, classTvsFds )
20 import Var              ( TyVar, Id )
21 import VarSet
22 import VarEnv
23 import Maybes           ( MaybeErr(..), returnMaB, failMaB, thenMaB, maybeToBool )
24 import Name             ( getSrcLoc )
25 import TcType           ( Type, tcTyConAppTyCon, mkTyVarTy,
26                           tcSplitDFunTy, tyVarsOfTypes,
27                           matchTys, unifyTyListsX, allDistinctTyVars
28                         )
29 import PprType          ( pprClassPred )
30 import FunDeps          ( checkClsFD )
31 import TyCon            ( TyCon )
32 import Outputable
33 import UniqFM           ( UniqFM, lookupWithDefaultUFM, addToUFM, emptyUFM, eltsUFM )
34 import Id               ( idType )
35 import ErrUtils         ( Message )
36 import CmdLineOpts
37 \end{code}
38
39
40 %************************************************************************
41 %*                                                                      *
42 \subsection{The key types}
43 %*                                                                      *
44 %************************************************************************
45
46 \begin{code}
47 type DFunId     = Id
48
49 type InstEnv    = UniqFM ClsInstEnv             -- Maps Class to instances for that class
50
51 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
52 simpleDFunClassTyCon dfun
53   = (clas, tycon)
54   where
55     (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
56     tycon           = tcTyConAppTyCon ty 
57
58 pprInstEnv :: InstEnv -> SDoc
59 pprInstEnv env
60   = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+> 
61            brackets (pprWithCommas ppr tys) <+> ppr dfun
62          | cls_inst_env <-  eltsUFM env
63          , (tyvars, tys, dfun) <- cls_inst_env
64          ]
65 \end{code}                    
66
67 %************************************************************************
68 %*                                                                      *
69 \subsection{Instance environments: InstEnv and ClsInstEnv}
70 %*                                                                      *
71 %************************************************************************
72
73 \begin{code}
74 type ClsInstEnv = [(TyVarSet, [Type], DFunId)]  -- The instances for a particular class
75         -- INVARIANTs: see notes below
76
77 emptyInstEnv :: InstEnv
78 emptyInstEnv = emptyUFM
79
80 classInstEnv :: InstEnv -> Class -> ClsInstEnv
81 classInstEnv env cls = lookupWithDefaultUFM env [] cls
82 \end{code}
83
84 A @ClsInstEnv@ all the instances of that class.  The @Id@ inside a
85 ClsInstEnv mapping is the dfun for that instance.
86
87 If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
88
89         forall a b, C t1 t2 t3  can be constructed by dfun
90
91 or, to put it another way, we have
92
93         instance (...) => C t1 t2 t3,  witnessed by dfun
94
95 There is an important consistency constraint in the elements of a ClsInstEnv:
96
97   * [a,b] must be a superset of the free vars of [t1,t2,t3]
98
99   * The dfun must itself be quantified over [a,b]
100  
101   * More specific instances come before less specific ones,
102     where they overlap
103
104 Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
105         [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
106 The "a" in the pattern must be one of the forall'd variables in
107 the dfun type.
108
109
110
111 Notes on overlapping instances
112 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
113 In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
114
115 In others, overlap is permitted, but only in such a way that one can make
116 a unique choice when looking up.  That is, overlap is only permitted if
117 one template matches the other, or vice versa.  So this is ok:
118
119   [a]  [Int]
120
121 but this is not
122
123   (Int,a)  (b,Int)
124
125 If overlap is permitted, the list is kept most specific first, so that
126 the first lookup is the right choice.
127
128
129 For now we just use association lists.
130
131 \subsection{Avoiding a problem with overlapping}
132
133 Consider this little program:
134
135 \begin{pseudocode}
136      class C a        where c :: a
137      class C a => D a where d :: a
138
139      instance C Int where c = 17
140      instance D Int where d = 13
141
142      instance C a => C [a] where c = [c]
143      instance ({- C [a], -} D a) => D [a] where d = c
144
145      instance C [Int] where c = [37]
146
147      main = print (d :: [Int])
148 \end{pseudocode}
149
150 What do you think `main' prints  (assuming we have overlapping instances, and
151 all that turned on)?  Well, the instance for `D' at type `[a]' is defined to
152 be `c' at the same type, and we've got an instance of `C' at `[Int]', so the
153 answer is `[37]', right? (the generic `C [a]' instance shouldn't apply because
154 the `C [Int]' instance is more specific).
155
156 Ghc-4.04 gives `[37]', while ghc-4.06 gives `[17]', so 4.06 is wrong.  That
157 was easy ;-)  Let's just consult hugs for good measure.  Wait - if I use old
158 hugs (pre-September99), I get `[17]', and stranger yet, if I use hugs98, it
159 doesn't even compile!  What's going on!?
160
161 What hugs complains about is the `D [a]' instance decl.
162
163 \begin{pseudocode}
164      ERROR "mj.hs" (line 10): Cannot build superclass instance
165      *** Instance            : D [a]
166      *** Context supplied    : D a
167      *** Required superclass : C [a]
168 \end{pseudocode}
169
170 You might wonder what hugs is complaining about.  It's saying that you
171 need to add `C [a]' to the context of the `D [a]' instance (as appears
172 in comments).  But there's that `C [a]' instance decl one line above
173 that says that I can reduce the need for a `C [a]' instance to the
174 need for a `C a' instance, and in this case, I already have the
175 necessary `C a' instance (since we have `D a' explicitly in the
176 context, and `C' is a superclass of `D').
177
178 Unfortunately, the above reasoning indicates a premature commitment to the
179 generic `C [a]' instance.  I.e., it prematurely rules out the more specific
180 instance `C [Int]'.  This is the mistake that ghc-4.06 makes.  The fix is to
181 add the context that hugs suggests (uncomment the `C [a]'), effectively
182 deferring the decision about which instance to use.
183
184 Now, interestingly enough, 4.04 has this same bug, but it's covered up
185 in this case by a little known `optimization' that was disabled in
186 4.06.  Ghc-4.04 silently inserts any missing superclass context into
187 an instance declaration.  In this case, it silently inserts the `C
188 [a]', and everything happens to work out.
189
190 (See `basicTypes/MkId:mkDictFunId' for the code in question.  Search for
191 `Mark Jones', although Mark claims no credit for the `optimization' in
192 question, and would rather it stopped being called the `Mark Jones
193 optimization' ;-)
194
195 So, what's the fix?  I think hugs has it right.  Here's why.  Let's try
196 something else out with ghc-4.04.  Let's add the following line:
197
198     d' :: D a => [a]
199     d' = c
200
201 Everyone raise their hand who thinks that `d :: [Int]' should give a
202 different answer from `d' :: [Int]'.  Well, in ghc-4.04, it does.  The
203 `optimization' only applies to instance decls, not to regular
204 bindings, giving inconsistent behavior.
205
206 Old hugs had this same bug.  Here's how we fixed it: like GHC, the
207 list of instances for a given class is ordered, so that more specific
208 instances come before more generic ones.  For example, the instance
209 list for C might contain:
210     ..., C Int, ..., C a, ...  
211 When we go to look for a `C Int' instance we'll get that one first.
212 But what if we go looking for a `C b' (`b' is unconstrained)?  We'll
213 pass the `C Int' instance, and keep going.  But if `b' is
214 unconstrained, then we don't know yet if the more specific instance
215 will eventually apply.  GHC keeps going, and matches on the generic `C
216 a'.  The fix is to, at each step, check to see if there's a reverse
217 match, and if so, abort the search.  This prevents hugs from
218 prematurely chosing a generic instance when a more specific one
219 exists.
220
221 --Jeff
222
223 BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
224 this test.  Suppose the instance envt had
225     ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
226 (still most specific first)
227 Now suppose we are looking for (C x y Int), where x and y are unconstrained.
228         C x y Int  doesn't match the template {a,b} C a a b
229 but neither does 
230         C a a b  match the template {x,y} C x y Int
231 But still x and y might subsequently be unified so they *do* match.
232
233 Simple story: unify, don't match.
234
235
236 %************************************************************************
237 %*                                                                      *
238 \subsection{Looking up an instance}
239 %*                                                                      *
240 %************************************************************************
241
242 @lookupInstEnv@ looks up in a @InstEnv@, using a one-way match.  Since
243 the env is kept ordered, the first match must be the only one.  The
244 thing we are looking up can have an arbitrary "flexi" part.
245
246 \begin{code}
247 lookupInstEnv :: DynFlags
248               -> InstEnv                -- The envt
249               -> Class -> [Type]        -- What we are looking for
250               -> InstLookupResult
251
252 data InstLookupResult 
253   = FoundInst                   -- There is a (template,substitution) pair 
254                                 -- that makes the template match the key, 
255                                 -- and no template is an instance of the key
256         TyVarSubstEnv Id
257
258   | NoMatch Bool        -- Boolean is true iff there is at least one
259                         -- template that matches the key.
260                         -- (but there are other template(s) that are
261                         --  instances of the key, so we don't report 
262                         --  FoundInst)
263         -- The NoMatch True case happens when we look up
264         --      Foo [a]
265         -- in an InstEnv that has entries for
266         --      Foo [Int]
267         --      Foo [b]
268         -- Then which we choose would depend on the way in which 'a'
269         -- is instantiated.  So we say there is no match, but identify
270         -- it as ambiguous case in the hope of giving a better error msg.
271         -- See the notes above from Jeff Lewis
272
273 lookupInstEnv dflags env key_cls key_tys
274   = find (classInstEnv env key_cls)
275   where
276     key_vars = tyVarsOfTypes key_tys
277
278     find [] = NoMatch False
279     find ((tpl_tyvars, tpl, dfun_id) : rest)
280       = case matchTys tpl_tyvars tpl key_tys of
281           Nothing                 ->
282                 -- Check whether the things unify, so that
283                 -- we bale out if a later instantiation of this
284                 -- predicate might match this instance
285                 -- [see notes about overlapping instances above]
286             case unifyTyListsX (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
287               Just _ | not (dopt Opt_AllowIncoherentInstances dflags)
288                      -> NoMatch (any_match rest)
289                 -- If we allow incoherent instances we don't worry about the 
290                 -- test and just blaze on anyhow.  Requested by John Hughes.
291               other  -> find rest
292
293           Just (subst, leftovers) -> ASSERT( null leftovers )
294                                      FoundInst subst dfun_id
295
296     any_match rest = or [ maybeToBool (matchTys tvs tpl key_tys)
297                         | (tvs,tpl,_) <- rest
298                         ]
299 \end{code}
300
301
302 %************************************************************************
303 %*                                                                      *
304 \subsection{Extending an instance environment}
305 %*                                                                      *
306 %************************************************************************
307
308 @extendInstEnv@ extends a @ClsInstEnv@, checking for overlaps.
309
310 A boolean flag controls overlap reporting.
311
312 True => overlap is permitted, but only if one template matches the other;
313         not if they unify but neither is 
314
315 \begin{code}
316 extendInstEnv :: DynFlags -> InstEnv -> [DFunId] -> (InstEnv, [Message])
317   -- Similar, but all we have is the DFuns
318 extendInstEnv dflags env dfun_ids = foldl (addToInstEnv dflags) (env, []) dfun_ids
319
320
321 addToInstEnv :: DynFlags
322              -> (InstEnv, [Message])
323              -> DFunId
324              -> (InstEnv, [Message])    -- Resulting InstEnv and augmented error messages
325
326 addToInstEnv dflags (inst_env, errs) dfun_id
327         -- Check first that the new instance doesn't 
328         -- conflict with another.  See notes below about fundeps.
329   | not (null bad_fundeps)
330   = (inst_env, fundep_err : errs)               -- Bad fundeps; report the first only
331
332   | otherwise
333   = case insert_into cls_inst_env of 
334         Failed err        -> (inst_env, err : errs)
335         Succeeded new_env -> (addToUFM inst_env clas new_env, errs)
336
337   where
338     cls_inst_env = classInstEnv inst_env clas
339     (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
340     bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
341     fundep_err  = fundepErr dfun_id (head bad_fundeps)
342
343     ins_tv_set = mkVarSet ins_tvs
344     ins_item   = (ins_tv_set, ins_tys, dfun_id)
345
346     insert_into [] = returnMaB [ins_item]
347     insert_into env@(cur_item@(tpl_tvs, tpl_tys, tpl_dfun_id) : rest)
348       = case unifyTyListsX (ins_tv_set `unionVarSet` tpl_tvs) tpl_tys ins_tys of
349           Just subst -> insert_unifiable env subst
350           Nothing    -> carry_on cur_item rest
351
352     carry_on cur_item rest = insert_into rest     `thenMaB` \ rest' ->
353                              returnMaB (cur_item : rest')
354
355             -- The two templates unify.  This is acceptable iff
356             -- (a) -fallow-overlapping-instances is on
357             -- (b) one is strictly more specific than the other
358             -- [It's bad if they are identical or incomparable]
359     insert_unifiable env@(cur_item@(tpl_tvs, tpl_tys, tpl_dfun_id) : rest) subst
360       |  ins_item_more_specific && cur_item_more_specific
361       =         -- Duplicates
362         failMaB (dupInstErr dfun_id tpl_dfun_id)
363
364       |  not (dopt Opt_AllowOverlappingInstances dflags)
365       || not (ins_item_more_specific || cur_item_more_specific)
366       =         -- Overlap illegal, or the two are incomparable
367          failMaB (overlapErr dfun_id tpl_dfun_id)
368          
369       | otherwise
370       =         -- OK, it's acceptable.  Remaining question is whether
371                 -- we drop it here or compare it with others
372         if ins_item_more_specific then
373                 -- New item is an instance of current item, so drop it here
374             returnMaB (ins_item : env)
375         else
376             carry_on cur_item rest
377
378       where
379         ins_item_more_specific = allVars subst ins_tvs
380         cur_item_more_specific = allVars subst (varSetElems tpl_tvs)
381
382 allVars :: TyVarSubstEnv -> [TyVar] -> Bool
383 -- True iff all the type vars are mapped to distinct type vars
384 allVars subst tvs
385   = allDistinctTyVars (map lookup tvs) emptyVarSet
386   where
387     lookup tv = case lookupSubstEnv subst tv of
388                   Just (DoneTy ty) -> ty
389                   Nothing          -> mkTyVarTy tv
390 \end{code}
391
392 Functional dependencies
393 ~~~~~~~~~~~~~~~~~~~~~~~
394 Here is the bad case:
395         class C a b | a->b where ...
396         instance C Int Bool where ...
397         instance C Int Char where ...
398
399 The point is that a->b, so Int in the first parameter must uniquely
400 determine the second.  In general, given the same class decl, and given
401
402         instance C s1 s2 where ...
403         instance C t1 t2 where ...
404
405 Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
406
407 Matters are a little more complicated if there are free variables in
408 the s2/t2.  
409
410         class D a b c | a -> b
411         instance D a b => D [(a,a)] [b] Int
412         instance D a b => D [a]     [b] Bool
413
414 The instance decls don't overlap, because the third parameter keeps
415 them separate.  But we want to make sure that given any constraint
416         D s1 s2 s3
417 if s1 matches 
418
419
420
421
422 \begin{code}
423 badFunDeps :: ClsInstEnv -> Class
424            -> TyVarSet -> [Type]        -- Proposed new instance type
425            -> [DFunId]
426 badFunDeps cls_inst_env clas ins_tv_set ins_tys 
427   = [ dfun_id | fd <- fds,
428                (tvs, tys, dfun_id) <- cls_inst_env,
429                not (null (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys))
430     ]
431   where
432     (clas_tvs, fds) = classTvsFds clas
433 \end{code}
434
435
436 \begin{code}
437 dupInstErr dfun1 dfun2 = addInstErr (ptext SLIT("Duplicate instance declarations:"))  dfun1 dfun2
438 overlapErr dfun1 dfun2 = addInstErr (ptext SLIT("Overlapping instance declarations:")) dfun1 dfun2
439 fundepErr  dfun1 dfun2 = addInstErr (ptext SLIT("Functional dependencies conflict between instance declarations:")) 
440                                     dfun1 dfun2
441
442 addInstErr what dfun1 dfun2 
443  = hang what 2 (ppr_dfun dfun1 $$ ppr_dfun dfun2)
444   where
445     ppr_dfun dfun = ppr (getSrcLoc dfun) <> colon <+> pprClassPred clas tys
446                   where
447                     (_,_,clas,tys) = tcSplitDFunTy (idType dfun)
448 \end{code}