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 tcSimplifyThetas, tcSimplifyCheckThetas,
18 #include "HsVersions.h"
20 import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
21 import TcHsSyn ( TcExpr, TcId,
22 TcMonoBinds, TcDictBinds
26 import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
27 tyVarsOfInst, predsOfInsts, predsOfInst,
28 isDict, isClassDict, instName,
29 isStdClassTyVarDict, isMethodFor,
30 instToId, tyVarsOfInsts,
31 instBindingRequired, instCanBeGeneralised,
32 newDictsFromOld, instMentionsIPs,
33 getDictClassTys, isTyVarDict,
34 instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
35 Inst, LIE, pprInsts, pprInstsInFull,
38 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
39 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
41 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
42 import TcType ( ThetaType, PredType, mkClassPred, isOverloadedTy,
43 mkTyVarTy, tcGetTyVar, isTyVarClassPred,
44 tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
45 inheritablePred, predHasFDs )
47 import NameSet ( mkNameSet )
48 import Class ( classBigSig )
49 import FunDeps ( oclose, grow, improve, pprEquationDoc )
50 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
52 import Subst ( mkTopTyVarSubst, substTheta, substTy )
53 import TysWiredIn ( unitTy )
57 import ListSetOps ( equivClasses )
58 import Util ( zipEqual )
59 import List ( partition )
64 %************************************************************************
68 %************************************************************************
70 --------------------------------------
71 Notes on quantification
72 --------------------------------------
74 Suppose we are about to do a generalisation step.
79 C the constraints from that RHS
81 The game is to figure out
83 Q the set of type variables over which to quantify
84 Ct the constraints we will *not* quantify over
85 Cq the constraints we will quantify over
87 So we're going to infer the type
91 and float the constraints Ct further outwards.
93 Here are the things that *must* be true:
95 (A) Q intersect fv(G) = EMPTY limits how big Q can be
96 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
98 (A) says we can't quantify over a variable that's free in the
99 environment. (B) says we must quantify over all the truly free
100 variables in T, else we won't get a sufficiently general type. We do
101 not *need* to quantify over any variable that is fixed by the free
102 vars of the environment G.
104 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
106 Example: class H x y | x->y where ...
108 fv(G) = {a} C = {H a b, H c d}
111 (A) Q intersect {a} is empty
112 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
114 So Q can be {c,d}, {b,c,d}
116 Other things being equal, however, we'd like to quantify over as few
117 variables as possible: smaller types, fewer type applications, more
118 constraints can get into Ct instead of Cq.
121 -----------------------------------------
124 fv(T) the free type vars of T
126 oclose(vs,C) The result of extending the set of tyvars vs
127 using the functional dependencies from C
129 grow(vs,C) The result of extend the set of tyvars vs
130 using all conceivable links from C.
132 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
133 Then grow(vs,C) = {a,b,c}
135 Note that grow(vs,C) `superset` grow(vs,simplify(C))
136 That is, simplfication can only shrink the result of grow.
139 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
140 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
143 -----------------------------------------
147 Here's a good way to choose Q:
149 Q = grow( fv(T), C ) \ oclose( fv(G), C )
151 That is, quantify over all variable that that MIGHT be fixed by the
152 call site (which influences T), but which aren't DEFINITELY fixed by
153 G. This choice definitely quantifies over enough type variables,
154 albeit perhaps too many.
156 Why grow( fv(T), C ) rather than fv(T)? Consider
158 class H x y | x->y where ...
163 If we used fv(T) = {c} we'd get the type
165 forall c. H c d => c -> b
167 And then if the fn was called at several different c's, each of
168 which fixed d differently, we'd get a unification error, because
169 d isn't quantified. Solution: quantify d. So we must quantify
170 everything that might be influenced by c.
172 Why not oclose( fv(T), C )? Because we might not be able to see
173 all the functional dependencies yet:
175 class H x y | x->y where ...
176 instance H x y => Eq (T x y) where ...
181 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
182 apparent yet, and that's wrong. We must really quantify over d too.
185 There really isn't any point in quantifying over any more than
186 grow( fv(T), C ), because the call sites can't possibly influence
187 any other type variables.
191 --------------------------------------
193 --------------------------------------
195 It's very hard to be certain when a type is ambiguous. Consider
199 instance H x y => K (x,y)
201 Is this type ambiguous?
202 forall a b. (K (a,b), Eq b) => a -> a
204 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
205 now we see that a fixes b. So we can't tell about ambiguity for sure
206 without doing a full simplification. And even that isn't possible if
207 the context has some free vars that may get unified. Urgle!
209 Here's another example: is this ambiguous?
210 forall a b. Eq (T b) => a -> a
211 Not if there's an insance decl (with no context)
212 instance Eq (T b) where ...
214 You may say of this example that we should use the instance decl right
215 away, but you can't always do that:
217 class J a b where ...
218 instance J Int b where ...
220 f :: forall a b. J a b => a -> a
222 (Notice: no functional dependency in J's class decl.)
223 Here f's type is perfectly fine, provided f is only called at Int.
224 It's premature to complain when meeting f's signature, or even
225 when inferring a type for f.
229 However, we don't *need* to report ambiguity right away. It'll always
230 show up at the call site.... and eventually at main, which needs special
231 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
233 So here's the plan. We WARN about probable ambiguity if
235 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
237 (all tested before quantification).
238 That is, all the type variables in Cq must be fixed by the the variables
239 in the environment, or by the variables in the type.
241 Notice that we union before calling oclose. Here's an example:
243 class J a b c | a b -> c
247 forall b c. (J a b c) => b -> b
249 Only if we union {a} from G with {b} from T before using oclose,
250 do we see that c is fixed.
252 It's a bit vague exactly which C we should use for this oclose call. If we
253 don't fix enough variables we might complain when we shouldn't (see
254 the above nasty example). Nothing will be perfect. That's why we can
255 only issue a warning.
258 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
260 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
262 then c is a "bubble"; there's no way it can ever improve, and it's
263 certainly ambiguous. UNLESS it is a constant (sigh). And what about
268 instance H x y => K (x,y)
270 Is this type ambiguous?
271 forall a b. (K (a,b), Eq b) => a -> a
273 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
274 is a "bubble" that's a set of constraints
276 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
278 Hence another idea. To decide Q start with fv(T) and grow it
279 by transitive closure in Cq (no functional dependencies involved).
280 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
281 The definitely-ambiguous can then float out, and get smashed at top level
282 (which squashes out the constants, like Eq (T a) above)
285 --------------------------------------
286 Notes on principal types
287 --------------------------------------
292 f x = let g y = op (y::Int) in True
294 Here the principal type of f is (forall a. a->a)
295 but we'll produce the non-principal type
296 f :: forall a. C Int => a -> a
299 --------------------------------------
300 Notes on implicit parameters
301 --------------------------------------
303 Question 1: can we "inherit" implicit parameters
304 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
309 where f is *not* a top-level binding.
310 From the RHS of f we'll get the constraint (?y::Int).
311 There are two types we might infer for f:
315 (so we get ?y from the context of f's definition), or
317 f :: (?y::Int) => Int -> Int
319 At first you might think the first was better, becuase then
320 ?y behaves like a free variable of the definition, rather than
321 having to be passed at each call site. But of course, the WHOLE
322 IDEA is that ?y should be passed at each call site (that's what
323 dynamic binding means) so we'd better infer the second.
325 BOTTOM LINE: you *must* quantify over implicit parameters. See
326 isFreeAndInheritable.
328 BUT WATCH OUT: for *expressions*, this isn't right. Consider:
332 This is perfectly reasonable. We do not want to insist on
334 (?x + 1) :: (?x::Int => Int)
336 That would be silly. Here, the definition site *is* the occurrence site,
337 so the above strictures don't apply. Hence the difference between
338 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
339 and tcSimplifyCheckBind (which does not).
342 Question 2: type signatures
343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
344 OK, so is it legal to give an explicit, user type signature to f, thus:
349 At first sight this seems reasonable, but it has the nasty property
350 that adding a type signature changes the dynamic semantics.
353 (let f x = (x::Int) + ?y
354 in (f 3, f 3 with ?y=5)) with ?y = 6
360 in (f 3, f 3 with ?y=5)) with ?y = 6
364 Indeed, simply inlining f (at the Haskell source level) would change the
367 Conclusion: the above type signature is illegal. You'll get a message
368 of the form "could not deduce (?y::Int) from ()".
371 Question 3: monomorphism
372 ~~~~~~~~~~~~~~~~~~~~~~~~
373 There's a nasty corner case when the monomorphism restriction bites:
377 The argument above suggests that we *must* generalise
378 over the ?y parameter, to get
379 z :: (?y::Int) => Int,
380 but the monomorphism restriction says that we *must not*, giving
382 Why does the momomorphism restriction say this? Because if you have
384 let z = x + ?y in z+z
386 you might not expect the addition to be done twice --- but it will if
387 we follow the argument of Question 2 and generalise over ?y.
393 (A) Always generalise over implicit parameters
394 Bindings that fall under the monomorphism restriction can't
398 * Inlining remains valid
399 * No unexpected loss of sharing
400 * But simple bindings like
402 will be rejected, unless you add an explicit type signature
403 (to avoid the monomorphism restriction)
404 z :: (?y::Int) => Int
406 This seems unacceptable
408 (B) Monomorphism restriction "wins"
409 Bindings that fall under the monomorphism restriction can't
411 Always generalise over implicit parameters *except* for bindings
412 that fall under the monomorphism restriction
415 * Inlining isn't valid in general
416 * No unexpected loss of sharing
417 * Simple bindings like
419 accepted (get value of ?y from binding site)
421 (C) Always generalise over implicit parameters
422 Bindings that fall under the monomorphism restriction can't
423 be generalised, EXCEPT for implicit parameters
425 * Inlining remains valid
426 * Unexpected loss of sharing (from the extra generalisation)
427 * Simple bindings like
429 accepted (get value of ?y from occurrence sites)
434 None of these choices seems very satisfactory. But at least we should
435 decide which we want to do.
437 It's really not clear what is the Right Thing To Do. If you see
441 would you expect the value of ?y to be got from the *occurrence sites*
442 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
443 case of function definitions, the answer is clearly the former, but
444 less so in the case of non-fucntion definitions. On the other hand,
445 if we say that we get the value of ?y from the definition site of 'z',
446 then inlining 'z' might change the semantics of the program.
448 Choice (C) really says "the monomorphism restriction doesn't apply
449 to implicit parameters". Which is fine, but remember that every
450 innocent binding 'x = ...' that mentions an implicit parameter in
451 the RHS becomes a *function* of that parameter, called at each
452 use of 'x'. Now, the chances are that there are no intervening 'with'
453 clauses that bind ?y, so a decent compiler should common up all
454 those function calls. So I think I strongly favour (C). Indeed,
455 one could make a similar argument for abolishing the monomorphism
456 restriction altogether.
458 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
462 %************************************************************************
464 \subsection{tcSimplifyInfer}
466 %************************************************************************
468 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
470 1. Compute Q = grow( fvs(T), C )
472 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
473 predicates will end up in Ct; we deal with them at the top level
475 3. Try improvement, using functional dependencies
477 4. If Step 3 did any unification, repeat from step 1
478 (Unification can change the result of 'grow'.)
480 Note: we don't reduce dictionaries in step 2. For example, if we have
481 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
482 after step 2. However note that we may therefore quantify over more
483 type variables than we absolutely have to.
485 For the guts, we need a loop, that alternates context reduction and
486 improvement with unification. E.g. Suppose we have
488 class C x y | x->y where ...
490 and tcSimplify is called with:
492 Then improvement unifies a with b, giving
495 If we need to unify anything, we rattle round the whole thing all over
502 -> TcTyVarSet -- fv(T); type vars
504 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
506 TcDictBinds, -- Bindings
507 [TcId]) -- Dict Ids that must be bound here (zonked)
512 tcSimplifyInfer doc tau_tvs wanted_lie
513 = inferLoop doc (varSetElems tau_tvs)
514 (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
516 -- Check for non-generalisable insts
517 mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
519 returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
521 inferLoop doc tau_tvs wanteds
523 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
524 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
525 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
527 preds = predsOfInsts wanteds'
528 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
531 | isFreeAndInheritable qtvs inst = Free
532 | isClassDict inst = DontReduceUnlessConstant -- Dicts
533 | otherwise = ReduceMe -- Lits and Methods
536 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
539 if no_improvement then
540 returnTc (varSetElems qtvs, frees, binds, irreds)
542 -- If improvement did some unification, we go round again. There
543 -- are two subtleties:
544 -- a) We start again with irreds, not wanteds
545 -- Using an instance decl might have introduced a fresh type variable
546 -- which might have been unified, so we'd get an infinite loop
547 -- if we started again with wanteds! See example [LOOP]
549 -- b) It's also essential to re-process frees, because unification
550 -- might mean that a type variable that looked free isn't now.
552 -- Hence the (irreds ++ frees)
554 -- However, NOTICE that when we are done, we might have some bindings, but
555 -- the final qtvs might be empty. See [NO TYVARS] below.
557 inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
558 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
563 class If b t e r | b t e -> r
566 class Lte a b c | a b -> c where lte :: a -> b -> c
568 instance (Lte a b l,If l b a c) => Max a b c
570 Wanted: Max Z (S x) y
572 Then we'll reduce using the Max instance to:
573 (Lte Z (S x) l, If l (S x) Z y)
574 and improve by binding l->T, after which we can do some reduction
575 on both the Lte and If constraints. What we *can't* do is start again
576 with (Max Z (S x) y)!
580 class Y a b | a -> b where
583 instance Y [[a]] a where
586 k :: X a -> X a -> X a
588 g :: Num a => [X a] -> [X a]
591 h ys = ys ++ map (k (y [[0]])) xs
593 The excitement comes when simplifying the bindings for h. Initially
594 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
595 From this we get t1:=:t2, but also various bindings. We can't forget
596 the bindings (because of [LOOP]), but in fact t1 is what g is
599 The net effect of [NO TYVARS]
602 isFreeAndInheritable qtvs inst
603 = isFree qtvs inst -- Constrains no quantified vars
604 && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
605 -- (see "Notes on implicit parameters")
608 = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
612 %************************************************************************
614 \subsection{tcSimplifyCheck}
616 %************************************************************************
618 @tcSimplifyCheck@ is used when we know exactly the set of variables
619 we are going to quantify over. For example, a class or instance declaration.
624 -> [TcTyVar] -- Quantify over these
628 TcDictBinds) -- Bindings
630 -- tcSimplifyCheck is used when checking exprssion type signatures,
631 -- class decls, instance decls etc.
632 -- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
633 -- It's important that we can float out non-inheritable predicates
634 -- Example: (?x :: Int) is ok!
635 tcSimplifyCheck doc qtvs givens wanted_lie
636 = tcSimplCheck doc isFree get_qtvs
637 givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
638 returnTc (frees, binds)
640 get_qtvs = zonkTcTyVarsAndFV qtvs
643 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
644 -- against, but we don't know the type variables over which we are going to quantify.
645 -- This happens when we have a type signature for a mutually recursive group
648 -> TcTyVarSet -- fv(T)
651 -> TcM ([TcTyVar], -- Variables over which to quantify
653 TcDictBinds) -- Bindings
655 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
656 = tcSimplCheck doc isFreeAndInheritable get_qtvs givens wanted_lie
658 -- Figure out which type variables to quantify over
659 -- You might think it should just be the signature tyvars,
660 -- but in bizarre cases you can get extra ones
661 -- f :: forall a. Num a => a -> a
662 -- f x = fst (g (x, head [])) + 1
664 -- Here we infer g :: forall a b. a -> b -> (b,a)
665 -- We don't want g to be monomorphic in b just because
666 -- f isn't quantified over b.
667 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
669 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenNF_Tc` \ all_tvs' ->
670 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
672 qtvs = all_tvs' `minusVarSet` gbl_tvs
673 -- We could close gbl_tvs, but its not necessary for
674 -- soundness, and it'll only affect which tyvars, not which
675 -- dictionaries, we quantify over
680 Here is the workhorse function for all three wrappers.
683 tcSimplCheck doc is_free get_qtvs givens wanted_lie
684 = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
686 -- Complain about any irreducible ones
687 complainCheck doc givens irreds `thenNF_Tc_`
690 returnTc (qtvs, mkLIE frees, binds)
693 check_loop givens wanteds
695 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
696 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
697 get_qtvs `thenNF_Tc` \ qtvs' ->
701 -- When checking against a given signature we always reduce
702 -- until we find a match against something given, or can't reduce
703 try_me inst | is_free qtvs' inst = Free
704 | otherwise = ReduceMe
706 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
709 if no_improvement then
710 returnTc (varSetElems qtvs', frees, binds, irreds)
712 check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
713 returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
717 %************************************************************************
719 \subsection{tcSimplifyRestricted}
721 %************************************************************************
724 tcSimplifyRestricted -- Used for restricted binding groups
725 -- i.e. ones subject to the monomorphism restriction
727 -> TcTyVarSet -- Free in the type of the RHSs
728 -> LIE -- Free in the RHSs
729 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
731 TcDictBinds) -- Bindings
733 tcSimplifyRestricted doc tau_tvs wanted_lie
734 = -- First squash out all methods, to find the constrained tyvars
735 -- We can't just take the free vars of wanted_lie because that'll
736 -- have methods that may incidentally mention entirely unconstrained variables
737 -- e.g. a call to f :: Eq a => a -> b -> b
738 -- Here, b is unconstrained. A good example would be
740 -- We want to infer the polymorphic type
741 -- foo :: forall b. b -> b
743 wanteds = lieToList wanted_lie
744 try_me inst = ReduceMe -- Reduce as far as we can. Don't stop at
745 -- dicts; the idea is to get rid of as many type
746 -- variables as possible, and we don't want to stop
747 -- at (say) Monad (ST s), because that reduces
748 -- immediately, with no constraint on s.
750 simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
752 -- Next, figure out the tyvars we will quantify over
753 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
754 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
756 constrained_tvs = tyVarsOfInsts constrained_dicts
757 qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
758 `minusVarSet` constrained_tvs
761 -- The first step may have squashed more methods than
762 -- necessary, so try again, this time knowing the exact
763 -- set of type variables to quantify over.
765 -- We quantify only over constraints that are captured by qtvs;
766 -- these will just be a subset of non-dicts. This in contrast
767 -- to normal inference (using isFreeAndInheritable) in which we quantify over
768 -- all *non-inheritable* constraints too. This implements choice
769 -- (B) under "implicit parameter and monomorphism" above.
770 mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
772 try_me inst | isFree qtvs inst = Free
773 | otherwise = ReduceMe
775 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
776 ASSERT( no_improvement )
777 ASSERT( null irreds )
778 -- No need to loop because simpleReduceLoop will have
779 -- already done any improvement necessary
781 returnTc (varSetElems qtvs, mkLIE frees, binds)
785 %************************************************************************
787 \subsection{tcSimplifyToDicts}
789 %************************************************************************
791 On the LHS of transformation rules we only simplify methods and constants,
792 getting dictionaries. We want to keep all of them unsimplified, to serve
793 as the available stuff for the RHS of the rule.
795 The same thing is used for specialise pragmas. Consider
798 {-# SPECIALISE f :: Int -> Int #-}
801 The type checker generates a binding like:
803 f_spec = (f :: Int -> Int)
805 and we want to end up with
807 f_spec = _inline_me_ (f Int dNumInt)
809 But that means that we must simplify the Method for f to (f Int dNumInt)!
810 So tcSimplifyToDicts squeezes out all Methods.
812 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
814 fromIntegral :: (Integral a, Num b) => a -> b
815 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
817 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
821 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
823 because the scsel will mess up matching. Instead we want
825 forall dIntegralInt, dNumInt.
826 fromIntegral Int Int dIntegralInt dNumInt = id Int
828 Hence "DontReduce NoSCs"
831 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
832 tcSimplifyToDicts wanted_lie
833 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
834 -- Since try_me doesn't look at types, we don't need to
835 -- do any zonking, so it's safe to call reduceContext directly
837 returnTc (irreds, binds)
840 doc = text "tcSimplifyToDicts"
841 wanteds = lieToList wanted_lie
843 -- Reduce methods and lits only; stop as soon as we get a dictionary
844 try_me inst | isDict inst = DontReduce NoSCs
845 | otherwise = ReduceMe
849 %************************************************************************
851 \subsection{Filtering at a dynamic binding}
853 %************************************************************************
858 we must discharge all the ?x constraints from B. We also do an improvement
859 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
861 Actually, the constraints from B might improve the types in ?x. For example
863 f :: (?x::Int) => Char -> Char
866 then the constraint (?x::Int) arising from the call to f will
867 force the binding for ?x to be of type Int.
870 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
872 -> TcM (LIE, TcDictBinds)
873 tcSimplifyIPs given_ips wanted_lie
874 = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
875 returnTc (mkLIE frees, binds)
877 doc = text "tcSimplifyIPs" <+> ppr ip_names
878 wanteds = lieToList wanted_lie
879 ip_names = map instName given_ips
880 ip_set = mkNameSet ip_names
882 -- Simplify any methods that mention the implicit parameter
883 try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
886 simpl_loop givens wanteds
887 = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
888 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
890 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
892 if no_improvement then
893 ASSERT( null irreds )
894 returnTc (frees, binds)
896 simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
897 returnTc (frees1, binds `AndMonoBinds` binds1)
901 %************************************************************************
903 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
905 %************************************************************************
907 When doing a binding group, we may have @Insts@ of local functions.
908 For example, we might have...
910 let f x = x + 1 -- orig local function (overloaded)
911 f.1 = f Int -- two instances of f
916 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
917 where @f@ is in scope; those @Insts@ must certainly not be passed
918 upwards towards the top-level. If the @Insts@ were binding-ified up
919 there, they would have unresolvable references to @f@.
921 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
922 For each method @Inst@ in the @init_lie@ that mentions one of the
923 @Ids@, we create a binding. We return the remaining @Insts@ (in an
924 @LIE@), as well as the @HsBinds@ generated.
927 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
929 bindInstsOfLocalFuns init_lie local_ids
930 | null overloaded_ids
932 = returnTc (init_lie, EmptyMonoBinds)
935 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
936 ASSERT( null irreds )
937 returnTc (mkLIE frees, binds)
939 doc = text "bindInsts" <+> ppr local_ids
940 wanteds = lieToList init_lie
941 overloaded_ids = filter is_overloaded local_ids
942 is_overloaded id = isOverloadedTy (idType id)
944 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
945 -- so it's worth building a set, so that
946 -- lookup (in isMethodFor) is faster
948 try_me inst | isMethodFor overloaded_set inst = ReduceMe
953 %************************************************************************
955 \subsection{Data types for the reduction mechanism}
957 %************************************************************************
959 The main control over context reduction is here
963 = ReduceMe -- Try to reduce this
964 -- If there's no instance, behave exactly like
965 -- DontReduce: add the inst to
966 -- the irreductible ones, but don't
967 -- produce an error message of any kind.
968 -- It might be quite legitimate such as (Eq a)!
970 | DontReduce WantSCs -- Return as irreducible
972 | DontReduceUnlessConstant -- Return as irreducible unless it can
973 -- be reduced to a constant in one step
975 | Free -- Return as free
977 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
978 -- of a predicate when adding it to the avails
984 type RedState = (Avails, -- What's available
985 [Inst]) -- Insts for which try_me returned Free
987 type Avails = FiniteMap Inst Avail
990 = Irred -- Used for irreducible dictionaries,
991 -- which are going to be lambda bound
993 | BoundTo TcId -- Used for dictionaries for which we have a binding
994 -- e.g. those "given" in a signature
996 | NoRhs -- Used for Insts like (CCallable f)
997 -- where no witness is required.
999 | Rhs -- Used when there is a RHS
1001 [Inst] -- Insts free in the RHS; we need these too
1003 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
1004 | (inst,avail) <- fmToList avails ]
1006 instance Outputable Avail where
1009 pprAvail NoRhs = text "<no rhs>"
1010 pprAvail Irred = text "Irred"
1011 pprAvail (BoundTo x) = text "Bound to" <+> ppr x
1012 pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
1015 Extracting the bindings from a bunch of Avails.
1016 The bindings do *not* come back sorted in dependency order.
1017 We assume that they'll be wrapped in a big Rec, so that the
1018 dependency analyser can sort them out later
1022 bindsAndIrreds :: Avails
1024 -> (TcDictBinds, -- Bindings
1025 [Inst]) -- Irreducible ones
1027 bindsAndIrreds avails wanteds
1028 = go avails EmptyMonoBinds [] wanteds
1030 go avails binds irreds [] = (binds, irreds)
1032 go avails binds irreds (w:ws)
1033 = case lookupFM avails w of
1034 Nothing -> -- Free guys come out here
1035 -- (If we didn't do addFree we could use this as the
1036 -- criterion for free-ness, and pick up the free ones here too)
1037 go avails binds irreds ws
1039 Just NoRhs -> go avails binds irreds ws
1041 Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
1043 Just (BoundTo id) -> go avails new_binds irreds ws
1045 -- For implicit parameters, all occurrences share the same
1046 -- Id, so there is no need for synonym bindings
1047 new_binds | new_id == id = binds
1048 | otherwise = addBind binds new_id (HsVar id)
1051 Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
1054 avails' = addToFM avails w (BoundTo id)
1056 addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
1060 %************************************************************************
1062 \subsection[reduce]{@reduce@}
1064 %************************************************************************
1066 When the "what to do" predicate doesn't depend on the quantified type variables,
1067 matters are easier. We don't need to do any zonking, unless the improvement step
1068 does something, in which case we zonk before iterating.
1070 The "given" set is always empty.
1073 simpleReduceLoop :: SDoc
1074 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1076 -> TcM ([Inst], -- Free
1078 [Inst]) -- Irreducible
1080 simpleReduceLoop doc try_me wanteds
1081 = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
1082 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
1083 if no_improvement then
1084 returnTc (frees, binds, irreds)
1086 simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
1087 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1093 reduceContext :: SDoc
1094 -> (Inst -> WhatToDo)
1097 -> NF_TcM (Bool, -- True <=> improve step did no unification
1099 TcDictBinds, -- Dictionary bindings
1100 [Inst]) -- Irreducible
1102 reduceContext doc try_me givens wanteds
1104 traceTc (text "reduceContext" <+> (vcat [
1105 text "----------------------",
1107 text "given" <+> ppr givens,
1108 text "wanted" <+> ppr wanteds,
1109 text "----------------------"
1112 -- Build the Avail mapping from "givens"
1113 foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
1116 reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
1118 -- Do improvement, using everything in avails
1119 -- In particular, avails includes all superclasses of everything
1120 tcImprove avails `thenTc` \ no_improvement ->
1122 traceTc (text "reduceContext end" <+> (vcat [
1123 text "----------------------",
1125 text "given" <+> ppr givens,
1126 text "wanted" <+> ppr wanteds,
1128 text "avails" <+> pprAvails avails,
1129 text "frees" <+> ppr frees,
1130 text "no_improvement =" <+> ppr no_improvement,
1131 text "----------------------"
1134 (binds, irreds) = bindsAndIrreds avails wanteds
1136 returnTc (no_improvement, frees, binds, irreds)
1139 = tcGetInstEnv `thenTc` \ inst_env ->
1141 preds = [ (pred, pp_loc)
1142 | inst <- keysFM avails,
1143 let pp_loc = pprInstLoc (instLoc inst),
1144 pred <- predsOfInst inst,
1147 -- Avails has all the superclasses etc (good)
1148 -- It also has all the intermediates of the deduction (good)
1149 -- It does not have duplicates (good)
1150 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1151 -- so that improve will see them separate
1152 eqns = improve (classInstEnv inst_env) preds
1157 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
1158 mapTc_ unify eqns `thenTc_`
1161 unify ((qtvs, t1, t2), doc)
1162 = tcAddErrCtxt doc $
1163 tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
1164 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1167 The main context-reduction function is @reduce@. Here's its game plan.
1170 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1171 -- along with its depth
1172 -> (Inst -> WhatToDo)
1179 try_me: given an inst, this function returns
1181 DontReduce return this in "irreds"
1182 Free return this in "frees"
1184 wanteds: The list of insts to reduce
1185 state: An accumulating parameter of type RedState
1186 that contains the state of the algorithm
1188 It returns a RedState.
1190 The (n,stack) pair is just used for error reporting.
1191 n is always the depth of the stack.
1192 The stack is the stack of Insts being reduced: to produce X
1193 I had to produce Y, to produce Y I had to produce Z, and so on.
1196 reduceList (n,stack) try_me wanteds state
1197 | n > opt_MaxContextReductionDepth
1198 = failWithTc (reduceDepthErr n stack)
1204 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1209 go [] state = returnTc state
1210 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
1213 -- Base case: we're done!
1214 reduce stack try_me wanted state
1215 -- It's the same as an existing inst, or a superclass thereof
1216 | isAvailable state wanted
1220 = case try_me wanted of {
1222 DontReduce want_scs -> addIrred want_scs state wanted
1224 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1225 -- First, see if the inst can be reduced to a constant in one step
1226 try_simple (addIrred AddSCs) -- Assume want superclasses
1228 ; Free -> -- It's free so just chuck it upstairs
1229 -- First, see if the inst can be reduced to a constant in one step
1232 ; ReduceMe -> -- It should be reduced
1233 lookupInst wanted `thenNF_Tc` \ lookup_result ->
1234 case lookup_result of
1235 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
1236 addWanted state' wanted rhs wanteds'
1237 SimpleInst rhs -> addWanted state wanted rhs []
1239 NoInstance -> -- No such instance!
1240 -- Add it and its superclasses
1241 addIrred AddSCs state wanted
1245 try_simple do_this_otherwise
1246 = lookupInst wanted `thenNF_Tc` \ lookup_result ->
1247 case lookup_result of
1248 SimpleInst rhs -> addWanted state wanted rhs []
1249 other -> do_this_otherwise state wanted
1254 isAvailable :: RedState -> Inst -> Bool
1255 isAvailable (avails, _) wanted = wanted `elemFM` avails
1256 -- NB: the Ord instance of Inst compares by the class/type info
1257 -- *not* by unique. So
1258 -- d1::C Int == d2::C Int
1260 -------------------------
1261 addFree :: RedState -> Inst -> NF_TcM RedState
1262 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1263 -- to avails, so that any other equal Insts will be commoned up right
1264 -- here rather than also being tossed upstairs. This is really just
1265 -- an optimisation, and perhaps it is more trouble that it is worth,
1266 -- as the following comments show!
1268 -- NB1: do *not* add superclasses. If we have
1271 -- but a is not bound here, then we *don't* want to derive
1272 -- dn from df here lest we lose sharing.
1274 -- NB2: do *not* add the Inst to avails at all if it's a method.
1275 -- The following situation shows why this is bad:
1276 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1277 -- From an application (truncate f i) we get
1278 -- t1 = truncate at f
1280 -- If we have also have a second occurrence of truncate, we get
1281 -- t3 = truncate at f
1283 -- When simplifying with i,f free, we might still notice that
1284 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1285 -- will continue to float out!
1286 -- Solution: never put methods in avail till they are captured
1287 -- in which case addFree isn't used
1289 -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1290 -- than BoundTo, else we end up with bogus bindings.
1291 -- c.f. instBindingRequired in addWanted
1292 addFree (avails, frees) free
1293 | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1294 | otherwise = returnNF_Tc (avails, free:frees)
1296 avail | instBindingRequired free = BoundTo (instToId free)
1299 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1300 addWanted state@(avails, frees) wanted rhs_expr wanteds
1301 -- Do *not* add superclasses as well. Here's an example of why not
1302 -- class Eq a => Foo a b
1303 -- instance Eq a => Foo [a] a
1304 -- If we are reducing
1306 -- we'll first deduce that it holds (via the instance decl). We
1307 -- must not then overwrite the Eq t constraint with a superclass selection!
1308 -- ToDo: this isn't entirely unsatisfactory, because
1309 -- we may also lose some entirely-legitimate sharing this way
1311 = ASSERT( not (isAvailable state wanted) )
1312 returnNF_Tc (addToFM avails wanted avail, frees)
1314 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1315 | otherwise = ASSERT( null wanteds ) NoRhs
1317 addGiven :: RedState -> Inst -> NF_TcM RedState
1318 addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
1320 addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
1321 addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
1322 addIrred AddSCs state irred = addAvailAndSCs state irred Irred
1324 addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
1325 addAvailAndSCs (avails, frees) wanted avail
1326 = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
1327 returnNF_Tc (avails', frees)
1329 ---------------------
1330 add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
1331 add_avail_and_scs avails wanted avail
1332 = add_scs (addToFM avails wanted avail) wanted
1334 add_scs :: Avails -> Inst -> NF_TcM Avails
1335 -- Add all the superclasses of the Inst to Avails
1336 -- Invariant: the Inst is already in Avails.
1339 | not (isClassDict dict)
1340 = returnNF_Tc avails
1342 | otherwise -- It is a dictionary
1343 = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
1344 foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1346 (clas, tys) = getDictClassTys dict
1347 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1348 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1350 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1351 = case lookupFM avails sc_dict of
1352 Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
1353 other -> add_avail_and_scs avails sc_dict avail
1355 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1356 avail = Rhs sc_sel_rhs [dict]
1359 Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
1360 and want to deduce (d2:C [a]) where
1362 class Ord a => C a where
1363 instance Ord a => C [a] where ...
1365 Then we'll use the instance decl to deduce C [a] and then add the
1366 superclasses of C [a] to avails. But we must not overwrite the binding
1367 for d1:Ord a (which is given) with a superclass selection or we'll just
1368 build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
1372 %************************************************************************
1374 \section{tcSimplifyTop: defaulting}
1376 %************************************************************************
1379 If a dictionary constrains a type variable which is
1380 * not mentioned in the environment
1381 * and not mentioned in the type of the expression
1382 then it is ambiguous. No further information will arise to instantiate
1383 the type variable; nor will it be generalised and turned into an extra
1384 parameter to a function.
1386 It is an error for this to occur, except that Haskell provided for
1387 certain rules to be applied in the special case of numeric types.
1389 * at least one of its classes is a numeric class, and
1390 * all of its classes are numeric or standard
1391 then the type variable can be defaulted to the first type in the
1392 default-type list which is an instance of all the offending classes.
1394 So here is the function which does the work. It takes the ambiguous
1395 dictionaries and either resolves them (producing bindings) or
1396 complains. It works by splitting the dictionary list by type
1397 variable, and using @disambigOne@ to do the real business.
1399 @tcSimplifyTop@ is called once per module to simplify all the constant
1400 and ambiguous Insts.
1402 We need to be careful of one case. Suppose we have
1404 instance Num a => Num (Foo a b) where ...
1406 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1407 to (Num x), and default x to Int. But what about y??
1409 It's OK: the final zonking stage should zap y to (), which is fine.
1413 tcSimplifyTop :: LIE -> TcM TcDictBinds
1414 tcSimplifyTop wanted_lie
1415 = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1416 ASSERT( null frees )
1419 -- All the non-std ones are definite errors
1420 (stds, non_stds) = partition isStdClassTyVarDict irreds
1422 -- Group by type variable
1423 std_groups = equivClasses cmp_by_tyvar stds
1425 -- Pick the ones which its worth trying to disambiguate
1426 (std_oks, std_bads) = partition worth_a_try std_groups
1428 -- Have a try at disambiguation
1429 -- if the type variable isn't bound
1430 -- up with one of the non-standard classes
1431 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1432 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1434 -- Collect together all the bad guys
1435 bad_guys = non_stds ++ concat std_bads
1437 -- Disambiguate the ones that look feasible
1438 mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
1440 -- And complain about the ones that don't
1441 -- This group includes both non-existent instances
1442 -- e.g. Num (IO a) and Eq (Int -> Int)
1443 -- and ambiguous dictionaries
1445 addTopAmbigErrs bad_guys `thenNF_Tc_`
1447 returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1449 wanteds = lieToList wanted_lie
1450 try_me inst = ReduceMe
1452 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1454 get_tv d = case getDictClassTys d of
1455 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1456 get_clas d = case getDictClassTys d of
1457 (clas, [ty]) -> clas
1460 @disambigOne@ assumes that its arguments dictionaries constrain all
1461 the same type variable.
1463 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1464 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1465 the most common use of defaulting is code like:
1467 _ccall_ foo `seqPrimIO` bar
1469 Since we're not using the result of @foo@, the result if (presumably)
1473 disambigGroup :: [Inst] -- All standard classes of form (C a)
1477 | any isNumericClass classes -- Guaranteed all standard classes
1478 -- see comment at the end of function for reasons as to
1479 -- why the defaulting mechanism doesn't apply to groups that
1480 -- include CCallable or CReturnable dicts.
1481 && not (any isCcallishClass classes)
1482 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1483 -- SO, TRY DEFAULT TYPES IN ORDER
1485 -- Failure here is caused by there being no type in the
1486 -- default list which can satisfy all the ambiguous classes.
1487 -- For example, if Real a is reqd, but the only type in the
1488 -- default list is Int.
1489 tcGetDefaultTys `thenNF_Tc` \ default_tys ->
1491 try_default [] -- No defaults work, so fail
1494 try_default (default_ty : default_tys)
1495 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1496 -- default_tys instead
1497 tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
1500 theta = [mkClassPred clas [default_ty] | clas <- classes]
1502 -- See if any default works, and if so bind the type variable to it
1503 -- If not, add an AmbigErr
1504 recoverTc (addAmbigErrs dicts `thenNF_Tc_`
1505 returnTc EmptyMonoBinds) $
1507 try_default default_tys `thenTc` \ chosen_default_ty ->
1509 -- Bind the type variable and reduce the context, for real this time
1510 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
1511 simpleReduceLoop (text "disambig" <+> ppr dicts)
1512 try_me dicts `thenTc` \ (frees, binds, ambigs) ->
1513 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1514 warnDefault dicts chosen_default_ty `thenTc_`
1517 | all isCreturnableClass classes
1518 = -- Default CCall stuff to (); we don't even both to check that () is an
1519 -- instance of CReturnable, because we know it is.
1520 unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
1521 returnTc EmptyMonoBinds
1523 | otherwise -- No defaults
1524 = addAmbigErrs dicts `thenNF_Tc_`
1525 returnTc EmptyMonoBinds
1528 try_me inst = ReduceMe -- This reduce should not fail
1529 tyvar = get_tv (head dicts) -- Should be non-empty
1530 classes = map get_clas dicts
1533 [Aside - why the defaulting mechanism is turned off when
1534 dealing with arguments and results to ccalls.
1536 When typechecking _ccall_s, TcExpr ensures that the external
1537 function is only passed arguments (and in the other direction,
1538 results) of a restricted set of 'native' types. This is
1539 implemented via the help of the pseudo-type classes,
1540 @CReturnable@ (CR) and @CCallable@ (CC.)
1542 The interaction between the defaulting mechanism for numeric
1543 values and CC & CR can be a bit puzzling to the user at times.
1552 What type has 'x' got here? That depends on the default list
1553 in operation, if it is equal to Haskell 98's default-default
1554 of (Integer, Double), 'x' has type Double, since Integer
1555 is not an instance of CR. If the default list is equal to
1556 Haskell 1.4's default-default of (Int, Double), 'x' has type
1559 To try to minimise the potential for surprises here, the
1560 defaulting mechanism is turned off in the presence of
1561 CCallable and CReturnable.
1566 %************************************************************************
1568 \subsection[simple]{@Simple@ versions}
1570 %************************************************************************
1572 Much simpler versions when there are no bindings to make!
1574 @tcSimplifyThetas@ simplifies class-type constraints formed by
1575 @deriving@ declarations and when specialising instances. We are
1576 only interested in the simplified bunch of class/type constraints.
1578 It simplifies to constraints of the form (C a b c) where
1579 a,b,c are type variables. This is required for the context of
1580 instance declarations.
1583 tcSimplifyThetas :: ThetaType -- Wanted
1584 -> TcM ThetaType -- Needed
1586 tcSimplifyThetas wanteds
1587 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
1588 reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
1590 -- For multi-param Haskell, check that the returned dictionaries
1591 -- don't have any of the form (C Int Bool) for which
1592 -- we expect an instance here
1593 -- For Haskell 98, check that all the constraints are of the form C a,
1594 -- where a is a type variable
1595 bad_guys | glaExts = [pred | pred <- irreds,
1596 isEmptyVarSet (tyVarsOfPred pred)]
1597 | otherwise = [pred | pred <- irreds,
1598 not (isTyVarClassPred pred)]
1600 if null bad_guys then
1603 mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
1607 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1608 used with \tr{default} declarations. We are only interested in
1609 whether it worked or not.
1612 tcSimplifyCheckThetas :: ThetaType -- Given
1613 -> ThetaType -- Wanted
1616 tcSimplifyCheckThetas givens wanteds
1617 = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
1621 mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
1627 type AvailsSimple = FiniteMap PredType Bool
1628 -- True => irreducible
1629 -- False => given, or can be derived from a given or from an irreducible
1631 reduceSimple :: ThetaType -- Given
1632 -> ThetaType -- Wanted
1633 -> NF_TcM ThetaType -- Irreducible
1635 reduceSimple givens wanteds
1636 = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
1637 returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
1639 givens_fm = foldl addNonIrred emptyFM givens
1641 reduce_simple :: (Int,ThetaType) -- Stack
1644 -> NF_TcM AvailsSimple
1646 reduce_simple (n,stack) avails wanteds
1649 go avails [] = returnNF_Tc avails
1650 go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
1653 reduce_simple_help stack givens wanted
1654 | wanted `elemFM` givens
1655 = returnNF_Tc givens
1657 | Just (clas, tys) <- getClassPredTys_maybe wanted
1658 = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
1660 Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
1661 Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1664 = returnNF_Tc (addSimpleIrred givens wanted)
1666 addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
1667 addSimpleIrred givens pred
1668 = addSCs (addToFM givens pred True) pred
1670 addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
1671 addNonIrred givens pred
1672 = addSCs (addToFM givens pred False) pred
1675 | not (isClassPred pred) = givens
1676 | otherwise = foldl add givens sc_theta
1678 Just (clas,tys) = getClassPredTys_maybe pred
1679 (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1680 sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1683 = case lookupFM givens ct of
1684 Nothing -> -- Add it and its superclasses
1685 addSCs (addToFM givens ct False) ct
1687 Just True -> -- Set its flag to False; superclasses already done
1688 addToFM givens ct False
1690 Just False -> -- Already done
1696 %************************************************************************
1698 \section{Errors and contexts}
1700 %************************************************************************
1702 ToDo: for these error messages, should we note the location as coming
1703 from the insts, or just whatever seems to be around in the monad just
1707 groupInsts :: [Inst] -> [[Inst]]
1708 -- Group together insts with the same origin
1709 -- We want to report them together in error messages
1711 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1713 -- (It may seem a bit crude to compare the error messages,
1714 -- but it makes sure that we combine just what the user sees,
1715 -- and it avoids need equality on InstLocs.)
1716 (friends, others) = partition is_friend insts
1717 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1718 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1721 addTopAmbigErrs dicts
1722 = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
1723 mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
1724 mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
1727 fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1728 (tidy_env, tidy_dicts) = tidyInsts dicts
1729 (bad_ips, non_ips) = partition is_ip tidy_dicts
1730 (no_insts, ambigs) = partition no_inst non_ips
1731 is_ip d = any isIPPred (predsOfInst d)
1732 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1735 plural xs = char 's'
1737 addTopIPErrs tidy_env tidy_dicts
1738 = addInstErrTcM (instLoc (head tidy_dicts))
1740 ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1742 -- Used for top-level irreducibles
1743 addTopInstanceErrs tidy_env tidy_dicts
1744 = addInstErrTcM (instLoc (head tidy_dicts))
1746 ptext SLIT("No instance") <> plural tidy_dicts <+>
1747 ptext SLIT("for") <+> pprInsts tidy_dicts)
1750 = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1752 (tidy_env, tidy_dicts) = tidyInsts dicts
1754 addAmbigErr tidy_env tidy_dict
1755 = addInstErrTcM (instLoc tidy_dict)
1757 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1758 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1760 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1762 warnDefault dicts default_ty
1763 = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
1764 tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1767 (_, tidy_dicts) = tidyInsts dicts
1768 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1769 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1770 quotes (ppr default_ty),
1771 pprInstsInFull tidy_dicts]
1773 complainCheck doc givens irreds
1774 = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
1775 mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
1778 given_dicts = filter isDict givens
1779 -- Filter out methods, which are only added to
1780 -- the given set as an optimisation
1782 addNoInstanceErrs what_doc givens dicts
1783 = tcGetInstEnv `thenNF_Tc` \ inst_env ->
1785 (tidy_env1, tidy_givens) = tidyInsts givens
1786 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
1788 doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1789 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1791 ptext SLIT("Probable fix:"),
1795 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1796 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1799 -- The error message when we don't find a suitable instance
1800 -- is complicated by the fact that sometimes this is because
1801 -- there is no instance, and sometimes it's because there are
1802 -- too many instances (overlap). See the comments in TcEnv.lhs
1803 -- with the InstEnv stuff.
1806 | not ambig_overlap = empty
1808 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1809 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1810 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1812 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1813 ptext SLIT("to the") <+> what_doc]
1815 fix2 | null instance_dicts
1818 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1820 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1821 -- Insts for which it is worth suggesting an adding an instance declaration
1822 -- Exclude implicit parameters, and tyvar dicts
1824 -- Checks for the ambiguous case when we have overlapping instances
1825 ambig_overlap = any ambig_overlap1 dicts
1828 = case lookupInstEnv inst_env clas tys of
1829 NoMatch ambig -> ambig
1833 (clas,tys) = getDictClassTys dict
1835 addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
1837 -- Used for the ...Thetas variants; all top level
1839 = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
1841 reduceDepthErr n stack
1842 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1843 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1844 nest 4 (pprInstsInFull stack)]
1846 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1848 -----------------------------------------------
1850 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1851 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])