2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
14 tcSimplifyDeriv, tcSimplifyDefault,
18 #include "HsVersions.h"
20 import {-# SOURCE #-} TcUnify( unifyTauTy )
22 import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
23 import TcHsSyn ( TcExpr, TcId,
24 TcMonoBinds, TcDictBinds
28 import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
29 tyVarsOfInst, predsOfInsts, predsOfInst, newDicts,
30 isDict, isClassDict, isLinearInst, linearInstType,
31 isStdClassTyVarDict, isMethodFor, isMethod,
32 instToId, tyVarsOfInsts, cloneDict,
33 ipNamesOfInsts, ipNamesOfInst, dictPred,
34 instBindingRequired, instCanBeGeneralised,
35 newDictsFromOld, newMethodAtLoc,
36 getDictClassTys, isTyVarDict,
37 instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
38 Inst, LIE, pprInsts, pprInstsInFull,
41 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupGlobalId )
42 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
43 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
44 import TcType ( TcTyVar, TcTyVarSet, ThetaType, PredType,
45 mkClassPred, isOverloadedTy, mkTyConApp,
46 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
47 tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
48 inheritablePred, predHasFDs )
49 import Id ( idType, mkUserLocal )
51 import Name ( getOccName, getSrcLoc )
52 import NameSet ( NameSet, mkNameSet, elemNameSet )
53 import Class ( classBigSig )
54 import FunDeps ( oclose, grow, improve, pprEquationDoc )
55 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass,
56 splitIdName, fstIdName, sndIdName )
58 import Subst ( mkTopTyVarSubst, substTheta, substTy )
59 import TysWiredIn ( unitTy, pairTyCon )
63 import ListSetOps ( equivClasses )
64 import Util ( zipEqual )
65 import List ( partition )
70 %************************************************************************
74 %************************************************************************
76 --------------------------------------
77 Notes on quantification
78 --------------------------------------
80 Suppose we are about to do a generalisation step.
85 C the constraints from that RHS
87 The game is to figure out
89 Q the set of type variables over which to quantify
90 Ct the constraints we will *not* quantify over
91 Cq the constraints we will quantify over
93 So we're going to infer the type
97 and float the constraints Ct further outwards.
99 Here are the things that *must* be true:
101 (A) Q intersect fv(G) = EMPTY limits how big Q can be
102 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
104 (A) says we can't quantify over a variable that's free in the
105 environment. (B) says we must quantify over all the truly free
106 variables in T, else we won't get a sufficiently general type. We do
107 not *need* to quantify over any variable that is fixed by the free
108 vars of the environment G.
110 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
112 Example: class H x y | x->y where ...
114 fv(G) = {a} C = {H a b, H c d}
117 (A) Q intersect {a} is empty
118 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
120 So Q can be {c,d}, {b,c,d}
122 Other things being equal, however, we'd like to quantify over as few
123 variables as possible: smaller types, fewer type applications, more
124 constraints can get into Ct instead of Cq.
127 -----------------------------------------
130 fv(T) the free type vars of T
132 oclose(vs,C) The result of extending the set of tyvars vs
133 using the functional dependencies from C
135 grow(vs,C) The result of extend the set of tyvars vs
136 using all conceivable links from C.
138 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
139 Then grow(vs,C) = {a,b,c}
141 Note that grow(vs,C) `superset` grow(vs,simplify(C))
142 That is, simplfication can only shrink the result of grow.
145 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
146 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
149 -----------------------------------------
153 Here's a good way to choose Q:
155 Q = grow( fv(T), C ) \ oclose( fv(G), C )
157 That is, quantify over all variable that that MIGHT be fixed by the
158 call site (which influences T), but which aren't DEFINITELY fixed by
159 G. This choice definitely quantifies over enough type variables,
160 albeit perhaps too many.
162 Why grow( fv(T), C ) rather than fv(T)? Consider
164 class H x y | x->y where ...
169 If we used fv(T) = {c} we'd get the type
171 forall c. H c d => c -> b
173 And then if the fn was called at several different c's, each of
174 which fixed d differently, we'd get a unification error, because
175 d isn't quantified. Solution: quantify d. So we must quantify
176 everything that might be influenced by c.
178 Why not oclose( fv(T), C )? Because we might not be able to see
179 all the functional dependencies yet:
181 class H x y | x->y where ...
182 instance H x y => Eq (T x y) where ...
187 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
188 apparent yet, and that's wrong. We must really quantify over d too.
191 There really isn't any point in quantifying over any more than
192 grow( fv(T), C ), because the call sites can't possibly influence
193 any other type variables.
197 --------------------------------------
199 --------------------------------------
201 It's very hard to be certain when a type is ambiguous. Consider
205 instance H x y => K (x,y)
207 Is this type ambiguous?
208 forall a b. (K (a,b), Eq b) => a -> a
210 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
211 now we see that a fixes b. So we can't tell about ambiguity for sure
212 without doing a full simplification. And even that isn't possible if
213 the context has some free vars that may get unified. Urgle!
215 Here's another example: is this ambiguous?
216 forall a b. Eq (T b) => a -> a
217 Not if there's an insance decl (with no context)
218 instance Eq (T b) where ...
220 You may say of this example that we should use the instance decl right
221 away, but you can't always do that:
223 class J a b where ...
224 instance J Int b where ...
226 f :: forall a b. J a b => a -> a
228 (Notice: no functional dependency in J's class decl.)
229 Here f's type is perfectly fine, provided f is only called at Int.
230 It's premature to complain when meeting f's signature, or even
231 when inferring a type for f.
235 However, we don't *need* to report ambiguity right away. It'll always
236 show up at the call site.... and eventually at main, which needs special
237 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
239 So here's the plan. We WARN about probable ambiguity if
241 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
243 (all tested before quantification).
244 That is, all the type variables in Cq must be fixed by the the variables
245 in the environment, or by the variables in the type.
247 Notice that we union before calling oclose. Here's an example:
249 class J a b c | a b -> c
253 forall b c. (J a b c) => b -> b
255 Only if we union {a} from G with {b} from T before using oclose,
256 do we see that c is fixed.
258 It's a bit vague exactly which C we should use for this oclose call. If we
259 don't fix enough variables we might complain when we shouldn't (see
260 the above nasty example). Nothing will be perfect. That's why we can
261 only issue a warning.
264 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
266 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
268 then c is a "bubble"; there's no way it can ever improve, and it's
269 certainly ambiguous. UNLESS it is a constant (sigh). And what about
274 instance H x y => K (x,y)
276 Is this type ambiguous?
277 forall a b. (K (a,b), Eq b) => a -> a
279 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
280 is a "bubble" that's a set of constraints
282 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
284 Hence another idea. To decide Q start with fv(T) and grow it
285 by transitive closure in Cq (no functional dependencies involved).
286 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
287 The definitely-ambiguous can then float out, and get smashed at top level
288 (which squashes out the constants, like Eq (T a) above)
291 --------------------------------------
292 Notes on principal types
293 --------------------------------------
298 f x = let g y = op (y::Int) in True
300 Here the principal type of f is (forall a. a->a)
301 but we'll produce the non-principal type
302 f :: forall a. C Int => a -> a
305 --------------------------------------
306 Notes on implicit parameters
307 --------------------------------------
309 Question 1: can we "inherit" implicit parameters
310 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
315 where f is *not* a top-level binding.
316 From the RHS of f we'll get the constraint (?y::Int).
317 There are two types we might infer for f:
321 (so we get ?y from the context of f's definition), or
323 f :: (?y::Int) => Int -> Int
325 At first you might think the first was better, becuase then
326 ?y behaves like a free variable of the definition, rather than
327 having to be passed at each call site. But of course, the WHOLE
328 IDEA is that ?y should be passed at each call site (that's what
329 dynamic binding means) so we'd better infer the second.
331 BOTTOM LINE: when *inferring types* you *must* quantify
332 over implicit parameters. See the predicate isFreeWhenInferring.
335 Question 2: type signatures
336 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
337 BUT WATCH OUT: When you supply a type signature, we can't force you
338 to quantify over implicit parameters. For example:
342 This is perfectly reasonable. We do not want to insist on
344 (?x + 1) :: (?x::Int => Int)
346 That would be silly. Here, the definition site *is* the occurrence site,
347 so the above strictures don't apply. Hence the difference between
348 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
349 and tcSimplifyCheckBind (which does not).
351 What about when you supply a type signature for a binding?
352 Is it legal to give the following explicit, user type
353 signature to f, thus:
358 At first sight this seems reasonable, but it has the nasty property
359 that adding a type signature changes the dynamic semantics.
362 (let f x = (x::Int) + ?y
363 in (f 3, f 3 with ?y=5)) with ?y = 6
369 in (f 3, f 3 with ?y=5)) with ?y = 6
373 Indeed, simply inlining f (at the Haskell source level) would change the
376 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
377 semantics for a Haskell program without knowing its typing, so if you
378 change the typing you may change the semantics.
380 To make things consistent in all cases where we are *checking* against
381 a supplied signature (as opposed to inferring a type), we adopt the
384 a signature does not need to quantify over implicit params.
386 [This represents a (rather marginal) change of policy since GHC 5.02,
387 which *required* an explicit signature to quantify over all implicit
388 params for the reasons mentioned above.]
390 But that raises a new question. Consider
392 Given (signature) ?x::Int
393 Wanted (inferred) ?x::Int, ?y::Bool
395 Clearly we want to discharge the ?x and float the ?y out. But
396 what is the criterion that distinguishes them? Clearly it isn't
397 what free type variables they have. The Right Thing seems to be
398 to float a constraint that
399 neither mentions any of the quantified type variables
400 nor any of the quantified implicit parameters
402 See the predicate isFreeWhenChecking.
405 Question 3: monomorphism
406 ~~~~~~~~~~~~~~~~~~~~~~~~
407 There's a nasty corner case when the monomorphism restriction bites:
411 The argument above suggests that we *must* generalise
412 over the ?y parameter, to get
413 z :: (?y::Int) => Int,
414 but the monomorphism restriction says that we *must not*, giving
416 Why does the momomorphism restriction say this? Because if you have
418 let z = x + ?y in z+z
420 you might not expect the addition to be done twice --- but it will if
421 we follow the argument of Question 2 and generalise over ?y.
427 (A) Always generalise over implicit parameters
428 Bindings that fall under the monomorphism restriction can't
432 * Inlining remains valid
433 * No unexpected loss of sharing
434 * But simple bindings like
436 will be rejected, unless you add an explicit type signature
437 (to avoid the monomorphism restriction)
438 z :: (?y::Int) => Int
440 This seems unacceptable
442 (B) Monomorphism restriction "wins"
443 Bindings that fall under the monomorphism restriction can't
445 Always generalise over implicit parameters *except* for bindings
446 that fall under the monomorphism restriction
449 * Inlining isn't valid in general
450 * No unexpected loss of sharing
451 * Simple bindings like
453 accepted (get value of ?y from binding site)
455 (C) Always generalise over implicit parameters
456 Bindings that fall under the monomorphism restriction can't
457 be generalised, EXCEPT for implicit parameters
459 * Inlining remains valid
460 * Unexpected loss of sharing (from the extra generalisation)
461 * Simple bindings like
463 accepted (get value of ?y from occurrence sites)
468 None of these choices seems very satisfactory. But at least we should
469 decide which we want to do.
471 It's really not clear what is the Right Thing To Do. If you see
475 would you expect the value of ?y to be got from the *occurrence sites*
476 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
477 case of function definitions, the answer is clearly the former, but
478 less so in the case of non-fucntion definitions. On the other hand,
479 if we say that we get the value of ?y from the definition site of 'z',
480 then inlining 'z' might change the semantics of the program.
482 Choice (C) really says "the monomorphism restriction doesn't apply
483 to implicit parameters". Which is fine, but remember that every
484 innocent binding 'x = ...' that mentions an implicit parameter in
485 the RHS becomes a *function* of that parameter, called at each
486 use of 'x'. Now, the chances are that there are no intervening 'with'
487 clauses that bind ?y, so a decent compiler should common up all
488 those function calls. So I think I strongly favour (C). Indeed,
489 one could make a similar argument for abolishing the monomorphism
490 restriction altogether.
492 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
496 %************************************************************************
498 \subsection{tcSimplifyInfer}
500 %************************************************************************
502 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
504 1. Compute Q = grow( fvs(T), C )
506 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
507 predicates will end up in Ct; we deal with them at the top level
509 3. Try improvement, using functional dependencies
511 4. If Step 3 did any unification, repeat from step 1
512 (Unification can change the result of 'grow'.)
514 Note: we don't reduce dictionaries in step 2. For example, if we have
515 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
516 after step 2. However note that we may therefore quantify over more
517 type variables than we absolutely have to.
519 For the guts, we need a loop, that alternates context reduction and
520 improvement with unification. E.g. Suppose we have
522 class C x y | x->y where ...
524 and tcSimplify is called with:
526 Then improvement unifies a with b, giving
529 If we need to unify anything, we rattle round the whole thing all over
536 -> TcTyVarSet -- fv(T); type vars
538 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
540 TcDictBinds, -- Bindings
541 [TcId]) -- Dict Ids that must be bound here (zonked)
546 tcSimplifyInfer doc tau_tvs wanted_lie
547 = inferLoop doc (varSetElems tau_tvs)
548 (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
550 -- Check for non-generalisable insts
551 mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
553 returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
555 inferLoop doc tau_tvs wanteds
557 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
558 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
559 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
561 preds = predsOfInsts wanteds'
562 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
565 | isFreeWhenInferring qtvs inst = Free
566 | isClassDict inst = DontReduceUnlessConstant -- Dicts
567 | otherwise = ReduceMe -- Lits and Methods
570 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
573 if no_improvement then
574 returnTc (varSetElems qtvs, frees, binds, irreds)
576 -- If improvement did some unification, we go round again. There
577 -- are two subtleties:
578 -- a) We start again with irreds, not wanteds
579 -- Using an instance decl might have introduced a fresh type variable
580 -- which might have been unified, so we'd get an infinite loop
581 -- if we started again with wanteds! See example [LOOP]
583 -- b) It's also essential to re-process frees, because unification
584 -- might mean that a type variable that looked free isn't now.
586 -- Hence the (irreds ++ frees)
588 -- However, NOTICE that when we are done, we might have some bindings, but
589 -- the final qtvs might be empty. See [NO TYVARS] below.
591 inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
592 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
597 class If b t e r | b t e -> r
600 class Lte a b c | a b -> c where lte :: a -> b -> c
602 instance (Lte a b l,If l b a c) => Max a b c
604 Wanted: Max Z (S x) y
606 Then we'll reduce using the Max instance to:
607 (Lte Z (S x) l, If l (S x) Z y)
608 and improve by binding l->T, after which we can do some reduction
609 on both the Lte and If constraints. What we *can't* do is start again
610 with (Max Z (S x) y)!
614 class Y a b | a -> b where
617 instance Y [[a]] a where
620 k :: X a -> X a -> X a
622 g :: Num a => [X a] -> [X a]
625 h ys = ys ++ map (k (y [[0]])) xs
627 The excitement comes when simplifying the bindings for h. Initially
628 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
629 From this we get t1:=:t2, but also various bindings. We can't forget
630 the bindings (because of [LOOP]), but in fact t1 is what g is
633 The net effect of [NO TYVARS]
636 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
637 isFreeWhenInferring qtvs inst
638 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
639 && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
640 -- (see "Notes on implicit parameters")
642 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
643 -> NameSet -- Quantified implicit parameters
645 isFreeWhenChecking qtvs ips inst
646 = isFreeWrtTyVars qtvs inst
647 && isFreeWrtIPs ips inst
649 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
650 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
654 %************************************************************************
656 \subsection{tcSimplifyCheck}
658 %************************************************************************
660 @tcSimplifyCheck@ is used when we know exactly the set of variables
661 we are going to quantify over. For example, a class or instance declaration.
666 -> [TcTyVar] -- Quantify over these
670 TcDictBinds) -- Bindings
672 -- tcSimplifyCheck is used when checking expression type signatures,
673 -- class decls, instance decls etc.
674 -- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
675 -- It's important that we can float out non-inheritable predicates
676 -- Example: (?x :: Int) is ok!
677 tcSimplifyCheck doc qtvs givens wanted_lie
678 = tcSimplCheck doc get_qtvs
679 givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
680 returnTc (frees, binds)
682 get_qtvs = zonkTcTyVarsAndFV qtvs
685 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
686 -- against, but we don't know the type variables over which we are going to quantify.
687 -- This happens when we have a type signature for a mutually recursive group
690 -> TcTyVarSet -- fv(T)
693 -> TcM ([TcTyVar], -- Variables over which to quantify
695 TcDictBinds) -- Bindings
697 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
698 = tcSimplCheck doc get_qtvs givens wanted_lie
700 -- Figure out which type variables to quantify over
701 -- You might think it should just be the signature tyvars,
702 -- but in bizarre cases you can get extra ones
703 -- f :: forall a. Num a => a -> a
704 -- f x = fst (g (x, head [])) + 1
706 -- Here we infer g :: forall a b. a -> b -> (b,a)
707 -- We don't want g to be monomorphic in b just because
708 -- f isn't quantified over b.
709 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
711 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenNF_Tc` \ all_tvs' ->
712 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
714 qtvs = all_tvs' `minusVarSet` gbl_tvs
715 -- We could close gbl_tvs, but its not necessary for
716 -- soundness, and it'll only affect which tyvars, not which
717 -- dictionaries, we quantify over
722 Here is the workhorse function for all three wrappers.
725 tcSimplCheck doc get_qtvs givens wanted_lie
726 = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
728 -- Complain about any irreducible ones
729 complainCheck doc givens irreds `thenNF_Tc_`
732 returnTc (qtvs, mkLIE frees, binds)
735 ip_set = mkNameSet (ipNamesOfInsts givens)
737 check_loop givens wanteds
739 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
740 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
741 get_qtvs `thenNF_Tc` \ qtvs' ->
745 -- When checking against a given signature we always reduce
746 -- until we find a match against something given, or can't reduce
747 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
748 | otherwise = ReduceMe
750 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
753 if no_improvement then
754 returnTc (varSetElems qtvs', frees, binds, irreds)
756 check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
757 returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
761 %************************************************************************
763 \subsection{tcSimplifyRestricted}
765 %************************************************************************
768 tcSimplifyRestricted -- Used for restricted binding groups
769 -- i.e. ones subject to the monomorphism restriction
771 -> TcTyVarSet -- Free in the type of the RHSs
772 -> LIE -- Free in the RHSs
773 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
775 TcDictBinds) -- Bindings
777 tcSimplifyRestricted doc tau_tvs wanted_lie
778 = -- First squash out all methods, to find the constrained tyvars
779 -- We can't just take the free vars of wanted_lie because that'll
780 -- have methods that may incidentally mention entirely unconstrained variables
781 -- e.g. a call to f :: Eq a => a -> b -> b
782 -- Here, b is unconstrained. A good example would be
784 -- We want to infer the polymorphic type
785 -- foo :: forall b. b -> b
787 wanteds = lieToList wanted_lie
788 try_me inst = ReduceMe -- Reduce as far as we can. Don't stop at
789 -- dicts; the idea is to get rid of as many type
790 -- variables as possible, and we don't want to stop
791 -- at (say) Monad (ST s), because that reduces
792 -- immediately, with no constraint on s.
794 simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
796 -- Next, figure out the tyvars we will quantify over
797 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
798 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
800 constrained_tvs = tyVarsOfInsts constrained_dicts
801 qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
802 `minusVarSet` constrained_tvs
805 -- The first step may have squashed more methods than
806 -- necessary, so try again, this time knowing the exact
807 -- set of type variables to quantify over.
809 -- We quantify only over constraints that are captured by qtvs;
810 -- these will just be a subset of non-dicts. This in contrast
811 -- to normal inference (using isFreeWhenInferring) in which we quantify over
812 -- all *non-inheritable* constraints too. This implements choice
813 -- (B) under "implicit parameter and monomorphism" above.
815 -- Remember that we may need to do *some* simplification, to
816 -- (for example) squash {Monad (ST s)} into {}. It's not enough
817 -- just to float all constraints
818 mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
820 try_me inst | isFreeWrtTyVars qtvs inst = Free
821 | otherwise = ReduceMe
823 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
824 ASSERT( no_improvement )
825 ASSERT( null irreds )
826 -- No need to loop because simpleReduceLoop will have
827 -- already done any improvement necessary
829 returnTc (varSetElems qtvs, mkLIE frees, binds)
833 %************************************************************************
835 \subsection{tcSimplifyToDicts}
837 %************************************************************************
839 On the LHS of transformation rules we only simplify methods and constants,
840 getting dictionaries. We want to keep all of them unsimplified, to serve
841 as the available stuff for the RHS of the rule.
843 The same thing is used for specialise pragmas. Consider
846 {-# SPECIALISE f :: Int -> Int #-}
849 The type checker generates a binding like:
851 f_spec = (f :: Int -> Int)
853 and we want to end up with
855 f_spec = _inline_me_ (f Int dNumInt)
857 But that means that we must simplify the Method for f to (f Int dNumInt)!
858 So tcSimplifyToDicts squeezes out all Methods.
860 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
862 fromIntegral :: (Integral a, Num b) => a -> b
863 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
865 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
869 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
871 because the scsel will mess up matching. Instead we want
873 forall dIntegralInt, dNumInt.
874 fromIntegral Int Int dIntegralInt dNumInt = id Int
876 Hence "DontReduce NoSCs"
879 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
880 tcSimplifyToDicts wanted_lie
881 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
882 -- Since try_me doesn't look at types, we don't need to
883 -- do any zonking, so it's safe to call reduceContext directly
885 returnTc (irreds, binds)
888 doc = text "tcSimplifyToDicts"
889 wanteds = lieToList wanted_lie
891 -- Reduce methods and lits only; stop as soon as we get a dictionary
892 try_me inst | isDict inst = DontReduce NoSCs
893 | otherwise = ReduceMe
897 %************************************************************************
899 \subsection{Filtering at a dynamic binding}
901 %************************************************************************
906 we must discharge all the ?x constraints from B. We also do an improvement
907 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
909 Actually, the constraints from B might improve the types in ?x. For example
911 f :: (?x::Int) => Char -> Char
914 then the constraint (?x::Int) arising from the call to f will
915 force the binding for ?x to be of type Int.
918 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
920 -> TcM (LIE, TcDictBinds)
921 tcSimplifyIPs given_ips wanted_lie
922 = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
923 returnTc (mkLIE frees, binds)
925 doc = text "tcSimplifyIPs" <+> ppr given_ips
926 wanteds = lieToList wanted_lie
927 ip_set = mkNameSet (ipNamesOfInsts given_ips)
929 -- Simplify any methods that mention the implicit parameter
930 try_me inst | isFreeWrtIPs ip_set inst = Free
931 | otherwise = ReduceMe
933 simpl_loop givens wanteds
934 = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
935 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
937 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
939 if no_improvement then
940 ASSERT( null irreds )
941 returnTc (frees, binds)
943 simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
944 returnTc (frees1, binds `AndMonoBinds` binds1)
948 %************************************************************************
950 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
952 %************************************************************************
954 When doing a binding group, we may have @Insts@ of local functions.
955 For example, we might have...
957 let f x = x + 1 -- orig local function (overloaded)
958 f.1 = f Int -- two instances of f
963 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
964 where @f@ is in scope; those @Insts@ must certainly not be passed
965 upwards towards the top-level. If the @Insts@ were binding-ified up
966 there, they would have unresolvable references to @f@.
968 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
969 For each method @Inst@ in the @init_lie@ that mentions one of the
970 @Ids@, we create a binding. We return the remaining @Insts@ (in an
971 @LIE@), as well as the @HsBinds@ generated.
974 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
976 bindInstsOfLocalFuns init_lie local_ids
977 | null overloaded_ids
979 = returnTc (init_lie, EmptyMonoBinds)
982 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
983 ASSERT( null irreds )
984 returnTc (mkLIE frees, binds)
986 doc = text "bindInsts" <+> ppr local_ids
987 wanteds = lieToList init_lie
988 overloaded_ids = filter is_overloaded local_ids
989 is_overloaded id = isOverloadedTy (idType id)
991 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
992 -- so it's worth building a set, so that
993 -- lookup (in isMethodFor) is faster
995 try_me inst | isMethodFor overloaded_set inst = ReduceMe
1000 %************************************************************************
1002 \subsection{Data types for the reduction mechanism}
1004 %************************************************************************
1006 The main control over context reduction is here
1010 = ReduceMe -- Try to reduce this
1011 -- If there's no instance, behave exactly like
1012 -- DontReduce: add the inst to
1013 -- the irreductible ones, but don't
1014 -- produce an error message of any kind.
1015 -- It might be quite legitimate such as (Eq a)!
1017 | DontReduce WantSCs -- Return as irreducible
1019 | DontReduceUnlessConstant -- Return as irreducible unless it can
1020 -- be reduced to a constant in one step
1022 | Free -- Return as free
1024 reduceMe :: Inst -> WhatToDo
1025 reduceMe inst = ReduceMe
1027 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1028 -- of a predicate when adding it to the avails
1034 type Avails = FiniteMap Inst Avail
1037 = IsFree -- Used for free Insts
1038 | Irred -- Used for irreducible dictionaries,
1039 -- which are going to be lambda bound
1041 | Given TcId -- Used for dictionaries for which we have a binding
1042 -- e.g. those "given" in a signature
1043 Bool -- True <=> actually consumed (splittable IPs only)
1045 | NoRhs -- Used for Insts like (CCallable f)
1046 -- where no witness is required.
1048 | Rhs -- Used when there is a RHS
1050 [Inst] -- Insts free in the RHS; we need these too
1052 | Linear -- Splittable Insts only.
1053 Int -- The Int is always 2 or more; indicates how
1054 -- many copies are required
1055 Inst -- The splitter
1056 Avail -- Where the "master copy" is
1058 | LinRhss -- Splittable Insts only; this is used only internally
1059 -- by extractResults, where a Linear
1060 -- is turned into an LinRhss
1061 [TcExpr] -- A supply of suitable RHSs
1063 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
1064 | (inst,avail) <- fmToList avails ]
1066 instance Outputable Avail where
1069 pprAvail NoRhs = text "<no rhs>"
1070 pprAvail IsFree = text "Free"
1071 pprAvail Irred = text "Irred"
1072 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1073 if b then text "(used)" else empty
1074 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1075 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1076 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1079 Extracting the bindings from a bunch of Avails.
1080 The bindings do *not* come back sorted in dependency order.
1081 We assume that they'll be wrapped in a big Rec, so that the
1082 dependency analyser can sort them out later
1086 extractResults :: Avails
1088 -> NF_TcM (TcDictBinds, -- Bindings
1089 [Inst], -- Irreducible ones
1090 [Inst]) -- Free ones
1092 extractResults avails wanteds
1093 = go avails EmptyMonoBinds [] [] wanteds
1095 go avails binds irreds frees []
1096 = returnNF_Tc (binds, irreds, frees)
1098 go avails binds irreds frees (w:ws)
1099 = case lookupFM avails w of
1100 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1101 go avails binds irreds frees ws
1103 Just NoRhs -> go avails binds irreds frees ws
1104 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1105 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1107 Just (Given id _) -> go avails new_binds irreds frees ws
1109 new_binds | id == instToId w = binds
1110 | otherwise = addBind binds w (HsVar id)
1111 -- The sought Id can be one of the givens, via a superclass chain
1112 -- and then we definitely don't want to generate an x=x binding!
1114 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1116 new_binds = addBind binds w rhs
1118 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1119 -> go new_avails new_binds irreds frees ws
1121 new_binds = addBind binds w rhs
1122 new_avails = addToFM avails w (LinRhss rhss)
1124 Just (Linear n split_inst avail)
1125 -> split n (instToId split_inst) avail w `thenNF_Tc` \ (binds', (rhs:rhss), irreds') ->
1126 go (addToFM avails w (LinRhss rhss))
1127 (binds `AndMonoBinds` addBind binds' w rhs)
1128 (irreds' ++ irreds) frees (split_inst:ws)
1132 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1133 | otherwise = addToFM avails w NoRhs
1134 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1135 -- than Given, else we end up with bogus bindings.
1137 add_free avails w | isMethod w = avails
1138 | otherwise = add_given avails w
1140 -- Do *not* replace Free by Given if it's a method.
1141 -- The following situation shows why this is bad:
1142 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1143 -- From an application (truncate f i) we get
1144 -- t1 = truncate at f
1146 -- If we have also have a second occurrence of truncate, we get
1147 -- t3 = truncate at f
1149 -- When simplifying with i,f free, we might still notice that
1150 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1151 -- will continue to float out!
1152 -- (split n i a) returns: n rhss
1153 -- auxiliary bindings
1154 -- 1 or 0 insts to add to irreds
1157 split :: Int -> TcId -> Avail -> Inst
1158 -> NF_TcM (TcDictBinds, [TcExpr], [Inst])
1159 -- (split n split_id avail wanted) returns
1160 -- * a list of 'n' expressions, all of which witness 'avail'
1161 -- * a bunch of auxiliary bindings to support these expressions
1162 -- * one or zero insts needed to witness the whole lot
1163 -- (maybe be zero if the initial Inst is a Given)
1164 split n split_id avail wanted
1167 ty = linearInstType wanted
1168 pair_ty = mkTyConApp pairTyCon [ty,ty]
1169 id = instToId wanted
1173 go 1 = case avail of
1174 Given id _ -> returnNF_Tc (EmptyMonoBinds, [HsVar id], [])
1175 Irred -> cloneDict wanted `thenNF_Tc` \ w' ->
1176 returnNF_Tc (EmptyMonoBinds, [HsVar (instToId w')], [w'])
1178 go n = go ((n+1) `div` 2) `thenNF_Tc` \ (binds1, rhss, irred) ->
1179 expand n rhss `thenNF_Tc` \ (binds2, rhss') ->
1180 returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss', irred)
1183 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1184 -- e.g. expand 3 [rhs1, rhs2]
1185 -- = ( { x = split rhs1 },
1186 -- [fst x, snd x, rhs2] )
1188 | n `rem` 2 == 0 = go rhss -- n is even
1189 | otherwise = go (tail rhss) `thenNF_Tc` \ (binds', rhss') ->
1190 returnNF_Tc (binds', head rhss : rhss')
1192 go rhss = mapAndUnzipNF_Tc do_one rhss `thenNF_Tc` \ (binds', rhss') ->
1193 returnNF_Tc (andMonoBindList binds', concat rhss')
1195 do_one rhs = tcGetUnique `thenNF_Tc` \ uniq ->
1196 tcLookupGlobalId fstIdName `thenNF_Tc` \ fst_id ->
1197 tcLookupGlobalId sndIdName `thenNF_Tc` \ snd_id ->
1199 x = mkUserLocal occ uniq pair_ty loc
1201 returnNF_Tc (VarMonoBind x (mk_app split_id rhs),
1202 [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
1204 mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
1206 mk_app id rhs = HsApp (HsVar id) rhs
1208 addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
1212 %************************************************************************
1214 \subsection[reduce]{@reduce@}
1216 %************************************************************************
1218 When the "what to do" predicate doesn't depend on the quantified type variables,
1219 matters are easier. We don't need to do any zonking, unless the improvement step
1220 does something, in which case we zonk before iterating.
1222 The "given" set is always empty.
1225 simpleReduceLoop :: SDoc
1226 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1228 -> TcM ([Inst], -- Free
1230 [Inst]) -- Irreducible
1232 simpleReduceLoop doc try_me wanteds
1233 = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
1234 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
1235 if no_improvement then
1236 returnTc (frees, binds, irreds)
1238 simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
1239 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1245 reduceContext :: SDoc
1246 -> (Inst -> WhatToDo)
1249 -> NF_TcM (Bool, -- True <=> improve step did no unification
1251 TcDictBinds, -- Dictionary bindings
1252 [Inst]) -- Irreducible
1254 reduceContext doc try_me givens wanteds
1256 traceTc (text "reduceContext" <+> (vcat [
1257 text "----------------------",
1259 text "given" <+> ppr givens,
1260 text "wanted" <+> ppr wanteds,
1261 text "----------------------"
1264 -- Build the Avail mapping from "givens"
1265 foldlNF_Tc addGiven emptyFM givens `thenNF_Tc` \ init_state ->
1268 reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ avails ->
1270 -- Do improvement, using everything in avails
1271 -- In particular, avails includes all superclasses of everything
1272 tcImprove avails `thenTc` \ no_improvement ->
1274 extractResults avails wanteds `thenNF_Tc` \ (binds, irreds, frees) ->
1276 traceTc (text "reduceContext end" <+> (vcat [
1277 text "----------------------",
1279 text "given" <+> ppr givens,
1280 text "wanted" <+> ppr wanteds,
1282 text "avails" <+> pprAvails avails,
1283 text "frees" <+> ppr frees,
1284 text "no_improvement =" <+> ppr no_improvement,
1285 text "----------------------"
1288 returnTc (no_improvement, frees, binds, irreds)
1291 = tcGetInstEnv `thenTc` \ inst_env ->
1293 preds = [ (pred, pp_loc)
1294 | inst <- keysFM avails,
1295 let pp_loc = pprInstLoc (instLoc inst),
1296 pred <- predsOfInst inst,
1299 -- Avails has all the superclasses etc (good)
1300 -- It also has all the intermediates of the deduction (good)
1301 -- It does not have duplicates (good)
1302 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1303 -- so that improve will see them separate
1304 eqns = improve (classInstEnv inst_env) preds
1309 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
1310 mapTc_ unify eqns `thenTc_`
1313 unify ((qtvs, t1, t2), doc)
1314 = tcAddErrCtxt doc $
1315 tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
1316 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1319 The main context-reduction function is @reduce@. Here's its game plan.
1322 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1323 -- along with its depth
1324 -> (Inst -> WhatToDo)
1331 try_me: given an inst, this function returns
1333 DontReduce return this in "irreds"
1334 Free return this in "frees"
1336 wanteds: The list of insts to reduce
1337 state: An accumulating parameter of type Avails
1338 that contains the state of the algorithm
1340 It returns a Avails.
1342 The (n,stack) pair is just used for error reporting.
1343 n is always the depth of the stack.
1344 The stack is the stack of Insts being reduced: to produce X
1345 I had to produce Y, to produce Y I had to produce Z, and so on.
1348 reduceList (n,stack) try_me wanteds state
1349 | n > opt_MaxContextReductionDepth
1350 = failWithTc (reduceDepthErr n stack)
1356 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1361 go [] state = returnTc state
1362 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
1365 -- Base case: we're done!
1366 reduce stack try_me wanted state
1367 -- It's the same as an existing inst, or a superclass thereof
1368 | Just avail <- isAvailable state wanted
1369 = if isLinearInst wanted then
1370 addLinearAvailable state avail wanted `thenNF_Tc` \ (state', wanteds') ->
1371 reduceList stack try_me wanteds' state'
1373 returnTc state -- No op for non-linear things
1376 = case try_me wanted of {
1378 DontReduce want_scs -> addIrred want_scs state wanted
1380 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1381 -- First, see if the inst can be reduced to a constant in one step
1382 try_simple (addIrred AddSCs) -- Assume want superclasses
1384 ; Free -> -- It's free so just chuck it upstairs
1385 -- First, see if the inst can be reduced to a constant in one step
1388 ; ReduceMe -> -- It should be reduced
1389 lookupInst wanted `thenNF_Tc` \ lookup_result ->
1390 case lookup_result of
1391 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
1392 addWanted state' wanted rhs wanteds'
1393 SimpleInst rhs -> addWanted state wanted rhs []
1395 NoInstance -> -- No such instance!
1396 -- Add it and its superclasses
1397 addIrred AddSCs state wanted
1401 try_simple do_this_otherwise
1402 = lookupInst wanted `thenNF_Tc` \ lookup_result ->
1403 case lookup_result of
1404 SimpleInst rhs -> addWanted state wanted rhs []
1405 other -> do_this_otherwise state wanted
1410 -------------------------
1411 isAvailable :: Avails -> Inst -> Maybe Avail
1412 isAvailable avails wanted = lookupFM avails wanted
1413 -- NB 1: the Ord instance of Inst compares by the class/type info
1414 -- *not* by unique. So
1415 -- d1::C Int == d2::C Int
1417 addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
1418 addLinearAvailable avails avail wanted
1420 = tcLookupGlobalId splitIdName `thenNF_Tc` \ split_id ->
1421 newMethodAtLoc (instLoc wanted) split_id
1422 [linearInstType wanted] `thenNF_Tc` \ (split_inst,_) ->
1423 returnNF_Tc (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1426 = returnNF_Tc (addToFM avails wanted avail', [])
1428 avail' = case avail of
1429 Given id _ -> Given id True
1430 Linear n i a -> Linear (n+1) i a
1432 need_split Irred = True
1433 need_split (Given _ used) = used
1434 need_split (Linear _ _ _) = False
1436 -------------------------
1437 addFree :: Avails -> Inst -> NF_TcM Avails
1438 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1439 -- to avails, so that any other equal Insts will be commoned up right
1440 -- here rather than also being tossed upstairs. This is really just
1441 -- an optimisation, and perhaps it is more trouble that it is worth,
1442 -- as the following comments show!
1444 -- NB1: do *not* add superclasses. If we have
1447 -- but a is not bound here, then we *don't* want to derive
1448 -- dn from df here lest we lose sharing.
1450 addFree avails free = returnNF_Tc (addToFM avails free IsFree)
1452 addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
1453 addWanted avails wanted rhs_expr wanteds
1454 -- Do *not* add superclasses as well. Here's an example of why not
1455 -- class Eq a => Foo a b
1456 -- instance Eq a => Foo [a] a
1457 -- If we are reducing
1459 -- we'll first deduce that it holds (via the instance decl). We
1460 -- must not then overwrite the Eq t constraint with a superclass selection!
1461 -- ToDo: this isn't entirely unsatisfactory, because
1462 -- we may also lose some entirely-legitimate sharing this way
1464 = ASSERT( not (wanted `elemFM` avails) )
1465 returnNF_Tc (addToFM avails wanted avail)
1467 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1468 | otherwise = ASSERT( null wanteds ) NoRhs
1470 addGiven :: Avails -> Inst -> NF_TcM Avails
1471 addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
1473 addIrred :: WantSCs -> Avails -> Inst -> NF_TcM Avails
1474 addIrred NoSCs state irred = returnNF_Tc (addToFM state irred Irred)
1475 addIrred AddSCs state irred = addAvailAndSCs state irred Irred
1477 addAvailAndSCs :: Avails -> Inst -> Avail -> NF_TcM Avails
1478 addAvailAndSCs avails wanted avail
1479 = add_scs (addToFM avails wanted avail) wanted
1481 add_scs :: Avails -> Inst -> NF_TcM Avails
1482 -- Add all the superclasses of the Inst to Avails
1483 -- Invariant: the Inst is already in Avails.
1486 | not (isClassDict dict)
1487 = returnNF_Tc avails
1489 | otherwise -- It is a dictionary
1490 = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
1491 foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1493 (clas, tys) = getDictClassTys dict
1494 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1495 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1497 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1498 = case lookupFM avails sc_dict of
1499 Just (Given _ _) -> returnNF_Tc avails -- See Note [SUPER] below
1500 other -> addAvailAndSCs avails sc_dict avail
1502 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1503 avail = Rhs sc_sel_rhs [dict]
1506 Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
1507 and want to deduce (d2:C [a]) where
1509 class Ord a => C a where
1510 instance Ord a => C [a] where ...
1512 Then we'll use the instance decl to deduce C [a] and then add the
1513 superclasses of C [a] to avails. But we must not overwrite the binding
1514 for d1:Ord a (which is given) with a superclass selection or we'll just
1515 build a loop! Hence looking for Given. Crudely, Given is cheaper
1519 %************************************************************************
1521 \section{tcSimplifyTop: defaulting}
1523 %************************************************************************
1526 @tcSimplifyTop@ is called once per module to simplify all the constant
1527 and ambiguous Insts.
1529 We need to be careful of one case. Suppose we have
1531 instance Num a => Num (Foo a b) where ...
1533 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1534 to (Num x), and default x to Int. But what about y??
1536 It's OK: the final zonking stage should zap y to (), which is fine.
1540 tcSimplifyTop :: LIE -> TcM TcDictBinds
1541 tcSimplifyTop wanted_lie
1542 = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenTc` \ (frees, binds, irreds) ->
1543 ASSERT( null frees )
1546 -- All the non-std ones are definite errors
1547 (stds, non_stds) = partition isStdClassTyVarDict irreds
1549 -- Group by type variable
1550 std_groups = equivClasses cmp_by_tyvar stds
1552 -- Pick the ones which its worth trying to disambiguate
1553 (std_oks, std_bads) = partition worth_a_try std_groups
1555 -- Have a try at disambiguation
1556 -- if the type variable isn't bound
1557 -- up with one of the non-standard classes
1558 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1559 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1561 -- Collect together all the bad guys
1562 bad_guys = non_stds ++ concat std_bads
1564 -- Disambiguate the ones that look feasible
1565 mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
1567 -- And complain about the ones that don't
1568 -- This group includes both non-existent instances
1569 -- e.g. Num (IO a) and Eq (Int -> Int)
1570 -- and ambiguous dictionaries
1572 addTopAmbigErrs bad_guys `thenNF_Tc_`
1574 returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1576 wanteds = lieToList wanted_lie
1578 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1580 get_tv d = case getDictClassTys d of
1581 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1582 get_clas d = case getDictClassTys d of
1583 (clas, [ty]) -> clas
1586 If a dictionary constrains a type variable which is
1587 * not mentioned in the environment
1588 * and not mentioned in the type of the expression
1589 then it is ambiguous. No further information will arise to instantiate
1590 the type variable; nor will it be generalised and turned into an extra
1591 parameter to a function.
1593 It is an error for this to occur, except that Haskell provided for
1594 certain rules to be applied in the special case of numeric types.
1596 * at least one of its classes is a numeric class, and
1597 * all of its classes are numeric or standard
1598 then the type variable can be defaulted to the first type in the
1599 default-type list which is an instance of all the offending classes.
1601 So here is the function which does the work. It takes the ambiguous
1602 dictionaries and either resolves them (producing bindings) or
1603 complains. It works by splitting the dictionary list by type
1604 variable, and using @disambigOne@ to do the real business.
1606 @disambigOne@ assumes that its arguments dictionaries constrain all
1607 the same type variable.
1609 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1610 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1611 the most common use of defaulting is code like:
1613 _ccall_ foo `seqPrimIO` bar
1615 Since we're not using the result of @foo@, the result if (presumably)
1619 disambigGroup :: [Inst] -- All standard classes of form (C a)
1623 | any isNumericClass classes -- Guaranteed all standard classes
1624 -- see comment at the end of function for reasons as to
1625 -- why the defaulting mechanism doesn't apply to groups that
1626 -- include CCallable or CReturnable dicts.
1627 && not (any isCcallishClass classes)
1628 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1629 -- SO, TRY DEFAULT TYPES IN ORDER
1631 -- Failure here is caused by there being no type in the
1632 -- default list which can satisfy all the ambiguous classes.
1633 -- For example, if Real a is reqd, but the only type in the
1634 -- default list is Int.
1635 tcGetDefaultTys `thenNF_Tc` \ default_tys ->
1637 try_default [] -- No defaults work, so fail
1640 try_default (default_ty : default_tys)
1641 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1642 -- default_tys instead
1643 tcSimplifyDefault theta `thenTc` \ _ ->
1646 theta = [mkClassPred clas [default_ty] | clas <- classes]
1648 -- See if any default works, and if so bind the type variable to it
1649 -- If not, add an AmbigErr
1650 recoverTc (addAmbigErrs dicts `thenNF_Tc_`
1651 returnTc EmptyMonoBinds) $
1653 try_default default_tys `thenTc` \ chosen_default_ty ->
1655 -- Bind the type variable and reduce the context, for real this time
1656 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
1657 simpleReduceLoop (text "disambig" <+> ppr dicts)
1658 reduceMe dicts `thenTc` \ (frees, binds, ambigs) ->
1659 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1660 warnDefault dicts chosen_default_ty `thenTc_`
1663 | all isCreturnableClass classes
1664 = -- Default CCall stuff to (); we don't even both to check that () is an
1665 -- instance of CReturnable, because we know it is.
1666 unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
1667 returnTc EmptyMonoBinds
1669 | otherwise -- No defaults
1670 = addAmbigErrs dicts `thenNF_Tc_`
1671 returnTc EmptyMonoBinds
1674 tyvar = get_tv (head dicts) -- Should be non-empty
1675 classes = map get_clas dicts
1678 [Aside - why the defaulting mechanism is turned off when
1679 dealing with arguments and results to ccalls.
1681 When typechecking _ccall_s, TcExpr ensures that the external
1682 function is only passed arguments (and in the other direction,
1683 results) of a restricted set of 'native' types. This is
1684 implemented via the help of the pseudo-type classes,
1685 @CReturnable@ (CR) and @CCallable@ (CC.)
1687 The interaction between the defaulting mechanism for numeric
1688 values and CC & CR can be a bit puzzling to the user at times.
1697 What type has 'x' got here? That depends on the default list
1698 in operation, if it is equal to Haskell 98's default-default
1699 of (Integer, Double), 'x' has type Double, since Integer
1700 is not an instance of CR. If the default list is equal to
1701 Haskell 1.4's default-default of (Int, Double), 'x' has type
1704 To try to minimise the potential for surprises here, the
1705 defaulting mechanism is turned off in the presence of
1706 CCallable and CReturnable.
1711 %************************************************************************
1713 \subsection[simple]{@Simple@ versions}
1715 %************************************************************************
1717 Much simpler versions when there are no bindings to make!
1719 @tcSimplifyThetas@ simplifies class-type constraints formed by
1720 @deriving@ declarations and when specialising instances. We are
1721 only interested in the simplified bunch of class/type constraints.
1723 It simplifies to constraints of the form (C a b c) where
1724 a,b,c are type variables. This is required for the context of
1725 instance declarations.
1728 tcSimplifyDeriv :: [TyVar]
1729 -> ThetaType -- Wanted
1730 -> TcM ThetaType -- Needed
1732 tcSimplifyDeriv tyvars theta
1733 = tcInstTyVars tyvars `thenNF_Tc` \ (tvs, _, tenv) ->
1734 -- The main loop may do unification, and that may crash if
1735 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
1736 -- ToDo: what if two of them do get unified?
1737 newDicts DataDeclOrigin (substTheta tenv theta) `thenNF_Tc` \ wanteds ->
1738 simpleReduceLoop doc reduceMe wanteds `thenTc` \ (frees, _, irreds) ->
1739 ASSERT( null frees ) -- reduceMe never returns Free
1742 tv_set = mkVarSet tvs
1743 simpl_theta = map dictPred irreds -- reduceMe squashes all non-dicts
1746 -- Check that the returned dictionaries are all of form (C a b)
1747 -- (where a, b are type variables).
1748 -- At one time we allowed this if we had -fallow-undecidable-instances,
1749 -- but that risks non-termination in the 'deriving' context-inference
1750 -- fixpoint loop. If you want fancy stuff you just have to write the
1751 -- instance decl yourself.
1752 | not (isTyVarClassPred pred)
1753 = addErrTc (noInstErr pred)
1755 -- Check for a bizarre corner case, when the derived instance decl should
1756 -- have form instance C a b => D (T a) where ...
1757 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
1758 -- of problems; in particular, it's hard to compare solutions for
1759 -- equality when finding the fixpoint. So I just rule it out for now.
1760 | not (tyVarsOfPred pred `subVarSet` tv_set)
1761 = addErrTc (badDerivedPred pred)
1766 rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
1767 -- This reverse-mapping is a Royal Pain,
1768 -- but the result should mention TyVars not TcTyVars
1771 mapNF_Tc check_pred simpl_theta `thenNF_Tc_`
1772 checkAmbiguity tvs simpl_theta tv_set `thenTc_`
1773 returnTc (substTheta rev_env simpl_theta)
1775 doc = ptext SLIT("deriving classes for a data type")
1778 @tcSimplifyDefault@ just checks class-type constraints, essentially;
1779 used with \tr{default} declarations. We are only interested in
1780 whether it worked or not.
1783 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
1786 tcSimplifyDefault theta
1787 = newDicts DataDeclOrigin theta `thenNF_Tc` \ wanteds ->
1788 simpleReduceLoop doc reduceMe wanteds `thenTc` \ (frees, _, irreds) ->
1789 ASSERT( null frees ) -- try_me never returns Free
1790 mapNF_Tc (addErrTc . noInstErr) irreds `thenNF_Tc_`
1796 doc = ptext SLIT("default declaration")
1800 %************************************************************************
1802 \section{Errors and contexts}
1804 %************************************************************************
1806 ToDo: for these error messages, should we note the location as coming
1807 from the insts, or just whatever seems to be around in the monad just
1811 groupInsts :: [Inst] -> [[Inst]]
1812 -- Group together insts with the same origin
1813 -- We want to report them together in error messages
1815 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1817 -- (It may seem a bit crude to compare the error messages,
1818 -- but it makes sure that we combine just what the user sees,
1819 -- and it avoids need equality on InstLocs.)
1820 (friends, others) = partition is_friend insts
1821 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1822 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1825 addTopAmbigErrs dicts
1826 = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
1827 mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
1828 mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
1831 fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1832 (tidy_env, tidy_dicts) = tidyInsts dicts
1833 (bad_ips, non_ips) = partition is_ip tidy_dicts
1834 (no_insts, ambigs) = partition no_inst non_ips
1835 is_ip d = any isIPPred (predsOfInst d)
1836 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1839 plural xs = char 's'
1841 addTopIPErrs tidy_env tidy_dicts
1842 = addInstErrTcM (instLoc (head tidy_dicts))
1844 ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1846 -- Used for top-level irreducibles
1847 addTopInstanceErrs tidy_env tidy_dicts
1848 = addInstErrTcM (instLoc (head tidy_dicts))
1850 ptext SLIT("No instance") <> plural tidy_dicts <+>
1851 ptext SLIT("for") <+> pprInsts tidy_dicts)
1854 = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1856 (tidy_env, tidy_dicts) = tidyInsts dicts
1858 addAmbigErr tidy_env tidy_dict
1859 = addInstErrTcM (instLoc tidy_dict)
1861 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1862 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1864 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1866 warnDefault dicts default_ty
1867 = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
1868 tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1871 (_, tidy_dicts) = tidyInsts dicts
1872 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1873 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1874 quotes (ppr default_ty),
1875 pprInstsInFull tidy_dicts]
1877 complainCheck doc givens irreds
1878 = mapNF_Tc zonkInst given_dicts_and_ips `thenNF_Tc` \ givens' ->
1879 mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
1882 given_dicts_and_ips = filter (not . isMethod) givens
1883 -- Filter out methods, which are only added to
1884 -- the given set as an optimisation
1886 addNoInstanceErrs what_doc givens dicts
1887 = getDOptsTc `thenNF_Tc` \ dflags ->
1888 tcGetInstEnv `thenNF_Tc` \ inst_env ->
1890 (tidy_env1, tidy_givens) = tidyInsts givens
1891 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
1893 doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1894 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1896 ptext SLIT("Probable fix:"),
1900 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1901 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1904 -- The error message when we don't find a suitable instance
1905 -- is complicated by the fact that sometimes this is because
1906 -- there is no instance, and sometimes it's because there are
1907 -- too many instances (overlap). See the comments in TcEnv.lhs
1908 -- with the InstEnv stuff.
1911 | not ambig_overlap = empty
1913 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1914 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1915 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1917 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1918 ptext SLIT("to the") <+> what_doc]
1920 fix2 | null instance_dicts
1923 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1925 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1926 -- Insts for which it is worth suggesting an adding an instance declaration
1927 -- Exclude implicit parameters, and tyvar dicts
1929 -- Checks for the ambiguous case when we have overlapping instances
1930 ambig_overlap = any ambig_overlap1 dicts
1933 = case lookupInstEnv dflags inst_env clas tys of
1934 NoMatch ambig -> ambig
1938 (clas,tys) = getDictClassTys dict
1940 addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
1942 -- Used for the ...Thetas variants; all top level
1943 noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
1946 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
1947 ptext SLIT("type variables that are not data type parameters"),
1948 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
1950 reduceDepthErr n stack
1951 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1952 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1953 nest 4 (pprInstsInFull stack)]
1955 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1957 -----------------------------------------------
1959 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1960 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])