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, 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, TyVarDetails(VanillaTv),
45 mkClassPred, isOverloadedTy, mkTyConApp,
46 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
47 tyVarsOfPred, isIPPred, isInheritablePred, predHasFDs )
48 import Id ( idType, mkUserLocal )
50 import Name ( getOccName, getSrcLoc )
51 import NameSet ( NameSet, mkNameSet, elemNameSet )
52 import Class ( classBigSig )
53 import FunDeps ( oclose, grow, improve, pprEquationDoc )
54 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass,
55 splitName, fstName, sndName )
57 import Subst ( mkTopTyVarSubst, substTheta, substTy )
58 import TysWiredIn ( unitTy, pairTyCon )
62 import ListSetOps ( equivClasses )
63 import Util ( zipEqual )
64 import List ( partition )
69 %************************************************************************
73 %************************************************************************
75 --------------------------------------
76 Notes on quantification
77 --------------------------------------
79 Suppose we are about to do a generalisation step.
84 C the constraints from that RHS
86 The game is to figure out
88 Q the set of type variables over which to quantify
89 Ct the constraints we will *not* quantify over
90 Cq the constraints we will quantify over
92 So we're going to infer the type
96 and float the constraints Ct further outwards.
98 Here are the things that *must* be true:
100 (A) Q intersect fv(G) = EMPTY limits how big Q can be
101 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
103 (A) says we can't quantify over a variable that's free in the
104 environment. (B) says we must quantify over all the truly free
105 variables in T, else we won't get a sufficiently general type. We do
106 not *need* to quantify over any variable that is fixed by the free
107 vars of the environment G.
109 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
111 Example: class H x y | x->y where ...
113 fv(G) = {a} C = {H a b, H c d}
116 (A) Q intersect {a} is empty
117 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
119 So Q can be {c,d}, {b,c,d}
121 Other things being equal, however, we'd like to quantify over as few
122 variables as possible: smaller types, fewer type applications, more
123 constraints can get into Ct instead of Cq.
126 -----------------------------------------
129 fv(T) the free type vars of T
131 oclose(vs,C) The result of extending the set of tyvars vs
132 using the functional dependencies from C
134 grow(vs,C) The result of extend the set of tyvars vs
135 using all conceivable links from C.
137 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
138 Then grow(vs,C) = {a,b,c}
140 Note that grow(vs,C) `superset` grow(vs,simplify(C))
141 That is, simplfication can only shrink the result of grow.
144 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
145 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
148 -----------------------------------------
152 Here's a good way to choose Q:
154 Q = grow( fv(T), C ) \ oclose( fv(G), C )
156 That is, quantify over all variable that that MIGHT be fixed by the
157 call site (which influences T), but which aren't DEFINITELY fixed by
158 G. This choice definitely quantifies over enough type variables,
159 albeit perhaps too many.
161 Why grow( fv(T), C ) rather than fv(T)? Consider
163 class H x y | x->y where ...
168 If we used fv(T) = {c} we'd get the type
170 forall c. H c d => c -> b
172 And then if the fn was called at several different c's, each of
173 which fixed d differently, we'd get a unification error, because
174 d isn't quantified. Solution: quantify d. So we must quantify
175 everything that might be influenced by c.
177 Why not oclose( fv(T), C )? Because we might not be able to see
178 all the functional dependencies yet:
180 class H x y | x->y where ...
181 instance H x y => Eq (T x y) where ...
186 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
187 apparent yet, and that's wrong. We must really quantify over d too.
190 There really isn't any point in quantifying over any more than
191 grow( fv(T), C ), because the call sites can't possibly influence
192 any other type variables.
196 --------------------------------------
198 --------------------------------------
200 It's very hard to be certain when a type is ambiguous. Consider
204 instance H x y => K (x,y)
206 Is this type ambiguous?
207 forall a b. (K (a,b), Eq b) => a -> a
209 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
210 now we see that a fixes b. So we can't tell about ambiguity for sure
211 without doing a full simplification. And even that isn't possible if
212 the context has some free vars that may get unified. Urgle!
214 Here's another example: is this ambiguous?
215 forall a b. Eq (T b) => a -> a
216 Not if there's an insance decl (with no context)
217 instance Eq (T b) where ...
219 You may say of this example that we should use the instance decl right
220 away, but you can't always do that:
222 class J a b where ...
223 instance J Int b where ...
225 f :: forall a b. J a b => a -> a
227 (Notice: no functional dependency in J's class decl.)
228 Here f's type is perfectly fine, provided f is only called at Int.
229 It's premature to complain when meeting f's signature, or even
230 when inferring a type for f.
234 However, we don't *need* to report ambiguity right away. It'll always
235 show up at the call site.... and eventually at main, which needs special
236 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
238 So here's the plan. We WARN about probable ambiguity if
240 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
242 (all tested before quantification).
243 That is, all the type variables in Cq must be fixed by the the variables
244 in the environment, or by the variables in the type.
246 Notice that we union before calling oclose. Here's an example:
248 class J a b c | a b -> c
252 forall b c. (J a b c) => b -> b
254 Only if we union {a} from G with {b} from T before using oclose,
255 do we see that c is fixed.
257 It's a bit vague exactly which C we should use for this oclose call. If we
258 don't fix enough variables we might complain when we shouldn't (see
259 the above nasty example). Nothing will be perfect. That's why we can
260 only issue a warning.
263 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
265 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
267 then c is a "bubble"; there's no way it can ever improve, and it's
268 certainly ambiguous. UNLESS it is a constant (sigh). And what about
273 instance H x y => K (x,y)
275 Is this type ambiguous?
276 forall a b. (K (a,b), Eq b) => a -> a
278 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
279 is a "bubble" that's a set of constraints
281 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
283 Hence another idea. To decide Q start with fv(T) and grow it
284 by transitive closure in Cq (no functional dependencies involved).
285 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
286 The definitely-ambiguous can then float out, and get smashed at top level
287 (which squashes out the constants, like Eq (T a) above)
290 --------------------------------------
291 Notes on principal types
292 --------------------------------------
297 f x = let g y = op (y::Int) in True
299 Here the principal type of f is (forall a. a->a)
300 but we'll produce the non-principal type
301 f :: forall a. C Int => a -> a
304 --------------------------------------
305 Notes on implicit parameters
306 --------------------------------------
308 Question 1: can we "inherit" implicit parameters
309 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
314 where f is *not* a top-level binding.
315 From the RHS of f we'll get the constraint (?y::Int).
316 There are two types we might infer for f:
320 (so we get ?y from the context of f's definition), or
322 f :: (?y::Int) => Int -> Int
324 At first you might think the first was better, becuase then
325 ?y behaves like a free variable of the definition, rather than
326 having to be passed at each call site. But of course, the WHOLE
327 IDEA is that ?y should be passed at each call site (that's what
328 dynamic binding means) so we'd better infer the second.
330 BOTTOM LINE: when *inferring types* you *must* quantify
331 over implicit parameters. See the predicate isFreeWhenInferring.
334 Question 2: type signatures
335 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
336 BUT WATCH OUT: When you supply a type signature, we can't force you
337 to quantify over implicit parameters. For example:
341 This is perfectly reasonable. We do not want to insist on
343 (?x + 1) :: (?x::Int => Int)
345 That would be silly. Here, the definition site *is* the occurrence site,
346 so the above strictures don't apply. Hence the difference between
347 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
348 and tcSimplifyCheckBind (which does not).
350 What about when you supply a type signature for a binding?
351 Is it legal to give the following explicit, user type
352 signature to f, thus:
357 At first sight this seems reasonable, but it has the nasty property
358 that adding a type signature changes the dynamic semantics.
361 (let f x = (x::Int) + ?y
362 in (f 3, f 3 with ?y=5)) with ?y = 6
368 in (f 3, f 3 with ?y=5)) with ?y = 6
372 Indeed, simply inlining f (at the Haskell source level) would change the
375 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
376 semantics for a Haskell program without knowing its typing, so if you
377 change the typing you may change the semantics.
379 To make things consistent in all cases where we are *checking* against
380 a supplied signature (as opposed to inferring a type), we adopt the
383 a signature does not need to quantify over implicit params.
385 [This represents a (rather marginal) change of policy since GHC 5.02,
386 which *required* an explicit signature to quantify over all implicit
387 params for the reasons mentioned above.]
389 But that raises a new question. Consider
391 Given (signature) ?x::Int
392 Wanted (inferred) ?x::Int, ?y::Bool
394 Clearly we want to discharge the ?x and float the ?y out. But
395 what is the criterion that distinguishes them? Clearly it isn't
396 what free type variables they have. The Right Thing seems to be
397 to float a constraint that
398 neither mentions any of the quantified type variables
399 nor any of the quantified implicit parameters
401 See the predicate isFreeWhenChecking.
404 Question 3: monomorphism
405 ~~~~~~~~~~~~~~~~~~~~~~~~
406 There's a nasty corner case when the monomorphism restriction bites:
410 The argument above suggests that we *must* generalise
411 over the ?y parameter, to get
412 z :: (?y::Int) => Int,
413 but the monomorphism restriction says that we *must not*, giving
415 Why does the momomorphism restriction say this? Because if you have
417 let z = x + ?y in z+z
419 you might not expect the addition to be done twice --- but it will if
420 we follow the argument of Question 2 and generalise over ?y.
426 (A) Always generalise over implicit parameters
427 Bindings that fall under the monomorphism restriction can't
431 * Inlining remains valid
432 * No unexpected loss of sharing
433 * But simple bindings like
435 will be rejected, unless you add an explicit type signature
436 (to avoid the monomorphism restriction)
437 z :: (?y::Int) => Int
439 This seems unacceptable
441 (B) Monomorphism restriction "wins"
442 Bindings that fall under the monomorphism restriction can't
444 Always generalise over implicit parameters *except* for bindings
445 that fall under the monomorphism restriction
448 * Inlining isn't valid in general
449 * No unexpected loss of sharing
450 * Simple bindings like
452 accepted (get value of ?y from binding site)
454 (C) Always generalise over implicit parameters
455 Bindings that fall under the monomorphism restriction can't
456 be generalised, EXCEPT for implicit parameters
458 * Inlining remains valid
459 * Unexpected loss of sharing (from the extra generalisation)
460 * Simple bindings like
462 accepted (get value of ?y from occurrence sites)
467 None of these choices seems very satisfactory. But at least we should
468 decide which we want to do.
470 It's really not clear what is the Right Thing To Do. If you see
474 would you expect the value of ?y to be got from the *occurrence sites*
475 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
476 case of function definitions, the answer is clearly the former, but
477 less so in the case of non-fucntion definitions. On the other hand,
478 if we say that we get the value of ?y from the definition site of 'z',
479 then inlining 'z' might change the semantics of the program.
481 Choice (C) really says "the monomorphism restriction doesn't apply
482 to implicit parameters". Which is fine, but remember that every
483 innocent binding 'x = ...' that mentions an implicit parameter in
484 the RHS becomes a *function* of that parameter, called at each
485 use of 'x'. Now, the chances are that there are no intervening 'with'
486 clauses that bind ?y, so a decent compiler should common up all
487 those function calls. So I think I strongly favour (C). Indeed,
488 one could make a similar argument for abolishing the monomorphism
489 restriction altogether.
491 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
495 %************************************************************************
497 \subsection{tcSimplifyInfer}
499 %************************************************************************
501 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
503 1. Compute Q = grow( fvs(T), C )
505 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
506 predicates will end up in Ct; we deal with them at the top level
508 3. Try improvement, using functional dependencies
510 4. If Step 3 did any unification, repeat from step 1
511 (Unification can change the result of 'grow'.)
513 Note: we don't reduce dictionaries in step 2. For example, if we have
514 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
515 after step 2. However note that we may therefore quantify over more
516 type variables than we absolutely have to.
518 For the guts, we need a loop, that alternates context reduction and
519 improvement with unification. E.g. Suppose we have
521 class C x y | x->y where ...
523 and tcSimplify is called with:
525 Then improvement unifies a with b, giving
528 If we need to unify anything, we rattle round the whole thing all over
535 -> TcTyVarSet -- fv(T); type vars
537 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
539 TcDictBinds, -- Bindings
540 [TcId]) -- Dict Ids that must be bound here (zonked)
545 tcSimplifyInfer doc tau_tvs wanted_lie
546 = inferLoop doc (varSetElems tau_tvs)
547 (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
549 -- Check for non-generalisable insts
550 mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
552 returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
554 inferLoop doc tau_tvs wanteds
556 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
557 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
558 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
560 preds = predsOfInsts wanteds'
561 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
564 | isFreeWhenInferring qtvs inst = Free
565 | isClassDict inst = DontReduceUnlessConstant -- Dicts
566 | otherwise = ReduceMe -- Lits and Methods
569 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
572 if no_improvement then
573 returnTc (varSetElems qtvs, frees, binds, irreds)
575 -- If improvement did some unification, we go round again. There
576 -- are two subtleties:
577 -- a) We start again with irreds, not wanteds
578 -- Using an instance decl might have introduced a fresh type variable
579 -- which might have been unified, so we'd get an infinite loop
580 -- if we started again with wanteds! See example [LOOP]
582 -- b) It's also essential to re-process frees, because unification
583 -- might mean that a type variable that looked free isn't now.
585 -- Hence the (irreds ++ frees)
587 -- However, NOTICE that when we are done, we might have some bindings, but
588 -- the final qtvs might be empty. See [NO TYVARS] below.
590 inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
591 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
596 class If b t e r | b t e -> r
599 class Lte a b c | a b -> c where lte :: a -> b -> c
601 instance (Lte a b l,If l b a c) => Max a b c
603 Wanted: Max Z (S x) y
605 Then we'll reduce using the Max instance to:
606 (Lte Z (S x) l, If l (S x) Z y)
607 and improve by binding l->T, after which we can do some reduction
608 on both the Lte and If constraints. What we *can't* do is start again
609 with (Max Z (S x) y)!
613 class Y a b | a -> b where
616 instance Y [[a]] a where
619 k :: X a -> X a -> X a
621 g :: Num a => [X a] -> [X a]
624 h ys = ys ++ map (k (y [[0]])) xs
626 The excitement comes when simplifying the bindings for h. Initially
627 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
628 From this we get t1:=:t2, but also various bindings. We can't forget
629 the bindings (because of [LOOP]), but in fact t1 is what g is
632 The net effect of [NO TYVARS]
635 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
636 isFreeWhenInferring qtvs inst
637 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
638 && all isInheritablePred (predsOfInst inst) -- And no implicit parameter involved
639 -- (see "Notes on implicit parameters")
641 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
642 -> NameSet -- Quantified implicit parameters
644 isFreeWhenChecking qtvs ips inst
645 = isFreeWrtTyVars qtvs inst
646 && isFreeWrtIPs ips inst
648 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
649 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
653 %************************************************************************
655 \subsection{tcSimplifyCheck}
657 %************************************************************************
659 @tcSimplifyCheck@ is used when we know exactly the set of variables
660 we are going to quantify over. For example, a class or instance declaration.
665 -> [TcTyVar] -- Quantify over these
669 TcDictBinds) -- Bindings
671 -- tcSimplifyCheck is used when checking expression type signatures,
672 -- class decls, instance decls etc.
674 -- NB: 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!
678 -- NB: tcSimplifyCheck does not consult the
679 -- global type variables in the environment; so you don't
680 -- need to worry about setting them before calling tcSimplifyCheck
681 tcSimplifyCheck doc qtvs givens wanted_lie
682 = tcSimplCheck doc get_qtvs
683 givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
684 returnTc (frees, binds)
686 get_qtvs = zonkTcTyVarsAndFV qtvs
689 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
690 -- against, but we don't know the type variables over which we are going to quantify.
691 -- This happens when we have a type signature for a mutually recursive group
694 -> TcTyVarSet -- fv(T)
697 -> TcM ([TcTyVar], -- Variables over which to quantify
699 TcDictBinds) -- Bindings
701 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
702 = tcSimplCheck doc get_qtvs givens wanted_lie
704 -- Figure out which type variables to quantify over
705 -- You might think it should just be the signature tyvars,
706 -- but in bizarre cases you can get extra ones
707 -- f :: forall a. Num a => a -> a
708 -- f x = fst (g (x, head [])) + 1
710 -- Here we infer g :: forall a b. a -> b -> (b,a)
711 -- We don't want g to be monomorphic in b just because
712 -- f isn't quantified over b.
713 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
715 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenNF_Tc` \ all_tvs' ->
716 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
718 qtvs = all_tvs' `minusVarSet` gbl_tvs
719 -- We could close gbl_tvs, but its not necessary for
720 -- soundness, and it'll only affect which tyvars, not which
721 -- dictionaries, we quantify over
726 Here is the workhorse function for all three wrappers.
729 tcSimplCheck doc get_qtvs givens wanted_lie
730 = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
732 -- Complain about any irreducible ones
733 complainCheck doc givens irreds `thenNF_Tc_`
736 returnTc (qtvs, mkLIE frees, binds)
739 ip_set = mkNameSet (ipNamesOfInsts givens)
741 check_loop givens wanteds
743 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
744 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
745 get_qtvs `thenNF_Tc` \ qtvs' ->
749 -- When checking against a given signature we always reduce
750 -- until we find a match against something given, or can't reduce
751 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
752 | otherwise = ReduceMe
754 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
757 if no_improvement then
758 returnTc (varSetElems qtvs', frees, binds, irreds)
760 check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
761 returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
765 %************************************************************************
767 \subsection{tcSimplifyRestricted}
769 %************************************************************************
772 tcSimplifyRestricted -- Used for restricted binding groups
773 -- i.e. ones subject to the monomorphism restriction
775 -> TcTyVarSet -- Free in the type of the RHSs
776 -> LIE -- Free in the RHSs
777 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
779 TcDictBinds) -- Bindings
781 tcSimplifyRestricted doc tau_tvs wanted_lie
782 = -- First squash out all methods, to find the constrained tyvars
783 -- We can't just take the free vars of wanted_lie because that'll
784 -- have methods that may incidentally mention entirely unconstrained variables
785 -- e.g. a call to f :: Eq a => a -> b -> b
786 -- Here, b is unconstrained. A good example would be
788 -- We want to infer the polymorphic type
789 -- foo :: forall b. b -> b
791 wanteds = lieToList wanted_lie
792 try_me inst = ReduceMe -- Reduce as far as we can. Don't stop at
793 -- dicts; the idea is to get rid of as many type
794 -- variables as possible, and we don't want to stop
795 -- at (say) Monad (ST s), because that reduces
796 -- immediately, with no constraint on s.
798 simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
800 -- Next, figure out the tyvars we will quantify over
801 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
802 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
804 constrained_tvs = tyVarsOfInsts constrained_dicts
805 qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
806 `minusVarSet` constrained_tvs
809 -- The first step may have squashed more methods than
810 -- necessary, so try again, this time knowing the exact
811 -- set of type variables to quantify over.
813 -- We quantify only over constraints that are captured by qtvs;
814 -- these will just be a subset of non-dicts. This in contrast
815 -- to normal inference (using isFreeWhenInferring) in which we quantify over
816 -- all *non-inheritable* constraints too. This implements choice
817 -- (B) under "implicit parameter and monomorphism" above.
819 -- Remember that we may need to do *some* simplification, to
820 -- (for example) squash {Monad (ST s)} into {}. It's not enough
821 -- just to float all constraints
822 mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
824 try_me inst | isFreeWrtTyVars qtvs inst = Free
825 | otherwise = ReduceMe
827 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
828 ASSERT( no_improvement )
829 ASSERT( null irreds )
830 -- No need to loop because simpleReduceLoop will have
831 -- already done any improvement necessary
833 returnTc (varSetElems qtvs, mkLIE frees, binds)
837 %************************************************************************
839 \subsection{tcSimplifyToDicts}
841 %************************************************************************
843 On the LHS of transformation rules we only simplify methods and constants,
844 getting dictionaries. We want to keep all of them unsimplified, to serve
845 as the available stuff for the RHS of the rule.
847 The same thing is used for specialise pragmas. Consider
850 {-# SPECIALISE f :: Int -> Int #-}
853 The type checker generates a binding like:
855 f_spec = (f :: Int -> Int)
857 and we want to end up with
859 f_spec = _inline_me_ (f Int dNumInt)
861 But that means that we must simplify the Method for f to (f Int dNumInt)!
862 So tcSimplifyToDicts squeezes out all Methods.
864 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
866 fromIntegral :: (Integral a, Num b) => a -> b
867 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
869 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
873 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
875 because the scsel will mess up matching. Instead we want
877 forall dIntegralInt, dNumInt.
878 fromIntegral Int Int dIntegralInt dNumInt = id Int
880 Hence "DontReduce NoSCs"
883 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
884 tcSimplifyToDicts wanted_lie
885 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
886 -- Since try_me doesn't look at types, we don't need to
887 -- do any zonking, so it's safe to call reduceContext directly
889 returnTc (irreds, binds)
892 doc = text "tcSimplifyToDicts"
893 wanteds = lieToList wanted_lie
895 -- Reduce methods and lits only; stop as soon as we get a dictionary
896 try_me inst | isDict inst = DontReduce NoSCs
897 | otherwise = ReduceMe
901 %************************************************************************
903 \subsection{Filtering at a dynamic binding}
905 %************************************************************************
910 we must discharge all the ?x constraints from B. We also do an improvement
911 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
913 Actually, the constraints from B might improve the types in ?x. For example
915 f :: (?x::Int) => Char -> Char
918 then the constraint (?x::Int) arising from the call to f will
919 force the binding for ?x to be of type Int.
922 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
924 -> TcM (LIE, TcDictBinds)
925 tcSimplifyIPs given_ips wanted_lie
926 = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
927 returnTc (mkLIE frees, binds)
929 doc = text "tcSimplifyIPs" <+> ppr given_ips
930 wanteds = lieToList wanted_lie
931 ip_set = mkNameSet (ipNamesOfInsts given_ips)
933 -- Simplify any methods that mention the implicit parameter
934 try_me inst | isFreeWrtIPs ip_set inst = Free
935 | otherwise = ReduceMe
937 simpl_loop givens wanteds
938 = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
939 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
941 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
943 if no_improvement then
944 ASSERT( null irreds )
945 returnTc (frees, binds)
947 simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
948 returnTc (frees1, binds `AndMonoBinds` binds1)
952 %************************************************************************
954 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
956 %************************************************************************
958 When doing a binding group, we may have @Insts@ of local functions.
959 For example, we might have...
961 let f x = x + 1 -- orig local function (overloaded)
962 f.1 = f Int -- two instances of f
967 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
968 where @f@ is in scope; those @Insts@ must certainly not be passed
969 upwards towards the top-level. If the @Insts@ were binding-ified up
970 there, they would have unresolvable references to @f@.
972 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
973 For each method @Inst@ in the @init_lie@ that mentions one of the
974 @Ids@, we create a binding. We return the remaining @Insts@ (in an
975 @LIE@), as well as the @HsBinds@ generated.
978 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
980 bindInstsOfLocalFuns init_lie local_ids
981 | null overloaded_ids
983 = returnTc (init_lie, EmptyMonoBinds)
986 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
987 ASSERT( null irreds )
988 returnTc (mkLIE frees, binds)
990 doc = text "bindInsts" <+> ppr local_ids
991 wanteds = lieToList init_lie
992 overloaded_ids = filter is_overloaded local_ids
993 is_overloaded id = isOverloadedTy (idType id)
995 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
996 -- so it's worth building a set, so that
997 -- lookup (in isMethodFor) is faster
999 try_me inst | isMethodFor overloaded_set inst = ReduceMe
1004 %************************************************************************
1006 \subsection{Data types for the reduction mechanism}
1008 %************************************************************************
1010 The main control over context reduction is here
1014 = ReduceMe -- Try to reduce this
1015 -- If there's no instance, behave exactly like
1016 -- DontReduce: add the inst to
1017 -- the irreductible ones, but don't
1018 -- produce an error message of any kind.
1019 -- It might be quite legitimate such as (Eq a)!
1021 | DontReduce WantSCs -- Return as irreducible
1023 | DontReduceUnlessConstant -- Return as irreducible unless it can
1024 -- be reduced to a constant in one step
1026 | Free -- Return as free
1028 reduceMe :: Inst -> WhatToDo
1029 reduceMe inst = ReduceMe
1031 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1032 -- of a predicate when adding it to the avails
1038 type Avails = FiniteMap Inst Avail
1041 = IsFree -- Used for free Insts
1042 | Irred -- Used for irreducible dictionaries,
1043 -- which are going to be lambda bound
1045 | Given TcId -- Used for dictionaries for which we have a binding
1046 -- e.g. those "given" in a signature
1047 Bool -- True <=> actually consumed (splittable IPs only)
1049 | NoRhs -- Used for Insts like (CCallable f)
1050 -- where no witness is required.
1052 | Rhs -- Used when there is a RHS
1054 [Inst] -- Insts free in the RHS; we need these too
1056 | Linear -- Splittable Insts only.
1057 Int -- The Int is always 2 or more; indicates how
1058 -- many copies are required
1059 Inst -- The splitter
1060 Avail -- Where the "master copy" is
1062 | LinRhss -- Splittable Insts only; this is used only internally
1063 -- by extractResults, where a Linear
1064 -- is turned into an LinRhss
1065 [TcExpr] -- A supply of suitable RHSs
1067 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1068 | (inst,avail) <- fmToList avails ]
1070 instance Outputable Avail where
1073 pprAvail NoRhs = text "<no rhs>"
1074 pprAvail IsFree = text "Free"
1075 pprAvail Irred = text "Irred"
1076 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1077 if b then text "(used)" else empty
1078 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1079 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1080 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1083 Extracting the bindings from a bunch of Avails.
1084 The bindings do *not* come back sorted in dependency order.
1085 We assume that they'll be wrapped in a big Rec, so that the
1086 dependency analyser can sort them out later
1090 extractResults :: Avails
1092 -> NF_TcM (TcDictBinds, -- Bindings
1093 [Inst], -- Irreducible ones
1094 [Inst]) -- Free ones
1096 extractResults avails wanteds
1097 = go avails EmptyMonoBinds [] [] wanteds
1099 go avails binds irreds frees []
1100 = returnNF_Tc (binds, irreds, frees)
1102 go avails binds irreds frees (w:ws)
1103 = case lookupFM avails w of
1104 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1105 go avails binds irreds frees ws
1107 Just NoRhs -> go avails binds irreds frees ws
1108 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1109 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1111 Just (Given id _) -> go avails new_binds irreds frees ws
1113 new_binds | id == instToId w = binds
1114 | otherwise = addBind binds w (HsVar id)
1115 -- The sought Id can be one of the givens, via a superclass chain
1116 -- and then we definitely don't want to generate an x=x binding!
1118 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1120 new_binds = addBind binds w rhs
1122 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1123 -> get_root irreds frees avail w `thenNF_Tc` \ (irreds', frees', root_id) ->
1124 split n (instToId split_inst) root_id w `thenNF_Tc` \ (binds', rhss) ->
1125 go (addToFM avails w (LinRhss rhss))
1126 (binds `AndMonoBinds` binds')
1127 irreds' frees' (split_inst : w : ws)
1129 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1130 -> go new_avails new_binds irreds frees ws
1132 new_binds = addBind binds w rhs
1133 new_avails = addToFM avails w (LinRhss rhss)
1135 get_root irreds frees (Given id _) w = returnNF_Tc (irreds, frees, id)
1136 get_root irreds frees Irred w = cloneDict w `thenNF_Tc` \ w' ->
1137 returnNF_Tc (w':irreds, frees, instToId w')
1138 get_root irreds frees IsFree w = cloneDict w `thenNF_Tc` \ w' ->
1139 returnNF_Tc (irreds, w':frees, instToId w')
1142 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1143 | otherwise = addToFM avails w NoRhs
1144 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1145 -- than Given, else we end up with bogus bindings.
1147 add_free avails w | isMethod w = avails
1148 | otherwise = add_given avails w
1150 -- Do *not* replace Free by Given if it's a method.
1151 -- The following situation shows why this is bad:
1152 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1153 -- From an application (truncate f i) we get
1154 -- t1 = truncate at f
1156 -- If we have also have a second occurrence of truncate, we get
1157 -- t3 = truncate at f
1159 -- When simplifying with i,f free, we might still notice that
1160 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1161 -- will continue to float out!
1162 -- (split n i a) returns: n rhss
1163 -- auxiliary bindings
1164 -- 1 or 0 insts to add to irreds
1167 split :: Int -> TcId -> TcId -> Inst
1168 -> NF_TcM (TcDictBinds, [TcExpr])
1169 -- (split n split_id root_id wanted) returns
1170 -- * a list of 'n' expressions, all of which witness 'avail'
1171 -- * a bunch of auxiliary bindings to support these expressions
1172 -- * one or zero insts needed to witness the whole lot
1173 -- (maybe be zero if the initial Inst is a Given)
1175 -- NB: 'wanted' is just a template
1177 split n split_id root_id wanted
1180 ty = linearInstType wanted
1181 pair_ty = mkTyConApp pairTyCon [ty,ty]
1182 id = instToId wanted
1186 go 1 = returnNF_Tc (EmptyMonoBinds, [HsVar root_id])
1188 go n = go ((n+1) `div` 2) `thenNF_Tc` \ (binds1, rhss) ->
1189 expand n rhss `thenNF_Tc` \ (binds2, rhss') ->
1190 returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss')
1193 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1194 -- e.g. expand 3 [rhs1, rhs2]
1195 -- = ( { x = split rhs1 },
1196 -- [fst x, snd x, rhs2] )
1198 | n `rem` 2 == 0 = go rhss -- n is even
1199 | otherwise = go (tail rhss) `thenNF_Tc` \ (binds', rhss') ->
1200 returnNF_Tc (binds', head rhss : rhss')
1202 go rhss = mapAndUnzipNF_Tc do_one rhss `thenNF_Tc` \ (binds', rhss') ->
1203 returnNF_Tc (andMonoBindList binds', concat rhss')
1205 do_one rhs = tcGetUnique `thenNF_Tc` \ uniq ->
1206 tcLookupGlobalId fstName `thenNF_Tc` \ fst_id ->
1207 tcLookupGlobalId sndName `thenNF_Tc` \ snd_id ->
1209 x = mkUserLocal occ uniq pair_ty loc
1211 returnNF_Tc (VarMonoBind x (mk_app split_id rhs),
1212 [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
1214 mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
1216 mk_app id rhs = HsApp (HsVar id) rhs
1218 addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
1222 %************************************************************************
1224 \subsection[reduce]{@reduce@}
1226 %************************************************************************
1228 When the "what to do" predicate doesn't depend on the quantified type variables,
1229 matters are easier. We don't need to do any zonking, unless the improvement step
1230 does something, in which case we zonk before iterating.
1232 The "given" set is always empty.
1235 simpleReduceLoop :: SDoc
1236 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1238 -> TcM ([Inst], -- Free
1240 [Inst]) -- Irreducible
1242 simpleReduceLoop doc try_me wanteds
1243 = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
1244 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
1245 if no_improvement then
1246 returnTc (frees, binds, irreds)
1248 simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
1249 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1255 reduceContext :: SDoc
1256 -> (Inst -> WhatToDo)
1259 -> NF_TcM (Bool, -- True <=> improve step did no unification
1261 TcDictBinds, -- Dictionary bindings
1262 [Inst]) -- Irreducible
1264 reduceContext doc try_me givens wanteds
1266 traceTc (text "reduceContext" <+> (vcat [
1267 text "----------------------",
1269 text "given" <+> ppr givens,
1270 text "wanted" <+> ppr wanteds,
1271 text "----------------------"
1274 -- Build the Avail mapping from "givens"
1275 foldlNF_Tc addGiven emptyFM givens `thenNF_Tc` \ init_state ->
1278 reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ avails ->
1280 -- Do improvement, using everything in avails
1281 -- In particular, avails includes all superclasses of everything
1282 tcImprove avails `thenTc` \ no_improvement ->
1284 extractResults avails wanteds `thenNF_Tc` \ (binds, irreds, frees) ->
1286 traceTc (text "reduceContext end" <+> (vcat [
1287 text "----------------------",
1289 text "given" <+> ppr givens,
1290 text "wanted" <+> ppr wanteds,
1292 text "avails" <+> pprAvails avails,
1293 text "frees" <+> ppr frees,
1294 text "no_improvement =" <+> ppr no_improvement,
1295 text "----------------------"
1298 returnTc (no_improvement, frees, binds, irreds)
1301 = tcGetInstEnv `thenTc` \ inst_env ->
1303 preds = [ (pred, pp_loc)
1304 | inst <- keysFM avails,
1305 let pp_loc = pprInstLoc (instLoc inst),
1306 pred <- predsOfInst inst,
1309 -- Avails has all the superclasses etc (good)
1310 -- It also has all the intermediates of the deduction (good)
1311 -- It does not have duplicates (good)
1312 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1313 -- so that improve will see them separate
1314 eqns = improve (classInstEnv inst_env) preds
1319 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
1320 mapTc_ unify eqns `thenTc_`
1323 unify ((qtvs, t1, t2), doc)
1324 = tcAddErrCtxt doc $
1325 tcInstTyVars VanillaTv (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
1326 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1329 The main context-reduction function is @reduce@. Here's its game plan.
1332 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1333 -- along with its depth
1334 -> (Inst -> WhatToDo)
1341 try_me: given an inst, this function returns
1343 DontReduce return this in "irreds"
1344 Free return this in "frees"
1346 wanteds: The list of insts to reduce
1347 state: An accumulating parameter of type Avails
1348 that contains the state of the algorithm
1350 It returns a Avails.
1352 The (n,stack) pair is just used for error reporting.
1353 n is always the depth of the stack.
1354 The stack is the stack of Insts being reduced: to produce X
1355 I had to produce Y, to produce Y I had to produce Z, and so on.
1358 reduceList (n,stack) try_me wanteds state
1359 | n > opt_MaxContextReductionDepth
1360 = failWithTc (reduceDepthErr n stack)
1366 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1371 go [] state = returnTc state
1372 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
1375 -- Base case: we're done!
1376 reduce stack try_me wanted state
1377 -- It's the same as an existing inst, or a superclass thereof
1378 | Just avail <- isAvailable state wanted
1379 = if isLinearInst wanted then
1380 addLinearAvailable state avail wanted `thenNF_Tc` \ (state', wanteds') ->
1381 reduceList stack try_me wanteds' state'
1383 returnTc state -- No op for non-linear things
1386 = case try_me wanted of {
1388 DontReduce want_scs -> addIrred want_scs state wanted
1390 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1391 -- First, see if the inst can be reduced to a constant in one step
1392 try_simple (addIrred AddSCs) -- Assume want superclasses
1394 ; Free -> -- It's free so just chuck it upstairs
1395 -- First, see if the inst can be reduced to a constant in one step
1398 ; ReduceMe -> -- It should be reduced
1399 lookupInst wanted `thenNF_Tc` \ lookup_result ->
1400 case lookup_result of
1401 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
1402 addWanted state' wanted rhs wanteds'
1403 SimpleInst rhs -> addWanted state wanted rhs []
1405 NoInstance -> -- No such instance!
1406 -- Add it and its superclasses
1407 addIrred AddSCs state wanted
1411 try_simple do_this_otherwise
1412 = lookupInst wanted `thenNF_Tc` \ lookup_result ->
1413 case lookup_result of
1414 SimpleInst rhs -> addWanted state wanted rhs []
1415 other -> do_this_otherwise state wanted
1420 -------------------------
1421 isAvailable :: Avails -> Inst -> Maybe Avail
1422 isAvailable avails wanted = lookupFM avails wanted
1423 -- NB 1: the Ord instance of Inst compares by the class/type info
1424 -- *not* by unique. So
1425 -- d1::C Int == d2::C Int
1427 addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
1428 addLinearAvailable avails avail wanted
1429 -- avails currently maps [wanted -> avail]
1430 -- Extend avails to reflect a neeed for an extra copy of avail
1432 | Just avail' <- split_avail avail
1433 = returnNF_Tc (addToFM avails wanted avail', [])
1436 = tcLookupGlobalId splitName `thenNF_Tc` \ split_id ->
1437 newMethodAtLoc (instLoc wanted) split_id
1438 [linearInstType wanted] `thenNF_Tc` \ (split_inst,_) ->
1439 returnNF_Tc (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1442 split_avail :: Avail -> Maybe Avail
1443 -- (Just av) if there's a modified version of avail that
1444 -- we can use to replace avail in avails
1445 -- Nothing if there isn't, so we need to create a Linear
1446 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1447 split_avail (Given id used) | not used = Just (Given id True)
1448 | otherwise = Nothing
1449 split_avail Irred = Nothing
1450 split_avail IsFree = Nothing
1451 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1453 -------------------------
1454 addFree :: Avails -> Inst -> NF_TcM Avails
1455 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1456 -- to avails, so that any other equal Insts will be commoned up right
1457 -- here rather than also being tossed upstairs. This is really just
1458 -- an optimisation, and perhaps it is more trouble that it is worth,
1459 -- as the following comments show!
1461 -- NB1: do *not* add superclasses. If we have
1464 -- but a is not bound here, then we *don't* want to derive
1465 -- dn from df here lest we lose sharing.
1467 addFree avails free = returnNF_Tc (addToFM avails free IsFree)
1469 addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
1470 addWanted avails wanted rhs_expr wanteds
1471 -- Do *not* add superclasses as well. Here's an example of why not
1472 -- class Eq a => Foo a b
1473 -- instance Eq a => Foo [a] a
1474 -- If we are reducing
1476 -- we'll first deduce that it holds (via the instance decl). We
1477 -- must not then overwrite the Eq t constraint with a superclass selection!
1478 -- ToDo: this isn't entirely unsatisfactory, because
1479 -- we may also lose some entirely-legitimate sharing this way
1481 = ASSERT( not (wanted `elemFM` avails) )
1482 returnNF_Tc (addToFM avails wanted avail)
1484 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1485 | otherwise = ASSERT( null wanteds ) NoRhs
1487 addGiven :: Avails -> Inst -> NF_TcM Avails
1488 addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
1490 addIrred :: WantSCs -> Avails -> Inst -> NF_TcM Avails
1491 addIrred NoSCs state irred = returnNF_Tc (addToFM state irred Irred)
1492 addIrred AddSCs state irred = addAvailAndSCs state irred Irred
1494 addAvailAndSCs :: Avails -> Inst -> Avail -> NF_TcM Avails
1495 addAvailAndSCs avails wanted avail
1496 = add_scs (addToFM avails wanted avail) wanted
1498 add_scs :: Avails -> Inst -> NF_TcM Avails
1499 -- Add all the superclasses of the Inst to Avails
1500 -- Invariant: the Inst is already in Avails.
1503 | not (isClassDict dict)
1504 = returnNF_Tc avails
1506 | otherwise -- It is a dictionary
1507 = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
1508 foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1510 (clas, tys) = getDictClassTys dict
1511 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1512 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1514 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1515 = case lookupFM avails sc_dict of
1516 Just (Given _ _) -> returnNF_Tc avails -- See Note [SUPER] below
1517 other -> addAvailAndSCs avails sc_dict avail
1519 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1520 avail = Rhs sc_sel_rhs [dict]
1523 Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
1524 and want to deduce (d2:C [a]) where
1526 class Ord a => C a where
1527 instance Ord a => C [a] where ...
1529 Then we'll use the instance decl to deduce C [a] and then add the
1530 superclasses of C [a] to avails. But we must not overwrite the binding
1531 for d1:Ord a (which is given) with a superclass selection or we'll just
1532 build a loop! Hence looking for Given. Crudely, Given is cheaper
1536 %************************************************************************
1538 \section{tcSimplifyTop: defaulting}
1540 %************************************************************************
1543 @tcSimplifyTop@ is called once per module to simplify all the constant
1544 and ambiguous Insts.
1546 We need to be careful of one case. Suppose we have
1548 instance Num a => Num (Foo a b) where ...
1550 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1551 to (Num x), and default x to Int. But what about y??
1553 It's OK: the final zonking stage should zap y to (), which is fine.
1557 tcSimplifyTop :: LIE -> TcM TcDictBinds
1558 tcSimplifyTop wanted_lie
1559 = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenTc` \ (frees, binds, irreds) ->
1560 ASSERT( null frees )
1563 -- All the non-std ones are definite errors
1564 (stds, non_stds) = partition isStdClassTyVarDict irreds
1566 -- Group by type variable
1567 std_groups = equivClasses cmp_by_tyvar stds
1569 -- Pick the ones which its worth trying to disambiguate
1570 (std_oks, std_bads) = partition worth_a_try std_groups
1572 -- Have a try at disambiguation
1573 -- if the type variable isn't bound
1574 -- up with one of the non-standard classes
1575 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1576 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1578 -- Collect together all the bad guys
1579 bad_guys = non_stds ++ concat std_bads
1581 -- Disambiguate the ones that look feasible
1582 mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
1584 -- And complain about the ones that don't
1585 -- This group includes both non-existent instances
1586 -- e.g. Num (IO a) and Eq (Int -> Int)
1587 -- and ambiguous dictionaries
1589 addTopAmbigErrs bad_guys `thenNF_Tc_`
1591 returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1593 wanteds = lieToList wanted_lie
1595 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1597 get_tv d = case getDictClassTys d of
1598 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1599 get_clas d = case getDictClassTys d of
1600 (clas, [ty]) -> clas
1603 If a dictionary constrains a type variable which is
1604 * not mentioned in the environment
1605 * and not mentioned in the type of the expression
1606 then it is ambiguous. No further information will arise to instantiate
1607 the type variable; nor will it be generalised and turned into an extra
1608 parameter to a function.
1610 It is an error for this to occur, except that Haskell provided for
1611 certain rules to be applied in the special case of numeric types.
1613 * at least one of its classes is a numeric class, and
1614 * all of its classes are numeric or standard
1615 then the type variable can be defaulted to the first type in the
1616 default-type list which is an instance of all the offending classes.
1618 So here is the function which does the work. It takes the ambiguous
1619 dictionaries and either resolves them (producing bindings) or
1620 complains. It works by splitting the dictionary list by type
1621 variable, and using @disambigOne@ to do the real business.
1623 @disambigOne@ assumes that its arguments dictionaries constrain all
1624 the same type variable.
1626 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1627 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1628 the most common use of defaulting is code like:
1630 _ccall_ foo `seqPrimIO` bar
1632 Since we're not using the result of @foo@, the result if (presumably)
1636 disambigGroup :: [Inst] -- All standard classes of form (C a)
1640 | any isNumericClass classes -- Guaranteed all standard classes
1641 -- see comment at the end of function for reasons as to
1642 -- why the defaulting mechanism doesn't apply to groups that
1643 -- include CCallable or CReturnable dicts.
1644 && not (any isCcallishClass classes)
1645 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1646 -- SO, TRY DEFAULT TYPES IN ORDER
1648 -- Failure here is caused by there being no type in the
1649 -- default list which can satisfy all the ambiguous classes.
1650 -- For example, if Real a is reqd, but the only type in the
1651 -- default list is Int.
1652 tcGetDefaultTys `thenNF_Tc` \ default_tys ->
1654 try_default [] -- No defaults work, so fail
1657 try_default (default_ty : default_tys)
1658 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1659 -- default_tys instead
1660 tcSimplifyDefault theta `thenTc` \ _ ->
1663 theta = [mkClassPred clas [default_ty] | clas <- classes]
1665 -- See if any default works, and if so bind the type variable to it
1666 -- If not, add an AmbigErr
1667 recoverTc (addAmbigErrs dicts `thenNF_Tc_`
1668 returnTc EmptyMonoBinds) $
1670 try_default default_tys `thenTc` \ chosen_default_ty ->
1672 -- Bind the type variable and reduce the context, for real this time
1673 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
1674 simpleReduceLoop (text "disambig" <+> ppr dicts)
1675 reduceMe dicts `thenTc` \ (frees, binds, ambigs) ->
1676 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1677 warnDefault dicts chosen_default_ty `thenTc_`
1680 | all isCreturnableClass classes
1681 = -- Default CCall stuff to (); we don't even both to check that () is an
1682 -- instance of CReturnable, because we know it is.
1683 unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
1684 returnTc EmptyMonoBinds
1686 | otherwise -- No defaults
1687 = addAmbigErrs dicts `thenNF_Tc_`
1688 returnTc EmptyMonoBinds
1691 tyvar = get_tv (head dicts) -- Should be non-empty
1692 classes = map get_clas dicts
1695 [Aside - why the defaulting mechanism is turned off when
1696 dealing with arguments and results to ccalls.
1698 When typechecking _ccall_s, TcExpr ensures that the external
1699 function is only passed arguments (and in the other direction,
1700 results) of a restricted set of 'native' types. This is
1701 implemented via the help of the pseudo-type classes,
1702 @CReturnable@ (CR) and @CCallable@ (CC.)
1704 The interaction between the defaulting mechanism for numeric
1705 values and CC & CR can be a bit puzzling to the user at times.
1714 What type has 'x' got here? That depends on the default list
1715 in operation, if it is equal to Haskell 98's default-default
1716 of (Integer, Double), 'x' has type Double, since Integer
1717 is not an instance of CR. If the default list is equal to
1718 Haskell 1.4's default-default of (Int, Double), 'x' has type
1721 To try to minimise the potential for surprises here, the
1722 defaulting mechanism is turned off in the presence of
1723 CCallable and CReturnable.
1728 %************************************************************************
1730 \subsection[simple]{@Simple@ versions}
1732 %************************************************************************
1734 Much simpler versions when there are no bindings to make!
1736 @tcSimplifyThetas@ simplifies class-type constraints formed by
1737 @deriving@ declarations and when specialising instances. We are
1738 only interested in the simplified bunch of class/type constraints.
1740 It simplifies to constraints of the form (C a b c) where
1741 a,b,c are type variables. This is required for the context of
1742 instance declarations.
1745 tcSimplifyDeriv :: [TyVar]
1746 -> ThetaType -- Wanted
1747 -> TcM ThetaType -- Needed
1749 tcSimplifyDeriv tyvars theta
1750 = tcInstTyVars VanillaTv tyvars `thenNF_Tc` \ (tvs, _, tenv) ->
1751 -- The main loop may do unification, and that may crash if
1752 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
1753 -- ToDo: what if two of them do get unified?
1754 newDicts DataDeclOrigin (substTheta tenv theta) `thenNF_Tc` \ wanteds ->
1755 simpleReduceLoop doc reduceMe wanteds `thenTc` \ (frees, _, irreds) ->
1756 ASSERT( null frees ) -- reduceMe never returns Free
1758 doptsTc Opt_AllowUndecidableInstances `thenNF_Tc` \ undecidable_ok ->
1760 tv_set = mkVarSet tvs
1761 simpl_theta = map dictPred irreds -- reduceMe squashes all non-dicts
1764 | isEmptyVarSet pred_tyvars -- Things like (Eq T) should be rejected
1765 = addErrTc (noInstErr pred)
1767 | not undecidable_ok && not (isTyVarClassPred pred)
1768 -- Check that the returned dictionaries are all of form (C a b)
1769 -- (where a, b are type variables).
1770 -- We allow this if we had -fallow-undecidable-instances,
1771 -- but note that risks non-termination in the 'deriving' context-inference
1772 -- fixpoint loop. It is useful for situations like
1773 -- data Min h a = E | M a (h a)
1774 -- which gives the instance decl
1775 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
1776 = addErrTc (noInstErr pred)
1778 | not (pred_tyvars `subVarSet` tv_set)
1779 -- Check for a bizarre corner case, when the derived instance decl should
1780 -- have form instance C a b => D (T a) where ...
1781 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
1782 -- of problems; in particular, it's hard to compare solutions for
1783 -- equality when finding the fixpoint. So I just rule it out for now.
1784 = addErrTc (badDerivedPred pred)
1789 pred_tyvars = tyVarsOfPred pred
1791 rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
1792 -- This reverse-mapping is a Royal Pain,
1793 -- but the result should mention TyVars not TcTyVars
1796 mapNF_Tc check_pred simpl_theta `thenNF_Tc_`
1797 checkAmbiguity tvs simpl_theta tv_set `thenTc_`
1798 returnTc (substTheta rev_env simpl_theta)
1800 doc = ptext SLIT("deriving classes for a data type")
1803 @tcSimplifyDefault@ just checks class-type constraints, essentially;
1804 used with \tr{default} declarations. We are only interested in
1805 whether it worked or not.
1808 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
1811 tcSimplifyDefault theta
1812 = newDicts DataDeclOrigin theta `thenNF_Tc` \ wanteds ->
1813 simpleReduceLoop doc reduceMe wanteds `thenTc` \ (frees, _, irreds) ->
1814 ASSERT( null frees ) -- try_me never returns Free
1815 mapNF_Tc (addErrTc . noInstErr) irreds `thenNF_Tc_`
1821 doc = ptext SLIT("default declaration")
1825 %************************************************************************
1827 \section{Errors and contexts}
1829 %************************************************************************
1831 ToDo: for these error messages, should we note the location as coming
1832 from the insts, or just whatever seems to be around in the monad just
1836 groupInsts :: [Inst] -> [[Inst]]
1837 -- Group together insts with the same origin
1838 -- We want to report them together in error messages
1840 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1842 -- (It may seem a bit crude to compare the error messages,
1843 -- but it makes sure that we combine just what the user sees,
1844 -- and it avoids need equality on InstLocs.)
1845 (friends, others) = partition is_friend insts
1846 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1847 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1850 addTopAmbigErrs dicts
1851 = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
1852 mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
1853 mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
1856 fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1857 (tidy_env, tidy_dicts) = tidyInsts dicts
1858 (bad_ips, non_ips) = partition is_ip tidy_dicts
1859 (no_insts, ambigs) = partition no_inst non_ips
1860 is_ip d = any isIPPred (predsOfInst d)
1861 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1864 plural xs = char 's'
1866 addTopIPErrs tidy_env tidy_dicts
1867 = addInstErrTcM (instLoc (head tidy_dicts))
1869 ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1871 -- Used for top-level irreducibles
1872 addTopInstanceErrs tidy_env tidy_dicts
1873 = addInstErrTcM (instLoc (head tidy_dicts))
1875 ptext SLIT("No instance") <> plural tidy_dicts <+>
1876 ptext SLIT("for") <+> pprInsts tidy_dicts)
1879 = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1881 (tidy_env, tidy_dicts) = tidyInsts dicts
1883 addAmbigErr tidy_env tidy_dict
1884 = addInstErrTcM (instLoc tidy_dict)
1886 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1887 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1889 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1891 warnDefault dicts default_ty
1892 = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
1893 tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1896 (_, tidy_dicts) = tidyInsts dicts
1897 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1898 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1899 quotes (ppr default_ty),
1900 pprInstsInFull tidy_dicts]
1902 complainCheck doc givens irreds
1903 = mapNF_Tc zonkInst given_dicts_and_ips `thenNF_Tc` \ givens' ->
1904 mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
1907 given_dicts_and_ips = filter (not . isMethod) givens
1908 -- Filter out methods, which are only added to
1909 -- the given set as an optimisation
1911 addNoInstanceErrs what_doc givens dicts
1912 = getDOptsTc `thenNF_Tc` \ dflags ->
1913 tcGetInstEnv `thenNF_Tc` \ inst_env ->
1915 (tidy_env1, tidy_givens) = tidyInsts givens
1916 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
1918 doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1919 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1921 ptext SLIT("Probable fix:"),
1925 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1926 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1929 -- The error message when we don't find a suitable instance
1930 -- is complicated by the fact that sometimes this is because
1931 -- there is no instance, and sometimes it's because there are
1932 -- too many instances (overlap). See the comments in TcEnv.lhs
1933 -- with the InstEnv stuff.
1936 | not ambig_overlap = empty
1938 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1939 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1940 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1942 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1943 ptext SLIT("to the") <+> what_doc]
1945 fix2 | null instance_dicts
1948 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1950 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1951 -- Insts for which it is worth suggesting an adding an instance declaration
1952 -- Exclude implicit parameters, and tyvar dicts
1954 -- Checks for the ambiguous case when we have overlapping instances
1955 ambig_overlap = any ambig_overlap1 dicts
1958 = case lookupInstEnv dflags inst_env clas tys of
1959 NoMatch ambig -> ambig
1963 (clas,tys) = getDictClassTys dict
1965 addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
1967 -- Used for the ...Thetas variants; all top level
1968 noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
1971 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
1972 ptext SLIT("type variables that are not data type parameters"),
1973 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
1975 reduceDepthErr n stack
1976 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1977 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1978 nest 4 (pprInstsInFull stack)]
1980 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1982 -----------------------------------------------
1984 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1985 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])