2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
15 tcSimplifyDeriv, tcSimplifyDefault,
19 #include "HsVersions.h"
21 import {-# SOURCE #-} TcUnify( unifyTauTy )
23 import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
24 import TcHsSyn ( TcExpr, TcId,
25 TcMonoBinds, TcDictBinds
29 import Inst ( lookupInst, LookupInstResult(..),
30 tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
31 isDict, isClassDict, isLinearInst, linearInstType,
32 isStdClassTyVarDict, isMethodFor, isMethod,
33 instToId, tyVarsOfInsts, cloneDict,
34 ipNamesOfInsts, ipNamesOfInst, dictPred,
35 instBindingRequired, instCanBeGeneralised,
36 newDictsFromOld, newMethodAtLoc,
37 getDictClassTys, isTyVarDict,
38 instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
39 Inst, pprInsts, pprInstsInFull,
40 isIPDict, isInheritableInst
42 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupId )
43 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
46 mkClassPred, isOverloadedTy, mkTyConApp,
47 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
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 splitName, fstName, sndName )
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)
539 TcDictBinds, -- Bindings
540 [TcId]) -- Dict Ids that must be bound here (zonked)
541 -- Any free (escaping) Insts are tossed into the environment
546 tcSimplifyInfer doc tau_tvs wanted_lie
547 = inferLoop doc (varSetElems tau_tvs)
548 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
550 -- Check for non-generalisable insts
551 mappM_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenM_`
553 extendLIEs frees `thenM_`
554 returnM (qtvs, binds, map instToId irreds)
556 inferLoop doc tau_tvs wanteds
558 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
559 mappM zonkInst wanteds `thenM` \ wanteds' ->
560 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
562 preds = fdPredsOfInsts wanteds'
563 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
566 | isFreeWhenInferring qtvs inst = Free
567 | isClassDict inst = DontReduceUnlessConstant -- Dicts
568 | otherwise = ReduceMe -- Lits and Methods
571 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
574 if no_improvement then
575 returnM (varSetElems qtvs, frees, binds, irreds)
577 -- If improvement did some unification, we go round again. There
578 -- are two subtleties:
579 -- a) We start again with irreds, not wanteds
580 -- Using an instance decl might have introduced a fresh type variable
581 -- which might have been unified, so we'd get an infinite loop
582 -- if we started again with wanteds! See example [LOOP]
584 -- b) It's also essential to re-process frees, because unification
585 -- might mean that a type variable that looked free isn't now.
587 -- Hence the (irreds ++ frees)
589 -- However, NOTICE that when we are done, we might have some bindings, but
590 -- the final qtvs might be empty. See [NO TYVARS] below.
592 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
593 returnM (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
598 class If b t e r | b t e -> r
601 class Lte a b c | a b -> c where lte :: a -> b -> c
603 instance (Lte a b l,If l b a c) => Max a b c
605 Wanted: Max Z (S x) y
607 Then we'll reduce using the Max instance to:
608 (Lte Z (S x) l, If l (S x) Z y)
609 and improve by binding l->T, after which we can do some reduction
610 on both the Lte and If constraints. What we *can't* do is start again
611 with (Max Z (S x) y)!
615 class Y a b | a -> b where
618 instance Y [[a]] a where
621 k :: X a -> X a -> X a
623 g :: Num a => [X a] -> [X a]
626 h ys = ys ++ map (k (y [[0]])) xs
628 The excitement comes when simplifying the bindings for h. Initially
629 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
630 From this we get t1:=:t2, but also various bindings. We can't forget
631 the bindings (because of [LOOP]), but in fact t1 is what g is
634 The net effect of [NO TYVARS]
637 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
638 isFreeWhenInferring qtvs inst
639 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
640 && isInheritableInst inst -- And no implicit parameter involved
641 -- (see "Notes on implicit parameters")
643 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
644 -> NameSet -- Quantified implicit parameters
646 isFreeWhenChecking qtvs ips inst
647 = isFreeWrtTyVars qtvs inst
648 && isFreeWrtIPs ips inst
650 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
651 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
655 %************************************************************************
657 \subsection{tcSimplifyCheck}
659 %************************************************************************
661 @tcSimplifyCheck@ is used when we know exactly the set of variables
662 we are going to quantify over. For example, a class or instance declaration.
667 -> [TcTyVar] -- Quantify over these
670 -> TcM TcDictBinds -- Bindings
672 -- tcSimplifyCheck is used when checking expression type signatures,
673 -- class decls, instance decls etc.
675 -- NB: tcSimplifyCheck does not consult the
676 -- global type variables in the environment; so you don't
677 -- need to worry about setting them before calling tcSimplifyCheck
678 tcSimplifyCheck doc qtvs givens wanted_lie
679 = tcSimplCheck doc get_qtvs
680 givens wanted_lie `thenM` \ (qtvs', binds) ->
683 get_qtvs = zonkTcTyVarsAndFV qtvs
686 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
687 -- against, but we don't know the type variables over which we are going to quantify.
688 -- This happens when we have a type signature for a mutually recursive group
691 -> TcTyVarSet -- fv(T)
694 -> 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 `thenM` \ all_tvs' ->
712 tcGetGlobalTyVars `thenM` \ 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 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
728 -- Complain about any irreducible ones
729 complainCheck doc givens irreds `thenM_`
732 extendLIEs frees `thenM_`
733 returnM (qtvs, binds)
736 ip_set = mkNameSet (ipNamesOfInsts givens)
738 check_loop givens wanteds
740 mappM zonkInst givens `thenM` \ givens' ->
741 mappM zonkInst wanteds `thenM` \ wanteds' ->
742 get_qtvs `thenM` \ qtvs' ->
746 -- When checking against a given signature we always reduce
747 -- until we find a match against something given, or can't reduce
748 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
749 | otherwise = ReduceMe
751 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
754 if no_improvement then
755 returnM (varSetElems qtvs', frees, binds, irreds)
757 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
758 returnM (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
762 %************************************************************************
764 \subsection{tcSimplifyRestricted}
766 %************************************************************************
769 tcSimplifyRestricted -- Used for restricted binding groups
770 -- i.e. ones subject to the monomorphism restriction
772 -> TcTyVarSet -- Free in the type of the RHSs
773 -> [Inst] -- Free in the RHSs
774 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
775 TcDictBinds) -- Bindings
777 tcSimplifyRestricted doc tau_tvs wanteds
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 try_me inst = ReduceMe -- Reduce as far as we can. Don't stop at
788 -- dicts; the idea is to get rid of as many type
789 -- variables as possible, and we don't want to stop
790 -- at (say) Monad (ST s), because that reduces
791 -- immediately, with no constraint on s.
793 simpleReduceLoop doc try_me wanteds `thenM` \ (_, _, constrained_dicts) ->
795 -- Next, figure out the tyvars we will quantify over
796 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
797 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
799 constrained_tvs = tyVarsOfInsts constrained_dicts
800 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs)
801 `minusVarSet` constrained_tvs
804 -- The first step may have squashed more methods than
805 -- necessary, so try again, this time knowing the exact
806 -- set of type variables to quantify over.
808 -- We quantify only over constraints that are captured by qtvs;
809 -- these will just be a subset of non-dicts. This in contrast
810 -- to normal inference (using isFreeWhenInferring) in which we quantify over
811 -- all *non-inheritable* constraints too. This implements choice
812 -- (B) under "implicit parameter and monomorphism" above.
814 -- Remember that we may need to do *some* simplification, to
815 -- (for example) squash {Monad (ST s)} into {}. It's not enough
816 -- just to float all constraints
817 mappM zonkInst wanteds `thenM` \ wanteds' ->
819 try_me inst | isFreeWrtTyVars qtvs inst = Free
820 | otherwise = ReduceMe
822 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
823 ASSERT( no_improvement )
824 ASSERT( null irreds )
825 -- No need to loop because simpleReduceLoop will have
826 -- already done any improvement necessary
828 extendLIEs frees `thenM_`
829 returnM (varSetElems qtvs, 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 :: [Inst] -> TcM (TcDictBinds)
880 tcSimplifyToDicts wanteds
881 = simpleReduceLoop doc try_me wanteds `thenM` \ (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 extendLIEs irreds `thenM_`
889 doc = text "tcSimplifyToDicts"
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
898 tcSimplifyBracket is used when simplifying the constraints arising from
899 a Template Haskell bracket [| ... |]. We want to check that there aren't
900 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
901 Show instance), but we aren't otherwise interested in the results.
902 Nor do we care about ambiguous dictionaries etc. We will type check
903 this bracket again at its usage site.
906 tcSimplifyBracket :: [Inst] -> TcM ()
907 tcSimplifyBracket wanteds
908 = simpleReduceLoop doc try_me wanteds `thenM_`
912 doc = text "tcSimplifyBracket"
913 try_me inst = ReduceMe
917 %************************************************************************
919 \subsection{Filtering at a dynamic binding}
921 %************************************************************************
926 we must discharge all the ?x constraints from B. We also do an improvement
927 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
929 Actually, the constraints from B might improve the types in ?x. For example
931 f :: (?x::Int) => Char -> Char
934 then the constraint (?x::Int) arising from the call to f will
935 force the binding for ?x to be of type Int.
938 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
941 tcSimplifyIPs given_ips wanteds
942 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
943 extendLIEs frees `thenM_`
946 doc = text "tcSimplifyIPs" <+> ppr given_ips
947 ip_set = mkNameSet (ipNamesOfInsts given_ips)
949 -- Simplify any methods that mention the implicit parameter
950 try_me inst | isFreeWrtIPs ip_set inst = Free
951 | otherwise = ReduceMe
953 simpl_loop givens wanteds
954 = mappM zonkInst givens `thenM` \ givens' ->
955 mappM zonkInst wanteds `thenM` \ wanteds' ->
957 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
959 if no_improvement then
960 ASSERT( null irreds )
961 returnM (frees, binds)
963 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
964 returnM (frees1, binds `AndMonoBinds` binds1)
968 %************************************************************************
970 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
972 %************************************************************************
974 When doing a binding group, we may have @Insts@ of local functions.
975 For example, we might have...
977 let f x = x + 1 -- orig local function (overloaded)
978 f.1 = f Int -- two instances of f
983 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
984 where @f@ is in scope; those @Insts@ must certainly not be passed
985 upwards towards the top-level. If the @Insts@ were binding-ified up
986 there, they would have unresolvable references to @f@.
988 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
989 For each method @Inst@ in the @init_lie@ that mentions one of the
990 @Ids@, we create a binding. We return the remaining @Insts@ (in an
991 @LIE@), as well as the @HsBinds@ generated.
994 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcMonoBinds
996 bindInstsOfLocalFuns wanteds local_ids
997 | null overloaded_ids
999 = extendLIEs wanteds `thenM_`
1000 returnM EmptyMonoBinds
1003 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1004 ASSERT( null irreds )
1005 extendLIEs frees `thenM_`
1008 doc = text "bindInsts" <+> ppr local_ids
1009 overloaded_ids = filter is_overloaded local_ids
1010 is_overloaded id = isOverloadedTy (idType id)
1012 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1013 -- so it's worth building a set, so that
1014 -- lookup (in isMethodFor) is faster
1016 try_me inst | isMethodFor overloaded_set inst = ReduceMe
1021 %************************************************************************
1023 \subsection{Data types for the reduction mechanism}
1025 %************************************************************************
1027 The main control over context reduction is here
1031 = ReduceMe -- Try to reduce this
1032 -- If there's no instance, behave exactly like
1033 -- DontReduce: add the inst to
1034 -- the irreductible ones, but don't
1035 -- produce an error message of any kind.
1036 -- It might be quite legitimate such as (Eq a)!
1038 | DontReduce WantSCs -- Return as irreducible
1040 | DontReduceUnlessConstant -- Return as irreducible unless it can
1041 -- be reduced to a constant in one step
1043 | Free -- Return as free
1045 reduceMe :: Inst -> WhatToDo
1046 reduceMe inst = ReduceMe
1048 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1049 -- of a predicate when adding it to the avails
1055 type Avails = FiniteMap Inst Avail
1058 = IsFree -- Used for free Insts
1059 | Irred -- Used for irreducible dictionaries,
1060 -- which are going to be lambda bound
1062 | Given TcId -- Used for dictionaries for which we have a binding
1063 -- e.g. those "given" in a signature
1064 Bool -- True <=> actually consumed (splittable IPs only)
1066 | NoRhs -- Used for Insts like (CCallable f)
1067 -- where no witness is required.
1069 | Rhs -- Used when there is a RHS
1071 [Inst] -- Insts free in the RHS; we need these too
1073 | Linear -- Splittable Insts only.
1074 Int -- The Int is always 2 or more; indicates how
1075 -- many copies are required
1076 Inst -- The splitter
1077 Avail -- Where the "master copy" is
1079 | LinRhss -- Splittable Insts only; this is used only internally
1080 -- by extractResults, where a Linear
1081 -- is turned into an LinRhss
1082 [TcExpr] -- A supply of suitable RHSs
1084 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1085 | (inst,avail) <- fmToList avails ]
1087 instance Outputable Avail where
1090 pprAvail NoRhs = text "<no rhs>"
1091 pprAvail IsFree = text "Free"
1092 pprAvail Irred = text "Irred"
1093 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1094 if b then text "(used)" else empty
1095 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1096 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1097 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1100 Extracting the bindings from a bunch of Avails.
1101 The bindings do *not* come back sorted in dependency order.
1102 We assume that they'll be wrapped in a big Rec, so that the
1103 dependency analyser can sort them out later
1107 extractResults :: Avails
1109 -> TcM (TcDictBinds, -- Bindings
1110 [Inst], -- Irreducible ones
1111 [Inst]) -- Free ones
1113 extractResults avails wanteds
1114 = go avails EmptyMonoBinds [] [] wanteds
1116 go avails binds irreds frees []
1117 = returnM (binds, irreds, frees)
1119 go avails binds irreds frees (w:ws)
1120 = case lookupFM avails w of
1121 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1122 go avails binds irreds frees ws
1124 Just NoRhs -> go avails binds irreds frees ws
1125 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1126 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1128 Just (Given id _) -> go avails new_binds irreds frees ws
1130 new_binds | id == instToId w = binds
1131 | otherwise = addBind binds w (HsVar id)
1132 -- The sought Id can be one of the givens, via a superclass chain
1133 -- and then we definitely don't want to generate an x=x binding!
1135 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1137 new_binds = addBind binds w rhs
1139 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1140 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1141 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1142 go (addToFM avails w (LinRhss rhss))
1143 (binds `AndMonoBinds` binds')
1144 irreds' frees' (split_inst : w : ws)
1146 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1147 -> go new_avails new_binds irreds frees ws
1149 new_binds = addBind binds w rhs
1150 new_avails = addToFM avails w (LinRhss rhss)
1152 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1153 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1154 returnM (w':irreds, frees, instToId w')
1155 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1156 returnM (irreds, w':frees, instToId w')
1159 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1160 | otherwise = addToFM avails w NoRhs
1161 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1162 -- than Given, else we end up with bogus bindings.
1164 add_free avails w | isMethod w = avails
1165 | otherwise = add_given avails w
1167 -- Do *not* replace Free by Given if it's a method.
1168 -- The following situation shows why this is bad:
1169 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1170 -- From an application (truncate f i) we get
1171 -- t1 = truncate at f
1173 -- If we have also have a second occurrence of truncate, we get
1174 -- t3 = truncate at f
1176 -- When simplifying with i,f free, we might still notice that
1177 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1178 -- will continue to float out!
1179 -- (split n i a) returns: n rhss
1180 -- auxiliary bindings
1181 -- 1 or 0 insts to add to irreds
1184 split :: Int -> TcId -> TcId -> Inst
1185 -> TcM (TcDictBinds, [TcExpr])
1186 -- (split n split_id root_id wanted) returns
1187 -- * a list of 'n' expressions, all of which witness 'avail'
1188 -- * a bunch of auxiliary bindings to support these expressions
1189 -- * one or zero insts needed to witness the whole lot
1190 -- (maybe be zero if the initial Inst is a Given)
1192 -- NB: 'wanted' is just a template
1194 split n split_id root_id wanted
1197 ty = linearInstType wanted
1198 pair_ty = mkTyConApp pairTyCon [ty,ty]
1199 id = instToId wanted
1203 go 1 = returnM (EmptyMonoBinds, [HsVar root_id])
1205 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1206 expand n rhss `thenM` \ (binds2, rhss') ->
1207 returnM (binds1 `AndMonoBinds` binds2, rhss')
1210 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1211 -- e.g. expand 3 [rhs1, rhs2]
1212 -- = ( { x = split rhs1 },
1213 -- [fst x, snd x, rhs2] )
1215 | n `rem` 2 == 0 = go rhss -- n is even
1216 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1217 returnM (binds', head rhss : rhss')
1219 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1220 returnM (andMonoBindList binds', concat rhss')
1222 do_one rhs = newUnique `thenM` \ uniq ->
1223 tcLookupId fstName `thenM` \ fst_id ->
1224 tcLookupId sndName `thenM` \ snd_id ->
1226 x = mkUserLocal occ uniq pair_ty loc
1228 returnM (VarMonoBind x (mk_app split_id rhs),
1229 [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
1231 mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
1233 mk_app id rhs = HsApp (HsVar id) rhs
1235 addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
1239 %************************************************************************
1241 \subsection[reduce]{@reduce@}
1243 %************************************************************************
1245 When the "what to do" predicate doesn't depend on the quantified type variables,
1246 matters are easier. We don't need to do any zonking, unless the improvement step
1247 does something, in which case we zonk before iterating.
1249 The "given" set is always empty.
1252 simpleReduceLoop :: SDoc
1253 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1255 -> TcM ([Inst], -- Free
1257 [Inst]) -- Irreducible
1259 simpleReduceLoop doc try_me wanteds
1260 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1261 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1262 if no_improvement then
1263 returnM (frees, binds, irreds)
1265 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1266 returnM (frees1, binds `AndMonoBinds` binds1, irreds1)
1272 reduceContext :: SDoc
1273 -> (Inst -> WhatToDo)
1276 -> TcM (Bool, -- True <=> improve step did no unification
1278 TcDictBinds, -- Dictionary bindings
1279 [Inst]) -- Irreducible
1281 reduceContext doc try_me givens wanteds
1283 traceTc (text "reduceContext" <+> (vcat [
1284 text "----------------------",
1286 text "given" <+> ppr givens,
1287 text "wanted" <+> ppr wanteds,
1288 text "----------------------"
1291 -- Build the Avail mapping from "givens"
1292 foldlM addGiven emptyFM givens `thenM` \ init_state ->
1295 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1297 -- Do improvement, using everything in avails
1298 -- In particular, avails includes all superclasses of everything
1299 tcImprove avails `thenM` \ no_improvement ->
1301 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1303 traceTc (text "reduceContext end" <+> (vcat [
1304 text "----------------------",
1306 text "given" <+> ppr givens,
1307 text "wanted" <+> ppr wanteds,
1309 text "avails" <+> pprAvails avails,
1310 text "frees" <+> ppr frees,
1311 text "no_improvement =" <+> ppr no_improvement,
1312 text "----------------------"
1315 returnM (no_improvement, frees, binds, irreds)
1318 = tcGetInstEnv `thenM` \ inst_env ->
1320 preds = [ (pred, pp_loc)
1321 | inst <- keysFM avails,
1322 let pp_loc = pprInstLoc (instLoc inst),
1323 pred <- fdPredsOfInst inst
1325 -- Avails has all the superclasses etc (good)
1326 -- It also has all the intermediates of the deduction (good)
1327 -- It does not have duplicates (good)
1328 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1329 -- so that improve will see them separate
1330 eqns = improve (classInstEnv inst_env) preds
1335 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1336 mappM_ unify eqns `thenM_`
1339 unify ((qtvs, t1, t2), doc)
1341 tcInstTyVars VanillaTv (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1342 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1345 The main context-reduction function is @reduce@. Here's its game plan.
1348 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1349 -- along with its depth
1350 -> (Inst -> WhatToDo)
1357 try_me: given an inst, this function returns
1359 DontReduce return this in "irreds"
1360 Free return this in "frees"
1362 wanteds: The list of insts to reduce
1363 state: An accumulating parameter of type Avails
1364 that contains the state of the algorithm
1366 It returns a Avails.
1368 The (n,stack) pair is just used for error reporting.
1369 n is always the depth of the stack.
1370 The stack is the stack of Insts being reduced: to produce X
1371 I had to produce Y, to produce Y I had to produce Z, and so on.
1374 reduceList (n,stack) try_me wanteds state
1375 | n > opt_MaxContextReductionDepth
1376 = failWithTc (reduceDepthErr n stack)
1382 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1387 go [] state = returnM state
1388 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1391 -- Base case: we're done!
1392 reduce stack try_me wanted state
1393 -- It's the same as an existing inst, or a superclass thereof
1394 | Just avail <- isAvailable state wanted
1395 = if isLinearInst wanted then
1396 addLinearAvailable state avail wanted `thenM` \ (state', wanteds') ->
1397 reduceList stack try_me wanteds' state'
1399 returnM state -- No op for non-linear things
1402 = case try_me wanted of {
1404 DontReduce want_scs -> addIrred want_scs state wanted
1406 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1407 -- First, see if the inst can be reduced to a constant in one step
1408 try_simple (addIrred AddSCs) -- Assume want superclasses
1410 ; Free -> -- It's free so just chuck it upstairs
1411 -- First, see if the inst can be reduced to a constant in one step
1414 ; ReduceMe -> -- It should be reduced
1415 lookupInst wanted `thenM` \ lookup_result ->
1416 case lookup_result of
1417 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenM` \ state' ->
1418 addWanted state' wanted rhs wanteds'
1419 SimpleInst rhs -> addWanted state wanted rhs []
1421 NoInstance -> -- No such instance!
1422 -- Add it and its superclasses
1423 addIrred AddSCs state wanted
1427 try_simple do_this_otherwise
1428 = lookupInst wanted `thenM` \ lookup_result ->
1429 case lookup_result of
1430 SimpleInst rhs -> addWanted state wanted rhs []
1431 other -> do_this_otherwise state wanted
1436 -------------------------
1437 isAvailable :: Avails -> Inst -> Maybe Avail
1438 isAvailable avails wanted = lookupFM avails wanted
1439 -- NB 1: the Ord instance of Inst compares by the class/type info
1440 -- *not* by unique. So
1441 -- d1::C Int == d2::C Int
1443 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1444 addLinearAvailable avails avail wanted
1445 -- avails currently maps [wanted -> avail]
1446 -- Extend avails to reflect a neeed for an extra copy of avail
1448 | Just avail' <- split_avail avail
1449 = returnM (addToFM avails wanted avail', [])
1452 = tcLookupId splitName `thenM` \ split_id ->
1453 newMethodAtLoc (instLoc wanted) split_id
1454 [linearInstType wanted] `thenM` \ split_inst ->
1455 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1458 split_avail :: Avail -> Maybe Avail
1459 -- (Just av) if there's a modified version of avail that
1460 -- we can use to replace avail in avails
1461 -- Nothing if there isn't, so we need to create a Linear
1462 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1463 split_avail (Given id used) | not used = Just (Given id True)
1464 | otherwise = Nothing
1465 split_avail Irred = Nothing
1466 split_avail IsFree = Nothing
1467 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1469 -------------------------
1470 addFree :: Avails -> Inst -> TcM Avails
1471 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1472 -- to avails, so that any other equal Insts will be commoned up right
1473 -- here rather than also being tossed upstairs. This is really just
1474 -- an optimisation, and perhaps it is more trouble that it is worth,
1475 -- as the following comments show!
1477 -- NB: do *not* add superclasses. If we have
1480 -- but a is not bound here, then we *don't* want to derive
1481 -- dn from df here lest we lose sharing.
1483 addFree avails free = returnM (addToFM avails free IsFree)
1485 addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> TcM Avails
1486 addWanted avails wanted rhs_expr wanteds
1487 = ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
1488 addAvailAndSCs avails wanted avail
1490 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1491 | otherwise = ASSERT( null wanteds ) NoRhs
1493 addGiven :: Avails -> Inst -> TcM Avails
1494 addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
1495 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1496 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1497 -- so the assert isn't true
1499 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1500 addIrred NoSCs avails irred = returnM (addToFM avails irred Irred)
1501 addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1502 addAvailAndSCs avails irred Irred
1504 addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
1505 addAvailAndSCs avails inst avail
1506 | not (isClassDict inst) = returnM avails1
1507 | otherwise = addSCs is_loop avails1 inst
1509 avails1 = addToFM avails inst avail
1510 is_loop inst = inst `elem` deps -- Note: this compares by *type*, not by Unique
1511 deps = findAllDeps avails avail
1513 findAllDeps :: Avails -> Avail -> [Inst]
1514 -- Find all the Insts that this one depends on
1515 -- See Note [SUPERCLASS-LOOP]
1516 findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
1517 findAllDeps avails other = []
1519 find_all_deps_help :: Avails -> Inst -> [Inst]
1520 find_all_deps_help avails inst
1521 = case lookupFM avails inst of
1522 Just avail -> findAllDeps avails avail
1525 addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
1526 -- Add all the superclasses of the Inst to Avails
1527 -- The first param says "dont do this because the original thing
1528 -- depends on this one, so you'd build a loop"
1529 -- Invariant: the Inst is already in Avails.
1531 addSCs is_loop avails dict
1532 = newDictsFromOld dict sc_theta' `thenM` \ sc_dicts ->
1533 foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1535 (clas, tys) = getDictClassTys dict
1536 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1537 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1539 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1540 = case lookupFM avails sc_dict of
1541 Just (Given _ _) -> returnM avails -- Given is cheaper than
1542 -- a superclass selection
1543 Just other | is_loop sc_dict -> returnM avails -- See Note [SUPERCLASS-LOOP]
1544 | otherwise -> returnM avails' -- SCs already added
1546 Nothing -> addSCs is_loop avails' sc_dict
1548 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1549 avail = Rhs sc_sel_rhs [dict]
1550 avails' = addToFM avails sc_dict avail
1553 Note [SUPERCLASS-LOOP]: Checking for loops
1554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1555 We have to be careful here. If we are *given* d1:Ord a,
1556 and want to deduce (d2:C [a]) where
1558 class Ord a => C a where
1559 instance Ord a => C [a] where ...
1561 Then we'll use the instance decl to deduce C [a] and then add the
1562 superclasses of C [a] to avails. But we must not overwrite the binding
1563 for d1:Ord a (which is given) with a superclass selection or we'll just
1566 Here's another example
1567 class Eq b => Foo a b
1568 instance Eq a => Foo [a] a
1572 we'll first deduce that it holds (via the instance decl). We must not
1573 then overwrite the Eq t constraint with a superclass selection!
1575 At first I had a gross hack, whereby I simply did not add superclass constraints
1576 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1577 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1578 I found a very obscure program (now tcrun021) in which improvement meant the
1579 simplifier got two bites a the cherry... so something seemed to be an Irred
1580 first time, but reducible next time.
1582 Now we implement the Right Solution, which is to check for loops directly
1583 when adding superclasses. It's a bit like the occurs check in unification.
1587 %************************************************************************
1589 \section{tcSimplifyTop: defaulting}
1591 %************************************************************************
1594 @tcSimplifyTop@ is called once per module to simplify all the constant
1595 and ambiguous Insts.
1597 We need to be careful of one case. Suppose we have
1599 instance Num a => Num (Foo a b) where ...
1601 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1602 to (Num x), and default x to Int. But what about y??
1604 It's OK: the final zonking stage should zap y to (), which is fine.
1608 tcSimplifyTop :: [Inst] -> TcM TcDictBinds
1609 tcSimplifyTop wanteds
1610 = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenM` \ (frees, binds, irreds) ->
1611 ASSERT( null frees )
1614 -- All the non-std ones are definite errors
1615 (stds, non_stds) = partition isStdClassTyVarDict irreds
1617 -- Group by type variable
1618 std_groups = equivClasses cmp_by_tyvar stds
1620 -- Pick the ones which its worth trying to disambiguate
1621 -- namely, the onese whose type variable isn't bound
1622 -- up with one of the non-standard classes
1623 (std_oks, std_bads) = partition worth_a_try std_groups
1624 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1625 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1627 -- Collect together all the bad guys
1628 bad_guys = non_stds ++ concat std_bads
1629 (tidy_env, tidy_dicts) = tidyInsts bad_guys
1630 (bad_ips, non_ips) = partition isIPDict tidy_dicts
1631 (no_insts, ambigs) = partition no_inst non_ips
1632 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1633 fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
1636 -- Report definite errors
1637 mappM (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenM_`
1638 mappM (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenM_`
1640 -- Deal with ambiguity errors, but only if
1641 -- if there has not been an error so far; errors often
1642 -- give rise to spurious ambiguous Insts
1643 ifErrsM (returnM []) (
1645 -- Complain about the ones that don't fall under
1646 -- the Haskell rules for disambiguation
1647 -- This group includes both non-existent instances
1648 -- e.g. Num (IO a) and Eq (Int -> Int)
1649 -- and ambiguous dictionaries
1651 mappM (addAmbigErr tidy_env) ambigs `thenM_`
1653 -- Disambiguate the ones that look feasible
1654 mappM disambigGroup std_oks
1655 ) `thenM` \ binds_ambig ->
1657 returnM (binds `andMonoBinds` andMonoBindList binds_ambig)
1659 ----------------------------------
1660 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1662 get_tv d = case getDictClassTys d of
1663 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1664 get_clas d = case getDictClassTys d of
1665 (clas, [ty]) -> clas
1668 If a dictionary constrains a type variable which is
1669 * not mentioned in the environment
1670 * and not mentioned in the type of the expression
1671 then it is ambiguous. No further information will arise to instantiate
1672 the type variable; nor will it be generalised and turned into an extra
1673 parameter to a function.
1675 It is an error for this to occur, except that Haskell provided for
1676 certain rules to be applied in the special case of numeric types.
1678 * at least one of its classes is a numeric class, and
1679 * all of its classes are numeric or standard
1680 then the type variable can be defaulted to the first type in the
1681 default-type list which is an instance of all the offending classes.
1683 So here is the function which does the work. It takes the ambiguous
1684 dictionaries and either resolves them (producing bindings) or
1685 complains. It works by splitting the dictionary list by type
1686 variable, and using @disambigOne@ to do the real business.
1688 @disambigOne@ assumes that its arguments dictionaries constrain all
1689 the same type variable.
1691 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1692 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1693 the most common use of defaulting is code like:
1695 _ccall_ foo `seqPrimIO` bar
1697 Since we're not using the result of @foo@, the result if (presumably)
1701 disambigGroup :: [Inst] -- All standard classes of form (C a)
1705 | any isNumericClass classes -- Guaranteed all standard classes
1706 -- see comment at the end of function for reasons as to
1707 -- why the defaulting mechanism doesn't apply to groups that
1708 -- include CCallable or CReturnable dicts.
1709 && not (any isCcallishClass classes)
1710 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1711 -- SO, TRY DEFAULT TYPES IN ORDER
1713 -- Failure here is caused by there being no type in the
1714 -- default list which can satisfy all the ambiguous classes.
1715 -- For example, if Real a is reqd, but the only type in the
1716 -- default list is Int.
1717 getDefaultTys `thenM` \ default_tys ->
1719 try_default [] -- No defaults work, so fail
1722 try_default (default_ty : default_tys)
1723 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1724 -- default_tys instead
1725 tcSimplifyDefault theta `thenM` \ _ ->
1728 theta = [mkClassPred clas [default_ty] | clas <- classes]
1730 -- See if any default works, and if so bind the type variable to it
1731 -- If not, add an AmbigErr
1732 recoverM (addAmbigErrs dicts `thenM_`
1733 returnM EmptyMonoBinds) $
1735 try_default default_tys `thenM` \ chosen_default_ty ->
1737 -- Bind the type variable and reduce the context, for real this time
1738 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenM_`
1739 simpleReduceLoop (text "disambig" <+> ppr dicts)
1740 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
1741 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1742 warnDefault dicts chosen_default_ty `thenM_`
1745 | all isCreturnableClass classes
1746 = -- Default CCall stuff to (); we don't even both to check that () is an
1747 -- instance of CReturnable, because we know it is.
1748 unifyTauTy (mkTyVarTy tyvar) unitTy `thenM_`
1749 returnM EmptyMonoBinds
1751 | otherwise -- No defaults
1752 = addAmbigErrs dicts `thenM_`
1753 returnM EmptyMonoBinds
1756 tyvar = get_tv (head dicts) -- Should be non-empty
1757 classes = map get_clas dicts
1760 [Aside - why the defaulting mechanism is turned off when
1761 dealing with arguments and results to ccalls.
1763 When typechecking _ccall_s, TcExpr ensures that the external
1764 function is only passed arguments (and in the other direction,
1765 results) of a restricted set of 'native' types. This is
1766 implemented via the help of the pseudo-type classes,
1767 @CReturnable@ (CR) and @CCallable@ (CC.)
1769 The interaction between the defaulting mechanism for numeric
1770 values and CC & CR can be a bit puzzling to the user at times.
1779 What type has 'x' got here? That depends on the default list
1780 in operation, if it is equal to Haskell 98's default-default
1781 of (Integer, Double), 'x' has type Double, since Integer
1782 is not an instance of CR. If the default list is equal to
1783 Haskell 1.4's default-default of (Int, Double), 'x' has type
1786 To try to minimise the potential for surprises here, the
1787 defaulting mechanism is turned off in the presence of
1788 CCallable and CReturnable.
1793 %************************************************************************
1795 \subsection[simple]{@Simple@ versions}
1797 %************************************************************************
1799 Much simpler versions when there are no bindings to make!
1801 @tcSimplifyThetas@ simplifies class-type constraints formed by
1802 @deriving@ declarations and when specialising instances. We are
1803 only interested in the simplified bunch of class/type constraints.
1805 It simplifies to constraints of the form (C a b c) where
1806 a,b,c are type variables. This is required for the context of
1807 instance declarations.
1810 tcSimplifyDeriv :: [TyVar]
1811 -> ThetaType -- Wanted
1812 -> TcM ThetaType -- Needed
1814 tcSimplifyDeriv tyvars theta
1815 = tcInstTyVars VanillaTv tyvars `thenM` \ (tvs, _, tenv) ->
1816 -- The main loop may do unification, and that may crash if
1817 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
1818 -- ToDo: what if two of them do get unified?
1819 newDicts DataDeclOrigin (substTheta tenv theta) `thenM` \ wanteds ->
1820 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
1821 ASSERT( null frees ) -- reduceMe never returns Free
1823 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
1825 tv_set = mkVarSet tvs
1826 simpl_theta = map dictPred irreds -- reduceMe squashes all non-dicts
1829 | isEmptyVarSet pred_tyvars -- Things like (Eq T) should be rejected
1830 = addErrTc (noInstErr pred)
1832 | not undecidable_ok && not (isTyVarClassPred pred)
1833 -- Check that the returned dictionaries are all of form (C a b)
1834 -- (where a, b are type variables).
1835 -- We allow this if we had -fallow-undecidable-instances,
1836 -- but note that risks non-termination in the 'deriving' context-inference
1837 -- fixpoint loop. It is useful for situations like
1838 -- data Min h a = E | M a (h a)
1839 -- which gives the instance decl
1840 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
1841 = addErrTc (noInstErr pred)
1843 | not (pred_tyvars `subVarSet` tv_set)
1844 -- Check for a bizarre corner case, when the derived instance decl should
1845 -- have form instance C a b => D (T a) where ...
1846 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
1847 -- of problems; in particular, it's hard to compare solutions for
1848 -- equality when finding the fixpoint. So I just rule it out for now.
1849 = addErrTc (badDerivedPred pred)
1854 pred_tyvars = tyVarsOfPred pred
1856 rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
1857 -- This reverse-mapping is a Royal Pain,
1858 -- but the result should mention TyVars not TcTyVars
1861 mappM check_pred simpl_theta `thenM_`
1862 checkAmbiguity tvs simpl_theta tv_set `thenM_`
1863 returnM (substTheta rev_env simpl_theta)
1865 doc = ptext SLIT("deriving classes for a data type")
1868 @tcSimplifyDefault@ just checks class-type constraints, essentially;
1869 used with \tr{default} declarations. We are only interested in
1870 whether it worked or not.
1873 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
1876 tcSimplifyDefault theta
1877 = newDicts DataDeclOrigin theta `thenM` \ wanteds ->
1878 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
1879 ASSERT( null frees ) -- try_me never returns Free
1880 mappM (addErrTc . noInstErr) irreds `thenM_`
1886 doc = ptext SLIT("default declaration")
1890 %************************************************************************
1892 \section{Errors and contexts}
1894 %************************************************************************
1896 ToDo: for these error messages, should we note the location as coming
1897 from the insts, or just whatever seems to be around in the monad just
1901 groupInsts :: [Inst] -> [[Inst]]
1902 -- Group together insts with the same origin
1903 -- We want to report them together in error messages
1905 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1907 -- (It may seem a bit crude to compare the error messages,
1908 -- but it makes sure that we combine just what the user sees,
1909 -- and it avoids need equality on InstLocs.)
1910 (friends, others) = partition is_friend insts
1911 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1912 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1915 plural xs = char 's'
1917 addTopIPErrs tidy_env tidy_dicts
1918 = addInstErrTcM (instLoc (head tidy_dicts))
1920 ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1922 -- Used for top-level irreducibles
1923 addTopInstanceErrs tidy_env tidy_dicts
1924 = addInstErrTcM (instLoc (head tidy_dicts))
1926 ptext SLIT("No instance") <> plural tidy_dicts <+>
1927 ptext SLIT("for") <+> pprInsts tidy_dicts)
1930 = mappM (addAmbigErr tidy_env) tidy_dicts
1932 (tidy_env, tidy_dicts) = tidyInsts dicts
1934 addAmbigErr tidy_env tidy_dict
1935 = addInstErrTcM (instLoc tidy_dict)
1937 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1938 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1940 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1942 warnDefault dicts default_ty
1943 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
1944 addSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1947 (_, tidy_dicts) = tidyInsts dicts
1948 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1949 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1950 quotes (ppr default_ty),
1951 pprInstsInFull tidy_dicts]
1953 complainCheck doc givens irreds
1954 = mappM zonkInst given_dicts_and_ips `thenM` \ givens' ->
1955 mappM (addNoInstanceErrs doc givens') (groupInsts irreds) `thenM_`
1958 given_dicts_and_ips = filter (not . isMethod) givens
1959 -- Filter out methods, which are only added to
1960 -- the given set as an optimisation
1962 addNoInstanceErrs what_doc givens dicts
1963 = getDOpts `thenM` \ dflags ->
1964 tcGetInstEnv `thenM` \ inst_env ->
1966 (tidy_env1, tidy_givens) = tidyInsts givens
1967 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
1969 doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1970 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1972 ptext SLIT("Probable fix:"),
1976 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1977 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1980 -- The error message when we don't find a suitable instance
1981 -- is complicated by the fact that sometimes this is because
1982 -- there is no instance, and sometimes it's because there are
1983 -- too many instances (overlap). See the comments in TcEnv.lhs
1984 -- with the InstEnv stuff.
1987 | not ambig_overlap = empty
1989 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1990 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1991 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1993 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1994 ptext SLIT("to the") <+> what_doc]
1996 fix2 | null instance_dicts
1999 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
2001 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
2002 -- Insts for which it is worth suggesting an adding an instance declaration
2003 -- Exclude implicit parameters, and tyvar dicts
2005 -- Checks for the ambiguous case when we have overlapping instances
2006 ambig_overlap = any ambig_overlap1 dicts
2009 = case lookupInstEnv dflags inst_env clas tys of
2010 NoMatch ambig -> ambig
2014 (clas,tys) = getDictClassTys dict
2016 addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
2018 -- Used for the ...Thetas variants; all top level
2019 noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
2022 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2023 ptext SLIT("type variables that are not data type parameters"),
2024 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2026 reduceDepthErr n stack
2027 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2028 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2029 nest 4 (pprInstsInFull stack)]
2031 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
2033 -----------------------------------------------
2035 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
2036 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])